From bfdf60eee1b40a3c6db0276d952c1e2199a22bfa Mon Sep 17 00:00:00 2001 From: Yuichi Nishiwaki Date: Mon, 20 Jul 2015 22:10:39 +0900 Subject: [PATCH] add (picrin logic) library --- contrib/60.logic/logic.scm | 131 ++++++++++++++++++++++++++++++ contrib/60.logic/nitro.mk | 7 ++ contrib/60.logic/t/logic-test.scm | 120 +++++++++++++++++++++++++++ 3 files changed, 258 insertions(+) create mode 100644 contrib/60.logic/logic.scm create mode 100644 contrib/60.logic/nitro.mk create mode 100644 contrib/60.logic/t/logic-test.scm diff --git a/contrib/60.logic/logic.scm b/contrib/60.logic/logic.scm new file mode 100644 index 00000000..b90b0fae --- /dev/null +++ b/contrib/60.logic/logic.scm @@ -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))))) diff --git a/contrib/60.logic/nitro.mk b/contrib/60.logic/nitro.mk new file mode 100644 index 00000000..c5b493a8 --- /dev/null +++ b/contrib/60.logic/nitro.mk @@ -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 diff --git a/contrib/60.logic/t/logic-test.scm b/contrib/60.logic/t/logic-test.scm new file mode 100644 index 00000000..33d36706 --- /dev/null +++ b/contrib/60.logic/t/logic-test.scm @@ -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)))))