typechek example for kanren added together with bugfixes

parent f1c0a913
This diff is collapsed.
......@@ -7,7 +7,7 @@
let-gls == query solve solution project project/no-check
predicate *equal? var? _ let-lv reify partially-eval-sgl
extend-relation extend-relation-with-recur-limit
intersect-relation exists any-union))
intersect-relation exists any-union trace-vars))
(define-syntax mk
......@@ -494,3 +494,19 @@
((_ (ex-id ...) gl)
(let-lv (ex-id ...) gl))
))
(define-syntax promise-one-answer
(syntax-rules ()
((_ gl) gl)))
(define-syntax trace-vars
(syntax-rules ()
((_ title (var0 ...))
(promise-one-answer
(project/no-check (var0 ...)
(predicate
(for-each
(lambda (name val)
(format "~a ~a: ~a~%" title name val))
'(var0 ...) (reify `(,var0 ...)))
))))))
(use-modules (logic guile-log kanren))
(use-modules (logic guile-log examples kanren type-inference))
(define (time x) x)
(define-syntax test-check
(syntax-rules ()
((_ title tested-expression expected-result)
(begin
(format #t "Testing ~a~%" title)
(let* ((expected expected-result)
(produced tested-expression))
(or (equal? expected produced)
(error
(format #f
"(Failed: ~a~%Expected: ~a~%Computed: ~a~%"
'tested-expression expected produced))))))))
(test-check 'test-!-1
(and
(equal?
(solution (?) (!- '() '(intc 17) int))
'v.0)
(equal?
(solution (?) (!- '() '(intc 17) ?))
'int))
#t)
(test-check 'arithmetic-primitives
(solution (?) (!- '() '(zero? (intc 24)) ?))
'bool)
(test-check 'test-!-sub1
(solution (?) (!- '() '(zero? (sub1 (intc 24))) ?))
'bool)
(test-check 'test-!-+
(solution (?)
(!- '() '(zero? (sub1 (+ (intc 18) (+ (intc 24) (intc 50))))) ?))
'bool)
(test-check 'test-!-2
(and
(equal?
(solution (?) (!- '() '(zero? (intc 24)) ?))
'bool)
(equal?
(solution (?) (!- '() '(zero? (+ (intc 24) (intc 50))) ?))
'bool)
(equal?
(solution (?)
(!- '() '(zero? (sub1 (+ (intc 18) (+ (intc 24) (intc 50))))) ?))
'bool))
#t)
(test-check 'test-!-3
(solution (?) (!- '() '(if (zero? (intc 24)) (intc 3) (intc 4)) ?))
'int)
(test-check 'if-expressions
(solution (?)
(!- '() '(if (zero? (intc 24)) (zero? (intc 3)) (zero? (intc 4))) ?))
'bool)
(test-check 'variables
(and
(equal?
(solution (?)
(env '((b non-generic int) (a non-generic bool)) 'a ?))
'bool)
(equal?
(solution (?)
(!- '((a non-generic int)) '(zero? (var a)) ?))
'bool)
(equal?
(solution (?)
(!- '((b non-generic bool) (a non-generic int))
'(zero? (var a))
?))
'bool))
#t)
(test-check 'variables-4a
(solution (?)
(!- '((b non-generic bool) (a non-generic int))
'(lambda (x) (+ (var x) (intc 5)))
?))
'(--> int int))
(test-check 'variables-4b
(solution (?)
(!- '((b non-generic bool) (a non-generic int))
'(lambda (x) (+ (var x) (var a)))
?))
'(--> int int))
(test-check 'variables-4c
(solution (?)
(!- '() '(lambda (a) (lambda (x) (+ (var x) (var a)))) ?))
'(--> int (--> int int)))
(test-check 'everything-but-polymorphic-let
(solution (?)
(!- '() (parse
'(lambda (f)
(lambda (x)
((f x) x))))
?))
'(-->
(--> v.0 (--> v.0 v.1))
(--> v.0 v.1)))
(test-check 'everything-but-polymorphic-let
(solution (?)
(!- '()
(parse
'((fix (lambda (sum)
(lambda (n)
(if (zero? n)
0
(+ n (sum (sub1 n)))))))
10))
?))
'int)
(test-check 'everything-but-polymorphic-let
(solution (?)
(!- '()
(parse
'((fix (lambda (sum)
(lambda (n)
(+ n (sum (sub1 n))))))
10))
?))
'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))))
?))
'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))
?))
'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))))
?))
'int)
(test-check 'type-habitation-1
(solution (g ?)
(!- g ? '(--> int int)))
'(((v.0 non-generic (--> int int)) . v.1)
(var v.0)))
(test-check 'type-habitation-2
(solution (g h r q z y t)
(!- g `(,h ,r (,q ,z ,y)) t))
'(((v.0 non-generic int) . v.1)
+
(var v.0)
+
(var v.0)
(var v.0)
int))
(test-check 'type-habitation-3
(and
(equal?
(solution (la f b)
(!- '() `(,la (,f) ,b) '(--> int int)))
'(lambda v.0 (var v.0)))
(equal?
(solution (h r q z y t u v)
(!- '() `(,h ,r (,q ,z ,y)) `(,t ,u ,v)))
'(lambda
(v.0)
+
(var v.0)
(var v.0)
-->
int
int)))
#t)
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