# HG changeset patch
# User blanchet
# Date 1292923136 -3600
# Node ID ae76960d86a2d772b15f744c037f9928b7dd0fad
# Parent  ffd730fcf0ac04c141c9e2ac7db6cecf8d514eda
added "sledgehammer_tac" as possible reconstructor in Mirabelle

diff -r ffd730fcf0ac -r ae76960d86a2 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Dec 21 06:53:20 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Dec 21 10:18:56 2010 +0100
@@ -13,6 +13,7 @@
 val minimizeK = "minimize"
 val minimize_timeoutK = "minimize_timeout"
 val metis_ftK = "metis_ft"
+val reconstructorK = "reconstructor"
 
 fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
 fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
@@ -331,10 +332,13 @@
 type locality = Sledgehammer_Filter.locality
 
 (* hack *)
-fun reconstructor_from_msg msg =
-  if String.isSubstring "metisFT" msg then "metisFT"
-  else if String.isSubstring "metis" msg then "metis"
-  else "smt"
+fun reconstructor_from_msg args msg =
+  (case AList.lookup (op =) args reconstructorK of
+    SOME name => name
+  | NONE =>
+    if String.isSubstring "metisFT" msg then "metisFT"
+    else if String.isSubstring "metis" msg then "metis"
+    else "smt")
 
 local
 
@@ -445,7 +449,7 @@
           change_data id (inc_sh_max_lems (length names));
           change_data id (inc_sh_time_isa time_isa);
           change_data id (inc_sh_time_prover time_prover);
-          reconstructor := reconstructor_from_msg msg;
+          reconstructor := reconstructor_from_msg args msg;
           named_thms := SOME (map_filter get_thms names);
           log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
             string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
@@ -487,7 +491,7 @@
          change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
          if length named_thms' = n0
          then log (minimize_tag id ^ "already minimal")
-         else (reconstructor := reconstructor_from_msg msg;
+         else (reconstructor := reconstructor_from_msg args msg;
                named_thms := SOME named_thms';
                log (minimize_tag id ^ "succeeded:\n" ^ msg))
         )
@@ -499,7 +503,11 @@
     ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
   let
     fun do_reconstructor thms ctxt =
-      (if !reconstructor = "smt" then
+      (if !reconstructor = "sledgehammer_tac" then
+         (fn ctxt => fn thms =>
+            Method.insert_tac thms THEN'
+            Sledgehammer_Tactics.sledgehammer_as_unsound_oracle_tac ctxt)
+       else if !reconstructor = "smt" then
          SMT_Solver.smt_tac
        else if full orelse !reconstructor = "metisFT" then
          Metis_Tactics.metisFT_tac
diff -r ffd730fcf0ac -r ae76960d86a2 src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML
--- a/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML	Tue Dec 21 06:53:20 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML	Tue Dec 21 10:18:56 2010 +0100
@@ -8,6 +8,7 @@
 signature SLEDGEHAMMER_TACTICS =
 sig
   val sledgehammer_with_metis_tac : Proof.context -> int -> tactic
+  val sledgehammer_as_unsound_oracle_tac : Proof.context -> int -> tactic
   val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic
 end;
 
@@ -20,7 +21,7 @@
     val params as {type_sys, relevance_thresholds, max_relevant, ...} =
       ((if force_full_types then [("full_types", "true")] else [])
        @ [("timeout", Int.toString (Time.toSeconds timeout))])
-       @ [("overlord", "true")]
+       (* @ [("overlord", "true")] *)
       |> Sledgehammer_Isar.default_params ctxt
     val prover = Sledgehammer_Provers.get_prover ctxt false name
     val default_max_relevant =
@@ -61,7 +62,7 @@
   | to_period (s :: ss) = s :: to_period ss
   | to_period [] = []
 
-val atp = "e" (* or "vampire" *)
+val atp = "vampire" (* or "e" or "spass" etc. *)
 
 fun thms_of_name ctxt name =
   let
@@ -81,18 +82,20 @@
     val timeout = Time.fromSeconds 30
   in
     case run_atp false timeout i i ctxt th atp of
-      SOME facts => Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th
+      SOME facts =>
+      Metis_Tactics.metis_tac ctxt (maps (thms_of_name ctxt) facts) i th
     | NONE => Seq.empty
   end
 
-fun sledgehammer_as_oracle_tac ctxt i th =
+fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th =
   let
     val thy = ProofContext.theory_of ctxt
     val timeout = Time.fromSeconds 30
-    val xs = run_atp true timeout i i ctxt th atp
-  in
-    if is_some xs then Skip_Proof.cheat_tac thy th
-    else Seq.empty
-  end
+    val xs = run_atp force_full_types timeout i i ctxt th atp
+  in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
+
+val sledgehammer_as_unsound_oracle_tac =
+  generic_sledgehammer_as_oracle_tac false
+val sledgehammer_as_oracle_tac = generic_sledgehammer_as_oracle_tac true
 
 end;