Embedded terms

Manifold.xcodeproj/project.pbxproj

@@ -9,6 +9,7 @@
 /* Begin PBXBuildFile section */
 		D415A09B1B51EFDE001C15E5 /* Term+Construction.swift in Sources */ = {isa = PBXBuildFile; fileRef = D415A09A1B51EFDE001C15E5 /* Term+Construction.swift */; };
 		D43AC8831BC1824D008762B7 /* Telescope.swift in Sources */ = {isa = PBXBuildFile; fileRef = D43AC8821BC1824D008762B7 /* Telescope.swift */; };
+		D43B6D1B1C1DB2CA008EF3D2 /* Module+String.swift in Sources */ = {isa = PBXBuildFile; fileRef = D43B6D1A1C1DB2CA008EF3D2 /* Module+String.swift */; };
 		D445417C1BCAB0C100F2946D /* Module+Unit.swift in Sources */ = {isa = PBXBuildFile; fileRef = D445417B1BCAB0C100F2946D /* Module+Unit.swift */; };
 		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 */; };
@@ -69,6 +70,7 @@
 /* Begin PBXFileReference section */
 		D415A09A1B51EFDE001C15E5 /* Term+Construction.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "Term+Construction.swift"; sourceTree = "<group>"; };
 		D43AC8821BC1824D008762B7 /* Telescope.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = Telescope.swift; sourceTree = "<group>"; };
+		D43B6D1A1C1DB2CA008EF3D2 /* Module+String.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "Module+String.swift"; sourceTree = "<group>"; };
 		D445417B1BCAB0C100F2946D /* Module+Unit.swift */ = {isa = PBXFileReference; fileEncoding = 4; lastKnownFileType = sourcecode.swift; path = "Module+Unit.swift"; sourceTree = "<group>"; };
 		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>"; };
@@ -241,6 +243,7 @@
 				D470CB971BDC27130003A931 /* Module+Vector.swift */,
 				D4ACE90C1BDC7E51009E928F /* Module+FiniteSet.swift */,
 				D4FB2D0A1BE44DAF00B3CCE0 /* Module+Functor.swift */,
+				D43B6D1A1C1DB2CA008EF3D2 /* Module+String.swift */,
 			);
 			name = Modules;
 			sourceTree = "<group>";
@@ -355,6 +358,7 @@
 			files = (
 				D445417C1BCAB0C100F2946D /* Module+Unit.swift in Sources */,
 				D4E9901C1BD3431D00F00CA7 /* Module+Either.swift in Sources */,
+				D43B6D1B1C1DB2CA008EF3D2 /* Module+String.swift in Sources */,
 				D415A09B1B51EFDE001C15E5 /* Term+Construction.swift in Sources */,
 				D44541901BCB028A00F2946D /* TermContainerType+CustomDebugStringConvertible.swift in Sources */,
 				D44541841BCAEDCD00F2946D /* Term+WeakHeadNormalForm.swift in Sources */,

Manifold/Expression.swift

@@ -5,6 +5,7 @@ public enum Expression<Recur> {
 	case Variable(Name)
 	case Application(Recur, Recur)
 	case Lambda(Int, Recur?, Recur)
+	case Embedded(Any, (Any, Any) -> Bool, Recur)
 
 
 	// MARK: Functor
@@ -19,6 +20,8 @@ public enum Expression<Recur> {
 			return try .Application(transform(a), transform(b))
 		case let .Lambda(i, a, b):
 			return try .Lambda(i, a.map(transform), transform(b))
+		case let .Embedded(a, eq, b):
+			return try .Embedded(a, eq, transform(b))
 		}
 	}
 
@@ -35,6 +38,8 @@ public enum Expression<Recur> {
 			return equal(t1, u1) && equal(t2, u2)
 		case let (.Lambda(i, t, a), .Lambda(j, u, b)):
 			return i == j && ((t &&& u).map(equal) ?? (t == nil && u == nil)) && equal(a, b)
+		case let (.Embedded(a, eq, t1), .Embedded(b, _, t2)) where a.dynamicType == b.dynamicType:
+			return eq(a, b) && equal(t1, t2)
 		default:
 			return false
 		}

Manifold/Module+Directory.swift

@@ -13,5 +13,6 @@ extension Module {
 		sigma,
 		vector,
 		finiteSet,
+		string,
 	].map { ($0.name, $0) })
 }

Manifold/Module+String.swift

@@ -0,0 +1,35 @@
+//  Copyright © 2015 Rob Rix. All rights reserved.
+
+extension Module {
+	public static var string: Module {
+		let List: Term = "List"
+		let cons: Term = "cons"
+		let `nil`: Term = "nil"
+
+		let String = Declaration("String",
+			type: .Type,
+			value: .Embedded(Swift.String.self))
+
+		let Character = Declaration("Character",
+			type: .Type,
+			value: .Embedded(Swift.Character.self))
+
+		func toTerm(characters: Swift.String.CharacterView) -> Term {
+			switch characters.first {
+			case let .Some(c):
+				return cons[Character.ref, .Embedded(c), toTerm(characters.dropFirst())]
+			default:
+				return `nil`[Character.ref]
+			}
+		}
+
+		let toList = Declaration("toList",
+			type: String.ref --> List[Character.ref],
+			value: () => { (string: Term) -> Term in
+				guard case let .Embedded(value as Swift.String, _, _) = string.out else { return ("toList" as Term)[string] }
+				return toTerm(value.characters)
+			})
+
+		return Module("String", [ list ], [ String, Character, toList ])
+	}
+}

Manifold/Term+Construction.swift

@@ -21,6 +21,26 @@ extension Term {
 		return Term(.Lambda(i, type, body))
 	}
 
+	public static func Embedded<A>(value: A, _ equal: (A, A) -> Bool, _ type: Term) -> Term {
+		let equal: (Any, Any) -> Bool = { a, b in
+			guard let a = a as? A, b = b as? A else { return false }
+			return equal(a, b)
+		}
+		return Term(.Embedded(value as Any, equal, type))
+	}
+
+	public static func Embedded<A: Equatable>(value: A, _ type: Term) -> Term {
+		return .Embedded(value, ==, type)
+	}
+
+	public static func Embedded<A: Equatable>(value: A) -> Term {
+		return .Embedded(value, .Embedded(A.self))
+	}
+
+	public static func Embedded<A: Equatable>(type: A.Type) -> Term {
+		return .Embedded(A.self, ==, .Type)
+	}
+
 
 	public subscript (operands: Term...) -> Term {
 		return operands.reduce(self, combine: Term.Application)

Manifold/Term+Elaboration.swift

@@ -28,6 +28,10 @@ extension Term {
 				let bʹ = try b.elaborateType(nil, environment, context + [ .Local(i): a ])
 				return .Unroll(a => { bʹ.annotation.substitute(i, $0) }, .Lambda(i, aʹ, bʹ))
 
+			case let (.Embedded(value, eq, type), .None):
+				let typeʹ = try type.elaborateType(.Type, environment, context)
+				return .Unroll(type, .Embedded(value, eq, typeʹ))
+
 			case let (.Type(m), .Some(.Type(n))) where n > m:
 				return try elaborateType(nil, environment, context)
 

Manifold/TermContainerType+CustomDebugStringConvertible.swift

@@ -12,6 +12,8 @@ extension TermContainerType {
 				return ".Application(\(a), \(b))"
 			case let .Lambda(i, a, b):
 				return ".Lambda(\(i), \(a), \(b))"
+			case let .Embedded(value, eq, type):
+				return ".Embedded(\(String(reflecting: value)), \(String(reflecting: eq)), \(type))"
 			}
 		}
 	}

Manifold/TermContainerType+CustomStringConvertible.swift

@@ -27,6 +27,9 @@ extension TermContainerType {
 
 			case let .Lambda(variable, _, (_, (body, _))):
 				return ("λ \(Name.Local(variable)) . \(body)", true)
+
+			case let .Embedded(value, _, (_, (type, _))):
+				return ("'\(value)' : \(type)", true)
 			}
 		}
 		return out

Manifold/TermContainerType+FreeVariables.swift

@@ -14,6 +14,8 @@ extension TermContainerType {
 				return i < 0 ? max(a, b) : max(i, a)
 			case let .Lambda(i, .None, b):
 				return i < 0 ? b : i
+			case let .Embedded(_, _, type):
+				return type
 			}
 		}
 	}
@@ -29,6 +31,8 @@ extension TermContainerType {
 				return a + b
 			case let .Lambda(i, a, b):
 				return (a ?? []) + b.filter { $0 != i }
+			case let .Embedded(_, _, type):
+				return type
 			}
 		}
 	}