|
| 1 | +/* eslint-disable */ |
| 2 | + |
| 3 | +// Relational programming rather than functional. |
| 4 | +// μ as in micro-kernel. Small is simpler. |
| 5 | + |
| 6 | +var fresh_counter = 0 |
| 7 | + |
| 8 | +// Wrapper for variables |
| 9 | +function Var(name) {this.name = name} |
| 10 | +var is_var = x => x instanceof Var |
| 11 | +var eq_var = (a, b) => a.name === b.name |
| 12 | + |
| 13 | +// Walk searches for a variable's value in the substitution. |
| 14 | +var walk = (u, subst) => |
| 15 | + is_var(u) && u.name in subst ? walk(subst[u.name], subst) |
| 16 | + : u |
| 17 | + |
| 18 | +// ext_s extends the substitution with a new (var, val) couple. |
| 19 | +var ext_s = (lvar, val, subst) => ({ |
| 20 | + __proto__: subst, |
| 21 | + [lvar.name]: val |
| 22 | +}) |
| 23 | + |
| 24 | +// Pretty printer for substitutions and variables |
| 25 | +var pp = subst => { |
| 26 | + var o = Object.create(null) |
| 27 | + for (var k in subst) |
| 28 | + o[k] = is_var(subst[k]) ? `#${subst[k].name}` : subst[k] |
| 29 | + return o |
| 30 | +} |
| 31 | + |
| 32 | +var a = new Var('a') |
| 33 | +var b = new Var('b') |
| 34 | +var c = new Var('c') |
| 35 | + |
| 36 | +walk(a, ext_s(a, b, ext_s(b, 1))) //: 1 |
| 37 | +walk(a, ext_s(b, 1, ext_s(a, b))) //: 1 |
| 38 | + |
| 39 | +// The core of the kernel : unify |
| 40 | +var unify = (u, v, subst) => { |
| 41 | + u = walk(u, subst) |
| 42 | + v = walk(v, subst) |
| 43 | + if (is_var(u) && is_var(v) && eq_var(u, v)) return subst |
| 44 | + else if (is_var(u)) return ext_s(u, v, subst) |
| 45 | + else if (is_var(v)) return ext_s(v, u, subst) |
| 46 | + else if (Array.isArray(u) && Array.isArray(v)) { |
| 47 | + if (u.length === 0 && v.length === 0) return subst // avoid infinite recursion |
| 48 | + var [[u1, ...us], [v1, ...vs]] = [u, v] |
| 49 | + var s = unify(u1, v1, subst) |
| 50 | + return s && unify(us, vs, s) |
| 51 | + } |
| 52 | + else if (u === v) return subst |
| 53 | + else return false |
| 54 | +} |
| 55 | + |
| 56 | +pp(unify(a, b, {})) //: Object {a:"#b"} |
| 57 | +pp(unify(a, 1, unify(a, b, {}))) //: Object {b:1,a:"#b"} |
| 58 | +pp(unify([a,b], [1,2], {})) //: Object {b:2,a:1} |
| 59 | + |
| 60 | +// Finite depth-first search |
| 61 | +// var mplus = (s1, s2) => s1.concat(s2) |
| 62 | +// var bind = (s, g) => s.length === 0 ? mzero() |
| 63 | +// : mplus(g(s[0]), bind(s.slice(1), g)) |
| 64 | + |
| 65 | +// Infinite streams |
| 66 | +var mplus = (s1, s2) => |
| 67 | + typeof s1 === 'function' ? _ => mplus(s2, s1()) |
| 68 | + : s1.concat(s2) |
| 69 | + |
| 70 | +var bind = (s, g) => { |
| 71 | + if (s.length === 0) return mzero() |
| 72 | + else if (typeof s === 'function') return _ => bind(s(), g) |
| 73 | + else return mplus(g(s[0]), bind(s.slice(1), g)) |
| 74 | +} |
| 75 | + |
| 76 | +// Goal constructors |
| 77 | +var unit = x => [x] |
| 78 | +var mzero = _ => [] |
| 79 | + |
| 80 | +var eq = (u, v) => subst => { |
| 81 | + var s = unify(u, v, subst) |
| 82 | + return s ? unit(s) : mzero() |
| 83 | +} |
| 84 | + |
| 85 | +var call_fresh = f => f(new Var(fresh_counter++)) |
| 86 | + |
| 87 | +var disj = (g1, g2) => subst => |
| 88 | + mplus(g1(subst), g2(subst)) |
| 89 | + |
| 90 | +var conj = (g1, g2) => subst => |
| 91 | + bind(g1(subst), g2) |
| 92 | + |
| 93 | +var force = f => typeof f === 'function' ? force(f()) : f |
| 94 | + |
| 95 | +var run = g => g(Object.create(null)).map(s => pp(force(s))) |
| 96 | + |
| 97 | +run(eq(1, 1)) //: [Object {}] |
| 98 | +run(eq(1, 2)) //: [] |
| 99 | +run(eq(a, 3)) //: [Object {a:3}] |
| 100 | +run(eq([a, 2], [1,2])) //: [Object {a:1}] |
| 101 | + |
| 102 | +var choice = (lvar, [h, ...t]) => |
| 103 | + h == null ? mzero |
| 104 | + : disj(eq(lvar, h), |
| 105 | + choice(lvar, t)) |
| 106 | + |
| 107 | +run(choice(a, [1,2,3])) //: [Object {a:1},Object {a:2},Object {a:3}] |
| 108 | + |
| 109 | +var common_el = (l1, l2) => |
| 110 | + call_fresh(a => conj(choice(a, l1), choice(a, l2))) |
| 111 | + |
| 112 | +run(common_el([1,2,3], [2,3,4,5])) //: [Object {0:2},Object {0:3}] |
| 113 | + |
| 114 | +var conso = (a, b, list) => eq([a, b], list) |
| 115 | + |
| 116 | +run(conso(1, [2,3], a)) //: [Object {a:[1,[2,3]]}] |
| 117 | +run(conso(a, [2,3], [1,[2,3]])) //: [Object {a:1}] |
| 118 | +run(conso(a, b, [1,[2,3]])) //: [Object {b:[2,3],a:1}] |
| 119 | +run(conso(a, b, [1,c])) //: [Object {b:"#c",a:1}] |
| 120 | + |
| 121 | + |
| 122 | + |
| 123 | + |
| 124 | +var fives = x => disj(eq(x, 5), |
| 125 | + (subst) => _ => fives(x)(subst)) |
| 126 | + |
| 127 | +run(fives(a)) //: [Object {a:5},Object {0:Object {a:5},1:function}] |
| 128 | + |
| 129 | +var minus = (n, m, n_m) => eq(n_m, n-m) |
| 130 | + |
| 131 | +run(minus(10, 5, 5)) //: [Object {}] |
| 132 | +run(minus(10, 5, a)) //: [Object {a:5}] |
| 133 | + |
| 134 | +var fact = (n, f) => call_fresh(f1 => call_fresh(n1 => |
| 135 | + disj(conj(eq(n, 0), eq(f, 1)), |
| 136 | + conj(subst => _ => fact(n1, f1)(subst), conj(eq(f, n * f1), minus(n, 1, n1)))))) |
| 137 | + |
| 138 | +run(fact(0, a)) //: [Object {a:1},Object {0:Object {2:-1}}] |
| 139 | +run(fact(1, a)) //: [Object {0:Object {a:NaN},1:Object {6:0}}] |
0 commit comments