# HG changeset patch # User blanchet # Date 1283375401 -7200 # Node ID 42fcb25de0827b424fb90c4d867184270ee2b6e4 # Parent f1b465f889b5d002642f1d477966fa41122b9f7a minor refactoring diff -r f1b465f889b5 -r 42fcb25de082 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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 diff -r f1b465f889b5 -r 42fcb25de082 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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, ...} => diff -r f1b465f889b5 -r 42fcb25de082 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- 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 diff -r f1b465f889b5 -r 42fcb25de082 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- 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