-
Notifications
You must be signed in to change notification settings - Fork 33
/
tree-unify.scm
67 lines (57 loc) · 1.59 KB
/
tree-unify.scm
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
(library
(cKanren tree-unify)
(export == unify)
(import (rnrs) (cKanren ck))
;; ---UNIFICATION--------------------------------------------------
(define ext-s
(lambda (x v s)
(cons `(,x . ,v) s)))
(define occurs-check
(lambda (x v s)
(let ((v (walk v s)))
(cond
((var? v) (eq? v x))
((pair? v)
(or (occurs-check x (car v) s)
(occurs-check x (cdr v) s)))
(else #f)))))
(define unify
(lambda (e s)
(cond
((null? e) s)
(else
(let loop ((u (caar e)) (v (cdar e)) (e (cdr e)))
(let ((u (walk u s)) (v (walk v s)))
(cond
((eq? u v) (unify e s))
((var? u)
(and (not (occurs-check u v s))
(unify e (ext-s u v s))))
((var? v)
(and (not (occurs-check v u s))
(unify e (ext-s v u s))))
((and (pair? u) (pair? v))
(loop (car u) (car v)
`((,(cdr u) . ,(cdr v)) . ,e)))
((equal? u v) (unify e s))
(else #f))))))))
;; ---GOAL---------------------------------------------------------
(define == (lambda (u v) (goal-construct (==-c u v))))
(define ==-c
(lambda (u v)
(lambdam@ (a : s c)
(cond
((unify `((,u . ,v)) s)
=> (lambda (s^)
((update-prefix s s^) a)))
(else #f)))))
(define update-prefix
(lambda (s s^)
(let loop ((s^ s^))
(cond
((eq? s s^) identitym)
(else
(composem
(update-s (caar s^) (cdar s^))
(loop (cdr s^))))))))
)