support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing

--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon May 30 15:30:05 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon May 30 17:00:38 2011 +0200
@@ -16,7 +16,7 @@
 
   datatype failure =
     Unprovable |
-    IncompleteUnprovable |
+    GaveUp |
     ProofMissing |
     ProofIncomplete |
     UnsoundProof of bool * string list |
@@ -73,7 +73,7 @@
 
 datatype failure =
   Unprovable |
-  IncompleteUnprovable |
+  GaveUp |
   ProofMissing |
   ProofIncomplete |
   UnsoundProof of bool * string list |
@@ -146,7 +146,7 @@
     " "
 
 fun string_for_failure Unprovable = "The problem is unprovable."
-  | string_for_failure IncompleteUnprovable = "The prover gave up."
+  | string_for_failure GaveUp = "The prover gave up."
   | string_for_failure ProofMissing =
     "The prover claims the conjecture is a theorem but did not provide a proof."
   | string_for_failure ProofIncomplete =
@@ -231,7 +231,7 @@
         extract_known_failure known_failures output) of
     (_, SOME ProofIncomplete) => ("", SOME ProofIncomplete)
   | ("", SOME failure) =>
-    ("", SOME (if failure = IncompleteUnprovable andalso complete then Unprovable
+    ("", SOME (if failure = GaveUp andalso complete then Unprovable
                else failure))
   | ("", NONE) =>
     ("", SOME (if res_code = 0 andalso output = "" then ProofMissing

--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon May 30 15:30:05 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon May 30 17:00:38 2011 +0200
@@ -256,7 +256,7 @@
    proof_delims = [("Here is a proof", "Formulae used in the proof")],
    known_failures =
      known_perl_failures @
-     [(IncompleteUnprovable, "SPASS beiseite: Completion found"),
+     [(GaveUp, "SPASS beiseite: Completion found"),
       (TimedOut, "SPASS beiseite: Ran out of time"),
       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
       (MalformedInput, "Undefined symbol"),
@@ -296,9 +296,9 @@
       ("% SZS output start Refutation", "% SZS output end Refutation"),
       ("% SZS output start Proof", "% SZS output end Proof")],
    known_failures =
-     [(Unprovable, "UNPROVABLE"),
-      (IncompleteUnprovable, "CANNOT PROVE"),
-      (IncompleteUnprovable, "SZS status GaveUp"),
+     [(GaveUp, "UNPROVABLE"),
+      (GaveUp, "CANNOT PROVE"),
+      (GaveUp, "SZS status GaveUp"),
       (ProofIncomplete, "predicate_definition_introduction,[]"),
       (TimedOut, "SZS status Timeout"),
       (Unprovable, "Satisfiability detected"),
@@ -329,8 +329,8 @@
    proof_delims = [],
    known_failures =
      [(Unprovable, "\nsat"),
-      (IncompleteUnprovable, "\nunknown"),
-      (IncompleteUnprovable, "SZS status Satisfiable"),
+      (GaveUp, "\nunknown"),
+      (GaveUp, "SZS status Satisfiable"),
       (ProofMissing, "\nunsat"),
       (ProofMissing, "SZS status Unsatisfiable")],
    conj_sym_kind = Hypothesis,
@@ -388,10 +388,10 @@
    known_failures = known_failures @ known_perl_failures @
      [(Unprovable, "says Satisfiable"),
       (Unprovable, "says CounterSatisfiable"),
+      (GaveUp, "says Unknown"),
+      (GaveUp, "says GaveUp"),
       (ProofMissing, "says Theorem"),
       (ProofMissing, "says Unsatisfiable"),
-      (IncompleteUnprovable, "says Unknown"),
-      (IncompleteUnprovable, "says GaveUp"),
       (TimedOut, "says Timeout"),
       (Inappropriate, "says Inappropriate")],
    conj_sym_kind = conj_sym_kind,

--- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon May 30 15:30:05 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon May 30 17:00:38 2011 +0200
@@ -9,6 +9,9 @@
 
 signature METIS_TACTICS =
 sig
+  val metisN : string
+  val metisF_N : string
+  val metisFT_N : string
   val trace : bool Config.T
   val verbose : bool Config.T
   val type_lits : bool Config.T
@@ -26,6 +29,14 @@
 open Metis_Translate
 open Metis_Reconstruct
 
+fun method_binding_for_mode HO = @{binding metis}
+  | method_binding_for_mode FO = @{binding metisF}
+  | method_binding_for_mode FT = @{binding metisFT}
+
+val metisN = Binding.qualified_name_of (method_binding_for_mode HO)
+val metisF_N = Binding.qualified_name_of (method_binding_for_mode FO)
+val metisFT_N = Binding.qualified_name_of (method_binding_for_mode FT)
+
 val type_lits = Attrib.setup_config_bool @{binding metis_type_lits} (K true)
 val new_skolemizer = Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false)
 
@@ -53,10 +64,6 @@
    models = []}
 val resolution_params = {active = active_params, waiting = waiting_params}
 
-fun method_binding_for_mode HO = @{binding metis}
-  | method_binding_for_mode FO = @{binding metisF}
-  | method_binding_for_mode FT = @{binding metisFT}
-
 (* Main function to start Metis proof and reconstruction *)
 fun FOL_SOLVE (mode :: fallback_modes) ctxt cls ths0 =
   let val thy = Proof_Context.theory_of ctxt
@@ -136,7 +143,8 @@
          | mode :: _ =>
            (verbose_warning ctxt
                 ("Falling back on " ^
-                 quote (Binding.str_of (method_binding_for_mode mode)) ^ "...");
+                 quote (Binding.qualified_name_of
+                            (method_binding_for_mode mode)) ^ "...");
             FOL_SOLVE fallback_modes ctxt cls ths0)
 
 val neg_clausify =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Mon May 30 15:30:05 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Mon May 30 17:00:38 2011 +0200
@@ -17,14 +17,14 @@
     MetisFT |
     SMT of string
 
-  datatype preplay =
-    Preplayed of reconstructor * Time.time |
+  datatype play =
+    Played of reconstructor * Time.time |
     Trust_Playable of reconstructor * Time.time option|
-    Failed_to_Preplay
+    Failed_to_Play
 
   type minimize_command = string list -> string
   type one_line_params =
-    preplay * string * (string * locality) list * minimize_command * int * int
+    play * string * (string * locality) list * minimize_command * int * int
   type isar_params =
     bool * bool * int * type_system * string Symtab.table * int list list
     * int * (string * locality) list vector * int Symtab.table * string proof
@@ -62,14 +62,14 @@
   MetisFT |
   SMT of string
 
-datatype preplay =
-  Preplayed of reconstructor * Time.time |
+datatype play =
+  Played of reconstructor * Time.time |
   Trust_Playable of reconstructor * Time.time option |
-  Failed_to_Preplay
+  Failed_to_Play
 
 type minimize_command = string list -> string
 type one_line_params =
-  preplay * string * (string * locality) list * minimize_command * int * int
+  play * string * (string * locality) list * minimize_command * int * int
 type isar_params =
   bool * bool * int * type_system * string Symtab.table * int list list * int
   * (string * locality) list vector * int Symtab.table * string proof * thm
@@ -288,7 +288,7 @@
     val (chained, extra) = split_used_facts used_facts
     val (reconstructor, ext_time) =
       case preplay of
-        Preplayed (reconstructor, time) =>
+        Played (reconstructor, time) =>
         (SOME reconstructor, (SOME (false, time)))
       | Trust_Playable (reconstructor, time) =>
         (SOME reconstructor,
@@ -296,7 +296,7 @@
            NONE => NONE
          | SOME time =>
            if time = Time.zeroTime then NONE else SOME (true, time))
-      | Failed_to_Preplay => (NONE, NONE)
+      | Failed_to_Play => (NONE, NONE)
     val try_line =
       case reconstructor of
         SOME r => ([], map fst extra)
@@ -1076,7 +1076,7 @@
 
 fun proof_text ctxt isar_proof isar_params
                (one_line_params as (preplay, _, _, _, _, _)) =
-  (if isar_proof orelse preplay = Failed_to_Preplay then
+  (if isar_proof orelse preplay = Failed_to_Play then
      isar_proof_text ctxt isar_params
    else
      one_line_proof_text) one_line_params

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Mon May 30 15:30:05 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Mon May 30 17:00:38 2011 +0200
@@ -75,13 +75,19 @@
     val problem =
       {state = state, goal = goal, subgoal = i, subgoal_count = n,
        facts = facts, smt_filter = NONE}
-    val result as {outcome, used_facts, ...} = prover params (K "") problem
+    val result as {outcome, used_facts, run_time_in_msecs, ...} =
+      prover params (K "") problem
   in
     print silent (fn () =>
         case outcome of
           SOME failure => string_for_failure failure
-        | NONE => if length used_facts = length facts then "Found proof."
-                  else "Found proof with " ^ n_facts used_facts ^ ".");
+        | NONE => "Found proof" ^
+                  (if length used_facts = length facts then ""
+                   else " with " ^ n_facts used_facts) ^
+                  (case run_time_in_msecs of
+                     SOME ms =>
+                     " (" ^ string_from_time (Time.fromMilliseconds ms) ^ ")"
+                   | NONE => "") ^ ".");
     result
   end
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 30 15:30:05 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 30 17:00:38 2011 +0200
@@ -73,6 +73,8 @@
   val smt_slice_min_secs : int Config.T
   val das_tool : string
   val select_smt_solver : string -> Proof.context -> Proof.context
+  val is_metis_prover : string -> bool
+  val is_atp : theory -> string -> bool
   val is_smt_prover : Proof.context -> string -> bool
   val is_unit_equational_atp : Proof.context -> string -> bool
   val is_prover_supported : Proof.context -> string -> bool
@@ -123,6 +125,11 @@
    "Async_Manager". *)
 val das_tool = "Sledgehammer"
 
+val metis_prover_names = [Metis_Tactics.metisN, Metis_Tactics.metisFT_N]
+
+val is_metis_prover = member (op =) metis_prover_names
+val is_atp = member (op =) o supported_atps
+
 val select_smt_solver =
   Context.proof_map o SMT_Config.select_solver
 
@@ -138,22 +145,27 @@
 
 fun is_prover_supported ctxt name =
   let val thy = Proof_Context.theory_of ctxt in
-    is_smt_prover ctxt name orelse member (op =) (supported_atps thy) name
+    is_metis_prover name orelse is_atp thy name orelse is_smt_prover ctxt name
   end
 
 fun is_prover_installed ctxt =
-  is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
+  is_metis_prover orf is_smt_prover ctxt orf
+  is_atp_installed (Proof_Context.theory_of ctxt)
 
 fun get_slices slicing slices =
   (0 upto length slices - 1) ~~ slices |> not slicing ? (List.last #> single)
 
+val metis_default_max_relevant = 20
+
 fun default_max_relevant_for_prover ctxt slicing name =
   let val thy = Proof_Context.theory_of ctxt in
-    if is_smt_prover ctxt name then
-      SMT_Solver.default_max_relevant ctxt name
-    else
+    if is_metis_prover name then
+      metis_default_max_relevant
+    else if is_atp thy name then
       fold (Integer.max o fst o snd o snd o snd)
            (get_slices slicing (#best_slices (get_atp thy name) ctxt)) 0
+    else (* is_smt_prover ctxt name *)
+      SMT_Solver.default_max_relevant ctxt name
   end
 
 (* These are either simplified away by "Meson.presimplify" (most of the time) or
@@ -250,6 +262,7 @@
   let
     val thy = Proof_Context.theory_of ctxt
     val (remote_provers, local_provers) =
+      metis_prover_names @
       sort_strings (supported_atps thy) @
       sort_strings (SMT_Solver.available_solvers_of ctxt)
       |> List.partition (String.isPrefix remote_prefix)
@@ -399,22 +412,21 @@
 
 fun filter_used_facts used = filter (member (op =) used o fst)
 
-fun preplay_one_line_proof debug timeout ths state i reconstructors =
+fun play_one_line_proof debug timeout ths state i reconstructors =
   let
-    fun preplay [] [] = Failed_to_Preplay
-      | preplay (timed_out :: _) [] = Trust_Playable (timed_out, SOME timeout)
-      | preplay timed_out (reconstructor :: reconstructors) =
+    fun play [] [] = Failed_to_Play
+      | play (timed_out :: _) [] = Trust_Playable (timed_out, SOME timeout)
+      | play timed_out (reconstructor :: reconstructors) =
         let val timer = Timer.startRealTimer () in
           case timed_reconstructor reconstructor debug timeout ths state i of
-            SOME (SOME _) =>
-            Preplayed (reconstructor, Timer.checkRealTimer timer)
-          | _ => preplay timed_out reconstructors
+            SOME (SOME _) => Played (reconstructor, Timer.checkRealTimer timer)
+          | _ => play timed_out reconstructors
         end
         handle TimeLimit.TimeOut =>
-               preplay (reconstructor :: timed_out) reconstructors
+               play (reconstructor :: timed_out) reconstructors
   in
     if timeout = Time.zeroTime then Trust_Playable (hd reconstructors, NONE)
-    else preplay [] reconstructors
+    else play [] reconstructors
   end
 
 
@@ -676,8 +688,7 @@
                            UnsoundProof (is_type_sys_virtually_sound type_sys,
                                          facts |> sort string_ord))
                   | SOME Unprovable =>
-                    if null blacklist then outcome
-                    else SOME IncompleteUnprovable
+                    if null blacklist then outcome else SOME GaveUp
                   | _ => outcome
               in
                 ((pool, conjecture_shape, facts_offset, fact_names,
@@ -763,8 +774,8 @@
                   |> filter_used_facts used_facts
                   |> map snd
           val preplay =
-            preplay_one_line_proof debug preplay_timeout used_ths state subgoal
-                                   reconstructors
+            play_one_line_proof debug preplay_timeout used_ths state subgoal
+                                reconstructors
           val full_types = uses_typed_helpers typed_helpers atp_proof
           val isar_params =
             (debug, full_types, isar_shrink_factor, type_sys, pool,
@@ -814,7 +825,7 @@
   remote_smt_failures @ z3_wrapper_failures @ z3_failures @ unix_failures
 
 fun failure_from_smt_failure (SMT_Failure.Counterexample {is_real_cex, ...}) =
-    if is_real_cex then Unprovable else IncompleteUnprovable
+    if is_real_cex then Unprovable else GaveUp
   | failure_from_smt_failure SMT_Failure.Time_Out = TimedOut
   | failure_from_smt_failure (SMT_Failure.Abnormal_Termination code) =
     (case AList.lookup (op =) smt_failures code of
@@ -953,9 +964,9 @@
             if name = SMT_Solver.solver_name_of ctxt then ""
             else "smt_solver = " ^ maybe_quote name
           val preplay =
-            case preplay_one_line_proof debug preplay_timeout used_ths state
-                                        subgoal [Metis, MetisFT] of
-              p as Preplayed _ => p
+            case play_one_line_proof debug preplay_timeout used_ths state
+                                     subgoal [Metis, MetisFT] of
+              p as Played _ => p
             | _ => Trust_Playable (SMT (smt_settings ()), NONE)
           val one_line_params =
             (preplay, proof_banner mode blocking name, used_facts,
@@ -975,12 +986,41 @@
      run_time_in_msecs = run_time_in_msecs, message = message}
   end
 
+fun run_metis mode name ({debug, blocking, timeout, ...} : params)
+              minimize_command
+              ({state, subgoal, subgoal_count, facts, ...} : prover_problem) =
+  let
+    val reconstructor = if name = Metis_Tactics.metisN then Metis
+                        else if name = Metis_Tactics.metisFT_N then MetisFT
+                        else raise Fail ("unknown Metis version: " ^ quote name)
+    val (used_facts, used_ths) =
+      facts |> map untranslated_fact |> ListPair.unzip
+  in
+    case play_one_line_proof debug timeout used_ths state subgoal
+                             [reconstructor] of
+      play as Played (_, time) =>
+      let
+        val one_line_params =
+          (play, proof_banner mode blocking name, used_facts,
+           minimize_command, subgoal, subgoal_count)
+      in
+        {outcome = NONE, used_facts = used_facts,
+         run_time_in_msecs = SOME (Time.toMilliseconds time),
+         message = one_line_proof_text one_line_params}
+      end
+    | play =>
+      {outcome = SOME (if play = Failed_to_Play then GaveUp else TimedOut),
+       used_facts = [], run_time_in_msecs = NONE, message = ""}
+  end
+
 fun get_prover ctxt mode name =
   let val thy = Proof_Context.theory_of ctxt in
-    if is_smt_prover ctxt name then
+    if is_metis_prover name then
+      run_metis mode name
+    else if is_atp thy name then
+      run_atp mode name (get_atp thy name)
+    else if is_smt_prover ctxt name then
       run_smt_solver mode name
-    else if member (op =) (supported_atps thy) name then
-      run_atp mode name (get_atp thy name)
     else
       error ("No such prover: " ^ name ^ ".")
   end