Permalink
Browse files

added a unifiable? predicate to mk-structs, so unify can deal with in…

…heritance
  • Loading branch information...
1 parent 4778362 commit 29a4c92c887c2f22f9c575e6984eed588679560f @calvis committed Apr 2, 2013
Showing with 41 additions and 25 deletions.
  1. +1 −1 README.md
  2. +2 −0 ak.rkt
  3. +6 −1 ck.rkt
  4. +7 −1 tests/vector.rkt
  5. +25 −22 tree-unify.rkt
View
@@ -1,4 +1,4 @@
-Copyright (C) 2011 Daniel P. Friedman, Oleg Kiselyov,
+Copyright (C) 2011-2013 Daniel P. Friedman, Oleg Kiselyov,
Claire E. Alvis, Jeremiah J. Willcock, Kyle M. Carter, William E. Byrd
Permission is hereby granted, free of charge, to any person obtaining a copy
View
2 ak.rkt
@@ -40,6 +40,8 @@
(define (constructor tie)
(lambda (a t-ls)
(make-tie a (car t-ls))))
+ (define (unifiable? tie x)
+ (tie? x))
(define (mk-struct->sexp tie)
`(tie ,(tie-a tie) ,(tie-t tie)))])
View
7 ck.rkt
@@ -12,7 +12,7 @@
conde conda condu ifa ifu project fresh succeed fail
lambdaf@ inc enforce-constraints reify empty-a take
format-source define-cvar-type reify-cvar var ext-s
- gen:mk-struct recur constructor mk-struct?
+ gen:mk-struct recur constructor mk-struct? unifiable?
lex<= sort-by-lex<= reify-with-colon occurs-check
(for-syntax build-srcloc))
@@ -257,6 +257,9 @@
;; arguments like the arguments to k
(constructor mk-struct)
+ ;; determines whether mk-struct can unify with x
+ (unifiable? mk-struct x)
+
;; for reification
(mk-struct->sexp mk-struct)
@@ -265,13 +268,15 @@
(define (recur p k)
(k (car p) (cdr p)))
(define (constructor p) cons)
+ (define (unifiable? p x) (pair? x))
(define (mk-struct->sexp v) v)]
[vector?
(define (recur v k)
(let ([v (vector->list v)])
(k (car v) (cdr v))))
(define (constructor v)
(compose list->vector cons))
+ (define (unifiable? v x) (vector? x))
(define (mk-struct->sexp v) v)]))
;; == SUBSTITUTIONS ============================================================
View
@@ -17,4 +17,10 @@
(fresh (x y)
(== (vector x 2) (vector 1 y))
(== q `(,x ,y))))
- `((1 2))))
+ `((1 2)))
+
+ (test-check "3"
+ (run* (q)
+ (== (vector 1 2) (list 1 2)))
+ `())
+ )
View
@@ -5,6 +5,12 @@
;; ---UNIFICATION--------------------------------------------------
+(define (unifiable-structs? u v)
+ (and (mk-struct? u)
+ (mk-struct? v)
+ (unifiable? u v)
+ (unifiable? v u)))
+
(define (unify e s)
(cond
((null? e) s)
@@ -19,8 +25,7 @@
((var? v)
(and (not (occurs-check v u s))
(unify e (ext-s v u s))))
- ((and (mk-struct? u)
- (mk-struct? v))
+ ((unifiable-structs? u v)
(recur u
(lambda (ua ud)
(recur v
@@ -31,24 +36,22 @@
;; ---GOAL---------------------------------------------------------
-(define == (lambda (u v) (goal-construct (==-c u v))))
-
-(define ==-c
- (lambda (u v)
- (lambdam@ (a : s c)
- (cond
- ((unify `((,u . ,v)) s)
- => (lambda (s^)
- ((update-prefix s s^) a)))
- (else #f)))))
-
-(define update-prefix
- (lambda (s s^)
- (let loop ((s^ s^))
- (cond
- ((eq? s s^) identitym)
- (else
- (composem
- (update-s (caar s^) (cdar s^))
- (loop (cdr s^))))))))
+(define (== u v) (goal-construct (==-c u v)))
+
+(define (==-c u v)
+ (lambdam@ (a : s c)
+ (cond
+ ((unify `((,u . ,v)) s)
+ => (lambda (s^)
+ ((update-prefix s s^) a)))
+ (else #f))))
+
+(define (update-prefix s s^)
+ (let loop ((s^ s^))
+ (cond
+ ((eq? s s^) identitym)
+ (else
+ (composem
+ (update-s (caar s^) (cdar s^))
+ (loop (cdr s^)))))))

0 comments on commit 29a4c92

Please sign in to comment.