suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

redex: refactor pattern unifier

Browse Source 
- swap mutable for immutable hashes represetning eqs
- most functions now return p*e pairing patterns with envs
This commit is contained in:
Burke Fetscher 2014-07-02 14:26:18 -05:00
parent 72a5e3949a
commit a1f7efc39d
5 changed files with 476 additions and 434 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
pkgs/redex-pkgs/redex-lib/redex/private/jdg-gen.rkt
View File

@ -21,7 +21,6 @@
;; pat->term lang pat* env env -> term ;; pat->term lang pat* env env -> term
(define (pat->term lang pat full-env [term-e (make-hash)]) (define (pat->term lang pat full-env [term-e (make-hash)])
(displayln (list 'pat->term lang pat))
(define nt-matchers (make-hash)) (define nt-matchers (make-hash))
(define eqs (env-eqs full-env)) (define eqs (env-eqs full-env))
(define (get-matcher nt) (define (get-matcher nt)

13
pkgs/redex-pkgs/redex-lib/redex/private/judgment-form.rkt
View File

@ -1479,7 +1479,7 @@
stx])) stx]))
(define-for-syntax (has-unsupported-pat? stx) (define-for-syntax (has-unsupported-pat? stx)
(syntax-case stx (repeat side-condition in-hole undatum-splicing) (syntax-case stx ()
[(repeat . rest) [(repeat . rest)
(and (identifier? #'repeat) (and (identifier? #'repeat)
(eq? (syntax-e #'repeat) 'repeat)) (eq? (syntax-e #'repeat) 'repeat))
@ -1492,8 +1492,15 @@
(and (identifier? #'in-hole) (and (identifier? #'in-hole)
(eq? (syntax-e #'in-hole) 'in-hole)) (eq? (syntax-e #'in-hole) 'in-hole))
#''(in-hole . rest)] #''(in-hole . rest)]
;; TODO check that s is quoted or a term [(undatum (variable-not-in (term . tr) (q/t s)))
[(undatum (variable-not-in (term . tr) . s)) (and (identifier? #'undatum)
(eq? (syntax-e #'undatum) 'undatum)
(identifier? #'variable-not-in)
(eq? (syntax-e #'variable-not-in) 'variable-not-in)
(identifier? #'q/t)
(or (eq? (syntax-e #'q/t) 'term)
(eq? (syntax-e #'q/t) 'quote)
(eq? (syntax-e #'q/t) 'quasiquote)))
#f] #f]
[(undatum . rest) [(undatum . rest)
(and (identifier? #'undatum) (and (identifier? #'undatum)

662
pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt
View File

@ -36,8 +36,8 @@
predef-pat? predef-pat?
unique-name-nums unique-name-nums
fresh-pat-vars fresh-pat-vars
make-uid) make-uid
p*e-eqs)
;; ;;
@ -136,24 +136,6 @@
cstr?)) cstr?))
(extracted-clauses->fns))) (extracted-clauses->fns)))
(define (bound-var? b)
(match b
[`(name ,(? var? name) ,(bound))
#t]
[_
#f]))
(define eqs/c
(hash/c lvar? (or/c lvar? pat*?)))
(define dq/c
(list/c (listof (or/c 'list bound-var?)) (listof (or/c 'list pat*?))))
(define dqs/c
(listof dq/c))
(define env/c
(struct/c env eqs/c dqs/c))
(define p*e/c
(struct/c p*e pat*? env/c))
;; used to track new equations for disunification ;; used to track new equations for disunification
(define new-eqs (make-parameter (make-hash))) (define new-eqs (make-parameter (make-hash)))
@ -161,31 +143,45 @@
;; disqequations generated (by mismatch-pattern) during a given unification pass ;; disqequations generated (by mismatch-pattern) during a given unification pass
(define dqs-found (make-parameter (make-hash))) (define dqs-found (make-parameter (make-hash)))
(define-syntax-rule
(maybe-let ([x e]) body ...)
(let ([val e])
(match val
[(unif-fail) val]
[_ (let ([x val]) body ...)])))
;; pat pat env -> (or/c p*e #f) (define-syntax maybe-let*
(syntax-rules ()
[(maybe-let* () body ...) (let () body ...)]
[(maybe-let* ([x x-e] [y e] ...) body ...)
(maybe-let ([x x-e])
(maybe-let* ([y e] ...) body ...))]))
(define-syntax-rule
(p*e-eqs x)
(env-eqs (p*e-e x)))
;; pat pat env lang -> (or/c p*e? unif-fail?)
(define (unify t u e L) (define (unify t u e L)
(parameterize ([dqs-found (make-hash)]) (parameterize ([dqs-found (make-hash)])
(define eqs (hash-copy (env-eqs e))) (maybe-let* ([t* (bind-names t e L)]
(define t* (bind-names t eqs L)) [u* (bind-names u (p*e-e t*) L)]
(define u* (bind-names u eqs L)) [res (unify* (p*e-p t*) (p*e-p u*) (p*e-e u*) L)])
(define res (and/fail (not-failed? t*) (define eqs (p*e-eqs res))
(not-failed? u*) (define res-pat (p*e-p res))
(unify* t* u* eqs L))) (define found-pre-dqs (apply set-union (set)
(and/fail (not-failed? res) (for/list ([dq-sides/id (hash-values (dqs-found))])
(let* ([static-eqs (hash/mut->imm eqs)] (list->dq-pairs dq-sides/id))))
[found-pre-dqs (maybe-let* ([found-dqs (for/fold ([fdqs '()])
(apply set-union (set) ([pdq (in-set found-pre-dqs)])
(for/list ([dq-sides/id (hash-values (dqs-found))]) (maybe-let* ([fdqs fdqs])
(list->dq-pairs dq-sides/id)))] (define new-dq (disunify* '() (first pdq) (second pdq) eqs L))
[found-dqs (and/fail new-dq
(for/list ([pdq found-pre-dqs]) (cons new-dq fdqs))))])
(disunify* '() (first pdq) (second pdq) static-eqs L))]) (define real-dqs (filter (λ (dq) (not (boolean? dq))) found-dqs))
(and/fail (for/and ([d found-dqs]) d) (define new-dqs (check-and-resimplify eqs (append real-dqs (env-dqs e)) L))
(let* ([real-dqs (filter (λ (dq) (not (boolean? dq))) found-dqs)]
[new-dqs (check-and-resimplify static-eqs (append real-dqs (env-dqs e)) L)])
(and/fail new-dqs (and/fail new-dqs
(p*e res (p*e res-pat (env eqs new-dqs)))))))
(env static-eqs new-dqs)))))))))
(define (list->dq-pairs dq-sides) (define (list->dq-pairs dq-sides)
(cond (cond
@ -197,28 +193,27 @@
(list (car dq-sides) rhs)) (list (car dq-sides) rhs))
(list->dq-pairs (cdr dq-sides)))])) (list->dq-pairs (cdr dq-sides)))]))
;; pat pat env lang -> (or/c env boolean?)
;; pat pat env lang -> (or/c env #f)
(define (disunify params t u e L) (define (disunify params t u e L)
(parameterize ([new-eqs (make-hash)]) (parameterize ([new-eqs (make-hash)])
(define eqs (hash-copy (env-eqs e))) (define t*e (bind-names t e L))
(define t* (bind-names t eqs L))
(define u* (bind-names u eqs L))
(define bn-eqs (hash/mut->imm eqs))
(cond (cond
[(or (unif-fail? t*) (unif-fail? u*)) [(unif-fail? t*e) e]
e]
[else [else
(define new-dq (disunify* params t* u* bn-eqs L)) (define u*e (bind-names u (p*e-e t*e) L))
(match new-dq (cond
[#f #f] [(unif-fail? u*e) e]
[#t [else
(env bn-eqs (define new-dq (disunify* params (p*e-p t*e) (p*e-p u*e) (env-eqs (p*e-e u*e)) L))
(env-dqs e))] (match new-dq
[_ [#f #f]
(env bn-eqs [#t
(cons new-dq (env (env-eqs (p*e-e u*e))
(env-dqs e)))])]))) (env-dqs e))]
[_
(env (env-eqs (p*e-e u*e))
(cons new-dq
(env-dqs e)))])])])))
(define base-dq `((list) (list))) (define base-dq `((list) (list)))
@ -240,7 +235,7 @@
(list ,@terms ,(resolve-no-nts/pat v eqs)))])]))) (list ,@terms ,(resolve-no-nts/pat v eqs)))])])))
(define (resolve-no-nts/var lv eqs) (define (resolve-no-nts/var lv eqs)
(define-values (rep pat) (lookup (lvar-id lv) eqs)) (define-values (rep pat _) (lookup (lvar-id lv) eqs))
(if (not (groundable? pat)) (if (not (groundable? pat))
`(name ,(lvar-id rep) ,(bound)) `(name ,(lvar-id rep) ,(bound))
(resolve-no-nts/pat pat eqs))) (resolve-no-nts/pat pat eqs)))
@ -270,12 +265,6 @@
[_ #t])) [_ #t]))
(define (hash/mut->imm h0)
(for/fold ([h (hash)])
([(k v) (in-hash h0)])
(hash-set h k v)))
;; eqs dqs -> dqs or #f ;; eqs dqs -> dqs or #f
;; simplified - first element in lhs of all inequations is a var not occuring in lhs of eqns ;; simplified - first element in lhs of all inequations is a var not occuring in lhs of eqns
(define (check-and-resimplify eqs dqs L) (define (check-and-resimplify eqs dqs L)
@ -301,30 +290,31 @@
[#t (loop ok rest)] [#t (loop ok rest)]
[_ (loop (cons new-dq ok) rest)])))])]))) [_ (loop (cons new-dq ok) rest)])))])])))
;; disunfy* pat* pat* eqs lang -> dq or boolean (dq is a pat*) ;; params pat* pat* eqs lang -> boolean or dq
(define (disunify* params u* t* static-eqs L) (define (disunify* params u* t* eqs L)
(define eqs (hash-copy static-eqs))
(parameterize ([new-eqs (make-hash)]) (parameterize ([new-eqs (make-hash)])
(let ([res (unify* u* t* eqs L)]) (define res (unify* u* t* (env eqs '()) L))
(cond (cond
[(unif-fail? res) #t] [(unif-fail? res) #t]
[(empty? (hash-keys (new-eqs))) #f] [(empty? (hash-keys (new-eqs))) #f]
[else [else
(define-values (new-ps new-dq) (define-values (new-ps new-dq)
(param-elim params (extend-dq (new-eqs) base-dq eqs))) (param-elim params (extend-dq (new-eqs) base-dq (env-eqs (p*e-e res)))))
(match new-dq (match new-dq
[`((list) (list)) [`((list) (list))
#f] #f]
[`((list (name ,var-ids ,(bound)) ...) (list ,pats ...)) [`((list (name, var-ids ,(bound)) ...) (list ,pats ...))
;; check to see if parameter elimination exposed some ;; check to see if parameter eliminations exposed some
;; equivalences... ;; equivalences...
(and (and
(or (equal? (length params) (length new-ps)) (or (equal? (length params) (length new-ps))
(for/and ([v (in-list var-ids)] [p (in-list pats)]) (for/and ([v (in-list var-ids)]
(or (not (hash-has-key? static-eqs (lvar v))) [p (in-list pats)])
(not (equal? (resolve-no-nts/pat `(name ,v ,(bound)) static-eqs) (or (not (hash-has-key? eqs (lvar v)))
p))))) (not (equal? (resolve-no-nts/pat `(name ,v ,(bound)) eqs)
(dq new-ps new-dq))])])))) p)))))
(dq new-ps new-dq))])])))
(define (param-elim params unquantified-dq) (define (param-elim params unquantified-dq)
(let loop ([dq-rest unquantified-dq] (let loop ([dq-rest unquantified-dq]
@ -376,61 +366,67 @@
;; which match both pat and pat*... ;; which match both pat and pat*...
;; (those are the ones bind-names does nothing with) ;; (those are the ones bind-names does nothing with)
;; bind-names : pat env lang -> pat* or unif-fail ;; pat env lang -> p*e or (unif-fail)
(define (bind-names pat e L) (define (bind-names pat e L)
(match pat (define eqs (env-eqs e))
[`(name ,name ,(bound)) (define dqs (env-dqs e))
(error 'bind-names "pat*, not a pat: ~s\n" pat)] (define res-pat
[`(name ,name ,pat) (let loop ([pat pat])
(define b-pat (bind-names pat e L)) (match pat
(and/fail (not-failed? b-pat) [`(name ,name ,(bound))
(let recur ([id name]) (error 'bind-names "pat*, not a pat: ~s" pat)]
(define res (hash-ref e (lvar id) (uninstantiated))) [`(name ,name ,pat)
(match res (maybe-let ([b-pat (loop pat)])
[(uninstantiated) (let recur ([id name])
(when (equal? b-pat (bound)) (define res (hash-ref eqs (lvar id) (uninstantiated)))
(error 'bind-names "tried to set something to bound")) (match res
(and/fail (not (occurs?* id b-pat e L)) [(uninstantiated)
(hash-set! e (lvar id) b-pat) (when (equal? b-pat (bound))
;; here we only bind to things in the LOCAL pattern (error 'bind-names "tried to set something to bound"))
;; so don't update new-eqs (and/fail (not (occurs?* id b-pat eqs L))
`(name ,name ,(bound)))] (set! eqs (hash-set eqs (lvar id) b-pat))
[(lvar id′) ;; here we only bind to things in the local pattern
(define next (recur id′)) ;; so don't update new-eqs
(match next `(name ,name ,(bound)))]
[`(name ,id-new ,(bound)) [(lvar new-id)
(unless (eq? id id-new) (define next (recur new-id))
;; path compression: don't update new-eqs here (match next
(hash-set! e (lvar id) (lvar id-new)))] [`(name ,id-new ,(bound))
[_ (void)]) (unless (eq? id id-new)
next] ;; path compression: don't update new-eqs here
[_ ;; some pat* (res is already bound) (set! eqs (hash-set eqs (lvar id) (lvar id-new))))]
(and/fail (not-failed? (unify-update* id b-pat res e L)) [_ (void)])
`(name ,id ,(bound)))])))] next]
[`(list ,pats ...) [_
(let/ec fail (maybe-let ([u-res (unify-update* id b-pat res (env eqs #f) L)])
`(list ,@(for/list ([p pats]) (set! eqs (p*e-eqs u-res))
(define res (bind-names p e L)) `(name ,id ,(bound)))])))]
(if (not-failed? res) [`(list ,pats ...)
res (let/ec fail
(fail (unif-fail))))))] `(list ,@(for/list ([p pats])
[`(variable-not-in ,p ,s) (define res (loop p))
(define pat (bind-names p e L)) (if (not-failed? res)
(and/fail (not-failed? pat) res
(let ([s-pat (bind-names s e L)]) (fail (unif-fail))))))]
(and/fail (not-failed? s-pat) [`(variable-not-in ,p ,s)
`(variable-not-in ,pat ,s-pat))))] (maybe-let* ([pat (loop p)]
[`(mismatch-name ,name ,p) [s-pat (loop s)])
(define b-pat (bind-names p e L)) `(variable-not-in ,pat ,s-pat))]
(and/fail (not-failed? b-pat) [`(mismatch-name ,name ,p)
`(mismatch-name ,name ,(bind-names p e L)))] (maybe-let ([b-pat (loop p)])
[_ pat])) `(mismatch-name ,name ,b-pat))]
[_ pat])))
(maybe-let ([res-pat res-pat])
(p*e res-pat (env eqs dqs))))
;; unify* : pat* pat* env lang -> pat* or unif-fail ;; unify* : pat* pat* env lang -> p*e? or unif-fail?
(define (unify* t0 u0 e L) (define (unify* t0 u0 e0 L)
(define t (resolve t0 e)) (define t*e (resolve t0 e0))
(define u (resolve u0 e)) (define u*e (resolve u0 (p*e-e t*e)))
(define t (p*e-p t*e))
(define u (p*e-p u*e))
(define e (p*e-e u*e))
#2dmatch #2dmatch
╔═════════════════╦═════════════════╦═════════════╦═══════════════╦═══════════╦══════╦════════════╦══════════════╦═══════════════════╦═════════╦══════════╦══════════════╦═════════════╗ ╔═════════════════╦═════════════════╦═════════════╦═══════════════╦═══════════╦══════╦════════════╦══════════════╦═══════════════════╦═════════╦══════════╦══════════════╦═════════════╗
║ u ║ `(mismatch-name ║ `(name ║ `(cstr ║`(nt ,n-u) ║`any ║ (? num-ty?)║`(list ║ (? pvar?) ║ `string ║ `boolean ║ (? base-ty?) ║(? not-pair?)║ ║ u ║ `(mismatch-name ║ `(name ║ `(cstr ║`(nt ,n-u) ║`any ║ (? num-ty?)║`(list ║ (? pvar?) ║ `string ║ `boolean ║ (? base-ty?) ║(? not-pair?)║
@ -452,26 +448,26 @@
║ ║ ║ n-t n-u ║ ║ ║ ║ ║ n-t n-u ║ ║
║ ║ ║ e L) ║ ║ ║ ║ ║ e L) ║ ║
╠═════════════════╣ ╚═══════════╬════════════════════════════════════════════════════════════════════════════════════════════════════════╣ ╠═════════════════╣ ╚═══════════╬════════════════════════════════════════════════════════════════════════════════════════════════════════╣
║ `any ║ ║ u ║ ║ `any ║ ║ (p*e u e) ║
║ ║ ║ ║ ║ ║ ║ ║
╠═════════════════╣ ╚══════╦════════════╦══════════════════════════════════════════════════════════════════════╦═════════════╣ ╠═════════════════╣ ╚══════╦════════════╦══════════════════════════════════════════════════════════════════════╦═════════════╣
║ (? num-ty?) ║ ║(u*-2nums ║ ║ ║ ║ (? num-ty?) ║ ║(u*-2nums ║ ║ ║
║ ║ ║ t u) ║ ║ ║ ║ ║ ║ t u e) ║ ║ ║
╠═════════════════╣ ╚════════════╬══════════════╗ ║ ║ ╠═════════════════╣ ╚════════════╬══════════════╗ ║ ║
║ `(list ,ts ...) ║ ║(u*-2lsts ║ (unif-fail) ║ ║ ║ `(list ,ts ...) ║ ║(u*-2lsts ║ (unif-fail) ║ ║
║ ║ ║ ts us e L) ║ ║(u*-matches? ║ ║ ║ ║ ts us e L) ║ ║(u*-matches? ║
╠═════════════════╣ ╚══════════════╬═══════════════════╗ ║ t u ║ ╠═════════════════╣ ╚══════════════╬═══════════════════╗ ║ t u ║
║ (? pvar?) ║ ║(u*-2pvars u t e L)║ ║ e L) ║ ║ (? pvar?) ║ ║(u*-2pvars u t e L)║ ║ e L) ║
╠═════════════════╣ ╚═══════════════════╬═════════╗ ║ ║ ╠═════════════════╣ ╚═══════════════════╬═════════╗ ║ ║
║ `string ║ (unify* u t e L) ║ t ║ ║ ║ ║ `string ║ (unify* u t e L) ║(p*e t e)║ ║ ║
╠═════════════════╣ ╚═════════╬══════════╗ ║ ║ ╠═════════════════╣ ╚═════════╬══════════╗ ║ ║
║ `boolean ║ ║ t ║ ║ ║ ║ `boolean ║ ║(p*e t e) ║ ║ ║
╠═════════════════╣ ╚══════════╬══════════════╣ ║ ╠═════════════════╣ ╚══════════╬══════════════╣ ║
║ (? base-ty?) ║ ║ t ║ ║ ║ (? base-ty?) ║ ║ (p*e t e) ║ ║
╠═════════════════╣ ╚══════════════╬═════════════╣ ╠═════════════════╣ ╚══════════════╬═════════════╣
║ (? not-pair?) ║ ║(and/fail ║ ║ (? not-pair?) ║ ║(and/fail ║
║ ║ ║ (equal? t u)║ ║ ║ ║ (equal? t u)║
║ ║ ║ t) ║ ║ ║ ║ (p*e t e)) ║
╚═════════════════╩══════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╩═════════════╝) ╚═════════════════╩══════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╩═════════════╝)
(define (pvar? x) (or (vnom? x) (define (pvar? x) (or (vnom? x)
@ -491,37 +487,45 @@
(match-lambda [`(variable-not-in ,e ,s) #t] (match-lambda [`(variable-not-in ,e ,s) #t]
[_ #f])) [_ #f]))
;; pvar? pvar? env lang -> (or/c p*e? unif-fail?)
(define (u*-2pvars v1 v2 e L) (define (u*-2pvars v1 v2 e L)
#2dmatch (define res
╔══════════════════════════╦══════════════════════════╦════════════════════════════════╦═══════════════════════════════╦════════════════╦══════════════════════════════════════╗ (begin
║ v1 ║`(variable-prefix ,p1) ║ `(variable-except ,e1 ... ) ║ (? vnom?) ║ `variable ║`(variable-not-in ,e1 ,s) ║ #2dmatch
║ v2 ║ ║ ║ ║ ║ ║ ╔══════════════════════════╦══════════════════════════╦════════════════════════════════╦═══════════════════════════════╦════════════════╦══════════════════════════════════════╗
╠══════════════════════════╬══════════════════════════╬════════════════════════════════╬═══════════════════════════════╬════════════════╬══════════════════════════════════════╣ ║ v1 ║`(variable-prefix ,p1) ║ `(variable-except ,e1 ... ) ║ (? vnom?) ║ `variable ║`(variable-not-in ,e1 ,s) ║
║ ║ (cond ║ (and/fail ║(u*-2pvars ║ ║(and/fail ║ ║ v2 ║ ║ ║ ║ ║ ║
║ `(variable-prefix ,p2) ║ [(sym-pref? p1 p2) ║ (not (ormap ║ v2 ║ ║ (sym-pref? p2 s) ║ ╠══════════════════════════╬══════════════════════════╬════════════════════════════════╬═══════════════════════════════╬════════════════╬══════════════════════════════════════╣
║ ║ `(variable-prefix ,p2)]║ (curry sym-pref? p2) ║ `(variable-except ║ ║ v1) ║ ║ ║ (cond ║ (and/fail ║(u*-2pvars ║ ║(and/fail ║
║ ║ [(sym-pref? p2 p1) ║ e1)) ║ ,@(compiled-lang-literals L)) ║ ║ ║ ║ `(variable-prefix ,p2) ║ [(sym-pref? p1 p2) ║ (not (ormap ║ v2 ║ ║ (sym-pref? p2 s) ║
║ ║ `(variable-prefix ,p1)]║ v2) ║ e L) ║ ║ ║ ║ ║ `(variable-prefix ,p2)]║ (curry sym-pref? p2) ║ `(variable-except ║ ║ v1) ║
║ ║ [else (unif-fail)]) ║ ║ ║ ║ ║ ║ ║ [(sym-pref? p2 p1) ║ e1)) ║ ,@(compiled-lang-literals L)) ║ ║ ║
╠══════════════════════════╬══════════════════════════╬════════════════════════════════╣ ║ ╠══════════════════════════════════════╣ ║ ║ `(variable-prefix ,p1)]║ v2) ║ e L) ║ ║ ║
║ ║ ║ `(variable-except ║ ║ ║`(variable-not-in ║ ║ ║ [else (unif-fail)]) ║ ║ ║ ║ ║
║ `(variable-except ║ ║ ,@(de-dupe/sorted ║ ║ v2 ║ (list ,e1 ,@e2) ║ ╠══════════════════════════╬══════════════════════════╬════════════════════════════════╣ ║ ╠══════════════════════════════════════╣
║ ,e2 ...) ║ ║ (merge/sorted e1 e2))) ║ ║ ║ ,s) ║ ║ ║ ║ `(variable-except ║ ║ ║`(variable-not-in ║
║ ║ ║ ║ ║ ║ ║ ║ `(variable-except ║ ║ ,@(de-dupe/sorted ║ ║ v2 ║ (list ,e1 ,@e2) ║
╠══════════════════════════╣ ╚════════════════════════════════╬═══════════════════════════════╣ ╠══════════════════════════════════════╣ ║ ,e2 ...) ║ ║ (merge/sorted e1 e2))) ║ ║ ║ ,s) ║
║ ║ ║ ║ ║(u*-2pvars v1 ║ ║ ║ ║ ║ ║ ║ ║
║ (? vnom?) ║ ║ v1 ║ ║`(variable-except ║ ╠══════════════════════════╣ ╚════════════════════════════════╬═══════════════════════════════╣ ╠══════════════════════════════════════╣
║ ║ ║ ║ ║ ,@(compiled-lang-literals L)) ║ ║ ║ ║ ║ ║(u*-2pvars v1 ║
║ ║ ║ ║ ║ e L) ║ ║ (? vnom?) ║ ║ v1 ║ ║`(variable-except ║
╠══════════════════════════╣ (u*-2pvars v2 v1 e L) ╚═══════════════════════════════╣ ╠══════════════════════════════════════╣ ║ ║ ║ ║ ║ ,@(compiled-lang-literals L)) ║
║ ║ ║ ║ ║ ║ ║ ║ ║ ║ e L) ║
║ `variable ║ ║ ║ v1 ║ ╠══════════════════════════╣ (u*-2pvars v2 v1 e L) ╚═══════════════════════════════╣ ╠══════════════════════════════════════╣
║ ║ ║ ║ ║ ║ ║ ║ ║ ║
╠══════════════════════════╣ ╚════════════════╬══════════════════════════════════════╣ ║ `variable ║ ║ ║ v1 ║
║ ║ ║ ║ ║ ║ ║ ║ ║
║ `(variable-not-in ,e2 ,t)║ ║ (2-vnis v1 v2 e L) ║ ╠══════════════════════════╣ ╚════════════════╬══════════════════════════════════════╣
║ ║ ║ ║ ║ ║ ║ ║
╚══════════════════════════╩════════════════════════════════════════════════════════════════════════════════════════════════════════════╩══════════════════════════════════════╝) ║ `(variable-not-in ,e2 ,t)║ ║ (2-vnis v1 v2 e L) ║
║ ║ ║ ║
╚══════════════════════════╩════════════════════════════════════════════════════════════════════════════════════════════════════════════╩══════════════════════════════════════╝))
(match res
[(unif-fail) res]
[(p*e _ _) res]
[_ (p*e res e)]))
(define (2-vnis v1 v2 e L) (define (2-vnis v1 v2 e L)
(match-define `(variable-not-in ,e1 ,s1) v1) (match-define `(variable-not-in ,e1 ,s1) v1)
@ -529,9 +533,9 @@
(cond (cond
[(not (and (symbol? s1) (symbol? s2))) [(not (and (symbol? s1) (symbol? s2)))
(displayln (list s1 s2)) (displayln (list s1 s2))
(define s-res (unify* s1 s2 e L)) (maybe-let ([s-res (unify* s1 s2 e L)])
(and/fail s-res (p*e `(variable-not-in (list ,e1 ,e2) ,(p*e-p s-res))
`(variable-not-in (list ,e1 ,e2) ,s-res))] (p*e-e s-res)))]
[(sym-pref? s1 s2) [(sym-pref? s1 s2)
`(variable-not-in (list ,e1 ,e2) s2)] `(variable-not-in (list ,e1 ,e2) s2)]
[(sym-pref? s2 s1) [(sym-pref? s2 s1)
@ -544,116 +548,131 @@
(symbol->string s))) (symbol->string s)))
(define (u*-2cstrs nts1 p1 nts2 p2 e L) (define (u*-2cstrs nts1 p1 nts2 p2 e L)
(let ([res (unify* p1 p2 e L)] (maybe-let ([res (unify* p1 p2 e L)])
[new-nts (merge-ids/sorted nts1 nts2 L)]) (define res-p (p*e-p res))
(and/fail (not-failed? res) (define new-nts (merge-ids/sorted nts1 nts2 L))
new-nts (and/fail new-nts
(when (lvar? res) (when (lvar? res-p)
(error 'unify* "unify* returned lvar as result: ~s\n~s\n~s\n" p1 p2 e)) (error 'unify* "unify* returned lvar as result: ~s\n~s\n~s\n" p1 p2 e))
`(cstr ,new-nts ,res)))) (p*e `(cstr ,new-nts ,res-p) (p*e-e res)))))
(define (u*-1cstr nts p u e L) (define (u*-1cstr nts p u e L)
(let ([res (unify* p u e L)]) (maybe-let ([res (unify* p u e L)])
(and/fail (not-failed? res) (define res-p (p*e-p res))
(match res (define res-e (p*e-e res))
[(lvar id) (match res-p
(error 'unify* "unify* returned lvar as result: ~s\n~s\n~s\n" p u e)] [(lvar id)
[`(nt ,nt) (error 'unify* "unify* returned lvar as result: ~s\n~s\n~s\n" p u e)]
(define new-nts (merge-ids/sorted (list nt) nts L)) [`(nt ,nt)
(and/fail new-nts (define new-nts (merge-ids/sorted (list nt) nts L))
`(cstr ,new-nts ,p))] (and/fail new-nts
[`(cstr ,nts2 ,new-p) (p*e `(cstr ,new-nts ,p) res-e))]
(define new-nts (merge-ids/sorted nts nts2 L)) [`(cstr ,nts2 ,new-p)
(and/fail new-nts (define new-nts (merge-ids/sorted nts nts2 L))
`(cstr ,new-nts ,new-p))] (and/fail new-nts
[_ (p*e `(cstr ,new-nts ,new-p) res-e))]
(and/fail (for/and ([n nts]) (check-nt n L res)) [_
`(cstr ,nts ,res))])))) (and/fail (for/and ([n nts]) (check-nt n L res-p))
(p*e `(cstr ,nts ,res-p) res-e))])))
(define (u*-2nts n-t n-u e L) (define (u*-2nts n-t n-u e L)
(if (equal? n-t n-u) (if (equal? n-t n-u)
`(nt ,n-t) (p*e `(nt ,n-t) e)
(u*-1nt n-t `(nt ,n-u) e L))) (u*-1nt n-t `(nt ,n-u) e L)))
(define (u*-1nt p u e L) (define (u*-1nt p u e L)
(and/fail (and/fail
(check-nt p L u) (check-nt p L u)
(if (hash-has-key? (compiled-lang-collapsible-nts L) p) (if (hash-has-key? (compiled-lang-collapsible-nts L) p)
(let ([p-bn (bind-names (fresh-pat-vars (hash-ref (compiled-lang-collapsible-nts L) p) (make-hash)) e L)]) (maybe-let ([bn-res (bind-names (fresh-pat-vars (hash-ref (compiled-lang-collapsible-nts L) p) (make-hash)) e L)])
(and/fail (unify* (p*e-p bn-res) u (p*e-e bn-res) L))
(not-failed? p-bn) ;; removed a unification of u with itself here
(unify* p-bn u e L))) (p*e `(cstr (,p) ,u) e))))
(let ([res (unify* u u e L)]) ;; look at structure of nt here?
(and/fail (not-failed? res)
(when (lvar? res)
(error 'unify* "unify* returned lvar as result: ~s\n~s\n~s\n" u u e))
`(cstr (,p) ,res))))))
(define (u*-2lsts ts us e L) (define (u*-2lsts ts us e L)
(and/fail (= (length ts) (length us)) (and/fail (= (length ts) (length us))
(let/ec fail (maybe-let ([res-ps-e
`(list ,@(for/list ([t ts] [u us]) (let loop ([ts ts]
(let ([res (unify* t u e L)]) [us us]
(if (not-failed? res) [e e]
res [rs '()])
(fail (unif-fail))))))))) (if (empty? ts)
(cons rs e)
(maybe-let ([res (unify* (car ts) (car us) e L)])
(loop (cdr ts)
(cdr us)
(p*e-e res)
(cons (p*e-p res) rs)))))])
(p*e `(list ,@(reverse (car res-ps-e)))
(cdr res-ps-e)))))
(define (u*-2nums t u) (define (u*-2nums t u e)
(cond (p*e
[(number-superset? t u) u] (cond
[(number-superset? u t) t])) [(number-superset? t u) u]
[(number-superset? u t) t])
e))
(define (u*-matches? t u e L) (define (u*-matches? t u e L)
(match* (t u) (maybe-let ([pat-res
[((? num-ty? t) _) (match* (t u)
(and/fail ((number-pred t) u) [((? num-ty? t) _)
u)] (and/fail ((number-pred t) u)
[(`variable-not-otherwise-mentioned (? symbol? s)) u)]
(and/fail (not (memq s (compiled-lang-literals L))) [(`variable-not-otherwise-mentioned (? symbol? s))
(not (base-ty? s)) (and/fail (not (memq s (compiled-lang-literals L)))
s)] (not (base-ty? s))
[(`(variable-except ,ss ...) (? symbol? s)) s)]
(and/fail (not (memq s ss)) [(`(variable-except ,ss ...) (? symbol? s))
u)] (and/fail (not (memq s ss))
[(`(variable-prefix ,pref) (? symbol? s)) u)]
(and/fail (regexp-match [(`(variable-prefix ,pref) (? symbol? s))
(regexp (string-append "^" (symbol->string pref) ".*$")) (and/fail (regexp-match
(symbol->string s)) (regexp (string-append "^" (symbol->string pref) ".*$"))
u)] (symbol->string s))
[(`variable (? symbol? s)) u)]
(and/fail (not (base-ty? s)) [(`variable (? symbol? s))
s)] (and/fail (not (base-ty? s))
[(`string (? string? s)) s)]
s] [(`string (? string? s))
[(`boolean (? boolean? b)) s]
b] [(`boolean (? boolean? b))
[(_ _) (unif-fail)])) b]
[(_ _) (unif-fail)])])
(p*e pat-res e)))
(define (resolve pat env) (define (resolve pat e)
(match pat (define e-eqs (env-eqs e))
[`(name ,id ,(bound)) (define-values (res-pat eqz)
(define id-rep (lvar-id (lookup-rep id env))) (let loop ([pat pat]
(match (hash-ref env (lvar id-rep)) [eqs e-eqs])
[`(name ,next-id ,(bound)) (match pat
(hash-set! env (lvar id) (lvar next-id)) [`(name ,id ,(bound))
(resolve `(name ,next-id ,(bound)) env)] (define-values (rep eqs2) (lookup-rep id eqs))
[_ (define id-rep (lvar-id rep))
`(name ,id-rep ,(bound))])] (match (hash-ref eqs2 (lvar id-rep))
[_ pat])) [`(name ,next-id ,(bound))
(loop `(name ,next-id ,(bound)) (hash-set eqs2 (lvar id) (lvar next-id)))]
[_
(values `(name ,id-rep ,(bound)) eqs2)])]
[_ (values pat eqs)])))
(p*e res-pat (struct-copy env e [eqs eqz])))
;; unify-update* : id pat* pat* env lang -> pat* or #f ;; id pat* pat* env lang -> p*e? or unif-fail?
(define (unify-update* id pat-1 pat-2 e L) (define (unify-update* id pat-1 pat-2 e L)
(let ([u-res (unify* pat-1 pat-2 e L)]) (maybe-let ([u-res (unify* pat-1 pat-2 e L)])
(and/fail (not (occurs?* id pat-1 e L)) (define res-e (p*e-e u-res))
(not (occurs?* id pat-2 e L)) (define res-eqs (env-eqs res-e))
(when (not-failed? u-res) (define res-p (p*e-p u-res))
(when (equal? u-res (bound)) (error 'update "tried to set something to bound")) (and/fail (not (occurs?* id pat-1 res-eqs L))
(unless (equal? u-res (hash-ref e (lvar id) (uninstantiated))) (not (occurs?* id pat-2 res-eqs L))
(hash-set! e (lvar id) u-res) (when (equal? u-res (bound))
(unless (or (nt-only-pat? u-res) (error 'update "tried to set something to bound"))
(ground-pat-eq? pat-1 pat-2)) (unless (equal? u-res (hash-ref res-eqs (lvar id) (uninstantiated)))
(hash-set! (new-eqs) (lvar id) u-res)))) (unless (or (nt-only-pat? res-p)
u-res))) (ground-pat-eq? pat-1 pat-2))
(hash-set! (new-eqs) (lvar id) res-p)))
(p*e res-p (struct-copy env res-e [eqs (hash-set res-eqs (lvar id) res-p)])))))
(define (nt-only-pat? p*) (define (nt-only-pat? p*)
(match p* (match p*
@ -673,50 +692,55 @@
;; we only need to look at the id in name, and the pattern it is bound to ;; we only need to look at the id in name, and the pattern it is bound to
;; TODO: replace name in p*'s with lvar - this is the most obvious of many ;; TODO: replace name in p*'s with lvar - this is the most obvious of many
;; functions that would be improved by this ;; functions that would be improved by this
(define (occurs?* name p e L) (define (occurs?* name p eqs L)
(match p (match p
[`(name ,name-p ,(bound)) [`(name ,name-p ,(bound))
(or (eq? name name-p) (or (eq? name name-p)
(occurs?* name (hash-ref e (lvar name-p) (uninstantiated)) e L))] (occurs?* name (hash-ref eqs (lvar name-p) (uninstantiated)) eqs L))]
[`(list ,ps ...) [`(list ,ps ...)
(for/or ([p ps]) (for/or ([p ps])
(occurs?* name p e L))] (occurs?* name p eqs L))]
[`(cstr (,nts ...) ,pat) [`(cstr (,nts ...) ,pat)
(occurs?* name pat e L)] (occurs?* name pat eqs L)]
[(lvar id) [(lvar id)
(or (eq? name id) (or (eq? name id)
(occurs?* name (hash-ref e (lvar id) (uninstantiated)) e L))] (occurs?* name (hash-ref eqs (lvar id) (uninstantiated)) eqs L))]
[`(cstr ,(lvar _)) [`(cstr ,(lvar _))
(error 'occurs?* "rogue lvar: ~s\n" p)] (error 'occurs?* "rogue lvar: ~s\n" p)]
[_ #f])) [_ #f]))
(define (instantiate* id pat e L) (define (instantiate* id pat e L)
(define id-pat (resolve (lookup-pat id e) e)) (define-values (p eqs2) (lookup-pat id (env-eqs e)))
(match id-pat (define id-res (resolve p (struct-copy env e [eqs eqs2])))
[`(name ,next-id ,(bound)) (define e-res (p*e-e id-res))
(and/fail (not-failed? (instantiate* next-id pat e L)) (define id-pat (p*e-p id-res))
(not (occurs?* id (lvar next-id) e L)) (define e-eqs (p*e-eqs id-res))
(hash-set! e (lvar id) (lvar next-id)) (match* (id-pat pat)
`(name ,next-id ,(bound)))] [(`(name ,next-id ,(bound)) _)
[_ (maybe-let ([n-res (instantiate* next-id pat e-res L)])
(match pat (define n-eqs (p*e-eqs n-res))
[`(name ,id-2 ,(bound)) (and/fail (not (occurs?* id (lvar next-id) n-eqs L))
(cond (p*e `(name ,next-id ,(bound))
[(eq? id id-2) (struct-copy env e
pat] [eqs (hash-set n-eqs (lvar id) (lvar next-id))]))))]
[else [(_ `(name ,id-2 ,(bound)))
(define id-2-pat (resolve (lookup-pat id-2 e) e)) (cond
(define res (unify-update* id id-pat id-2-pat e L)) [(eq? id id-2) (p*e pat e)]
(and/fail (not-failed? res) [else
(not (occurs?* id-2 (lvar id) e L)) (define-values (p2 eqsp2) (lookup-pat id-2 e-eqs))
(hash-set! e (lvar id-2) (lvar id)) (define id-2-res (resolve p2 (struct-copy env e-res [eqs eqsp2])))
(unless (ground-pat-eq? id-pat id-2-pat) (define id-2-pat (p*e-p id-2-res))
(hash-set! (new-eqs) (lvar id-2) (lvar id))) (maybe-let ([res (unify-update* id id-pat id-2-pat (p*e-e id-2-res) L)])
`(name ,id ,(bound)))])] (define e-res (p*e-e res))
[_ (and/fail (not (occurs?* id-2 (lvar id) (env-eqs e-res) L))
(and/fail (not-failed? (unify-update* id id-pat pat e L)) (unless (ground-pat-eq? id-pat id-2-pat)
`(name ,id ,(bound)))])])) (hash-set! (new-eqs) (lvar id-2) (lvar id)))
(p*e `(name ,id ,(bound))
(struct-copy env e
[eqs (hash-set (env-eqs e-res) (lvar id-2) (lvar id))]))))])]
[(_ _)
(maybe-let ([res (unify-update* id id-pat pat e L)])
(p*e `(name ,id ,(bound)) (p*e-e res)))]))
;; we want to consider ground pats that are equal ;; we want to consider ground pats that are equal
;; modulo constraints as equal when disunifying (see uses) ;; modulo constraints as equal when disunifying (see uses)
@ -792,38 +816,38 @@
'(any number string natural integer real boolean '(any number string natural integer real boolean
variable variable-not-otherwise-mentioned))) variable variable-not-otherwise-mentioned)))
(define (lookup-pat id env) (define (lookup-pat id eqs)
(define-values (_ pat) (lookup id env)) (define-values (_ pat new-eqs) (lookup id eqs))
pat) (values pat new-eqs))
(define (lookup-rep id env) (define (lookup-rep id eqs)
(define-values (rep _) (lookup id env)) (define-values (rep _ new-eqs) (lookup id eqs))
rep) (values rep new-eqs))
(define (lookup id env) (define (lookup id eqs)
(define res (hash-ref env (lvar id) (λ () #f))) (let loop ([id id])
(match res (define res (hash-ref eqs (lvar id)
[(lvar new-id) (λ () (error 'lookup "unbound var: ~a" id))))
(define-values (rep pat) (lookup new-id env)) (match res
(hash-set! env (lvar id) rep) [(lvar new-id)
(values rep pat)] (define-values (rep pat new-eqs) (loop new-id))
[_ (values rep pat (hash-set new-eqs (lvar id) rep))]
(values (lvar id) res)])) [_
(values (lvar id) res eqs)])))
(provide check-nt (provide check-nt
normalize-pat) normalize-pat)
(define check-nt (define check-nt
(let ([memo (hash)]) (let ([memo (make-hash)])
(λ (nt clang pat) (λ (nt clang pat)
(define npat (normalize-pat clang pat)) (define npat (normalize-pat clang pat))
(hash-ref memo (list nt clang npat) (hash-ref memo (list nt clang npat)
(λ () (λ ()
(define pat-ok? (define pat-ok?
(for/or ([ntp (in-list (map ((curry normalize-pat) clang) (nt-pats nt clang)))]) (for/or ([ntp (in-list (map ((curry normalize-pat) clang) (nt-pats nt clang)))])
(not-failed? (unify* npat ntp #f empty-lang)))) (not-failed? (unify* npat ntp empty-env empty-lang))))
(set! memo (hash-set! memo (list nt clang npat) pat-ok?)
(hash-set memo (list nt clang npat) pat-ok?))
pat-ok?))))) pat-ok?)))))
(define (normalize-pat lang pat) (define (normalize-pat lang pat)

6
pkgs/redex-pkgs/redex-lib/redex/private/search.rkt
View File

@ -243,15 +243,15 @@
(define (check-depth-limits bound tr-loc fails) (define (check-depth-limits bound tr-loc fails)
(when ((pushdown-count) . > . (pushdown-limit)) (when ((pushdown-count) . > . (pushdown-limit))
(define str (format "pushdown count of ~s exceeded at ~s" (pushdown-count) tr-loc)) (define str (format "pushdown count of ~s exceeded at ~s" (pushdown-count) tr-loc))
(printf "!*\n\t~s\t*!\n" str) ;(printf "!*\n\t~s\t*!\n" str)
(raise (make-exn:fail:redex:search-failure str (current-continuation-marks) fails))) (raise (make-exn:fail:redex:search-failure str (current-continuation-marks) fails)))
(when (> (bt-count) (bt-limit)) (when (> (bt-count) (bt-limit))
(define str (format "backtrack count of ~s exceeded at ~s" (bt-limit) tr-loc)) (define str (format "backtrack count of ~s exceeded at ~s" (bt-limit) tr-loc))
(displayln str) ;(displayln str)
(raise (make-exn:fail:redex:search-failure str (current-continuation-marks) fails))) (raise (make-exn:fail:redex:search-failure str (current-continuation-marks) fails)))
(when (> (length tr-loc) (* 3 (+ (length tr-loc) bound))) (when (> (length tr-loc) (* 3 (+ (length tr-loc) bound)))
(define str (format "depth bound exceeded at depth: ~s" (length tr-loc))) (define str (format "depth bound exceeded at depth: ~s" (length tr-loc)))
(displayln str) ;(displayln str)
(raise (make-exn:fail:redex:search-failure str (current-continuation-marks) fails)))) (raise (make-exn:fail:redex:search-failure str (current-continuation-marks) fails))))

220
pkgs/redex-pkgs/redex-test/redex/tests/unify-tests.rkt
View File

@ -236,23 +236,21 @@
(define (unify*/format p1 p2 eqs L) (define (unify*/format p1 p2 eqs L)
(define e eqs) (define e (env eqs '()))
(define e2 (hash-copy eqs)) (define res (unify*/lt p1 p2 e L))
(define res-p (unify*/lt p1 p2 e L)) (define res-bkwd (unify*/lt p2 p1 e L))
(define res-p-bkwd (unify*/lt p2 p1 e2 L))
(cond (cond
[(and (not-failed? res-p) [(and (not-failed? res)
(not-failed? res-p-bkwd) (not-failed? res-bkwd)
(p*e-equivalent? (p*e res-p (env e '())) (p*e-equivalent? res res-bkwd eqs))
(p*e res-p-bkwd (env e2 '())) eqs)) res]
res-p] [(and (unif-fail? res)
[(and (unif-fail? res-p) (unif-fail? res-bkwd))
(unif-fail? res-p-bkwd))
#f] #f]
[else [else
(list 'different-orders=>different-results (list 'different-orders=>different-results
res-p res
res-p-bkwd)])) res-bkwd)]))
;; This looks really strange but it is for backwards compatability ;; This looks really strange but it is for backwards compatability
;; with tests that didn't take nonterminal productions into account. ;; with tests that didn't take nonterminal productions into account.
@ -304,35 +302,42 @@
(check-equal? (unify #t '(name x any) (env (hash) '()) #f) (check-equal? (unify #t '(name x any) (env (hash) '()) #f)
(p*e `(name x ,(bound)) (p*e `(name x ,(bound))
(env (hash (lvar 'x) #t) '()))) (env (hash (lvar 'x) #t) '())))
(check-equal? (unify* #t 'any (hash) #f) (check-equal? (unify* #t 'any (env (hash) '()) #f)
#t) (p*e #t (env (hash) '())))
(check-equal? (unify* #f 'any (hash) #f) (check-equal? (unify* #f 'any (env (hash) '()) #f)
#f) (p*e #f (env (hash) '())))
(check-equal? (unify* #t 'any (hash) #f) (check-equal? (unify* #t 'any (env (hash) '()) #f)
#t) (p*e #t (env (hash) '())))
(check-equal? (unify* #f 'number (hash) #f) (check-equal? (unify* #f 'number (env (hash) '()) #f)
(unif-fail)) (unif-fail))
(check-equal? (unify* '(list 1) 1 (hash) #f) (check-equal? (unify* '(list 1) 1 (env (hash) '()) #f)
(unif-fail)) (unif-fail))
(check-equal? (unify* 'boolean #t (hash) #f) (check-equal? (unify* 'boolean #t (env (hash) '()) #f)
#t) (p*e #t (env (hash) '())))
(check-equal? (unify* 'boolean #f (hash) #f) (check-equal? (unify* 'boolean #f (env (hash) '()) #f)
#f) (p*e #f (env (hash) '())))
(check-equal? (unify* 'number #f (hash) #f) (check-equal? (unify* 'number #f (env (hash) '()) #f)
(unif-fail)) (unif-fail))
(check-equal? (unify* 'integer #f (hash) #f) (check-equal? (unify* 'integer #f (env (hash) '()) #f)
(unif-fail)) (unif-fail))
(check-equal? (unify* 'natural #f (hash) #f) (check-equal? (unify* 'natural #f (env (hash) '()) #f)
(unif-fail)) (unif-fail))
(check-equal? (unify* 'real #f (hash) #f) (check-equal? (unify* 'real #f (env (hash) '()) #f)
(unif-fail)) (unif-fail))
(check-equal? (unify* 'string #f (hash) #f) (check-equal? (unify* 'string #f (env (hash) '()) #f)
(unif-fail)) (unif-fail))
(check-equal? (unify* 'variable #f (hash) #f) (check-equal? (unify* 'variable #f (env (hash) '()) #f)
(unif-fail)) (unif-fail))
(check-equal? (unify* 'variable-not-otherwise-mentioned #f (hash) #f) (check-equal? (unify* 'variable-not-otherwise-mentioned #f (env (hash) '()) #f)
(unif-fail)) (unif-fail))
(define (p-eqs-equal? a b)
(check-equal?
(cons (p*e-p a)
(p*e-eqs a))
(cons (p*e-p b)
(p*e-eqs b))))
(define-syntax (unify-all/results stx) (define-syntax (unify-all/results stx)
(syntax-case stx () (syntax-case stx ()
[(_ lhs eqs ([rhs res res-eqs] rest ...)) [(_ lhs eqs ([rhs res res-eqs] rest ...))
@ -348,7 +353,7 @@
(unify-all/results lhs eqs (rest ...)))] (unify-all/results lhs eqs (rest ...)))]
[(_ lhs eqs ([rhs res] rest ...)) [(_ lhs eqs ([rhs res] rest ...))
#'(begin #'(begin
(check-equal? (unify/format lhs rhs eqs L0) (p-eqs-equal? (unify/format lhs rhs eqs L0)
res) res)
(unify-all/results lhs eqs (rest ...)))] (unify-all/results lhs eqs (rest ...)))]
[(_ lhs eqs ()) [(_ lhs eqs ())
@ -542,21 +547,28 @@
['(variable-prefix b) #f])) ['(variable-prefix b) #f]))
(define-syntax-rule
(check-pat-equal? a b)
(check-equal? (let ([ans a])
(match ans
[(p*e p _) p]
[_ ans]))
b))
(check-equal? (unify*/lt `(nt v) `(cstr (e) (list (nt e) (nt v))) (hash) L0) (check-pat-equal? (unify*/lt `(nt v) `(cstr (e) (list (nt e) (nt v))) empty-env L0)
`(cstr (e v) (list (nt e) (nt v)))) `(cstr (e v) (list (nt e) (nt v))))
(check-equal? (unify*/lt `(cstr (e) (list (nt e) (nt v))) `(nt v) (hash) L0) (check-pat-equal? (unify*/lt `(cstr (e) (list (nt e) (nt v))) `(nt v) empty-env L0)
`(cstr (e v) (list (nt e) (nt v)))) `(cstr (e v) (list (nt e) (nt v))))
(check-equal? (unify*/lt `(cstr (e) (list (nt e) (nt v))) 5 (hash) L0) (check-pat-equal? (unify*/lt `(cstr (e) (list (nt e) (nt v))) 5 empty-env L0)
(unif-fail)) (unif-fail))
(check-equal? (unify*/lt `(cstr (e) (list (nt e) (nt v))) `(list (nt e) (nt v)) (hash) L0) (check-pat-equal? (unify*/lt `(cstr (e) (list (nt e) (nt v))) `(list (nt e) (nt v)) empty-env L0)
`(cstr (e) (list (nt e) (nt v)))) `(cstr (e) (list (nt e) (nt v))))
(check-equal? (unify*/lt `(cstr (e) number) `(cstr (v) natural) (hash) L0) (check-pat-equal? (unify*/lt `(cstr (e) number) `(cstr (v) natural) empty-env L0)
`(cstr (e v) natural)) `(cstr (e v) natural))
(check-equal? (unify*/lt `(cstr (e) (list number variable)) `(cstr (e) number) (hash) L0) (check-pat-equal? (unify*/lt `(cstr (e) (list number variable)) `(cstr (e) number) empty-env L0)
(unif-fail)) (unif-fail))
(check-equal? (unify*/lt `(cstr (e) (list number variable-not-otherwise-mentioned)) (check-pat-equal? (unify*/lt `(cstr (e) (list number variable-not-otherwise-mentioned))
`(cstr (e) (list integer variable)) (hash) L0) `(cstr (e) (list integer variable)) empty-env L0)
`(cstr (e) (list integer variable-not-otherwise-mentioned))) `(cstr (e) (list integer variable-not-otherwise-mentioned)))
@ -564,55 +576,55 @@
(syntax-case stx () (syntax-case stx ()
[(_ lhs eqs ([rhs res res-eqs] ...)) [(_ lhs eqs ([rhs res res-eqs] ...))
#'(begin #'(begin
(let ([h eqs]) (let ([pe (unify*/format lhs rhs eqs L0)])
(check-equal? (unify*/format lhs rhs h L0) res) (check-equal? (p*e-p pe) res)
(check-equal? h res-eqs)) ...)])) (check-equal? (env-eqs (p*e-e pe)) res-eqs)) ...)]))
(unify*-all/results (unify*-all/results
`(cstr (e) (nt q)) (make-hash) `(cstr (e) (nt q)) (hash)
(['any `(cstr (e q) any) (make-hash)] (['any `(cstr (e q) any) (hash)]
['integer `(cstr (e q) integer) (make-hash)] ['integer `(cstr (e q) integer) (hash)]
['natural `(cstr (e q) natural) (make-hash)] ['natural `(cstr (e q) natural) (hash)]
['number `(cstr (e q) number) (make-hash)] ['number `(cstr (e q) number) (hash)]
['real `(cstr (e q) real) (make-hash)] ['real `(cstr (e q) real) (hash)]
['string `(cstr (e q) string) (make-hash)] ['string `(cstr (e q) string) (hash)]
[`boolean `(cstr (e q) boolean) (make-hash)] [`boolean `(cstr (e q) boolean) (hash)]
['variable `(cstr (e q) variable) (make-hash)] ['variable `(cstr (e q) variable) (hash)]
['variable-not-otherwise-mentioned ['variable-not-otherwise-mentioned
`(cstr (e q) variable-not-otherwise-mentioned) (make-hash)] `(cstr (e q) variable-not-otherwise-mentioned) (hash)]
['(variable-except a) ['(variable-except a)
`(cstr (e q) (variable-except a)) (make-hash)] `(cstr (e q) (variable-except a)) (hash)]
['(variable-prefix a) ['(variable-prefix a)
`(cstr (e q) (variable-prefix a)) (make-hash)] `(cstr (e q) (variable-prefix a)) (hash)]
['(list 1 2 3) ['(list 1 2 3)
'(cstr (e q) (list 1 2 3)) (make-hash)] '(cstr (e q) (list 1 2 3)) (hash)]
[5 '(cstr (e q) 5) (make-hash)] [5 '(cstr (e q) 5) (hash)]
["a string" '(cstr (e q) "a string") (make-hash)] ["a string" '(cstr (e q) "a string") (hash)]
['(mismatch-name x 5) '(cstr (e q) 5) (make-hash)])) ['(mismatch-name x 5) '(cstr (e q) 5) (hash)]))
(unify*-all/results (unify*-all/results
`(name x ,(bound)) (make-hash `((,(lvar 'x) . any))) `(name x ,(bound)) (hash (lvar 'x) 'any)
(['any `(name x ,(bound)) (make-hash `((,(lvar 'x) . any)))] (['any `(name x ,(bound)) (hash (lvar 'x) 'any)]
[5 `(name x ,(bound)) (make-hash `((,(lvar 'x) . 5)))] [5 `(name x ,(bound)) (hash (lvar 'x) 5)]
['number `(name x ,(bound)) (make-hash `((,(lvar 'x) . number)))] ['number `(name x ,(bound)) (hash (lvar 'x) 'number)]
['integer `(name x ,(bound)) (make-hash `((,(lvar 'x) . integer)))] ['integer `(name x ,(bound)) (hash (lvar 'x) 'integer)]
['natural `(name x ,(bound)) (make-hash `((,(lvar 'x) . natural)))] ['natural `(name x ,(bound)) (hash (lvar 'x) 'natural)]
['real `(name x ,(bound)) (make-hash `((,(lvar 'x) . real)))] ['real `(name x ,(bound)) (hash (lvar 'x) 'real)]
['string `(name x ,(bound)) (make-hash `((,(lvar 'x) . string)))] ['string `(name x ,(bound)) (hash (lvar 'x) 'string)]
['boolean `(name x ,(bound)) (make-hash `((,(lvar 'x) . boolean)))] ['boolean `(name x ,(bound)) (hash (lvar 'x) 'boolean)]
['variable `(name x ,(bound)) (make-hash `((,(lvar 'x) . variable)))] ['variable `(name x ,(bound)) (hash (lvar 'x) 'variable)]
['variable-not-otherwise-mentioned `(name x ,(bound)) (make-hash `((,(lvar 'x) . variable-not-otherwise-mentioned)))] ['variable-not-otherwise-mentioned `(name x ,(bound)) (hash (lvar 'x) 'variable-not-otherwise-mentioned)]
['(variable-except a) `(name x ,(bound)) (make-hash `((,(lvar 'x) . (variable-except a))))] ['(variable-except a) `(name x ,(bound)) (hash (lvar 'x) '(variable-except a))]
['(variable-prefix a) `(name x ,(bound)) (make-hash `((,(lvar 'x) . (variable-prefix a))))] ['(variable-prefix a) `(name x ,(bound)) (hash (lvar 'x) '(variable-prefix a))]
['(cstr (n) any) `(name x ,(bound)) (make-hash `((,(lvar 'x) . (cstr (n) any))))] ['(cstr (n) any) `(name x ,(bound)) (hash (lvar 'x) '(cstr (n) any))]
['(list 1 2) `(name x ,(bound)) (make-hash `((,(lvar 'x) . (list 1 2))))] ['(list 1 2) `(name x ,(bound)) (hash (lvar 'x) '(list 1 2))]
['(mismatch-name z any) `(name x ,(bound)) (make-hash `((,(lvar 'x) . any)))] ['(mismatch-name z any) `(name x ,(bound)) (hash (lvar 'x) 'any)]
['(nt q) `(name x ,(bound)) (make-hash `((,(lvar 'x) . (cstr (q) any))))])) ['(nt q) `(name x ,(bound)) (hash (lvar 'x) '(cstr (q) any))]))
(unify*-all/results (unify*-all/results
`(name x ,(bound)) (make-hash `((,(lvar 'x) . any) (,(lvar 'y) . variable))) `(name x ,(bound)) (hash (lvar 'x) 'any (lvar 'y) 'variable)
([`(name x ,(bound)) `(name x ,(bound)) (make-hash `((,(lvar 'x) . any) (,(lvar 'y) . variable)))] ([`(name x ,(bound)) `(name x ,(bound)) (hash (lvar 'x) 'any (lvar 'y) 'variable)]
[`(name y ,(bound)) `(name x ,(bound)) (make-hash `((,(lvar 'y) . ,(lvar 'x)) (,(lvar 'x) . variable)))])) [`(name y ,(bound)) `(name x ,(bound)) (hash (lvar 'y) (lvar 'x) (lvar 'x) 'variable)]))
(let () (let ()
@ -765,16 +777,13 @@
(lvar 'n_1) (lvar 'n_2)))) (lvar 'n_1) (lvar 'n_2))))
(check-not-false (let ([h (make-hash)]) (check-not-false (bind-names 'any empty-env L0))
(bind-names 'any h L0))) (check-equal? (bind-names `(name x any) empty-env L0)
(check-equal? (let ([h (make-hash)]) (p*e `(name x ,(bound))
(list (bind-names `(name x any) h L0) (env (hash (lvar 'x) 'any) '())))
h)) (check-equal? (let ([h (hash (lvar 'x) (lvar 'y)
(list `(name x ,(bound)) (lvar 'y) 'any)])
(make-hash (list (cons (lvar 'x) 'any))))) (bind-names `(list (name x 5) (name y 6)) (env h '()) L0))
(check-equal? (let ([h (make-hash (list (cons (lvar 'x) (lvar 'y))
(cons (lvar 'y) 'any)))])
(bind-names `(list (name x 5) (name y 6)) h L0))
(unif-fail)) (unif-fail))
(define-syntax do-unify (define-syntax do-unify
@ -815,8 +824,11 @@
(n O (n O
(S n))) (S n)))
(check-equal? (unify*/lt '(cstr (n) (list S O)) '(list S O) (hash) U-nums) (define (m-env . eqs)
'(cstr (n) (list S O))) (env (apply hash eqs) '()))
(check-pat-equal? (unify*/lt '(cstr (n) (list S O)) '(list S O) empty-env U-nums)
'(cstr (n) (list S O)))
(u-succeeds U-nums (S O) (S O) (hash)) (u-succeeds U-nums (S O) (S O) (hash))
(u-succeeds U-nums (S (S O)) (S n) (hash)) (u-succeeds U-nums (S (S O)) (S n) (hash))
(u-fails U-nums (S (S O)) (S n) (m-hash (lvar 'n) '(list O))) (u-fails U-nums (S (S O)) (S n) (m-hash (lvar 'n) '(list O)))
@ -955,32 +967,32 @@
(disunify* '() (disunify* '()
`(list (name x_1 ,(bound))) `(list (name x_1 ,(bound)))
`(list (name x_2 ,(bound))) `(list (name x_2 ,(bound)))
(make-hash `((,(lvar 'x_1) . a) (hash (lvar 'x_1) 'a
(,(lvar 'x_2) . a))) (lvar 'x_2) 'a)
L0)) L0))
(check-not-false (check-not-false
(disunify* '() (disunify* '()
`(list (name x_1 ,(bound))) `(list (name x_1 ,(bound)))
`(list (name x_2 ,(bound))) `(list (name x_2 ,(bound)))
(make-hash `((,(lvar 'x_1) . (nt x)) (hash (lvar 'x_1) '(nt x)
(,(lvar 'x_2) . a))) (lvar 'x_2) 'a)
L0)) L0))
(check-not-false (check-not-false
(disunify* '() (disunify* '()
`(list (name x_1 ,(bound))) `(list (name x_1 ,(bound)))
`(list (name x_2 ,(bound))) `(list (name x_2 ,(bound)))
(make-hash `((,(lvar 'x_1) . (nt x)) (hash (lvar 'x_1) '(nt x)
(,(lvar 'x_2) . (nt x)))) (lvar 'x_2) '(nt x))
L0)) L0))
(check-false (check-false
(disunify* '() 'a '(cstr (s) a) (make-hash) L0)) (disunify* '() 'a '(cstr (s) a) (hash) L0))
(check-false (check-false
(let ([h (make-hash (list (cons (lvar 'a2) 'a)))]) (disunify* '() `(name a2 ,(bound)) '(cstr (s) a) (hash (lvar 'a2) 'a) L0))
(disunify* '() `(name a2 ,(bound)) '(cstr (s) a) h L0)))
(check-false (check-false
(let ([h (make-hash (list (cons (lvar 'a2) 'a) (disunify* '() `(name a2 ,(bound)) `(name s6 ,(bound))
(cons (lvar 's6) '(cstr (s) a))))]) (hash (lvar 'a2) 'a
(disunify* '() `(name a2 ,(bound)) `(name s6 ,(bound)) h L0))) (lvar 's6) '(cstr (s) a))
L0))
(define (make-eqs eqs) (define (make-eqs eqs)
(for/hash ([eq eqs]) (for/hash ([eq eqs])