Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
branch: master
Fetching contributors…

Cannot retrieve contributors at this time

286 lines (244 sloc) 5.987 kb
(define-syntax lambdag@
(syntax-rules ()
((_ (a) e) (lambda (a) e))))
(define-syntax lambdaf@
(syntax-rules ()
((_ () e) (lambda () e))))
(define-syntax run*
(syntax-rules ()
((_ (x) g ...) (run #f (x) g ...))))
(define rhs
(lambda (pair)
(cdr pair)))
(define lhs
(lambda (pair)
(car pair)))
(define size-s
(lambda (s)
(length s)))
(define var
(lambda (name)
(vector name)))
(define var?
(lambda (x)
(vector? x)))
(define s-of
(lambda (a) a))
(define empty-s '())
(define empty-a empty-s)
(define walk
(lambda (v s)
(cond
((var? v)
(let ((a (assq v s)))
(cond
(a (walk (rhs a) s))
(else v))))
(else v))))
(define ext-s
(lambda (x v s)
(cons `(,x . ,v) s)))
(define unify
(lambda (u v s)
(let ((u (walk u s))
(v (walk v s)))
(cond
((eq? 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))))
((equal? u v) s)
(else #f)))))
(define unify-check
(lambda (u v s)
(let ((u (walk u s))
(v (walk v s)))
(cond
((eq? u v) s)
((var? u) (ext-s-check u v s))
((var? v) (ext-s-check v u s))
((and (pair? u) (pair? v))
(let ((s (unify-check
(car u) (car v) s)))
(and s (unify-check
(cdr u) (cdr v) s))))
((equal? u v) 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 walk*
(lambda (w s)
(let ((v (walk w 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 s)
(let ((v (walk* v s)))
(walk* v (reify-s v empty-s)))))
(define mzero
(lambda () #f))
(define-syntax inc
(syntax-rules () ((_ e) (lambdaf@ () e))))
(define unit
(lambda (a) a))
(define choice
(lambda (a f)
(cons a f)))
(define-syntax case-inf
(syntax-rules ()
((_ e (() e0) ((f^) e1) ((a^) e2) ((a f) e3))
(let ((a-inf e))
(cond
((not a-inf) e0)
((procedure? a-inf) (let ((f^ a-inf)) e1))
((not (and (pair? a-inf)
(procedure? (cdr a-inf))))
(let ((a^ a-inf)) e2))
(else (let ((a (car a-inf)) (f (cdr a-inf)))
e3)))))))
(define-syntax run
(syntax-rules ()
((_ n (x) g0 g ...)
(take n
(lambdaf@ ()
((exist (x) g0 g ...
(lambdag@ (a)
(cons (reify x a) '())))
empty-a))))))
(define take
(lambda (n f)
(if (and n (zero? n))
'()
(case-inf (f)
(() '())
((f) (take n f))
((a) a)
((a f)
(cons (car a)
(take (and n (- n 1)) f)))))))
(define ==
(lambda (u v)
(lambdag@ (a)
(unify u v a))))
(define ==-check
(lambda (u v)
(lambdag@ (a)
(unify-check u v a))))
(define-syntax exist
(syntax-rules ()
((_ (x ...) g0 g ...)
(lambdag@ (a)
(inc
(let ((x (var 'x)) ...)
(bind* (g0 a) g ...)))))))
(define-syntax bind*
(syntax-rules ()
((_ e) e)
((_ e g0 g ...) (bind* (bind e g0) g ...))))
(define bind
(lambda (a-inf g)
(case-inf a-inf
(() (mzero))
((f) (inc (bind (f) g)))
((a) (g a))
((a f) (mplus (g a) (lambdaf@ () (bind (f) g)))))))
(define-syntax conde
(syntax-rules ()
((_ (g0 g ...) (g1 g^ ...) ...)
(lambdag@ (a)
(inc
(mplus*
(bind* (g0 a) g ...)
(bind* (g1 a) g^ ...) ...))))))
(define-syntax mplus*
(syntax-rules ()
((_ e) e)
((_ e0 e ...) (mplus e0
(lambdaf@ () (mplus* e ...))))))
(define mplus
(lambda (a-inf f)
(case-inf a-inf
(() (f))
((f^) (inc (mplus (f) f^)))
((a) (choice a f))
((a f^) (choice a (lambdaf@ () (mplus (f) f^)))))))
(define-syntax conda
(syntax-rules ()
((_ (g0 g ...) (g1 g^ ...) ...)
(lambdag@ (a)
(inc
(ifa ((g0 a) g ...)
((g1 a) g^ ...) ...))))))
(define-syntax ifa
(syntax-rules ()
((_) (mzero))
((_ (e g ...) b ...)
(let loop ((a-inf e))
(case-inf a-inf
(() (ifa b ...))
((f) (inc (loop (f))))
((a) (bind* a-inf g ...))
((a f) (bind* a-inf g ...)))))))
(define-syntax condu
(syntax-rules ()
((_ (g0 g ...) (g1 g^ ...) ...)
(lambdag@ (a)
(inc
(ifu ((g0 a) g ...)
((g1 a) g^ ...) ...))))))
(define-syntax ifu
(syntax-rules ()
((_) (mzero))
((_ (e g ...) b ...)
(let loop ((a-inf e))
(case-inf a-inf
(() (ifu b ...))
((f) (inc (loop (f))))
((a) (bind* a-inf g ...))
((a f) (bind* (unit a) g ...)))))))
(define-syntax project
(syntax-rules ()
((_ (x ...) g g* ...)
(lambdag@ (a)
(let ((x (walk* x a)) ...)
((exist () g g* ...) a))))))
(define succeed (== #f #f))
(define fail (== #f #t))
(define onceo
(lambda (g)
(condu
(g succeed)
((== #f #f) fail))))
Jump to Line
Something went wrong with that request. Please try again.