[WIP] Diff entire types

Manifold.xcodeproj/project.pbxproj

@@ -14,7 +14,6 @@
 		D44541801BCAC38500F2946D /* Module+List.swift in Sources */ = {isa = PBXBuildFile; fileRef = D445417F1BCAC38500F2946D /* Module+List.swift */; };
 		D44541841BCAEDCD00F2946D /* Term+WeakHeadNormalForm.swift in Sources */ = {isa = PBXBuildFile; fileRef = D44541831BCAEDCD00F2946D /* Term+WeakHeadNormalForm.swift */; };
 		D44541861BCAEF1000F2946D /* Term+Substitution.swift in Sources */ = {isa = PBXBuildFile; fileRef = D44541851BCAEF1000F2946D /* Term+Substitution.swift */; };
-		D445418C1BCAF3ED00F2946D /* Term+DefinitionalEquality.swift in Sources */ = {isa = PBXBuildFile; fileRef = D445418B1BCAF3ED00F2946D /* Term+DefinitionalEquality.swift */; };
 		D445418E1BCAF57D00F2946D /* Term+Evaluation.swift in Sources */ = {isa = PBXBuildFile; fileRef = D445418D1BCAF57D00F2946D /* Term+Evaluation.swift */; };
 		D44541901BCB028A00F2946D /* TermContainerType+CustomDebugStringConvertible.swift in Sources */ = {isa = PBXBuildFile; fileRef = D445418F1BCB028A00F2946D /* TermContainerType+CustomDebugStringConvertible.swift */; };
 		D44541921BCB030F00F2946D /* TermContainerType+CustomStringConvertible.swift in Sources */ = {isa = PBXBuildFile; fileRef = D44541911BCB030F00F2946D /* TermContainerType+CustomStringConvertible.swift */; };
@@ -23,6 +22,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 */; };
+		D492927D1C2726F900BA59F3 /* Unification.swift in Sources */ = {isa = PBXBuildFile; fileRef = D492927C1C2726F900BA59F3 /* Unification.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 */; };
@@ -76,7 +76,6 @@
 		D445417F1BCAC38500F2946D /* Module+List.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "Module+List.swift"; sourceTree = "<group>"; };
 		D44541831BCAEDCD00F2946D /* Term+WeakHeadNormalForm.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "Term+WeakHeadNormalForm.swift"; sourceTree = "<group>"; };
 		D44541851BCAEF1000F2946D /* Term+Substitution.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "Term+Substitution.swift"; sourceTree = "<group>"; };
-		D445418B1BCAF3ED00F2946D /* Term+DefinitionalEquality.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "Term+DefinitionalEquality.swift"; sourceTree = "<group>"; };
 		D445418D1BCAF57D00F2946D /* Term+Evaluation.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "Term+Evaluation.swift"; sourceTree = "<group>"; };
 		D445418F1BCB028A00F2946D /* TermContainerType+CustomDebugStringConvertible.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "TermContainerType+CustomDebugStringConvertible.swift"; sourceTree = "<group>"; };
 		D44541911BCB030F00F2946D /* TermContainerType+CustomStringConvertible.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "TermContainerType+CustomStringConvertible.swift"; sourceTree = "<group>"; };
@@ -85,6 +84,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>"; };
+		D492927C1C2726F900BA59F3 /* Unification.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = Unification.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>"; };
@@ -178,8 +178,8 @@
 				D445418D1BCAF57D00F2946D /* Term+Evaluation.swift */,
 				D4D0FBFF1BD420B20010F243 /* Term+Elaboration.swift */,
 				D44541851BCAEF1000F2946D /* Term+Substitution.swift */,
-				D445418B1BCAF3ED00F2946D /* Term+DefinitionalEquality.swift */,
 				D415A09A1B51EFDE001C15E5 /* Term+Construction.swift */,
+				D492927C1C2726F900BA59F3 /* Unification.swift */,
 				D445418F1BCB028A00F2946D /* TermContainerType+CustomDebugStringConvertible.swift */,
 				D44541911BCB030F00F2946D /* TermContainerType+CustomStringConvertible.swift */,
 				D4E1F7121BD4176100FCA0B4 /* TermContainerType+FreeVariables.swift */,
@@ -373,6 +373,7 @@
 				D4B56CB11AFDA26A00D7BD6F /* Expression.swift in Sources */,
 				D4B4AA571A90320F0089A5F2 /* Dictionary.swift in Sources */,
 				D4E8289D1B5202BB00713E60 /* StringLiteralConvertible.swift in Sources */,
+				D492927D1C2726F900BA59F3 /* Unification.swift in Sources */,
 				D4EDEF571AFEDEC5001B9A1D /* Name.swift in Sources */,
 				D4A31B2A1AA366EC00B3FC68 /* TermContainerType.swift in Sources */,
 				D44541801BCAC38500F2946D /* Module+List.swift in Sources */,
@@ -386,7 +387,6 @@
 				D4E829191B521BFC00713E60 /* Declaration.swift in Sources */,
 				D4D0FC021BD4276B0010F243 /* Module+Pair.swift in Sources */,
 				D492927F1C278CC000BA59F3 /* Module+PropositionalEquality.swift in Sources */,
-				D445418C1BCAF3ED00F2946D /* Term+DefinitionalEquality.swift in Sources */,
 				D4DE7E731AF66E25004D0CB9 /* Term.swift in Sources */,
 				D44541941BCB389400F2946D /* Datatype.swift in Sources */,
 				D4FB02D91B71D06A0090E764 /* Module+Boolean.swift in Sources */,

Manifold/AnnotatedTerm.swift

@@ -20,6 +20,14 @@ public enum AnnotatedTerm<Annotation>: TermContainerType {
 	}
 
 
+	// MARK: Functor
+
+	public func map<Other>(@noescape transform: Annotation throws -> Other) rethrows -> AnnotatedTerm<Other> {
+		let (annotation, expression) = destructure
+		return try .Unroll(transform(annotation), expression.map { try $0.map(transform) })
+	}
+
+
 	// MARK: TermContainerType
 
 	public var out: Expression<AnnotatedTerm> {

Manifold/Term+Elaboration.swift

@@ -4,56 +4,66 @@ extension String: ErrorType {}
 
 extension Term {
 	public func elaborateType(against: Term, _ environment: [Name:Term], _ context: [Name:Term]) throws -> AnnotatedTerm<Term> {
+		return try elaborateUnification(against, environment, context).map {
+			guard let unified = $0.unified else {
+				throw "Type mismatch for '\(self)':\n\($0)in context: \(Term.toString(context, separator: ":")),\nenvironment: \(Term.toString(environment, separator: "="))"
+			}
+			return unified
+		}
+	}
+
+	public func elaborateUnification(against: Term, _ environment: [Name:Term], _ context: [Name:Term]) throws -> AnnotatedTerm<Unification> {
 		do {
 			switch (out, against.weakHeadNormalForm(environment).out) {
 			case let (.Type(n), .Implicit):
-				return .Unroll(.Type(n + 1), .Type(n))
+				return .Unroll(Unification(.Type(n + 1)), .Type(n))
 
 			case let (.Variable(name), .Implicit):
 				guard let type = context[name] else {
 					throw "Unexpectedly free variable \(name) in context: \(Term.toString(context, separator: ":")), environment: \(Term.toString(environment, separator: "="))"
 				}
-				return .Unroll(type, .Variable(name))
+				return .Unroll(Unification(type), .Variable(name))
 
 			case let (.Application(a, b), .Implicit):
-				let aʹ = try a.elaborateType(nil, environment, context)
-				guard case let .Lambda(i, type, body) = aʹ.annotation.weakHeadNormalForm(environment).out else {
+				let aʹ = try a.elaborateUnification(nil, environment, context)
+				guard case let .Lambda(i, type, body) = aʹ.annotation.actual.weakHeadNormalForm(environment).out else {
 					throw "Illegal application of \(a) : \(aʹ.annotation) in context: \(Term.toString(context, separator: ":")), environment: \(Term.toString(environment, separator: "="))"
 				}
-				let bʹ = try b.elaborateType(type, environment, context)
-				return .Unroll(body.substitute(i, b), .Application(aʹ, bʹ))
+				let bʹ = try b.elaborateUnification(type, environment, context)
+				return .Unroll(Unification(body.substitute(i, b)), .Application(aʹ, bʹ))
 
 			case let (.Lambda(i, a, b), .Implicit) where a != nil:
-				let aʹ = try a.elaborateType(.Type, environment, context)
-				let bʹ = try b.elaborateType(nil, environment, context + [ .Local(i): a ])
-				return .Unroll(a => { bʹ.annotation.substitute(i, $0) }, .Lambda(i, aʹ, bʹ))
+				let aʹ = try a.elaborateUnification(.Type, environment, context)
+				let bʹ = try b.elaborateUnification(nil, environment, context + [ .Local(i): a ])
+				return .Unroll(Unification(a => { bʹ.annotation.actual.substitute(i, $0) }), .Lambda(i, aʹ, bʹ))
 
 			case let (.Embedded(value, eq, type), .Implicit):
-				let typeʹ = try type.elaborateType(.Type, environment, context)
-				return .Unroll(type, .Embedded(value, eq, typeʹ))
+				let typeʹ = try type.elaborateUnification(.Type, environment, context)
+				return .Unroll(Unification(type), .Embedded(value, eq, typeʹ))
 
 			case let (.Type(m), .Type(n)) where n > m:
-				return try elaborateType(nil, environment, context)
+				return try elaborateUnification(nil, environment, context)
 
-			case let (.Lambda(i, type, body), .Lambda(j, type2, bodyType)) where Term.equate(type, type2, environment) != nil:
-				let t = try type2.elaborateType(.Type, environment, context)
-				let b = try body.elaborateType(bodyType.substitute(j, Term.Variable(Name.Local(i))), environment, context + [ Name.Local(i) : type2 ])
-				return .Unroll(.Lambda(j, type2, bodyType), .Lambda(i, t, b))
+			case let (.Lambda(i, type, body), .Lambda(j, type2, bodyType)) where Unification(type, type2, environment).unified != nil:
+				let t = try type2.elaborateUnification(.Type, environment, context)
+				let b = try body.elaborateUnification(bodyType.substitute(j, Term.Variable(Name.Local(i))), environment, context + [ Name.Local(i) : type2 ])
+				return .Unroll(Unification(.Lambda(j, type2, bodyType)), .Lambda(i, t, b))
 
 			case let (.Lambda(i, type, body), .Type(n)):
-				let typeʹ = try type.elaborateType(.Type, environment, context) ?? .Unroll(.Type(n + 1), .Type(n))
-				return .Unroll(.Lambda(i, .Type, .Type), .Lambda(i, typeʹ, try body.elaborateType(.Type, environment, context + [ Name.Local(i) : type ?? .Type(n) ])))
+				let typeʹ = try type.elaborateUnification(.Type, environment, context) ?? .Unroll(Unification(.Type(n + 1)), .Type(n))
+				return .Unroll(Unification(.Lambda(i, .Type, .Type)), .Lambda(i, typeʹ, try body.elaborateUnification(.Type, environment, context + [ Name.Local(i) : type ?? .Type(n) ])))
 
 			case (.Implicit, .Implicit):
 				throw "No rule to infer type of '\(self)'"
 
 			case let (.Implicit, type):
-				return .Unroll(Term(type), .Implicit)
+				return .Unroll(Unification(Term(type)), .Implicit)
 
 			case let (_, b):
-				let a = try elaborateType(nil, environment, context)
-				guard Term.equate(a.annotation, 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: "="))"
+				let a = try elaborateUnification(nil, environment, context)
+				let unification = Unification(a.annotation.actual, Term(b), environment)
+				guard unification.unified != nil else {
+					throw "Type mismatch for '\(self)':\n\(unification)in context: \(Term.toString(context, separator: ":")),\nenvironment: \(Term.toString(environment, separator: "="))"
 				}
 				return a
 			}

Manifold/Unification.swift

@@ -0,0 +1,95 @@
+//  Copyright © 2015 Rob Rix. All rights reserved.
+
+public enum Unification: CustomStringConvertible {
+	case Patch(Term, Term)
+	indirect case Roll(Expression<Unification>)
+
+	public init(_ term: Term) {
+		self = .Roll(term.out.map(Unification.init))
+	}
+
+	public init(_ left: Term, _ right: Term, _ environment: [Name:Term]) {
+		var visited: Set<Term> = []
+		func unify(left: Term, _ right: Term) -> (Unification, Set<Term>) {
+			let (leftʹ, visitedLeft) = left.weakHeadNormalForm(environment, shouldRecur: false, visited: visited)
+			let (rightʹ, visitedRight) = right.weakHeadNormalForm(environment, shouldRecur: false, visited: visited)
+			visited.unionInPlace(visitedLeft)
+			visited.unionInPlace(visitedRight)
+
+			if leftʹ == rightʹ { return (Unification(rightʹ), visited) }
+
+			switch (leftʹ.out, rightʹ.out) {
+			case (.Implicit, _):
+				return (Unification(rightʹ), visited)
+			case (_, .Implicit):
+				return (Unification(leftʹ), visited)
+
+			case (.Type, .Type):
+				return (Unification(rightʹ), visited)
+
+			case let (.Application(a1, b1), .Application(a2, b2)):
+				let (a, visitedA) = unify(a1, a2)
+				let (b, visitedB) = unify(b1, b2)
+				visited.unionInPlace(visitedA)
+				visited.unionInPlace(visitedB)
+				return (.Roll(.Application(a, b)), visited)
+
+			case let (.Lambda(_, type1, body1), .Lambda(i, type2, body2)):
+				let (type, visitedType) = unify(type1, type2)
+				let (body, visitedBody) = unify(body1, body2)
+				visited.unionInPlace(visitedType)
+				visited.unionInPlace(visitedBody)
+				return (.Roll(.Lambda(i, type, body)), visited)
+
+			default:
+				return (.Patch(leftʹ, rightʹ), visited)
+			}
+		}
+		(self, _) = unify(left, right)
+	}
+
+
+	/// Produces the unified term for the receiver, if any.
+	///
+	/// This will be a valid term for unifiable terms, and `nil` otherwise.
+	public var unified: Term? {
+		struct E: ErrorType {}
+		func unified(diff: Unification) throws -> Term {
+			switch diff {
+			case .Patch:
+				throw E()
+
+			case let .Roll(expression):
+				return try Term(expression.map(unified))
+			}
+		}
+		return try? unified(self)
+	}
+
+
+	public var expected: Term {
+		switch self {
+		case let .Patch(_, expected):
+			return expected
+		case let .Roll(expression):
+			return Term(expression.map { $0.expected })
+		}
+	}
+
+	public var actual: Term {
+		switch self {
+		case let .Patch(actual, _):
+			return actual
+		case let .Roll(expression):
+			return Term(expression.map { $0.actual })
+		}
+	}
+
+
+	// MARK: CustomStringConvertible
+
+	public var description: String {
+		guard let unified = unified else { return "Expected: \(expected)\n" + "  Actual: \(actual)\n" }
+		return "\(unified)"
+	}
+}

ManifoldTests/ModuleTests.swift

@@ -84,8 +84,8 @@ final class ModuleTests: XCTestCase {
 			list[Boolean, (unit, List[Unit]) => { _ in `false` }, `true`]
 		}
 
-		assert((try? isEmpty[list].evaluate(module.environment)).flatMap { Term.equate($0, `false`, module.environment) }, !=, nil)
-		assert((try? isEmpty[`nil`[Term.Implicit]].evaluate(module.environment)).flatMap { Term.equate($0, `true`, module.environment) }, !=, nil)
+		assert((try? isEmpty[list].evaluate(module.environment)).flatMap { Unification($0, `false`, module.environment).unified }, !=, nil)
+		assert((try? isEmpty[`nil`[Term.Implicit]].evaluate(module.environment)).flatMap { Unification($0, `true`, module.environment).unified }, !=, nil)
 	}