--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Dec 08 22:17:52 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Dec 08 22:17:52 2010 +0100
@@ -370,7 +370,7 @@
val problem =
{state = st', goal = goal, subgoal = i,
subgoal_count = Sledgehammer_Util.subgoal_count st,
- facts = facts |> map Sledgehammer_Provers.Untranslated}
+ facts = facts |> map Sledgehammer_Provers.Untranslated_Fact}
val time_limit =
(case hard_timeout of
NONE => I
--- a/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML Wed Dec 08 22:17:52 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/sledgehammer_tactic.ML Wed Dec 08 22:17:52 2010 +0100
@@ -43,8 +43,8 @@
not (String.isSubstring "HOL" s))
(prop_of goal))
val problem =
- {state = Proof.init ctxt, goal = goal, subgoal = i,
- subgoal_count = n, facts = map Sledgehammer_Provers.Untranslated facts}
+ {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n,
+ facts = map Sledgehammer_Provers.Untranslated_Fact facts}
in
(case prover params (K "") problem of
{outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Dec 08 22:17:52 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Dec 08 22:17:52 2010 +0100
@@ -55,7 +55,7 @@
max_relevant = NONE, isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""}
val facts =
- facts |> maps (fn (n, ths) => ths |> map (Untranslated o pair n))
+ facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
val {goal, ...} = Proof.goal state
val problem =
{state = state, goal = goal, subgoal = i, subgoal_count = n,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 08 22:17:52 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 08 22:17:52 2010 +0100
@@ -29,16 +29,17 @@
timeout: Time.time,
expect: string}
- datatype fact =
- Untranslated of (string * locality) * thm |
- ATP_Translated of term * ((string * locality) * translated_formula) option
+ datatype prover_fact =
+ Untranslated_Fact of (string * locality) * thm |
+ ATP_Translated_Fact of
+ term * ((string * locality) * translated_formula) option
type prover_problem =
{state: Proof.state,
goal: thm,
subgoal: int,
subgoal_count: int,
- facts: fact list}
+ facts: prover_fact list}
type prover_result =
{outcome: failure option,
@@ -210,16 +211,17 @@
timeout: Time.time,
expect: string}
-datatype fact =
- Untranslated of (string * locality) * thm |
- ATP_Translated of term * ((string * locality) * translated_formula) option
+datatype prover_fact =
+ Untranslated_Fact of (string * locality) * thm |
+ ATP_Translated_Fact of
+ term * ((string * locality) * translated_formula) option
type prover_problem =
{state: Proof.state,
goal: thm,
subgoal: int,
subgoal_count: int,
- facts: fact list}
+ facts: prover_fact list}
type prover_result =
{outcome: failure option,
@@ -252,10 +254,11 @@
(* generic TPTP-based ATPs *)
-fun dest_Untranslated (Untranslated p) = p
- | dest_Untranslated (ATP_Translated _) = raise Fail "dest_Untranslated"
-fun atp_translated_fact ctxt (Untranslated p) = translate_atp_fact ctxt p
- | atp_translated_fact _ (ATP_Translated p) = p
+fun dest_Untranslated_Fact (Untranslated_Fact p) = p
+ | dest_Untranslated_Fact (ATP_Translated_Fact _) =
+ raise Fail "dest_Untranslated_Fact"
+fun atp_translated_fact ctxt (Untranslated_Fact p) = translate_atp_fact ctxt p
+ | atp_translated_fact _ (ATP_Translated_Fact p) = p
fun int_opt_add (SOME m) (SOME n) = SOME (m + n)
| int_opt_add _ _ = NONE
@@ -527,7 +530,8 @@
#> Config.put SMT_Config.monomorph_limit smt_monomorph_limit
val state = state |> Proof.map_context repair_context
val thy = Proof.theory_of state
- val get_fact = Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated
+ val get_fact =
+ Option.map (apsnd (Thm.transfer thy)) o try dest_Untranslated_Fact
val facts = facts |> map_filter get_fact
val {outcome, used_facts, run_time_in_msecs} =
smt_filter_loop params remote state subgoal facts
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Dec 08 22:17:52 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Wed Dec 08 22:17:52 2010 +0100
@@ -101,8 +101,8 @@
(* FUDGE *)
val auto_max_relevant_divisor = 2
-fun fact_name (Untranslated ((name, _), _)) = SOME name
- | fact_name (ATP_Translated (_, p)) = Option.map (fst o fst) p
+fun fact_name (Untranslated_Fact ((name, _), _)) = SOME name
+ | fact_name (ATP_Translated_Fact (_, p)) = Option.map (fst o fst) p
fun run_sledgehammer (params as {blocking, debug, provers, full_types,
relevance_thresholds, max_relevant, ...})
@@ -171,9 +171,9 @@
end
val run_atps =
run_provers "ATP" full_types atp_relevance_fudge
- (ATP_Translated o translate_atp_fact ctxt) atps
+ (ATP_Translated_Fact o translate_atp_fact ctxt) atps
val run_smts =
- run_provers "SMT solver" true smt_relevance_fudge Untranslated smts
+ run_provers "SMT solver" true smt_relevance_fudge Untranslated_Fact smts
fun run_atps_and_smt_solvers () =
[run_atps, run_smts] |> Par_List.map (fn f => f (false, state) |> K ())
in