[WIP] Datatype descriptions

Manifold.xcodeproj/project.pbxproj

@@ -24,6 +24,7 @@
 		D470CB981BDC27130003A931 /* Module+Vector.swift in Sources */ = {isa = PBXBuildFile; fileRef = D470CB971BDC27130003A931 /* Module+Vector.swift */; };
 		D4809FBD1AF6BD400084B8FE /* TermTests.swift in Sources */ = {isa = PBXBuildFile; fileRef = D4809FBC1AF6BD400084B8FE /* TermTests.swift */; };
 		D484903C1B2A40E800F249F7 /* EvaluationTests.swift in Sources */ = {isa = PBXBuildFile; fileRef = D484903B1B2A40E800F249F7 /* EvaluationTests.swift */; };
+		D492927B1C26837000BA59F3 /* Module+Tag.swift in Sources */ = {isa = PBXBuildFile; fileRef = D492927A1C26837000BA59F3 /* Module+Tag.swift */; };
 		D492927F1C278CC000BA59F3 /* Module+PropositionalEquality.swift in Sources */ = {isa = PBXBuildFile; fileRef = D492927E1C278CC000BA59F3 /* Module+PropositionalEquality.swift */; };
 		D4A31B2A1AA366EC00B3FC68 /* TermContainerType.swift in Sources */ = {isa = PBXBuildFile; fileRef = D4A31B291AA366EC00B3FC68 /* TermContainerType.swift */; };
 		D4ACE90D1BDC7E51009E928F /* Module+FiniteSet.swift in Sources */ = {isa = PBXBuildFile; fileRef = D4ACE90C1BDC7E51009E928F /* Module+FiniteSet.swift */; };
@@ -53,6 +54,7 @@
 		D4F969981B98F3220069F481 /* Term+Arbitrary.swift in Sources */ = {isa = PBXBuildFile; fileRef = D4F969971B98F3220069F481 /* Term+Arbitrary.swift */; };
 		D4F9F86B1A8496F700B7071E /* Prelude.framework in Frameworks */ = {isa = PBXBuildFile; fileRef = D4F9F86A1A8496F700B7071E /* Prelude.framework */; };
 		D4F9F86C1A84970900B7071E /* Prelude.framework in Frameworks */ = {isa = PBXBuildFile; fileRef = D4F9F86A1A8496F700B7071E /* Prelude.framework */; };
+		D4FA652D1C1CF228009999A3 /* Module+Datatype.swift in Sources */ = {isa = PBXBuildFile; fileRef = D4FA652C1C1CF228009999A3 /* Module+Datatype.swift */; };
 		D4FB02D91B71D06A0090E764 /* Module+Boolean.swift in Sources */ = {isa = PBXBuildFile; fileRef = D4FB02D81B71D06A0090E764 /* Module+Boolean.swift */; };
 		D4FB2D071BE447DE00B3CCE0 /* Module+Directory.swift in Sources */ = {isa = PBXBuildFile; fileRef = D4FB2D061BE447DE00B3CCE0 /* Module+Directory.swift */; };
 		D4FB2D091BE4490000B3CCE0 /* ModuleTests.swift in Sources */ = {isa = PBXBuildFile; fileRef = D4FB2D081BE4490000B3CCE0 /* ModuleTests.swift */; };
@@ -88,6 +90,7 @@
 		D470CB971BDC27130003A931 /* Module+Vector.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "Module+Vector.swift"; sourceTree = "<group>"; };
 		D4809FBC1AF6BD400084B8FE /* TermTests.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = TermTests.swift; sourceTree = "<group>"; };
 		D484903B1B2A40E800F249F7 /* EvaluationTests.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = EvaluationTests.swift; sourceTree = "<group>"; };
+		D492927A1C26837000BA59F3 /* Module+Tag.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "Module+Tag.swift"; sourceTree = "<group>"; };
 		D492927E1C278CC000BA59F3 /* Module+PropositionalEquality.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "Module+PropositionalEquality.swift"; sourceTree = "<group>"; };
 		D4A31B291AA366EC00B3FC68 /* TermContainerType.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = TermContainerType.swift; sourceTree = "<group>"; };
 		D4ACE90C1BDC7E51009E928F /* Module+FiniteSet.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "Module+FiniteSet.swift"; sourceTree = "<group>"; };
@@ -119,6 +122,7 @@
 		D4F969951B98ECE80069F481 /* SwiftCheck.framework */ = {isa = PBXFileReference; lastKnownFileType = wrapper.framework; path = SwiftCheck.framework; sourceTree = BUILT_PRODUCTS_DIR; };
 		D4F969971B98F3220069F481 /* Term+Arbitrary.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "Term+Arbitrary.swift"; sourceTree = "<group>"; };
 		D4F9F86A1A8496F700B7071E /* Prelude.framework */ = {isa = PBXFileReference; lastKnownFileType = wrapper.framework; path = Prelude.framework; sourceTree = BUILT_PRODUCTS_DIR; };
+		D4FA652C1C1CF228009999A3 /* Module+Datatype.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "Module+Datatype.swift"; sourceTree = "<group>"; };
 		D4FB02D81B71D06A0090E764 /* Module+Boolean.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "Module+Boolean.swift"; sourceTree = "<group>"; };
 		D4FB2D061BE447DE00B3CCE0 /* Module+Directory.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "Module+Directory.swift"; sourceTree = "<group>"; };
 		D4FB2D081BE4490000B3CCE0 /* ModuleTests.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = ModuleTests.swift; sourceTree = "<group>"; };
@@ -240,6 +244,8 @@
 			isa = PBXGroup;
 			children = (
 				D445417B1BCAB0C100F2946D /* Module+Unit.swift */,
+				D4FA652C1C1CF228009999A3 /* Module+Datatype.swift */,
+				D492927A1C26837000BA59F3 /* Module+Tag.swift */,
 				D4FB02D81B71D06A0090E764 /* Module+Boolean.swift */,
 				D445417F1BCAC38500F2946D /* Module+List.swift */,
 				D4E101B91B484611001A7E55 /* Module+Natural.swift */,
@@ -365,6 +371,7 @@
 			isa = PBXSourcesBuildPhase;
 			buildActionMask = 2147483647;
 			files = (
+				D492927B1C26837000BA59F3 /* Module+Tag.swift in Sources */,
 				D445417C1BCAB0C100F2946D /* Module+Unit.swift in Sources */,
 				D4E9901C1BD3431D00F00CA7 /* Module+Either.swift in Sources */,
 				D43B6D1B1C1DB2CA008EF3D2 /* Module+String.swift in Sources */,
@@ -382,6 +389,7 @@
 				D4A31B2A1AA366EC00B3FC68 /* TermContainerType.swift in Sources */,
 				D44541801BCAC38500F2946D /* Module+List.swift in Sources */,
 				D463F6D21BD2A83E00BA0628 /* Module+Maybe.swift in Sources */,
+				D4FA652D1C1CF228009999A3 /* Module+Datatype.swift in Sources */,
 				D4E990241BD3EE5300F00CA7 /* AnnotatedTerm.swift in Sources */,
 				D4FB2D0B1BE44DAF00B3CCE0 /* Module+Functor.swift in Sources */,
 				D445418E1BCAF57D00F2946D /* Term+Evaluation.swift in Sources */,

Manifold/Module+Datatype.swift

@@ -0,0 +1,46 @@
+//  Copyright © 2015 Rob Rix. All rights reserved.
+
+extension Module {
+	public static var datatype: Module {
+		let _Datatype: Term = "Datatype"
+		let datatype = Declaration("Datatype", Datatype("I", .Type,
+			[
+				"end": .Argument("index", "I", .End),
+				"recursive": .Argument("index", "I", .Recursive("recur", .End)),
+				"argument": Telescope.Argument("A", .Type, .Argument("telescope", "A" --> _Datatype["I" as Term], .End)),
+			]
+		))
+
+		let μ = Declaration("μ",
+			type: nil => { I in _Datatype[I] --> I --> .Type },
+			value: nil => { I in (_Datatype[I], I, .Type) => { _, _, Motive in (_Datatype[I] --> I --> Motive) --> Motive } })
+
+		let IType = Declaration("IType",
+			type: .Type --> .Type(1),
+			value: .Type => { I in I --> .Type })
+
+		let Identical: Term = "≡"
+		let Pair: Term = "Pair"
+		let Sigma: Term = "Sigma"
+		let El: Term = "El"
+		let el = Declaration("El",
+			type: .Type => { I in _Datatype[I] --> IType.ref[I] --> IType.ref[I] },
+			value: .Type => { I in
+				(_Datatype[I], IType.ref[I], I) => { D, X, i in
+					D[.Type,
+						I => { j in Identical[I, i, j] },
+						(I, _Datatype[I]) => { j, D in Pair[X[j], El[I, D, X, i]] },
+						.Type => { A in (A --> _Datatype[I]) => { B in Sigma[A, nil => { a in El[I, B[a], X, i] }] } }]
+				}
+			})
+
+		let `init` = Declaration("init",
+			type: nil => { I in (_Datatype[I], I) => { D, i in El[I, D, μ.ref[I, D], i] --> μ.ref[I, D, i] } },
+			value: nil => { I in (nil, nil) => { D, i in nil => { _ in nil } } })
+
+		return Module("Datatype", [ tag, propositionalEquality, pair, sigma ], [ datatype, μ, `init`, IType, el ])
+	}
+}
+
+
+import Prelude

Manifold/Module+Directory.swift

@@ -15,5 +15,7 @@ extension Module {
 		vector,
 		finiteSet,
 		string,
+		datatype,
+		tag,
 	].map { ($0.name, $0) })
 }

Manifold/Module+Pair.swift

@@ -7,12 +7,12 @@ extension Module {
 		))
 
 		let first = Declaration("first",
-			type: (nil, nil) => { A, B in Pair.ref[A, B] --> A },
-			value: (nil, nil, nil) => { A, B, pair in pair[nil, (nil, B) => { a, _ in a }] })
+			type: (.Type, .Type) => { A, B in Pair.ref[A, B] --> A },
+			value: (nil, nil) => { A, B in nil => { pair in pair[nil, (nil, B) => { a, _ in a }] } })
 
 		let second = Declaration("second",
-			type: (nil, nil) => { A, B in Pair.ref[A, B] --> B },
-			value: (nil, nil, nil) => { A, B, pair in pair[nil, (nil, nil) => { _, b in b }] })
+			type: (.Type, .Type) => { A, B in Pair.ref[A, B] --> B },
+			value: (nil, nil) => { A, B in nil => { pair in pair[nil, (nil, nil) => { _, b in b }] } })
 
 		return Module("Pair", [ Pair, first, second ])
 	}

Manifold/Module+Tag.swift

@@ -0,0 +1,48 @@
+//  Copyright © 2015 Rob Rix. All rights reserved.
+
+extension Module {
+	public static var tag: Module {
+		let List: Term = "List"
+		let cons: Term = "cons"
+		let String: Term = "String"
+		let Enum = Declaration("Enum",
+			type: .Type,
+			value: List[String])
+
+		let Tag = Declaration("Tag",
+			type: Enum.ref --> .Type,
+			value: (Enum.ref, .Type) => { e, Motive in (String --> Motive) --> (List[String] --> Motive) --> Motive })
+
+		let here = Declaration("here",
+			type: (String, List[String]) => { l, E in Tag.ref[cons[nil, l, E]] },
+			value: (String, List[String], .Type) => { l, _, Motive in (String --> Motive, List[String] --> Motive) => { f, _ in f[l] }  })
+
+		let there = Declaration("there",
+			type: (String, List[String]) => { l, E in Tag.ref[E] --> Tag.ref[cons[nil, l, E]] },
+			value: (String, List[String]) => { _, E in Tag.ref[E] --> .Type => { Motive in (String --> Motive, List[String] --> Motive) => { _, f in f[E] } } })
+
+		let Unit: Term = "Unit"
+		let Pair: Term = "Pair"
+		let Branches: Term = "Branches"
+		let branches = Declaration("Branches",
+			type: Enum.ref => { E in (Tag.ref[E] --> .Type) --> .Type },
+			value: nil => { E in nil => { P in E[nil, (nil, nil) => { l, E in Pair[P[here.ref[nil, nil]], Branches[E, nil => { t in P[there.ref[nil, nil, t]] }]] }, Unit] } })
+
+		let first: Term = "first"
+		let firstBranch = Declaration("firstBranch",
+			type: (String, Enum.ref) => { l, E in (Tag.ref[cons[String, l, E]] --> .Type) => { P in Branches[cons[String, l, E], P] => { cs in P[here.ref[l, E]] } } },
+			value: (String, Enum.ref) => { l, E in (Tag.ref[cons[String, l, E]] --> .Type) => { P in Branches[cons[String, l, E], P] => { cs in first[nil, nil, cs] } } })
+
+		let second: Term = "second"
+		let secondBranch = Declaration("secondBranch",
+			type: (String, Enum.ref) => { l, E in (Tag.ref[cons[String, l, E]] --> .Type) => { P in Branches[cons[String, l, E], P] => { cs in P[there.ref[l, E, here.ref[nil, nil]]] } } },
+			value: (String, Enum.ref) => { l, E in (Tag.ref[cons[String, l, E]] --> .Type) => { P in Branches[cons[String, l, E], P] => { cs in second[nil, nil, cs] } } })
+
+		let _case: Term = "case"
+		let `case` = Declaration("case",
+			type: Enum.ref => { E in (Tag.ref[E] --> .Type) => { P in Branches[E, P] --> Tag.ref[E] => { t in P[t] } } },
+			value: nil => { E in nil => { P in (nil, nil) => { cs, t in t[nil, nil => { _ in firstBranch.ref[nil, nil, P, cs] }, nil => { t in _case[E, nil => { t in P[E, there.ref[nil, nil, t]] }, secondBranch.ref[nil, nil, P, cs], t] }] } } })
+
+		return Module("Tag", [ list, string, unit, pair ], [ Enum, Tag, here, there, branches, firstBranch, secondBranch, `case` ])
+	}
+}

Manifold/Term+Elaboration.swift

@@ -16,7 +16,7 @@ extension Term {
 				return .Unroll(type, .Variable(name))
 
 			case let (.Identity(.Application(a, b)), .Identity(.Implicit)):
-				let aʹ = try a.elaborateType(nil, environment, context)
+				let aʹ = try a.elaborateType(nil --> nil, environment, context)
 				guard case let .Identity(.Lambda(type, body)) = aʹ.annotation.weakHeadNormalForm(environment).out else {
 					throw "Illegal application of \(a) : \(aʹ.annotation) in context: \(Term.toString(context, separator: ":")), environment: \(Term.toString(environment, separator: "="))"
 				}
@@ -60,7 +60,7 @@ extension Term {
 
 			case let (_, b):
 				let a = try elaborateType(nil, environment, context)
-				guard Term.equate(a.annotation, Term(b), environment) != nil else {
+				guard Term.equate(a.annotation.weakHeadNormalForm(environment), Term(b), environment) != nil else {
 					throw "Type mismatch: expected '\(self)' to be of type '\(Term(b))', but it was actually of type '\(a.annotation)' in context: \(Term.toString(context, separator: ":")), environment: \(Term.toString(environment, separator: "="))"
 				}
 				return a

ManifoldTests/ModuleTests.swift

@@ -11,10 +11,7 @@ final class ModuleTests: XCTestCase {
 	// 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)")
-		}
+		assertEquivalent(encodedBoolean, Module.boolean)
 	}
 
 
@@ -32,40 +29,28 @@ final class ModuleTests: XCTestCase {
 	// 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)")
-		}
+		assertEquivalent(encodedPair, Module.pair)
 	}
 
 
 	// 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)'\nexpected '\(value)'\nactual '\(Module.sigma.environment[symbol] ?? "nil")'")
-		}
+		assertEquivalent(encodedSigma, Module.sigma)
 	}
 
 
 	// 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)")
-		}
+		assertEquivalent(encodedEither, Module.either)
 	}
 
 
 	// 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])'")
-		}
+		assertEquivalent(encodedList, Module.list)
 	}
 
 	func testListValuesAsEliminators() {
@@ -115,6 +100,37 @@ final class ModuleTests: XCTestCase {
 		assert(try term.elaborateType("String", environment, Module.string.context).annotation, Term.equate, "String")
 		assert(try term.evaluate(environment), Term.equate, Term.Embedded("hi", "String"))
 	}
+
+
+	// MARK: Datatype
+
+	func testEquivalenceOfDatatypeEncodedAndDatatypeBooleans() {
+		datatypeEncodedBoolean.typecheck().forEach { XCTFail($0) }
+		assertEquivalent(datatypeEncodedBoolean, Module.boolean)
+	}
+
+
+	// MARK: Assertions
+
+	func assertEquivalent(a: Module, _ b: Module, _ file: String = __FILE__, _ line: UInt = __LINE__) {
+		a.definitions.forEach { definition in assertEquivalent(definition, b, file, line) }
+	}
+
+	func assertEquivalent(definition: (Name, Term, Term), _ module: Module, _ file: String = __FILE__, _ line: UInt = __LINE__) {
+		let (symbol, type, value) = definition
+		if let actual = module.context[symbol] {
+			assert(actual, Term.equate, type, message:
+				"Type mismatch in '\(module.name).\(symbol)'\n"
+					+ "expected : \(type)\n"
+					+ "  actual : \(actual)\n", file: file, line: line)
+		}
+		if let actual = module.environment[symbol] {
+			assert(actual, Term.equate, value, message:
+				"Term mismatch in '\(module.name).\(symbol)'\n"
+					+ "expected = \(value)\n"
+					+ "  actual = \(actual)\n", file: file, line: line)
+		}
+	}
 }
 
 
@@ -203,6 +219,62 @@ private let encodedList: Module = {
 private let embedCharacter: Character -> Term = { Term.Embedded($0, "Character") }
 
 
+private let datatypeEncodedBoolean: Module = {
+	let Enum: Term = "Enum"
+	let cons: Term = "cons"
+	let `nil`: Term = "nil"
+	let Tag: Term = "Tag"
+	let here: Term = "here"
+	let there: Term = "there"
+	let Datatype: Term = "Datatype"
+	let argument: Term = "argument"
+	let end: Term = "end"
+	let μ: Term = "μ"
+	let caseD: Term = "caseD"
+	let `init`: Term = "init"
+	let refl: Term = "refl"
+	let Unit: Term = "Unit"
+	let unit: Term = "unit"
+	let String: Term = "String"
+
+	let embedString: Swift.String -> Term = { .Embedded($0, String) }
+
+	let BooleanT = Declaration("BooleanT",
+		type: .Type,
+		value: Tag[cons[nil, embedString("true"), cons[nil, embedString("false"), `nil`[Term.Implicit]]]])
+
+	let BooleanC = Declaration("BooleanC",
+		type: BooleanT.ref --> Datatype[Unit],
+		value: caseD[end[unit], end[unit]])
+
+	let BooleanD = Declaration("BooleanD",
+		type: Datatype[Unit],
+		value: argument[BooleanT.ref, BooleanC.ref])
+
+	let Boolean = Declaration("Boolean",
+		type: .Type,
+		value: μ[BooleanD.ref])
+
+	let trueT = Declaration("trueT",
+		type: BooleanT.ref,
+		value: here)
+
+	let `true` = Declaration("true",
+		type: Boolean.ref,
+		value: `init`[trueT.ref, refl])
+
+	let falseT = Declaration("falseT",
+		type: BooleanT.ref,
+		value: there[here])
+
+	let `false` = Declaration("false",
+		type: Boolean.ref,
+		value: `init`[falseT.ref, refl])
+
+	return Module("DatatypeEncodedBoolean", [ Module.unit, Module.datatype ], [ BooleanT, BooleanC, BooleanD, Boolean, trueT, `true`, falseT, `false` ])
+}()
+
+
 import Assertions
 @testable import Manifold
 import Prelude