<div dir="ltr">TEST CASES!!!<div><br></div><div>(my throat is hoarse.)</div><div><br></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><br></div><div>It is really really easy to make incorrect test cases when you've already got the bugfix in hand.</div><div><br></div><div>Robby</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">
On Tue, Nov 12, 2013 at 2:58 PM,  <span dir="ltr"><<a href="mailto:bfetscher@racket-lang.org" target="_blank">bfetscher@racket-lang.org</a>></span> wrote:<br><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.<br>
  <a href="http://git.racket-lang.org/plt/b982c4dd6c..8b17d99d44" target="_blank">http://git.racket-lang.org/plt/b982c4dd6c..8b17d99d44</a><br>
<br>
=====[ 2 Commits ]======================================================<br>
Directory summary:<br>
 100.0% pkgs/redex-pkgs/redex-lib/redex/private/<br>
<br>
~~~~~~~~~~<br>
<br>
1b08b03 Burke Fetscher <<a href="mailto:bfetscher@racket-lang.org">bfetscher@racket-lang.org</a>> 2013-11-11 16:11<br>
:<br>
| Bug fix for disequations<br>
|<br>
| Correctly eliminate dqs where the lhs is a parameter.<br>
| (Eliminate them if there is only one for a given parameter,<br>
| otherwise keep them.)<br>
|<br>
| Also, add path compression for lvar lookup.<br>
:<br>
  M .../redex-lib/redex/private/pat-unify.rkt         | 45 ++++++++++++++++----<br>
<br>
~~~~~~~~~~<br>
<br>
8b17d99 Burke Fetscher <<a href="mailto:bfetscher@racket-lang.org">bfetscher@racket-lang.org</a>> 2013-11-12 14:55<br>
:<br>
| Disunification bug fix.<br>
|<br>
| After parameter elimination, check the results to<br>
| make sure some pre-existing equality hasn't been<br>
| reproduced.<br>
:<br>
  M .../redex-lib/redex/private/pat-unify.rkt         | 28 +++++++++++++-------<br>
<br>
=====[ Overall Diff ]===================================================<br>
<br>
pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt<br>
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~<br>
--- OLD/pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt<br>
+++ NEW/pkgs/redex-pkgs/redex-lib/redex/private/pat-unify.rkt<br>
@@ -31,12 +31,14 @@<br>
          (struct-out unif-fail)<br>
          not-failed?<br>
          dq<br>
+         dq-dq<br>
          predef-pat?<br>
          unique-name-nums<br>
          fresh-pat-vars<br>
          make-uid)<br>
<br>
<br>
+<br>
 ;;<br>
 ;; atom := `any | `number | `string | `integer | `boolean | `real | `variable | `variable-not-otherwise-mentioned<br>
 ;; var  := symbol?<br>
@@ -176,7 +178,7 @@<br>
                                (list->dq-pairs dq-sides/id)))]<br>
                      [found-dqs<br>
                       (for/list ([pdq found-pre-dqs])<br>
-                        (disunify* '() (first pdq) (second pdq) (hash-copy static-eqs) L))])<br>
+                        (disunify* '() (first pdq) (second pdq) static-eqs L))])<br>
                 (and/fail (for/and ([d found-dqs]) d)<br>
                           (let* ([real-dqs (filter (λ (dq) (not (boolean? dq))) found-dqs)]<br>
                                  [new-dqs (check-and-resimplify static-eqs (append real-dqs (env-dqs e)) L)])<br>
@@ -201,19 +203,19 @@<br>
     (define eqs (hash-copy (env-eqs e)))<br>
     (define t* (bind-names t eqs L))<br>
     (define u* (bind-names u eqs L))<br>
+    (define bn-eqs (hash/mut->imm eqs))<br>
     (cond<br>
       [(or (unif-fail? t*) (unif-fail? u*))<br>
        e]<br>
       [else<br>
-       (define bn-eqs (hash-copy eqs))<br>
-       (define new-dq (disunify* params t* u* eqs L))<br>
+       (define new-dq (disunify* params t* u* bn-eqs L))<br>
        (match new-dq<br>
          [#f #f]<br>
          [#t<br>
-          (env (hash/mut->imm bn-eqs)<br>
+          (env bn-eqs<br>
                (env-dqs e))]<br>
          [_<br>
-          (env (hash/mut->imm bn-eqs)<br>
+          (env bn-eqs<br>
                (cons new-dq<br>
                      (env-dqs e)))])])))<br>
<br>
@@ -292,14 +294,15 @@<br>
       [else<br>
        (match notok<br>
          [`(,(dq ps `(,vars-p* ,term-p*)) ,rest ...)<br>
-          (let ([new-dq (disunify* ps vars-p* term-p* (hash-copy eqs) L)])<br>
+          (let ([new-dq (disunify* ps vars-p* term-p* eqs L)])<br>
             (and new-dq<br>
                  (match new-dq<br>
                    [#t (loop ok rest)]<br>
                    [_ (loop (cons new-dq ok) rest)])))])])))<br>
<br>
 ;; disunfy* pat* pat* eqs lang -> dq or boolean (dq is a pat*)<br>
-(define (disunify* params u* t* eqs L)<br>
+(define (disunify* params u* t* static-eqs L)<br>
+  (define eqs (hash-copy static-eqs))<br>
   (parameterize ([new-eqs (make-hash)])<br>
     (let ([res (unify* u* t* eqs L)])<br>
       (cond<br>
@@ -311,29 +314,61 @@<br>
          (match new-dq<br>
            [`((list) (list))<br>
             #f]<br>
-           [_<br>
-            (dq new-ps new-dq)])]))))<br>
+           [`((list (name ,var-ids ,(bound)) ...) (list ,pats ...))<br>
+            ;; check to see if parameter elimination exposed some<br>
+            ;; equivalences...<br>
+            (and<br>
+             (or (equal? (length params) (length new-ps))<br>
+                 (for/and ([v (in-list var-ids)] [p (in-list pats)])<br>
+                   (or (not (hash-has-key? static-eqs (lvar v)))<br>
+                       (not (equal? (resolve-no-nts/pat `(name ,v ,(bound)) static-eqs)<br>
+                                    p)))))<br>
+             (dq new-ps new-dq))])]))))<br>
<br>
 (define (param-elim params unquantified-dq)<br>
   (let loop ([dq-rest unquantified-dq]<br>
              [ps params]<br>
-             [new-dq-l '()]<br>
-             [new-dq-r '()])<br>
+             [new-dq-l '()]<br>
+             [new-dq-r '()]<br>
+             [lhs-ps (hash)])<br>
     (match dq-rest<br>
-      ['((list) (list))<br>
-       (values ps `((list ,@new-dq-l) (list ,@new-dq-r)))]<br>
+      ['((list) (list))<br>
+       (define-values<br>
+         (ndql ndqr nps)<br>
+         (for/fold ([ndql new-dq-l] [ndqr new-dq-r] [nps ps])<br>
+           ([(p lhss) (in-hash lhs-ps)])<br>
+           (if ((length lhss) . > . 1)<br>
+               (values (foldr cons ndql lhss)<br>
+                       (foldr cons ndqr (build-list (length lhss)<br>
+                                                    (λ (_) p)))<br>
+                       nps)<br>
+               (values ndql<br>
+                       ndqr<br>
+                       (remove (list-ref p 1) nps)))))<br>
+       (values nps `((list ,@ndql) (list ,@ndqr)))]<br>
       [`((list (name ,v1,(bound)) ,vs ...) (list ,t1 ,ts ...))<br>
        (cond<br>
-         [(member v1 params)<br>
+         [(member v1 params)<br>
           (loop `((list ,@vs) (list ,@ts))<br>
                 (remove v1 ps)<br>
                 new-dq-l<br>
-                new-dq-r)]<br>
+                new-dq-r<br>
+                lhs-ps)]<br>
+         [(match t1<br>
+            [`(name ,tn ,(bound)) (member tn ps)]<br>
+            [_ #f])<br>
+          (loop `((list ,@vs) (list ,@ts))<br>
+                ps<br>
+                new-dq-l<br>
+                new-dq-r<br>
+                (hash-set lhs-ps t1 (cons `(name ,v1 ,(bound))<br>
+                                          (hash-ref lhs-ps t1 '()))))]<br>
          [else<br>
           (loop `((list ,@vs) (list ,@ts))<br>
                 ps<br>
                 (cons `(name ,v1 ,(bound)) new-dq-l)<br>
-                (cons t1 new-dq-r))])])))<br>
+                (cons t1 new-dq-r)<br>
+                lhs-ps)])])))<br>
<br>
<br>
 ;; the "root" pats will be pats without names,<br>
@@ -738,7 +773,9 @@<br>
   (define res (hash-ref env (lvar id) (λ () #f)))<br>
   (match res<br>
     [(lvar new-id)<br>
-     (lookup new-id env)]<br>
+     (define-values (rep pat) (lookup new-id env))<br>
+     (hash-set! env (lvar id) rep)<br>
+     (values rep pat)]<br>
     [_<br>
      (values (lvar id) res)]))<br>
<br>
@@ -835,4 +872,4 @@<br>
 (define (make-uid id)<br>
   (let ([uid-num (unique-name-nums)])<br>
     (unique-name-nums (add1 uid-num))<br>
-    (string->symbol (string-append (symbol->string id) "_" (number->string uid-num)))))<br>
\ No newline at end of file<br>
+    (string->symbol (string-append (symbol->string id) "_" (number->string uid-num)))))<br>
</blockquote></div><br></div>