; miniKanren (Reasoned Schemer) --- SchemeのProlog風DSL
;
; ソクラテスは死ぬ?
(define-syntax lambdag@
(syntax-rules ()
((_ (s) e) (lambda (s) e))))
(define-syntax lambdaf@
(syntax-rules ()
((_ () e) (lambda () e))))
(define-syntax rhs
(syntax-rules ()
((rhs p) (cdr p))))
(define-syntax lhs
(syntax-rules ()
((lhs p) (car p))))
(define-syntax var
(syntax-rules ()
((var w) (vector w))))
(define-syntax var?
(syntax-rules ()
((var? w) (vector? w))))
(define-syntax size-s
(syntax-rules ()
((size-s ls) (length ls))))
(define empty-s '())
(define walk
(lambda (v s)
(cond
((var? v)
(cond
((assq v s) =>
(lambda (a)
(let ((v^ (rhs a)))
(walk v^ s))))
(else v)))
(else v))))
(define ext-s
(lambda (x v s)
(cons `(,x . ,v) s)))
(define unify
(lambda (v w s)
(let ((v (walk v s))
(w (walk w s)))
(cond
((eq? v w) s)
((var? v) (ext-s v w s))
((var? w) (ext-s w v s))
((and (pair? v) (pair? w))
(cond
((unify (car v) (car w) s) =>
(lambda (s)
(unify (cdr v) (cdr w) s)))
(else #f)))
((equal? v w) s)
(else #f)))))
(define ext-s-check
(lambda (x v s)
(cond
((occurs-check x v s) #f)
(else (ext-s x v s)))))
(define occurs-check
(lambda (x v s)
(let ((v (walk v s)))
(cond
((var? v) (eq? v x))
((pair? v)
(or
(occurs-check x (car v) s)
(occurs-check x (cdr v) s)))
(else #f)))))
(define unify-check
(lambda (v w s)
(let ((v (walk v s))
(w (walk w s)))
(cond
((eq? v w) s)
((var? v) (ext-s-check v w s))
((var? w) (ext-s-check w v s))
((and (pair? v) (pair? w))
(cond
((unify-check (car v) (car w) s) =>
(lambda (s)
(unify-check (cdr v) (cdr w) s)))
(else #f)))
((equal? v w) s)
(else #f)))))
(define walk*
(lambda (v s)
(let ((v (walk v s)))
(cond
((var? v) v)
((pair? v)
(cons
(walk* (car v) s)
(walk* (cdr v) s)))
(else v)))))
(define reify-s
(lambda (v s)
(let ((v (walk v s)))
(cond
((var? v) (ext-s v (reify-name (size-s s)) s))
((pair? v) (reify-s (cdr v) (reify-s (car v) s)))
(else s)))))
(define reify-name
(lambda (n)
(string->symbol
(string-append "_" "." (number->string n)))))
(define reify
(lambda (v)
(walk* v (reify-s v empty-s))))
(define-syntax run
(syntax-rules ()
((_ n^ (x) g ...)
(let ((n n^) (x (var 'x)))
(if (or (not n) (> n 0))
(map-inf n
(lambda (s) (reify (walk* x s)))
((all g ...) empty-s))
'())))))
(define-syntax case-inf
(syntax-rules ()
((_ e on-zero ((a^) on-one) ((a f) on-choice))
(let ((a-inf e))
(cond
((not a-inf) on-zero)
((not (and
(pair? a-inf)
(procedure? (cdr a-inf))))
(let ((a^ a-inf))
on-one))
(else (let ((a (car a-inf))
(f (cdr a-inf)))
on-choice)))))))
(define-syntax mzero
(syntax-rules ()
((_) #f)))
(define-syntax unit
(syntax-rules ()
((_ a) a)))
(define-syntax choice
(syntax-rules ()
((_ a f) (cons a f))))
(define map-inf
(lambda (n p a-inf)
(case-inf a-inf
'()
((a)
(cons (p a) '()))
((a f)
(cons (p a)
(cond
((not n) (map-inf n p (f)))
((> n 1) (map-inf (- n 1) p (f)))
(else '())))))))
(define ==
(lambda (v w)
(lambdag@ (s)
(cond
((unify v w s) => succeed)
(else (fail s))))))
(define ==-check
(lambda (v w)
(lambdag@ (s)
(cond
((unify-check v w s) => succeed)
(else (fail s))))))
(define-syntax fresh
(syntax-rules ()
((_ (x ...) g ...)
(lambdag@ (s)
(let ((x (var 'x)) ...)
((all g ...) s))))))
(define-syntax all
(syntax-rules ()
((_) succeed)
((_ g) (lambdag@ (s) (g s)))
((_ g^ g ...) (lambdag@ (s) (bind (g^ s) (all g ...))))))
(define-syntax conde
(syntax-rules (else)
((_) fail)
((_ (else g0 g ...)) (all g0 g ...))
((_ (g0 g ...) c ...)
(anye (all g0 g ...) (conde c ...)))))
(define succeed (lambdag@ (s) (unit s)))
(define fail (lambdag@ (s) (mzero)))
(define bind
(lambda (a-inf g)
(case-inf a-inf
(mzero)
((a) (g a))
((a f) (mplus (g a)
(lambdaf@ () (bind (f) g)))))))
(define mplus
(lambda (a-inf f)
(case-inf a-inf
(f)
((a) (choice a f))
((a f0) (choice a
(lambdaf@ () (mplus (f0) f)))))))
(define-syntax anye
(syntax-rules ()
((_ g1 g2)
(lambdag@ (s)
(mplus (g1 s)
(lambdaf@ () (g2 s)))))))
(define-syntax alli
(syntax-rules ()
((_) succeed)
((_ g) (lambdag@ (s) (g s)))
((_ g^ g ...)
(lambdag@ (s)
(bindi (g^ s) (alli g ...))))))
(define-syntax condi
(syntax-rules (else)
((_) fail)
((_ (else g0 g ...)) (all g0 g ...))
((_ (g0 g ...) c ...)
(anyi (all g0 g ...) (condi c ...)))))
(define-syntax anyi
(syntax-rules ()
((_ g1 g2)
(lambdag@ (s)
(mplusi (g1 s)
(lambdaf@ () (g2 s)))))))
(define bindi
(lambda (a-inf g)
(case-inf a-inf
(mzero)
((a) (g a))
((a f) (mplusi (g a)
(lambdaf@ () (bindi (f) g)))))))
(define mplusi
(lambda (a-inf f)
(case-inf a-inf
(f)
((a) (choice a f))
((a f0) (choice a
(lambdaf@ () (mplusi (f) f0)))))))
(define-syntax conda
(syntax-rules (else)
((_) fail)
((_ (else g0 g ...)) (all g0 g ...))
((_ (g0 g ...) c ...)
(ifa g0 (all g ...) (conda c ...)))))
(define-syntax condu
(syntax-rules (else)
((_) fail)
((_ (else g0 g ...)) (all g0 g ...))
((_ (g0 g ...) c ...)
(ifu g0 (all g ...) (condu c ...)))))
(define-syntax ifa
(syntax-rules ()
((_ g0 g1 g2)
(lambdag@ (s)
(let ((s-inf (g0 s)) (g^ g1))
(case-inf s-inf
(g2 s)
((s) (g^ s))
((s f) (bind s-inf g^))))))))
(define-syntax ifu
(syntax-rules ()
((_ g0 g1 g2)
(lambdag@ (s)
(let ((s-inf (g0 s)) (g^ g1))
(case-inf s-inf
(g2 s)
((s) (g^ s))
((s f) (g^ s))))))))
(define-syntax run*
(syntax-rules ()
((_ (x) g ...) (run #f (x) g ...))))
(define-syntax lambda-limited
(syntax-rules ()
((_ n formals g)
(let ((x (var 'x)))
(lambda formals
(ll n x g))))))
(define ll
(lambda (n x g)
(lambdag@ (s)
(let ((v (walk x s)))
(cond
((var? v) (g (ext-s x 1 s)))
((< v n) (g (ext-s x (+ v 1) s)))
(else (fail s)))))))
(define-syntax project
(syntax-rules ()
((_ (x ...) g ...)
(lambdag@ (s)
(let ((x (walk* x s)) ...)
((all g ...) s))))))
(define nl (string #\newline))
(define (cout . args)
(for-each (lambda (x)
(if (procedure? x) (x) (display x)))
args))
(define errorf
(lambda (tag . args)
(display "Failed: ") (display tag) (newline)
(for-each display args)
(error 'WiljaCodeTester "That's all, folks!")))
(define caro
(lambda (p a)
(fresh (d)
(== (cons a d) p))))
(define cdro
(lambda (p d)
(fresh (a)
(== (cons a d) p))))
(define conso
(lambda (a d p)
(== (cons a d) p)))
(define choose
(lambda (l a b)
(fresh ()
(== #t (pair? l))
(conde
((== (car l) (cons a b)))
(else (choose (cdr l) a b))))))
(define 名前
'(("ソクラテス" . "人")
("アリストテレス" . "人")
("飯島愛" . "天使")
("HAL9000" . "ロボット")))
(define 名前?
(lambda (l a d)
(fresh (p)
(choose l a d))))
(define 生死
'(("人" . "死ぬ")
("天使" . "不滅")
("ロボット" . "壊れる")))
(define 生死?
(lambda (l a d)
(fresh (p)
(choose l a d))))
(define 死ぬの?
(lambda (a live_or_die)
(run* (out)
(fresh (d)
(名前? 名前 a d)
(生死? 生死 d live_or_die)
(conso a live_or_die out)))))
(define a (var 'a))
(define d (var 'd))
(cout (死ぬの? a "死ぬ")) (newline) (newline)
(cout (死ぬの? a "不滅")) (newline) (newline)
(cout (死ぬの? a d))