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

public struct Term: BooleanLiteralConvertible, CustomDebugStringConvertible, FixpointType, Hashable, IntegerLiteralConvertible, CustomStringConvertible {
	public init(_ expression: Expression<Term>) {
		self.init { expression }
	}

	public init(_ expression: () -> Expression<Term>) {
		_expression = expression
	}


	// MARK: Constructors

	public static var unit: Term {
		return Term(.Unit)
	}

	public static var unitType: Term {
		return Term(.UnitType)
	}


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

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


	public static func application(a: Term, _ b: Term) -> Term {
		return Term(.Application(a, b))
	}


	public static func projection(a: Term, _ b: Bool) -> Term {
		return Term(.Projection(a, b))
	}


	public static func variable(i: Int) -> Term {
		return Term.variable(.Local(i))
	}

	public static func variable(name: String) -> Term {
		return Term.variable(.Global(name))
	}

	public static func variable(name: Name) -> Term {
		return Term(.Variable(name))
	}


	public static func lambda(variable: Int, _ type: Term, _ body: Term) -> Term {
		return Term(.Lambda(variable, type, body))
	}

	public static func sigma(variable: Int, _ type: Term, _ body: Term) -> Term {
		return Term(.Sigma(variable, type, body))
	}


	public static func sum(a: Term, _ b: Term) -> Term {
		return sigma(booleanType) { c in `if`(c, then: a, `else`: b) }
	}

	public static func sum(terms: [Term]) -> Term {
		return terms.first.map { dropFirst(terms).reduce($0, combine: sum) } ?? unitType
	}


	public static var booleanType: Term {
		return Term(.BooleanType)
	}

	public static func boolean(b: Bool) -> Term {
		return Term(.Boolean(b))
	}

	public static func `if`(condition: Term, then: Term, `else`: Term) -> Term {
		return Term(.If(condition, then, `else`))
	}


	// MARK: Higher-order construction

	public static func lambda(type: Term, _ f: Term -> Term) -> Term {
		var n = 0
		let body = f(Term { .Variable(.Local(n)) })
		n = body.maxBoundVariable + 1
		return Term { .Lambda(n, type, body) }
	}

	public static func sigma(type: Term, _ f: Term -> Term) -> Term {
		var n = 0
		let body = f(Term { .Variable(.Local(n)) })
		n = body.maxBoundVariable + 1
		return Term { .Sigma(n, type, body) }
	}


	// MARK: Destructors

	public var isUnitTerm: Bool {
		return expression.analysis(ifUnit: const(true), otherwise: const(false))
	}

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

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

	public var application: (Term, Term)? {
		return expression.analysis(ifApplication: Optional.Some, otherwise: const(nil))
	}

	public var lambda: (Int, Term, Term)? {
		return expression.analysis(ifLambda: Optional.Some, otherwise: const(nil))
	}

	public var sigma: (Int, Term, Term)? {
		return expression.analysis(ifSigma: Optional.Some, otherwise: const(nil))
	}

	public var boolean: Bool? {
		return expression.analysis(ifBoolean: Optional.Some, otherwise: const(nil))
	}

	private var _expression: () -> Expression<Term>
	public var expression: Expression<Term> {
		return _expression()
	}


	// MARK: Normalization

	public var isNormalForm: Bool {
		return expression.analysis(
			ifVariable: const(false),
			ifApplication: const(false),
			ifProjection: const(false),
			ifIf: const(false),
			otherwise: const(true))
	}


	// MARK: Bound variables

	private var maxBoundVariable: Int {
		return cata {
			$0.analysis(
				ifApplication: max,
				ifLambda: { max($0.0, $0.1) },
				ifProjection: { $0.0 },
				ifSigma: { max($0.0, $0.1) },
				ifIf: { max($0, $1, $2) },
				otherwise: const(-1))
		} (self)
	}


	// MARK: Substitution

	private func substitute(i: Int, _ term: Term) -> Term {
		return cata { t in
			t.analysis(
				ifVariable: {
					$0.analysis(
						ifGlobal: const(Term(t)),
						ifLocal: { $0 == i ? term : Term.variable($0) })
				},
				ifApplication: Term.application,
				ifLambda: Term.lambda,
				ifProjection: Term.projection,
				ifSigma: Term.sigma,
				ifIf: Term.`if`,
				otherwise: const(Term(t)))
		} (self)
	}


	// MARK: Type-checking

	public func typecheck(environment: [Name: Term] = [:]) -> Either<Error, Term> {
		switch expression {
		case .Unit:
			return .right(.unitType)
		case .UnitType, .BooleanType:
			return .right(.type)
		case let .Type(n):
			return .right(.type(n + 1))<commit_msg>Remove basically unused overloads.<commit_after>//  Copyright (c) 2015 <NAME>. All rights reserved.

public struct Term: BooleanLiteralConvertible, CustomDebugStringConvertible, FixpointType, Hashable, IntegerLiteralConvertible, CustomStringConvertible {
	public init(_ expression: Expression<Term>) {
		self.init { expression }
	}

	public init(_ expression: () -> Expression<Term>) {
		_expression = expression
	}


	// MARK: Constructors

	public static var unit: Term {
		return Term(.Unit)
	}

	public static var unitType: Term {
		return Term(.UnitType)
	}


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

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


	public static func application(a: Term, _ b: Term) -> Term {
		return Term(.Application(a, b))
	}


	public static func projection(a: Term, _ b: Bool) -> Term {
		return Term(.Projection(a, b))
	}


	public static func variable(name: Name) -> Term {
		return Term(.Variable(name))
	}


	public static func lambda(variable: Int, _ type: Term, _ body: Term) -> Term {
		return Term(.Lambda(variable, type, body))
	}

	public static func sigma(variable: Int, _ type: Term, _ body: Term) -> Term {
		return Term(.Sigma(variable, type, body))
	}


	public static func sum(a: Term, _ b: Term) -> Term {
		return sigma(booleanType) { c in `if`(c, then: a, `else`: b) }
	}

	public static func sum(terms: [Term]) -> Term {
		return terms.first.map { dropFirst(terms).reduce($0, combine: sum) } ?? unitType
	}


	public static var booleanType: Term {
		return Term(.BooleanType)
	}

	public static func boolean(b: Bool) -> Term {
		return Term(.Boolean(b))
	}

	public static func `if`(condition: Term, then: Term, `else`: Term) -> Term {
		return Term(.If(condition, then, `else`))
	}


	// MARK: Higher-order construction

	public static func lambda(type: Term, _ f: Term -> Term) -> Term {
		var n = 0
		let body = f(Term { .Variable(.Local(n)) })
		n = body.maxBoundVariable + 1
		return Term { .Lambda(n, type, body) }
	}

	public static func sigma(type: Term, _ f: Term -> Term) -> Term {
		var n = 0
		let body = f(Term { .Variable(.Local(n)) })
		n = body.maxBoundVariable + 1
		return Term { .Sigma(n, type, body) }
	}


	// MARK: Destructors

	public var isUnitTerm: Bool {
		return expression.analysis(ifUnit: const(true), otherwise: const(false))
	}

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

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

	public var application: (Term, Term)? {
		return expression.analysis(ifApplication: Optional.Some, otherwise: const(nil))
	}

	public var lambda: (Int, Term, Term)? {
		return expression.analysis(ifLambda: Optional.Some, otherwise: const(nil))
	}

	public var sigma: (Int, Term, Term)? {
		return expression.analysis(ifSigma: Optional.Some, otherwise: const(nil))
	}

	public var boolean: Bool? {
		return expression.analysis(ifBoolean: Optional.Some, otherwise: const(nil))
	}

	private var _expression: () -> Expression<Term>
	public var expression: Expression<Term> {
		return _expression()
	}


	// MARK: Normalization

	public var isNormalForm: Bool {
		return expression.analysis(
			ifVariable: const(false),
			ifApplication: const(false),
			ifProjection: const(false),
			ifIf: const(false),
			otherwise: const(true))
	}


	// MARK: Bound variables

	private var maxBoundVariable: Int {
		return cata {
			$0.analysis(
				ifApplication: max,
				ifLambda: { max($0.0, $0.1) },
				ifProjection: { $0.0 },
				ifSigma: { max($0.0, $0.1) },
				ifIf: { max($0, $1, $2) },
				otherwise: const(-1))
		} (self)
	}


	// MARK: Substitution

	private func substitute(i: Int, _ term: Term) -> Term {
		return cata { t in
			t.analysis(
				ifVariable: {
					$0.analysis(
						ifGlobal: const(Term(t)),
						ifLocal: { $0 == i ? term : Term.variable(.Local($0)) })
				},
				ifApplication: Term.application,
				ifLambda: Term.lambda,
				ifProjection: Term.projection,
				ifSigma: Term.sigma,
				ifIf: Term.`if`,
				otherwise: const(Term(t)))
		} (self)
	}


	// MARK: Type-checking

	public func typecheck(environment: [Name: Term] = [:]) -> Either<Error, Term> {
		switch expression {
		case .Unit:
			return .right(.unitType)
		case .UnitType, .BooleanType:
			return .right(.type)
		case let .Type(n):
			return .right(.type(n + 1))
{'fraction_non_alphanumeric': 0.14344490159012566, 'fraction_numerical': 0.006449460691649061, 'mean_word_length': 3.579429735234216, 'pattern_counts': {'":': 0, '<': 15, '<?xml version=': 0, '>': 53, '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': '68722', 'n_tokens_mistral': 3366, 'n_tokens_neox': 2914, 'n_words': 846}