# HG changeset patch # User blanchet # Date 1280407329 -7200 # Node ID e2aac207d13b8c58070ab29c3883b2ea995fc347 # Parent c4b57f68ddb3ff6f1e2dfd135ffc7cd726f43505 "axiom_clauses" -> "axioms" (these are no longer clauses) diff -r c4b57f68ddb3 -r e2aac207d13b src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jul 29 14:39:43 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jul 29 14:42:09 2010 +0200 @@ -309,8 +309,7 @@ val params = Sledgehammer_Isar.default_params thy [] val problem = {subgoal = 1, goal = (ctxt', (facts, goal)), - relevance_override = {add = [], del = [], only = false}, - axiom_clauses = NONE, filtered_clauses = NONE} + relevance_override = {add = [], del = [], only = false}, axioms = NONE} val time_limit = (case hard_timeout of NONE => I diff -r c4b57f68ddb3 -r e2aac207d13b src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 14:39:43 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 14:42:09 2010 +0200 @@ -30,7 +30,7 @@ {subgoal: int, goal: Proof.context * (thm list * thm), relevance_override: relevance_override, - axiom_clauses: (string * thm) list option} + axioms: (string * thm) list option} type prover_result = {outcome: failure option, message: string, @@ -98,7 +98,7 @@ {subgoal: int, goal: Proof.context * (thm list * thm), relevance_override: relevance_override, - axiom_clauses: (string * thm) list option} + axioms: (string * thm) list option} type prover_result = {outcome: failure option, @@ -355,16 +355,14 @@ map (s_not o HOLogic.dest_Trueprop) hyp_ts @ [HOLogic.dest_Trueprop concl_t] |> make_conjecture_clauses ctxt - val (clnames, axiom_clauses) = - ListPair.unzip (map (make_axiom_clause ctxt) axcls) + val (clnames, axioms) = ListPair.unzip (map (make_axiom_clause ctxt) axcls) val helper_clauses = - get_helper_clauses ctxt is_FO full_types conjectures axiom_clauses + get_helper_clauses 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' in (Vector.fromList clnames, - (conjectures, axiom_clauses, helper_clauses, class_rel_clauses, - arity_clauses)) + (conjectures, axioms, helper_clauses, class_rel_clauses, arity_clauses)) end fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t]) @@ -587,10 +585,10 @@ (const_table_for_problem explicit_apply problem) problem fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply - file (conjectures, axiom_clauses, helper_clauses, + file (conjectures, axioms, helper_clauses, class_rel_clauses, arity_clauses) = let - val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses + val axiom_lines = map (problem_line_for_axiom full_types) axioms val class_rel_lines = map problem_line_for_class_rel_clause class_rel_clauses val arity_lines = map problem_line_for_arity_clause arity_clauses @@ -675,15 +673,15 @@ relevance_convergence, theory_relevant, defs_relevant, isar_proof, isar_shrink_factor, ...} : params) minimize_command timeout - ({subgoal, goal, relevance_override, axiom_clauses} : problem) = + ({subgoal, goal, relevance_override, axioms} : problem) = let (* get clauses and prepare them for writing *) val (ctxt, (_, th)) = goal; val thy = ProofContext.theory_of ctxt (* ### FIXME: (1) preprocessing for "if" etc. *) val (params, hyp_ts, concl_t) = strip_subgoal th subgoal - val the_axiom_clauses = - case axiom_clauses of + val the_axioms = + case axioms of SOME axioms => axioms | NONE => relevant_facts full_types relevance_threshold relevance_convergence defs_relevant @@ -691,7 +689,7 @@ (the_default prefers_theory_relevant theory_relevant) relevance_override goal hyp_ts concl_t val (internal_thm_names, clauses) = - prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses + prepare_clauses ctxt full_types hyp_ts concl_t the_axioms (* path to unique problem file *) val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER" @@ -824,7 +822,7 @@ let val problem = {subgoal = i, goal = (ctxt, (facts, goal)), - relevance_override = relevance_override, axiom_clauses = NONE} + relevance_override = relevance_override, axioms = NONE} in prover params (minimize_command name) timeout problem |> #message handle ERROR message => "Error: " ^ message ^ "\n" diff -r c4b57f68ddb3 -r e2aac207d13b src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Thu Jul 29 14:39:43 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Thu Jul 29 14:42:09 2010 +0200 @@ -38,22 +38,22 @@ fun sledgehammer_test_theorems (params : params) prover timeout subgoal state name_thms_pairs = let - val num_theorems = length name_thms_pairs + val num_axioms = length name_thms_pairs val _ = - priority ("Testing " ^ string_of_int num_theorems ^ - " theorem" ^ plural_s num_theorems ^ - (if num_theorems > 0 then + priority ("Testing " ^ string_of_int num_axioms ^ + " theorem" ^ plural_s num_axioms ^ + (if num_axioms > 0 then ": " ^ space_implode " " (name_thms_pairs |> map fst |> sort_distinct string_ord) else "") ^ "...") - val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs + val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs val {context = ctxt, facts, goal} = Proof.goal state val problem = {subgoal = subgoal, goal = (ctxt, (facts, goal)), relevance_override = {add = [], del = [], only = false}, - axiom_clauses = SOME name_thm_pairs} + axioms = SOME axioms} in prover params (K "") timeout problem |> tap (fn result : prover_result =>