all kanren testcases passes

parent 6e9a27ff
......@@ -354,206 +354,6 @@
(define !!- (s!- s!-))
; And we re-do all the tests
#|
(test-check 'test-!-1
(and
(equal?
(solution (?) (!- '(intc 17) int))
'((?.0 _.0)))
(equal?
(solution (?) (!- '(intc 17) ?))
'((?.0 int))))
#t)
(test-check 'arithmetic-primitives
(solution (?) (!- '(zero? (intc 24)) ?))
'((?.0 bool)))
(test-check 'test-!-sub1
(solution (?) (!- '(zero? (sub1 (intc 24))) ?))
'((?.0 bool)))
(test-check 'test-!-+
(solution (?)
(!- '(zero? (sub1 (+ (intc 18) (+ (intc 24) (intc 50))))) ?))
'((?.0 bool)))
(test-check 'test-!-2
(and
(equal?
(solution (?) (!- '(zero? (intc 24)) ?))
'((?.0 bool)))
(equal?
(solution (?) (!- '(zero? (+ (intc 24) (intc 50))) ?))
'((?.0 bool)))
(equal?
(solution (?)
(!- '(zero? (sub1 (+ (intc 18) (+ (intc 24) (intc 50))))) ?))
'((?.0 bool))))
#t)
(test-check 'test-!-3
(solution (?) (!- '(if (zero? (intc 24)) (intc 3) (intc 4)) ?))
'((?.0 int)))
(test-check 'if-expressions
(solution (?)
(!- '(if (zero? (intc 24)) (zero? (intc 3)) (zero? (intc 4))) ?))
'((?.0 bool)))
; Commented out: we need to extend !- if we wish to typecheck open terms
'(test-check 'variables
(and
(equal?
(solution (?)
(env '((b non-generic int) (a non-generic bool)) 'a ?))
'((?.0 bool)))
(equal?
(solution (?)
(!- '((a non-generic int)) '(zero? (var a)) ?))
'((?.0 bool)))
(equal?
(solution (?)
(!- '((b non-generic bool) (a non-generic int))
'(zero? (var a))
?))
'((?.0 bool))))
#t)
(test-check 'variables-4a
(solution (?)
(!- '(lambda (x) (+ (var x) (intc 5)))
?))
'((?.0 (--> int int))))
; Commented out: we need to extend !- if we wish to typecheck open terms
'(test-check 'variables-4b
(solution (?)
(!- '((b non-generic bool) (a non-generic int))
'(lambda (x) (+ (var x) (var a)))
?))
'((?.0 (--> int int))))
(test-check 'variables-4c
(solution (?)
(!- '(lambda (a) (lambda (x) (+ (var x) (var a)))) ?))
'((?.0 (--> int (--> int int)))))
(test-check 'everything-but-polymorphic-let
(solution (?)
(!- (parse
'(lambda (f)
(lambda (x)
((f x) x))))
?))
'((?.0 (-->
(--> _.0 (--> _.0 _.1))
(--> _.0 _.1)))))
(test-check 'everything-but-polymorphic-let
(solution (?)
(!- (parse
'((fix (lambda (sum)
(lambda (n)
(if (zero? n)
0
(+ n (sum (sub1 n)))))))
10))
?))
'((?.0 int)))
(test-check 'everything-but-polymorphic-let
(solution (?)
(!- (parse
'((fix (lambda (sum)
(lambda (n)
(+ n (sum (sub1 n))))))
10))
?))
'((?.0 int)))
(test-check 'everything-but-polymorphic-let
(solution (?)
(!- (parse '((lambda (f)
(if (f (zero? 5))
(+ (f 4) 8)
(+ (f 3) 7)))
(lambda (x) x)))
?))
#f)
(test-check 'polymorphic-let
(solution (?)
(!- (parse
'(let ((f (lambda (x) x)))
(if (f (zero? 5))
(+ (f 4) 8)
(+ (f 3) 7))))
?))
'((?.0 int)))
(test-check 'with-robust-syntax
(solution (?)
(!- '(app
(fix
(lambda (sum)
(lambda (n)
(if (if (zero? (var n)) (boolc #t) (boolc #f))
(intc 0)
(+ (var n) (app (var sum) (sub1 (var n))))))))
(intc 10))
?))
'((?.0 int)))
(test-check 'with-robust-syntax-but-long-jumps/poly-let
(solution (?)
(!- '(let ((f (lambda (x) (var x))))
(if (app (var f) (zero? (intc 5)))
(+ (app (var f) (intc 4)) (intc 8))
(+ (app (var f) (intc 3)) (intc 7))))
?))
'((?.0 int)))
; The latter doesn't work: but it wasn't too informative anyway
'(test-check 'type-habitation-1
(solution (?)
(!- ? '(--> int int)))
'((g.0 ((v.0 non-generic (--> int int)) . lt.0)) (?.0 (var v.0))))
(test-check 'type-habitation-2
(solution (h r q z y t)
(!- `(,h ,r (,q ,z ,y)) t))
'((h.0 +)
(r.0 (intc _.0))
(q.0 +)
(z.0 (intc _.1))
(y.0 (intc _.2))
(t.0 int))
)
(test-check 'type-habitation-3
(and
(equal?
(solution (la f b)
(!- `(,la (,f) ,b) '(--> int int)))
'((la.0 lambda) (f.0 _.0) (b.0 (var _.0))))
(equal?
(solution (h r q z y t u v)
(!- `(,h ,r (,q ,z ,y)) `(,t ,u ,v)))
'((h.0 lambda)
(r.0 (_.0))
(q.0 +)
(z.0 (var _.0))
(y.0 (var _.0))
(t.0 -->)
(u.0 int)
(v.0 int))))
#t)
|#
; The code below uses the low-level function var? Every use of var?
; entails a proof obligation that such use is safe. In our case here,
; invertible-binary-function->ternary-relation and
......
(define-module (logic guile-log kanren)
(define-module (logic guile-log kanren)
#:use-module (logic guile-log umatch)
#:use-module (logic guile-log)
#:export(succeed fail sfail exists all all! all!! if-only
......@@ -50,7 +50,7 @@
(define var? gp-logical-var?)
(define reify (lambda (x)
(tr 'v. x '())))
(tr 'v. x *current-stack*)))
(define-syntax let-lv
(syntax-rules ()
......
......@@ -231,3 +231,27 @@
int
int)))
#t)
(test-check 'test-instantiated-1
(and
(equal?
(solution (x) (++ x 16.0 8))
'-8.0)
(equal?
(solution (x) (++ 10 16.0 x))
'26.0)
(equal?
(solution (x) (-- 10 x 3))
'13))
#t)
(test-check 'test-instantiated-2
(and
(equal?
(solution (x) (name 'sleep x))
'(115 108 101 101 112))
(equal?
(solution (x) (name x '(115 108 101 101 112)))
'sleep))
#t)
......@@ -1426,6 +1426,7 @@
(+o m k n))
(<define> (*o n m p)
(<pp> `(,n ,m ,p))
(<condi>
((<=> '() n) (<=> '() p))
((poso n) (<=> '() m) (<=> '() p))
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment