Module: MicroKanren::Core

Includes:
Lisp
Defined in:
lib/micro_kanren/core.rb

Instance Method Summary collapse

Methods included from Lisp

#assp, #car, #cdr, #cons, #cons?, #length, #lists_equal?, #lprint, #map, #procedure?

Instance Method Details

#bind(d, g) ⇒ Object 



87
88
89
90
91
92
93
94
95
 
# File 'lib/micro_kanren/core.rb', line 87

def bind(d, g)
  if d.nil?
    mzero
  elsif procedure?(d)
    -> { bind(d.call, g) }
  else
    mplus(g.call(car(d)), bind(cdr(d), g))
  end
end

#call_fresh(f) ⇒ Object

Call function f with a fresh variable.



62
63
64
65
66
67
 
# File 'lib/micro_kanren/core.rb', line 62

def call_fresh(f)
  -> (s_c) {
    c = cdr(s_c)
    f.call(var(c)).call(cons(car(s_c), c + 1))
  }
end

#conj(g1, g2) ⇒ Object 



73
74
75
 
# File 'lib/micro_kanren/core.rb', line 73

def conj(g1, g2)
  -> (s_c) { bind(g1.call(s_c), g2) }
end

#disj(g1, g2) ⇒ Object 



69
70
71
 
# File 'lib/micro_kanren/core.rb', line 69

def disj(g1, g2)
  -> (s_c) { mplus(g1.call(s_c), g2.call(s_c)) }
end

#eq(u, v) ⇒ Object

Constrain u to be equal to v.

in Scheme implementation, ≡ in uKanren papers.



28
29
30
31
32
33
 
# File 'lib/micro_kanren/core.rb', line 28

def eq(u, v)
  ->(s_c) {
    s = unify(u, v, car(s_c))
    s ? unit(cons(s, cdr(s_c))) : mzero
  }
end

#ext_s(x, v, s) ⇒ Object 



22
23
24
 
# File 'lib/micro_kanren/core.rb', line 22

def ext_s(x, v, s)
  cons(cons(x, v), s)
end

#mplus(d1, d2) ⇒ Object 



77
78
79
80
81
82
83
84
85
 
# File 'lib/micro_kanren/core.rb', line 77

def mplus(d1, d2)
  if d1.nil?
    d2
  elsif procedure?(d1)
    -> { mplus(d2, d1.call) }
  else
    cons(car(d1), mplus(cdr(d1), d2))
  end
end

#mzero ⇒ Object 



36
 
# File 'lib/micro_kanren/core.rb', line 36

def mzero ; nil ; end

#unify(u, v, s) ⇒ Object 



38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
 
# File 'lib/micro_kanren/core.rb', line 38

def unify(u, v, s)
  u = walk(u, s)
  v = walk(v, s)

  if var?(u) && var?(v) && vars_eq?(u, v)
    s

  elsif var?(u)
    ext_s(u, v, s)

  elsif var?(v)
    ext_s(v, u, s)

  elsif pair?(u) && pair?(v)
    s = unify(car(u), car(v), s)
    s && unify(cdr(u), cdr(v), s)

  else
    # Object identity (equal?) seems closest to eqv? in Scheme.
    u.equal?(v) && s
  end
end

#unit(s_c) ⇒ Object 



35
 
# File 'lib/micro_kanren/core.rb', line 35

def unit(s_c) ; cons(s_c, mzero) ; end

#var(*c) ⇒ Object 



5
 
# File 'lib/micro_kanren/core.rb', line 5

def var(*c)       ; Var.new(c)   ; end

#var?(x) ⇒ Boolean

Returns:

  • (Boolean) 


6
 
# File 'lib/micro_kanren/core.rb', line 6

def var?(x)       ; x.is_a?(Var) ; end

#vars_eq?(x1, x2) ⇒ Boolean

var=? in Scheme implementation.

Returns:

  • (Boolean) 


9
 
# File 'lib/micro_kanren/core.rb', line 9

def vars_eq?(x1, x2) ; x1[0] == x2[0]  ; end

#walk(u, s) ⇒ Object

Walk environment S and look up value of U, if present.



12
13
14
15
16
17
18
19
20
 
# File 'lib/micro_kanren/core.rb', line 12

def walk(u, s)
  if var?(u)
    pr = assp(-> (v) { u == v }, s)
    pr ? walk(cdr(pr), s) : u

  else
    u
  end
end