--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Sep 01 22:33:31 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Wed Sep 01 23:04:47 2010 +0200
@@ -319,7 +319,10 @@
Sledgehammer_Filter.relevant_facts ctxt full_types relevance_thresholds
(the_default default_max_relevant max_relevant)
relevance_override chained_ths hyp_ts concl_t
- val problem = {ctxt = ctxt', goal = goal, subgoal = i, axioms = axioms}
+ 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}
val time_limit =
(case hard_timeout of
NONE => I
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Sep 01 22:33:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Sep 01 23:04:47 2010 +0200
@@ -11,6 +11,7 @@
type failure = ATP_Systems.failure
type locality = Sledgehammer_Filter.locality
type relevance_override = Sledgehammer_Filter.relevance_override
+ type fol_formula = Sledgehammer_Translate.fol_formula
type minimize_command = Sledgehammer_Reconstruct.minimize_command
type params =
{blocking: bool,
@@ -30,7 +31,8 @@
{ctxt: Proof.context,
goal: thm,
subgoal: int,
- axioms: ((string * locality) * thm) list}
+ axiom_ts: term list,
+ prepared_axioms: ((string * locality) * fol_formula) option list}
type prover_result =
{outcome: failure option,
message: string,
@@ -99,7 +101,8 @@
{ctxt: Proof.context,
goal: thm,
subgoal: int,
- axioms: ((string * locality) * thm) list}
+ axiom_ts: term list,
+ prepared_axioms: ((string * locality) * fol_formula) option list}
type prover_result =
{outcome: failure option,
@@ -217,11 +220,13 @@
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, axioms} : problem) =
+ minimize_command
+ ({ctxt, goal, subgoal, axiom_ts, prepared_axioms} : problem) =
let
val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
val max_relevant = the_default default_max_relevant max_relevant
- val axioms = take max_relevant axioms
+ val axiom_ts = take max_relevant axiom_ts
+ val prepared_axioms = take max_relevant prepared_axioms
(* path to unique problem file *)
val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
else Config.get ctxt dest_dir
@@ -283,7 +288,8 @@
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 axioms
+ explicit_apply hyp_ts concl_t axiom_ts
+ prepared_axioms
val ss = strings_for_tptp_problem use_conjecture_for_hypotheses
problem
val _ = File.write_list probfile ss
@@ -360,7 +366,10 @@
"\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i)))
fun run () =
let
- val problem = {ctxt = ctxt, goal = goal, subgoal = i, axioms = axioms}
+ val problem =
+ {ctxt = ctxt, goal = goal, subgoal = i,
+ axiom_ts = map (prop_of o snd) axioms,
+ prepared_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 22:33:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Sep 01 23:04:47 2010 +0200
@@ -23,6 +23,7 @@
open ATP_Systems
open Sledgehammer_Util
open Sledgehammer_Filter
+open Sledgehammer_Translate
open Sledgehammer_Reconstruct
open Sledgehammer
@@ -57,7 +58,10 @@
isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""}
val axioms = maps (fn (n, ths) => map (pair n) ths) axioms
val {context = ctxt, goal, ...} = Proof.goal state
- val problem = {ctxt = ctxt, goal = goal, subgoal = subgoal, axioms = axioms}
+ val problem =
+ {ctxt = ctxt, goal = goal, subgoal = subgoal,
+ axiom_ts = map (prop_of o snd) axioms,
+ prepared_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 22:33:31 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Sep 01 23:04:47 2010 +0200
@@ -9,6 +9,7 @@
signature SLEDGEHAMMER_TRANSLATE =
sig
type 'a problem = 'a ATP_Problem.problem
+ type fol_formula
val axiom_prefix : string
val conjecture_prefix : string
@@ -16,9 +17,11 @@
val class_rel_clause_prefix : string
val arity_clause_prefix : string
val tfrees_name : string
+ val prepare_axiom :
+ Proof.context -> (string * 'a) * thm -> ((string * 'a) * fol_formula) option
val prepare_problem :
Proof.context -> bool -> bool -> bool -> bool -> term list -> term
- -> ((string * 'a) * thm) list
+ -> term list -> ((string * 'a) * fol_formula) option list
-> string problem * string Symtab.table * int * (string * 'a) list vector
end;
@@ -246,10 +249,11 @@
|> map_filter (Option.map snd o make_axiom ctxt false)
end
-fun prepare_formulas ctxt full_types hyp_ts concl_t axiom_pairs =
+fun prepare_axiom ctxt = make_axiom ctxt true
+
+fun prepare_formulas ctxt full_types hyp_ts concl_t axiom_ts prepared_axioms =
let
val thy = ProofContext.theory_of ctxt
- val axiom_ts = map (prop_of o snd) axiom_pairs
val hyp_ts =
(* Remove existing axioms from the conjecture, as this can dramatically
boost an ATP's performance (for some reason). *)
@@ -261,8 +265,7 @@
val tycons = type_consts_of_terms thy (goal_t :: axiom_ts)
(* TFrees in the conjecture; TVars in the axioms *)
val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
- val (axiom_names, axioms) =
- ListPair.unzip (map_filter (make_axiom ctxt true) axiom_pairs)
+ val (axiom_names, axioms) = ListPair.unzip (map_filter I prepared_axioms)
val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
val (supers', arity_clauses) = make_arity_clauses thy tycons supers
val class_rel_clauses = make_class_rel_clauses thy subs supers'
@@ -495,12 +498,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_pairs =
+ explicit_apply hyp_ts concl_t axiom_ts prepared_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_pairs
+ prepare_formulas ctxt full_types hyp_ts concl_t axiom_ts prepared_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