|
|
@ -0,0 +1,29 @@
|
|
|
1
|
(load "/home/lu/t/miniKanren/mk.scm")
|
|
|
2
|
|
|
|
3
|
; a simple lambda calculus in miniKanren
|
|
|
4
|
|
|
|
5
|
; x - variables
|
|
|
6
|
; (lambda (x) x) - abstraction
|
|
|
7
|
; (e1 e2) - application
|
|
|
8
|
|
|
|
9
|
(define lookupo
|
|
|
10
|
(lambda (x env val)
|
|
|
11
|
(fresh (y v rest)
|
|
|
12
|
(== `((,y . ,v) . ,rest) env)
|
|
|
13
|
(conde
|
|
|
14
|
[(== x y) (== v val)]
|
|
|
15
|
[(=/= x y) (lookupo x rest val)]))))
|
|
|
16
|
|
|
|
17
|
(define evalo
|
|
|
18
|
(lambda (expr env val)
|
|
|
19
|
(conde
|
|
|
20
|
[(symbolo expr)
|
|
|
21
|
(lookupo expr env val)]
|
|
|
22
|
[(fresh (x body)
|
|
|
23
|
(== `(lambda (,x) ,body) expr)
|
|
|
24
|
(== `(closure ,x ,body ,env) val))]
|
|
|
25
|
[(fresh (e1 e2 x body env^ arg)
|
|
|
26
|
(== `(,e1 ,e2) expr)
|
|
|
27
|
(evalo e1 env `(closure ,x ,body ,env^))
|
|
|
28
|
(evalo e2 env arg)
|
|
|
29
|
(evalo body `((,x . ,arg) . ,env^) val))])))
|