1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 12:07:09 2010 +0200
1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 14:39:43 2010 +0200
1.3 @@ -30,8 +30,7 @@
1.4 {subgoal: int,
1.5 goal: Proof.context * (thm list * thm),
1.6 relevance_override: relevance_override,
1.7 - axiom_clauses: (string * thm) list option,
1.8 - filtered_clauses: (string * thm) list option}
1.9 + axiom_clauses: (string * thm) list option}
1.10 type prover_result =
1.11 {outcome: failure option,
1.12 message: string,
1.13 @@ -41,8 +40,7 @@
1.14 output: string,
1.15 proof: string,
1.16 internal_thm_names: string Vector.vector,
1.17 - conjecture_shape: int list list,
1.18 - filtered_clauses: (string * thm) list}
1.19 + conjecture_shape: int list list}
1.20 type prover =
1.21 params -> minimize_command -> Time.time -> problem -> prover_result
1.22
1.23 @@ -100,8 +98,7 @@
1.24 {subgoal: int,
1.25 goal: Proof.context * (thm list * thm),
1.26 relevance_override: relevance_override,
1.27 - axiom_clauses: (string * thm) list option,
1.28 - filtered_clauses: (string * thm) list option}
1.29 + axiom_clauses: (string * thm) list option}
1.30
1.31 type prover_result =
1.32 {outcome: failure option,
1.33 @@ -112,8 +109,7 @@
1.34 output: string,
1.35 proof: string,
1.36 internal_thm_names: string Vector.vector,
1.37 - conjecture_shape: int list list,
1.38 - filtered_clauses: (string * thm) list}
1.39 + conjecture_shape: int list list}
1.40
1.41 type prover =
1.42 params -> minimize_command -> Time.time -> problem -> prover_result
1.43 @@ -345,14 +341,12 @@
1.44 fun s_not (@{const Not} $ t) = t
1.45 | s_not t = @{const Not} $ t
1.46
1.47 -(* prepare for passing to writer,
1.48 - create additional clauses based on the information from extra_cls *)
1.49 -fun prepare_clauses ctxt full_types hyp_ts concl_t axcls extra_cls =
1.50 +fun prepare_clauses ctxt full_types hyp_ts concl_t axcls =
1.51 let
1.52 val thy = ProofContext.theory_of ctxt
1.53 val goal_t = Logic.list_implies (hyp_ts, concl_t)
1.54 val is_FO = Meson.is_fol_term thy goal_t
1.55 - val axtms = map (prop_of o snd) extra_cls
1.56 + val axtms = map (prop_of o snd) axcls
1.57 val subs = tfree_classes_of_terms [goal_t]
1.58 val supers = tvar_classes_of_terms axtms
1.59 val tycons = type_consts_of_terms thy (goal_t :: axtms)
1.60 @@ -361,19 +355,16 @@
1.61 map (s_not o HOLogic.dest_Trueprop) hyp_ts @
1.62 [HOLogic.dest_Trueprop concl_t]
1.63 |> make_conjecture_clauses ctxt
1.64 - val extra_clauses = map (snd o make_axiom_clause ctxt) extra_cls
1.65 val (clnames, axiom_clauses) =
1.66 ListPair.unzip (map (make_axiom_clause ctxt) axcls)
1.67 - (* FIXME: Should it read "extra_clauses" or "axiom_clauses" in the
1.68 - "get_helper_clauses" call? *)
1.69 val helper_clauses =
1.70 - get_helper_clauses ctxt is_FO full_types conjectures extra_clauses
1.71 + get_helper_clauses ctxt is_FO full_types conjectures axiom_clauses
1.72 val (supers', arity_clauses) = make_arity_clauses thy tycons supers
1.73 val class_rel_clauses = make_class_rel_clauses thy subs supers'
1.74 in
1.75 (Vector.fromList clnames,
1.76 - (conjectures, axiom_clauses, extra_clauses, helper_clauses,
1.77 - class_rel_clauses, arity_clauses))
1.78 + (conjectures, axiom_clauses, helper_clauses, class_rel_clauses,
1.79 + arity_clauses))
1.80 end
1.81
1.82 fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
1.83 @@ -596,8 +587,8 @@
1.84 (const_table_for_problem explicit_apply problem) problem
1.85
1.86 fun write_tptp_file thy readable_names explicit_forall full_types explicit_apply
1.87 - file (conjectures, axiom_clauses, extra_clauses,
1.88 - helper_clauses, class_rel_clauses, arity_clauses) =
1.89 + file (conjectures, axiom_clauses, helper_clauses,
1.90 + class_rel_clauses, arity_clauses) =
1.91 let
1.92 val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
1.93 val class_rel_lines =
1.94 @@ -684,26 +675,23 @@
1.95 relevance_convergence, theory_relevant, defs_relevant, isar_proof,
1.96 isar_shrink_factor, ...} : params)
1.97 minimize_command timeout
1.98 - ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
1.99 - : problem) =
1.100 + ({subgoal, goal, relevance_override, axiom_clauses} : problem) =
1.101 let
1.102 (* get clauses and prepare them for writing *)
1.103 val (ctxt, (_, th)) = goal;
1.104 val thy = ProofContext.theory_of ctxt
1.105 (* ### FIXME: (1) preprocessing for "if" etc. *)
1.106 val (params, hyp_ts, concl_t) = strip_subgoal th subgoal
1.107 - val the_filtered_clauses =
1.108 - case filtered_clauses of
1.109 - SOME fcls => fcls
1.110 + val the_axiom_clauses =
1.111 + case axiom_clauses of
1.112 + SOME axioms => axioms
1.113 | NONE => relevant_facts full_types relevance_threshold
1.114 relevance_convergence defs_relevant
1.115 max_new_relevant_facts_per_iter
1.116 (the_default prefers_theory_relevant theory_relevant)
1.117 relevance_override goal hyp_ts concl_t
1.118 - val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
1.119 val (internal_thm_names, clauses) =
1.120 prepare_clauses ctxt full_types hyp_ts concl_t the_axiom_clauses
1.121 - the_filtered_clauses
1.122
1.123 (* path to unique problem file *)
1.124 val the_dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
1.125 @@ -814,8 +802,7 @@
1.126 {outcome = outcome, message = message, pool = pool,
1.127 used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,
1.128 output = output, proof = proof, internal_thm_names = internal_thm_names,
1.129 - conjecture_shape = conjecture_shape,
1.130 - filtered_clauses = the_filtered_clauses}
1.131 + conjecture_shape = conjecture_shape}
1.132 end
1.133
1.134 fun get_prover_fun thy name = prover_fun name (get_prover thy name)
1.135 @@ -837,8 +824,7 @@
1.136 let
1.137 val problem =
1.138 {subgoal = i, goal = (ctxt, (facts, goal)),
1.139 - relevance_override = relevance_override, axiom_clauses = NONE,
1.140 - filtered_clauses = NONE}
1.141 + relevance_override = relevance_override, axiom_clauses = NONE}
1.142 in
1.143 prover params (minimize_command name) timeout problem |> #message
1.144 handle ERROR message => "Error: " ^ message ^ "\n"
2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Thu Jul 29 12:07:09 2010 +0200
2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Thu Jul 29 14:39:43 2010 +0200
2.3 @@ -18,7 +18,6 @@
2.4 structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =
2.5 struct
2.6
2.7 -open Metis_Clauses
2.8 open Sledgehammer_Util
2.9 open Sledgehammer_Fact_Filter
2.10 open Sledgehammer_Proof_Reconstruct
2.11 @@ -37,7 +36,7 @@
2.12 | string_for_outcome (SOME failure) = string_for_failure failure
2.13
2.14 fun sledgehammer_test_theorems (params : params) prover timeout subgoal state
2.15 - filtered_clauses name_thms_pairs =
2.16 + name_thms_pairs =
2.17 let
2.18 val num_theorems = length name_thms_pairs
2.19 val _ =
2.20 @@ -54,8 +53,7 @@
2.21 val problem =
2.22 {subgoal = subgoal, goal = (ctxt, (facts, goal)),
2.23 relevance_override = {add = [], del = [], only = false},
2.24 - axiom_clauses = SOME name_thm_pairs,
2.25 - filtered_clauses = SOME (the_default name_thm_pairs filtered_clauses)}
2.26 + axiom_clauses = SOME name_thm_pairs}
2.27 in
2.28 prover params (K "") timeout problem
2.29 |> tap (fn result : prover_result =>
2.30 @@ -91,15 +89,14 @@
2.31 sledgehammer_test_theorems params prover minimize_timeout i state
2.32 val {context = ctxt, goal, ...} = Proof.goal state;
2.33 in
2.34 - (* try prove first to check result and get used theorems *)
2.35 - (case test_facts NONE name_thms_pairs of
2.36 - result as {outcome = NONE, pool, proof, used_thm_names,
2.37 - conjecture_shape, filtered_clauses, ...} =>
2.38 + (* FIXME: merge both "test_facts" calls *)
2.39 + (case test_facts name_thms_pairs of
2.40 + result as {outcome = NONE, pool, used_thm_names,
2.41 + conjecture_shape, ...} =>
2.42 let
2.43 val (min_thms, {proof, internal_thm_names, ...}) =
2.44 - sublinear_minimize (test_facts (SOME filtered_clauses))
2.45 - (filter_used_facts used_thm_names name_thms_pairs)
2.46 - ([], result)
2.47 + sublinear_minimize test_facts
2.48 + (filter_used_facts used_thm_names name_thms_pairs) ([], result)
2.49 val m = length min_thms
2.50 val _ = priority (cat_lines
2.51 ["Minimized: " ^ string_of_int m ^ " theorem" ^ plural_s m] ^ ".")