# HG changeset patch # User blanchet # Date 1314117725 -7200 # Node ID e5506cfe1b5a50ca76bbc310cc375523e48bf841 # Parent ccb8998f70b7cf172aaa8f10624fafaf74b7aafb clean up Sledgehammer tactic diff -r ccb8998f70b7 -r e5506cfe1b5a src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Tue Aug 23 17:44:31 2011 +0200 +++ b/src/HOL/ex/sledgehammer_tactics.ML Tue Aug 23 18:42:05 2011 +0200 @@ -7,22 +7,21 @@ 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 + val sledgehammer_with_metis_tac : + Proof.context -> (string * string) list -> int -> tactic + val sledgehammer_as_oracle_tac : + Proof.context -> (string * string) list -> int -> tactic end; structure Sledgehammer_Tactics : SLEDGEHAMMER_TACTICS = struct -fun run_atp force_full_types timeout i n ctxt goal name = +fun run_atp override_params i n ctxt goal = let val chained_ths = [] (* a tactic has no chained ths *) - val params as {relevance_thresholds, max_relevant, slicing, ...} = - ((if force_full_types then [("sound", "true")] else []) - @ [("timeout", string_of_int (Time.toSeconds timeout))]) - (* @ [("overlord", "true")] *) - |> Sledgehammer_Isar.default_params ctxt + val params as {provers, relevance_thresholds, max_relevant, slicing, ...} = + Sledgehammer_Isar.default_params ctxt override_params + val name = hd provers val prover = Sledgehammer_Provers.get_prover ctxt Sledgehammer_Provers.Normal name val default_max_relevant = @@ -50,8 +49,6 @@ handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE) end -val atp = "e" (* or "vampire" or "spass" etc. *) - fun thms_of_name ctxt name = let val lex = Keyword.get_lexicons @@ -65,25 +62,16 @@ |> Source.exhaust end -fun sledgehammer_with_metis_tac ctxt i th = - let - 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 - | NONE => Seq.empty - end +fun sledgehammer_with_metis_tac ctxt override_params i th = + case run_atp override_params i i ctxt th of + SOME facts => + Metis_Tactics.metis_tac [] ctxt (maps (thms_of_name ctxt) facts) i th + | NONE => Seq.empty -fun generic_sledgehammer_as_oracle_tac force_full_types ctxt i th = +fun sledgehammer_as_oracle_tac ctxt override_params i th = let val thy = Proof_Context.theory_of ctxt - val timeout = Time.fromSeconds 30 - val xs = run_atp force_full_types timeout i i ctxt th atp + val xs = run_atp (override_params @ [("sound", "true")]) i i ctxt th 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;