# HG changeset patch
# User blanchet
# Date 1342815586 -7200
# Node ID 4bacc8983b3d50636c5eea85010ba070390e59cf
# Parent  b86450f5b5cb427e01fdf72212b2917d92749bf2
learn from SMT proofs when they can be minimized by Metis

diff -r b86450f5b5cb -r 4bacc8983b3d src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Jul 20 22:19:46 2012 +0200
@@ -367,7 +367,7 @@
       handle List.Empty => error "No ATP available."
     fun get_prover name =
       (name, Sledgehammer_Minimize.get_minimizing_prover ctxt
-                Sledgehammer_Provers.Normal (K ()) name)
+                Sledgehammer_Provers.Normal (K (K ())) name)
   in
     (case AList.lookup (op =) args proverK of
       SOME name => get_prover name
@@ -597,7 +597,7 @@
       |> max_new_mono_instancesLST
       |> max_mono_itersLST)
     val minimize =
-      Sledgehammer_Minimize.minimize_facts (K ()) prover_name params
+      Sledgehammer_Minimize.minimize_facts (K (K ())) prover_name params
           true 1 (Sledgehammer_Util.subgoal_count st)
     val _ = log separator
     val (used_facts, (preplay, message, message_tail)) =
diff -r b86450f5b5cb -r 4bacc8983b3d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
@@ -381,8 +381,8 @@
         val goal = prop_of (#goal (Proof.goal state))
         val facts = nearly_all_facts ctxt false fact_override Symtab.empty
                                      Termtab.empty [] [] goal
-        val do_learn = mash_learn_proof ctxt params (hd provers) goal facts
-      in run_minimize params do_learn i (#add fact_override) state end
+        fun learn prover = mash_learn_proof ctxt params prover goal facts
+      in run_minimize params learn i (#add fact_override) state end
     else if subcommand = messagesN then
       messages opt_i
     else if subcommand = supported_proversN then
diff -r b86450f5b5cb -r 4bacc8983b3d src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jul 20 22:19:46 2012 +0200
@@ -248,7 +248,7 @@
        facts = facts |> map (apfst (apfst (fn name => name ())))
                      |> map Untranslated_Fact}
   in
-    get_minimizing_prover ctxt MaSh (K ()) prover params (K (K (K "")))
+    get_minimizing_prover ctxt MaSh (K (K ())) prover params (K (K (K "")))
                           problem
   end
 
diff -r b86450f5b5cb -r 4bacc8983b3d src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jul 20 22:19:46 2012 +0200
@@ -17,15 +17,15 @@
   val auto_minimize_min_facts : int Config.T
   val auto_minimize_max_time : real Config.T
   val minimize_facts :
-    (thm list -> unit) -> string -> params -> bool -> int -> int -> Proof.state
-    -> ((string * stature) * thm list) list
+    (string -> thm list -> unit) -> string -> params -> bool -> int -> int
+    -> Proof.state -> ((string * stature) * thm list) list
     -> ((string * stature) * thm list) list option
        * ((unit -> play) * (play -> string) * string)
   val get_minimizing_prover :
-    Proof.context -> mode -> (thm list -> unit) -> string -> prover
+    Proof.context -> mode -> (string -> thm list -> unit) -> string -> prover
   val run_minimize :
-    params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list
-    -> Proof.state -> unit
+    params -> (string -> thm list -> unit) -> int
+    -> (Facts.ref * Attrib.src list) list -> Proof.state -> unit
 end;
 
 structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
@@ -211,7 +211,7 @@
                               |> length of
                  0 => ""
                | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
-         (if learn then do_learn (maps snd min_facts) else ());
+         (if learn then do_learn prover_name (maps snd min_facts) else ());
          (SOME min_facts, (preplay, message, message_tail))
        end
      | {outcome = SOME TimedOut, preplay, ...} =>
diff -r b86450f5b5cb -r 4bacc8983b3d src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Jul 20 22:19:46 2012 +0200
@@ -93,12 +93,12 @@
       |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
                   " proof (of " ^ string_of_int (length facts) ^ "): ") "."
       |> Output.urgent_message
+    fun learn prover =
+       mash_learn_proof ctxt params prover (prop_of goal)
+                        (map untranslated_fact facts)
     fun really_go () =
       problem
-      |> get_minimizing_prover ctxt mode
-             (mash_learn_proof ctxt params name (prop_of goal)
-                               (map untranslated_fact facts))
-             name params minimize_command
+      |> get_minimizing_prover ctxt mode learn name params minimize_command
       |> verbose ? tap (fn {outcome = NONE, used_facts as _ :: _, ...} =>
                            print_used_facts used_facts
                          | _ => ())