<commit_before>//  Copyright (c) 2015 <NAME>. All rights reserved.

/// `Value` represents a form which cannot undergo further evaluation.
///
/// This makes it sort of like a `Term` in normal form, i.e. already evaluated.
public enum Value: DebugPrintable {
	// MARK: Constructors

	public static func pi(value: Value, _ f: Value -> Value) -> Value {
		return .Pi(Box(value), f)
	}

	public static func sigma(value: Value, _ f: Value -> Value) -> Value {
		return .Sigma(Box(value), f)
	}

	public static func forall(f: Value -> Value) -> Value {
		return .pi(.type, f)
	}

	public static func function(from: Value, _ to: Value) -> Value {
		return .pi(from, const(to))
	}

	public static func product(a: Value, _ b: Value) -> Value {
		return .sigma(a, const(b))
	}

	public static func product(types: [Value]) -> Value {
		return foldr(types, Value.UnitValue, Value.product)
	}

	public static func application(f: Manifold.Neutral, _ v: Value) -> Value {
		return .neutral(.application(f, v))
	}

	public static func free(name: Name) -> Value {
		return .neutral(.Free(name))
	}

	public static func neutral(value: Manifold.Neutral) -> Value {
		return .Neutral(Box(value))
	}

	public static var type: Value {
		return .Type(0)
	}

	public static func type(n: Int) -> Value {
		return .Type(n)
	}


	// MARK: Destructors

	public var isUnitValue: Bool {
		return analysis(
			ifUnitValue: const(true),
			otherwise: const(false))
	}

	public var isUnitType: Bool {
		return analysis(
			ifUnitType: const(true),
			otherwise: const(false))
	}

	public var isType: Bool {
		return analysis(
			ifType: const(true),
			otherwise: const(false))
	}

	public var pi: (Value, Value -> Value)? {
		return analysis(
			ifPi: unit,
			otherwise: const(nil))
	}

	public var sigma: (Value, Value -> Value)? {
		return analysis(
			ifSigma: unit,
			otherwise: const(nil))
	}

	public var neutral: Manifold.Neutral? {
		return analysis(
			ifNeutral: unit,
			otherwise: const(nil))
	}


	// MARK: Application

	public func apply(other: Value) -> Value {
		return analysis(
			ifPi: { _, f in f(other) },
			ifSigma: { _, f in f(other) },
			ifNeutral: { .neutral(.application($0, other)) },
			otherwise: { assert(false, "illegal application of \(self) to \(other)") ; return .type })
	}


	// MARK: Quotation

	public var quote: Term {
		return quote(0)
	}

	func quote(n: Int) -> Term {
		return analysis(
			ifUnitValue: const(.unitTerm),
			ifUnitType: const(.unitType),
			ifType: const(.type),
			ifPi: { type, f in
				Term(Checkable.Pi(Box(type.quote(n)), Box(f(.free(.Quote(n))).quote(n + 1))))
			},
			ifSigma: { type, f in
				Term(Checkable.Sigma(Box(type.quote(n)), Box(f(.free(.Quote(n))).quote(n + 1))))
			},
			ifNeutral: {
				$0.quote(n)
			})
	}


	// MARK: Analyses

	public func analysis<T>(
		@noescape #ifUnitValue: () -> T,
		@noescape ifUnitType: () -> T,
		@noescape ifType: Int -> T,
		@noescape ifPi: (Value, Value -> Value) -> T,
		@noescape ifSigma: (Value, Value -> Value) -> T,
		@noescape ifNeutral: Manifold.Neutral -> T) -> T {
		switch self {
		case .UnitValue:
			return ifUnitValue()<commit_msg>Type values are quoted to equivalent type terms.<commit_after>//  Copyright (c) 2015 <NAME>. All rights reserved.

/// `Value` represents a form which cannot undergo further evaluation.
///
/// This makes it sort of like a `Term` in normal form, i.e. already evaluated.
public enum Value: DebugPrintable {
	// MARK: Constructors

	public static func pi(value: Value, _ f: Value -> Value) -> Value {
		return .Pi(Box(value), f)
	}

	public static func sigma(value: Value, _ f: Value -> Value) -> Value {
		return .Sigma(Box(value), f)
	}

	public static func forall(f: Value -> Value) -> Value {
		return .pi(.type, f)
	}

	public static func function(from: Value, _ to: Value) -> Value {
		return .pi(from, const(to))
	}

	public static func product(a: Value, _ b: Value) -> Value {
		return .sigma(a, const(b))
	}

	public static func product(types: [Value]) -> Value {
		return foldr(types, Value.UnitValue, Value.product)
	}

	public static func application(f: Manifold.Neutral, _ v: Value) -> Value {
		return .neutral(.application(f, v))
	}

	public static func free(name: Name) -> Value {
		return .neutral(.Free(name))
	}

	public static func neutral(value: Manifold.Neutral) -> Value {
		return .Neutral(Box(value))
	}

	public static var type: Value {
		return .Type(0)
	}

	public static func type(n: Int) -> Value {
		return .Type(n)
	}


	// MARK: Destructors

	public var isUnitValue: Bool {
		return analysis(
			ifUnitValue: const(true),
			otherwise: const(false))
	}

	public var isUnitType: Bool {
		return analysis(
			ifUnitType: const(true),
			otherwise: const(false))
	}

	public var isType: Bool {
		return analysis(
			ifType: const(true),
			otherwise: const(false))
	}

	public var pi: (Value, Value -> Value)? {
		return analysis(
			ifPi: unit,
			otherwise: const(nil))
	}

	public var sigma: (Value, Value -> Value)? {
		return analysis(
			ifSigma: unit,
			otherwise: const(nil))
	}

	public var neutral: Manifold.Neutral? {
		return analysis(
			ifNeutral: unit,
			otherwise: const(nil))
	}


	// MARK: Application

	public func apply(other: Value) -> Value {
		return analysis(
			ifPi: { _, f in f(other) },
			ifSigma: { _, f in f(other) },
			ifNeutral: { .neutral(.application($0, other)) },
			otherwise: { assert(false, "illegal application of \(self) to \(other)") ; return .type })
	}


	// MARK: Quotation

	public var quote: Term {
		return quote(0)
	}

	func quote(n: Int) -> Term {
		return analysis(
			ifUnitValue: const(.unitTerm),
			ifUnitType: const(.unitType),
			ifType: Term.type,
			ifPi: { type, f in
				Term(Checkable.Pi(Box(type.quote(n)), Box(f(.free(.Quote(n))).quote(n + 1))))
			},
			ifSigma: { type, f in
				Term(Checkable.Sigma(Box(type.quote(n)), Box(f(.free(.Quote(n))).quote(n + 1))))
			},
			ifNeutral: {
				$0.quote(n)
			})
	}


	// MARK: Analyses

	public func analysis<T>(
		@noescape #ifUnitValue: () -> T,
		@noescape ifUnitType: () -> T,
		@noescape ifType: Int -> T,
		@noescape ifPi: (Value, Value -> Value) -> T,
		@noescape ifSigma: (Value, Value -> Value) -> T,
		@noescape ifNeutral: Manifold.Neutral -> T) -> T {
		switch self {
		case .UnitValue:
			return ifUnitValue()
{'fraction_non_alphanumeric': 0.15310015898251192, 'fraction_numerical': 0.003179650238473768, 'mean_word_length': 3.2708757637474544, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 59, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '310765', 'n_tokens_mistral': 2487, 'n_tokens_neox': 2137, 'n_words': 638}