# HG changeset patch
# User bulwahn
# Date 1290418913 -3600
# Node ID 6cd611ceb64e4bb52e05f0e3d73e27374bb09dc6
# Parent  dc55e6752046c78ff5ef58eb8a08062f5f34af40
adding files to use sledgehammer as a tactic for non-interactive use

diff -r dc55e6752046 -r 6cd611ceb64e src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML	Mon Nov 22 10:41:53 2010 +0100
@@ -0,0 +1,87 @@
+(*  Title:      sledgehammer_tactics.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2010
+
+Sledgehammer as a tactic.
+*)
+
+signature SLEDGEHAMMER_TACTICS =
+sig
+  val sledgehammer_with_metis_tac : Proof.context -> int -> tactic
+  val sledgehammer_as_oracle_tac : Proof.context -> int -> tactic
+end;
+
+structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS =
+struct
+  
+fun run_atp force_full_types timeout i n ctxt goal name =
+  let
+    val thy = ProofContext.theory_of ctxt
+    val params as {full_types, ...} =
+      ((if force_full_types then [("full_types", "true")] else [])
+       @ [("timeout", Int.toString (Time.toMilliseconds timeout) ^ " ms")])
+(*      @ [("overlord", "true")] *)
+      |> Sledgehammer_Isar.default_params thy
+    val prover = Sledgehammer.get_prover_fun thy name
+    val facts = []
+    (* Check for constants other than the built-in HOL constants. If none of
+       them appear (as should be the case for TPTP problems, unless "auto" or
+       "simp" already did its "magic"), we can skip the relevance filter. *)
+    val pure_goal =
+      not (exists_Const (fn (s, _) => String.isSubstring "." s andalso
+                                      not (String.isSubstring "HOL" s))
+                        (prop_of goal))
+    val problem =
+      {state = Proof.init ctxt, goal = goal, subgoal = i, axioms = [],
+       only = true}
+  in
+    prover params (K "") problem |> #message
+    handle ERROR message => "Error: " ^ message ^ "\n"
+  end
+
+fun to_period ("." :: _) = []
+  | to_period ("" :: ss) = to_period ss
+  | to_period (s :: ss) = s :: to_period ss
+  | to_period [] = []
+
+val extract_metis_facts =
+  space_explode " "
+  #> fold (maps o space_explode) ["(", ")", Symbol.ENQ, Symbol.ACK, "\n"]
+  #> Library.dropwhile (not o member (op =) ["metis", "metisFT"])
+  #> (fn _ :: ss => SOME (to_period ss) | _ => NONE)
+
+val atp = "e" (* or "vampire" *)
+
+fun thms_of_name ctxt name =
+  let
+    val lex = Keyword.get_lexicons
+    val get = maps (ProofContext.get_fact ctxt o fst)
+  in
+    Source.of_string name
+    |> Symbol.source {do_recover=false}
+    |> Token.source {do_recover=SOME false} lex Position.start
+    |> Token.source_proper
+    |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
+    |> Source.exhaust
+  end
+
+fun sledgehammer_with_metis_tac ctxt i th =
+  let
+    val thy = ProofContext.theory_of ctxt
+    val timeout = Time.fromSeconds (60 * 60 * 24 * 365) (* one year *)
+    val s = run_atp false timeout i i ctxt th atp
+    val xs = these (extract_metis_facts s)
+    val ths = maps (thms_of_name ctxt) xs
+  in Metis_Tactics.metis_tac ctxt ths i th end
+
+fun sledgehammer_as_oracle_tac ctxt i th =
+  let
+    val thy = ProofContext.theory_of ctxt
+    val timeout = Time.fromSeconds (60 * 60 * 24 * 365) (* one year *)
+    val s = run_atp true timeout i i ctxt th atp
+  in
+    if is_some (extract_metis_facts s) then Skip_Proof.cheat_tac thy th
+    else Seq.empty
+  end
+
+end;