Permalink
Browse files

alphaKanren merged in with cKanren

  • Loading branch information...
1 parent 72156bc commit 3a727b6f29280e890d6cd9923e6f20a78075ed0d @calvis committed Mar 30, 2013
Showing with 1,935 additions and 5 deletions.
  1. +329 −0 ak.rkt
  2. +16 −4 ck.rkt
  3. +121 −0 nominal/alphaleantap.rkt
  4. +174 −0 nominal/nnf.rkt
  5. +3 −1 testall.rkt
  6. +859 −0 tests/aktests-long.rkt
  7. +433 −0 tests/aktests.rkt
View
329 ak.rkt
@@ -0,0 +1,329 @@
+#lang racket
+
+(require (except-in "ck.rkt" walk walk*))
+(provide
+ == nom-constrained? project nom ==-check
+ fresh-nom hash (rename-out [make-tie tie]) unify-s walk get-sus nom?)
+
+(define-cvar-type nom "a")
+
+(define-syntax-rule (fresh-nom (n ...) g g* ...)
+ (fresh-aux nom (n ...) g g* ...))
+
+(define (sus-constrained? x oc)
+ (and (eq? (oc->rator oc) 'sus-c)
+ (eq? (sus-constraint-v oc) x)))
+
+(define (sus-constraint-v oc) (car (oc->rands oc)))
+
+(define (sus? x)
+ (and (pair? x) (eq? (car x) 'sus)))
+
+(define (get-sus x c)
+ (let ((oc (findf (lambda (oc) (sus-constrained? x oc)) c)))
+ (and oc (cons 'sus (oc->rands oc)))))
+
+(define (sus-v s) (cadr s))
+(define (sus-pi s) (caddr s))
+
+(define sus-c
+ (lambda (v pi)
+ (lambdam@ (a : s c)
+ (let ((v (walk v s c)))
+ ((update-c (build-oc sus-c v pi)) a)))))
+
+(define (make-tie a t) `(tie ,a ,t))
+(define (tie? x) (and (pair? x) (eq? (car x) 'tie)))
+(define (tie-a t) (cadr t))
+(define (tie-t t) (caddr t))
+
+(define sus
+ (lambda (x pi)
+ (goal-construct (sus-c x pi))))
+
+(define (nom-constrained? x c)
+ (and (findf (lambda (oc) (nom-constraint? x oc)) c) #t))
+
+(define (nom-constraint? x oc)
+ (and (eq? (oc->rator oc) 'nom-c)
+ (eq? (nom-v oc) x)))
+
+(define (nom-v oc) (car (oc->rands oc)))
+
+(define (nom-c x)
+ (lambdam@ (a : s c)
+ (let ((y (assq x s))) ;; hack
+ (cond
+ ((and y (nom? (cdr y))) #f)
+ (else ((update-c (build-oc nom-c x)) a))))))
+
+(define ==
+ (lambda (u v)
+ (goal-construct (unify-s u v))))
+
+(define unify-s
+ (lambda (u v)
+ (lambdam@ (a : s c)
+ (let ((u (walk u s c)) (v (walk v s c)))
+ (cond
+ ((eq? u v) a)
+ ((sus? u)
+ ((update-s (sus-v u) (apply-pi (sus-pi u) v c)) a))
+ ((get-sus u c)
+ => (lambda (s)
+ ((update-s u (apply-pi (sus-pi s) v c)) a)))
+ ((sus? v)
+ ((update-s (sus-v v) (apply-pi (sus-pi v) u c)) a))
+ ((get-sus v c)
+ => (lambda (s)
+ ((update-s v (apply-pi (sus-pi s) u c)) a)))
+ ((and (tie? u) (tie? v))
+ (let ((au (tie-a u)) (av (tie-a v))
+ (tu (tie-t u)) (tv (tie-t v)))
+ (if (eq? au av)
+ ((unify-s tu tv) a)
+ ((composem
+ (hash-c au tv)
+ (unify-s tu (apply-pi `((,au . ,av)) tv c)))
+ a))))
+ ((and (pair? u) (pair? v))
+ ((composem
+ (unify-s (car u) (car v))
+ (unify-s (cdr u) (cdr v)))
+ a))
+ ((and (var? u) (not (nom? u)))
+ ((composem
+ (sus u `())
+ (update-s u (apply-pi `() v c)))
+ a))
+ ((and (var? v) (not (nom? v)))
+ ((composem
+ (sus v `())
+ (update-s v (apply-pi `() u c)))
+ a))
+ ((or (nom? u) (nom? v)) #f)
+ ((equal? u v) a)
+ (else #f))))))
+
+(define ==-check
+ (lambda (u v)
+ (goal-construct (unify-s-check u v))))
+
+(define unify-s-check
+ (lambda (u v)
+ (lambdam@ (a : s c)
+ (let ((u (walk u s c)) (v (walk v s c)))
+ (cond
+ ((eq? u v) a)
+ ((sus? u)
+ ((ext-s-check (cadr u) (apply-pi (caddr u) v c)) a))
+ ((get-sus u c)
+ => (lambda (oc)
+ ((ext-s-check u (apply-pi (sus-pi oc) v c)) a)))
+ ((sus? v)
+ ((ext-s-check (cadr v) (apply-pi (caddr v) u c)) a))
+ ((get-sus v c)
+ => (lambda (oc)
+ ((ext-s-check v (apply-pi (sus-pi oc) u c)) a)))
+ ((and (tie? u) (tie? v))
+ (let ((au (tie-a u)) (av (tie-a v))
+ (tu (tie-t u)) (tv (tie-t v)))
+ (if (eq? au av)
+ ((unify-s-check tu tv) a)
+ ((composem
+ (hash-c au tv)
+ (unify-s-check tu (apply-pi `((,au . ,av)) tv c)))
+ a))))
+ ((and (pair? u) (pair? v))
+ ((composem
+ (unify-s-check (car u) (car v))
+ (unify-s-check (cdr u) (cdr v)))
+ a))
+ ((and (var? u) (not (nom? u)))
+ ((composem
+ (sus u `())
+ (ext-s-check u (apply-pi `() v c)))
+ a))
+ ((and (var? v) (not (nom? v)))
+ ((composem
+ (sus v `())
+ (ext-s-check v (apply-pi `() u c)))
+ a))
+ ((or (nom? u) (nom? v)) #f)
+ ((equal? u v) a)
+ (else #f))))))
+
+(define ext-s-check
+ (lambda (x u)
+ (lambdam@ (a : s c)
+ (and (occurs-check x u s c)
+ ((update-s x u) a)))))
+
+(define occurs-check
+ (lambda (x t s c)
+ (let rec ([t t])
+ (let ([t (walk (tie-t* t) s c)])
+ (cond
+ [(sus? t) (not (eq? x (sus-v t)))]
+ [(get-sus t c)
+ => (lambda (sus-c)
+ (not (eq? x (sus-v sus-c))))]
+ [(pair? t) (and (rec (car t)) (rec (cdr t)))]
+ [else #t])))))
+
+(define hash
+ (lambda (b t)
+ (goal-construct (hash-c b t))))
+
+(define hash-c
+ (lambda (b t)
+ (let rec ((t t))
+ (lambdam@ (a : s c)
+ (let ((t (walk t s c)))
+ (cond
+ ((eq? b t) #f)
+ ((sus? t)
+ (let ((lhs (apply-pi (caddr t) b c)))
+ ((update-c (build-oc hash-c lhs t)) a)))
+ ((get-sus t c)
+ => (lambda (sus-c)
+ (let ((lhs (apply-pi (sus-pi sus-c) b c)))
+ ((update-c (build-oc hash-c lhs t)) a))))
+ ((tie? t)
+ (if (eq? b (tie-a t)) a ((rec (tie-t t)) a)))
+ ((pair? t)
+ ((composem (rec (car t)) (rec (cdr t))) a))
+ ((and (var? t) (not (nom? t)))
+ ((composem (sus t `()) (rec t)) a))
+ (else a)))))))
+
+(define tie-t*
+ (lambda (t)
+ (if (tie? t) (tie-t* (tie-t t)) t)))
+
+(define walk-sym
+ (lambda (v s)
+ (let loop ((s s))
+ (cond
+ ((null? s) #f)
+ ((eq? v (caar s)) (car s))
+ (else (loop (cdr s)))))))
+
+(define walk
+ (lambda (x s c)
+ (let f ((x x) (pi '()))
+ (cond
+ ((sus? x)
+ (cond
+ ((walk-sym (sus-v x) s)
+ => (lambda (a) (f (cdr a) (compose-pis (sus-pi x) pi))))
+ (else (apply-pi pi x c))))
+ ((get-sus x c)
+ => (lambda (sus-c)
+ (cond
+ ((walk-sym x s)
+ => (lambda (a)
+ (f (cdr a)
+ (compose-pis (sus-pi sus-c) pi))))
+ (else (apply-pi pi x c)))))
+ (else (apply-pi pi x c))))))
+
+(define walk*
+ (lambda (t s c)
+ (let ((t (walk t s c)))
+ (cond
+ ((tie? t)
+ (make-tie (tie-a t) (walk* (tie-t t) s c)))
+ ((pair? t)
+ (cons (walk* (car t) s c) (walk* (cdr t) s c)))
+ (else t)))))
+
+(define compose-pis append)
+
+(define get-noms
+ (let ((with (lambda (n s) (if (memq n s) s (cons n s)))))
+ (lambda (pi s)
+ (cond
+ ((null? pi) s)
+ (else
+ (get-noms (cdr pi)
+ (with (caar pi) (with (cdar pi) s))))))))
+
+(define pi-ds
+ (lambda (pi1 pi2 c)
+ (for/fold ([s '()])
+ ([nom (get-noms pi1 (get-noms pi2 '()))])
+ (cond
+ ((eq? (apply-pi pi1 nom c) (apply-pi pi2 nom c)) s)
+ (else (cons nom s))))))
+
+(define id-pi?
+ (lambda (pi c) (null? (pi-ds pi '() c))))
+
+(define app
+ (lambda (pi a)
+ (let ((pi (reverse pi)))
+ (cond
+ ((null? pi) a)
+ ((eq? (caar pi) a)
+ (app (cdr pi) (cdar pi)))
+ ((eq? (cdar pi) a)
+ (app (cdr pi) (caar pi)))
+ (else (app (cdr pi) a))))))
+
+(define apply-pi
+ (lambda (pi t c)
+ (let rec ((t t))
+ (cond
+ ((nom? t) (app pi t))
+ ((sus? t)
+ (let ((pi (compose-pis pi (caddr t))))
+ (if (id-pi? pi c) t `(sus ,(cadr t) ,pi))))
+ ((get-sus t c)
+ => (lambda (sus-c)
+ (let ((pi (compose-pis pi (sus-pi sus-c))))
+ (if (id-pi? pi c) t `(sus ,t ,pi)))))
+ ((var? t)
+ (if (id-pi? pi c) t `(sus ,t ,pi)))
+ ((tie? t)
+ (make-tie (app pi (tie-a t))
+ (rec (tie-t t))))
+ ((pair? t) (cons (rec (car t)) (rec (cdr t))))
+ (else t)))))
+
+(define alpha-constraint?
+ (lambda (oc)
+ (memq (oc->rator oc) '(sus-c nom-c hash-c))))
+
+(define reify-alpha-constraints
+ (lambda (v r c)
+ (let ((c (filter alpha-constraint? c)))
+ (let ((c (reify-alpha r c)))
+ (if (null? c) c `((alpha . ,c)))))))
+
+(define reify-alpha
+ (lambda (r c)
+ (for/fold ([c^ '()])
+ ([oc c])
+ (cond
+ ((reify-oc oc r)
+ => (lambda (oc-sym)
+ (if (member oc-sym c^) c^ (cons oc-sym c^))))
+ (else c^)))))
+
+(define reify-oc
+ (lambda (oc r)
+ (case (oc->rator oc)
+ ((hash-c)
+ (let ((lhs (car (oc->rands oc)))
+ (rhs (cadr (oc->rands oc))))
+ (let ((rhs (if (sus? rhs) (cadr rhs) rhs)))
+ (let ((lhs (reify-cvar lhs r))
+ (rhs (reify-cvar rhs r)))
+ (and (not (any/var? lhs))
+ (not (any/var? rhs))
+ `(hash (,lhs ,rhs)))))))
+ (else #f))))
+
+(extend-reify-fns 'alpha reify-alpha-constraints)
+
View
20 ck.rkt
@@ -8,10 +8,10 @@
lambdam@ identitym composem goal-construct ext-c
build-oc oc->proc oc->rands oc->rator run run* prt
extend-enforce-fns extend-reify-fns goal? a?
- walk walk* var? lambdag@ mzerog unitg onceo
+ walk walk* var? lambdag@ mzerog unitg onceo fresh-aux
conde conda condu ifa ifu project fresh succeed fail
lambdaf@ inc enforce-constraints reify empty-a take
- format-source
+ format-source define-cvar-type reify-cvar var
(for-syntax build-srcloc))
;; == VARIABLES =================================================================
@@ -27,6 +27,13 @@
#:methods gen:custom-write
[(define (write-proc . args) (apply write-var args))])
+(define-syntax-rule (define-cvar-type name str)
+ (struct name var ()
+ #:methods gen:cvar
+ [(define (cvar->str x) str)]
+ #:methods gen:custom-write
+ [(define (write-proc . args) (apply write-var args))]))
+
;; write-var controls how variables are displayed
(define (write-var var port mode)
((parse-mode mode) (format "#~a(~s)" (cvar->str var) (var-x var)) port))
@@ -110,12 +117,15 @@
;; =============================================================================
-(define-syntax-rule (fresh (x ...) g g* ...)
+(define-syntax-rule (fresh-aux constructor (x ...) g g* ...)
(lambdag@ (a)
(inc
- (let ((x (var 'x)) ...)
+ (let ((x (constructor 'x)) ...)
(bindg* (app-goal g a) g* ...)))))
+(define-syntax-rule (fresh (x ...) g g* ...)
+ (fresh-aux var (x ...) g g* ...))
+
(define-syntax bindg*
(syntax-rules ()
[(_ e) e]
@@ -456,6 +466,8 @@
(else (reify-constraints (walk* v r) r c))))
(choiceg answer empty-f)))
+(define (reify-cvar cvar r) (walk cvar r))
+
;; reifies the substitution, returning the reified substitution
(define (reify-s v s)
(let ((v (walk v s)))
Oops, something went wrong.

0 comments on commit 3a727b6

Please sign in to comment.