<commit_before>//  Copyright © 2015 <NAME>. All rights reserved.

final class ModuleTests: XCTestCase {
	func testModulesTypecheck() {
		for (_, module) in Module.modules {
			module.typecheck().forEach { XCTFail($0) }
		}
	}


	// MARK: Boolean

	func testEquivalenceOfEncodedAndDatatypeBooleans() {
		encodedBoolean.definitions.forEach { symbol, type, value in
			assert(Module.boolean.context[symbol], Term.equate, type, message: "\(symbol)")
			assert(Module.boolean.environment[symbol], Term.equate, value, message: "\(symbol)")
		}
	}


	// MARK: Natural

	func testZeroTypechecksAsNatural() {
		assert(try? zero.elaborateType(nil, Module.natural.environment, Module.natural.context), ==, .Unroll(Natural, .Variable(.Global("zero"))))
	}

	func testSuccessorOfZeroTypechecksAsNatural() {
		assert(try? successor[zero].elaborateType(nil, Module.natural.environment, Module.natural.context), ==, .Unroll(Natural, .Identity(.Application(.Unroll(Natural --> Natural, .Variable(.Global("successor"))), .Unroll(Natural, .Variable(.Global("zero")))))))
	}


	// MARK: Pair

	func testEquivalenceOfEncodedAndDatatypePairs() {
		encodedPair.definitions.forEach { symbol, type, value in
			assert(Module.pair.context[symbol], Term.equate, type, message: "\(symbol)")
			assert(Module.pair.environment[symbol], Term.equate, value, message: "\(symbol)")
		}
	}


	// MARK: Sigma

	func testEquivalenceOfEncodedAndDatatypeSigmas() {
		encodedSigma.definitions.forEach { symbol, type, value in
			assert(Module.sigma.context[symbol], Term.equate, type, message: "'\(symbol)' expected '\(type)', actual '\(Module.sigma.context[symbol])'")
			assert(Module.sigma.environment[symbol], Term.equate, value, message: "'\(symbol)' expected '\(value)', actual '\(Module.sigma.environment[symbol])'")
		}
	}


	// MARK: Either

	func testEquivalenceOfEncodedAndDatatypeEithers() {
		Module.either.definitions.forEach { symbol, type, value in
			assert(encodedEither.context[symbol], Term.equate, type, message: "\(symbol)")
			assert(encodedEither.environment[symbol], Term.equate, value, message: "\(symbol)")
		}
	}


	// MARK: List

	func testEquivalenceOfEncodedAndDatatypeLists() {
		encodedList.definitions.forEach { symbol, type, value in
			assert(Module.list.context[symbol], Term.equate, type, message: "'\(symbol)' expected '\(type)', actual '\(Module.list.context[symbol])'")
			assert(Module.list.environment[symbol], Term.equate, value, message: "'\(symbol)' expected '\(value)', actual '\(Module.list.environment[symbol])'")
		}
	}

	func testListValuesAsEliminators() {
		let module = Module("test", [ Module.list, Module.unit, Module.boolean ], [])
		let List: Term = "List"
		let cons: Term = "cons"
		let `nil`: Term = "nil"
		let Unit: Term = "Unit"
		let unit: Term = "unit"
		let Boolean: Term = "Boolean"
		let `true`: Term = "true"
		let `false`: Term = "false"
		let list: Term = cons[nil, unit, `nil`[Term.Implicit]]

		let isEmpty = List[Unit] => { list in
			list[Boolean, (unit, List[Unit]) => { _ in `false` }, `true`]
		}

		assert((try? isEmpty[list].evaluate(module.environment)).flatMap { Term.equate($0, `false`, module.environment) }, !=, nil)
		assert((try? isEmpty[`nil`[Term.Implicit]].evaluate(module.environment)).flatMap { Term.equate($0, `true`, module.environment) }, !=, nil)
	}


	// MARK: String

	func testStringToListConversion() {
		let environment = Module.string.environment
		let toList: Term = "toList"
		let string = Term.Embedded("hi", "String")
		let cons: Term = "cons"
		let `nil`: Term = "nil"
		assert(try? toList[string].evaluate(environment), ==, try? cons[nil, embedCharacter("h"), cons[nil, embedCharacter("i"), `nil`[Term.Implicit]]].evaluate(environment))
	}

	func testListToStringConversion() {
		let environment = Module.string.environment
		let cons: Term = "cons"
		let `nil`: Term = "nil"
		let fromList: Term = "fromList"
		let nilTerm: Term = fromList[`nil`[Term.Implicit]]
		let consTerm: Term = fromList[cons[nil, embedCharacter("a"), `nil`[Term.Implicit]]]
		let term = fromList[cons[nil, embedCharacter("h"), cons[nil, embedCharacter("i"), `nil`[Term.Implicit]]]]
		assert(try? nilTerm.evaluate(environment), ==, Term.Embedded("", "String"))
		assert(try? consTerm.evaluate(environment), Term.equate, Term.Embedded("a", "String"))
		assert(try? term.evaluate(environment), Term.equate, Term.Embedded("hi", "String"))
	}
}


private let encodedBoolean: Module = {
	let Boolean = Declaration("Boolean",
		type: .Type,
		value: .Type => { ($0, $0) => const($0) })

	let `true` = Declaration("true",
		type: Boolean.ref,<commit_msg>Test the nilTerm’s result up to renaming.<commit_after>//  Copyright © 2015 <NAME>. All rights reserved.

final class ModuleTests: XCTestCase {
	func testModulesTypecheck() {
		for (_, module) in Module.modules {
			module.typecheck().forEach { XCTFail($0) }
		}
	}


	// MARK: Boolean

	func testEquivalenceOfEncodedAndDatatypeBooleans() {
		encodedBoolean.definitions.forEach { symbol, type, value in
			assert(Module.boolean.context[symbol], Term.equate, type, message: "\(symbol)")
			assert(Module.boolean.environment[symbol], Term.equate, value, message: "\(symbol)")
		}
	}


	// MARK: Natural

	func testZeroTypechecksAsNatural() {
		assert(try? zero.elaborateType(nil, Module.natural.environment, Module.natural.context), ==, .Unroll(Natural, .Variable(.Global("zero"))))
	}

	func testSuccessorOfZeroTypechecksAsNatural() {
		assert(try? successor[zero].elaborateType(nil, Module.natural.environment, Module.natural.context), ==, .Unroll(Natural, .Identity(.Application(.Unroll(Natural --> Natural, .Variable(.Global("successor"))), .Unroll(Natural, .Variable(.Global("zero")))))))
	}


	// MARK: Pair

	func testEquivalenceOfEncodedAndDatatypePairs() {
		encodedPair.definitions.forEach { symbol, type, value in
			assert(Module.pair.context[symbol], Term.equate, type, message: "\(symbol)")
			assert(Module.pair.environment[symbol], Term.equate, value, message: "\(symbol)")
		}
	}


	// MARK: Sigma

	func testEquivalenceOfEncodedAndDatatypeSigmas() {
		encodedSigma.definitions.forEach { symbol, type, value in
			assert(Module.sigma.context[symbol], Term.equate, type, message: "'\(symbol)' expected '\(type)', actual '\(Module.sigma.context[symbol])'")
			assert(Module.sigma.environment[symbol], Term.equate, value, message: "'\(symbol)' expected '\(value)', actual '\(Module.sigma.environment[symbol])'")
		}
	}


	// MARK: Either

	func testEquivalenceOfEncodedAndDatatypeEithers() {
		Module.either.definitions.forEach { symbol, type, value in
			assert(encodedEither.context[symbol], Term.equate, type, message: "\(symbol)")
			assert(encodedEither.environment[symbol], Term.equate, value, message: "\(symbol)")
		}
	}


	// MARK: List

	func testEquivalenceOfEncodedAndDatatypeLists() {
		encodedList.definitions.forEach { symbol, type, value in
			assert(Module.list.context[symbol], Term.equate, type, message: "'\(symbol)' expected '\(type)', actual '\(Module.list.context[symbol])'")
			assert(Module.list.environment[symbol], Term.equate, value, message: "'\(symbol)' expected '\(value)', actual '\(Module.list.environment[symbol])'")
		}
	}

	func testListValuesAsEliminators() {
		let module = Module("test", [ Module.list, Module.unit, Module.boolean ], [])
		let List: Term = "List"
		let cons: Term = "cons"
		let `nil`: Term = "nil"
		let Unit: Term = "Unit"
		let unit: Term = "unit"
		let Boolean: Term = "Boolean"
		let `true`: Term = "true"
		let `false`: Term = "false"
		let list: Term = cons[nil, unit, `nil`[Term.Implicit]]

		let isEmpty = List[Unit] => { list in
			list[Boolean, (unit, List[Unit]) => { _ in `false` }, `true`]
		}

		assert((try? isEmpty[list].evaluate(module.environment)).flatMap { Term.equate($0, `false`, module.environment) }, !=, nil)
		assert((try? isEmpty[`nil`[Term.Implicit]].evaluate(module.environment)).flatMap { Term.equate($0, `true`, module.environment) }, !=, nil)
	}


	// MARK: String

	func testStringToListConversion() {
		let environment = Module.string.environment
		let toList: Term = "toList"
		let string = Term.Embedded("hi", "String")
		let cons: Term = "cons"
		let `nil`: Term = "nil"
		assert(try? toList[string].evaluate(environment), ==, try? cons[nil, embedCharacter("h"), cons[nil, embedCharacter("i"), `nil`[Term.Implicit]]].evaluate(environment))
	}

	func testListToStringConversion() {
		let environment = Module.string.environment
		let cons: Term = "cons"
		let `nil`: Term = "nil"
		let fromList: Term = "fromList"
		let nilTerm: Term = fromList[`nil`[Term.Implicit]]
		let consTerm: Term = fromList[cons[nil, embedCharacter("a"), `nil`[Term.Implicit]]]
		let term = fromList[cons[nil, embedCharacter("h"), cons[nil, embedCharacter("i"), `nil`[Term.Implicit]]]]
		assert(try? nilTerm.evaluate(environment), Term.equate, Term.Embedded("", "String"))
		assert(try? consTerm.evaluate(environment), Term.equate, Term.Embedded("a", "String"))
		assert(try? term.evaluate(environment), Term.equate, Term.Embedded("hi", "String"))
	}
}


private let encodedBoolean: Module = {
	let Boolean = Declaration("Boolean",
		type: .Type,
		value: .Type => { ($0, $0) => const($0) })

	let `true` = Declaration("true",
		type: Boolean.ref,
{'fraction_non_alphanumeric': 0.17413475100358033, 'fraction_numerical': 0.002169903439296951, 'mean_word_length': 5.060486522024983, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 15, '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': '338970', 'n_tokens_mistral': 3272, 'n_tokens_neox': 2965, 'n_words': 646}