# HG changeset patch
# User wenzelm
# Date 1320706950 -3600
# Node ID e4e9394ddb0c97bdc9da0b441b33295c5fa71ac1
# Parent  fdc73782278f21ea1d796b35d655b9b4c70b60e0# Parent  35e378c11283090f1f15464b11c809c22704deb3
merged;

diff -r 35e378c11283 -r e4e9394ddb0c NEWS
--- a/NEWS	Mon Nov 07 23:03:52 2011 +0100
+++ b/NEWS	Tue Nov 08 00:02:30 2011 +0100
@@ -76,6 +76,11 @@
 a list and a nat.
 
 
+* Nitpick:
+  - Fixed infinite loop caused by the 'peephole_optim' option and affecting
+    'rat' and 'real'.
+
+
 *** FOL ***
 
 * New "case_product" attribute (see HOL).
diff -r 35e378c11283 -r e4e9394ddb0c src/HOL/Mutabelle/lib/Tools/mutabelle
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle	Mon Nov 07 23:03:52 2011 +0100
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Tue Nov 08 00:02:30 2011 +0100
@@ -94,7 +94,10 @@
   MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false) \"narrowing_no_finite_types\",
   MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false
     #> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ nat}])))) \"narrowing_nat\"
-(*  MutabelleExtra.nitpick_mtd *)
+(*
+, MutabelleExtra.refute_mtd,
+  MutabelleExtra.nitpick_mtd
+*)
 ]
 *}
 
@@ -124,11 +127,11 @@
 # make statistics
 
 function count() {
-  cat "$MUTABELLE_OUTPUT_PATH/log" | grep "$1: $2" | wc -l
+  cat "$MUTABELLE_OUTPUT_PATH/log" | grep "$1: $2" | wc -l | sed "s/     //"
 }
 
 function mk_stat() {
-  printf "%-40s : C: $(count $1 "GenuineCex") N: $(count $1 "NoCex") T: $(count $1 "Timeout") E: $(count $1 "Error")\n" "$1"
+  printf "%-40s C:$(count $1 "GenuineCex")  P:$(count $1 "PotentialCex")  N:$(count $1 "NoCex")  T:$(count $1 "Timeout")  D:$(count $1 "Donno")  E: $(count $1 "Error")\n" "$1"
 }
 
 mk_stat "quickcheck_random"
@@ -137,6 +140,7 @@
 mk_stat "quickcheck_narrowing"
 mk_stat "quickcheck_narrowing_no_finite_types"
 mk_stat "quickcheck_narrowing_nat"
+mk_stat "refute"
 mk_stat "nitpick"
 
 ## cleanup
diff -r 35e378c11283 -r e4e9394ddb0c src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Nov 07 23:03:52 2011 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Nov 08 00:02:30 2011 +0100
@@ -30,9 +30,7 @@
 *)
 val nitpick_mtd : mtd
 
-(*
 val refute_mtd : mtd
-*)
 
 val freezeT : term -> term
 val thms_of : bool -> theory -> thm list
@@ -175,25 +173,25 @@
 
 val sledgehammer_mtd = ("sledgehammer", invoke_sledgehammer)
 *)
-(*
+
 fun invoke_refute thy t =
   let
-    val res = MyRefute.refute_term thy [] t
+    val params = []
+    val res = Refute.refute_term (Proof_Context.init_global thy) params [] t
     val _ = Output.urgent_message ("Refute: " ^ res)
   in
-    case res of
+    (rpair []) (case res of
       "genuine" => GenuineCex
     | "likely_genuine" => GenuineCex
     | "potential" => PotentialCex
     | "none" => NoCex
     | "unknown" => Donno
-    | _ => Error
+    | _ => Error)
   end
-  handle MyRefute.REFUTE (loc, details) =>
+  handle Refute.REFUTE (loc, details) =>
          (error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^
                    "."))
 val refute_mtd = ("refute", invoke_refute)
-*)
 
 (** nitpick **)
 
diff -r 35e378c11283 -r e4e9394ddb0c src/HOL/Tools/Nitpick/nitpick_peephole.ML
--- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Mon Nov 07 23:03:52 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML	Tue Nov 08 00:02:30 2011 +0100
@@ -358,8 +358,6 @@
       (case (r1, r2) of
          (Join (r11, Rel x), _) =>
          if x = not3_rel then s_rel_eq r11 (s_not3 r2) else raise SAME ()
-       | (_, Join (r21, Rel x)) =>
-         if x = not3_rel then s_rel_eq r21 (s_not3 r1) else raise SAME ()
        | (RelIf (f, r11, r12), _) =>
          if inline_rel_expr r2 then
            s_formula_if f (s_rel_eq r11 r2) (s_rel_eq r12 r2)
diff -r 35e378c11283 -r e4e9394ddb0c src/HOL/Tools/Nitpick/nitpick_scope.ML
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Nov 07 23:03:52 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Nov 08 00:02:30 2011 +0100
@@ -446,6 +446,8 @@
       has_exact_card hol_ctxt facto finitizable_dataTs card_assigns T
     fun is_concrete facto =
       is_word_type T orelse
+      (* FIXME: looks wrong other types than just functions might be
+         abstract. *)
       xs |> maps (binder_types o snd) |> maps binder_types
          |> forall (has_exact_card hol_ctxt facto finitizable_dataTs
                                    card_assigns)