[racket-dev] [plt] Push #27758: master branch updated

Oh, sorry for cc'ing dev. That was an accident.

Robby


On Tue, Nov 12, 2013 at 3:05 PM, Robby Findler
<robby at 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, <bfetscher at 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 <bfetscher at 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 <bfetscher at 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 , at new-dq-l) (list , at 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 , at ndql) (list , at ndqr)))]
>>        [`((list (name ,v1,(bound)) ,vs ...) (list ,t1 ,ts ...))
>>         (cond
>> -         [(member v1 params)
>> +         [(member v1 params)
>>            (loop `((list , at vs) (list , at 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 , at vs) (list , at 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 , at vs) (list , at 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)))))
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/dev/archive/attachments/20131112/5d3eaf0f/attachment-0001.html>