conservatory
/
picrin
4
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

add (picrin logic) library

This commit is contained in:
Yuichi Nishiwaki 2015-07-20 22:10:39 +09:00
parent d11b569abf
commit bfdf60eee1
3 changed files with 258 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

131
contrib/60.logic/logic.scm Normal file
View File

@ -0,0 +1,131 @@
(define-library (picrin logic)
(import (scheme base)
(picrin control))
(export call/fresh
disj
conj
is
run-goal
run-goal*
zero
plus
unit
bind
reify
reflect)
(define (assp p alist)
(if (null? alist)
#f
(if (p (caar alist))
(car alist)
(assp p (cdr alist)))))
(define (force* $)
(if (procedure? $) (force* ($)) $))
;; fundation
(define (var c) (vector c))
(define (var? x) (vector? x))
(define (var=? x1 x2) (= (vector-ref x1 0) (vector-ref x2 0)))
(define (subst u s)
(let ((pr (and (var? u) (assp (lambda (v) (var=? u v)) s))))
(if pr (subst (cdr pr) s) u)))
(define (subst* v s)
(let ((v (subst v s)))
(cond
((var? v) v)
((pair? v) (cons (subst* (car v) s)
(subst* (cdr v) s)))
(else v))))
(define (ext-s x v s) `((,x . ,v) . ,s))
(define (unify u v s)
(let ((u (subst u s)) (v (subst v s)))
(cond
((and (var? u) (var? v) (var=? u v)) s)
((var? u) (ext-s u v s))
((var? v) (ext-s v u s))
((and (pair? u) (pair? v))
(let ((s (unify (car u) (car v) s)))
(and s (unify (cdr u) (cdr v) s))))
(else (and (eqv? u v) s)))))
;; klist monad
(define zero '())
(define (plus $1 $2)
(cond
((null? $1) $2)
((procedure? $1) (lambda () (plus $2 ($1))))
((pair? $1) (cons (car $1) (plus (cdr $1) $2)))))
(define (unit s/c) (list s/c))
(define (bind $ g)
(cond
((null? $) zero)
((procedure? $) (lambda () (bind ($) g)))
((pair? $) (plus (g (car $)) (bind (cdr $) g)))))
(define-syntax reify
(syntax-rules ()
((_ expr)
(reset (unit expr)))))
(define (reflect m)
(shift k (bind m k)))
;; goal constructors
(define (call/fresh f)
(lambda (s/c)
(let ((s (car s/c)) (c (cdr s/c)))
((f (var c)) `(,s . ,(+ c 1))))))
(define (disj g1 g2) (lambda (s/c) (plus (g1 s/c) (g2 s/c))))
(define (conj g1 g2) (lambda (s/c) (bind (g1 s/c) g2)))
(define (is u v)
(lambda (s/c)
(let ((s (unify u v (car s/c))))
(if s (unit `(,s . ,(cdr s/c))) zero))))
;; goal runner
(define initial-state '(() . 0))
(define (run-goal n g)
(map reify-1st (take n (g initial-state))))
(define (run-goal* g)
(map reify-1st (take* (g initial-state))))
(define (take n $)
(if (zero? n) '()
(let (($ (force* $)))
(if (null? $) '() (cons (car $) (take (- n 1) (cdr $)))))))
(define (take* $)
(let (($ (force* $)))
(if (null? $) '() (cons (car $) (take* (cdr $))))))
(define (reify-1st s/c)
(let ((v (subst* (var 0) (car s/c))))
(subst* v (reify-s v '()))))
(define (reify-s v s)
(let ((v (subst v s)))
(cond
((var? v)
(let ((n (reify-name (length s))))
(cons `(,v . ,n) s)))
((pair? v) (reify-s (cdr v) (reify-s (car v) s)))
(else s))))
(define (reify-name n)
(string->symbol
(string-append "_" "." (number->string n)))))

7
contrib/60.logic/nitro.mk Normal file
View File

@ -0,0 +1,7 @@
CONTRIB_LIBS += $(wildcard contrib/60.logic/*.scm)
CONTRIB_TESTS += test-logic
test-logic: bin/picrin
for test in `ls contrib/60.logic/t/*.scm`; do \
$(TEST_RUNNER) "$$test"; \
done

120
contrib/60.logic/t/logic-test.scm Normal file
View File

@ -0,0 +1,120 @@
(import (scheme base)
(scheme lazy)
(scheme write)
(picrin logic)
(picrin test))
(define-syntax Zzz
(syntax-rules ()
((_ g) (lambda (s/c) (lambda () (g s/c))))))
(define-syntax conj+
(syntax-rules ()
((_ g) (Zzz g))
((_ g0 g ...) (conj (Zzz g0) (conj+ g ...)))))
(define-syntax disj+
(syntax-rules ()
((_ g) (Zzz g))
((_ g0 g ...) (disj (Zzz g0) (disj+ g ...)))))
(define-syntax fresh
(syntax-rules ()
((_ () g0 g ...) (conj+ g0 g ...))
((_ (x0 x ...) g0 g ...)
(call/fresh
(lambda (x0)
(fresh (x ...) g0 g ...))))))
(define-syntax conde
(syntax-rules ()
((_ (g0 g ...) ...) (disj+ (conj+ g0 g ...) ...))))
(define-syntax run
(syntax-rules ()
((_ n (x ...) g0 g ...)
(run-goal n (fresh (x ...) g0 g ...)))))
(define-syntax run*
(syntax-rules ()
((_ (x ...) g0 g ...)
(run-goal* (fresh (x ...) g0 g ...)))))
(define (appendo l s out)
(conde
((is '() l) (is s out))
((fresh (a d res)
(is `(,a . ,d) l)
(is `(,a . ,res) out)
(appendo d s res)))))
(test '((() (1 2 3 4 5))
((1) (2 3 4 5))
((1 2) (3 4 5))
((1 2 3) (4 5))
((1 2 3 4) (5))
((1 2 3 4 5) ()))
(run* (q) (fresh (x y) (is `(,x ,y) q) (appendo x y '(1 2 3 4 5)))))
(test '((() (1 2 3 4 5))
((1) (2 3 4 5))
((1 2) (3 4 5))
((1 2 3) (4 5))
((1 2 3 4) (5))
((1 2 3 4 5) ()))
(run* (q x y) (is `(,x ,y) q) (appendo x y '(1 2 3 4 5))))
(test '((1 2 8 3 4 5)
(1 2 8 3 4 5 8)
(1 2 8 3 4 8 5)
(1 2 8 3 8 4 5)
(1 2 8 8 3 4 5)
(1 2 8 8 3 4 5)
(1 8 2 8 3 4 5)
(8 1 2 8 3 4 5))
(letrec
((rember*o (lambda (tr o)
(conde
((is '() tr) (is '() o))
((fresh (a d)
(is `(,a . ,d) tr)
(conde
((fresh (aa da)
(is `(,aa . ,da) a)
(fresh (a^ d^)
(rember*o a a^)
(rember*o d d^)
(is `(,a^ . ,d^) o))))
((is a 8) (rember*o d o))
((fresh (d^)
(rember*o d d^)
(is `(,a . ,d^) o))))))))))
(run 8 (q) (rember*o q '(1 2 8 3 4 5)))))
(test '((1 (2 8 3 4) 5)
(1 (2 8 3 4) 5 8)
(1 (2 8 3 4) 5 8 8)
(1 (2 8 3 4) 8 5)
(1 8 (2 8 3 4) 5)
(8 1 (2 8 3 4) 5)
(1 (2 8 3 4) 5 8 8 8)
(1 (2 8 3 4) 5 8 8 8 8)
(1 (2 8 3 4) 5 8 8 8 8 8))
(letrec
((rember*o (lambda (tr o)
(conde
((is '() tr) (is '() o))
((fresh (a d)
(is `(,a . ,d) tr)
(conde
((fresh (aa da)
(is `(,aa . ,da) a)
(fresh (a^ d^)
(is `(,a^ . ,d^) o)
(rember*o d d^)
(rember*o a a^))))
((is a 8) (rember*o d o))
((fresh (d^)
(is `(,a . ,d^) o)
(rember*o d d^))))))))))
(run 9 (q) (rember*o q '(1 (2 8 3 4) 5)))))