TEST CASES!!! (my throat is hoarse.)
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. It is really really easy to make incorrect test cases when you've already got the bugfix in hand. Robby On Tue, Nov 12, 2013 at 2:58 PM, <bfetsc...@racket-lang.org> wrote: > bfetscher has updated `master' from b982c4dd6c to 8b17d99d44. > http://git.racket-lang.org/plt/b982c4dd6c..8b17d99d44 > > =====[ 2 Commits ]====================================================== > Directory summary: > 100.0% pkgs/redex-pkgs/redex-lib/redex/private/ > > ~~~~~~~~~~ > > 1b08b03 Burke Fetscher <bfetsc...@racket-lang.org> 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 <bfetsc...@racket-lang.org> 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))))) >
_________________________ Racket Developers list: http://lists.racket-lang.org/dev
