# HG changeset patch
# User blanchet
# Date 1307385394 -7200
# Node ID 467d5b34e1f5290894d20e54776f07c240aa3be0
# Parent  839f599bc7ed945cfcdf93ffb4603dd37073e208
temporarily added "MetisX" as reconstructor and minimizer

diff -r 839f599bc7ed -r 467d5b34e1f5 src/HOL/Tools/ATP/atp_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Jun 06 20:36:34 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Jun 06 20:36:34 2011 +0200
@@ -17,6 +17,7 @@
   datatype reconstructor =
     Metis |
     MetisFT |
+    MetisX |
     SMT of string
 
   datatype play =
@@ -68,6 +69,7 @@
 datatype reconstructor =
   Metis |
   MetisFT |
+  MetisX |
   SMT of string
 
 datatype play =
@@ -253,6 +255,7 @@
 
 fun reconstructor_name Metis = "metis"
   | reconstructor_name MetisFT = "metisFT"
+  | reconstructor_name MetisX = "metisX"
   | reconstructor_name (SMT _) = "smt"
 
 fun reconstructor_settings (SMT settings) = settings
@@ -1023,7 +1026,7 @@
        else
          if member (op =) qs Show then "show" else "have")
     val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
-    val reconstructor = if full_types then MetisFT else Metis
+    val reconstructor = if full_types then MetisX else Metis
     fun do_facts (ls, ss) =
       reconstructor_command reconstructor 1 1
           (ls |> sort_distinct (prod_ord string_ord int_ord),
diff -r 839f599bc7ed -r 467d5b34e1f5 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 06 20:36:34 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon Jun 06 20:36:34 2011 +0200
@@ -129,7 +129,8 @@
    "Async_Manager". *)
 val das_tool = "Sledgehammer"
 
-val metis_prover_names = [Metis_Tactics.metisN, Metis_Tactics.metisFT_N]
+val metis_prover_names =
+  [Metis_Tactics.metisN, Metis_Tactics.metisFT_N, Metis_Tactics.metisX_N]
 
 val is_metis_prover = member (op =) metis_prover_names
 val is_atp = member (op =) o supported_atps
@@ -418,6 +419,8 @@
 
 fun tac_for_reconstructor Metis = Metis_Tactics.metisHO_tac
   | tac_for_reconstructor MetisFT = Metis_Tactics.metisFT_tac
+  | tac_for_reconstructor MetisX =
+    (fn ctxt => Metis_Tactics.metisX_tac ctxt NONE)
   | tac_for_reconstructor _ = raise Fail "unexpected reconstructor"
 
 fun timed_reconstructor reconstructor debug timeout ths =
@@ -787,7 +790,7 @@
                         |> map snd
               in
                 play_one_line_proof debug preplay_timeout used_ths state subgoal
-                                    [Metis, MetisFT]
+                                    [Metis, MetisX]
               end,
            fn preplay =>
               let
@@ -981,9 +984,9 @@
                 else "smt_solver = " ^ maybe_quote name
             in
               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)
+                                       subgoal [Metis, MetisX] of
+                p as Played _ => p
+              | _ => Trust_Playable (SMT (smt_settings ()), NONE)
             end,
          fn preplay =>
             let
@@ -1013,6 +1016,7 @@
   let
     val reconstructor = if name = Metis_Tactics.metisN then Metis
                         else if name = Metis_Tactics.metisFT_N then MetisFT
+                        else if name = Metis_Tactics.metisX_N then MetisX
                         else raise Fail ("unknown Metis version: " ^ quote name)
     val (used_facts, used_ths) =
       facts |> map untranslated_fact |> ListPair.unzip