miniKanren
// µKanren | |
struct Var: Equatable, Hashable { | |
let i: Int | |
init(_ i: Int) { | |
self.i = i | |
} | |
} | |
enum Term: Equatable { | |
case none | |
case int(Int) | |
case double(Double) | |
case string(String) | |
case bool(Bool) | |
indirect case pair(Term, Term) | |
case `var`(Var) | |
case sym(String) | |
} | |
extension Term: CustomStringConvertible { | |
var description: String { | |
switch self { | |
case .int(let i): | |
return "\(i)" | |
case .double(let d): | |
return "\(d)" | |
case .string(let s): | |
return "\"\(s)\"" | |
case .bool(let b): | |
return "\(b)" | |
case .var(let v): | |
return "\(v)" | |
case .sym(let s): | |
return s | |
case .none: | |
return "()" | |
case .pair(_, _): | |
var elements = [String]() | |
var l = self | |
while case .pair(let first, let rest) = l { | |
elements.append("\(first)") | |
l = rest | |
} | |
if l != Term.none { | |
elements.append(". \(l)") | |
} | |
return "(\(elements.joined(separator: " ")))" | |
} | |
} | |
} | |
extension Term: ExpressibleByIntegerLiteral { | |
init(integerLiteral: Int) { | |
self = .int(integerLiteral) | |
} | |
} | |
extension Term: ExpressibleByFloatLiteral { | |
init(floatLiteral: Double) { | |
self = .double(floatLiteral) | |
} | |
} | |
extension Term: ExpressibleByStringLiteral { | |
init(stringLiteral: String) { | |
self = .string(stringLiteral) | |
} | |
} | |
extension Term: ExpressibleByBooleanLiteral { | |
init(booleanLiteral: Bool) { | |
self = .bool(booleanLiteral) | |
} | |
} | |
extension Term: ExpressibleByArrayLiteral { | |
init(arrayLiteral elements: Term...) { | |
var l: Term = .none | |
for e in elements.reversed() { | |
l = .pair(e, l) | |
} | |
self = l | |
} | |
} | |
extension Term: Sequence { | |
struct Iterator: IteratorProtocol { | |
var term: Term | |
mutating func next() -> Term? { | |
switch term { | |
case .pair(let value, let next): | |
defer { term = next } | |
return value | |
default: | |
return nil | |
} | |
} | |
} | |
public func makeIterator() -> Iterator { | |
return Iterator(term: self) | |
} | |
} | |
typealias Substitution = [Var: Term] | |
extension Substitution { | |
func walk(_ u: Term) -> Term { | |
if case .var(let u) = u, let v = self[u] { | |
return walk(v) | |
} else { | |
return u | |
} | |
} | |
func extend(_ x: Var, _ v: Term) -> Substitution { | |
return merging([x: v]) { current, new in new } | |
} | |
} | |
struct State: CustomStringConvertible { | |
let sub: Substitution | |
var nfresh: Int | |
static let empty = State(sub: Substitution(), nfresh: 0) | |
var description: String { | |
return "{\(sub) \(nfresh)}" | |
} | |
mutating func makeVar() -> Term { | |
defer { nfresh += 1 } | |
return .var(Var(nfresh)) | |
} | |
} | |
enum Stream { | |
case empty | |
indirect case mature(State, Stream) | |
case immature(() -> Stream) | |
static func unit(_ state: State) -> Stream { | |
return .mature(state, .empty) | |
} | |
func append(_ other: Stream) -> Stream { | |
switch self { | |
case .empty: | |
return other | |
case .immature(let f): | |
return .immature { other.append(f()) } | |
case .mature(let state, let rest): | |
return .mature(state, rest.append(other)) | |
} | |
} | |
func appendMap(_ g: @escaping Goal) -> Stream { | |
switch self { | |
case .empty: | |
return .empty | |
case .immature(let f): | |
return .immature { f().appendMap(g) } | |
case .mature(let state, let rest): | |
return g(state).append(rest.appendMap(g)) | |
} | |
} | |
} | |
extension Stream: Sequence { | |
struct Iterator: IteratorProtocol { | |
var stream: Stream | |
mutating func next() -> Stream? { | |
switch stream { | |
case .mature(_, let next): | |
defer { stream = next } | |
return stream | |
case .immature(_): | |
defer { stream = .empty } | |
return stream | |
case .empty: | |
return nil | |
} | |
} | |
} | |
public func makeIterator() -> Iterator { | |
return Iterator(stream: self) | |
} | |
} | |
extension Stream: CustomStringConvertible { | |
var description: String { | |
let elements = compactMap { stream in | |
switch stream { | |
case .mature(let state, _): | |
return String(describing: state) | |
case .immature(_): | |
return "..." | |
case .empty: | |
return nil | |
} | |
}.joined(separator: " ") | |
return "(\(elements))" | |
} | |
} | |
func unify(_ u: Term, _ v: Term, _ s: Substitution) -> Substitution? { | |
let u = s.walk(u) | |
let v = s.walk(v) | |
if case .var(let u) = u, case .var(let v) = v, u == v { | |
return s | |
} else if case .var(let u) = u { | |
return s.extend(u, v) | |
} else if case .var(let v) = v { | |
return s.extend(v, u) | |
} else if case .pair(let ua, let ud) = u, | |
case .pair(let va, let vd) = v { | |
guard let s = unify(ua, va, s) else { | |
return nil | |
} | |
return unify(ud, vd, s) | |
} else if u == v { | |
return s | |
} else { | |
return nil | |
} | |
} | |
typealias Goal = (State) -> Stream | |
infix operator =~: ComparisonPrecedence | |
func =~ (_ u: Term, _ v: Term) -> Goal { | |
return { state in | |
if let sub = unify(u, v, state.sub) { | |
return Stream.unit(State(sub: sub, nfresh: state.nfresh)) | |
} else { | |
return .empty | |
} | |
} | |
} | |
func callFresh(f: @escaping (Term) -> Goal) -> Goal { | |
return { state in | |
var state = state | |
let g = f(state.makeVar()) | |
return g(state) | |
} | |
} | |
func conj_(_ g1: @escaping Goal, _ g2: @escaping Goal) -> Goal { | |
return { state in | |
g1(state).appendMap(g2) | |
} | |
} | |
func disj_(_ g1: @escaping Goal, _ g2: @escaping Goal) -> Goal { | |
return { state in | |
g1(state).append(g2(state)) | |
} | |
} | |
// miniKanren | |
func zzz(_ g: @escaping @autoclosure () -> Goal) -> Goal { | |
return { state in | |
return .immature { | |
g()(state) | |
} | |
} | |
} | |
func && (_ g1: @escaping @autoclosure () -> Goal, _ g2: @escaping @autoclosure () -> Goal) -> Goal { | |
conj_(zzz(g1()), zzz(g2())) | |
} | |
func || (_ g1: @escaping @autoclosure () -> Goal, _ g2: @escaping @autoclosure () -> Goal) -> Goal { | |
disj_(zzz(g1()), zzz(g2())) | |
} | |
let succeed: Goal = { state in .unit(state) } | |
let fail: Goal = { state in .empty } | |
@_functionBuilder struct ConjBuilder { | |
static func buildBlock(_ goals: Goal...) -> Goal { | |
goals.reduce(succeed) { x, y in x && y } | |
} | |
} | |
@_functionBuilder struct DisjBuilder { | |
static func buildBlock(_ goals: Goal...) -> Goal { | |
goals.reduce(fail) { x, y in x || y } | |
} | |
} | |
func conj(@ConjBuilder f: () -> Goal) -> Goal { | |
f() | |
} | |
func disj(@DisjBuilder f: () -> Goal) -> Goal { | |
f() | |
} | |
func ifte(_ g1: @escaping Goal, _ g2: @escaping Goal, _ g3: @escaping Goal) -> Goal { | |
return { state in | |
var stream = g1(state) | |
while true { | |
switch stream { | |
case .empty: | |
return g3(state) | |
case .mature(_, _): | |
return stream.appendMap(g2) | |
case .immature(let f): | |
stream = f() | |
} | |
} | |
} | |
} | |
func once(_ g: @escaping Goal) -> Goal { | |
return { state in | |
var stream = g(state) | |
while true { | |
switch stream { | |
case .empty: | |
return .empty | |
case .mature(let state, _): | |
return .unit(state) | |
case .immature(let f): | |
stream = f() | |
} | |
} | |
} | |
} | |
@_functionBuilder struct CondaBuilder { | |
static func buildBlock(_ goals: [Goal]...) -> Goal { | |
makeGoal(goals) | |
} | |
static func makeGoal(_ goals: [[Goal]]) -> Goal { | |
var g = succeed | |
for line in goals.reversed() { | |
if line.count > 0 { | |
g = ifte( | |
line[0], | |
line.dropFirst().reduce(succeed) { a, b in a && b }, | |
g) | |
} | |
} | |
return g | |
} | |
} | |
func conda(@CondaBuilder f: () -> Goal) -> Goal { | |
f() | |
} | |
@_functionBuilder struct ConduBuilder { | |
static func buildBlock(_ goals: [Goal]...) -> Goal { | |
let goals: [[Goal]] = goals.map { line in | |
if line.count > 0 { | |
return [once(line[0])] + line.dropFirst() | |
} else { | |
return line | |
} | |
} | |
return CondaBuilder.makeGoal(goals) | |
} | |
} | |
func condu(@ConduBuilder f: () -> Goal) -> Goal { | |
f() | |
} | |
extension Stream { | |
func takeAll() -> [State] { | |
switch self { | |
case .empty: | |
return [] | |
case .mature(let state, let rest): | |
return [state] + rest.takeAll() | |
case .immature(let f): | |
return f().takeAll() | |
} | |
} | |
func take(_ n: Int) -> [State] { | |
if n == 0 { | |
return [] | |
} | |
switch self { | |
case .empty: | |
return [] | |
case .mature(let state, let rest): | |
return [state] + rest.take(n-1) | |
case .immature(let f): | |
return f().take(n) | |
} | |
} | |
} | |
func reifyName(_ n: Int) -> Term { | |
return .sym("_\(n)") | |
} | |
extension Substitution { | |
func walkAll(_ v: Term) -> Term { | |
let v = walk(v) | |
if case .var(_) = v { | |
return v | |
} else if case .pair(let value, let rest) = v { | |
return .pair(walkAll(value), walkAll(rest)) | |
} else { | |
return v | |
} | |
} | |
func reifyS(_ v: Term) -> Substitution { | |
let v = walk(v) | |
if case .var(let v) = v { | |
let n = count | |
let name = reifyName(n) | |
return extend(v, name) | |
} else if case .pair(let value, let rest) = v { | |
let r = reifyS(value) | |
return r.reifyS(rest) | |
} else { | |
return self | |
} | |
} | |
func reify(_ v: Term) -> Term { | |
let v = walkAll(v) | |
let names = Substitution().reifyS(v) | |
return names.walkAll(v) | |
} | |
} | |
func fresh(@ConjBuilder f: @escaping (Term) -> Goal) -> Goal { | |
callFresh { a in f(a) } | |
} | |
func run(n: Int? = nil, @ConjBuilder f: (Term) -> Goal) -> [Term] { | |
var state = State.empty | |
let a = state.makeVar() | |
if let n = n { | |
return f(a)(state).take(n).map { $0.sub.reify(a) } | |
} else { | |
return f(a)(state).takeAll().map { $0.sub.reify(a) } | |
} | |
} | |
// For convenience | |
func fresh(@ConjBuilder f: @escaping (Term, Term) -> Goal) -> Goal { | |
fresh { a in fresh { b in f(a, b) }} | |
} | |
func fresh(@ConjBuilder f: @escaping (Term, Term, Term) -> Goal) -> Goal { | |
fresh { a, b in fresh { c in f(a, b, c) }} | |
} | |
func fresh(@ConjBuilder f: @escaping (Term, Term, Term, Term) -> Goal) -> Goal { | |
fresh { a, b, c in fresh { d in f(a, b, c, d) }} | |
} | |
func fresh(@ConjBuilder f: @escaping (Term, Term, Term, Term, Term) -> Goal) -> Goal { | |
fresh { a, b, c, d in fresh { e in f(a, b, c, d, e) }} | |
} | |
func fresh(@ConjBuilder z: @escaping (Term, Term, Term, Term, Term, Term) -> Goal) -> Goal { | |
fresh { a, b, c, d, e in fresh { f in z(a, b, c, d, e, f) }} | |
} | |
func fresh(@ConjBuilder z: @escaping (Term, Term, Term, Term, Term, Term, Term) -> Goal) -> Goal { | |
fresh { a, b, c, d, e, f in fresh { g in z(a, b, c, d, e, f, g) }} | |
} | |
func fresh(@ConjBuilder z: @escaping (Term, Term, Term, Term, Term, Term, Term, Term) -> Goal) -> Goal { | |
fresh { a, b, c, d, e, f, g in fresh { h in z(a, b, c, d, e, f, g, h) }} | |
} | |
func fresh(@ConjBuilder z: @escaping (Term, Term, Term, Term, Term, Term, Term, Term, Term) -> Goal) -> Goal { | |
fresh { a, b, c, d, e, f, g, h in fresh { i in z(a, b, c, d, e, f, g, h, i) }} | |
} | |
func fresh(@ConjBuilder z: @escaping (Term, Term, Term, Term, Term, Term, Term, Term, Term, Term) -> Goal) -> Goal { | |
fresh { a, b, c, d, e, f, g, h, i in fresh { j in z(a, b, c, d, e, f, g, h, i, j) }} | |
} | |
func fresh(@ConjBuilder z: @escaping (Term, Term, Term, Term, Term, Term, Term, Term, Term, Term, Term) -> Goal) -> Goal { | |
fresh { a, b, c, d, e, f, g, h, i, j in fresh { k in z(a, b, c, d, e, f, g, h, i, j, k) }} | |
} | |
func run(n: Int? = nil, @ConjBuilder f: (Term, Term) -> Goal) -> [Term] { | |
var state = State.empty | |
let a = state.makeVar() | |
let b = state.makeVar() | |
if let n = n { | |
return f(a, b)(state).take(n).map { $0.sub.reify([a, b]) } | |
} else { | |
return f(a, b)(state).takeAll().map { $0.sub.reify([a, b]) } | |
} | |
} | |
func run(n: Int? = nil, @ConjBuilder f: (Term, Term, Term) -> Goal) -> [Term] { | |
var state = State.empty | |
let a = state.makeVar() | |
let b = state.makeVar() | |
let c = state.makeVar() | |
if let n = n { | |
return f(a, b, c)(state).take(n).map { $0.sub.reify([a, b, c]) } | |
} else { | |
return f(a, b, c)(state).takeAll().map { $0.sub.reify([a, b, c]) } | |
} | |
} | |
func run(n: Int? = nil, @ConjBuilder f: (Term, Term, Term, Term) -> Goal) -> [Term] { | |
var state = State.empty | |
let a = state.makeVar() | |
let b = state.makeVar() | |
let c = state.makeVar() | |
let d = state.makeVar() | |
if let n = n { | |
return f(a, b, c, d)(state).take(n).map { $0.sub.reify([a, b, c, d]) } | |
} else { | |
return f(a, b, c, d)(state).takeAll().map { $0.sub.reify([a, b, c, d]) } | |
} | |
} | |
func run(n: Int? = nil, @ConjBuilder f: (Term, Term, Term, Term, Term) -> Goal) -> [Term] { | |
var state = State.empty | |
let a = state.makeVar() | |
let b = state.makeVar() | |
let c = state.makeVar() | |
let d = state.makeVar() | |
let e = state.makeVar() | |
if let n = n { | |
return f(a, b, c, d, e)(state).take(n).map { $0.sub.reify([a, b, c, d, e]) } | |
} else { | |
return f(a, b, c, d, e)(state).takeAll().map { $0.sub.reify([a, b, c, d, e]) } | |
} | |
} | |
// Actual playground | |
func nullo(_ x: Term) -> Goal { | |
x =~ [] | |
} | |
func conso(_ a: Term, _ d: Term, _ p: Term) -> Goal { | |
p =~ .pair(a, d) | |
} | |
func caro(_ l: Term, _ a: Term) -> Goal { | |
fresh { d in | |
conso(a, d, l) | |
} | |
} | |
func cdro(_ l: Term, _ d: Term) -> Goal { | |
fresh { a in | |
conso(a, d, l) | |
} | |
} | |
func singletono(_ l: Term) -> Goal { | |
fresh { d in | |
cdro(l, d) | |
nullo(d) | |
} | |
} | |
func appendo(_ l: Term, _ t: Term, _ out: Term) -> Goal { | |
disj { | |
nullo(l) && t =~ out | |
fresh { a, d, res in | |
conso(a, d, l) | |
conso(a, res, out) | |
appendo(d, t, res) | |
} | |
} | |
} | |
let r = run(n: 5) { q, r, s in | |
appendo(q, r, s) | |
} | |
print(r) // => [(() _0 _0), ((_0) _1 (_0 . _1)), ((_0 _1) _2 (_0 _1 . _2)), ((_0 _1 _2) _3 (_0 _1 _2 . _3)), ((_0 _1 _2 _3) _4 (_0 _1 _2 _3 . _4))] |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment