--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Sep 01 23:03:31 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,162 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML
- Author: Philipp Meyer, TU Muenchen
- Author: Jasmin Blanchette, TU Muenchen
-
-Minimization of theorem list for Metis using automatic theorem provers.
-*)
-
-signature SLEDGEHAMMER_FACT_MINIMIZE =
-sig
- type locality = Sledgehammer_Fact_Filter.locality
- type params = Sledgehammer.params
-
- val minimize_theorems :
- params -> int -> int -> Proof.state -> ((string * locality) * thm list) list
- -> ((string * locality) * thm list) list option * string
- val run_minimize : params -> int -> Facts.ref list -> Proof.state -> unit
-end;
-
-structure Sledgehammer_Fact_Minimize : SLEDGEHAMMER_FACT_MINIMIZE =
-struct
-
-open ATP_Systems
-open Sledgehammer_Util
-open Sledgehammer_Fact_Filter
-open Sledgehammer_Proof_Reconstruct
-open Sledgehammer
-
-(* wrapper for calling external prover *)
-
-fun string_for_failure Unprovable = "Unprovable."
- | string_for_failure TimedOut = "Timed out."
- | string_for_failure _ = "Unknown error."
-
-fun n_theorems names =
- let val n = length names in
- string_of_int n ^ " theorem" ^ plural_s n ^
- (if n > 0 then
- ": " ^ (names |> map fst
- |> sort_distinct string_ord |> space_implode " ")
- else
- "")
- end
-
-fun test_theorems ({debug, verbose, overlord, atps, full_types, isar_proof,
- isar_shrink_factor, ...} : params)
- (prover : prover) explicit_apply timeout subgoal state
- axioms =
- let
- val _ =
- priority ("Testing " ^ n_theorems (map fst axioms) ^ "...")
- val params =
- {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
- full_types = full_types, explicit_apply = explicit_apply,
- relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
- theory_relevant = NONE, isar_proof = isar_proof,
- isar_shrink_factor = isar_shrink_factor, timeout = timeout}
- val axioms = maps (fn (n, ths) => map (pair n) ths) axioms
- val {context = ctxt, facts, goal} = Proof.goal state
- val problem =
- {subgoal = subgoal, goal = (ctxt, (facts, goal)),
- relevance_override = {add = [], del = [], only = false},
- axioms = SOME axioms}
- val result as {outcome, used_thm_names, ...} = prover params (K "") problem
- in
- priority (case outcome of
- NONE =>
- if length used_thm_names = length axioms then
- "Found proof."
- else
- "Found proof with " ^ n_theorems used_thm_names ^ "."
- | SOME failure => string_for_failure failure);
- result
- end
-
-(* minimalization of thms *)
-
-fun filter_used_facts used = filter (member (op =) used o fst)
-
-fun sublinear_minimize _ [] p = p
- | sublinear_minimize test (x :: xs) (seen, result) =
- case test (xs @ seen) of
- result as {outcome = NONE, proof, used_thm_names, ...} : prover_result =>
- sublinear_minimize test (filter_used_facts used_thm_names xs)
- (filter_used_facts used_thm_names seen, result)
- | _ => sublinear_minimize test xs (x :: seen, result)
-
-(* Give the ATP some slack. The ATP gets further slack because the Sledgehammer
- preprocessing time is included in the estimate below but isn't part of the
- timeout. *)
-val fudge_msecs = 1000
-
-fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set."
- | minimize_theorems (params as {debug, atps = atp :: _, full_types,
- isar_proof, isar_shrink_factor, timeout, ...})
- i n state axioms =
- let
- val thy = Proof.theory_of state
- val prover = get_prover_fun thy atp
- val msecs = Time.toMilliseconds timeout
- val _ = priority ("Sledgehammer minimize: ATP " ^ quote atp ^ ".")
- val {context = ctxt, goal, ...} = Proof.goal state
- val (_, hyp_ts, concl_t) = strip_subgoal goal i
- val explicit_apply =
- not (forall (Meson.is_fol_term thy)
- (concl_t :: hyp_ts @ maps (map prop_of o snd) axioms))
- fun do_test timeout =
- test_theorems params prover explicit_apply timeout i state
- val timer = Timer.startRealTimer ()
- in
- (case do_test timeout axioms of
- result as {outcome = NONE, pool, used_thm_names,
- conjecture_shape, ...} =>
- let
- val time = Timer.checkRealTimer timer
- val new_timeout =
- Int.min (msecs, Time.toMilliseconds time + fudge_msecs)
- |> Time.fromMilliseconds
- val (min_thms, {proof, axiom_names, ...}) =
- sublinear_minimize (do_test new_timeout)
- (filter_used_facts used_thm_names axioms) ([], result)
- val n = length min_thms
- val _ = priority (cat_lines
- ["Minimized: " ^ string_of_int n ^ " theorem" ^ plural_s n] ^
- (case length (filter (curry (op =) Chained o snd o fst) min_thms) of
- 0 => ""
- | n => " (including " ^ Int.toString n ^ " chained)") ^ ".")
- in
- (SOME min_thms,
- proof_text isar_proof
- (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
- (full_types, K "", proof, axiom_names, goal, i) |> fst)
- end
- | {outcome = SOME TimedOut, ...} =>
- (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
- \option (e.g., \"timeout = " ^
- string_of_int (10 + msecs div 1000) ^ " s\").")
- | {outcome = SOME UnknownError, ...} =>
- (* Failure sometimes mean timeout, unfortunately. *)
- (NONE, "Failure: No proof was found with the current time limit. You \
- \can increase the time limit using the \"timeout\" \
- \option (e.g., \"timeout = " ^
- string_of_int (10 + msecs div 1000) ^ " s\").")
- | {message, ...} => (NONE, "ATP error: " ^ message))
- handle ERROR msg => (NONE, "Error: " ^ msg)
- end
-
-fun run_minimize params i refs state =
- let
- val ctxt = Proof.context_of state
- val reserved = reserved_isar_keyword_table ()
- val chained_ths = #facts (Proof.goal state)
- val axioms =
- maps (map (apsnd single)
- o name_thm_pairs_from_ref ctxt reserved chained_ths) refs
- in
- case subgoal_count state of
- 0 => priority "No subgoal!"
- | n =>
- (kill_atps (); priority (#2 (minimize_theorems params i n state axioms)))
- end
-
-end;