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

Bug fix for disequations

Browse Source 
Correctly eliminate dqs where the lhs is a parameter.
(Eliminate them if there is only one for a given parameter,
otherwise keep them.)

Also, add path compression for lvar lookup.
This commit is contained in:
Burke Fetscher 2013-11-11 16:11:39 -06:00
parent b982c4dd6c
commit 1b08b03262
1 changed files with 36 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -31,6 +31,7 @@
(struct-out unif-fail)
not-failed?
dq
dq-dq
predef-pat?
unique-name-nums
fresh-pat-vars
@ -317,23 +318,47 @@
(define (param-elim params unquantified-dq)
(let loop ([dq-rest unquantified-dq]
[ps params]
[new-dq-l '()]
[new-dq-r '()])
[new-dq-l '()]
[new-dq-r '()]
[lhs-ps (hash)])
(match dq-rest
['((list) (list))
(values ps `((list ,@new-dq-l) (list ,@new-dq-r)))]
['((list) (list))
(define-values
(ndql ndqr nps)
(for/fold ([ndql new-dq-l] [ndqr new-dq-r] [nps ps])
([(p lhss) (in-hash lhs-ps)])
(if ((length lhss) . > . 1)
(values (foldr cons ndql lhss)
(foldr cons ndqr (build-list (length lhss)
(λ (_) p)))
nps)
(values ndql
ndqr
(remove (list-ref p 1) nps)))))
(values nps `((list ,@ndql) (list ,@ndqr)))]
[`((list (name ,v1,(bound)) ,vs ...) (list ,t1 ,ts ...))
(cond
[(member v1 params)
[(member v1 params)
(loop `((list ,@vs) (list ,@ts))
(remove v1 ps)
new-dq-l
new-dq-r)]
new-dq-r
lhs-ps)]
[(match t1
[`(name ,tn ,(bound)) (member tn ps)]
[_ #f])
(loop `((list ,@vs) (list ,@ts))
ps
new-dq-l
new-dq-r
(hash-set lhs-ps t1 (cons `(name ,v1 ,(bound))
(hash-ref lhs-ps t1 '()))))]
[else
(loop `((list ,@vs) (list ,@ts))
ps
(cons `(name ,v1 ,(bound)) new-dq-l)
(cons t1 new-dq-r))])])))
(cons t1 new-dq-r)
lhs-ps)])])))
;; the "root" pats will be pats without names,
@ -738,7 +763,9 @@
(define res (hash-ref env (lvar id) (λ () #f)))
(match res
[(lvar new-id)
(lookup new-id env)]
(define-values (rep pat) (lookup new-id env))
(hash-set! env (lvar id) rep)
(values rep pat)]
[_
(values (lvar id) res)]))
@ -835,4 +862,4 @@
(define (make-uid id)
(let ([uid-num (unique-name-nums)])
(unique-name-nums (add1 uid-num))
(string->symbol (string-append (symbol->string id) "_" (number->string uid-num)))))
(string->symbol (string-append (symbol->string id) "_" (number->string uid-num)))))