From bdd775a6d05279d2a5d32b86eb1ff880fd2d37ef Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sat, 12 Dec 2015 19:25:23 -0500 Subject: [PATCH 01/75] Stub in a module of datatypes. --- Manifold.xcodeproj/project.pbxproj | 4 ++++ Manifold/Module+Datatype.swift | 7 +++++++ 2 files changed, 11 insertions(+) create mode 100644 Manifold/Module+Datatype.swift diff --git a/Manifold.xcodeproj/project.pbxproj b/Manifold.xcodeproj/project.pbxproj index e8e7fc6..602483b 100644 --- a/Manifold.xcodeproj/project.pbxproj +++ b/Manifold.xcodeproj/project.pbxproj @@ -49,6 +49,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 */; }; @@ -111,6 +112,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 = ""; }; 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 = ""; }; D4FB02D81B71D06A0090E764 /* Module+Boolean.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "Module+Boolean.swift"; sourceTree = ""; }; D4FB2D061BE447DE00B3CCE0 /* Module+Directory.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "Module+Directory.swift"; sourceTree = ""; }; D4FB2D081BE4490000B3CCE0 /* ModuleTests.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = ModuleTests.swift; sourceTree = ""; }; @@ -230,6 +232,7 @@ isa = PBXGroup; children = ( D445417B1BCAB0C100F2946D /* Module+Unit.swift */, + D4FA652C1C1CF228009999A3 /* Module+Datatype.swift */, D4FB02D81B71D06A0090E764 /* Module+Boolean.swift */, D445417F1BCAC38500F2946D /* Module+List.swift */, D4E101B91B484611001A7E55 /* Module+Natural.swift */, @@ -370,6 +373,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 */, diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift new file mode 100644 index 0000000..07467b8 --- /dev/null +++ b/Manifold/Module+Datatype.swift @@ -0,0 +1,7 @@ +// Copyright © 2015 Rob Rix. All rights reserved. + +extension Module { + public static var datatype: Module { + return Module("Datatype", []) + } +} From 9faf9c4bfdc7412b8dbc8ac80ff9110f6eb31710 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sat, 12 Dec 2015 19:28:21 -0500 Subject: [PATCH 02/75] Datatype has a Datatype named Datatype. --- Manifold/Module+Datatype.swift | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index 07467b8..f0be2df 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -2,6 +2,8 @@ extension Module { public static var datatype: Module { - return Module("Datatype", []) + return Module("Datatype", [ + .Datatype("Datatype", [:]) + ]) } } From 1b9853a26663c9d52a4d6ad1da465ebdacb72557 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sat, 12 Dec 2015 19:30:38 -0500 Subject: [PATCH 03/75] Add an `end` constructor. --- Manifold/Module+Datatype.swift | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index f0be2df..8382f84 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -3,7 +3,9 @@ extension Module { public static var datatype: Module { return Module("Datatype", [ - .Datatype("Datatype", [:]) + .Datatype("Datatype", [ + "end": .End, + ]) ]) } } From 41b6e6d9693309709b134cc738c32a069ab72802 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sat, 12 Dec 2015 19:35:17 -0500 Subject: [PATCH 04/75] Datatype is parameterized by an index type. --- Manifold/Module+Datatype.swift | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index 8382f84..1019cd1 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -3,9 +3,14 @@ extension Module { public static var datatype: Module { return Module("Datatype", [ - .Datatype("Datatype", [ - "end": .End, - ]) + Declaration("Datatype", Datatype(.Type) { I in + [ + "end": .Argument(I, const(.End)), + ] + }) ]) } } + + +import Prelude From 45811536d758ad5c6c7595a86562aaea6198d830 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sat, 12 Dec 2015 19:37:04 -0500 Subject: [PATCH 05/75] Add a recursive case to Datatype. --- Manifold/Module+Datatype.swift | 1 + 1 file changed, 1 insertion(+) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index 1019cd1..762daaa 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -6,6 +6,7 @@ extension Module { Declaration("Datatype", Datatype(.Type) { I in [ "end": .Argument(I, const(.End)), + "recursive": .Argument(I, const(.Recursive(.End))), ] }) ]) From ff5228c56a8fee423363a58296c518c691830252 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sat, 12 Dec 2015 19:43:08 -0500 Subject: [PATCH 06/75] Add an argument case to Datatype. --- Manifold/Module+Datatype.swift | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index 762daaa..ace76ac 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -2,11 +2,13 @@ extension Module { public static var datatype: Module { + let _Datatype: Term = "Datatype" return Module("Datatype", [ Declaration("Datatype", Datatype(.Type) { I in [ "end": .Argument(I, const(.End)), "recursive": .Argument(I, const(.Recursive(.End))), + "argument": Telescope.Argument(.Type) { A in .Argument(A --> _Datatype[I], const(.End)) }, ] }) ]) From 6c26495288ec667783c6253dfb985d151c7e4193 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sat, 12 Dec 2015 19:43:43 -0500 Subject: [PATCH 07/75] Add the Datatype module to the directory. --- Manifold/Module+Directory.swift | 1 + 1 file changed, 1 insertion(+) diff --git a/Manifold/Module+Directory.swift b/Manifold/Module+Directory.swift index 2c929a7..6a965ea 100644 --- a/Manifold/Module+Directory.swift +++ b/Manifold/Module+Directory.swift @@ -13,5 +13,6 @@ extension Module { sigma, vector, finiteSet, + datatype, ].map { ($0.name, $0) }) } From 29e526a01857d7fbda32a163a2a1317ce0a164e7 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sat, 12 Dec 2015 20:12:27 -0500 Subject: [PATCH 08/75] Expand the error messages for the encoded Either tests. --- ManifoldTests/ModuleTests.swift | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index 75740b5..1cba224 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -53,8 +53,8 @@ final class ModuleTests: XCTestCase { func testEquivalenceOfEncodedAndDatatypeEithers() { Module.either.definitions.forEach { symbol, type, value in - assert(encodedEither.context[symbol], ==, type, message: "\(symbol)") - assert(encodedEither.environment[symbol], ==, value, message: "\(symbol)") + assert(encodedEither.context[symbol], ==, type, message: "'\(symbol)' expected '\(type), actual '\(Module.either.context[symbol])'") + assert(encodedEither.environment[symbol], ==, value, message: "'\(symbol)' expected '\(type)', actual '\(Module.either.environment[symbol])'") } } From bca25eb6c92d4810cc8e6ec69a858b43f906a7f8 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sat, 12 Dec 2015 20:12:38 -0500 Subject: [PATCH 09/75] Stub in a private datatype-encoded boolean module. --- ManifoldTests/ModuleTests.swift | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index 1cba224..8fc5f6d 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -153,6 +153,11 @@ private let encodedList: Module = { }() +private let datatypeEncodedBoolean: Module = { + return Module("DatatypeEncodedBoolean", []) +}() + + import Assertions import Manifold import Prelude From bc442ee730c150c8f6528cb8ee4ef05afa9f1540 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sat, 12 Dec 2015 20:13:10 -0500 Subject: [PATCH 10/75] =?UTF-8?q?Test=20the=20equivalence=20of=20the=20dat?= =?UTF-8?q?atype-encoded=20boolean=20module=E2=80=99s=20definitions=20with?= =?UTF-8?q?=20those=20in=20the=20canonical=20module.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ManifoldTests/ModuleTests.swift | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index 8fc5f6d..4490d6a 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -67,6 +67,16 @@ final class ModuleTests: XCTestCase { assert(Module.list.environment[symbol], ==, value, message: "'\(symbol)' expected '\(value)', actual '\(Module.list.environment[symbol])'") } } + + + // MARK: Datatype + + func testEquivalenceOfDatatypeEncodedAndDatatypeBooleans() { + datatypeEncodedBoolean.definitions.forEach { symbol, type, value in + assert(Module.boolean.context[symbol], ==, type, message: "'\(symbol)' expected '\(type)', actual '\(Module.boolean.context[symbol])'") + assert(Module.boolean.environment[symbol], ==, value, message: "'\(symbol)' expected '\(value)', actual '\(Module.boolean.environment[symbol])'") + } + } } From 75031d95f5ddea919e76cfa4e17dd1374af2021e Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sat, 12 Dec 2015 20:25:04 -0500 Subject: [PATCH 11/75] Pull the Datatype declaration into a temporary. --- Manifold/Module+Datatype.swift | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index ace76ac..1807ea4 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -3,14 +3,15 @@ extension Module { public static var datatype: Module { let _Datatype: Term = "Datatype" + let datatype = Declaration("Datatype", Datatype(.Type) { I in + [ + "end": .Argument(I, const(.End)), + "recursive": .Argument(I, const(.Recursive(.End))), + "argument": Telescope.Argument(.Type) { A in .Argument(A --> _Datatype[I], const(.End)) }, + ] + }) return Module("Datatype", [ - Declaration("Datatype", Datatype(.Type) { I in - [ - "end": .Argument(I, const(.End)), - "recursive": .Argument(I, const(.Recursive(.End))), - "argument": Telescope.Argument(.Type) { A in .Argument(A --> _Datatype[I], const(.End)) }, - ] - }) + datatype ]) } } From 744f3a63a4317051b4af14d576ae5b6d3796a736 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sat, 12 Dec 2015 21:08:42 -0500 Subject: [PATCH 12/75] Define everything in the datatype-encoded Boolean module. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This is approximately correct, but note that I’m basically shrugging when it comes to `BooleanE`, and most of the dependencies aren’t actually defined. --- ManifoldTests/ModuleTests.swift | 52 ++++++++++++++++++++++++++++++++- 1 file changed, 51 insertions(+), 1 deletion(-) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index 4490d6a..83b9459 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -164,7 +164,57 @@ private let encodedList: Module = { private let datatypeEncodedBoolean: Module = { - return Module("DatatypeEncodedBoolean", []) + let Enum: Term = "Tag" + 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 BooleanE = Declaration("BooleanE", + type: Enum, + value: Enum[]) + + let BooleanT = Declaration("BooleanT", + type: .Type, + value: Tag[BooleanE.ref]) + + 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) + + let `false` = Declaration("false", + type: Boolean.ref, + value: `init`[falseT.ref, refl]) + + return Module("DatatypeEncodedBoolean", [ Module.unit, Module.datatype ], [ BooleanE, BooleanT, BooleanC, BooleanD, Boolean, trueT, `true`, falseT, `false` ]) }() From 4c159062bd248a51b4707c975836c423a65372e8 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 01:35:49 -0500 Subject: [PATCH 13/75] Stub in a Tag module. --- Manifold.xcodeproj/project.pbxproj | 4 ++++ Manifold/Module+Tag.swift | 7 +++++++ 2 files changed, 11 insertions(+) create mode 100644 Manifold/Module+Tag.swift diff --git a/Manifold.xcodeproj/project.pbxproj b/Manifold.xcodeproj/project.pbxproj index ca41110..cdb91c2 100644 --- a/Manifold.xcodeproj/project.pbxproj +++ b/Manifold.xcodeproj/project.pbxproj @@ -23,6 +23,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 */; }; D4A31B2A1AA366EC00B3FC68 /* TermContainerType.swift in Sources */ = {isa = PBXBuildFile; fileRef = D4A31B291AA366EC00B3FC68 /* TermContainerType.swift */; }; D4ACE90D1BDC7E51009E928F /* Module+FiniteSet.swift in Sources */ = {isa = PBXBuildFile; fileRef = D4ACE90C1BDC7E51009E928F /* Module+FiniteSet.swift */; }; D4B3FBF11A83515800DA2AC3 /* Manifold.h in Headers */ = {isa = PBXBuildFile; fileRef = D4B3FBF01A83515800DA2AC3 /* Manifold.h */; settings = {ATTRIBUTES = (Public, ); }; }; @@ -85,6 +86,7 @@ D470CB971BDC27130003A931 /* Module+Vector.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "Module+Vector.swift"; sourceTree = ""; }; D4809FBC1AF6BD400084B8FE /* TermTests.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = TermTests.swift; sourceTree = ""; }; D484903B1B2A40E800F249F7 /* EvaluationTests.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = EvaluationTests.swift; sourceTree = ""; }; + D492927A1C26837000BA59F3 /* Module+Tag.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "Module+Tag.swift"; sourceTree = ""; }; D4A31B291AA366EC00B3FC68 /* TermContainerType.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = TermContainerType.swift; sourceTree = ""; }; D4ACE90C1BDC7E51009E928F /* Module+FiniteSet.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "Module+FiniteSet.swift"; sourceTree = ""; }; D4B3FBEB1A83515800DA2AC3 /* Manifold.framework */ = {isa = PBXFileReference; explicitFileType = wrapper.framework; includeInIndex = 0; path = Manifold.framework; sourceTree = BUILT_PRODUCTS_DIR; }; @@ -235,6 +237,7 @@ 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 */, @@ -359,6 +362,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 */, diff --git a/Manifold/Module+Tag.swift b/Manifold/Module+Tag.swift new file mode 100644 index 0000000..87f27ef --- /dev/null +++ b/Manifold/Module+Tag.swift @@ -0,0 +1,7 @@ +// Copyright © 2015 Rob Rix. All rights reserved. + +extension Module { + public static var tag: Module { + return Module("Tag", []) + } +} From cbf1f67a753f13857fcd701888b8d0fc5fedf8be Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 01:35:57 -0500 Subject: [PATCH 14/75] Add the tag module to the directory. --- Manifold/Module+Directory.swift | 1 + 1 file changed, 1 insertion(+) diff --git a/Manifold/Module+Directory.swift b/Manifold/Module+Directory.swift index 76f7b05..b8e50c9 100644 --- a/Manifold/Module+Directory.swift +++ b/Manifold/Module+Directory.swift @@ -15,5 +15,6 @@ extension Module { finiteSet, string, datatype, + tag, ].map { ($0.name, $0) }) } From dadb2f6434ceced3b0715ae10b1ee81a0c750ec4 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 01:37:17 -0500 Subject: [PATCH 15/75] Tag depends on List. --- Manifold/Module+Tag.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manifold/Module+Tag.swift b/Manifold/Module+Tag.swift index 87f27ef..4fdfbd4 100644 --- a/Manifold/Module+Tag.swift +++ b/Manifold/Module+Tag.swift @@ -2,6 +2,6 @@ extension Module { public static var tag: Module { - return Module("Tag", []) + return Module("Tag", [ list ], []) } } From 603450b4af567355ab7d10ca137f9bfc5bcd2d51 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 01:37:52 -0500 Subject: [PATCH 16/75] Tag depends on String. --- Manifold/Module+Tag.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manifold/Module+Tag.swift b/Manifold/Module+Tag.swift index 4fdfbd4..8200ca8 100644 --- a/Manifold/Module+Tag.swift +++ b/Manifold/Module+Tag.swift @@ -2,6 +2,6 @@ extension Module { public static var tag: Module { - return Module("Tag", [ list ], []) + return Module("Tag", [ list, string ], []) } } From 424fb142f467b4a3a21cf452ca68ad7bf932796a Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 01:38:12 -0500 Subject: [PATCH 17/75] Add an Enum type to the Tag module. --- Manifold/Module+Tag.swift | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/Manifold/Module+Tag.swift b/Manifold/Module+Tag.swift index 8200ca8..7fd7361 100644 --- a/Manifold/Module+Tag.swift +++ b/Manifold/Module+Tag.swift @@ -2,6 +2,12 @@ extension Module { public static var tag: Module { - return Module("Tag", [ list, string ], []) + let List: Term = "List" + let String: Term = "String" + let Enum = Declaration("Enum", + type: .Type, + value: List[String]) + + return Module("Tag", [ list, string ], [ Enum ]) } } From a0affd6674cc1b6a1928a3221f1201ff5b692664 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 01:43:07 -0500 Subject: [PATCH 18/75] The Datatype module depends on the Tag module. --- Manifold/Module+Datatype.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index 1807ea4..bc94e48 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -10,7 +10,7 @@ extension Module { "argument": Telescope.Argument(.Type) { A in .Argument(A --> _Datatype[I], const(.End)) }, ] }) - return Module("Datatype", [ + return Module("Datatype", [ tag ], [ datatype ]) } From 46f799f1a89eb502e605a2c75aa858165f0390a0 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 01:44:09 -0500 Subject: [PATCH 19/75] Correct one of the stubbed in terms. --- ManifoldTests/ModuleTests.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index 58be4d2..13bdd14 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -211,7 +211,7 @@ private let embedCharacter: Character -> Term = { Term.Embedded($0, "Character") private let datatypeEncodedBoolean: Module = { - let Enum: Term = "Tag" + let Enum: Term = "Enum" let Tag: Term = "Tag" let here: Term = "here" let there: Term = "there" From 994d78c540a0695f85ee23ce34b8127a597e70ed Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 01:47:17 -0500 Subject: [PATCH 20/75] Define the Boolean enumeration. --- ManifoldTests/ModuleTests.swift | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index 13bdd14..1cc723d 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -212,6 +212,8 @@ 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" @@ -224,10 +226,13 @@ private let datatypeEncodedBoolean: Module = { 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 BooleanE = Declaration("BooleanE", type: Enum, - value: Enum[]) + value: cons[nil, embedString("true"), cons[nil, embedString("false"), `nil`[Term.Implicit]]]) let BooleanT = Declaration("BooleanT", type: .Type, From 59c6443441f7925d8ac917be908aa0de82ae5c59 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 08:51:58 -0500 Subject: [PATCH 21/75] Add a Tag binding. --- Manifold/Module+Tag.swift | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Manifold/Module+Tag.swift b/Manifold/Module+Tag.swift index 7fd7361..6a4fd72 100644 --- a/Manifold/Module+Tag.swift +++ b/Manifold/Module+Tag.swift @@ -8,6 +8,10 @@ extension Module { type: .Type, value: List[String]) - return Module("Tag", [ list, string ], [ Enum ]) + let Tag = Declaration("Tag", + type: Enum.ref --> .Type, + value: (Enum.ref, .Type) => { e, Motive in (Enum.ref --> Motive) => { f in f[e] } }) + + return Module("Tag", [ list, string ], [ Enum, Tag ]) } } From 5ffd5becc952414a56b2b21b6cb3684fdf256523 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 19:39:28 -0500 Subject: [PATCH 22/75] Tags eliminate from their specific labels. --- Manifold/Module+Tag.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manifold/Module+Tag.swift b/Manifold/Module+Tag.swift index 6a4fd72..4424e9a 100644 --- a/Manifold/Module+Tag.swift +++ b/Manifold/Module+Tag.swift @@ -10,7 +10,7 @@ extension Module { let Tag = Declaration("Tag", type: Enum.ref --> .Type, - value: (Enum.ref, .Type) => { e, Motive in (Enum.ref --> Motive) => { f in f[e] } }) + value: (Enum.ref, .Type) => { e, Motive in (String --> Motive) --> Motive }) return Module("Tag", [ list, string ], [ Enum, Tag ]) } From 447cc08a89b766504b3e692ea015e6a293cd202b Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 19:39:34 -0500 Subject: [PATCH 23/75] Add a `here` binding. --- Manifold/Module+Tag.swift | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/Manifold/Module+Tag.swift b/Manifold/Module+Tag.swift index 4424e9a..7650a1d 100644 --- a/Manifold/Module+Tag.swift +++ b/Manifold/Module+Tag.swift @@ -3,6 +3,7 @@ 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, @@ -12,6 +13,10 @@ extension Module { type: Enum.ref --> .Type, value: (Enum.ref, .Type) => { e, Motive in (String --> Motive) --> Motive }) - return Module("Tag", [ list, string ], [ Enum, Tag ]) + let here = Declaration("here", + type: (String, List[String]) => { l, E in Tag.ref[cons[nil, l, E]] }, + value: (String, List[String], .Type) => { s, _, Motive in (String --> Motive) => { f in f[s] } }) + + return Module("Tag", [ list, string ], [ Enum, Tag, here ]) } } From a58bcbb276e321236accc7df7e717a7af0b40dcb Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 19:41:58 -0500 Subject: [PATCH 24/75] Eliminate Tag casewise. --- Manifold/Module+Tag.swift | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Manifold/Module+Tag.swift b/Manifold/Module+Tag.swift index 7650a1d..8839e9a 100644 --- a/Manifold/Module+Tag.swift +++ b/Manifold/Module+Tag.swift @@ -11,11 +11,11 @@ extension Module { let Tag = Declaration("Tag", type: Enum.ref --> .Type, - value: (Enum.ref, .Type) => { e, Motive in (String --> Motive) --> Motive }) + 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) => { s, _, Motive in (String --> Motive) => { f in f[s] } }) + value: (String, List[String], .Type) => { s, _, Motive in (String --> Motive, List[String] --> Motive) => { f, _ in f[s] } }) return Module("Tag", [ list, string ], [ Enum, Tag, here ]) } From e37342c07e44d759e0b553a84b6b3db46493284f Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 19:43:56 -0500 Subject: [PATCH 25/75] Rename the label parameter. --- Manifold/Module+Tag.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manifold/Module+Tag.swift b/Manifold/Module+Tag.swift index 8839e9a..eb08b6b 100644 --- a/Manifold/Module+Tag.swift +++ b/Manifold/Module+Tag.swift @@ -15,7 +15,7 @@ extension Module { let here = Declaration("here", type: (String, List[String]) => { l, E in Tag.ref[cons[nil, l, E]] }, - value: (String, List[String], .Type) => { s, _, Motive in (String --> Motive, List[String] --> Motive) => { f, _ in f[s] } }) + value: (String, List[String], .Type) => { l, _, Motive in (String --> Motive, List[String] --> Motive) => { f, _ in f[l] } }) return Module("Tag", [ list, string ], [ Enum, Tag, here ]) } From 67a28f5031a48323eaae5642129e89dfa37281ec Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 19:45:24 -0500 Subject: [PATCH 26/75] Add a `there` binding. --- Manifold/Module+Tag.swift | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Manifold/Module+Tag.swift b/Manifold/Module+Tag.swift index eb08b6b..93a997b 100644 --- a/Manifold/Module+Tag.swift +++ b/Manifold/Module+Tag.swift @@ -17,6 +17,10 @@ extension Module { 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] } }) - return Module("Tag", [ list, string ], [ Enum, Tag, here ]) + 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] } } }) + + return Module("Tag", [ list, string ], [ Enum, Tag, here, there ]) } } From e14213ceb04a29292d6eb7cd59ad02bdbfd5be7d Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 19:46:06 -0500 Subject: [PATCH 27/75] The false tag follows the true tag. --- ManifoldTests/ModuleTests.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index 1cc723d..626edbc 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -260,7 +260,7 @@ private let datatypeEncodedBoolean: Module = { let falseT = Declaration("falseT", type: BooleanT.ref, - value: there) + value: there[here]) let `false` = Declaration("false", type: Boolean.ref, From aac26a78aa7af1772d1be88a5ae67a82bbdb7cb1 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 19:51:55 -0500 Subject: [PATCH 28/75] Log the error messages more legibly. --- ManifoldTests/ModuleTests.swift | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index 626edbc..83ad5d1 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -118,8 +118,8 @@ final class ModuleTests: XCTestCase { func testEquivalenceOfDatatypeEncodedAndDatatypeBooleans() { datatypeEncodedBoolean.definitions.forEach { symbol, type, value in - assert(Module.boolean.context[symbol], ==, type, message: "'\(symbol)' expected '\(type)', actual '\(Module.boolean.context[symbol])'") - assert(Module.boolean.environment[symbol], ==, value, message: "'\(symbol)' expected '\(value)', actual '\(Module.boolean.environment[symbol])'") + assert(Module.boolean.context[symbol], ==, type, message: "'\(symbol)'\nexpected : '\(type)',\n actual : '\(Module.boolean.context[symbol])'") + assert(Module.boolean.environment[symbol], ==, value, message: "'\(symbol)'\nexpected = '\(value)',\n actual = '\(Module.boolean.environment[symbol])'") } } } From 474ee0e624986786f64b35b0c9383498c8f4afbf Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 19:52:51 -0500 Subject: [PATCH 29/75] Log whether this is a type mismatch or a term mismatch. --- ManifoldTests/ModuleTests.swift | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index 83ad5d1..39a0430 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -118,8 +118,8 @@ final class ModuleTests: XCTestCase { func testEquivalenceOfDatatypeEncodedAndDatatypeBooleans() { datatypeEncodedBoolean.definitions.forEach { symbol, type, value in - assert(Module.boolean.context[symbol], ==, type, message: "'\(symbol)'\nexpected : '\(type)',\n actual : '\(Module.boolean.context[symbol])'") - assert(Module.boolean.environment[symbol], ==, value, message: "'\(symbol)'\nexpected = '\(value)',\n actual = '\(Module.boolean.environment[symbol])'") + assert(Module.boolean.context[symbol], ==, type, message: "Type mismatch in '\(symbol)'\nexpected : '\(type)',\n actual : '\(Module.boolean.context[symbol])'") + assert(Module.boolean.environment[symbol], ==, value, message: "Term mismatch in '\(symbol)'\nexpected = '\(value)',\n actual = '\(Module.boolean.environment[symbol])'") } } } From a148c43ad18fb22338e09304a9590914c010cfa1 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 20:01:34 -0500 Subject: [PATCH 30/75] Abstract a method to assert equivalent definitions. --- ManifoldTests/ModuleTests.swift | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index 39a0430..6dfd311 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -116,6 +116,18 @@ final class ModuleTests: XCTestCase { // MARK: Datatype + func assertEquivalent(definition: (Name, Term, Term), _ module: Module, _ file: String = __FILE__, _ line: UInt = __LINE__) { + let (symbol, type, value) = definition + assert(module.context[symbol], ==, type, message: + "Type mismatch in '\(module.name).\(symbol)'\n" + + "expected : \(type)\n" + + " actual : \(module.context[symbol])\n", file: file, line: line) + assert(module.environment[symbol], ==, value, message: + "Term mismatch in '\(module.name).\(symbol)'\n" + + "expected : \(value)\n" + + " actual : \(module.environment[symbol])\n", file: file, line: line) + } + func testEquivalenceOfDatatypeEncodedAndDatatypeBooleans() { datatypeEncodedBoolean.definitions.forEach { symbol, type, value in assert(Module.boolean.context[symbol], ==, type, message: "Type mismatch in '\(symbol)'\nexpected : '\(type)',\n actual : '\(Module.boolean.context[symbol])'") From a6914f2483cec81c836a089609362551549235f3 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 20:03:03 -0500 Subject: [PATCH 31/75] Pretty-print the actual values. --- ManifoldTests/ModuleTests.swift | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index 6dfd311..577505a 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -121,11 +121,11 @@ final class ModuleTests: XCTestCase { assert(module.context[symbol], ==, type, message: "Type mismatch in '\(module.name).\(symbol)'\n" + "expected : \(type)\n" - + " actual : \(module.context[symbol])\n", file: file, line: line) + + " actual : \(module.context[symbol] ?? "nil")\n", file: file, line: line) assert(module.environment[symbol], ==, value, message: "Term mismatch in '\(module.name).\(symbol)'\n" + "expected : \(value)\n" - + " actual : \(module.environment[symbol])\n", file: file, line: line) + + " actual : \(module.environment[symbol] ?? "nil")\n", file: file, line: line) } func testEquivalenceOfDatatypeEncodedAndDatatypeBooleans() { From 32c70b79df04c68ee4f297ee3417394c39687969 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 20:03:14 -0500 Subject: [PATCH 32/75] Delegate the equivalence assertions. --- ManifoldTests/ModuleTests.swift | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index 577505a..c0f092b 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -129,9 +129,8 @@ final class ModuleTests: XCTestCase { } func testEquivalenceOfDatatypeEncodedAndDatatypeBooleans() { - datatypeEncodedBoolean.definitions.forEach { symbol, type, value in - assert(Module.boolean.context[symbol], ==, type, message: "Type mismatch in '\(symbol)'\nexpected : '\(type)',\n actual : '\(Module.boolean.context[symbol])'") - assert(Module.boolean.environment[symbol], ==, value, message: "Term mismatch in '\(symbol)'\nexpected = '\(value)',\n actual = '\(Module.boolean.environment[symbol])'") + datatypeEncodedBoolean.definitions.forEach { definition in + assertEquivalent(definition, Module.boolean) } } } From 8b43b94d40597045501c14cb9825fca90e421b21 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 20:04:37 -0500 Subject: [PATCH 33/75] Test the equivalence of only the intersection. --- ManifoldTests/ModuleTests.swift | 1 + 1 file changed, 1 insertion(+) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index c0f092b..f099e75 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -130,6 +130,7 @@ final class ModuleTests: XCTestCase { func testEquivalenceOfDatatypeEncodedAndDatatypeBooleans() { datatypeEncodedBoolean.definitions.forEach { definition in + guard Module.boolean.context[definition.0] != nil else { return } assertEquivalent(definition, Module.boolean) } } From 10abab0049c813ad6e486ec8aceac0cffbffc8d6 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 20:05:39 -0500 Subject: [PATCH 34/75] Move the assertion into its own section. --- ManifoldTests/ModuleTests.swift | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index f099e75..1cbe594 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -116,6 +116,16 @@ final class ModuleTests: XCTestCase { // MARK: Datatype + func testEquivalenceOfDatatypeEncodedAndDatatypeBooleans() { + datatypeEncodedBoolean.definitions.forEach { definition in + guard Module.boolean.context[definition.0] != nil else { return } + assertEquivalent(definition, Module.boolean) + } + } + + + // MARK: Assertions + func assertEquivalent(definition: (Name, Term, Term), _ module: Module, _ file: String = __FILE__, _ line: UInt = __LINE__) { let (symbol, type, value) = definition assert(module.context[symbol], ==, type, message: @@ -127,13 +137,6 @@ final class ModuleTests: XCTestCase { + "expected : \(value)\n" + " actual : \(module.environment[symbol] ?? "nil")\n", file: file, line: line) } - - func testEquivalenceOfDatatypeEncodedAndDatatypeBooleans() { - datatypeEncodedBoolean.definitions.forEach { definition in - guard Module.boolean.context[definition.0] != nil else { return } - assertEquivalent(definition, Module.boolean) - } - } } From 209d59ade5b601feb1e67e3eeeb97620e7d06564 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 20:09:43 -0500 Subject: [PATCH 35/75] Delegate all of the equivalences tests to the new assertion. --- ManifoldTests/ModuleTests.swift | 25 ++++++++++--------------- 1 file changed, 10 insertions(+), 15 deletions(-) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index 1cbe594..46c0441 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -11,9 +11,8 @@ final class ModuleTests: XCTestCase { // MARK: Boolean func testEquivalenceOfEncodedAndDatatypeBooleans() { - encodedBoolean.definitions.forEach { symbol, type, value in - assert(Module.boolean.context[symbol], ==, type, message: "\(symbol)") - assert(Module.boolean.environment[symbol], ==, value, message: "\(symbol)") + encodedBoolean.definitions.forEach { definition in + assertEquivalent(definition, Module.boolean) } } @@ -32,9 +31,8 @@ final class ModuleTests: XCTestCase { // MARK: Pair func testEquivalenceOfEncodedAndDatatypePairs() { - encodedPair.definitions.forEach { symbol, type, value in - assert(Module.pair.context[symbol], ==, type, message: "\(symbol)") - assert(Module.pair.environment[symbol], ==, value, message: "\(symbol)") + encodedPair.definitions.forEach { definition in + assertEquivalent(definition, Module.pair) } } @@ -42,9 +40,8 @@ final class ModuleTests: XCTestCase { // MARK: Sigma func testEquivalenceOfEncodedAndDatatypeSigmas() { - encodedSigma.definitions.forEach { symbol, type, value in - assert(Module.sigma.context[symbol], ==, type, message: "'\(symbol)' expected '\(type)', actual '\(Module.sigma.context[symbol])'") - assert(Module.sigma.environment[symbol], ==, value, message: "'\(symbol)' expected '\(value)', actual '\(Module.sigma.environment[symbol])'") + encodedSigma.definitions.forEach { definition in + assertEquivalent(definition, Module.sigma) } } @@ -52,9 +49,8 @@ final class ModuleTests: XCTestCase { // MARK: Either func testEquivalenceOfEncodedAndDatatypeEithers() { - Module.either.definitions.forEach { symbol, type, value in - assert(encodedEither.context[symbol], ==, type, message: "'\(symbol)' expected '\(type), actual '\(Module.either.context[symbol])'") - assert(encodedEither.environment[symbol], ==, value, message: "'\(symbol)' expected '\(type)', actual '\(Module.either.environment[symbol])'") + Module.either.definitions.forEach { definition in + assertEquivalent(definition, encodedEither) } } @@ -62,9 +58,8 @@ final class ModuleTests: XCTestCase { // MARK: List func testEquivalenceOfEncodedAndDatatypeLists() { - encodedList.definitions.forEach { symbol, type, value in - assert(Module.list.context[symbol], ==, type, message: "'\(symbol)' expected '\(type)', actual '\(Module.list.context[symbol])'") - assert(Module.list.environment[symbol], ==, value, message: "'\(symbol)' expected '\(value)', actual '\(Module.list.environment[symbol])'") + encodedList.definitions.forEach { definition in + assertEquivalent(definition, Module.list) } } From b47ba76e4d32b3a818274c03f59bf65c7f89adf6 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 20:13:04 -0500 Subject: [PATCH 36/75] Test only the intersection in the assertion. --- ManifoldTests/ModuleTests.swift | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index 46c0441..a5aee3c 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -113,7 +113,6 @@ final class ModuleTests: XCTestCase { func testEquivalenceOfDatatypeEncodedAndDatatypeBooleans() { datatypeEncodedBoolean.definitions.forEach { definition in - guard Module.boolean.context[definition.0] != nil else { return } assertEquivalent(definition, Module.boolean) } } @@ -123,14 +122,18 @@ final class ModuleTests: XCTestCase { func assertEquivalent(definition: (Name, Term, Term), _ module: Module, _ file: String = __FILE__, _ line: UInt = __LINE__) { let (symbol, type, value) = definition - assert(module.context[symbol], ==, type, message: - "Type mismatch in '\(module.name).\(symbol)'\n" - + "expected : \(type)\n" - + " actual : \(module.context[symbol] ?? "nil")\n", file: file, line: line) - assert(module.environment[symbol], ==, value, message: - "Term mismatch in '\(module.name).\(symbol)'\n" - + "expected : \(value)\n" - + " actual : \(module.environment[symbol] ?? "nil")\n", file: file, line: line) + if let actual = module.context[symbol] { + assert(actual, ==, 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, ==, value, message: + "Term mismatch in '\(module.name).\(symbol)'\n" + + "expected : \(value)\n" + + " actual : \(actual)\n", file: file, line: line) + } } } From dedbd006453a2f48c4ee9cbb363abc0ded463aea Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 20:13:59 -0500 Subject: [PATCH 37/75] =?UTF-8?q?Add=20an=20assertion=20of=20the=20equival?= =?UTF-8?q?ence=20of=20two=20modules=E2=80=99=20intersections.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ManifoldTests/ModuleTests.swift | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index a5aee3c..e1d51ac 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -120,6 +120,10 @@ final class ModuleTests: XCTestCase { // 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] { From 0f978ba6f7666aa1c1d28dad02a6bbdde28ebbe1 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 20:15:17 -0500 Subject: [PATCH 38/75] Delegate module equivalence assertions to the new assertion method. --- ManifoldTests/ModuleTests.swift | 24 ++++++------------------ 1 file changed, 6 insertions(+), 18 deletions(-) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index e1d51ac..4e78b0a 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -11,9 +11,7 @@ final class ModuleTests: XCTestCase { // MARK: Boolean func testEquivalenceOfEncodedAndDatatypeBooleans() { - encodedBoolean.definitions.forEach { definition in - assertEquivalent(definition, Module.boolean) - } + assertEquivalent(encodedBoolean, Module.boolean) } @@ -31,36 +29,28 @@ final class ModuleTests: XCTestCase { // MARK: Pair func testEquivalenceOfEncodedAndDatatypePairs() { - encodedPair.definitions.forEach { definition in - assertEquivalent(definition, Module.pair) - } + assertEquivalent(encodedPair, Module.pair) } // MARK: Sigma func testEquivalenceOfEncodedAndDatatypeSigmas() { - encodedSigma.definitions.forEach { definition in - assertEquivalent(definition, Module.sigma) - } + assertEquivalent(encodedSigma, Module.sigma) } // MARK: Either func testEquivalenceOfEncodedAndDatatypeEithers() { - Module.either.definitions.forEach { definition in - assertEquivalent(definition, encodedEither) - } + assertEquivalent(encodedEither, Module.either) } // MARK: List func testEquivalenceOfEncodedAndDatatypeLists() { - encodedList.definitions.forEach { definition in - assertEquivalent(definition, Module.list) - } + assertEquivalent(encodedList, Module.list) } func testListValuesAsEliminators() { @@ -112,9 +102,7 @@ final class ModuleTests: XCTestCase { // MARK: Datatype func testEquivalenceOfDatatypeEncodedAndDatatypeBooleans() { - datatypeEncodedBoolean.definitions.forEach { definition in - assertEquivalent(definition, Module.boolean) - } + assertEquivalent(datatypeEncodedBoolean, Module.boolean) } From 9e390a8ca09bfbc925be1c51c94fb1174a69658d Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 21:45:54 -0500 Subject: [PATCH 39/75] Formatting. --- Manifold/Module+Datatype.swift | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index bc94e48..e12506c 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -10,9 +10,7 @@ extension Module { "argument": Telescope.Argument(.Type) { A in .Argument(A --> _Datatype[I], const(.End)) }, ] }) - return Module("Datatype", [ tag ], [ - datatype - ]) + return Module("Datatype", [ tag ], [ datatype ]) } } From 2795353069de469a1a05dbb54c1281020bca71cc Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 21:48:18 -0500 Subject: [PATCH 40/75] =?UTF-8?q?Provide=20a=20definition=20of=20=CE=BC.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Manifold/Module+Datatype.swift | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index e12506c..9aaecf9 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -10,7 +10,12 @@ extension Module { "argument": Telescope.Argument(.Type) { A in .Argument(A --> _Datatype[I], const(.End)) }, ] }) - return Module("Datatype", [ tag ], [ datatype ]) + + 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 } }) + + return Module("Datatype", [ tag ], [ datatype, μ ]) } } From ad71dd5a2e73d7c5c090128c955fac72cfb1917d Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 21:50:58 -0500 Subject: [PATCH 41/75] Stub in an `init` binding. --- Manifold/Module+Datatype.swift | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index 9aaecf9..11578b5 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -15,7 +15,12 @@ extension Module { type: nil => { I in _Datatype[I] --> I --> .Type }, value: nil => { I in (_Datatype[I], I, .Type) => { _, _, Motive in (_Datatype[I] --> I --> Motive) --> Motive } }) - return Module("Datatype", [ tag ], [ datatype, μ ]) + let El: Term = "El" + let `init` = Declaration("init", + type: nil => { I in (_Datatype[I], I) => { D, i in El[D, μ.ref[D], i] --> μ.ref[D, i] } }, + value: nil) + + return Module("Datatype", [ tag ], [ datatype, μ, `init` ]) } } From 866e1dfc3f8651ddabb88d9e933ff38c578a88e6 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 21:59:57 -0500 Subject: [PATCH 42/75] Add a declaration of `ISet`. --- Manifold/Module+Datatype.swift | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index 11578b5..9ffbe1d 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -15,12 +15,16 @@ extension Module { type: nil => { I in _Datatype[I] --> I --> .Type }, value: nil => { I in (_Datatype[I], I, .Type) => { _, _, Motive in (_Datatype[I] --> I --> Motive) --> Motive } }) + let ISet = Declaration("ISet", + type: .Type --> .Type(1), + value: .Type => { I in I --> .Type }) + let El: Term = "El" let `init` = Declaration("init", type: nil => { I in (_Datatype[I], I) => { D, i in El[D, μ.ref[D], i] --> μ.ref[D, i] } }, value: nil) - return Module("Datatype", [ tag ], [ datatype, μ, `init` ]) + return Module("Datatype", [ tag ], [ datatype, μ, `init`, ISet ]) } } From e85717a91b311d6ed736e7fd93dd7676778c140f Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 22:00:27 -0500 Subject: [PATCH 43/75] =?UTF-8?q?Rename=20ISet=20=E2=86=92=20IType,=20as?= =?UTF-8?q?=20it=E2=80=99s=20more=20in=20the=20zeitgeist.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Manifold/Module+Datatype.swift | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index 9ffbe1d..928f4da 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -15,7 +15,7 @@ extension Module { type: nil => { I in _Datatype[I] --> I --> .Type }, value: nil => { I in (_Datatype[I], I, .Type) => { _, _, Motive in (_Datatype[I] --> I --> Motive) --> Motive } }) - let ISet = Declaration("ISet", + let IType = Declaration("IType", type: .Type --> .Type(1), value: .Type => { I in I --> .Type }) @@ -24,7 +24,7 @@ extension Module { type: nil => { I in (_Datatype[I], I) => { D, i in El[D, μ.ref[D], i] --> μ.ref[D, i] } }, value: nil) - return Module("Datatype", [ tag ], [ datatype, μ, `init`, ISet ]) + return Module("Datatype", [ tag ], [ datatype, μ, `init`, IType ]) } } From 1e8fcb782d180a0c705b2762b6127da241c738c1 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 22:04:40 -0500 Subject: [PATCH 44/75] Datatype depends on PropositionalEquality. --- Manifold/Module+Datatype.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index 928f4da..f7db2b8 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -24,7 +24,7 @@ extension Module { type: nil => { I in (_Datatype[I], I) => { D, i in El[D, μ.ref[D], i] --> μ.ref[D, i] } }, value: nil) - return Module("Datatype", [ tag ], [ datatype, μ, `init`, IType ]) + return Module("Datatype", [ tag, propositionalEquality ], [ datatype, μ, `init`, IType ]) } } From 303e44f0dfafe32a1a27f088e3ce0ddd04326b32 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 22:09:58 -0500 Subject: [PATCH 45/75] Datatype depends on Pair. --- Manifold/Module+Datatype.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index f7db2b8..5ea5d86 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -24,7 +24,7 @@ extension Module { type: nil => { I in (_Datatype[I], I) => { D, i in El[D, μ.ref[D], i] --> μ.ref[D, i] } }, value: nil) - return Module("Datatype", [ tag, propositionalEquality ], [ datatype, μ, `init`, IType ]) + return Module("Datatype", [ tag, propositionalEquality, pair ], [ datatype, μ, `init`, IType, el ]) } } From 80e3f41fd57773167f966402faf6f879512a0ff5 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 22:12:12 -0500 Subject: [PATCH 46/75] Datatype depends on Sigma. --- Manifold/Module+Datatype.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index 5ea5d86..9f34804 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -24,7 +24,7 @@ extension Module { type: nil => { I in (_Datatype[I], I) => { D, i in El[D, μ.ref[D], i] --> μ.ref[D, i] } }, value: nil) - return Module("Datatype", [ tag, propositionalEquality, pair ], [ datatype, μ, `init`, IType, el ]) + return Module("Datatype", [ tag, propositionalEquality, pair, sigma ], [ datatype, μ, `init`, IType, el ]) } } From ad9bb65888661c66eaef6dfd7fd22ff9e2f2a0fe Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 22:22:40 -0500 Subject: [PATCH 47/75] Define `El` by eliminating datatypes. --- Manifold/Module+Datatype.swift | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index 9f34804..d4fe443 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -19,7 +19,21 @@ extension Module { 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] --> (I --> .Type) --> I --> .Type }, + 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[D, X, i]] }, + (.Type) => { A in (A --> _Datatype[I]) => { B in Sigma[A, nil => { a in El[B[a], X, i] }] } }] + } + }) + let `init` = Declaration("init", type: nil => { I in (_Datatype[I], I) => { D, i in El[D, μ.ref[D], i] --> μ.ref[D, i] } }, value: nil) From 5bbcac483e7ea866e991d5e08b4fc9739126a8be Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 22:50:11 -0500 Subject: [PATCH 48/75] El expects a type parameter. --- Manifold/Module+Datatype.swift | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index d4fe443..95207cc 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -29,13 +29,13 @@ extension Module { (_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[D, X, i]] }, - (.Type) => { A in (A --> _Datatype[I]) => { B in Sigma[A, nil => { a in El[B[a], X, i] }] } }] + (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[D, μ.ref[D], i] --> μ.ref[D, i] } }, + type: nil => { I in (_Datatype[I], I) => { D, i in El[I, D, μ.ref[D], i] --> μ.ref[D, i] } }, value: nil) return Module("Datatype", [ tag, propositionalEquality, pair, sigma ], [ datatype, μ, `init`, IType, el ]) From 7d85abc726da3ff6a4f043db2b181ff56e34e313 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 22:51:24 -0500 Subject: [PATCH 49/75] =?UTF-8?q?=CE=BC=20expects=20a=20type=20parameter.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Manifold/Module+Datatype.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index 95207cc..096efd5 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -35,7 +35,7 @@ extension Module { }) let `init` = Declaration("init", - type: nil => { I in (_Datatype[I], I) => { D, i in El[I, D, μ.ref[D], i] --> μ.ref[D, i] } }, + type: nil => { I in (_Datatype[I], I) => { D, i in El[I, D, μ.ref[I, D], i] --> μ.ref[I, D, i] } }, value: nil) return Module("Datatype", [ tag, propositionalEquality, pair, sigma ], [ datatype, μ, `init`, IType, el ]) From d09ee519f129221a2ab3a06310c0d8ca55d47adc Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 22:59:06 -0500 Subject: [PATCH 50/75] Test whether bindings are definitionally equal. --- ManifoldTests/ModuleTests.swift | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index 4e78b0a..82d4398 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -114,14 +114,15 @@ final class ModuleTests: XCTestCase { func assertEquivalent(definition: (Name, Term, Term), _ module: Module, _ file: String = __FILE__, _ line: UInt = __LINE__) { let (symbol, type, value) = definition + let equate = { l, r in Term.equate(l, r, module.environment) != nil } if let actual = module.context[symbol] { - assert(actual, ==, type, message: + assert(actual, 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, ==, value, message: + assert(actual, equate, value, message: "Term mismatch in '\(module.name).\(symbol)'\n" + "expected : \(value)\n" + " actual : \(actual)\n", file: file, line: line) From 354e939a2e0a424d197c8c3d92f7925def63ce39 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 23:00:38 -0500 Subject: [PATCH 51/75] Remove a use of IType. --- Manifold/Module+Datatype.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index 096efd5..248c0bc 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -26,7 +26,7 @@ extension Module { let el = Declaration("El", type: .Type => { I in _Datatype[I] --> (I --> .Type) --> I --> .Type }, value: .Type => { I in - (_Datatype[I], IType.ref[I], I) => { D, X, i in + (_Datatype[I], I --> .Type, 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]] }, From aef38efa1db6416282e681cdae7b1a7fff1817b3 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 23:00:52 -0500 Subject: [PATCH 52/75] Revert "Remove a use of IType." This reverts commit 354e939a2e0a424d197c8c3d92f7925def63ce39. --- Manifold/Module+Datatype.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index 248c0bc..096efd5 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -26,7 +26,7 @@ extension Module { let el = Declaration("El", type: .Type => { I in _Datatype[I] --> (I --> .Type) --> I --> .Type }, value: .Type => { I in - (_Datatype[I], I --> .Type, I) => { D, X, 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]] }, From cf4ddca1d34df7655d02cb5215dd838d18c5bf0f Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 23:01:22 -0500 Subject: [PATCH 53/75] Use `IType` a bit more widely. --- Manifold/Module+Datatype.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index 096efd5..345d758 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -24,7 +24,7 @@ extension Module { let Sigma: Term = "Sigma" let El: Term = "El" let el = Declaration("El", - type: .Type => { I in _Datatype[I] --> (I --> .Type) --> I --> .Type }, + 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, From 18ab314ae428bec5fdd5850f8f2916f5c2636b8c Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 23:05:07 -0500 Subject: [PATCH 54/75] Remove unnecessary parens. --- Manifold/Module+Datatype.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index 345d758..9ef586d 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -30,7 +30,7 @@ extension Module { 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] }] } }] + .Type => { A in (A --> _Datatype[I]) => { B in Sigma[A, nil => { a in El[I, B[a], X, i] }] } }] } }) From 933cfde30cf8dbde676f1485de22ed390b6e4e20 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 23:13:50 -0500 Subject: [PATCH 55/75] Stub in some more of the definition of `init`. --- Manifold/Module+Datatype.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manifold/Module+Datatype.swift b/Manifold/Module+Datatype.swift index 9ef586d..3a36f57 100644 --- a/Manifold/Module+Datatype.swift +++ b/Manifold/Module+Datatype.swift @@ -36,7 +36,7 @@ extension Module { 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) + value: nil => { I in (nil, nil) => { D, i in nil => { _ in nil } } }) return Module("Datatype", [ tag, propositionalEquality, pair, sigma ], [ datatype, μ, `init`, IType, el ]) } From 61e93375fae568cfddc8d9ca9af1aba930c735c5 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 23:14:26 -0500 Subject: [PATCH 56/75] Typecheck the datatype-encoded booleans. --- ManifoldTests/ModuleTests.swift | 1 + 1 file changed, 1 insertion(+) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index 82d4398..8fb382d 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -102,6 +102,7 @@ final class ModuleTests: XCTestCase { // MARK: Datatype func testEquivalenceOfDatatypeEncodedAndDatatypeBooleans() { + datatypeEncodedBoolean.typecheck().forEach { XCTFail($0) } assertEquivalent(datatypeEncodedBoolean, Module.boolean) } From e97a3ba41a6595c405a277cd5884cf46e1067548 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 23:14:47 -0500 Subject: [PATCH 57/75] Inline the enumeration of boolean case names. --- ManifoldTests/ModuleTests.swift | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index 8fb382d..8cb81d9 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -237,13 +237,9 @@ private let datatypeEncodedBoolean: Module = { let embedString: Swift.String -> Term = { .Embedded($0, String) } - let BooleanE = Declaration("BooleanE", - type: Enum, - value: cons[nil, embedString("true"), cons[nil, embedString("false"), `nil`[Term.Implicit]]]) - let BooleanT = Declaration("BooleanT", type: .Type, - value: Tag[BooleanE.ref]) + value: Tag[cons[nil, embedString("true"), cons[nil, embedString("false"), `nil`[Term.Implicit]]]]) let BooleanC = Declaration("BooleanC", type: BooleanT.ref --> Datatype[Unit], @@ -273,7 +269,7 @@ private let datatypeEncodedBoolean: Module = { type: Boolean.ref, value: `init`[falseT.ref, refl]) - return Module("DatatypeEncodedBoolean", [ Module.unit, Module.datatype ], [ BooleanE, BooleanT, BooleanC, BooleanD, Boolean, trueT, `true`, falseT, `false` ]) + return Module("DatatypeEncodedBoolean", [ Module.unit, Module.datatype ], [ BooleanT, BooleanC, BooleanD, Boolean, trueT, `true`, falseT, `false` ]) }() From 0727b6f51b4b7ed4628f97a492103f60caa8fb3f Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Sun, 20 Dec 2015 23:15:05 -0500 Subject: [PATCH 58/75] =?UTF-8?q?=C2=B5=20=E2=86=92=20=CE=BC.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- ManifoldTests/ModuleTests.swift | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index 8cb81d9..7b99a8b 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -227,7 +227,7 @@ private let datatypeEncodedBoolean: Module = { let Datatype: Term = "Datatype" let argument: Term = "argument" let end: Term = "end" - let µ: Term = "µ" + let μ: Term = "μ" let caseD: Term = "caseD" let `init`: Term = "init" let refl: Term = "refl" @@ -251,7 +251,7 @@ private let datatypeEncodedBoolean: Module = { let Boolean = Declaration("Boolean", type: .Type, - value: µ[BooleanD.ref]) + value: μ[BooleanD.ref]) let trueT = Declaration("trueT", type: BooleanT.ref, From f3cd0ff97813f401f2e239d36fb68708428e1696 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Tue, 22 Dec 2015 21:26:25 -0500 Subject: [PATCH 59/75] Stub in a `Branches` binding. --- Manifold/Module+Tag.swift | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/Manifold/Module+Tag.swift b/Manifold/Module+Tag.swift index 93a997b..a629126 100644 --- a/Manifold/Module+Tag.swift +++ b/Manifold/Module+Tag.swift @@ -21,6 +21,13 @@ extension Module { 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] } } }) - return Module("Tag", [ list, string ], [ Enum, Tag, here, there ]) + 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], Branches[E, nil => { t in P[there.ref[t]] }]] }, Unit] } }) + + return Module("Tag", [ list, string, unit, pair ], [ Enum, Tag, here, there, branches ]) } } From 9350cb83de1bdaa1905174d6fd944eb286505d3e Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Tue, 22 Dec 2015 21:38:01 -0500 Subject: [PATCH 60/75] here/there expect more parameters. --- Manifold/Module+Tag.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manifold/Module+Tag.swift b/Manifold/Module+Tag.swift index a629126..470ac4a 100644 --- a/Manifold/Module+Tag.swift +++ b/Manifold/Module+Tag.swift @@ -26,7 +26,7 @@ extension Module { 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], Branches[E, nil => { t in P[there.ref[t]] }]] }, Unit] } }) + 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] } }) return Module("Tag", [ list, string, unit, pair ], [ Enum, Tag, here, there, branches ]) } From 0fa47119481cbf495d56ed32c70951629be51ca7 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Tue, 22 Dec 2015 21:38:33 -0500 Subject: [PATCH 61/75] The first argument apparently needs to be `List String` instead of `Enum`. Something will need to be done about synonyms not working, but for now this works around it. --- Manifold/Module+Tag.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manifold/Module+Tag.swift b/Manifold/Module+Tag.swift index 470ac4a..3443b5f 100644 --- a/Manifold/Module+Tag.swift +++ b/Manifold/Module+Tag.swift @@ -25,7 +25,7 @@ extension Module { let Pair: Term = "Pair" let Branches: Term = "Branches" let branches = Declaration("Branches", - type: Enum.ref => { E in (Tag.ref[E] --> .Type) --> .Type }, + type: List[String] => { 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] } }) return Module("Tag", [ list, string, unit, pair ], [ Enum, Tag, here, there, branches ]) From 8ecda221911f88e2883b3181ceb1833d3a8777f2 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Tue, 22 Dec 2015 21:41:17 -0500 Subject: [PATCH 62/75] Stub in a `case` definition. --- Manifold/Module+Tag.swift | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/Manifold/Module+Tag.swift b/Manifold/Module+Tag.swift index 3443b5f..19fce4a 100644 --- a/Manifold/Module+Tag.swift +++ b/Manifold/Module+Tag.swift @@ -28,6 +28,11 @@ extension Module { type: List[String] => { 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] } }) - return Module("Tag", [ list, string, unit, pair ], [ Enum, Tag, here, there, branches ]) + 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 => { _ in nil }) + + + return Module("Tag", [ list, string, unit, pair ], [ Enum, Tag, here, there, branches, `case` ]) } } From a31a7735b5e1c883a882ab298d4be6e99d9e7e85 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Tue, 22 Dec 2015 21:42:01 -0500 Subject: [PATCH 63/75] Type the first argument to `case` as `List String`. --- Manifold/Module+Tag.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manifold/Module+Tag.swift b/Manifold/Module+Tag.swift index 19fce4a..115386d 100644 --- a/Manifold/Module+Tag.swift +++ b/Manifold/Module+Tag.swift @@ -29,7 +29,7 @@ extension Module { 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 `case` = Declaration("case", - type: Enum.ref => { E in (Tag.ref[E] --> .Type) => { P in Branches[E, P] --> Tag.ref[E] => { t in P[t] } } }, + type: List[String] => { E in (Tag.ref[E] --> .Type) => { P in Branches[E, P] --> Tag.ref[E] => { t in P[t] } } }, value: nil => { _ in nil }) From ba11f5550999be524f9f5fcef8b70f3dfa905219 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Tue, 22 Dec 2015 21:55:13 -0500 Subject: [PATCH 64/75] Stub in the value for `case`. --- Manifold/Module+Tag.swift | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/Manifold/Module+Tag.swift b/Manifold/Module+Tag.swift index 115386d..aadabdc 100644 --- a/Manifold/Module+Tag.swift +++ b/Manifold/Module+Tag.swift @@ -28,9 +28,12 @@ extension Module { type: List[String] => { 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 _case: Term = "case" + let first: Term = "first" + let second: Term = "second" let `case` = Declaration("case", type: List[String] => { E in (Tag.ref[E] --> .Type) => { P in Branches[E, P] --> Tag.ref[E] => { t in P[t] } } }, - value: nil => { _ in nil }) + value: nil => { E in nil => { P in (nil, nil) => { cs, t in t[nil, nil => { _ in first[nil, nil, cs] }, nil => { t in _case[E, nil => { t in P[E, there.ref[nil, nil, t]] }, second[nil, nil, cs], t] }] } } }) return Module("Tag", [ list, string, unit, pair ], [ Enum, Tag, here, there, branches, `case` ]) From 1aa1459b37f7c5c8cfb11f2c7b9493037dddba97 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Tue, 22 Dec 2015 22:38:03 -0500 Subject: [PATCH 65/75] Reduce the annotation. This seems broken. --- Manifold/Term+Elaboration.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manifold/Term+Elaboration.swift b/Manifold/Term+Elaboration.swift index 5eb9fc6..7861957 100644 --- a/Manifold/Term+Elaboration.swift +++ b/Manifold/Term+Elaboration.swift @@ -52,7 +52,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 From 8b7dabdff68026f2b3c71f9673c1fc473d7fc2af Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Tue, 22 Dec 2015 22:55:36 -0500 Subject: [PATCH 66/75] Spacing. --- Manifold/Module+Tag.swift | 1 - 1 file changed, 1 deletion(-) diff --git a/Manifold/Module+Tag.swift b/Manifold/Module+Tag.swift index aadabdc..ad047e2 100644 --- a/Manifold/Module+Tag.swift +++ b/Manifold/Module+Tag.swift @@ -35,7 +35,6 @@ extension Module { type: List[String] => { 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 first[nil, nil, cs] }, nil => { t in _case[E, nil => { t in P[E, there.ref[nil, nil, t]] }, second[nil, nil, cs], t] }] } } }) - return Module("Tag", [ list, string, unit, pair ], [ Enum, Tag, here, there, branches, `case` ]) } } From 63aff41b7f27b6ba661d287e1ec513e9dfa738d8 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Tue, 22 Dec 2015 23:54:08 -0500 Subject: [PATCH 67/75] Type the enumerations as Enum. --- Manifold/Module+Tag.swift | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Manifold/Module+Tag.swift b/Manifold/Module+Tag.swift index ad047e2..b76d3ed 100644 --- a/Manifold/Module+Tag.swift +++ b/Manifold/Module+Tag.swift @@ -25,14 +25,14 @@ extension Module { let Pair: Term = "Pair" let Branches: Term = "Branches" let branches = Declaration("Branches", - type: List[String] => { E in (Tag.ref[E] --> .Type) --> .Type }, + 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 _case: Term = "case" let first: Term = "first" let second: Term = "second" let `case` = Declaration("case", - type: List[String] => { E in (Tag.ref[E] --> .Type) => { P in Branches[E, P] --> Tag.ref[E] => { t in P[t] } } }, + 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 first[nil, nil, cs] }, nil => { t in _case[E, nil => { t in P[E, there.ref[nil, nil, t]] }, second[nil, nil, cs], t] }] } } }) return Module("Tag", [ list, string, unit, pair ], [ Enum, Tag, here, there, branches, `case` ]) From edee9465e2fe602c1441b01bd59682d7d109e597 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Tue, 22 Dec 2015 23:57:45 -0500 Subject: [PATCH 68/75] Correct the definitions of first & second. --- Manifold/Module+Pair.swift | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Manifold/Module+Pair.swift b/Manifold/Module+Pair.swift index 98b8475..b3e881e 100644 --- a/Manifold/Module+Pair.swift +++ b/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 ]) } From 33751b49e3f70b028ffbfc6e8dace02d619ce45d Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Tue, 22 Dec 2015 23:58:30 -0500 Subject: [PATCH 69/75] Attempt to elaborate the types of applications against a lambda type. --- Manifold/Term+Elaboration.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manifold/Term+Elaboration.swift b/Manifold/Term+Elaboration.swift index 7861957..f5b3241 100644 --- a/Manifold/Term+Elaboration.swift +++ b/Manifold/Term+Elaboration.swift @@ -16,7 +16,7 @@ extension Term { return .Unroll(type, .Variable(name)) case let (.Application(a, b), .Implicit): - let aʹ = try a.elaborateType(nil, environment, context) + let aʹ = try a.elaborateType(nil --> nil, environment, context) guard case let .Lambda(i, 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: "="))" } From c41c4d90a347cae0ae885730e46a295d63219b87 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Fri, 25 Dec 2015 10:24:32 -0500 Subject: [PATCH 70/75] Add a `firstBranch` binding to eliminate values in `Branches`. --- Manifold/Module+Tag.swift | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/Manifold/Module+Tag.swift b/Manifold/Module+Tag.swift index b76d3ed..ad4fad7 100644 --- a/Manifold/Module+Tag.swift +++ b/Manifold/Module+Tag.swift @@ -28,13 +28,17 @@ extension Module { 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 _case: Term = "case" 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 _case: Term = "case" let second: Term = "second" 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 first[nil, nil, cs] }, nil => { t in _case[E, nil => { t in P[E, there.ref[nil, nil, t]] }, second[nil, nil, cs], t] }] } } }) - return Module("Tag", [ list, string, unit, pair ], [ Enum, Tag, here, there, branches, `case` ]) + return Module("Tag", [ list, string, unit, pair ], [ Enum, Tag, here, there, branches, firstBranch, `case` ]) } } From 1bcfb0240a07d7ef76412f6cfdca868057870f4e Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Fri, 25 Dec 2015 10:27:05 -0500 Subject: [PATCH 71/75] Add a `secondBranch` binding. --- Manifold/Module+Tag.swift | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/Manifold/Module+Tag.swift b/Manifold/Module+Tag.swift index ad4fad7..5a7300b 100644 --- a/Manifold/Module+Tag.swift +++ b/Manifold/Module+Tag.swift @@ -33,12 +33,16 @@ extension Module { 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 _case: Term = "case" 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 first[nil, nil, cs] }, nil => { t in _case[E, nil => { t in P[E, there.ref[nil, nil, t]] }, second[nil, nil, cs], t] }] } } }) - return Module("Tag", [ list, string, unit, pair ], [ Enum, Tag, here, there, branches, firstBranch, `case` ]) + return Module("Tag", [ list, string, unit, pair ], [ Enum, Tag, here, there, branches, firstBranch, secondBranch, `case` ]) } } From 161d7506cf67a84badf77e45914a53bf583cba42 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Fri, 25 Dec 2015 10:33:29 -0500 Subject: [PATCH 72/75] Define `case` in terms of `firstBranch`. --- Manifold/Module+Tag.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manifold/Module+Tag.swift b/Manifold/Module+Tag.swift index 5a7300b..8a6d4a4 100644 --- a/Manifold/Module+Tag.swift +++ b/Manifold/Module+Tag.swift @@ -41,7 +41,7 @@ extension Module { 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 first[nil, nil, cs] }, nil => { t in _case[E, nil => { t in P[E, there.ref[nil, nil, t]] }, second[nil, nil, cs], 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]] }, second[nil, nil, cs], t] }] } } }) return Module("Tag", [ list, string, unit, pair ], [ Enum, Tag, here, there, branches, firstBranch, secondBranch, `case` ]) } From c7b260a6afe4da66416ae00bfa4cfdc4dd5fff2c Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Fri, 25 Dec 2015 10:33:39 -0500 Subject: [PATCH 73/75] Define `case` in terms of `secondBranch`. --- Manifold/Module+Tag.swift | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manifold/Module+Tag.swift b/Manifold/Module+Tag.swift index 8a6d4a4..f38560e 100644 --- a/Manifold/Module+Tag.swift +++ b/Manifold/Module+Tag.swift @@ -41,7 +41,7 @@ extension Module { 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]] }, second[nil, nil, cs], 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` ]) } From b249859cb5342173cd1938fdbb87caff88d6c7e6 Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Fri, 1 Jan 2016 01:29:23 -0500 Subject: [PATCH 74/75] Indicate value mismatches with =. --- ManifoldTests/ModuleTests.swift | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index c5ce211..9bb0996 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -128,8 +128,8 @@ final class ModuleTests: XCTestCase { if let actual = module.environment[symbol] { assert(actual, equate, value, message: "Term mismatch in '\(module.name).\(symbol)'\n" - + "expected : \(value)\n" - + " actual : \(actual)\n", file: file, line: line) + + "expected = \(value)\n" + + " actual = \(actual)\n", file: file, line: line) } } } From 31b80bccd3b0596ed49c27f3b4eeb062a7bb361a Mon Sep 17 00:00:00 2001 From: Rob Rix Date: Fri, 1 Jan 2016 01:31:05 -0500 Subject: [PATCH 75/75] Use the Term.equate method. --- ManifoldTests/ModuleTests.swift | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/ManifoldTests/ModuleTests.swift b/ManifoldTests/ModuleTests.swift index 9bb0996..048252c 100644 --- a/ManifoldTests/ModuleTests.swift +++ b/ManifoldTests/ModuleTests.swift @@ -118,15 +118,14 @@ final class ModuleTests: XCTestCase { func assertEquivalent(definition: (Name, Term, Term), _ module: Module, _ file: String = __FILE__, _ line: UInt = __LINE__) { let (symbol, type, value) = definition - let equate = { l, r in Term.equate(l, r, module.environment) != nil } if let actual = module.context[symbol] { - assert(actual, equate, type, message: + 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, equate, value, message: + assert(actual, Term.equate, value, message: "Term mismatch in '\(module.name).\(symbol)'\n" + "expected = \(value)\n" + " actual = \(actual)\n", file: file, line: line)