1.1 --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jul 29 14:39:43 2010 +0200
1.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Thu Jul 29 14:42:09 2010 +0200
1.3 @@ -309,8 +309,7 @@
1.4 val params = Sledgehammer_Isar.default_params thy []
1.5 val problem =
1.6 {subgoal = 1, goal = (ctxt', (facts, goal)),
1.7 - relevance_override = {add = [], del = [], only = false},
1.8 - axiom_clauses = NONE, filtered_clauses = NONE}
1.9 + relevance_override = {add = [], del = [], only = false}, axioms = NONE}
1.10 val time_limit =
1.11 (case hard_timeout of
1.12 NONE => I
2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 14:39:43 2010 +0200
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 14:42:09 2010 +0200
2.3 @@ -30,7 +30,7 @@
2.4 {subgoal: int,
2.5 goal: Proof.context * (thm list * thm),
2.6 relevance_override: relevance_override,
2.7 - axiom_clauses: (string * thm) list option}
2.8 + axioms: (string * thm) list option}
2.9 type prover_result =
2.10 {outcome: failure option,
2.11 message: string,
2.12 @@ -98,7 +98,7 @@
2.13 {subgoal: int,
2.14 goal: Proof.context * (thm list * thm),
2.15 relevance_override: relevance_override,
2.16 - axiom_clauses: (string * thm) list option}
2.17 + axioms: (string * thm) list option}
2.18
2.19 type prover_result =
2.20 {outcome: failure option,
2.21 @@ -355,16 +355,14 @@
2.22 map (s_not o HOLogic.dest_Trueprop) hyp_ts @
2.23 [HOLogic.dest_Trueprop concl_t]
2.24 |> make_conjecture_clauses ctxt
2.25 - val (clnames, axiom_clauses) =
2.26 - ListPair.unzip (map (make_axiom_clause ctxt) axcls)
2.27 + val (clnames, axioms) = ListPair.unzip (map (make_axiom_clause ctxt) axcls)
2.28 val helper_clauses =
2.29 - get_helper_clauses ctxt is_FO full_types conjectures axiom_clauses
2.30 + get_helper_clauses ctxt is_FO full_types conjectures axioms
2.31 val (supers', arity_clauses) = make_arity_clauses thy tycons supers
2.32 val class_rel_clauses = make_class_rel_clauses thy subs supers'
2.33 in
2.34 (Vector.fromList clnames,
2.35 - (conjectures, axiom_clauses, helper_clauses, class_rel_clauses,
2.36 - arity_clauses))
2.37 + (conjectures, axioms, helper_clauses, class_rel_clauses, arity_clauses))
2.38 end
2.39
2.40 fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
2.41 @@ -587,10 +585,10 @@
2.42 (const_table_for_problem explicit_apply problem) problem
2.43
2.44 fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply
2.45 - file (conjectures, axiom_clauses, helper_clauses,
2.46 + file (conjectures, axioms, helper_clauses,
2.47 class_rel_clauses, arity_clauses) =
2.48 let
2.49 - val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
2.50 + val axiom_lines = map (problem_line_for_axiom full_types) axioms
2.51 val class_rel_lines =
2.52 map problem_line_for_class_rel_clause class_rel_clauses
2.53 val arity_lines = map problem_line_for_arity_clause arity_clauses
2.54 @@ -675,15 +673,15 @@
2.55 relevance_convergence, theory_relevant, defs_relevant, isar_proof,
2.56 isar_shrink_factor, ...} : params)
2.57 minimize_command timeout
2.58 - ({subgoal, goal, relevance_override, axiom_clauses} : problem) =
2.59 + ({subgoal, goal, relevance_override, axioms} : problem) =
2.60 let
2.61 (* get clauses and prepare them for writing *)
2.62 val (ctxt, (_, th)) = goal;
2.63 val thy = ProofContext.theory_of ctxt
2.64 (* ### FIXME: (1) preprocessing for "if" etc. *)
2.65 val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
2.66 - val the_axiom_clauses =
2.67 - case axiom_clauses of
2.68 + val the_axioms =
2.69 + case axioms of
2.70 SOME axioms => axioms
2.71 | NONE => relevant_facts full_types relevance_threshold
2.72 relevance_convergence defs_relevant
2.73 @@ -691,7 +689,7 @@
2.74 (the_default prefers_theory_relevant theory_relevant)
2.75 relevance_override goal hyp_ts concl_t
2.76 val (internal_thm_names, clauses) =
2.77 - prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses
2.78 + prepare_clauses ctxt full_types hyp_ts concl_t the_axioms
2.79
2.80 (* path to unique problem file *)
2.81 val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
2.82 @@ -824,7 +822,7 @@
2.83 let
2.84 val problem =
2.85 {subgoal = i, goal = (ctxt, (facts, goal)),
2.86 - relevance_override = relevance_override, axiom_clauses = NONE}
2.87 + relevance_override = relevance_override, axioms = NONE}
2.88 in
2.89 prover params (minimize_command name) timeout problem |> #message
2.90 handle ERROR message => "Error: " ^ message ^ "\n"
3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Thu Jul 29 14:39:43 2010 +0200
3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Thu Jul 29 14:42:09 2010 +0200
3.3 @@ -38,22 +38,22 @@
3.4 fun sledgehammer_test_theorems (params : params) prover timeout subgoal state
3.5 name_thms_pairs =
3.6 let
3.7 - val num_theorems = length name_thms_pairs
3.8 + val num_axioms = length name_thms_pairs
3.9 val _ =
3.10 - priority ("Testing " ^ string_of_int num_theorems ^
3.11 - " theorem" ^ plural_s num_theorems ^
3.12 - (if num_theorems > 0 then
3.13 + priority ("Testing " ^ string_of_int num_axioms ^
3.14 + " theorem" ^ plural_s num_axioms ^
3.15 + (if num_axioms > 0 then
3.16 ": " ^ space_implode " "
3.17 (name_thms_pairs
3.18 |> map fst |> sort_distinct string_ord)
3.19 else
3.20 "") ^ "...")
3.21 - val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
3.22 + val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
3.23 val {context = ctxt, facts, goal} = Proof.goal state
3.24 val problem =
3.25 {subgoal = subgoal, goal = (ctxt, (facts, goal)),
3.26 relevance_override = {add = [], del = [], only = false},
3.27 - axiom_clauses = SOME name_thm_pairs}
3.28 + axioms = SOME axioms}
3.29 in
3.30 prover params (K "") timeout problem
3.31 |> tap (fn result : prover_result =>