Hopefully we have a working and-i by now based on guarded state variables

parent 8b3a2495
......@@ -401,16 +401,30 @@ will put the @code{p} and the @code{cc} in front and execute that. e.g. to defin
@findex <if>
@findex <cond>
@findex <or!>
@findex <or-i>
@findex <succeeds>
@findex <and-i>
@findex interleave
@findex and-interleave
@code{G.L. (<if> p x)}, if @code{p} is a success then @code{x}, @code{p} will only success at most one time.
@code{G.L. (<if> p x y)}, if @code{p} is success then @code{x}, else backtrack and use @code{y}, the same condition holds on @code{p} as the previous version of if.
@code{G.L. (<cond> (P X) ...)}, like the ordinary cond, but using @code{<if>} in stead of @code{if}
@code{G.L. (<or!> p1 p2 ... pn)}, if @code{p1} successes and we later backtrack then try @code{p2} etc and so on until @code{pn} if @code{pn} successes and we later backtrack then @code{p1} is tried again and interleave like that. To note here is that this form uses both bank a and b and in order to function correctly when storing a state both bank a and bank b need to be stored.
@code{G.L. (<or-i> p1 p2 ... pn)}, if @code{p1} successes and we later backtrack then try @code{p2} etc and so on until @code{pn} if @code{pn} successes and we later backtrack then @code{p1} is tried again and interleave like that. To note here is that this form uses both bank a and b and in order to function correctly when storing a state both bank a and bank b need to be stored.
@code{G.L. (interleave l)}, the same as @code{<or-i>} but with the difference l is a list of lambdas typically made by @code{(</.> ...)}.
@code{G.L. (<and-i> p1 p2 p3 ...)}, and interleaving! this is an and which will in parctice behave as
@verbatim
(<and-i> (<or> A B) (<or> C D))
<=>
(<or> (<and> A C) (<and> B C) (<and> A C) (<and> B C))
@end verbatim
e.g. backtracking is shallow and we will backtrack all the first combinations, then all the second combinations then all the third ones etc. To accomplish this state information needs to be stored hence using this tool can be slow and memory intensive.
@code{G.L. (and-interleave l)}, the same as @code{<and-i>} but with the difference l is a list of lambdas typically made by @code{(</.> ...)}.
@code{G.L. (<succeeds> p)} will try @code{p} and if it succeeds undo any bindings and continue.
......
;; sematically after kanrens all-interleave
(define-guile-log <or!>
(define-guile-log <or-i>
(syntax-rules ()
((_ w)
(parse<> w <fail>))
......@@ -10,56 +9,116 @@
((_ w a ...)
(parse<> w (interleave (list (</.> a) ...))))))
(define-guile-log <and-i>
(syntax-rules ()
((_ w)
(parse<> w <cc>))
((_ w a)
(parse<> w a))
((_ w a ...)
(parse<> w (and-interleave (list (</.> a) ...))))))
(define (interleave p cc l)
(let ((s (gp-store-state)))
(gp-swap-to-b)
(let* ((ul (u-var!))
(ur (u-var!))
(n (u-var!))
(fr (gp-newframe)))
(u-set! n 0)
(gp-swap-to-a)
(let ((ul '())
(ur '()))
(letrec ((loop (lambda (l r)
(if (null? l)
(if (null? r)
(p)
(loop (reverse r) '()))
(begin
(gp-swap-to-b)
(u-set! ul l)
(u-set! ur r)
(gp-swap-to-a)
(set! ul l)
(set! ur r)
((car l)))))))
(define (unwind-if-more-then-one-set)
(begin
(gp-swap-to-b)
(let ((m (gp-lookup n)))
(if (= m 1)
(gp-unwind 2)
(u-set! n (+ m 1))))
(gp-swap-to-a)))
(loop
(map (lambda (a)
(lambda ()
(gp-restore-state s)
(a
(lambda ()
(loop (cdr (gp-lookup ul))
(gp-lookup ur)))
(loop (cdr ul) ur))
(lambda (pp)
(cc (let* ((s (gp-store-state))
(l (gp-lookup ul))
(r (gp-lookup ur)))
(unwind-if-more-then-one-set)
(cc (let ((s (gp-store-state)))
(lambda ()
(loop (cdr l)
(loop (cdr ul)
(cons (lambda ()
(gp-restore-state s)
(pp))
r)))))))))
ur)))))))))
l)
'())))))
#|
and-interleave
--------------
(define (f p cc g1 g2)
(g1 p (lambda (p)
(let ((f (lambda (pp ccc) (p))))
(with-guile-log (p cc)
(<or> (g2 p cc)
f))))))
|#
(define (and-interleave p cc gs)
(match gs
(()
(cc p))
((g)
(g p cc))
((g . gl)
(alli p cc g gl))))
(define (alli p cc g1 gs)
(with-guarded-states guard-set! ((l '()) (r '()))
(define fail
(lambda ()
(let loop ((ll l) (rr r))
(if (null? ll)
(if (null? rr)
(p)
(loop (reverse rr) '()))
(let ((thunk (car ll)))
(guard-set! (cdr ll) rr)
(thunk))))))
(define (mk-cont p)
(let ((state (gp-store-state)))
(lambda ()
(gp-restore-wind state)
(p))))
(let loop ((p p) (g1 g1) (gs gs))
(match gs
((g2)
(g1 fail
(lambda (p2)
(guard-set! l (cons (mk-cont p2) r))
(g2 fail
(lambda (p3)
(guard-set! l (cons (mk-cont p3) r))
(cc fail))))))
((g2 . gs)
(g1 fail
(lambda (p2)
(guard-set! l (cons (mk-cont p2) r))
(loop p2 g2 gs))))))))
#|
This is kanren interleave,
s(a,1) -> s(b,1), a1,b1
s(a,2) -> s(b,1), b1,a2,b2
s(a,1) -> s(b,2), a2,b2,b3
* , b2,b3
s(a,2) -> s(b,2), b3,b4
* , b4
* , *
|#
......@@ -8,8 +8,9 @@
<and!> <and!!> <succeeds>
<format> <tail-code> <code> <ret> <return>
<def> <<define>> <with-fail> <dynwind> parse<>
let<> <or!> <stall> <continue> <take>
<state-ref> <state-set!> <lv*> <clear>)
let<> <or-i> <stall> <continue> <take>
<state-ref> <state-set!> <lv*> <clear>
<and-i> and-interleave interleave)
(re-export define-guile-log guile-log-macro? log-code-macro log-code-macro?)
......@@ -146,7 +147,6 @@
(cons #f (lambda (mm)
(set! n mm)
(u-abort p))))
(pk *cc*)
r)
(u-abort p)))
(reverse ret))))))))
......@@ -380,6 +380,10 @@
(log-code-macro '<when>)
(define (pp x)
(pretty-print x)
x)
(define-guile-log <pp>
(syntax-rules ()
((_ wc x) (begin (pp (u-scm x))
......
......@@ -23,6 +23,8 @@
#:use-module (ice-9 pretty-print)
#:use-module (ice-9 format)
#:use-module (srfi srfi-1)
#:use-module (srfi srfi-11)
#:use-module (srfi srfi-9)
#:export (gp-clear gp-unify! gp-unify-raw! gp-newframe gp-unwind gp-var!
gp->scm gp-print
gp-budy gp-swap-to-a gp-swap-to-b gp-m-unify!
......@@ -30,18 +32,15 @@
gp-var? gp-cons! gp-set! u-list
gp-printer gp-var-number
gp-car gp-cdr gp-pair?
gp-store-state gp-restore-state
gp-store-state gp-restore-state gp-restore-wind
gp-make-fluid gp-fluid-set! gp-fluid-ref with-gp-fluids
gp-dynwind
u-prompt u-abort u-set! u-var! u-call u-deref gp-atomic?
u-context u-modded
u-unify! u-scm u-unify-raw! u-cons u-dynwind umatch
gp-copy **um** gp-get-stack))
;;need to add modded,
(define-syntax **um** (syntax-rules () ((_ . l) (umatch . l))))
gp-copy **um** gp-get-stack
push-setup que-setup
with-guarded-states))
(define gp-module-init #f)
(define gp? #f)
......@@ -50,6 +49,7 @@
(define gp-cdr #f)
;;need to add modded,
(let ((file (%search-load-path "logic/guile-log/src/libguile-unify.so")))
(if file
(load-extension file "gp_init")
......@@ -57,6 +57,87 @@
(gp-module-init)
(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)
(if *setup*
(dynamic-wind
(lambda x #f)
(lambda ()
(for-each (lambda (thunk) (thunk))
(car *setup*))
(for-each (lambda (thunk) (thunk))
(reverse (cdr *setup*))))
(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*)))
(set! *setup* (cons (list x) '()))))
(define (que-setup x)
(if *setup*
(set-cdr! *setup* (cons x (cdr *setup*)))
(set! *setup* (cons '() (list x)))))
(define *wind* #f)
(define *states* #t)
(define-syntax mk-guard
(lambda (x)
(syntax-case x ()
((_ fr done guard s ...)
(with-syntax (((ss ...) (generate-temporaries #'(s ...)))
((so ...) (generate-temporaries #'(s ...))))
#'(lambda (ss ...)
(let ((so s) ...)
(set! s ss) ...
(dyn
;;rewind
(lambda ()
(if (and *wind* (not done))
(begin
(set! done #t)
(push-setup
(let ((ss s) ...)
(lambda ()
(set! done #f)
(if fr
(guard ss ...)))))))
(set! s ss) ...)
(lambda ()
(if (and *wind* (not done))
(begin
(set! done #t)
(push-setup
(let ((ss s) ...)
(lambda ()
(set! done #f)
(if fr
(guard ss ...)))))))
(set! s so) ...)))))))))
(define-syntax with-guarded-states
(lambda (x)
(syntax-case x ()
((_ guard ((s v) ...) code ...)
#'(let ((s v) ... (fr #t) (done #f))
(letrec ((guard (mk-guard fr done guard s ...)))
(dyn
(lambda () (set! fr #t))
(lambda () (set! fr #f)))
(let () code ...)))))))
(define old gp-make-fluid)
(define gp-make-fluid
......@@ -277,5 +358,14 @@
...
(_ (error (format #f "umatch ~a did not match" n))))))))
(define gp-restore-state-raw gp-restore-state)
(define (gp-restore-wind x)
(set! *wind* #t)
(set! *setup* #f)
(gp-restore-state-raw x)
(do-setup))
(define (gp-restore-state x)
(set! *wind* #f)
(gp-restore-state-raw x))
......@@ -1161,7 +1161,7 @@
(define-guile-log <condi>
(syntax-rules ()
((_ w (x y ...) ...)
(parse<> w (<or!> (<and> (pelse x) y ...) ...)))))
(parse<> w (<or-i> (<and> (pelse x) y ...) ...)))))
(check?
......@@ -1180,3 +1180,183 @@
(<=> #t q))
'(#t #t #t #t #t))
(check?
(<run> 5 (r)
(<condi>
((teacup r))
((<=> #f r))))
'(tea #f cup))
(check?
(<run> 5 (q)
(<condi>
((<=> #f q) (alwayso))
((<=> #t q) (alwayso)))
(<=> #t q))
'(#t #t #t #t #t))
(check?
(<run> 5 (q)
(<and-i>
(<conde>
((<=> #f q))
((<=> #t q)))
(alwayso))
(<=> #t q))
'(#t #t #t #t #t))
(<define> (bit-xoro x y r)
(<conde>
((<=> (0 0 0) (x y r)))
((<=> (1 0 1) (x y r)))
((<=> (0 1 1) (x y r)))
((<=> (1 1 0) (x y r)))))
(check?
(<run> * (s)
(<var> (x y)
(bit-xoro x y 0)
(<=> (x y) s)))
'((0 0) (1 1)))
(check?
(<run> * (s)
(<var> (x y)
(bit-xoro x y 1)
(<=> (x y) s)))
'((1 0) (0 1)))
(<define> (bit-ando x y r)
(<conde>
((<=> (0 0 0) (x y r)))
((<=> (1 0 0) (x y r)))
((<=> (0 1 0) (x y r)))
((<=> (1 1 1) (x y r)))))
(check?
(<run> * (s)
(<var> (x y)
(bit-ando x y 1)
(<=> (x y) s)))
'((1 1)))
(<define> (half-addero x y r c)
(bit-xoro x y r)
(bit-ando x y c))
(check?
(<run> * (s)
(<var> (x y r c)
(half-addero x y r c)
(<=> (x y r c) s)))
'((0 0 0 0)
(1 0 1 0)
(0 1 1 0)
(1 1 0 1)))
(<define> (full-addero b x y r c)
(<var> (w xy wz)
(half-addero x y w xy)
(half-addero w b r wz)
(bit-xoro xy wz c)))
(check?
(<run> * (s)
(<var> (r c)
(full-addero 0 1 1 r c)
(<=> (r c) s)))
'((0 1)))
(check?
(<run> * (s)
(<var> (r c)
(full-addero 1 1 1 r c)
(<=> (r c) s)))
'((1 1)))
(define (build-num n)
(cond
((odd? n)
(cons 1 (build-num (/ (- n 1) 2))))
((and (not (zero? n)) (even? n))
(cons 0 (build-num (/ n 2))))
((zero? n) '())))
(<define> (poso n)
(<var> (x y)
(<=> (x . y) n)))
(<define> (>1o n)
(<var> (a ad dd)
(<=> (a ad . dd) n)))
(<define> (addero d n m r)
(<condi>
((<=> (0 '() n) (d m r)))
((<=> (0 '() m) (d n r))
(poso m))
((<=> (1 '()) (d m))
(addero 0 n '(1) r))
((<=> (1 '()) (d n))
(poso m)
(addero 0 '(1) m r))
((<=> ('(1) '(1)) (n m))
(<var> (a c)
(<=> (a c) r)
(full-addero d 1 1 a c)))
((<=> '(1) n)
(gen-addero d n m r))
((<=> '(1) m) (>1o n) (>1o r)
(addero d '(1) n r))
((>1o n)
(gen-addero d n m r))))
(<define> (gen-addero d n m r)
(<var> (a b c e x y z)
(<=> (a . x) n)
(<=> (b . y) m) (poso y)
(<=> (c . z) r) (poso z)
(<and-i>
(full-addero d a b c e)
(addero e x y z))))
(check?
(<run> 3 (s)
(<var> (x y r)
(addero 0 x y r)
(<=> (x y r) s)))
'((v0 () v0)
(() (v0 . v1) (v0 . v1))
((1) (1) (0 1))))
(check?
(<run> 22 (s)
(<var> (x y r)
(addero 0 x y r)
(<=> (x y r) s)))
'((v0 () v0)
(() (v0 . v1) (v0 . v1))
((1) (1) (0 1))
((1) (0 v0 . v1) (1 v0 . v1))
((0 v0 . v1) (1) (1 v0 . v1))
((0 1) (0 1) (0 0 1))
((1) (1 1) (0 0 1))
((1 1) (1) (0 0 1))
((1 1) (0 1) (1 0 1))
((1) (1 0 v0 . v1) (0 1 v0 . v1))
((1 0 v0 . v1) (1) (0 1 v0 . v1))
((0 1) (0 0 v0 . v1) (0 1 v0 . v1))
((1) (1 1 1) (0 0 0 1))
((1 1 1) (1) (0 0 0 1))
((0 1) (1 1) (1 0 1))
((1) (1 1 0 v0 . v1) (0 0 1 v0 . v1))
((1 1 0 v0 . v1) (1) (0 0 1 v0 . v1))
((1 1) (0 0 v0 . v1) (1 1 v0 . v1))
((1) (1 1 1 1) (0 0 0 0 1))
((1 1 1 1) (1) (0 0 0 0 1))
((0 0 v0 . v1) (0 1) (0 1 v0 . v1))
((1) (1 1 1 0 v0 . v1) (0 0 0 1 v0 . v1))))
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