avoid infinite recursion in peephole optimizer function -- this had a debilitating effect on rationals and reals
authorblanchet
Mon Nov 07 22:22:01 2011 +0100 (2011-11-07)
changeset 453987dbb7b044a11
parent 45397 20128348e9b9
child 45399 fdc73782278f
avoid infinite recursion in peephole optimizer function -- this had a debilitating effect on rationals and reals
NEWS
src/HOL/Tools/Nitpick/nitpick_peephole.ML
     1.1 --- a/NEWS	Mon Nov 07 22:21:57 2011 +0100
     1.2 +++ b/NEWS	Mon Nov 07 22:22:01 2011 +0100
     1.3 @@ -76,6 +76,11 @@
     1.4  a list and a nat.
     1.5  
     1.6  
     1.7 +* Nitpick:
     1.8 +  - Fixed infinite loop caused by the 'peephole_optim' option and affecting
     1.9 +    'rat' and 'real'.
    1.10 +
    1.11 +
    1.12  *** FOL ***
    1.13  
    1.14  * New "case_product" attribute (see HOL).
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Mon Nov 07 22:21:57 2011 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Mon Nov 07 22:22:01 2011 +0100
     2.3 @@ -358,8 +358,6 @@
     2.4        (case (r1, r2) of
     2.5           (Join (r11, Rel x), _) =>
     2.6           if x = not3_rel then s_rel_eq r11 (s_not3 r2) else raise SAME ()
     2.7 -       | (_, Join (r21, Rel x)) =>
     2.8 -         if x = not3_rel then s_rel_eq r21 (s_not3 r1) else raise SAME ()
     2.9         | (RelIf (f, r11, r12), _) =>
    2.10           if inline_rel_expr r2 then
    2.11             s_formula_if f (s_rel_eq r11 r2) (s_rel_eq r12 r2)