--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Sep 01 23:04:47 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Sep 01 23:10:01 2010 +0200
@@ -321,8 +321,7 @@
relevance_override chained_ths hyp_ts concl_t
val problem =
{ctxt = ctxt', goal = goal, subgoal = i,
- axiom_ts = map (prop_of o snd) axioms,
- prepared_axioms = map (Sledgehammer_Translate.prepare_axiom ctxt) axioms}
+ axioms = map (Sledgehammer_Translate.prepare_axiom ctxt) axioms}
val time_limit =
(case hard_timeout of
NONE => I
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Sep 01 23:04:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Sep 01 23:10:01 2010 +0200
@@ -31,8 +31,7 @@
{ctxt: Proof.context,
goal: thm,
subgoal: int,
- axiom_ts: term list,
- prepared_axioms: ((string * locality) * fol_formula) option list}
+ axioms: (term * ((string * locality) * fol_formula) option) list}
type prover_result =
{outcome: failure option,
message: string,
@@ -101,8 +100,7 @@
{ctxt: Proof.context,
goal: thm,
subgoal: int,
- axiom_ts: term list,
- prepared_axioms: ((string * locality) * fol_formula) option list}
+ axioms: (term * ((string * locality) * fol_formula) option) list}
type prover_result =
{outcome: failure option,
@@ -220,13 +218,11 @@
use_conjecture_for_hypotheses}
({debug, verbose, overlord, full_types, explicit_apply,
max_relevant, isar_proof, isar_shrink_factor, timeout, ...} : params)
- minimize_command
- ({ctxt, goal, subgoal, axiom_ts, prepared_axioms} : problem) =
+ minimize_command ({ctxt, goal, subgoal, axioms} : problem) =
let
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
val max_relevant = the_default default_max_relevant max_relevant
- val axiom_ts = take max_relevant axiom_ts
- val prepared_axioms = take max_relevant prepared_axioms
+ val axioms = take max_relevant axioms
(* path to unique problem file *)
val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
else Config.get ctxt dest_dir
@@ -288,8 +284,7 @@
val readable_names = debug andalso overlord
val (problem, pool, conjecture_offset, axiom_names) =
prepare_problem ctxt readable_names explicit_forall full_types
- explicit_apply hyp_ts concl_t axiom_ts
- prepared_axioms
+ explicit_apply hyp_ts concl_t axioms
val ss = strings_for_tptp_problem use_conjecture_for_hypotheses
problem
val _ = File.write_list probfile ss
@@ -368,8 +363,7 @@
let
val problem =
{ctxt = ctxt, goal = goal, subgoal = i,
- axiom_ts = map (prop_of o snd) axioms,
- prepared_axioms = map (prepare_axiom ctxt) axioms}
+ axioms = map (prepare_axiom ctxt) axioms}
val (outcome_code, message) =
prover_fun atp_name prover params (minimize_command atp_name) problem
|> (fn {outcome, message, ...} =>
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Sep 01 23:04:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Sep 01 23:10:01 2010 +0200
@@ -60,8 +60,7 @@
val {context = ctxt, goal, ...} = Proof.goal state
val problem =
{ctxt = ctxt, goal = goal, subgoal = subgoal,
- axiom_ts = map (prop_of o snd) axioms,
- prepared_axioms = map (prepare_axiom ctxt) axioms}
+ axioms = map (prepare_axiom ctxt) axioms}
val result as {outcome, used_thm_names, ...} = prover params (K "") problem
in
priority (case outcome of
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Sep 01 23:04:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Sep 01 23:10:01 2010 +0200
@@ -18,10 +18,11 @@
val arity_clause_prefix : string
val tfrees_name : string
val prepare_axiom :
- Proof.context -> (string * 'a) * thm -> ((string * 'a) * fol_formula) option
+ Proof.context -> (string * 'a) * thm
+ -> term * ((string * 'a) * fol_formula) option
val prepare_problem :
Proof.context -> bool -> bool -> bool -> bool -> term list -> term
- -> term list -> ((string * 'a) * fol_formula) option list
+ -> (term * ((string * 'a) * fol_formula) option) list
-> string problem * string Symtab.table * int * (string * 'a) list vector
end;
@@ -249,15 +250,15 @@
|> map_filter (Option.map snd o make_axiom ctxt false)
end
-fun prepare_axiom ctxt = make_axiom ctxt true
+fun prepare_axiom ctxt (ax as (_, th)) = (prop_of th, make_axiom ctxt true ax)
-fun prepare_formulas ctxt full_types hyp_ts concl_t axiom_ts prepared_axioms =
+fun prepare_formulas ctxt full_types hyp_ts concl_t axioms =
let
val thy = ProofContext.theory_of ctxt
- val hyp_ts =
- (* Remove existing axioms from the conjecture, as this can dramatically
- boost an ATP's performance (for some reason). *)
- hyp_ts |> filter_out (member (op aconv) axiom_ts)
+ val (axiom_ts, prepared_axioms) = ListPair.unzip axioms
+ (* Remove existing axioms from the conjecture, as this can dramatically
+ boost an ATP's performance (for some reason). *)
+ val hyp_ts = hyp_ts |> filter_out (member (op aconv) axiom_ts)
val goal_t = Logic.list_implies (hyp_ts, concl_t)
val is_FO = Meson.is_fol_term thy goal_t
val subs = tfree_classes_of_terms [goal_t]
@@ -498,12 +499,12 @@
(const_table_for_problem explicit_apply problem) problem
fun prepare_problem ctxt readable_names explicit_forall full_types
- explicit_apply hyp_ts concl_t axiom_ts prepared_axioms =
+ explicit_apply hyp_ts concl_t axioms =
let
val thy = ProofContext.theory_of ctxt
val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses,
arity_clauses)) =
- prepare_formulas ctxt full_types hyp_ts concl_t axiom_ts prepared_axioms
+ prepare_formulas ctxt full_types hyp_ts concl_t axioms
val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
val helper_lines =
map (problem_line_for_fact helper_prefix full_types) helper_facts