Oh, sorry for cc'ing dev. That was an accident. Robby
On Tue, Nov 12, 2013 at 3:05 PM, Robby Findler <ro...@eecs.northwestern.edu>wrote: > 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
