<div dir="ltr">Oh, sorry for cc'ing dev. That was an accident.<div> </div><div>Robby</div></div><div class="gmail_extra"> <div class="gmail_quote">On Tue, Nov 12, 2013 at 3:05 PM, Robby Findler <<a href="mailto:robby@eecs.northwestern.edu" target="_blank">robby@eecs.northwestern.edu</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">TEST CASES!!!<div> </div><div>(my throat is hoarse.)</div><div> </div><div>What you should really do is revert these commits (locally), develop good automated test cases that fail properly and then revert the revert and then see if they pass.</div> <div> </div><div>It is really really easy to make incorrect test cases when you've already got the bugfix in hand.</div><div> </div><div>Robby</div></div> <div class="HOEnZb"><div class="h5"><div class="gmail_extra"> <div class="gmail_quote"> On Tue, Nov 12, 2013 at 2:58 PM, <<a href="mailto:bfetscher@racket-lang.org" target="_blank">bfetscher@racket-lang.org</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> bfetscher has updated `master' from b982c4dd6c to 8b17d99d44. <a href="http://git.racket-lang.org/plt/b982c4dd6c..8b17d99d44" target="_blank">http://git.racket-lang.org/plt/b982c4dd6c..8b17d99d44</a> =====[ 2 Commits ]====================================================== Directory summary: 100.0% pkgs/redex-pkgs/redex-lib/redex/private/ ~~~~~~~~~~ 1b08b03 Burke Fetscher <<a href="mailto:bfetscher@racket-lang.org" target="_blank">bfetscher@racket-lang.org</a>> 2013-11-11 16:11 : | Bug fix for disequations | | 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. : M .../redex-lib/redex/private/pat-unify.rkt | 45 ++++++++++++++++---- ~~~~~~~~~~ 8b17d99 Burke Fetscher <<a href="mailto:bfetscher@racket-lang.org" target="_blank">bfetscher@racket-lang.org</a>> 2013-11-12 14:55 : | Disunification bug fix. | | After parameter elimination, check the results to | make sure some pre-existing equality hasn't been | reproduced. : M .../redex-lib/redex/private/pat-unify.rkt | 28 +++++++++++++------- =====[ Overall Diff ]=================================================== pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ --- OLD/pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt +++ NEW/pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt @@ -31,12 +31,14 @@ (struct-out unif-fail) not-failed? dq + dq-dq predef-pat? unique-name-nums fresh-pat-vars make-uid) + ;; ;; atom := `any | `number | `string | `integer | `boolean | `real | `variable | `variable-not-otherwise-mentioned ;; var := symbol? @@ -176,7 +178,7 @@ (list->dq-pairs dq-sides/id)))] [found-dqs (for/list ([pdq found-pre-dqs]) - (disunify* '() (first pdq) (second pdq) (hash-copy static-eqs) L))]) + (disunify* '() (first pdq) (second pdq) static-eqs L))]) (and/fail (for/and ([d found-dqs]) d) (let* ([real-dqs (filter (λ (dq) (not (boolean? dq))) found-dqs)] [new-dqs (check-and-resimplify static-eqs (append real-dqs (env-dqs e)) L)]) @@ -201,19 +203,19 @@ (define eqs (hash-copy (env-eqs e))) (define t* (bind-names t eqs L)) (define u* (bind-names u eqs L)) + (define bn-eqs (hash/mut->imm eqs)) (cond [(or (unif-fail? t*) (unif-fail? u*)) e] [else - (define bn-eqs (hash-copy eqs)) - (define new-dq (disunify* params t* u* eqs L)) + (define new-dq (disunify* params t* u* bn-eqs L)) (match new-dq [#f #f] [#t - (env (hash/mut->imm bn-eqs) + (env bn-eqs (env-dqs e))] [_ - (env (hash/mut->imm bn-eqs) + (env bn-eqs (cons new-dq (env-dqs e)))])]))) @@ -292,14 +294,15 @@ [else (match notok [`(,(dq ps `(,vars-p* ,term-p*)) ,rest ...) - (let ([new-dq (disunify* ps vars-p* term-p* (hash-copy eqs) L)]) + (let ([new-dq (disunify* ps vars-p* term-p* eqs L)]) (and new-dq (match new-dq [#t (loop ok rest)] [_ (loop (cons new-dq ok) rest)])))])]))) ;; disunfy* pat* pat* eqs lang -> dq or boolean (dq is a pat*) -(define (disunify* params u* t* eqs L) +(define (disunify* params u* t* static-eqs L) + (define eqs (hash-copy static-eqs)) (parameterize ([new-eqs (make-hash)]) (let ([res (unify* u* t* eqs L)]) (cond @@ -311,29 +314,61 @@ (match new-dq [`((list) (list)) #f] - [_ - (dq new-ps new-dq)])])))) + [`((list (name ,var-ids ,(bound)) ...) (list ,pats ...)) + ;; check to see if parameter elimination exposed some + ;; equivalences... + (and + (or (equal? (length params) (length new-ps)) + (for/and ([v (in-list var-ids)] [p (in-list pats)]) + (or (not (hash-has-key? static-eqs (lvar v))) + (not (equal? (resolve-no-nts/pat `(name ,v ,(bound)) static-eqs) + p))))) + (dq new-ps new-dq))])])))) (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 +773,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 +872,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))))) \ No newline at end of file + (string->symbol (string-append (symbol->string id) "_" (number->string uid-num))))) </blockquote></div> </div> </div></div></blockquote></div> </div>