kanren example works, remains to fix matchers

parent e0211eeb
......@@ -31,7 +31,7 @@
((_ w a ...)
(parse<> w (and-interleave (list (</.> a) ...))))))
(define (interleave p cc as)
(define (interleave sin p cc as)
(with-guarded-states guard-set! ((l '()) (r '()))
(let ((s (gp-store-state)))
(define fail
......@@ -55,15 +55,16 @@
(map (lambda (a)
(lambda ()
(gp-restore-wind s)
(a fail
(lambda (p2)
(a sin
fail
(lambda (ss p2)
(guard-set! l (cons (mk-cont p2) r))
(cc fail)))))
(cc ss fail)))))
as)
'())
(fail))))
(define (interleave-union p cc as)
(define (interleave-union sin p cc as)
(with-guarded-states guard-set! ((l '()) (r '()) (gs '()) (gr '()))
(let ((s (gp-store-state)))
(define fail
......@@ -87,16 +88,18 @@
(map (lambda (a)
(lambda ()
(gp-restore-wind s)
(a fail
(lambda (p2)
(a sin
fail
(lambda (ss p2)
(let check ((ggs gs))
(if (pair? ggs)
(let ((fr (gp-newframe)))
(let ((fr (gp-newframe ss)))
((car ggs)
ss
(lambda ()
(gp-unwind fr)
(check (cdr ggs)))
(lambda (p)
(lambda (sss p)
(gp-unwind fr)
(guard-set! l (cons (mk-cont p2) r)
gs (cons a gr))
......@@ -104,7 +107,7 @@
(begin
(guard-set! l (cons (mk-cont p2) r)
gs (cons a gr))
(cc fail))))))))
(cc ss fail))))))))
as)
'()
as
......@@ -125,16 +128,16 @@ and-interleave
|#
(define (and-interleave p cc gs)
(define (and-interleave sin p cc gs)
(match gs
(()
(cc p))
(cc sin p))
((g)
(g p cc))
(g sin p cc))
((g . gl)
(alli p cc g gl))))
(alli sin p cc g gl))))
(define (alli p cc g1 gs)
(define (alli sin p cc g1 gs)
(with-guarded-states guard-set! ((l '()) (r '()))
(define fail
(lambda ()
......@@ -153,21 +156,21 @@ and-interleave
(gp-restore-wind state)
(p))))
(let loop ((p p) (g1 g1) (gs gs))
(let loop ((sin sin) (p p) (g1 g1) (gs gs))
(match gs
((g2)
(g1 fail
(lambda (p2)
(g1 sin fail
(lambda (ss p2)
(guard-set! l (cons (mk-cont p2) r))
(g2 fail
(lambda (p3)
(g2 ss fail
(lambda (sss p3)
(guard-set! l (cons (mk-cont p3) r))
(cc fail))))))
(cc sss fail))))))
((g2 . gs)
(g1 fail
(lambda (p2)
(g1 sin fail
(lambda (ss p2)
(guard-set! l (cons (mk-cont p2) r))
(loop p2 g2 gs))))))))
(loop ss p2 g2 gs))))))))
......
......@@ -10,15 +10,22 @@
intersect-relation exists any-union trace-vars))
(define (mk-names x)
(syntax-case x ()
((x . l) #`(#,(datum->syntax #'x (gensym "a"))
#,@(mk-names #'l)))
(() #'())))
(define-syntax mk
(syntax-rules ()
((_ name gl-name)
(define-syntax name
(syntax-rules ()
((_ a (... ...))
(lambda (p cc)
(<with-guile-log> (p cc)
(gl-name (a) (... ...))))))))))
(lambda (x)
(syntax-case x ()
((_ a (... ...))
#'(lambda (s p cc)
(<with-guile-log> (s p cc)
(gl-name (a) (... ...)))))))))))
(define partially-eval-sgl
(lambda x
......@@ -37,8 +44,8 @@
(mk succeeds <succeds>)
(define succeed (lambda (p cc) (cc p))) ; eta-reduced
(define fail (lambda (p cc) (p)))
(define succeed (lambda (s p cc) (cc s p))) ; eta-reduced
(define fail (lambda (s p cc) (p)))
(define sfail fail)
(define var? gp-var?)
......@@ -99,14 +106,15 @@
; (let ((x 1))
; (id-memv?? x (x a b) 'OK #f))
(define-syntax do-preds
(define-syntax let*-and
(syntax-rules ()
((_ fail () code)
code)
((_ fail (x y ...) code )
(if x
(do-preds fail (y ...) code)
fail))))
((_ false-exp () body0 body1 ...) (begin body0 body1 ...))
((_ false-exp ((var0 exp0) (var1 exp1) ...) body0 body1 ...)
(let ((var0 exp0))
(if var0
(let*-and false-exp ((var1 exp1) ...) body0 body1 ...)
false-exp)))))
; Relations...........................
......@@ -247,8 +255,8 @@
(relation "g" vars once-vars (gs ... g) gunis
(term . bvars)
(subst
(subst**** (gp-unify! term g))
. cls)
(subst (gp-unify! term g subst))
. cls)
terms . gl))
; term is not a bare var
(relation "g" vars once-vars (gs ... g) ((g . term) . gunis)
......@@ -266,12 +274,13 @@
(exists (ex-id ...) gl)))
; the most general
((_ "f" (ex-id ...) once-vars (g ...) ((gv . term) ...)
(subst let*-clause ...) gl)
(s let*-clause ...) gl)
(lambda (g ...)
(exists (ex-id ...)
(let* (let*-clause ...)
(do-preds sfail ((gp-unify! gv term) ...)
gl)))))))
(lambda (s p cc)
(let* (let*-clause ...)
(let*-and (p) ((s (gp-unify! gv term s)) ...)
(gl s p cc)))))))))
; relation-head-let (head-term ...) gl
; A simpler, and more efficient kind of relation. The simplicity comes
......@@ -339,17 +348,19 @@
; final generation
((_ "f" vars ((gv term) ...) gvs) ; no body
(lambda gvs ; don't bother bind vars
(do-preds sfail ((gp-unify! gv term) ...)
succeed)))
(lambda gvs
(lambda (s p cc)
(let*-and (p) ((s (gp-unify! gv term s)) ...)
(succeed s p cc)))))
((_ "f" (var0 ...) ((gvo term) ...) gvs gl)
(lambda gvs
(do-preds sfail ((gp-unify! gvo term) ...)
(let ((var0 (if (eq? var0 _)
(gp-var!)
var0)) ...)
gl))))))
(lambda (s p cc)
(let*-and (p) ((s (gp-unify! gvo term s)) ...)
(let ((var0 (if (eq? var0 _)
(gp-var!)
var0)) ...)
(gl s p cc))))))))
(define-syntax fact
(syntax-rules ()
......@@ -397,12 +408,16 @@
; Unify lifted to be a binary relation
(define-syntax ==
(syntax-rules (_)
((_ t u)
(lambda (p cc)
(if (gp-unify! t u)
(cc p)
(p))))))
(lambda (x)
(syntax-case x ()
((x t u)
(or (eq? '_ (syntax->datum #'t))
(eq? '_ (syntax->datum #'u)))
#'(lambda (s p cc) (cc s p)))
((x t u)
#'(lambda (s p cc)
(<with-guile-log> (s p cc)
(<unify> gp-unify! t u)))))))
; query (redo-k subst id ...) A SE ... -> result or '()
; The macro 'query' runs the goal A in the empty
......@@ -445,7 +460,12 @@
((_ scheme-expression)
(if scheme-expression succeed fail))))
(define (*equal? x y) (gp-m-unify! x y))
(define-syntax *equal?
(syntax-rules (_)
((_ t u)
(lambda (s p cc)
(<with-guile-log> (s p cc)
(<unify> gp-m-unify! t u))))))
(define nonvar!
(lambda (t)
......
This diff is collapsed.
......@@ -57,9 +57,33 @@
(gp-module-init)
(define gpn gp-newframe)
(define (gp-newframe x)
(if x
(cons (gpn) (cdr x))
(cons (gpn) '())))
(define gpun gp-unwind)
(define (gp-unwind x)
(set! *wind* #t)
(set! *setup* #f)
(gpun (car x))
(do-setup))
(define gpun! gp-unify!)
(define (gp-unify! x y s)
(if (gpun! x y) s #f))
(define gpunr! gp-unify-raw!)
(define (gp-unify-raw! x y s) (if (gpunr! x y) s #f))
(define gpmun! gp-m-unify!)
(define (gp-m-unify! x y s) (if (gpmun! x y) s #f))
(define-syntax **um** (syntax-rules () ((_ . l) (umatch . l))))
(define dyn gp-dynwind)
(define uw gp-unwind)
(define *wind* #f)
(define *setup* #f)
(define (do-setup)
......@@ -74,12 +98,6 @@
(lambda x
(set! *setup* #f)))))
(define (gp-unwind x)
(set! *wind* #t)
(set! *setup* #f)
(uw x)
(do-setup))
(define (push-setup x)
(if *setup*
(set-car! *setup* (cons x (car *setup*)))
......@@ -335,22 +353,6 @@
;(pk `(umatch*** ,@(syntax->datum #'l)))
#'(umatch***+ . l)))))
#;
(define (mk-failure0 fr code)
(letrec ((base (case-lambda
(()
(gp-unwind fr)
(code))
((x)
(gp-unwind fr)
(let ((s (gp-store-state)))
(letrec ((self (case-lambda
(() (base))
((x) self))))
self))))))
base))
(define (mk-failure0 fr code)
(lambda ()
(gp-unwind fr)
......@@ -403,3 +405,4 @@
(define (gp-restore-state x)
(set! *wind* #f)
(gp-restore-state-raw x))
......@@ -51,7 +51,7 @@
(test-check 'test-conscientious-parents
(solve 7 (x y) (conscientious-parents x y))
(solve 7 (x y) (conscientious-parents x y))
'((sam rob)
(roz sue)
(rob sal)
......@@ -70,11 +70,11 @@
(let
((grandpa-sam
(relation (grandchild)
(to-show grandchild)
(exists (parent)
(all (father 'sam parent)
(father parent grandchild))))))
(relation (grandchild)
(to-show grandchild)
(exists (parent)
(all (father 'sam parent)
(father parent grandchild))))))
(test-check 'test-grandpa-sam-1
(solve 6 (y) (grandpa-sam y))
'(sal pat)))
......@@ -128,6 +128,7 @@
'(sal pat))))
(let*
((father
(extend-relation (a1 a2)
......@@ -184,7 +185,7 @@
(test-check 'test-grandpa-55
(solve 6 (y) (grandpa-sam y))
'(sal pat)))
; Now we don't need it
(let*
((grandpa/father
......@@ -238,6 +239,7 @@
; Properly, this requires soft cuts, aka *->, or Mercury's
; if-then-else. But we emulate it...
(let
((grandpa
(let-gls (a1 a2) ((grandpa/father grandpa/father)
......@@ -252,9 +254,9 @@
(sam pat)))
(test-check 'test-grandpa-10-1
(solve 10 (x) (grandpa x 'sue))
'(sam))
)
'(sam)))
; The same as above, with if-all! -- just to test the latter.
(let
((grandpa
......@@ -277,11 +279,12 @@
; Now do it with soft-cuts
(let
((grandpa
(let-gls (a1 a2) ((grandpa/father grandpa/father)
(grandpa/mother grandpa/mother))
(if-some grandpa/father succeed grandpa/mother))))
(if-some grandpa/father succeed grandpa/mother))))
(test-check 'test-grandpa-10-soft-cut
(solve 10 (x y) (grandpa x y))
......@@ -289,9 +292,10 @@
(jon roz)
(sam sal)
(sam pat))))
(let*
((a-grandma
((a-grandma
(relation (grandad grandchild)
(to-show grandad grandchild)
(exists (parent)
......@@ -336,28 +340,27 @@
(test-check 'test-Seres-Spivey
(let ((father
(lambda (dad child)
(any
(all (== dad 'jon) (== child 'sam))
(all (== dad 'sam) (== child 'rob))
(all (== dad 'sam) (== child 'roz))
(all (== dad 'rob) (== child 'sal))
(all (== dad 'rob) (== child 'pat))
(all (== dad 'jon) (== child 'hal))
(all (== dad 'hal) (== child 'ted))
(all (== dad 'sam) (== child 'jay))))))
(lambda (dad child)
(any
(all (== dad 'jon) (== child 'sam))
(all (== dad 'sam) (== child 'rob))
(all (== dad 'sam) (== child 'roz))
(all (== dad 'rob) (== child 'sal))
(all (== dad 'rob) (== child 'pat))
(all (== dad 'jon) (== child 'hal))
(all (== dad 'hal) (== child 'ted))
(all (== dad 'sam) (== child 'jay))))))
(letrec
((ancestor
(lambda (old young)
(any
(father old young)
(exists (not-so-old)
(all
(father old not-so-old)
(ancestor not-so-old young)))))))
(solve 20 (x) (ancestor 'jon x))))
(lambda (old young)
(any
(father old young)
(exists (not-so-old)
(all (father old not-so-old)
(ancestor not-so-old young)))))))
(pk (solve 20 (x) (ancestor 'jon x)))))
'(sam
hal
hal
rob
roz
jay
......@@ -753,38 +756,37 @@
((s (s (s (s (s (s z)))))) (s (s (s (s (s (s z)))))))
((s (s (s (s (s (s (s (s z)))))))) (s (s (s (s (s (s (s (s z)))))))))))
#;(test-check "Rinf+Rinf2"
(test-check "Rinf+Rinf2"
(solve 9 (x y)
(any-union (Rinf x y) (Rinf2 x y)))
'(((x.0 z) (y.0 z))
((x.0 (s z)) (y.0 (s z)))
((x.0 (s (s z))) (y.0 (s (s z))))
((x.0 (s (s (s (s z))))) (y.0 (s (s (s (s z))))))
((x.0 (s (s (s z)))) (y.0 (s (s (s z)))))
((x.0 (s (s (s (s (s (s z)))))))
(y.0 (s (s (s (s (s (s z))))))))
((x.0 (s (s (s (s (s (s (s (s z)))))))))
(y.0 (s (s (s (s (s (s (s (s z))))))))))
((x.0 (s (s (s (s (s z)))))) (y.0 (s (s (s (s (s z)))))))
((x.0 (s (s (s (s (s (s (s (s (s (s z)))))))))))
(y.0 (s (s (s (s (s (s (s (s (s (s z))))))))))))))
'((z z)
((s z) (s z))
((s (s z)) (s (s z)))
((s (s (s (s z)))) (s (s (s (s z)))))
((s (s (s z))) (s (s (s z))))
((s (s (s (s (s (s z))))))
(s (s (s (s (s (s z)))))))
((s (s (s (s (s (s (s (s z))))))))
(s (s (s (s (s (s (s (s z)))))))))
((s (s (s (s (s z))))) (s (s (s (s (s z))))))
((s (s (s (s (s (s (s (s (s (s z))))))))))
(s (s (s (s (s (s (s (s (s (s z)))))))))))))
#;(test-check "Rinf2+Rinf"
(test-check "Rinf2+Rinf"
(solve 9 (x y)
(any-union (Rinf2 x y) (Rinf x y)))
'(((x.0 z) (y.0 z))
((x.0 (s z)) (y.0 (s z)))
((x.0 (s (s z))) (y.0 (s (s z))))
((x.0 (s (s (s z)))) (y.0 (s (s (s z)))))
((x.0 (s (s (s (s z))))) (y.0 (s (s (s (s z))))))
((x.0 (s (s (s (s (s z)))))) (y.0 (s (s (s (s (s z)))))))
((x.0 (s (s (s (s (s (s z)))))))
(y.0 (s (s (s (s (s (s z))))))))
((x.0 (s (s (s (s (s (s (s z))))))))
(y.0 (s (s (s (s (s (s (s z)))))))))
((x.0 (s (s (s (s (s (s (s (s z)))))))))
(y.0 (s (s (s (s (s (s (s (s z))))))))))))
)))
'((z z)
((s z) (s z))
((s (s z)) (s (s z)))
((s (s (s z))) (s (s (s z))))
((s (s (s (s z)))) (s (s (s (s z)))))
((s (s (s (s (s z))))) (s (s (s (s (s z))))))
((s (s (s (s (s (s z))))))
(s (s (s (s (s (s z)))))))
((s (s (s (s (s (s (s z)))))))
(s (s (s (s (s (s (s z))))))))
((s (s (s (s (s (s (s (s z))))))))
(s (s (s (s (s (s (s (s z))))))))))))))
......@@ -864,3 +866,4 @@
((succ (succ (succ (succ zero)))) (succ zero))
((succ (succ (succ (succ (succ zero))))) zero))))
......@@ -2,7 +2,6 @@
#:use-module (ice-9 match)
#:use-module (logic guile-log)
#:use-module (logic guile-log umatch)
#:use-module (language tree-il)
#:use-module (test-suite lib))
#| Mapping the examples from reasoned schemer to guile-log |#
......
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