# HG changeset patch
# User blanchet
# Date 1320700917 -3600
# Node ID 20128348e9b95ab3a7872457973f497edab599cf
# Parent  13ab80eafd71ec4d6421a97bad77d8926d24c2af
revived Refute in Mutabelle

diff -r 13ab80eafd71 -r 20128348e9b9 src/HOL/Mutabelle/lib/Tools/mutabelle
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle	Mon Nov 07 17:54:38 2011 +0100
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Mon Nov 07 22:21:57 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 13ab80eafd71 -r 20128348e9b9 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Nov 07 17:54:38 2011 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Nov 07 22:21:57 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 **)