--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jan 31 10:23:32 2014 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Jan 31 10:23:32 2014 +0100
@@ -376,8 +376,7 @@
let
val learn = Sledgehammer_MaSh.mash_learn_proof ctxt params (prop_of goal) all_facts
in
- Sledgehammer_Minimize.get_minimizing_prover ctxt Sledgehammer_Prover.Normal
- learn name
+ Sledgehammer_Prover_Minimize.get_minimizing_prover ctxt Sledgehammer_Prover.Normal learn name
end
type stature = ATP_Problem_Generate.stature
@@ -488,7 +487,7 @@
Sledgehammer_Fact.no_fact_override hyp_ts concl_t
|> tap (fn factss =>
"Line " ^ str0 (Position.line_of pos) ^ ": " ^
- Sledgehammer_Run.string_of_factss factss
+ Sledgehammer.string_of_factss factss
|> Output.urgent_message)
val prover = get_prover ctxt prover_name params goal facts
val problem =
@@ -608,7 +607,7 @@
|> max_new_mono_instancesLST
|> max_mono_itersLST)
val minimize =
- Sledgehammer_Minimize.minimize_facts (K ()) prover_name params true 1
+ Sledgehammer_Prover_Minimize.minimize_facts (K ()) prover_name params true 1
(Sledgehammer_Util.subgoal_count st)
val _ = log separator
val (used_facts, (preplay, message, message_tail)) =
--- a/src/HOL/Sledgehammer.thy Fri Jan 31 10:23:32 2014 +0100
+++ b/src/HOL/Sledgehammer.thy Fri Jan 31 10:23:32 2014 +0100
@@ -16,21 +16,21 @@
ML_file "Tools/Sledgehammer/async_manager.ML"
ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"
ML_file "Tools/Sledgehammer/sledgehammer_fact.ML"
ML_file "Tools/Sledgehammer/sledgehammer_reconstructor.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_proof.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_print.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_preplay.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_compress.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_try0.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_minimize_isar.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_isar_proof.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_isar_annotate.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_isar_print.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_isar_preplay.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_isar_compress.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_isar_try0.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_isar_minimize.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_isar.ML"
ML_file "Tools/Sledgehammer/sledgehammer_prover.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_minimize.ML"
+ML_file "Tools/Sledgehammer/sledgehammer_prover_minimize.ML"
ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML"
ML_file "Tools/Sledgehammer/sledgehammer_mash.ML"
-ML_file "Tools/Sledgehammer/sledgehammer_run.ML"
+ML_file "Tools/Sledgehammer/sledgehammer.ML"
ML_file "Tools/Sledgehammer/sledgehammer_commands.ML"
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Jan 31 10:23:32 2014 +0100
@@ -0,0 +1,302 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer.ML
+ Author: Fabian Immler, TU Muenchen
+ Author: Makarius
+ Author: Jasmin Blanchette, TU Muenchen
+
+Sledgehammer's heart.
+*)
+
+signature SLEDGEHAMMER =
+sig
+ type fact = Sledgehammer_Fact.fact
+ type fact_override = Sledgehammer_Fact.fact_override
+ type minimize_command = Sledgehammer_Reconstructor.minimize_command
+ type mode = Sledgehammer_Prover.mode
+ type params = Sledgehammer_Prover.params
+
+ val someN : string
+ val noneN : string
+ val timeoutN : string
+ val unknownN : string
+ val string_of_factss : (string * fact list) list -> string
+ val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override ->
+ ((string * string list) list -> string -> minimize_command) -> Proof.state ->
+ bool * (string * Proof.state)
+end;
+
+structure Sledgehammer : SLEDGEHAMMER =
+struct
+
+open ATP_Util
+open ATP_Problem_Generate
+open ATP_Proof
+open ATP_Proof_Reconstruct
+open Sledgehammer_Util
+open Sledgehammer_Fact
+open Sledgehammer_Prover
+open Sledgehammer_Prover_Minimize
+open Sledgehammer_MaSh
+
+val someN = "some"
+val noneN = "none"
+val timeoutN = "timeout"
+val unknownN = "unknown"
+
+val ordered_outcome_codes = [someN, unknownN, timeoutN, noneN]
+
+fun max_outcome_code codes =
+ NONE
+ |> fold (fn candidate =>
+ fn accum as SOME _ => accum
+ | NONE => if member (op =) codes candidate then SOME candidate
+ else NONE)
+ ordered_outcome_codes
+ |> the_default unknownN
+
+fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i
+ n goal =
+ (quote name,
+ (if verbose then
+ " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
+ else
+ "") ^
+ " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^
+ (if blocking then "."
+ else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
+
+fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, expect, ...}) mode
+ output_result minimize_command only learn
+ {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
+ let
+ val ctxt = Proof.context_of state
+
+ val hard_timeout = time_mult 3.0 timeout
+ val _ = spying spy (fn () => (state, subgoal, name, "Launched"));
+ val birth_time = Time.now ()
+ val death_time = Time.+ (birth_time, hard_timeout)
+ val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name)
+ val num_facts = length facts |> not only ? Integer.min max_facts
+
+ fun desc () = prover_description ctxt params name num_facts subgoal subgoal_count goal
+
+ val problem =
+ {comment = comment, state = state, goal = goal, subgoal = subgoal,
+ subgoal_count = subgoal_count,
+ factss = factss
+ |> map (apsnd ((not (is_ho_atp ctxt name)
+ ? filter_out (fn ((_, (_, Induction)), _) => true
+ | _ => false))
+ #> take num_facts))}
+
+ fun print_used_facts used_facts used_from =
+ tag_list 1 used_from
+ |> map (fn (j, fact) => fact |> apsnd (K j))
+ |> filter_used_facts false used_facts
+ |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
+ |> commas
+ |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
+ " proof (of " ^ string_of_int (length facts) ^ "): ") "."
+ |> Output.urgent_message
+
+ fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) =
+ let
+ val num_used_facts = length used_facts
+
+ fun find_indices facts =
+ tag_list 1 facts
+ |> map (fn (j, fact) => fact |> apsnd (K j))
+ |> filter_used_facts false used_facts
+ |> distinct (eq_fst (op =))
+ |> map (prefix "@" o string_of_int o snd)
+
+ fun filter_info (fact_filter, facts) =
+ let
+ val indices = find_indices facts
+ (* "Int.max" is there for robustness -- it shouldn't be necessary *)
+ val unknowns = replicate (Int.max (0, num_used_facts - length indices)) "?"
+ in
+ (commas (indices @ unknowns), fact_filter)
+ end
+
+ val filter_infos =
+ map filter_info (("actual", used_from) :: factss)
+ |> AList.group (op =)
+ |> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices)
+ in
+ "Success: Found proof with " ^ string_of_int num_used_facts ^
+ " of " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
+ (if num_used_facts = 0 then "" else ": " ^ commas filter_infos)
+ end
+ | spying_str_of_res {outcome = SOME failure, ...} =
+ "Failure: " ^ string_of_atp_failure failure
+
+ fun really_go () =
+ problem
+ |> get_minimizing_prover ctxt mode learn name params minimize_command
+ |> verbose
+ ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} =>
+ print_used_facts used_facts used_from
+ | _ => ())
+ |> spy
+ ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
+ |> (fn {outcome, preplay, message, message_tail, ...} =>
+ (if outcome = SOME ATP_Proof.TimedOut then timeoutN
+ else if is_some outcome then noneN
+ else someN, fn () => message (Lazy.force preplay) ^ message_tail))
+
+ fun go () =
+ let
+ val (outcome_code, message) =
+ if debug then
+ really_go ()
+ else
+ (really_go ()
+ handle ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n")
+ | exn =>
+ if Exn.is_interrupt exn then
+ reraise exn
+ else
+ (unknownN, fn () => "Internal error:\n" ^
+ ML_Compiler.exn_message exn ^ "\n"))
+ val _ =
+ (* The "expect" argument is deliberately ignored if the prover is
+ missing so that the "Metis_Examples" can be processed on any
+ machine. *)
+ if expect = "" orelse outcome_code = expect orelse
+ not (is_prover_installed ctxt name) then
+ ()
+ else if blocking then
+ error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
+ else
+ warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
+ in (outcome_code, message) end
+ in
+ if mode = Auto_Try then
+ let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
+ (outcome_code,
+ state
+ |> outcome_code = someN
+ ? Proof.goal_message (fn () =>
+ Pretty.mark Markup.information (Pretty.str (message ()))))
+ end
+ else if blocking then
+ let
+ val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
+ val outcome =
+ if outcome_code = someN orelse mode = Normal then
+ quote name ^ ": " ^ message ()
+ else ""
+ val _ =
+ if outcome <> "" andalso is_some output_result then
+ the output_result outcome
+ else
+ outcome
+ |> Async_Manager.break_into_chunks
+ |> List.app Output.urgent_message
+ in (outcome_code, state) end
+ else
+ (Async_Manager.thread SledgehammerN birth_time death_time (desc ())
+ ((fn (outcome_code, message) =>
+ (verbose orelse outcome_code = someN,
+ message ())) o go);
+ (unknownN, state))
+ end
+
+val auto_try_max_facts_divisor = 2 (* FUDGE *)
+
+fun string_of_facts facts =
+ "Including " ^ string_of_int (length facts) ^
+ " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
+ (facts |> map (fst o fst) |> space_implode " ") ^ "."
+
+fun string_of_factss factss =
+ if forall (null o snd) factss then
+ "Found no relevant facts."
+ else case factss of
+ [(_, facts)] => string_of_facts facts
+ | _ =>
+ factss
+ |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts)
+ |> space_implode "\n\n"
+
+fun run_sledgehammer (params as {debug, verbose, spy, blocking, provers, max_facts, ...}) mode
+ output_result i (fact_override as {only, ...}) minimize_command state =
+ if null provers then
+ error "No prover is set."
+ else case subgoal_count state of
+ 0 =>
+ ((if blocking then error else Output.urgent_message) "No subgoal!"; (false, (noneN, state)))
+ | n =>
+ let
+ val _ = Proof.assert_backward state
+ val print =
+ if mode = Normal andalso is_none output_result then Output.urgent_message else K ()
+ val state = state |> Proof.map_context (Config.put SMT_Config.verbose debug)
+ val ctxt = Proof.context_of state
+ val {facts = chained, goal, ...} = Proof.goal state
+ val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
+ val ho_atp = exists (is_ho_atp ctxt) provers
+ val reserved = reserved_isar_keyword_table ()
+ val css = clasimpset_rule_table_of ctxt
+ val all_facts =
+ nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts
+ concl_t
+ val _ = () |> not blocking ? kill_provers
+ val _ = case find_first (not o is_prover_supported ctxt) provers of
+ SOME name => error ("No such prover: " ^ name ^ ".")
+ | NONE => ()
+ val _ = print "Sledgehammering..."
+ val _ = spying spy (fn () => (state, i, "***", "Starting " ^ @{make_string} mode ^ " mode"))
+
+ val spying_str_of_factss =
+ commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts))
+
+ fun get_factss provers =
+ let
+ val max_max_facts =
+ case max_facts of
+ SOME n => n
+ | NONE =>
+ 0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers
+ |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)
+ val _ = spying spy (fn () => (state, i, "All",
+ "Filtering " ^ string_of_int (length all_facts) ^ " facts"));
+ in
+ all_facts
+ |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t
+ |> tap (fn factss => if verbose then print (string_of_factss factss) else ())
+ |> spy ? tap (fn factss => spying spy (fn () =>
+ (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss)))
+ end
+
+ fun launch_provers state =
+ let
+ val factss = get_factss provers
+ val problem =
+ {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
+ factss = factss}
+ val learn = mash_learn_proof ctxt params (prop_of goal) all_facts
+ val launch = launch_prover params mode output_result minimize_command only learn
+ in
+ if mode = Auto_Try then
+ (unknownN, state)
+ |> fold (fn prover => fn accum as (outcome_code, _) =>
+ if outcome_code = someN then accum
+ else launch problem prover)
+ provers
+ else
+ provers
+ |> (if blocking then Par_List.map else map) (launch problem #> fst)
+ |> max_outcome_code |> rpair state
+ end
+
+ fun maybe f (accum as (outcome_code, _)) =
+ accum |> (mode = Normal orelse outcome_code <> someN) ? f
+ in
+ (if blocking then launch_provers state
+ else (Future.fork (tap (fn () => launch_provers state)); (unknownN, state)))
+ handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (unknownN, state))
+ end
+ |> `(fn (outcome_code, _) => outcome_code = someN)
+
+end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML Fri Jan 31 10:23:32 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,214 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_annotate.ML
- Author: Jasmin Blanchette, TU Muenchen
- Author: Steffen Juilf Smolka, TU Muenchen
-
-Supplements term with a locally minmal, complete set of type constraints.
-Complete: The constraints suffice to infer the term's types.
-Minimal: Reducing the set of constraints further will make it incomplete.
-
-When configuring the pretty printer appropriately, the constraints will show up
-as type annotations when printing the term. This allows the term to be printed
-and reparsed without a change of types.
-
-NOTE: Terms should be unchecked before calling annotate_types to avoid awkward
-syntax.
-*)
-
-signature SLEDGEHAMMER_ANNOTATE =
-sig
- val annotate_types : Proof.context -> term -> term
-end;
-
-structure Sledgehammer_Annotate : SLEDGEHAMMER_ANNOTATE =
-struct
-
-(* Util *)
-fun post_traverse_term_type' f _ (t as Const (_, T)) s = f t T s
- | post_traverse_term_type' f _ (t as Free (_, T)) s = f t T s
- | post_traverse_term_type' f _ (t as Var (_, T)) s = f t T s
- | post_traverse_term_type' f env (t as Bound i) s = f t (nth env i) s
- | post_traverse_term_type' f env (Abs (x, T1, b)) s =
- let
- val ((b', s'), T2) = post_traverse_term_type' f (T1 :: env) b s
- in f (Abs (x, T1, b')) (T1 --> T2) s' end
- | post_traverse_term_type' f env (u $ v) s =
- let
- val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s
- val ((v', s''), _) = post_traverse_term_type' f env v s'
- in f (u' $ v') T s'' end
- handle Bind => raise Fail "Sledgehammer_Annotate: post_traverse_term_type'"
-
-fun post_traverse_term_type f s t =
- post_traverse_term_type' (fn t => fn T => fn s => (f t T s, T)) [] t s |> fst
-fun post_fold_term_type f s t =
- post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd
-
-fun fold_map_atypes f T s =
- case T of
- Type (name, Ts) =>
- let val (Ts, s) = fold_map (fold_map_atypes f) Ts s in
- (Type (name, Ts), s)
- end
- | _ => f T s
-
-(** get unique elements of a list **)
-local
- fun unique' b x [] = if b then [x] else []
- | unique' b x (y :: ys) =
- if x = y then unique' false x ys
- else unique' true y ys |> b ? cons x
-in
- fun unique ord xs =
- case sort ord xs of x :: ys => unique' true x ys | [] => []
-end
-
-(** Data structures, orders **)
-val indexname_ord = Term_Ord.fast_indexname_ord
-val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)
-structure Var_Set_Tab = Table(
- type key = indexname list
- val ord = list_ord indexname_ord)
-
-(* (1) Generalize types *)
-fun generalize_types ctxt t =
- let
- val erase_types = map_types (fn _ => dummyT)
- (* use schematic type variables *)
- val ctxt = ctxt |> Proof_Context.set_mode Proof_Context.mode_pattern
- val infer_types = singleton (Type_Infer_Context.infer_types ctxt)
- in
- t |> erase_types |> infer_types
- end
-
-(* (2) match types *)
-fun match_types ctxt t1 t2 =
- let
- val thy = Proof_Context.theory_of ctxt
- val get_types = post_fold_term_type (K cons) []
- in
- fold (Sign.typ_match thy) (get_types t1 ~~ get_types t2) Vartab.empty
- handle Type.TYPE_MATCH => raise Fail "Sledgehammer_Annotate: match_types"
- end
-
-
-(* (3) handle trivial tfrees *)
-fun handle_trivial_tfrees ctxt (t', subst) =
- let
- val add_tfree_names =
- snd #> snd #> fold_atyps (fn TFree (x, _) => cons x | _ => I)
-
- val trivial_tfree_names =
- Vartab.fold add_tfree_names subst []
- |> filter_out (Variable.is_declared ctxt)
- |> unique fast_string_ord
- val tfree_name_trivial = Ord_List.member fast_string_ord trivial_tfree_names
-
- val trivial_tvar_names =
- Vartab.fold
- (fn (tvar_name, (_, TFree (tfree_name, _))) =>
- tfree_name_trivial tfree_name ? cons tvar_name
- | _ => I)
- subst
- []
- |> sort indexname_ord
- val tvar_name_trivial = Ord_List.member indexname_ord trivial_tvar_names
-
- val t' =
- t' |> map_types
- (map_type_tvar
- (fn (idxn, sort) =>
- if tvar_name_trivial idxn then dummyT else TVar (idxn, sort)))
-
- val subst =
- subst |> fold Vartab.delete trivial_tvar_names
- |> Vartab.map
- (K (apsnd (map_type_tfree
- (fn (name, sort) =>
- if tfree_name_trivial name then dummyT
- else TFree (name, sort)))))
- in
- (t', subst)
- end
-
-
-(* (4) Typing-spot table *)
-local
-fun key_of_atype (TVar (z, _)) = Ord_List.insert indexname_ord z
- | key_of_atype _ = I
-fun key_of_type T = fold_atyps key_of_atype T []
-fun update_tab t T (tab, pos) =
- (case key_of_type T of
- [] => tab
- | key =>
- let val cost = (size_of_typ T, (size_of_term t, pos)) in
- case Var_Set_Tab.lookup tab key of
- NONE => Var_Set_Tab.update_new (key, cost) tab
- | SOME old_cost =>
- (case cost_ord (cost, old_cost) of
- LESS => Var_Set_Tab.update (key, cost) tab
- | _ => tab)
- end,
- pos + 1)
-in
-val typing_spot_table =
- post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst
-end
-
-(* (5) Reverse-greedy *)
-fun reverse_greedy typing_spot_tab =
- let
- fun update_count z =
- fold (fn tvar => fn tab =>
- let val c = Vartab.lookup tab tvar |> the_default 0 in
- Vartab.update (tvar, c + z) tab
- end)
- fun superfluous tcount =
- forall (fn tvar => the (Vartab.lookup tcount tvar) > 1)
- fun drop_superfluous (tvars, (_, (_, spot))) (spots, tcount) =
- if superfluous tcount tvars then (spots, update_count ~1 tvars tcount)
- else (spot :: spots, tcount)
- val (typing_spots, tvar_count_tab) =
- Var_Set_Tab.fold
- (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k))
- typing_spot_tab ([], Vartab.empty)
- |>> sort_distinct (rev_order o cost_ord o pairself snd)
- in fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst end
-
-(* (6) Introduce annotations *)
-fun introduce_annotations subst spots t t' =
- let
- fun subst_atype (T as TVar (idxn, S)) subst =
- (Envir.subst_type subst T, Vartab.update (idxn, (S, dummyT)) subst)
- | subst_atype T subst = (T, subst)
- val subst_type = fold_map_atypes subst_atype
- fun collect_annot _ T (subst, cp, ps as p :: ps', annots) =
- if p <> cp then
- (subst, cp + 1, ps, annots)
- else
- let val (T, subst) = subst_type T subst in
- (subst, cp + 1, ps', (p, T)::annots)
- end
- | collect_annot _ _ x = x
- val (_, _, _, annots) =
- post_fold_term_type collect_annot (subst, 0, spots, []) t'
- fun insert_annot t _ (cp, annots as (p, T) :: annots') =
- if p <> cp then (t, (cp + 1, annots)) else (Type.constraint T t, (cp + 1, annots'))
- | insert_annot t _ x = (t, x)
- in
- t |> post_traverse_term_type insert_annot (0, rev annots)
- |> fst
- end
-
-(* (7) Annotate *)
-fun annotate_types ctxt t =
- let
- val t' = generalize_types ctxt t
- val subst = match_types ctxt t' t
- val (t', subst) = (t', subst) |> handle_trivial_tfrees ctxt
- val typing_spots =
- t' |> typing_spot_table
- |> reverse_greedy
- |> sort int_ord
- in introduce_annotations subst typing_spots t t' end
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Jan 31 10:23:32 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Jan 31 10:23:32 2014 +0100
@@ -22,9 +22,9 @@
open Sledgehammer_Util
open Sledgehammer_Fact
open Sledgehammer_Prover
-open Sledgehammer_Minimize
+open Sledgehammer_Prover_Minimize
open Sledgehammer_MaSh
-open Sledgehammer_Run
+open Sledgehammer
(* val cvc3N = "cvc3" *)
val yicesN = "yices"
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Fri Jan 31 10:23:32 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,297 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_compress.ML
- Author: Steffen Juilf Smolka, TU Muenchen
- Author: Jasmin Blanchette, TU Muenchen
-
-Compression of isar proofs by merging steps.
-Only proof steps using the same proof method are merged.
-*)
-
-signature SLEDGEHAMMER_COMPRESS =
-sig
- type isar_proof = Sledgehammer_Proof.isar_proof
- type preplay_interface = Sledgehammer_Preplay.preplay_interface
-
- val compress_proof : real -> preplay_interface -> isar_proof -> isar_proof
-end;
-
-structure Sledgehammer_Compress : SLEDGEHAMMER_COMPRESS =
-struct
-
-open Sledgehammer_Util
-open Sledgehammer_Reconstructor
-open Sledgehammer_Proof
-open Sledgehammer_Preplay
-
-(* traverses steps in post-order and collects the steps with the given labels *)
-fun collect_successors steps lbls =
- let
- fun do_steps _ ([], accu) = ([], accu)
- | do_steps [] accum = accum
- | do_steps (step :: steps) accum = do_steps steps (do_step step accum)
- and do_step (Let _) x = x
- | do_step (step as Prove (_, _, l, _, subproofs, _)) x =
- (case do_subproofs subproofs x of
- ([], accu) => ([], accu)
- | accum as (l' :: lbls', accu) => if l = l' then (lbls', step :: accu) else accum)
- and do_subproofs [] x = x
- | do_subproofs (proof :: subproofs) x =
- (case do_steps (steps_of_proof proof) x of
- accum as ([], _) => accum
- | accum => do_subproofs subproofs accum)
- in
- (case do_steps steps (lbls, []) of
- ([], succs) => rev succs
- | _ => raise Fail "Sledgehammer_Compress: collect_successors")
- end
-
-(* traverses steps in reverse post-order and inserts the given updates *)
-fun update_steps steps updates =
- let
- fun do_steps [] updates = ([], updates)
- | do_steps steps [] = (steps, [])
- | do_steps (step :: steps) updates = do_step step (do_steps steps updates)
- and do_step step (steps, []) = (step :: steps, [])
- | do_step (step as Let _) (steps, updates) = (step :: steps, updates)
- | do_step (Prove (qs, xs, l, t, subproofs, by))
- (steps, updates as Prove (qs', xs', l', t', subproofs', by') :: updates') =
- let
- val (subproofs, updates) =
- if l = l' then do_subproofs subproofs' updates' else do_subproofs subproofs updates
- in
- if l = l' then (Prove (qs', xs', l', t', subproofs, by') :: steps, updates)
- else (Prove (qs, xs, l, t, subproofs, by) :: steps, updates)
- end
- | do_step _ _ = raise Fail "Sledgehammer_Compress: update_steps (invalid update)"
- and do_subproofs [] updates = ([], updates)
- | do_subproofs steps [] = (steps, [])
- | do_subproofs (proof :: subproofs) updates =
- do_proof proof (do_subproofs subproofs updates)
- and do_proof proof (proofs, []) = (proof :: proofs, [])
- | do_proof (Proof (fix, assms, steps)) (proofs, updates) =
- let val (steps, updates) = do_steps steps updates in
- (Proof (fix, assms, steps) :: proofs, updates)
- end
- in
- (case do_steps steps (rev updates) of
- (steps, []) => steps
- | _ => raise Fail "Sledgehammer_Compress: update_steps")
- end
-
-(* Tries merging the first step into the second step. Arbitrarily picks the second step's method. *)
-fun try_merge (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), _)))
- (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), meth2))) =
- let
- val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
- val gfs = union (op =) gfs1 gfs2
- in
- SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), meth2)))
- end
- | try_merge _ _ = NONE
-
-val compress_degree = 2
-val merge_timeout_slack = 1.2
-
-(* Precondition: The proof must be labeled canonically
- (cf. "Slegehammer_Proof.relabel_proof_canonically"). *)
-fun compress_proof compress_isar
- ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_interface) proof =
- if compress_isar <= 1.0 then
- proof
- else
- let
- val (compress_further, decrement_step_count) =
- let
- val number_of_steps = add_proof_steps (steps_of_proof proof) 0
- val target_number_of_steps = Real.round (Real.fromInt number_of_steps / compress_isar)
- val delta = Unsynchronized.ref (number_of_steps - target_number_of_steps)
- in
- (fn () => !delta > 0, fn () => delta := !delta - 1)
- end
-
- val (get_successors, replace_successor) =
- let
- fun add_refs (Let _) = I
- | add_refs (Prove (_, _, v, _, _, ((lfs, _), _))) =
- fold (fn key => Canonical_Lbl_Tab.cons_list (key, v)) lfs
-
- val tab =
- Canonical_Lbl_Tab.empty
- |> fold_isar_steps add_refs (steps_of_proof proof)
- (* "rev" should have the same effect as "sort canonical_label_ord" *)
- |> Canonical_Lbl_Tab.map (K rev)
- |> Unsynchronized.ref
-
- fun get_successors l = Canonical_Lbl_Tab.lookup_list (!tab) l
- fun set_successors l refs = tab := Canonical_Lbl_Tab.update (l, refs) (!tab)
- fun replace_successor old new dest =
- get_successors dest
- |> Ord_List.remove canonical_label_ord old
- |> Ord_List.union canonical_label_ord new
- |> set_successors dest
- in
- (get_successors, replace_successor)
- end
-
- (** elimination of trivial, one-step subproofs **)
-
- fun elim_subproofs' time qs fix l t lfs gfs meth subs nontriv_subs =
- if null subs orelse not (compress_further ()) then
- (set_preplay_outcome l (Played time);
- Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meth)))
- else
- (case subs of
- (sub as Proof (_, assms, sub_steps)) :: subs =>
- (let
- (* trivial subproofs have exactly one Prove step *)
- val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), _))) = try the_single sub_steps
-
- (* only touch proofs that can be preplayed sucessfully *)
- val Played time' = get_preplay_outcome l'
-
- (* merge steps *)
- val subs'' = subs @ nontriv_subs
- val lfs'' =
- subtract (op =) (map fst assms) lfs'
- |> union (op =) lfs
- val gfs'' = union (op =) gfs' gfs
- val by = ((lfs'', gfs''), meth)
- val step'' = Prove (qs, fix, l, t, subs'', by)
-
- (* check if the modified step can be preplayed fast enough *)
- val timeout = time_mult merge_timeout_slack (Time.+(time, time'))
- val Played time'' = preplay_quietly timeout step''
-
- in
- decrement_step_count (); (* l' successfully eliminated! *)
- map (replace_successor l' [l]) lfs';
- elim_subproofs' time'' qs fix l t lfs'' gfs'' meth subs nontriv_subs
- end
- handle Bind =>
- elim_subproofs' time qs fix l t lfs gfs meth subs (sub :: nontriv_subs))
- | _ => raise Fail "Sledgehammer_Compress: elim_subproofs'")
-
- fun elim_subproofs (step as Let _) = step
- | elim_subproofs (step as Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meth))) =
- if subproofs = [] then
- step
- else
- (case get_preplay_outcome l of
- Played time => elim_subproofs' time qs fix l t lfs gfs meth subproofs []
- | _ => step)
-
- (** top_level compression: eliminate steps by merging them into their
- successors **)
-
- fun compress_top_level steps =
- let
- (* (#successors, (size_of_term t, position)) *)
- fun cand_key (i, l, t_size) = (get_successors l |> length, (t_size, i))
-
- val compression_ord =
- prod_ord int_ord (prod_ord (int_ord #> rev_order) int_ord)
- #> rev_order
-
- val cand_ord = pairself cand_key #> compression_ord
-
- fun pop_next_cand candidates =
- (case max_list cand_ord candidates of
- NONE => (NONE, [])
- | cand as SOME (i, _, _) => (cand, filter_out (fn (j, _, _) => j = i) candidates))
-
- val candidates =
- let
- fun add_cand (_, Let _) = I
- | add_cand (i, Prove (_, _, l, t, _, _)) = cons (i, l, size_of_term t)
- in
- (steps
- |> split_last |> fst (* keep last step *)
- |> fold_index add_cand) []
- end
-
- fun try_eliminate (i, l, _) succ_lbls steps =
- let
- (* only touch steps that can be preplayed successfully *)
- val Played time = get_preplay_outcome l
-
- val succ_times =
- map (get_preplay_outcome #> (fn Played t => t)) succ_lbls
- val timeslice = time_mult (1.0 / (Real.fromInt (length succ_lbls))) time
- val timeouts =
- map (curry Time.+ timeslice #> time_mult merge_timeout_slack) succ_times
-
- val ((cand as Prove (_, _, l, _, _, ((lfs, _), _))) :: steps') = drop i steps
-
- (* FIXME: debugging *)
- val _ =
- if the (label_of_step cand) <> l then
- raise Fail "Sledgehammer_Compress: try_eliminate"
- else
- ()
-
- val succs = collect_successors steps' succ_lbls
- val succs' = map (try_merge cand #> the) succs
-
- (* TODO: should be lazy: stop preplaying as soon as one step fails/times out *)
- val play_outcomes = map2 preplay_quietly timeouts succs'
-
- (* ensure none of the modified successors timed out *)
- val true = List.all (fn Played _ => true) play_outcomes
-
- val (steps1, _ :: steps2) = chop i steps
- (* replace successors with their modified versions *)
- val steps2 = update_steps steps2 succs'
- in
- decrement_step_count (); (* candidate successfully eliminated *)
- map2 set_preplay_outcome succ_lbls play_outcomes;
- map (replace_successor l succ_lbls) lfs;
- (* removing the step would mess up the indices -> replace with dummy step instead *)
- steps1 @ dummy_isar_step :: steps2
- end
- handle Bind => steps
- | Match => steps
- | Option.Option => steps
-
- fun compression_loop candidates steps =
- if not (compress_further ()) then
- steps
- else
- (case pop_next_cand candidates of
- (NONE, _) => steps (* no more candidates for elimination *)
- | (SOME (cand as (_, l, _)), candidates) =>
- let val successors = get_successors l in
- if length successors > compress_degree then steps
- else compression_loop candidates (try_eliminate cand successors steps)
- end)
- in
- compression_loop candidates steps
- |> remove (op =) dummy_isar_step
- end
-
- (** recusion over the proof tree **)
- (*
- Proofs are compressed bottom-up, beginning with the innermost
- subproofs.
- On the innermost proof level, the proof steps have no subproofs.
- In the best case, these steps can be merged into just one step,
- resulting in a trivial subproof. Going one level up, trivial subproofs
- can be eliminated. In the best case, this once again leads to a proof
- whose proof steps do not have subproofs. Applying this approach
- recursively will result in a flat proof in the best cast.
- *)
- fun do_proof (proof as (Proof (fix, assms, steps))) =
- if compress_further () then Proof (fix, assms, do_steps steps) else proof
- and do_steps steps =
- (* bottom-up: compress innermost proofs first *)
- steps |> map (fn step => step |> compress_further () ? do_sub_levels)
- |> compress_further () ? compress_top_level
- and do_sub_levels (Let x) = Let x
- | do_sub_levels (Prove (qs, xs, l, t, subproofs, by)) =
- (* compress subproofs *)
- Prove (qs, xs, l, t, map do_proof subproofs, by)
- (* eliminate trivial subproofs *)
- |> compress_further () ? elim_subproofs
- in
- do_proof proof
- end
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Jan 31 10:23:32 2014 +0100
@@ -0,0 +1,423 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Author: Steffen Juilf Smolka, TU Muenchen
+
+Isar proof reconstruction from ATP proofs.
+*)
+
+signature SLEDGEHAMMER_ISAR =
+sig
+ type atp_step_name = ATP_Proof.atp_step_name
+ type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
+ type 'a atp_proof = 'a ATP_Proof.atp_proof
+ type stature = ATP_Problem_Generate.stature
+ type one_line_params = Sledgehammer_Reconstructor.one_line_params
+
+ type isar_params =
+ bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
+
+ val proof_text : Proof.context -> bool -> bool option -> (unit -> isar_params) -> int ->
+ one_line_params -> string
+end;
+
+structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
+struct
+
+open ATP_Util
+open ATP_Problem
+open ATP_Proof
+open ATP_Problem_Generate
+open ATP_Proof_Reconstruct
+open Sledgehammer_Util
+open Sledgehammer_Reconstructor
+open Sledgehammer_Isar_Proof
+open Sledgehammer_Isar_Annotate
+open Sledgehammer_Isar_Print
+open Sledgehammer_Isar_Preplay
+open Sledgehammer_Isar_Compress
+open Sledgehammer_Isar_Try0
+open Sledgehammer_Isar_Minimize
+
+structure String_Redirect = ATP_Proof_Redirect(
+ type key = atp_step_name
+ val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s')
+ val string_of = fst)
+
+open String_Redirect
+
+val e_skolemize_rules = ["skolemize", "shift_quantors"]
+val spass_pirate_datatype_rule = "DT"
+val vampire_skolemisation_rule = "skolemisation"
+(* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *)
+val z3_skolemize_rule = "sk"
+val z3_th_lemma_rule = "th-lemma"
+
+val skolemize_rules =
+ e_skolemize_rules @ [spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule]
+
+val is_skolemize_rule = member (op =) skolemize_rules
+val is_arith_rule = String.isPrefix z3_th_lemma_rule
+val is_datatype_rule = String.isPrefix spass_pirate_datatype_rule
+
+fun raw_label_of_num num = (num, 0)
+
+fun label_of_clause [(num, _)] = raw_label_of_num num
+ | label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0)
+
+fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss)
+ | add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names))
+
+(* No "real" literals means only type information (tfree_tcs, clsrel, or clsarity). *)
+fun is_only_type_information t = t aconv @{prop True}
+
+(* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in
+ type information. *)
+fun add_line_pass1 (line as (name, role, t, rule, [])) lines =
+ (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or
+ definitions. *)
+ if role = Lemma orelse role = Conjecture orelse role = Negated_Conjecture orelse
+ role = Hypothesis orelse is_arith_rule rule then
+ line :: lines
+ else if role = Axiom then
+ (* Facts are not proof lines. *)
+ lines |> is_only_type_information t ? map (replace_dependencies_in_line (name, []))
+ else
+ map (replace_dependencies_in_line (name, [])) lines
+ | add_line_pass1 line lines = line :: lines
+
+fun add_lines_pass2 res [] = rev res
+ | add_lines_pass2 res ((name, role, t, rule, deps) :: lines) =
+ let
+ val is_last_line = null lines
+
+ fun looks_interesting () =
+ not (is_only_type_information t) andalso null (Term.add_tvars t [])
+ andalso length deps >= 2 andalso not (can the_single lines)
+
+ fun is_skolemizing_line (_, _, _, rule', deps') =
+ is_skolemize_rule rule' andalso member (op =) deps' name
+ fun is_before_skolemize_rule () = exists is_skolemizing_line lines
+ in
+ if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse
+ is_datatype_rule rule orelse is_last_line orelse looks_interesting () orelse
+ is_before_skolemize_rule () then
+ add_lines_pass2 ((name, role, t, rule, deps) :: res) lines
+ else
+ add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines)
+ end
+
+val add_labels_of_proof =
+ steps_of_proof
+ #> fold_isar_steps (byline_of_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I))
+
+fun kill_useless_labels_in_proof proof =
+ let
+ val used_ls = add_labels_of_proof proof []
+
+ fun kill_label l = if member (op =) used_ls l then l else no_label
+ fun kill_assms assms = map (apfst kill_label) assms
+
+ fun kill_step (Prove (qs, xs, l, t, subproofs, by)) =
+ Prove (qs, xs, kill_label l, t, map kill_proof subproofs, by)
+ | kill_step step = step
+ and kill_proof (Proof (fix, assms, steps)) =
+ Proof (fix, kill_assms assms, map kill_step steps)
+ in
+ kill_proof proof
+ end
+
+val assume_prefix = "a"
+val have_prefix = "f"
+
+val relabel_proof =
+ let
+ fun fresh_label depth prefix (accum as (l, subst, next)) =
+ if l = no_label then
+ accum
+ else
+ let val l' = (replicate_string (depth + 1) prefix, next) in
+ (l', (l, l') :: subst, next + 1)
+ end
+
+ fun relabel_facts subst = apfst (maps (the_list o AList.lookup (op =) subst))
+
+ fun relabel_assm depth (l, t) (subst, next) =
+ let val (l, subst, next) = (l, subst, next) |> fresh_label depth assume_prefix in
+ ((l, t), (subst, next))
+ end
+
+ fun relabel_assms subst depth assms = fold_map (relabel_assm depth) assms (subst, 1) ||> fst
+
+ fun relabel_steps _ _ _ [] = []
+ | relabel_steps subst depth next (Prove (qs, xs, l, t, sub, by) :: steps) =
+ let
+ val (l, subst, next) = (l, subst, next) |> fresh_label depth have_prefix
+ val sub = relabel_proofs subst depth sub
+ val by = apfst (relabel_facts subst) by
+ in
+ Prove (qs, xs, l, t, sub, by) :: relabel_steps subst depth next steps
+ end
+ | relabel_steps subst depth next (step :: steps) =
+ step :: relabel_steps subst depth next steps
+ and relabel_proof subst depth (Proof (fix, assms, steps)) =
+ let val (assms, subst) = relabel_assms subst depth assms in
+ Proof (fix, assms, relabel_steps subst depth 1 steps)
+ end
+ and relabel_proofs subst depth = map (relabel_proof subst (depth + 1))
+ in
+ relabel_proof [] 0
+ end
+
+val chain_direct_proof =
+ let
+ fun chain_qs_lfs NONE lfs = ([], lfs)
+ | chain_qs_lfs (SOME l0) lfs =
+ if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs)
+ fun chain_step lbl (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss))) =
+ let val (qs', lfs) = chain_qs_lfs lbl lfs in
+ Prove (qs' @ qs, xs, l, t, chain_proofs subproofs, ((lfs, gfs), methss))
+ end
+ | chain_step _ step = step
+ and chain_steps _ [] = []
+ | chain_steps (prev as SOME _) (i :: is) =
+ chain_step prev i :: chain_steps (label_of_step i) is
+ | chain_steps _ (i :: is) = i :: chain_steps (label_of_step i) is
+ and chain_proof (Proof (fix, assms, steps)) =
+ Proof (fix, assms, chain_steps (try (List.last #> fst) assms) steps)
+ and chain_proofs proofs = map (chain_proof) proofs
+ in
+ chain_proof
+ end
+
+type isar_params =
+ bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
+
+val arith_methodss =
+ [[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
+ Metis_Method], [Meson_Method]]
+val datatype_methodss = [[Simp_Size_Method, Simp_Method]]
+val metislike_methodss =
+ [[Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
+ Force_Method], [Meson_Method]]
+val rewrite_methodss =
+ [[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method], [Meson_Method]]
+val skolem_methodss = [[Metis_Method, Blast_Method], [Meson_Method]]
+
+fun isar_proof_text ctxt debug isar_proofs isar_params
+ (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
+ let
+ fun isar_proof_of () =
+ let
+ val SOME (verbose, metis_type_enc, metis_lam_trans, preplay_timeout, compress_isar,
+ try0_isar, atp_proof, goal) = try isar_params ()
+
+ val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
+ val (_, ctxt) =
+ params
+ |> map (fn (s, T) => (Binding.name s, SOME T, NoSyn))
+ |> (fn fixes => ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes)
+
+ val do_preplay = preplay_timeout <> Time.zeroTime
+ val try0_isar = try0_isar andalso do_preplay
+
+ val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
+ fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
+
+ fun get_role keep_role ((num, _), role, t, rule, _) =
+ if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
+
+ val atp_proof =
+ atp_proof
+ |> rpair [] |-> fold_rev add_line_pass1
+ |> add_lines_pass2 []
+
+ val conjs =
+ map_filter (fn (name, role, _, _, _) =>
+ if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE)
+ atp_proof
+ val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof
+ val lems =
+ map_filter (get_role (curry (op =) Lemma)) atp_proof
+ |> map (fn ((l, t), rule) =>
+ let
+ val (skos, methss) =
+ if is_skolemize_rule rule then (skolems_of t, skolem_methodss)
+ else if is_arith_rule rule then ([], arith_methodss)
+ else ([], rewrite_methodss)
+ in
+ Prove ([], skos, l, t, [], (([], []), methss))
+ end)
+
+ val bot = atp_proof |> List.last |> #1
+
+ val refute_graph =
+ atp_proof
+ |> map (fn (name, _, _, _, from) => (from, name))
+ |> make_refute_graph bot
+ |> fold (Atom_Graph.default_node o rpair ()) conjs
+
+ val axioms = axioms_of_refute_graph refute_graph conjs
+
+ val tainted = tainted_atoms_of_refute_graph refute_graph conjs
+ val is_clause_tainted = exists (member (op =) tainted)
+ val steps =
+ Symtab.empty
+ |> fold (fn (name as (s, _), role, t, rule, _) =>
+ Symtab.update_new (s, (rule, t
+ |> (if is_clause_tainted [name] then
+ HOLogic.dest_Trueprop
+ #> role <> Conjecture ? s_not
+ #> fold exists_of (map Var (Term.add_vars t []))
+ #> HOLogic.mk_Trueprop
+ else
+ I))))
+ atp_proof
+
+ val rule_of_clause_id = fst o the o Symtab.lookup steps o fst
+
+ fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> close_form
+ | prop_of_clause names =
+ let
+ val lits = map (HOLogic.dest_Trueprop o snd)
+ (map_filter (Symtab.lookup steps o fst) names)
+ in
+ (case List.partition (can HOLogic.dest_not) lits of
+ (negs as _ :: _, pos as _ :: _) =>
+ s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos)
+ | _ => fold (curry s_disj) lits @{term False})
+ end
+ |> HOLogic.mk_Trueprop |> close_form
+
+ fun maybe_show outer c = (outer andalso eq_set (op =) (c, conjs)) ? cons Show
+
+ fun isar_steps outer predecessor accum [] =
+ accum
+ |> (if tainted = [] then
+ cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
+ ((the_list predecessor, []), metislike_methodss)))
+ else
+ I)
+ |> rev
+ | isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) =
+ let
+ val l = label_of_clause c
+ val t = prop_of_clause c
+ val rule = rule_of_clause_id id
+ val skolem = is_skolemize_rule rule
+
+ fun prove sub by = Prove (maybe_show outer c [], [], l, t, sub, by)
+ fun do_rest l step = isar_steps outer (SOME l) (step :: accum) infs
+
+ val deps = fold add_fact_of_dependencies gamma no_facts
+ val methss =
+ if is_arith_rule rule then arith_methodss
+ else if is_datatype_rule rule then datatype_methodss
+ else metislike_methodss
+ val by = (deps, methss)
+ in
+ if is_clause_tainted c then
+ (case gamma of
+ [g] =>
+ if skolem andalso is_clause_tainted g then
+ let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in
+ isar_steps outer (SOME l) [prove [subproof] (no_facts, skolem_methodss)] infs
+ end
+ else
+ do_rest l (prove [] by)
+ | _ => do_rest l (prove [] by))
+ else
+ do_rest l (if skolem then Prove ([], skolems_of t, l, t, [], by) else prove [] by)
+ end
+ | isar_steps outer predecessor accum (Cases cases :: infs) =
+ let
+ fun isar_case (c, subinfs) =
+ isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs
+ val c = succedent_of_cases cases
+ val l = label_of_clause c
+ val t = prop_of_clause c
+ val step =
+ Prove (maybe_show outer c [], [], l, t,
+ map isar_case (filter_out (null o snd) cases),
+ ((the_list predecessor, []), metislike_methodss))
+ in
+ isar_steps outer (SOME l) (step :: accum) infs
+ end
+ and isar_proof outer fix assms lems infs =
+ Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
+
+ val (preplay_interface as {overall_preplay_outcome, ...}, isar_proof) =
+ refute_graph
+(*
+ |> tap (tracing o prefix "Refute graph: " o string_of_refute_graph)
+*)
+ |> redirect_graph axioms tainted bot
+(*
+ |> tap (tracing o prefix "Direct proof: " o string_of_direct_proof)
+*)
+ |> isar_proof true params assms lems
+ |> postprocess_remove_unreferenced_steps I
+ |> relabel_proof_canonically
+ |> `(proof_preplay_interface debug ctxt metis_type_enc metis_lam_trans do_preplay
+ preplay_timeout)
+
+ val (play_outcome, isar_proof) =
+ isar_proof
+ |> compress_proof (if isar_proofs = SOME true then compress_isar else 1000.0)
+ preplay_interface
+ |> try0_isar ? try0 preplay_timeout preplay_interface
+ |> postprocess_remove_unreferenced_steps (try0_isar ? min_deps_of_step preplay_interface)
+ |> `overall_preplay_outcome
+ ||> (chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof)
+
+ val isar_text =
+ string_of_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count isar_proof
+ in
+ (case isar_text of
+ "" =>
+ if isar_proofs = SOME true then
+ "\nNo structured proof available (proof too simple)."
+ else
+ ""
+ | _ =>
+ let
+ val msg =
+ (if verbose then
+ let val num_steps = add_proof_steps (steps_of_proof isar_proof) 0 in
+ [string_of_int num_steps ^ " step" ^ plural_s num_steps]
+ end
+ else
+ []) @
+ (if do_preplay then [string_of_play_outcome play_outcome] else [])
+ in
+ "\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
+ Active.sendback_markup [Markup.padding_command] isar_text
+ end)
+ end
+
+ val one_line_proof = one_line_proof_text 0 one_line_params
+ val isar_proof =
+ if debug then
+ isar_proof_of ()
+ else
+ (case try isar_proof_of () of
+ SOME s => s
+ | NONE =>
+ if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "")
+ in one_line_proof ^ isar_proof end
+
+fun isar_proof_would_be_a_good_idea (reconstr, play) =
+ (case play of
+ Played _ => reconstr = SMT
+ | Play_Timed_Out _ => true
+ | Play_Failed => true
+ | Not_Played => false)
+
+fun proof_text ctxt debug isar_proofs isar_params num_chained
+ (one_line_params as (preplay, _, _, _, _, _)) =
+ (if isar_proofs = SOME true orelse
+ (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
+ isar_proof_text ctxt debug isar_proofs isar_params
+ else
+ one_line_proof_text num_chained) one_line_params
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML Fri Jan 31 10:23:32 2014 +0100
@@ -0,0 +1,214 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Author: Steffen Juilf Smolka, TU Muenchen
+
+Supplements term with a locally minmal, complete set of type constraints.
+Complete: The constraints suffice to infer the term's types.
+Minimal: Reducing the set of constraints further will make it incomplete.
+
+When configuring the pretty printer appropriately, the constraints will show up
+as type annotations when printing the term. This allows the term to be printed
+and reparsed without a change of types.
+
+NOTE: Terms should be unchecked before calling annotate_types to avoid awkward
+syntax.
+*)
+
+signature SLEDGEHAMMER_ISAR_ANNOTATE =
+sig
+ val annotate_types : Proof.context -> term -> term
+end;
+
+structure Sledgehammer_Isar_Annotate : SLEDGEHAMMER_ISAR_ANNOTATE =
+struct
+
+(* Util *)
+fun post_traverse_term_type' f _ (t as Const (_, T)) s = f t T s
+ | post_traverse_term_type' f _ (t as Free (_, T)) s = f t T s
+ | post_traverse_term_type' f _ (t as Var (_, T)) s = f t T s
+ | post_traverse_term_type' f env (t as Bound i) s = f t (nth env i) s
+ | post_traverse_term_type' f env (Abs (x, T1, b)) s =
+ let
+ val ((b', s'), T2) = post_traverse_term_type' f (T1 :: env) b s
+ in f (Abs (x, T1, b')) (T1 --> T2) s' end
+ | post_traverse_term_type' f env (u $ v) s =
+ let
+ val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s
+ val ((v', s''), _) = post_traverse_term_type' f env v s'
+ in f (u' $ v') T s'' end
+ handle Bind => raise Fail "Sledgehammer_Isar_Annotate: post_traverse_term_type'"
+
+fun post_traverse_term_type f s t =
+ post_traverse_term_type' (fn t => fn T => fn s => (f t T s, T)) [] t s |> fst
+fun post_fold_term_type f s t =
+ post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t |> snd
+
+fun fold_map_atypes f T s =
+ case T of
+ Type (name, Ts) =>
+ let val (Ts, s) = fold_map (fold_map_atypes f) Ts s in
+ (Type (name, Ts), s)
+ end
+ | _ => f T s
+
+(** get unique elements of a list **)
+local
+ fun unique' b x [] = if b then [x] else []
+ | unique' b x (y :: ys) =
+ if x = y then unique' false x ys
+ else unique' true y ys |> b ? cons x
+in
+ fun unique ord xs =
+ case sort ord xs of x :: ys => unique' true x ys | [] => []
+end
+
+(** Data structures, orders **)
+val indexname_ord = Term_Ord.fast_indexname_ord
+val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord)
+structure Var_Set_Tab = Table(
+ type key = indexname list
+ val ord = list_ord indexname_ord)
+
+(* (1) Generalize types *)
+fun generalize_types ctxt t =
+ let
+ val erase_types = map_types (fn _ => dummyT)
+ (* use schematic type variables *)
+ val ctxt = ctxt |> Proof_Context.set_mode Proof_Context.mode_pattern
+ val infer_types = singleton (Type_Infer_Context.infer_types ctxt)
+ in
+ t |> erase_types |> infer_types
+ end
+
+(* (2) match types *)
+fun match_types ctxt t1 t2 =
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val get_types = post_fold_term_type (K cons) []
+ in
+ fold (Sign.typ_match thy) (get_types t1 ~~ get_types t2) Vartab.empty
+ handle Type.TYPE_MATCH => raise Fail "Sledgehammer_Isar_Annotate: match_types"
+ end
+
+
+(* (3) handle trivial tfrees *)
+fun handle_trivial_tfrees ctxt (t', subst) =
+ let
+ val add_tfree_names =
+ snd #> snd #> fold_atyps (fn TFree (x, _) => cons x | _ => I)
+
+ val trivial_tfree_names =
+ Vartab.fold add_tfree_names subst []
+ |> filter_out (Variable.is_declared ctxt)
+ |> unique fast_string_ord
+ val tfree_name_trivial = Ord_List.member fast_string_ord trivial_tfree_names
+
+ val trivial_tvar_names =
+ Vartab.fold
+ (fn (tvar_name, (_, TFree (tfree_name, _))) =>
+ tfree_name_trivial tfree_name ? cons tvar_name
+ | _ => I)
+ subst
+ []
+ |> sort indexname_ord
+ val tvar_name_trivial = Ord_List.member indexname_ord trivial_tvar_names
+
+ val t' =
+ t' |> map_types
+ (map_type_tvar
+ (fn (idxn, sort) =>
+ if tvar_name_trivial idxn then dummyT else TVar (idxn, sort)))
+
+ val subst =
+ subst |> fold Vartab.delete trivial_tvar_names
+ |> Vartab.map
+ (K (apsnd (map_type_tfree
+ (fn (name, sort) =>
+ if tfree_name_trivial name then dummyT
+ else TFree (name, sort)))))
+ in
+ (t', subst)
+ end
+
+
+(* (4) Typing-spot table *)
+local
+fun key_of_atype (TVar (z, _)) = Ord_List.insert indexname_ord z
+ | key_of_atype _ = I
+fun key_of_type T = fold_atyps key_of_atype T []
+fun update_tab t T (tab, pos) =
+ (case key_of_type T of
+ [] => tab
+ | key =>
+ let val cost = (size_of_typ T, (size_of_term t, pos)) in
+ case Var_Set_Tab.lookup tab key of
+ NONE => Var_Set_Tab.update_new (key, cost) tab
+ | SOME old_cost =>
+ (case cost_ord (cost, old_cost) of
+ LESS => Var_Set_Tab.update (key, cost) tab
+ | _ => tab)
+ end,
+ pos + 1)
+in
+val typing_spot_table =
+ post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst
+end
+
+(* (5) Reverse-greedy *)
+fun reverse_greedy typing_spot_tab =
+ let
+ fun update_count z =
+ fold (fn tvar => fn tab =>
+ let val c = Vartab.lookup tab tvar |> the_default 0 in
+ Vartab.update (tvar, c + z) tab
+ end)
+ fun superfluous tcount =
+ forall (fn tvar => the (Vartab.lookup tcount tvar) > 1)
+ fun drop_superfluous (tvars, (_, (_, spot))) (spots, tcount) =
+ if superfluous tcount tvars then (spots, update_count ~1 tvars tcount)
+ else (spot :: spots, tcount)
+ val (typing_spots, tvar_count_tab) =
+ Var_Set_Tab.fold
+ (fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k))
+ typing_spot_tab ([], Vartab.empty)
+ |>> sort_distinct (rev_order o cost_ord o pairself snd)
+ in fold drop_superfluous typing_spots ([], tvar_count_tab) |> fst end
+
+(* (6) Introduce annotations *)
+fun introduce_annotations subst spots t t' =
+ let
+ fun subst_atype (T as TVar (idxn, S)) subst =
+ (Envir.subst_type subst T, Vartab.update (idxn, (S, dummyT)) subst)
+ | subst_atype T subst = (T, subst)
+ val subst_type = fold_map_atypes subst_atype
+ fun collect_annot _ T (subst, cp, ps as p :: ps', annots) =
+ if p <> cp then
+ (subst, cp + 1, ps, annots)
+ else
+ let val (T, subst) = subst_type T subst in
+ (subst, cp + 1, ps', (p, T)::annots)
+ end
+ | collect_annot _ _ x = x
+ val (_, _, _, annots) =
+ post_fold_term_type collect_annot (subst, 0, spots, []) t'
+ fun insert_annot t _ (cp, annots as (p, T) :: annots') =
+ if p <> cp then (t, (cp + 1, annots)) else (Type.constraint T t, (cp + 1, annots'))
+ | insert_annot t _ x = (t, x)
+ in
+ t |> post_traverse_term_type insert_annot (0, rev annots)
+ |> fst
+ end
+
+(* (7) Annotate *)
+fun annotate_types ctxt t =
+ let
+ val t' = generalize_types ctxt t
+ val subst = match_types ctxt t' t
+ val (t', subst) = (t', subst) |> handle_trivial_tfrees ctxt
+ val typing_spots =
+ t' |> typing_spot_table
+ |> reverse_greedy
+ |> sort int_ord
+ in introduce_annotations subst typing_spots t t' end
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Fri Jan 31 10:23:32 2014 +0100
@@ -0,0 +1,297 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
+ Author: Steffen Juilf Smolka, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
+
+Compression of Isar proofs by merging steps.
+Only proof steps using the same proof method are merged.
+*)
+
+signature SLEDGEHAMMER_ISAR_COMPRESS =
+sig
+ type isar_proof = Sledgehammer_Isar_Proof.isar_proof
+ type preplay_interface = Sledgehammer_Isar_Preplay.preplay_interface
+
+ val compress_proof : real -> preplay_interface -> isar_proof -> isar_proof
+end;
+
+structure Sledgehammer_Isar_Compress : SLEDGEHAMMER_ISAR_COMPRESS =
+struct
+
+open Sledgehammer_Util
+open Sledgehammer_Reconstructor
+open Sledgehammer_Isar_Proof
+open Sledgehammer_Isar_Preplay
+
+(* traverses steps in post-order and collects the steps with the given labels *)
+fun collect_successors steps lbls =
+ let
+ fun do_steps _ ([], accu) = ([], accu)
+ | do_steps [] accum = accum
+ | do_steps (step :: steps) accum = do_steps steps (do_step step accum)
+ and do_step (Let _) x = x
+ | do_step (step as Prove (_, _, l, _, subproofs, _)) x =
+ (case do_subproofs subproofs x of
+ ([], accu) => ([], accu)
+ | accum as (l' :: lbls', accu) => if l = l' then (lbls', step :: accu) else accum)
+ and do_subproofs [] x = x
+ | do_subproofs (proof :: subproofs) x =
+ (case do_steps (steps_of_proof proof) x of
+ accum as ([], _) => accum
+ | accum => do_subproofs subproofs accum)
+ in
+ (case do_steps steps (lbls, []) of
+ ([], succs) => rev succs
+ | _ => raise Fail "Sledgehammer_Isar_Compress: collect_successors")
+ end
+
+(* traverses steps in reverse post-order and inserts the given updates *)
+fun update_steps steps updates =
+ let
+ fun do_steps [] updates = ([], updates)
+ | do_steps steps [] = (steps, [])
+ | do_steps (step :: steps) updates = do_step step (do_steps steps updates)
+ and do_step step (steps, []) = (step :: steps, [])
+ | do_step (step as Let _) (steps, updates) = (step :: steps, updates)
+ | do_step (Prove (qs, xs, l, t, subproofs, by))
+ (steps, updates as Prove (qs', xs', l', t', subproofs', by') :: updates') =
+ let
+ val (subproofs, updates) =
+ if l = l' then do_subproofs subproofs' updates' else do_subproofs subproofs updates
+ in
+ if l = l' then (Prove (qs', xs', l', t', subproofs, by') :: steps, updates)
+ else (Prove (qs, xs, l, t, subproofs, by) :: steps, updates)
+ end
+ | do_step _ _ = raise Fail "Sledgehammer_Isar_Compress: update_steps (invalid update)"
+ and do_subproofs [] updates = ([], updates)
+ | do_subproofs steps [] = (steps, [])
+ | do_subproofs (proof :: subproofs) updates =
+ do_proof proof (do_subproofs subproofs updates)
+ and do_proof proof (proofs, []) = (proof :: proofs, [])
+ | do_proof (Proof (fix, assms, steps)) (proofs, updates) =
+ let val (steps, updates) = do_steps steps updates in
+ (Proof (fix, assms, steps) :: proofs, updates)
+ end
+ in
+ (case do_steps steps (rev updates) of
+ (steps, []) => steps
+ | _ => raise Fail "Sledgehammer_Isar_Compress: update_steps")
+ end
+
+(* Tries merging the first step into the second step. Arbitrarily picks the second step's method. *)
+fun try_merge (Prove (_, [], lbl1, _, [], ((lfs1, gfs1), _)))
+ (Prove (qs2, fix, lbl2, t, subproofs, ((lfs2, gfs2), meth2))) =
+ let
+ val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1
+ val gfs = union (op =) gfs1 gfs2
+ in
+ SOME (Prove (qs2, fix, lbl2, t, subproofs, ((lfs, gfs), meth2)))
+ end
+ | try_merge _ _ = NONE
+
+val compress_degree = 2
+val merge_timeout_slack = 1.2
+
+(* Precondition: The proof must be labeled canonically
+ (cf. "Slegehammer_Proof.relabel_proof_canonically"). *)
+fun compress_proof compress_isar
+ ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_interface) proof =
+ if compress_isar <= 1.0 then
+ proof
+ else
+ let
+ val (compress_further, decrement_step_count) =
+ let
+ val number_of_steps = add_proof_steps (steps_of_proof proof) 0
+ val target_number_of_steps = Real.round (Real.fromInt number_of_steps / compress_isar)
+ val delta = Unsynchronized.ref (number_of_steps - target_number_of_steps)
+ in
+ (fn () => !delta > 0, fn () => delta := !delta - 1)
+ end
+
+ val (get_successors, replace_successor) =
+ let
+ fun add_refs (Let _) = I
+ | add_refs (Prove (_, _, v, _, _, ((lfs, _), _))) =
+ fold (fn key => Canonical_Lbl_Tab.cons_list (key, v)) lfs
+
+ val tab =
+ Canonical_Lbl_Tab.empty
+ |> fold_isar_steps add_refs (steps_of_proof proof)
+ (* "rev" should have the same effect as "sort canonical_label_ord" *)
+ |> Canonical_Lbl_Tab.map (K rev)
+ |> Unsynchronized.ref
+
+ fun get_successors l = Canonical_Lbl_Tab.lookup_list (!tab) l
+ fun set_successors l refs = tab := Canonical_Lbl_Tab.update (l, refs) (!tab)
+ fun replace_successor old new dest =
+ get_successors dest
+ |> Ord_List.remove canonical_label_ord old
+ |> Ord_List.union canonical_label_ord new
+ |> set_successors dest
+ in
+ (get_successors, replace_successor)
+ end
+
+ (** elimination of trivial, one-step subproofs **)
+
+ fun elim_subproofs' time qs fix l t lfs gfs meth subs nontriv_subs =
+ if null subs orelse not (compress_further ()) then
+ (set_preplay_outcome l (Played time);
+ Prove (qs, fix, l, t, List.revAppend (nontriv_subs, subs), ((lfs, gfs), meth)))
+ else
+ (case subs of
+ (sub as Proof (_, assms, sub_steps)) :: subs =>
+ (let
+ (* trivial subproofs have exactly one Prove step *)
+ val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), _))) = try the_single sub_steps
+
+ (* only touch proofs that can be preplayed sucessfully *)
+ val Played time' = get_preplay_outcome l'
+
+ (* merge steps *)
+ val subs'' = subs @ nontriv_subs
+ val lfs'' =
+ subtract (op =) (map fst assms) lfs'
+ |> union (op =) lfs
+ val gfs'' = union (op =) gfs' gfs
+ val by = ((lfs'', gfs''), meth)
+ val step'' = Prove (qs, fix, l, t, subs'', by)
+
+ (* check if the modified step can be preplayed fast enough *)
+ val timeout = time_mult merge_timeout_slack (Time.+(time, time'))
+ val Played time'' = preplay_quietly timeout step''
+
+ in
+ decrement_step_count (); (* l' successfully eliminated! *)
+ map (replace_successor l' [l]) lfs';
+ elim_subproofs' time'' qs fix l t lfs'' gfs'' meth subs nontriv_subs
+ end
+ handle Bind =>
+ elim_subproofs' time qs fix l t lfs gfs meth subs (sub :: nontriv_subs))
+ | _ => raise Fail "Sledgehammer_Isar_Compress: elim_subproofs'")
+
+ fun elim_subproofs (step as Let _) = step
+ | elim_subproofs (step as Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meth))) =
+ if subproofs = [] then
+ step
+ else
+ (case get_preplay_outcome l of
+ Played time => elim_subproofs' time qs fix l t lfs gfs meth subproofs []
+ | _ => step)
+
+ (** top_level compression: eliminate steps by merging them into their
+ successors **)
+
+ fun compress_top_level steps =
+ let
+ (* (#successors, (size_of_term t, position)) *)
+ fun cand_key (i, l, t_size) = (get_successors l |> length, (t_size, i))
+
+ val compression_ord =
+ prod_ord int_ord (prod_ord (int_ord #> rev_order) int_ord)
+ #> rev_order
+
+ val cand_ord = pairself cand_key #> compression_ord
+
+ fun pop_next_cand candidates =
+ (case max_list cand_ord candidates of
+ NONE => (NONE, [])
+ | cand as SOME (i, _, _) => (cand, filter_out (fn (j, _, _) => j = i) candidates))
+
+ val candidates =
+ let
+ fun add_cand (_, Let _) = I
+ | add_cand (i, Prove (_, _, l, t, _, _)) = cons (i, l, size_of_term t)
+ in
+ (steps
+ |> split_last |> fst (* keep last step *)
+ |> fold_index add_cand) []
+ end
+
+ fun try_eliminate (i, l, _) succ_lbls steps =
+ let
+ (* only touch steps that can be preplayed successfully *)
+ val Played time = get_preplay_outcome l
+
+ val succ_times =
+ map (get_preplay_outcome #> (fn Played t => t)) succ_lbls
+ val timeslice = time_mult (1.0 / (Real.fromInt (length succ_lbls))) time
+ val timeouts =
+ map (curry Time.+ timeslice #> time_mult merge_timeout_slack) succ_times
+
+ val ((cand as Prove (_, _, l, _, _, ((lfs, _), _))) :: steps') = drop i steps
+
+ (* FIXME: debugging *)
+ val _ =
+ if the (label_of_step cand) <> l then
+ raise Fail "Sledgehammer_Isar_Compress: try_eliminate"
+ else
+ ()
+
+ val succs = collect_successors steps' succ_lbls
+ val succs' = map (try_merge cand #> the) succs
+
+ (* TODO: should be lazy: stop preplaying as soon as one step fails/times out *)
+ val play_outcomes = map2 preplay_quietly timeouts succs'
+
+ (* ensure none of the modified successors timed out *)
+ val true = List.all (fn Played _ => true) play_outcomes
+
+ val (steps1, _ :: steps2) = chop i steps
+ (* replace successors with their modified versions *)
+ val steps2 = update_steps steps2 succs'
+ in
+ decrement_step_count (); (* candidate successfully eliminated *)
+ map2 set_preplay_outcome succ_lbls play_outcomes;
+ map (replace_successor l succ_lbls) lfs;
+ (* removing the step would mess up the indices -> replace with dummy step instead *)
+ steps1 @ dummy_isar_step :: steps2
+ end
+ handle Bind => steps
+ | Match => steps
+ | Option.Option => steps
+
+ fun compression_loop candidates steps =
+ if not (compress_further ()) then
+ steps
+ else
+ (case pop_next_cand candidates of
+ (NONE, _) => steps (* no more candidates for elimination *)
+ | (SOME (cand as (_, l, _)), candidates) =>
+ let val successors = get_successors l in
+ if length successors > compress_degree then steps
+ else compression_loop candidates (try_eliminate cand successors steps)
+ end)
+ in
+ compression_loop candidates steps
+ |> remove (op =) dummy_isar_step
+ end
+
+ (** recusion over the proof tree **)
+ (*
+ Proofs are compressed bottom-up, beginning with the innermost
+ subproofs.
+ On the innermost proof level, the proof steps have no subproofs.
+ In the best case, these steps can be merged into just one step,
+ resulting in a trivial subproof. Going one level up, trivial subproofs
+ can be eliminated. In the best case, this once again leads to a proof
+ whose proof steps do not have subproofs. Applying this approach
+ recursively will result in a flat proof in the best cast.
+ *)
+ fun do_proof (proof as (Proof (fix, assms, steps))) =
+ if compress_further () then Proof (fix, assms, do_steps steps) else proof
+ and do_steps steps =
+ (* bottom-up: compress innermost proofs first *)
+ steps |> map (fn step => step |> compress_further () ? do_sub_levels)
+ |> compress_further () ? compress_top_level
+ and do_sub_levels (Let x) = Let x
+ | do_sub_levels (Prove (qs, xs, l, t, subproofs, by)) =
+ (* compress subproofs *)
+ Prove (qs, xs, l, t, map do_proof subproofs, by)
+ (* eliminate trivial subproofs *)
+ |> compress_further () ? elim_subproofs
+ in
+ do_proof proof
+ end
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Fri Jan 31 10:23:32 2014 +0100
@@ -0,0 +1,95 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
+ Author: Steffen Juilf Smolka, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
+
+Minimize dependencies (used facts) of Isar proof steps.
+*)
+
+signature SLEDGEHAMMER_ISAR_MINIMIZE =
+sig
+ type preplay_interface = Sledgehammer_Isar_Preplay.preplay_interface
+ type isar_step = Sledgehammer_Isar_Proof.isar_step
+ type isar_proof = Sledgehammer_Isar_Proof.isar_proof
+
+ val min_deps_of_step : preplay_interface -> isar_step -> isar_step
+ val postprocess_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
+end;
+
+structure Sledgehammer_Isar_Minimize : SLEDGEHAMMER_ISAR_MINIMIZE =
+struct
+
+open Sledgehammer_Util
+open Sledgehammer_Reconstructor
+open Sledgehammer_Isar_Proof
+open Sledgehammer_Isar_Preplay
+
+val slack = seconds 0.1
+
+fun min_deps_of_step (_ : preplay_interface) (step as Let _) = step
+ | min_deps_of_step {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
+ (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
+ (case get_preplay_outcome l of
+ Played time =>
+ let
+ fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))
+ val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
+
+ fun minimize_facts _ time min_facts [] = (time, min_facts)
+ | minimize_facts mk_step time min_facts (f :: facts) =
+ (case preplay_quietly (Time.+ (time, slack)) (mk_step (min_facts @ facts)) of
+ Played time => minimize_facts mk_step time min_facts facts
+ | _ => minimize_facts mk_step time (f :: min_facts) facts)
+
+ val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs
+ val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
+ in
+ set_preplay_outcome l (Played time); mk_step_lfs_gfs min_lfs min_gfs
+ end
+ | _ => step (* don't touch steps that time out or fail *))
+
+fun postprocess_remove_unreferenced_steps postproc_step =
+ let
+ val add_lfs = fold (Ord_List.insert label_ord)
+
+ fun do_proof (Proof (fix, assms, steps)) =
+ let val (refed, steps) = do_steps steps in
+ (refed, Proof (fix, assms, steps))
+ end
+ and do_steps [] = ([], [])
+ | do_steps steps =
+ let
+ (* the last step is always implicitly referenced *)
+ val (steps, (refed, concl)) =
+ split_last steps
+ ||> do_refed_step
+ in
+ fold_rev do_step steps (refed, [concl])
+ end
+ and do_step step (refed, accu) =
+ (case label_of_step step of
+ NONE => (refed, step :: accu)
+ | SOME l =>
+ if Ord_List.member label_ord refed l then
+ do_refed_step step
+ |>> Ord_List.union label_ord refed
+ ||> (fn x => x :: accu)
+ else
+ (refed, accu))
+ and do_refed_step step = step |> postproc_step |> do_refed_step'
+ and do_refed_step' (Let _) = raise Fail "Sledgehammer_Isar_Minimize"
+ | do_refed_step' (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) =
+ let
+ val (refed, subproofs) =
+ map do_proof subproofs
+ |> split_list
+ |>> Ord_List.unions label_ord
+ |>> add_lfs lfs
+ val step = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))
+ in
+ (refed, step)
+ end
+ in
+ snd o do_proof
+ end
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Fri Jan 31 10:23:32 2014 +0100
@@ -0,0 +1,252 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
+ Author: Steffen Juilf Smolka, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
+
+Preplaying of Isar proofs.
+*)
+
+signature SLEDGEHAMMER_ISAR_PREPLAY =
+sig
+ type play_outcome = Sledgehammer_Reconstructor.play_outcome
+ type isar_proof = Sledgehammer_Isar_Proof.isar_proof
+ type isar_step = Sledgehammer_Isar_Proof.isar_step
+ type label = Sledgehammer_Isar_Proof.label
+
+ val trace: bool Config.T
+
+ type preplay_interface =
+ {get_preplay_outcome: label -> play_outcome,
+ set_preplay_outcome: label -> play_outcome -> unit,
+ preplay_quietly: Time.time -> isar_step -> play_outcome,
+ overall_preplay_outcome: isar_proof -> play_outcome}
+
+ val proof_preplay_interface: bool -> Proof.context -> string -> string -> bool -> Time.time ->
+ isar_proof -> preplay_interface
+end;
+
+structure Sledgehammer_Isar_Preplay : SLEDGEHAMMER_ISAR_PREPLAY =
+struct
+
+open ATP_Util
+open Sledgehammer_Util
+open Sledgehammer_Reconstructor
+open Sledgehammer_Isar_Proof
+
+val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false)
+
+fun preplay_trace ctxt assmsp concl result =
+ let
+ val ctxt = ctxt |> Config.put show_markup true
+ val assms = op @ assmsp
+ val time = "[" ^ string_of_play_outcome result ^ "]" |> Pretty.str
+ val nr_of_assms = length assms
+ val assms = assms
+ |> map (Display.pretty_thm ctxt)
+ |> (fn [] => Pretty.str ""
+ | [a] => a
+ | assms => Pretty.enum ";" "\<lbrakk>" "\<rbrakk>" assms) (* Syntax.pretty_term!? *)
+ val concl = concl |> Syntax.pretty_term ctxt
+ val trace_list = []
+ |> cons concl
+ |> nr_of_assms > 0 ? cons (Pretty.str "\<Longrightarrow>")
+ |> cons assms
+ |> cons time
+ val pretty_trace = Pretty.blk (2, Pretty.breaks trace_list)
+ in
+ tracing (Pretty.string_of pretty_trace)
+ end
+
+fun take_time timeout tac arg =
+ let val timing = Timing.start () in
+ (TimeLimit.timeLimit timeout tac arg; Played (#cpu (Timing.result timing)))
+ handle TimeLimit.TimeOut => Play_Timed_Out timeout
+ end
+
+fun resolve_fact_names ctxt names =
+ (names
+ |>> map string_of_label
+ |> pairself (maps (thms_of_name ctxt)))
+ handle ERROR msg => error ("preplay error: " ^ msg)
+
+fun thm_of_proof ctxt (Proof (fixed_frees, assms, steps)) =
+ let
+ val thy = Proof_Context.theory_of ctxt
+
+ val concl =
+ (case try List.last steps of
+ SOME (Prove (_, [], _, t, _, _)) => t
+ | _ => raise Fail "preplay error: malformed subproof")
+
+ val var_idx = maxidx_of_term concl + 1
+ fun var_of_free (x, T) = Var ((x, var_idx), T)
+ val subst = map (`var_of_free #> swap #> apfst Free) fixed_frees
+ in
+ Logic.list_implies (assms |> map snd, concl)
+ |> subst_free subst
+ |> Skip_Proof.make_thm thy
+ end
+
+fun tac_of_method meth type_enc lam_trans ctxt (local_facts, global_facts) =
+ Method.insert_tac local_facts THEN'
+ (case meth of
+ Meson_Method => Meson.meson_tac ctxt global_facts
+ | Metis_Method => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt global_facts
+ | _ =>
+ Method.insert_tac global_facts THEN'
+ (case meth of
+ Simp_Method => Simplifier.asm_full_simp_tac ctxt
+ | Simp_Size_Method =>
+ Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
+ | Auto_Method => K (Clasimp.auto_tac ctxt)
+ | Fastforce_Method => Clasimp.fast_force_tac ctxt
+ | Force_Method => Clasimp.force_tac ctxt
+ | Arith_Method => Arith_Data.arith_tac ctxt
+ | Blast_Method => blast_tac ctxt
+ | _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
+
+(* main function for preplaying Isar steps; may throw exceptions *)
+fun preplay_raw _ _ _ _ _ (Let _) = Played Time.zeroTime
+ | preplay_raw debug type_enc lam_trans ctxt timeout
+ (Prove (_, xs, _, t, subproofs, (fact_names, (meth :: _) :: _))) =
+ let
+ val goal =
+ (case xs of
+ [] => t
+ | _ =>
+ (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
+ (cf. "~~/src/Pure/Isar/obtain.ML") *)
+ let
+ (* FIXME: generate fresh name *)
+ val thesis = Free ("thesis", HOLogic.boolT)
+ val thesis_prop = thesis |> HOLogic.mk_Trueprop
+ val frees = map Free xs
+
+ (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
+ val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
+ in
+ (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
+ Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
+ end)
+
+ val facts =
+ resolve_fact_names ctxt fact_names
+ |>> append (map (thm_of_proof ctxt) subproofs)
+
+ val ctxt' = ctxt |> silence_reconstructors debug
+
+ fun prove () =
+ Goal.prove ctxt' [] [] goal (fn {context = ctxt, ...} =>
+ HEADGOAL (tac_of_method meth type_enc lam_trans ctxt facts))
+ handle ERROR msg => error ("Preplay error: " ^ msg)
+
+ val play_outcome = take_time timeout prove ()
+ in
+ (if Config.get ctxt trace then preplay_trace ctxt facts goal play_outcome else ();
+ play_outcome)
+ end
+
+
+(*** proof preplay interface ***)
+
+type preplay_interface =
+ {get_preplay_outcome: label -> play_outcome,
+ set_preplay_outcome: label -> play_outcome -> unit,
+ preplay_quietly: Time.time -> isar_step -> play_outcome,
+ overall_preplay_outcome: isar_proof -> play_outcome}
+
+fun enrich_context_with_local_facts proof ctxt =
+ let
+ val thy = Proof_Context.theory_of ctxt
+
+ fun enrich_with_fact l t =
+ Proof_Context.put_thms false (string_of_label l, SOME [Skip_Proof.make_thm thy t])
+
+ val enrich_with_assms = fold (uncurry enrich_with_fact)
+
+ fun enrich_with_proof (Proof (_, assms, isar_steps)) =
+ enrich_with_assms assms #> fold enrich_with_step isar_steps
+ and enrich_with_step (Let _) = I
+ | enrich_with_step (Prove (_, _, l, t, subproofs, _)) =
+ enrich_with_fact l t #> fold enrich_with_proof subproofs
+ in
+ enrich_with_proof proof ctxt
+ end
+
+fun merge_preplay_outcomes _ Play_Failed = Play_Failed
+ | merge_preplay_outcomes Play_Failed _ = Play_Failed
+ | merge_preplay_outcomes (Play_Timed_Out t1) (Play_Timed_Out t2) =
+ Play_Timed_Out (Time.+ (t1, t2))
+ | merge_preplay_outcomes (Played t1) (Play_Timed_Out t2) = Play_Timed_Out (Time.+ (t1, t2))
+ | merge_preplay_outcomes (Play_Timed_Out t1) (Played t2) = Play_Timed_Out (Time.+ (t1, t2))
+ | merge_preplay_outcomes (Played t1) (Played t2) = Played (Time.+ (t1, t2))
+
+(* Given a proof, produces an imperative preplay interface with a shared table mapping from labels
+ to preplay results. The preplay results are caluclated lazyly and cached to avoid repeated
+ calculation.
+
+ Precondition: The proof must be labeled canonically; cf.
+ "Slegehammer_Proof.relabel_proof_canonically". *)
+fun proof_preplay_interface debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
+ if not do_preplay then
+ (* the "dont_preplay" option pretends that everything works just fine *)
+ {get_preplay_outcome = K (Played Time.zeroTime),
+ set_preplay_outcome = K (K ()),
+ preplay_quietly = K (K (Played Time.zeroTime)),
+ overall_preplay_outcome = K (Played Time.zeroTime)} : preplay_interface
+ else
+ let
+ val ctxt = enrich_context_with_local_facts proof ctxt
+
+ fun preplay quietly timeout step =
+ preplay_raw debug type_enc lam_trans ctxt timeout step
+ handle exn =>
+ if Exn.is_interrupt exn then
+ reraise exn
+ else
+ (if not quietly andalso debug then
+ warning ("Preplay failure:\n " ^ @{make_string} step ^ "\n " ^
+ @{make_string} exn)
+ else
+ ();
+ Play_Failed)
+
+ (* preplay steps treating exceptions like timeouts *)
+ fun preplay_quietly timeout = preplay true timeout
+
+ val preplay_tab =
+ let
+ fun add_step_to_tab step tab =
+ (case label_of_step step of
+ NONE => tab
+ | SOME l =>
+ Canonical_Lbl_Tab.update_new
+ (l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy) tab)
+ handle Canonical_Lbl_Tab.DUP _ =>
+ raise Fail "Sledgehammer_Isar_Preplay: preplay time table"
+ in
+ Canonical_Lbl_Tab.empty
+ |> fold_isar_steps add_step_to_tab (steps_of_proof proof)
+ |> Unsynchronized.ref
+ end
+
+ fun get_preplay_outcome l =
+ Canonical_Lbl_Tab.lookup (!preplay_tab) l |> the |> Lazy.force
+ handle Option.Option => raise Fail "Sledgehammer_Isar_Preplay: preplay time table"
+
+ fun set_preplay_outcome l result =
+ preplay_tab := Canonical_Lbl_Tab.update (l, Lazy.value result) (!preplay_tab)
+
+ val result_of_step =
+ try (label_of_step #> the #> get_preplay_outcome)
+ #> the_default (Played Time.zeroTime)
+
+ fun overall_preplay_outcome (Proof (_, _, steps)) =
+ fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
+ in
+ {get_preplay_outcome = get_preplay_outcome,
+ set_preplay_outcome = set_preplay_outcome,
+ preplay_quietly = preplay_quietly,
+ overall_preplay_outcome = overall_preplay_outcome}
+ end
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_print.ML Fri Jan 31 10:23:32 2014 +0100
@@ -0,0 +1,262 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_print.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Author: Steffen Juilf Smolka, TU Muenchen
+
+Basic mapping from proof data structures to proof strings.
+*)
+
+signature SLEDGEHAMMER_ISAR_PRINT =
+sig
+ type isar_proof = Sledgehammer_Isar_Proof.isar_proof
+ type reconstructor = Sledgehammer_Reconstructor.reconstructor
+ type one_line_params = Sledgehammer_Reconstructor.one_line_params
+
+ val string_of_reconstructor : reconstructor -> string
+ val one_line_proof_text : int -> one_line_params -> string
+ val string_of_proof : Proof.context -> string -> string -> int -> int -> isar_proof -> string
+end;
+
+structure Sledgehammer_Isar_Print : SLEDGEHAMMER_ISAR_PRINT =
+struct
+
+open ATP_Util
+open ATP_Proof
+open ATP_Problem_Generate
+open ATP_Proof_Reconstruct
+open Sledgehammer_Util
+open Sledgehammer_Reconstructor
+open Sledgehammer_Isar_Proof
+open Sledgehammer_Isar_Annotate
+
+
+(** reconstructors **)
+
+fun string_of_reconstructor (Metis (type_enc, lam_trans)) = metis_call type_enc lam_trans
+ | string_of_reconstructor SMT = smtN
+
+
+(** one-liner reconstructor proofs **)
+
+fun show_time NONE = ""
+ | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
+
+(* FIXME: Various bugs, esp. with "unfolding"
+fun unusing_chained_facts _ 0 = ""
+ | unusing_chained_facts used_chaineds num_chained =
+ if length used_chaineds = num_chained then ""
+ else if null used_chaineds then "(* using no facts *) "
+ else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
+*)
+
+fun apply_on_subgoal _ 1 = "by "
+ | apply_on_subgoal 1 _ = "apply "
+ | apply_on_subgoal i n =
+ "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
+
+fun using_labels [] = ""
+ | using_labels ls = "using " ^ space_implode " " (map string_of_label ls) ^ " "
+
+fun command_call name [] =
+ name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
+ | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
+
+fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =
+ (* unusing_chained_facts used_chaineds num_chained ^ *)
+ using_labels ls ^ apply_on_subgoal i n ^ command_call (string_of_reconstructor reconstr) ss
+
+fun try_command_line banner time command =
+ banner ^ ": " ^
+ Active.sendback_markup [Markup.padding_command] command ^
+ show_time time ^ "."
+
+fun minimize_line _ [] = ""
+ | minimize_line minimize_command ss =
+ (case minimize_command ss of
+ "" => ""
+ | command => "\nTo minimize: " ^ Active.sendback_markup [Markup.padding_command] command ^ ".")
+
+fun split_used_facts facts =
+ facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
+ |> pairself (sort_distinct (string_ord o pairself fst))
+
+fun one_line_proof_text num_chained
+ ((reconstr, play), banner, used_facts, minimize_command, subgoal, subgoal_count) =
+ let
+ val (chained, extra) = split_used_facts used_facts
+ val (failed, ext_time) =
+ (case play of
+ Played time => (false, (SOME (false, time)))
+ | Play_Timed_Out time => (false, SOME (true, time))
+ | Play_Failed => (true, NONE)
+ | Not_Played => (false, NONE))
+ val try_line =
+ ([], map fst extra)
+ |> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained
+ |> (if failed then
+ enclose "One-line proof reconstruction failed: "
+ ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
+ \solve this.)"
+ else
+ try_command_line banner ext_time)
+ in
+ try_line ^ minimize_line minimize_command (map fst (extra @ chained))
+ end
+
+
+(** detailed Isar proofs **)
+
+val indent_size = 2
+
+fun string_of_proof ctxt type_enc lam_trans i n proof =
+ let
+ (* Make sure only type constraints inserted by the type annotation code are printed. *)
+ val ctxt =
+ ctxt |> Config.put show_markup false
+ |> Config.put Printer.show_type_emphasis false
+ |> Config.put show_types false
+ |> Config.put show_sorts false
+ |> Config.put show_consts false
+
+ val register_fixes = map Free #> fold Variable.auto_fixes
+
+ fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
+
+ fun of_indent ind = replicate_string (ind * indent_size) " "
+ fun of_moreover ind = of_indent ind ^ "moreover\n"
+ fun of_label l = if l = no_label then "" else string_of_label l ^ ": "
+
+ fun of_obtain qs nr =
+ (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
+ "ultimately "
+ else if nr = 1 orelse member (op =) qs Then then
+ "then "
+ else
+ "") ^ "obtain"
+
+ fun of_show_have qs = if member (op =) qs Show then "show" else "have"
+ fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence"
+
+ fun of_have qs nr =
+ if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
+ "ultimately " ^ of_show_have qs
+ else if nr = 1 orelse member (op =) qs Then then
+ of_thus_hence qs
+ else
+ of_show_have qs
+
+ fun add_term term (s, ctxt) =
+ (s ^ (term
+ |> singleton (Syntax.uncheck_terms ctxt)
+ |> annotate_types ctxt
+ |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
+ |> simplify_spaces
+ |> maybe_quote),
+ ctxt |> Variable.auto_fixes term)
+
+ fun by_method meth = "by " ^
+ (case meth of
+ Simp_Method => "simp"
+ | Simp_Size_Method => "(simp add: size_ne_size_imp_ne)"
+ | Auto_Method => "auto"
+ | Fastforce_Method => "fastforce"
+ | Force_Method => "force"
+ | Arith_Method => "arith"
+ | Blast_Method => "blast"
+ | Meson_Method => "meson"
+ | _ => raise Fail "Sledgehammer_Isar_Print: by_method")
+
+ fun with_facts none _ [] [] = none
+ | with_facts _ some ls ss = some (space_implode " " (map string_of_label ls @ ss))
+
+ val using_facts = with_facts "" (enclose "using " " ")
+
+ (* Local facts are always passed via "using", which affects "meson" and "metis". This is
+ arguably stylistically superior, because it emphasises the structure of the proof. It is also
+ more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence"
+ and "thus" is introduced. See also "tac_of_method" in "Sledgehammer_Isar_Preplay". *)
+ fun of_method ls ss Metis_Method =
+ using_facts ls [] ^ reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 ([], ss)
+ | of_method ls ss Meson_Method =
+ using_facts ls [] ^ with_facts "by meson" (enclose "by (meson " ")") [] ss
+ | of_method ls ss meth = using_facts ls ss ^ by_method meth
+
+ fun of_byline ind (ls, ss) meth =
+ let
+ val ls = ls |> sort_distinct label_ord
+ val ss = ss |> sort_distinct string_ord
+ in
+ "\n" ^ of_indent (ind + 1) ^ of_method ls ss meth
+ end
+
+ fun of_free (s, T) =
+ maybe_quote s ^ " :: " ^
+ maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T))
+
+ fun add_frees xs (s, ctxt) =
+ (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs)
+
+ fun add_fix _ [] = I
+ | add_fix ind xs =
+ add_suffix (of_indent ind ^ "fix ")
+ #> add_frees xs
+ #> add_suffix "\n"
+
+ fun add_assm ind (l, t) =
+ add_suffix (of_indent ind ^ "assume " ^ of_label l)
+ #> add_term t
+ #> add_suffix "\n"
+
+ fun add_assms ind assms = fold (add_assm ind) assms
+
+ fun add_step_post ind l t facts meth =
+ add_suffix (of_label l)
+ #> add_term t
+ #> add_suffix (of_byline ind facts meth ^ "\n")
+
+ fun of_subproof ind ctxt proof =
+ let
+ val ind = ind + 1
+ val s = of_proof ind ctxt proof
+ val prefix = "{ "
+ val suffix = " }"
+ in
+ replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
+ String.extract (s, ind * indent_size, SOME (size s - ind * indent_size - 1)) ^
+ suffix ^ "\n"
+ end
+ and of_subproofs _ _ _ [] = ""
+ | of_subproofs ind ctxt qs subproofs =
+ (if member (op =) qs Then then of_moreover ind else "") ^
+ space_implode (of_moreover ind) (map (of_subproof ind ctxt) subproofs)
+ and add_step_pre ind qs subproofs (s, ctxt) =
+ (s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt)
+ and add_step ind (Let (t1, t2)) =
+ add_suffix (of_indent ind ^ "let ")
+ #> add_term t1
+ #> add_suffix " = "
+ #> add_term t2
+ #> add_suffix "\n"
+ | add_step ind (Prove (qs, xs, l, t, subproofs, (facts, (meth :: _) :: _))) =
+ add_step_pre ind qs subproofs
+ #> (case xs of
+ [] => add_suffix (of_have qs (length subproofs) ^ " ")
+ | _ =>
+ add_suffix (of_obtain qs (length subproofs) ^ " ")
+ #> add_frees xs
+ #> add_suffix " where ")
+ #> add_step_post ind l t facts meth
+ and add_steps ind = fold (add_step ind)
+ and of_proof ind ctxt (Proof (xs, assms, steps)) =
+ ("", ctxt) |> add_fix ind xs |> add_assms ind assms |> add_steps ind steps |> fst
+ in
+ (* One-step Metis proofs are pointless; better use the one-liner directly. *)
+ (case proof of
+ Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *)
+ | Proof ([], [], [Prove (_, [], _, _, [], (_, (Metis_Method :: _) :: _))]) => ""
+ | _ =>
+ (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
+ of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
+ of_indent 0 ^ (if n <> 1 then "next" else "qed"))
+ end
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Fri Jan 31 10:23:32 2014 +0100
@@ -0,0 +1,157 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
+ Author: Jasmin Blanchette, TU Muenchen
+ Author: Steffen Juilf Smolka, TU Muenchen
+
+Basic data structures for representing and basic methods
+for dealing with Isar proof texts.
+*)
+
+signature SLEDGEHAMMER_ISAR_PROOF =
+sig
+ type label = string * int
+ type facts = label list * string list (* local and global facts *)
+
+ datatype isar_qualifier = Show | Then
+
+ datatype isar_proof =
+ Proof of (string * typ) list * (label * term) list * isar_step list
+ and isar_step =
+ Let of term * term |
+ Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
+ (facts * proof_method list list)
+ and proof_method =
+ Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
+ Arith_Method | Blast_Method | Meson_Method
+
+ val no_label : label
+ val no_facts : facts
+
+ val label_ord : label * label -> order
+
+ val dummy_isar_step : isar_step
+
+ val string_of_label : label -> string
+
+ val fix_of_proof : isar_proof -> (string * typ) list
+ val assms_of_proof : isar_proof -> (label * term) list
+ val steps_of_proof : isar_proof -> isar_step list
+
+ val label_of_step : isar_step -> label option
+ val subproofs_of_step : isar_step -> isar_proof list option
+ val byline_of_step : isar_step -> (facts * proof_method list list) option
+
+ val fold_isar_step : (isar_step -> 'a -> 'a) -> isar_step -> 'a -> 'a
+ val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
+
+ val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
+
+ val add_proof_steps : isar_step list -> int -> int
+
+ (** canonical proof labels: 1, 2, 3, ... in postorder **)
+ val canonical_label_ord : (label * label) -> order
+ val relabel_proof_canonically : isar_proof -> isar_proof
+
+ structure Canonical_Lbl_Tab : TABLE
+end;
+
+structure Sledgehammer_Isar_Proof : SLEDGEHAMMER_ISAR_PROOF =
+struct
+
+type label = string * int
+type facts = label list * string list (* local and global facts *)
+
+datatype isar_qualifier = Show | Then
+
+datatype isar_proof =
+ Proof of (string * typ) list * (label * term) list * isar_step list
+and isar_step =
+ Let of term * term |
+ Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
+ (facts * proof_method list list)
+and proof_method =
+ Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
+ Arith_Method | Blast_Method | Meson_Method
+
+val no_label = ("", ~1)
+val no_facts = ([],[])
+
+val label_ord = pairself swap #> prod_ord int_ord fast_string_ord
+
+val dummy_isar_step = Let (Term.dummy, Term.dummy)
+
+fun string_of_label (s, num) = s ^ string_of_int num
+
+fun fix_of_proof (Proof (fix, _, _)) = fix
+fun assms_of_proof (Proof (_, assms, _)) = assms
+fun steps_of_proof (Proof (_, _, steps)) = steps
+
+fun label_of_step (Prove (_, _, l, _, _, _)) = SOME l
+ | label_of_step _ = NONE
+
+fun subproofs_of_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs
+ | subproofs_of_step _ = NONE
+
+fun byline_of_step (Prove (_, _, _, _, _, byline)) = SOME byline
+ | byline_of_step _ = NONE
+
+fun fold_isar_steps f = fold (fold_isar_step f)
+and fold_isar_step f step =
+ fold (steps_of_proof #> fold_isar_steps f) (these (subproofs_of_step step)) #> f step
+
+fun map_isar_steps f =
+ let
+ fun do_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map do_step steps)
+ and do_step (step as Let _) = f step
+ | do_step (Prove (qs, xs, l, t, subproofs, by)) =
+ f (Prove (qs, xs, l, t, map do_proof subproofs, by))
+ in
+ do_proof
+ end
+
+val add_proof_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I)
+
+
+(** canonical proof labels: 1, 2, 3, ... in post traversal order **)
+
+fun canonical_label_ord (((_, i1), (_, i2)) : label * label) = int_ord (i1, i2)
+
+structure Canonical_Lbl_Tab = Table(
+ type key = label
+ val ord = canonical_label_ord)
+
+fun relabel_proof_canonically proof =
+ let
+ fun next_label l (next, subst) =
+ let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end
+
+ fun do_byline by (_, subst) = apfst (apfst (map (AList.lookup (op =) subst #> the))) by
+ handle Option.Option =>
+ raise Fail "Sledgehammer_Isar_Proof: relabel_proof_canonically"
+
+ fun do_assm (l, t) state =
+ let
+ val (l, state) = next_label l state
+ in ((l, t), state) end
+
+ fun do_proof (Proof (fix, assms, steps)) state =
+ let
+ val (assms, state) = fold_map do_assm assms state
+ val (steps, state) = fold_map do_step steps state
+ in
+ (Proof (fix, assms, steps), state)
+ end
+
+ and do_step (step as Let _) state = (step, state)
+ | do_step (Prove (qs, fix, l, t, subproofs, by)) state=
+ let
+ val by = do_byline by state
+ val (subproofs, state) = fold_map do_proof subproofs state
+ val (l, state) = next_label l state
+ in
+ (Prove (qs, fix, l, t, subproofs, by), state)
+ end
+ in
+ fst (do_proof proof (0, []))
+ end
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML Fri Jan 31 10:23:32 2014 +0100
@@ -0,0 +1,53 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML
+ Author: Steffen Juilf Smolka, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
+
+Try replacing calls to "metis" with calls to other proof methods to speed up proofs, eliminate
+dependencies, and repair broken proof steps.
+*)
+
+signature SLEDGEHAMMER_ISAR_TRY0 =
+sig
+ type isar_proof = Sledgehammer_Isar_Proof.isar_proof
+ type preplay_interface = Sledgehammer_Isar_Preplay.preplay_interface
+
+ val try0 : Time.time -> preplay_interface -> isar_proof -> isar_proof
+end;
+
+structure Sledgehammer_Isar_Try0 : SLEDGEHAMMER_ISAR_TRY0 =
+struct
+
+open Sledgehammer_Util
+open Sledgehammer_Reconstructor
+open Sledgehammer_Isar_Proof
+open Sledgehammer_Isar_Preplay
+
+fun variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, methss))) =
+ map (fn meth => Prove (qs, xs, l, t, subproofs, (facts, [[meth]]))) (tl (flat methss))
+ | variants_of_step _ = raise Fail "Sledgehammer_Isar_Try0: variants_of_step"
+
+val slack = seconds 0.05
+
+fun try0_step _ _ (step as Let _) = step
+ | try0_step preplay_timeout
+ ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_interface)
+ (step as Prove (_, _, l, _, _, _)) =
+ let
+ val timeout =
+ (case get_preplay_outcome l of
+ Played time => Time.+ (time, slack)
+ | _ => preplay_timeout)
+
+ fun try_variant variant =
+ (case preplay_quietly timeout variant of
+ result as Played _ => SOME (variant, result)
+ | _ => NONE)
+ in
+ (case Par_List.get_some try_variant (variants_of_step step) of
+ SOME (step', result) => (set_preplay_outcome l result; step')
+ | NONE => step)
+ end
+
+val try0 = map_isar_steps oo try0_step
+
+end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jan 31 10:23:32 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jan 31 10:23:32 2014 +0100
@@ -107,7 +107,7 @@
open Sledgehammer_Util
open Sledgehammer_Fact
open Sledgehammer_Prover
-open Sledgehammer_Minimize
+open Sledgehammer_Prover_Minimize
open Sledgehammer_MePo
val trace =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jan 31 10:23:32 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,336 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
- Author: Philipp Meyer, TU Muenchen
- Author: Jasmin Blanchette, TU Muenchen
-
-Minimization of fact list for Metis using external provers.
-*)
-
-signature SLEDGEHAMMER_MINIMIZE =
-sig
- type stature = ATP_Problem_Generate.stature
- type reconstructor = Sledgehammer_Reconstructor.reconstructor
- type play_outcome = Sledgehammer_Reconstructor.play_outcome
- type mode = Sledgehammer_Prover.mode
- type params = Sledgehammer_Prover.params
- type prover = Sledgehammer_Prover.prover
-
- val binary_min_facts : int Config.T
- val auto_minimize_min_facts : int Config.T
- val auto_minimize_max_time : real Config.T
- val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int ->
- Proof.state -> thm -> (reconstructor * play_outcome) Lazy.lazy option ->
- ((string * stature) * thm list) list ->
- ((string * stature) * thm list) list option
- * ((reconstructor * play_outcome) Lazy.lazy * ((reconstructor * play_outcome) -> string)
- * string)
- val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover
- val run_minimize : params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list ->
- Proof.state -> unit
-end;
-
-structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
-struct
-
-open ATP_Util
-open ATP_Proof
-open ATP_Problem_Generate
-open ATP_Systems
-open Sledgehammer_Util
-open Sledgehammer_Fact
-open Sledgehammer_Reconstructor
-open Sledgehammer_Reconstruct
-open Sledgehammer_Prover
-
-(* wrapper for calling external prover *)
-
-fun n_facts names =
- let val n = length names in
- string_of_int n ^ " fact" ^ plural_s n ^
- (if n > 0 then
- ": " ^ (names |> map fst |> sort string_ord |> space_implode " ")
- else
- "")
- end
-
-fun print silent f = if silent then () else Output.urgent_message (f ())
-
-fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
- type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress_isar, try0_isar,
- preplay_timeout, ...} : params)
- silent (prover : prover) timeout i n state goal facts =
- let
- val _ =
- print silent (fn () =>
- "Testing " ^ n_facts (map fst facts) ^
- (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...")
- val facts = facts |> maps (fn (n, ths) => map (pair n) ths)
- val params =
- {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = true,
- provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans,
- uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE,
- max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01),
- max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
- isar_proofs = isar_proofs, compress_isar = compress_isar, try0_isar = try0_isar,
- slice = false, minimize = SOME false, timeout = timeout, preplay_timeout = preplay_timeout,
- expect = ""}
- val problem =
- {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
- factss = [("", facts)]}
- val result as {outcome, used_facts, run_time, ...} =
- prover params (K (K (K ""))) problem
- in
- print silent
- (fn () =>
- case outcome of
- SOME failure => string_of_atp_failure failure
- | NONE =>
- "Found proof" ^
- (if length used_facts = length facts then ""
- else " with " ^ n_facts used_facts) ^
- " (" ^ string_of_time run_time ^ ").");
- result
- end
-
-(* minimalization of facts *)
-
-(* Give the external prover 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 slack_msecs = 200
-
-fun new_timeout timeout run_time =
- Int.min (Time.toMilliseconds timeout, Time.toMilliseconds run_time + slack_msecs)
- |> Time.fromMilliseconds
-
-(* The linear algorithm usually outperforms the binary algorithm when over 60%
- of the facts are actually needed. The binary algorithm is much more
- appropriate for provers that cannot return the list of used facts and hence
- returns all facts as used. Since we cannot know in advance how many facts are
- actually needed, we heuristically set the threshold to 10 facts. *)
-val binary_min_facts =
- Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts}
- (K 20)
-val auto_minimize_min_facts =
- Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
- (fn generic => Config.get_generic generic binary_min_facts)
-val auto_minimize_max_time =
- Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time}
- (K 5.0)
-
-fun linear_minimize test timeout result xs =
- let
- fun min _ [] p = p
- | min timeout (x :: xs) (seen, result) =
- (case test timeout (xs @ seen) of
- result as {outcome = NONE, used_facts, run_time, ...} : prover_result =>
- min (new_timeout timeout run_time)
- (filter_used_facts true used_facts xs)
- (filter_used_facts false used_facts seen, result)
- | _ => min timeout xs (x :: seen, result))
- in
- min timeout xs ([], result)
- end
-
-fun binary_minimize test timeout result xs =
- let
- fun min depth (result as {run_time, ...} : prover_result) sup
- (xs as _ :: _ :: _) =
- let
- val (l0, r0) = chop (length xs div 2) xs
-(*
- val _ = warning (replicate_string depth " " ^ "{ " ^
- "sup: " ^ n_facts (map fst sup))
- val _ = warning (replicate_string depth " " ^ " " ^
- "xs: " ^ n_facts (map fst xs))
- val _ = warning (replicate_string depth " " ^ " " ^
- "l0: " ^ n_facts (map fst l0))
- val _ = warning (replicate_string depth " " ^ " " ^
- "r0: " ^ n_facts (map fst r0))
-*)
- val depth = depth + 1
- val timeout = new_timeout timeout run_time
- in
- case test timeout (sup @ l0) of
- result as {outcome = NONE, used_facts, ...} =>
- min depth result (filter_used_facts true used_facts sup)
- (filter_used_facts true used_facts l0)
- | _ =>
- case test timeout (sup @ r0) of
- result as {outcome = NONE, used_facts, ...} =>
- min depth result (filter_used_facts true used_facts sup)
- (filter_used_facts true used_facts r0)
- | _ =>
- let
- val (sup_r0, (l, result)) = min depth result (sup @ r0) l0
- val (sup, r0) =
- (sup, r0)
- |> pairself (filter_used_facts true (map fst sup_r0))
- val (sup_l, (r, result)) = min depth result (sup @ l) r0
- val sup = sup |> filter_used_facts true (map fst sup_l)
- in (sup, (l @ r, result)) end
- end
-(*
- |> tap (fn _ => warning (replicate_string depth " " ^ "}"))
-*)
- | min _ result sup xs = (sup, (xs, result))
- in
- case snd (min 0 result [] xs) of
- ([x], result as {run_time, ...}) =>
- (case test (new_timeout timeout run_time) [] of
- result as {outcome = NONE, ...} => ([], result)
- | _ => ([x], result))
- | p => p
- end
-
-fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent i n state goal
- preplay0 facts =
- let
- val ctxt = Proof.context_of state
- val prover = get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
- fun test timeout = test_facts params silent prover timeout i n state goal
- val (chained, non_chained) = List.partition is_fact_chained facts
- (* Push chained facts to the back, so that they are less likely to be
- kicked out by the linear minimization algorithm. *)
- val facts = non_chained @ chained
- in
- (print silent (fn () => "Sledgehammer minimizer: " ^ quote prover_name ^ ".");
- case test timeout facts of
- result as {outcome = NONE, used_facts, run_time, ...} =>
- let
- val facts = filter_used_facts true used_facts facts
- val min =
- if length facts >= Config.get ctxt binary_min_facts then binary_minimize
- else linear_minimize
- val (min_facts, {preplay, message, message_tail, ...}) =
- min test (new_timeout timeout run_time) result facts
- in
- print silent (fn () => cat_lines
- ["Minimized to " ^ n_facts (map fst min_facts)] ^
- (case min_facts |> filter is_fact_chained |> length of
- 0 => ""
- | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
- (if learn then do_learn (maps snd min_facts) else ());
- (SOME min_facts,
- (if is_some preplay0 andalso length min_facts = length facts then the preplay0
- else preplay,
- message, message_tail))
- end
- | {outcome = SOME TimedOut, preplay, ...} =>
- (NONE, (preplay, fn _ =>
- "Timeout: You can increase the time limit using the \"timeout\" option (e.g., \
- \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\").", ""))
- | {preplay, message, ...} => (NONE, (preplay, prefix "Prover error: " o message, "")))
- handle ERROR msg => (NONE, (Lazy.value (plain_metis, Play_Failed), fn _ => "Error: " ^ msg, ""))
- end
-
-fun adjust_reconstructor_params override_params
- ({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, lam_trans,
- uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters,
- max_new_mono_instances, isar_proofs, compress_isar, try0_isar, slice, minimize, timeout,
- preplay_timeout, expect} : params) =
- let
- fun lookup_override name default_value =
- case AList.lookup (op =) override_params name of
- SOME [s] => SOME s
- | _ => default_value
- (* Only those options that reconstructors are interested in are considered
- here. *)
- val type_enc = lookup_override "type_enc" type_enc
- val lam_trans = lookup_override "lam_trans" lam_trans
- in
- {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking,
- provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans,
- uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
- max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
- max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
- compress_isar = compress_isar, try0_isar = try0_isar, slice = slice, minimize = minimize,
- timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
- end
-
-fun maybe_minimize ctxt mode do_learn name
- (params as {verbose, isar_proofs, minimize, ...})
- ({state, goal, subgoal, subgoal_count, ...} : prover_problem)
- (result as {outcome, used_facts, used_from, run_time, preplay, message,
- message_tail} : prover_result) =
- if is_some outcome orelse null used_facts then
- result
- else
- let
- val num_facts = length used_facts
- val ((perhaps_minimize, (minimize_name, params)), preplay) =
- if mode = Normal then
- if num_facts >= Config.get ctxt auto_minimize_min_facts then
- ((true, (name, params)), preplay)
- else
- let
- fun can_min_fast_enough time =
- 0.001
- * Real.fromInt ((num_facts + 1) * Time.toMilliseconds time)
- <= Config.get ctxt auto_minimize_max_time
- fun prover_fast_enough () = can_min_fast_enough run_time
- in
- (case Lazy.force preplay of
- (reconstr as Metis _, Played timeout) =>
- if isar_proofs = SOME true then
- (* Cheat: Assume the selected ATP is as fast as "metis" for the goal it proved
- itself. *)
- (can_min_fast_enough timeout, (isar_proof_reconstructor ctxt name, params))
- else if can_min_fast_enough timeout then
- (true, extract_reconstructor params reconstr
- ||> (fn override_params =>
- adjust_reconstructor_params override_params params))
- else
- (prover_fast_enough (), (name, params))
- | (SMT, Played timeout) =>
- (* Cheat: Assume the original prover is as fast as "smt" for the goal it proved
- itself. *)
- (can_min_fast_enough timeout, (name, params))
- | _ => (prover_fast_enough (), (name, params)),
- preplay)
- end
- else
- ((false, (name, params)), preplay)
- val minimize = minimize |> the_default perhaps_minimize
- val (used_facts, (preplay, message, _)) =
- if minimize then
- minimize_facts do_learn minimize_name params
- (not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal subgoal_count state
- goal (SOME preplay) (filter_used_facts true used_facts (map (apsnd single) used_from))
- |>> Option.map (map fst)
- else
- (SOME used_facts, (preplay, message, ""))
- in
- case used_facts of
- SOME used_facts =>
- {outcome = NONE, used_facts = used_facts, used_from = used_from,
- run_time = run_time, preplay = preplay, message = message,
- message_tail = message_tail}
- | NONE => result
- end
-
-fun get_minimizing_prover ctxt mode do_learn name params minimize_command
- problem =
- get_prover ctxt mode name params minimize_command problem
- |> maybe_minimize ctxt mode do_learn name params problem
-
-fun run_minimize (params as {provers, ...}) do_learn i refs state =
- let
- val ctxt = Proof.context_of state
- val {goal, facts = chained_ths, ...} = Proof.goal state
- val reserved = reserved_isar_keyword_table ()
- val css = clasimpset_rule_table_of ctxt
- val facts = refs |> maps (map (apsnd single) o fact_of_ref ctxt reserved chained_ths css)
- in
- case subgoal_count state of
- 0 => Output.urgent_message "No subgoal!"
- | n => case provers of
- [] => error "No prover is set."
- | prover :: _ =>
- (kill_provers ();
- minimize_facts do_learn prover params false i n state goal NONE facts
- |> (fn (_, (preplay, message, message_tail)) =>
- message (Lazy.force preplay) ^ message_tail
- |> Output.urgent_message))
- end
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML Fri Jan 31 10:23:32 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,95 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML
- Author: Steffen Juilf Smolka, TU Muenchen
- Author: Jasmin Blanchette, TU Muenchen
-
-Minimize dependencies (used facts) of Isar proof steps.
-*)
-
-signature SLEDGEHAMMER_MINIMIZE_ISAR =
-sig
- type preplay_interface = Sledgehammer_Preplay.preplay_interface
- type isar_step = Sledgehammer_Proof.isar_step
- type isar_proof = Sledgehammer_Proof.isar_proof
-
- val min_deps_of_step : preplay_interface -> isar_step -> isar_step
- val postprocess_remove_unreferenced_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
-end;
-
-structure Sledgehammer_Minimize_Isar : SLEDGEHAMMER_MINIMIZE_ISAR =
-struct
-
-open Sledgehammer_Util
-open Sledgehammer_Reconstructor
-open Sledgehammer_Proof
-open Sledgehammer_Preplay
-
-val slack = seconds 0.1
-
-fun min_deps_of_step (_ : preplay_interface) (step as Let _) = step
- | min_deps_of_step {get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...}
- (step as Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))) =
- (case get_preplay_outcome l of
- Played time =>
- let
- fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meth))
- val mk_step_gfs_lfs = curry (swap #> uncurry mk_step_lfs_gfs)
-
- fun minimize_facts _ time min_facts [] = (time, min_facts)
- | minimize_facts mk_step time min_facts (f :: facts) =
- (case preplay_quietly (Time.+ (time, slack)) (mk_step (min_facts @ facts)) of
- Played time => minimize_facts mk_step time min_facts facts
- | _ => minimize_facts mk_step time (f :: min_facts) facts)
-
- val (time, min_lfs) = minimize_facts (mk_step_gfs_lfs gfs) time [] lfs
- val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs
- in
- set_preplay_outcome l (Played time); mk_step_lfs_gfs min_lfs min_gfs
- end
- | _ => step (* don't touch steps that time out or fail *))
-
-fun postprocess_remove_unreferenced_steps postproc_step =
- let
- val add_lfs = fold (Ord_List.insert label_ord)
-
- fun do_proof (Proof (fix, assms, steps)) =
- let val (refed, steps) = do_steps steps in
- (refed, Proof (fix, assms, steps))
- end
- and do_steps [] = ([], [])
- | do_steps steps =
- let
- (* the last step is always implicitly referenced *)
- val (steps, (refed, concl)) =
- split_last steps
- ||> do_refed_step
- in
- fold_rev do_step steps (refed, [concl])
- end
- and do_step step (refed, accu) =
- (case label_of_step step of
- NONE => (refed, step :: accu)
- | SOME l =>
- if Ord_List.member label_ord refed l then
- do_refed_step step
- |>> Ord_List.union label_ord refed
- ||> (fn x => x :: accu)
- else
- (refed, accu))
- and do_refed_step step = step |> postproc_step |> do_refed_step'
- and do_refed_step' (Let _) = raise Fail "Sledgehammer_Minimize_Isar"
- | do_refed_step' (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) =
- let
- val (refed, subproofs) =
- map do_proof subproofs
- |> split_list
- |>> Ord_List.unions label_ord
- |>> add_lfs lfs
- val step = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))
- in
- (refed, step)
- end
- in
- snd o do_proof
- end
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri Jan 31 10:23:32 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,251 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
- Author: Steffen Juilf Smolka, TU Muenchen
- Author: Jasmin Blanchette, TU Muenchen
-
-Preplaying of Isar proofs.
-*)
-
-signature SLEDGEHAMMER_PREPLAY =
-sig
- type play_outcome = Sledgehammer_Reconstructor.play_outcome
- type isar_proof = Sledgehammer_Proof.isar_proof
- type isar_step = Sledgehammer_Proof.isar_step
- type label = Sledgehammer_Proof.label
-
- val trace: bool Config.T
-
- type preplay_interface =
- {get_preplay_outcome: label -> play_outcome,
- set_preplay_outcome: label -> play_outcome -> unit,
- preplay_quietly: Time.time -> isar_step -> play_outcome,
- overall_preplay_outcome: isar_proof -> play_outcome}
-
- val proof_preplay_interface: bool -> Proof.context -> string -> string -> bool -> Time.time ->
- isar_proof -> preplay_interface
-end;
-
-structure Sledgehammer_Preplay : SLEDGEHAMMER_PREPLAY =
-struct
-
-open ATP_Util
-open Sledgehammer_Util
-open Sledgehammer_Reconstructor
-open Sledgehammer_Proof
-
-val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false)
-
-fun preplay_trace ctxt assmsp concl result =
- let
- val ctxt = ctxt |> Config.put show_markup true
- val assms = op @ assmsp
- val time = "[" ^ string_of_play_outcome result ^ "]" |> Pretty.str
- val nr_of_assms = length assms
- val assms = assms
- |> map (Display.pretty_thm ctxt)
- |> (fn [] => Pretty.str ""
- | [a] => a
- | assms => Pretty.enum ";" "\<lbrakk>" "\<rbrakk>" assms) (* Syntax.pretty_term!? *)
- val concl = concl |> Syntax.pretty_term ctxt
- val trace_list = []
- |> cons concl
- |> nr_of_assms > 0 ? cons (Pretty.str "\<Longrightarrow>")
- |> cons assms
- |> cons time
- val pretty_trace = Pretty.blk (2, Pretty.breaks trace_list)
- in
- tracing (Pretty.string_of pretty_trace)
- end
-
-fun take_time timeout tac arg =
- let val timing = Timing.start () in
- (TimeLimit.timeLimit timeout tac arg; Played (#cpu (Timing.result timing)))
- handle TimeLimit.TimeOut => Play_Timed_Out timeout
- end
-
-fun resolve_fact_names ctxt names =
- (names
- |>> map string_of_label
- |> pairself (maps (thms_of_name ctxt)))
- handle ERROR msg => error ("preplay error: " ^ msg)
-
-fun thm_of_proof ctxt (Proof (fixed_frees, assms, steps)) =
- let
- val thy = Proof_Context.theory_of ctxt
-
- val concl =
- (case try List.last steps of
- SOME (Prove (_, [], _, t, _, _)) => t
- | _ => raise Fail "preplay error: malformed subproof")
-
- val var_idx = maxidx_of_term concl + 1
- fun var_of_free (x, T) = Var ((x, var_idx), T)
- val subst = map (`var_of_free #> swap #> apfst Free) fixed_frees
- in
- Logic.list_implies (assms |> map snd, concl)
- |> subst_free subst
- |> Skip_Proof.make_thm thy
- end
-
-fun tac_of_method meth type_enc lam_trans ctxt (local_facts, global_facts) =
- Method.insert_tac local_facts THEN'
- (case meth of
- Meson_Method => Meson.meson_tac ctxt global_facts
- | Metis_Method => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt global_facts
- | _ =>
- Method.insert_tac global_facts THEN'
- (case meth of
- Simp_Method => Simplifier.asm_full_simp_tac ctxt
- | Simp_Size_Method =>
- Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
- | Auto_Method => K (Clasimp.auto_tac ctxt)
- | Fastforce_Method => Clasimp.fast_force_tac ctxt
- | Force_Method => Clasimp.force_tac ctxt
- | Arith_Method => Arith_Data.arith_tac ctxt
- | Blast_Method => blast_tac ctxt
- | _ => raise Fail "Sledgehammer_Preplay: tac_of_method"))
-
-(* main function for preplaying Isar steps; may throw exceptions *)
-fun preplay_raw _ _ _ _ _ (Let _) = Played Time.zeroTime
- | preplay_raw debug type_enc lam_trans ctxt timeout
- (Prove (_, xs, _, t, subproofs, (fact_names, (meth :: _) :: _))) =
- let
- val goal =
- (case xs of
- [] => t
- | _ =>
- (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis
- (cf. "~~/src/Pure/Isar/obtain.ML") *)
- let
- (* FIXME: generate fresh name *)
- val thesis = Free ("thesis", HOLogic.boolT)
- val thesis_prop = thesis |> HOLogic.mk_Trueprop
- val frees = map Free xs
-
- (* !!x1..xn. t ==> thesis (xs = [x1, .., xn]) *)
- val inner_prop = fold_rev Logic.all frees (Logic.mk_implies (t, thesis_prop))
- in
- (* !!thesis. (!!x1..xn. t ==> thesis) ==> thesis *)
- Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
- end)
-
- val facts =
- resolve_fact_names ctxt fact_names
- |>> append (map (thm_of_proof ctxt) subproofs)
-
- val ctxt' = ctxt |> silence_reconstructors debug
-
- fun prove () =
- Goal.prove ctxt' [] [] goal (fn {context = ctxt, ...} =>
- HEADGOAL (tac_of_method meth type_enc lam_trans ctxt facts))
- handle ERROR msg => error ("Preplay error: " ^ msg)
-
- val play_outcome = take_time timeout prove ()
- in
- (if Config.get ctxt trace then preplay_trace ctxt facts goal play_outcome else ();
- play_outcome)
- end
-
-
-(*** proof preplay interface ***)
-
-type preplay_interface =
- {get_preplay_outcome: label -> play_outcome,
- set_preplay_outcome: label -> play_outcome -> unit,
- preplay_quietly: Time.time -> isar_step -> play_outcome,
- overall_preplay_outcome: isar_proof -> play_outcome}
-
-fun enrich_context_with_local_facts proof ctxt =
- let
- val thy = Proof_Context.theory_of ctxt
-
- fun enrich_with_fact l t =
- Proof_Context.put_thms false (string_of_label l, SOME [Skip_Proof.make_thm thy t])
-
- val enrich_with_assms = fold (uncurry enrich_with_fact)
-
- fun enrich_with_proof (Proof (_, assms, isar_steps)) =
- enrich_with_assms assms #> fold enrich_with_step isar_steps
- and enrich_with_step (Let _) = I
- | enrich_with_step (Prove (_, _, l, t, subproofs, _)) =
- enrich_with_fact l t #> fold enrich_with_proof subproofs
- in
- enrich_with_proof proof ctxt
- end
-
-fun merge_preplay_outcomes _ Play_Failed = Play_Failed
- | merge_preplay_outcomes Play_Failed _ = Play_Failed
- | merge_preplay_outcomes (Play_Timed_Out t1) (Play_Timed_Out t2) =
- Play_Timed_Out (Time.+ (t1, t2))
- | merge_preplay_outcomes (Played t1) (Play_Timed_Out t2) = Play_Timed_Out (Time.+ (t1, t2))
- | merge_preplay_outcomes (Play_Timed_Out t1) (Played t2) = Play_Timed_Out (Time.+ (t1, t2))
- | merge_preplay_outcomes (Played t1) (Played t2) = Played (Time.+ (t1, t2))
-
-(* Given a proof, produces an imperative preplay interface with a shared table mapping from labels
- to preplay results. The preplay results are caluclated lazyly and cached to avoid repeated
- calculation.
-
- Precondition: The proof must be labeled canonically; cf.
- "Slegehammer_Proof.relabel_proof_canonically". *)
-fun proof_preplay_interface debug ctxt type_enc lam_trans do_preplay preplay_timeout proof =
- if not do_preplay then
- (* the "dont_preplay" option pretends that everything works just fine *)
- {get_preplay_outcome = K (Played Time.zeroTime),
- set_preplay_outcome = K (K ()),
- preplay_quietly = K (K (Played Time.zeroTime)),
- overall_preplay_outcome = K (Played Time.zeroTime)} : preplay_interface
- else
- let
- val ctxt = enrich_context_with_local_facts proof ctxt
-
- fun preplay quietly timeout step =
- preplay_raw debug type_enc lam_trans ctxt timeout step
- handle exn =>
- if Exn.is_interrupt exn then
- reraise exn
- else
- (if not quietly andalso debug then
- warning ("Preplay failure:\n " ^ @{make_string} step ^ "\n " ^
- @{make_string} exn)
- else
- ();
- Play_Failed)
-
- (* preplay steps treating exceptions like timeouts *)
- fun preplay_quietly timeout = preplay true timeout
-
- val preplay_tab =
- let
- fun add_step_to_tab step tab =
- (case label_of_step step of
- NONE => tab
- | SOME l =>
- Canonical_Lbl_Tab.update_new
- (l, (fn () => preplay false preplay_timeout step) |> Lazy.lazy) tab)
- handle Canonical_Lbl_Tab.DUP _ => raise Fail "Sledgehammer_Preplay: preplay time table"
- in
- Canonical_Lbl_Tab.empty
- |> fold_isar_steps add_step_to_tab (steps_of_proof proof)
- |> Unsynchronized.ref
- end
-
- fun get_preplay_outcome l =
- Canonical_Lbl_Tab.lookup (!preplay_tab) l |> the |> Lazy.force
- handle Option.Option => raise Fail "Sledgehammer_Preplay: preplay time table"
-
- fun set_preplay_outcome l result =
- preplay_tab := Canonical_Lbl_Tab.update (l, Lazy.value result) (!preplay_tab)
-
- val result_of_step =
- try (label_of_step #> the #> get_preplay_outcome)
- #> the_default (Played Time.zeroTime)
-
- fun overall_preplay_outcome (Proof (_, _, steps)) =
- fold_isar_steps (merge_preplay_outcomes o result_of_step) steps (Played Time.zeroTime)
- in
- {get_preplay_outcome = get_preplay_outcome,
- set_preplay_outcome = set_preplay_outcome,
- preplay_quietly = preplay_quietly,
- overall_preplay_outcome = overall_preplay_outcome}
- end
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Fri Jan 31 10:23:32 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,262 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_print.ML
- Author: Jasmin Blanchette, TU Muenchen
- Author: Steffen Juilf Smolka, TU Muenchen
-
-Basic mapping from proof data structures to proof strings.
-*)
-
-signature SLEDGEHAMMER_PRINT =
-sig
- type isar_proof = Sledgehammer_Proof.isar_proof
- type reconstructor = Sledgehammer_Reconstructor.reconstructor
- type one_line_params = Sledgehammer_Reconstructor.one_line_params
-
- val string_of_reconstructor : reconstructor -> string
- val one_line_proof_text : int -> one_line_params -> string
- val string_of_proof : Proof.context -> string -> string -> int -> int -> isar_proof -> string
-end;
-
-structure Sledgehammer_Print : SLEDGEHAMMER_PRINT =
-struct
-
-open ATP_Util
-open ATP_Proof
-open ATP_Problem_Generate
-open ATP_Proof_Reconstruct
-open Sledgehammer_Util
-open Sledgehammer_Reconstructor
-open Sledgehammer_Proof
-open Sledgehammer_Annotate
-
-
-(** reconstructors **)
-
-fun string_of_reconstructor (Metis (type_enc, lam_trans)) = metis_call type_enc lam_trans
- | string_of_reconstructor SMT = smtN
-
-
-(** one-liner reconstructor proofs **)
-
-fun show_time NONE = ""
- | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
-
-(* FIXME: Various bugs, esp. with "unfolding"
-fun unusing_chained_facts _ 0 = ""
- | unusing_chained_facts used_chaineds num_chained =
- if length used_chaineds = num_chained then ""
- else if null used_chaineds then "(* using no facts *) "
- else "(* using only " ^ space_implode " " used_chaineds ^ " *) "
-*)
-
-fun apply_on_subgoal _ 1 = "by "
- | apply_on_subgoal 1 _ = "apply "
- | apply_on_subgoal i n =
- "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n
-
-fun using_labels [] = ""
- | using_labels ls = "using " ^ space_implode " " (map string_of_label ls) ^ " "
-
-fun command_call name [] =
- name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
- | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
-
-fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) =
- (* unusing_chained_facts used_chaineds num_chained ^ *)
- using_labels ls ^ apply_on_subgoal i n ^ command_call (string_of_reconstructor reconstr) ss
-
-fun try_command_line banner time command =
- banner ^ ": " ^
- Active.sendback_markup [Markup.padding_command] command ^
- show_time time ^ "."
-
-fun minimize_line _ [] = ""
- | minimize_line minimize_command ss =
- (case minimize_command ss of
- "" => ""
- | command => "\nTo minimize: " ^ Active.sendback_markup [Markup.padding_command] command ^ ".")
-
-fun split_used_facts facts =
- facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
- |> pairself (sort_distinct (string_ord o pairself fst))
-
-fun one_line_proof_text num_chained
- ((reconstr, play), banner, used_facts, minimize_command, subgoal, subgoal_count) =
- let
- val (chained, extra) = split_used_facts used_facts
- val (failed, ext_time) =
- (case play of
- Played time => (false, (SOME (false, time)))
- | Play_Timed_Out time => (false, SOME (true, time))
- | Play_Failed => (true, NONE)
- | Not_Played => (false, NONE))
- val try_line =
- ([], map fst extra)
- |> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained
- |> (if failed then
- enclose "One-line proof reconstruction failed: "
- ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
- \solve this.)"
- else
- try_command_line banner ext_time)
- in
- try_line ^ minimize_line minimize_command (map fst (extra @ chained))
- end
-
-
-(** detailed Isar proofs **)
-
-val indent_size = 2
-
-fun string_of_proof ctxt type_enc lam_trans i n proof =
- let
- (* Make sure only type constraints inserted by the type annotation code are printed. *)
- val ctxt =
- ctxt |> Config.put show_markup false
- |> Config.put Printer.show_type_emphasis false
- |> Config.put show_types false
- |> Config.put show_sorts false
- |> Config.put show_consts false
-
- val register_fixes = map Free #> fold Variable.auto_fixes
-
- fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt)
-
- fun of_indent ind = replicate_string (ind * indent_size) " "
- fun of_moreover ind = of_indent ind ^ "moreover\n"
- fun of_label l = if l = no_label then "" else string_of_label l ^ ": "
-
- fun of_obtain qs nr =
- (if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
- "ultimately "
- else if nr = 1 orelse member (op =) qs Then then
- "then "
- else
- "") ^ "obtain"
-
- fun of_show_have qs = if member (op =) qs Show then "show" else "have"
- fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence"
-
- fun of_have qs nr =
- if nr > 1 orelse (nr = 1 andalso member (op =) qs Then) then
- "ultimately " ^ of_show_have qs
- else if nr = 1 orelse member (op =) qs Then then
- of_thus_hence qs
- else
- of_show_have qs
-
- fun add_term term (s, ctxt) =
- (s ^ (term
- |> singleton (Syntax.uncheck_terms ctxt)
- |> annotate_types ctxt
- |> with_vanilla_print_mode (Syntax.unparse_term ctxt #> Pretty.string_of)
- |> simplify_spaces
- |> maybe_quote),
- ctxt |> Variable.auto_fixes term)
-
- fun by_method meth = "by " ^
- (case meth of
- Simp_Method => "simp"
- | Simp_Size_Method => "(simp add: size_ne_size_imp_ne)"
- | Auto_Method => "auto"
- | Fastforce_Method => "fastforce"
- | Force_Method => "force"
- | Arith_Method => "arith"
- | Blast_Method => "blast"
- | Meson_Method => "meson"
- | _ => raise Fail "Sledgehammer_Print: by_method")
-
- fun with_facts none _ [] [] = none
- | with_facts _ some ls ss = some (space_implode " " (map string_of_label ls @ ss))
-
- val using_facts = with_facts "" (enclose "using " " ")
-
- (* Local facts are always passed via "using", which affects "meson" and "metis". This is
- arguably stylistically superior, because it emphasises the structure of the proof. It is also
- more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence"
- and "thus" is introduced. See also "tac_of_method" in "Sledgehammer_Preplay". *)
- fun of_method ls ss Metis_Method =
- using_facts ls [] ^ reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 ([], ss)
- | of_method ls ss Meson_Method =
- using_facts ls [] ^ with_facts "by meson" (enclose "by (meson " ")") [] ss
- | of_method ls ss meth = using_facts ls ss ^ by_method meth
-
- fun of_byline ind (ls, ss) meth =
- let
- val ls = ls |> sort_distinct label_ord
- val ss = ss |> sort_distinct string_ord
- in
- "\n" ^ of_indent (ind + 1) ^ of_method ls ss meth
- end
-
- fun of_free (s, T) =
- maybe_quote s ^ " :: " ^
- maybe_quote (simplify_spaces (with_vanilla_print_mode (Syntax.string_of_typ ctxt) T))
-
- fun add_frees xs (s, ctxt) =
- (s ^ space_implode " and " (map of_free xs), ctxt |> register_fixes xs)
-
- fun add_fix _ [] = I
- | add_fix ind xs =
- add_suffix (of_indent ind ^ "fix ")
- #> add_frees xs
- #> add_suffix "\n"
-
- fun add_assm ind (l, t) =
- add_suffix (of_indent ind ^ "assume " ^ of_label l)
- #> add_term t
- #> add_suffix "\n"
-
- fun add_assms ind assms = fold (add_assm ind) assms
-
- fun add_step_post ind l t facts meth =
- add_suffix (of_label l)
- #> add_term t
- #> add_suffix (of_byline ind facts meth ^ "\n")
-
- fun of_subproof ind ctxt proof =
- let
- val ind = ind + 1
- val s = of_proof ind ctxt proof
- val prefix = "{ "
- val suffix = " }"
- in
- replicate_string (ind * indent_size - size prefix) " " ^ prefix ^
- String.extract (s, ind * indent_size, SOME (size s - ind * indent_size - 1)) ^
- suffix ^ "\n"
- end
- and of_subproofs _ _ _ [] = ""
- | of_subproofs ind ctxt qs subproofs =
- (if member (op =) qs Then then of_moreover ind else "") ^
- space_implode (of_moreover ind) (map (of_subproof ind ctxt) subproofs)
- and add_step_pre ind qs subproofs (s, ctxt) =
- (s ^ of_subproofs ind ctxt qs subproofs ^ of_indent ind, ctxt)
- and add_step ind (Let (t1, t2)) =
- add_suffix (of_indent ind ^ "let ")
- #> add_term t1
- #> add_suffix " = "
- #> add_term t2
- #> add_suffix "\n"
- | add_step ind (Prove (qs, xs, l, t, subproofs, (facts, (meth :: _) :: _))) =
- add_step_pre ind qs subproofs
- #> (case xs of
- [] => add_suffix (of_have qs (length subproofs) ^ " ")
- | _ =>
- add_suffix (of_obtain qs (length subproofs) ^ " ")
- #> add_frees xs
- #> add_suffix " where ")
- #> add_step_post ind l t facts meth
- and add_steps ind = fold (add_step ind)
- and of_proof ind ctxt (Proof (xs, assms, steps)) =
- ("", ctxt) |> add_fix ind xs |> add_assms ind assms |> add_steps ind steps |> fst
- in
- (* One-step Metis proofs are pointless; better use the one-liner directly. *)
- (case proof of
- Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *)
- | Proof ([], [], [Prove (_, [], _, _, [], (_, (Metis_Method :: _) :: _))]) => ""
- | _ =>
- (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
- of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
- of_indent 0 ^ (if n <> 1 then "next" else "qed"))
- end
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Fri Jan 31 10:23:32 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,157 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_proof.ML
- Author: Jasmin Blanchette, TU Muenchen
- Author: Steffen Juilf Smolka, TU Muenchen
-
-Basic data structures for representing and basic methods
-for dealing with Isar proof texts.
-*)
-
-signature SLEDGEHAMMER_PROOF =
-sig
- type label = string * int
- type facts = label list * string list (* local and global facts *)
-
- datatype isar_qualifier = Show | Then
-
- datatype isar_proof =
- Proof of (string * typ) list * (label * term) list * isar_step list
- and isar_step =
- Let of term * term |
- Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
- (facts * proof_method list list)
- and proof_method =
- Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
- Arith_Method | Blast_Method | Meson_Method
-
- val no_label : label
- val no_facts : facts
-
- val label_ord : label * label -> order
-
- val dummy_isar_step : isar_step
-
- val string_of_label : label -> string
-
- val fix_of_proof : isar_proof -> (string * typ) list
- val assms_of_proof : isar_proof -> (label * term) list
- val steps_of_proof : isar_proof -> isar_step list
-
- val label_of_step : isar_step -> label option
- val subproofs_of_step : isar_step -> isar_proof list option
- val byline_of_step : isar_step -> (facts * proof_method list list) option
-
- val fold_isar_step : (isar_step -> 'a -> 'a) -> isar_step -> 'a -> 'a
- val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
-
- val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
-
- val add_proof_steps : isar_step list -> int -> int
-
- (** canonical proof labels: 1, 2, 3, ... in postorder **)
- val canonical_label_ord : (label * label) -> order
- val relabel_proof_canonically : isar_proof -> isar_proof
-
- structure Canonical_Lbl_Tab : TABLE
-end;
-
-structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF =
-struct
-
-type label = string * int
-type facts = label list * string list (* local and global facts *)
-
-datatype isar_qualifier = Show | Then
-
-datatype isar_proof =
- Proof of (string * typ) list * (label * term) list * isar_step list
-and isar_step =
- Let of term * term |
- Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
- (facts * proof_method list list)
-and proof_method =
- Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
- Arith_Method | Blast_Method | Meson_Method
-
-val no_label = ("", ~1)
-val no_facts = ([],[])
-
-val label_ord = pairself swap #> prod_ord int_ord fast_string_ord
-
-val dummy_isar_step = Let (Term.dummy, Term.dummy)
-
-fun string_of_label (s, num) = s ^ string_of_int num
-
-fun fix_of_proof (Proof (fix, _, _)) = fix
-fun assms_of_proof (Proof (_, assms, _)) = assms
-fun steps_of_proof (Proof (_, _, steps)) = steps
-
-fun label_of_step (Prove (_, _, l, _, _, _)) = SOME l
- | label_of_step _ = NONE
-
-fun subproofs_of_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs
- | subproofs_of_step _ = NONE
-
-fun byline_of_step (Prove (_, _, _, _, _, byline)) = SOME byline
- | byline_of_step _ = NONE
-
-fun fold_isar_steps f = fold (fold_isar_step f)
-and fold_isar_step f step =
- fold (steps_of_proof #> fold_isar_steps f) (these (subproofs_of_step step)) #> f step
-
-fun map_isar_steps f =
- let
- fun do_proof (Proof (fix, assms, steps)) = Proof (fix, assms, map do_step steps)
- and do_step (step as Let _) = f step
- | do_step (Prove (qs, xs, l, t, subproofs, by)) =
- f (Prove (qs, xs, l, t, map do_proof subproofs, by))
- in
- do_proof
- end
-
-val add_proof_steps = fold_isar_steps (fn Prove _ => Integer.add 1 | _ => I)
-
-
-(** canonical proof labels: 1, 2, 3, ... in post traversal order **)
-
-fun canonical_label_ord (((_, i1), (_, i2)) : label * label) = int_ord (i1, i2)
-
-structure Canonical_Lbl_Tab = Table(
- type key = label
- val ord = canonical_label_ord)
-
-fun relabel_proof_canonically proof =
- let
- fun next_label l (next, subst) =
- let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end
-
- fun do_byline by (_, subst) = apfst (apfst (map (AList.lookup (op =) subst #> the))) by
- handle Option.Option =>
- raise Fail "Sledgehammer_Proof: relabel_proof_canonically"
-
- fun do_assm (l, t) state =
- let
- val (l, state) = next_label l state
- in ((l, t), state) end
-
- fun do_proof (Proof (fix, assms, steps)) state =
- let
- val (assms, state) = fold_map do_assm assms state
- val (steps, state) = fold_map do_step steps state
- in
- (Proof (fix, assms, steps), state)
- end
-
- and do_step (step as Let _) state = (step, state)
- | do_step (Prove (qs, fix, l, t, subproofs, by)) state=
- let
- val by = do_byline by state
- val (subproofs, state) = fold_map do_proof subproofs state
- val (l, state) = next_label l state
- in
- (Prove (qs, fix, l, t, subproofs, by), state)
- end
- in
- fst (do_proof proof (0, []))
- end
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Jan 31 10:23:32 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Jan 31 10:23:32 2014 +0100
@@ -127,8 +127,8 @@
open Sledgehammer_Util
open Sledgehammer_Fact
open Sledgehammer_Reconstructor
-open Sledgehammer_Print
-open Sledgehammer_Reconstruct
+open Sledgehammer_Isar_Print
+open Sledgehammer_Isar
(** The Sledgehammer **)
@@ -503,8 +503,8 @@
else remotify_prover_if_not_installed ctxt eN |> the_default name
end
-(* See the analogous logic in the function "maybe_minimize" in
- "sledgehammer_minimize.ML". *)
+(* FIXME: See the analogous logic in the function "maybe_minimize" in
+ "sledgehammer_prover_minimize.ML". *)
fun choose_minimize_command ctxt (params as {isar_proofs, ...}) minimize_command name preplay =
let
val maybe_isar_name = name |> isar_proofs = SOME true ? isar_proof_reconstructor ctxt
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Jan 31 10:23:32 2014 +0100
@@ -0,0 +1,322 @@
+(* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
+ Author: Philipp Meyer, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
+
+Minimization of fact list for Metis using external provers.
+*)
+
+signature SLEDGEHAMMER_PROVER_MINIMIZE =
+sig
+ type stature = ATP_Problem_Generate.stature
+ type reconstructor = Sledgehammer_Reconstructor.reconstructor
+ type play_outcome = Sledgehammer_Reconstructor.play_outcome
+ type mode = Sledgehammer_Prover.mode
+ type params = Sledgehammer_Prover.params
+ type prover = Sledgehammer_Prover.prover
+
+ val binary_min_facts : int Config.T
+ val auto_minimize_min_facts : int Config.T
+ val auto_minimize_max_time : real Config.T
+ val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int ->
+ Proof.state -> thm -> (reconstructor * play_outcome) Lazy.lazy option ->
+ ((string * stature) * thm list) list ->
+ ((string * stature) * thm list) list option
+ * ((reconstructor * play_outcome) Lazy.lazy * ((reconstructor * play_outcome) -> string)
+ * string)
+ val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover
+ val run_minimize : params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list ->
+ Proof.state -> unit
+end;
+
+structure Sledgehammer_Prover_Minimize : SLEDGEHAMMER_PROVER_MINIMIZE =
+struct
+
+open ATP_Util
+open ATP_Proof
+open ATP_Problem_Generate
+open ATP_Systems
+open Sledgehammer_Util
+open Sledgehammer_Fact
+open Sledgehammer_Reconstructor
+open Sledgehammer_Isar
+open Sledgehammer_Prover
+
+(* wrapper for calling external prover *)
+
+fun n_facts names =
+ let val n = length names in
+ string_of_int n ^ " fact" ^ plural_s n ^
+ (if n > 0 then
+ ": " ^ (names |> map fst |> sort string_ord |> space_implode " ")
+ else
+ "")
+ end
+
+fun print silent f = if silent then () else Output.urgent_message (f ())
+
+fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
+ type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress_isar, try0_isar,
+ preplay_timeout, ...} : params)
+ silent (prover : prover) timeout i n state goal facts =
+ let
+ val _ =
+ print silent (fn () =>
+ "Testing " ^ n_facts (map fst facts) ^
+ (if verbose then " (timeout: " ^ string_of_time timeout ^ ")" else "") ^ "...")
+ val facts = facts |> maps (fn (n, ths) => map (pair n) ths)
+ val params =
+ {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = true,
+ provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans,
+ uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE,
+ max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01),
+ max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
+ isar_proofs = isar_proofs, compress_isar = compress_isar, try0_isar = try0_isar,
+ slice = false, minimize = SOME false, timeout = timeout, preplay_timeout = preplay_timeout,
+ expect = ""}
+ val problem =
+ {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
+ factss = [("", facts)]}
+ val result as {outcome, used_facts, run_time, ...} =
+ prover params (K (K (K ""))) problem
+ in
+ print silent (fn () =>
+ (case outcome of
+ SOME failure => string_of_atp_failure failure
+ | NONE =>
+ "Found proof" ^
+ (if length used_facts = length facts then "" else " with " ^ n_facts used_facts) ^
+ " (" ^ string_of_time run_time ^ ")."));
+ result
+ end
+
+(* minimalization of facts *)
+
+(* Give the external prover 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 slack_msecs = 200
+
+fun new_timeout timeout run_time =
+ Int.min (Time.toMilliseconds timeout, Time.toMilliseconds run_time + slack_msecs)
+ |> Time.fromMilliseconds
+
+(* The linear algorithm usually outperforms the binary algorithm when over 60%
+ of the facts are actually needed. The binary algorithm is much more
+ appropriate for provers that cannot return the list of used facts and hence
+ returns all facts as used. Since we cannot know in advance how many facts are
+ actually needed, we heuristically set the threshold to 10 facts. *)
+val binary_min_facts =
+ Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts} (K 20)
+val auto_minimize_min_facts =
+ Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
+ (fn generic => Config.get_generic generic binary_min_facts)
+val auto_minimize_max_time =
+ Attrib.setup_config_real @{binding sledgehammer_auto_minimize_max_time} (K 5.0)
+
+fun linear_minimize test timeout result xs =
+ let
+ fun min _ [] p = p
+ | min timeout (x :: xs) (seen, result) =
+ (case test timeout (xs @ seen) of
+ result as {outcome = NONE, used_facts, run_time, ...} : prover_result =>
+ min (new_timeout timeout run_time) (filter_used_facts true used_facts xs)
+ (filter_used_facts false used_facts seen, result)
+ | _ => min timeout xs (x :: seen, result))
+ in
+ min timeout xs ([], result)
+ end
+
+fun binary_minimize test timeout result xs =
+ let
+ fun min depth (result as {run_time, ...} : prover_result) sup (xs as _ :: _ :: _) =
+ let
+ val (l0, r0) = chop (length xs div 2) xs
+(*
+ val _ = warning (replicate_string depth " " ^ "{ " ^ "sup: " ^ n_facts (map fst sup))
+ val _ = warning (replicate_string depth " " ^ " " ^ "xs: " ^ n_facts (map fst xs))
+ val _ = warning (replicate_string depth " " ^ " " ^ "l0: " ^ n_facts (map fst l0))
+ val _ = warning (replicate_string depth " " ^ " " ^ "r0: " ^ n_facts (map fst r0))
+*)
+ val depth = depth + 1
+ val timeout = new_timeout timeout run_time
+ in
+ (case test timeout (sup @ l0) of
+ result as {outcome = NONE, used_facts, ...} =>
+ min depth result (filter_used_facts true used_facts sup)
+ (filter_used_facts true used_facts l0)
+ | _ =>
+ (case test timeout (sup @ r0) of
+ result as {outcome = NONE, used_facts, ...} =>
+ min depth result (filter_used_facts true used_facts sup)
+ (filter_used_facts true used_facts r0)
+ | _ =>
+ let
+ val (sup_r0, (l, result)) = min depth result (sup @ r0) l0
+ val (sup, r0) = (sup, r0) |> pairself (filter_used_facts true (map fst sup_r0))
+ val (sup_l, (r, result)) = min depth result (sup @ l) r0
+ val sup = sup |> filter_used_facts true (map fst sup_l)
+ in (sup, (l @ r, result)) end))
+ end
+(*
+ |> tap (fn _ => warning (replicate_string depth " " ^ "}"))
+*)
+ | min _ result sup xs = (sup, (xs, result))
+ in
+ (case snd (min 0 result [] xs) of
+ ([x], result as {run_time, ...}) =>
+ (case test (new_timeout timeout run_time) [] of
+ result as {outcome = NONE, ...} => ([], result)
+ | _ => ([x], result))
+ | p => p)
+ end
+
+fun minimize_facts do_learn prover_name (params as {learn, timeout, ...}) silent i n state goal
+ preplay0 facts =
+ let
+ val ctxt = Proof.context_of state
+ val prover = get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
+ fun test timeout = test_facts params silent prover timeout i n state goal
+ val (chained, non_chained) = List.partition is_fact_chained facts
+ (* Push chained facts to the back, so that they are less likely to be
+ kicked out by the linear minimization algorithm. *)
+ val facts = non_chained @ chained
+ in
+ (print silent (fn () => "Sledgehammer minimizer: " ^ quote prover_name ^ ".");
+ (case test timeout facts of
+ result as {outcome = NONE, used_facts, run_time, ...} =>
+ let
+ val facts = filter_used_facts true used_facts facts
+ val min =
+ if length facts >= Config.get ctxt binary_min_facts then binary_minimize
+ else linear_minimize
+ val (min_facts, {preplay, message, message_tail, ...}) =
+ min test (new_timeout timeout run_time) result facts
+ in
+ print silent (fn () => cat_lines
+ ["Minimized to " ^ n_facts (map fst min_facts)] ^
+ (case min_facts |> filter is_fact_chained |> length of
+ 0 => ""
+ | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
+ (if learn then do_learn (maps snd min_facts) else ());
+ (SOME min_facts,
+ (if is_some preplay0 andalso length min_facts = length facts then the preplay0
+ else preplay,
+ message, message_tail))
+ end
+ | {outcome = SOME TimedOut, preplay, ...} =>
+ (NONE, (preplay, fn _ =>
+ "Timeout: You can increase the time limit using the \"timeout\" option (e.g., \
+ \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\").", ""))
+ | {preplay, message, ...} => (NONE, (preplay, prefix "Prover error: " o message, ""))))
+ handle ERROR msg => (NONE, (Lazy.value (plain_metis, Play_Failed), fn _ => "Error: " ^ msg, ""))
+ end
+
+fun adjust_reconstructor_params override_params
+ ({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, lam_trans,
+ uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters,
+ max_new_mono_instances, isar_proofs, compress_isar, try0_isar, slice, minimize, timeout,
+ preplay_timeout, expect} : params) =
+ let
+ fun lookup_override name default_value =
+ (case AList.lookup (op =) override_params name of
+ SOME [s] => SOME s
+ | _ => default_value)
+ (* Only those options that reconstructors are interested in are considered here. *)
+ val type_enc = lookup_override "type_enc" type_enc
+ val lam_trans = lookup_override "lam_trans" lam_trans
+ in
+ {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking,
+ provers = provers, type_enc = type_enc, strict = strict, lam_trans = lam_trans,
+ uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
+ max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
+ max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
+ compress_isar = compress_isar, try0_isar = try0_isar, slice = slice, minimize = minimize,
+ timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+ end
+
+fun maybe_minimize ctxt mode do_learn name
+ (params as {verbose, isar_proofs, minimize, ...})
+ ({state, goal, subgoal, subgoal_count, ...} : prover_problem)
+ (result as {outcome, used_facts, used_from, run_time, preplay, message,
+ message_tail} : prover_result) =
+ if is_some outcome orelse null used_facts then
+ result
+ else
+ let
+ val num_facts = length used_facts
+ val ((perhaps_minimize, (minimize_name, params)), preplay) =
+ if mode = Normal then
+ if num_facts >= Config.get ctxt auto_minimize_min_facts then
+ ((true, (name, params)), preplay)
+ else
+ let
+ fun can_min_fast_enough time =
+ 0.001
+ * Real.fromInt ((num_facts + 1) * Time.toMilliseconds time)
+ <= Config.get ctxt auto_minimize_max_time
+ fun prover_fast_enough () = can_min_fast_enough run_time
+ in
+ (case Lazy.force preplay of
+ (reconstr as Metis _, Played timeout) =>
+ if isar_proofs = SOME true then
+ (* Cheat: Assume the selected ATP is as fast as "metis" for the goal it proved
+ itself. *)
+ (can_min_fast_enough timeout, (isar_proof_reconstructor ctxt name, params))
+ else if can_min_fast_enough timeout then
+ (true, extract_reconstructor params reconstr
+ ||> (fn override_params =>
+ adjust_reconstructor_params override_params params))
+ else
+ (prover_fast_enough (), (name, params))
+ | (SMT, Played timeout) =>
+ (* Cheat: Assume the original prover is as fast as "smt" for the goal it proved
+ itself. *)
+ (can_min_fast_enough timeout, (name, params))
+ | _ => (prover_fast_enough (), (name, params)),
+ preplay)
+ end
+ else
+ ((false, (name, params)), preplay)
+ val minimize = minimize |> the_default perhaps_minimize
+ val (used_facts, (preplay, message, _)) =
+ if minimize then
+ minimize_facts do_learn minimize_name params
+ (not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal subgoal_count state
+ goal (SOME preplay) (filter_used_facts true used_facts (map (apsnd single) used_from))
+ |>> Option.map (map fst)
+ else
+ (SOME used_facts, (preplay, message, ""))
+ in
+ (case used_facts of
+ SOME used_facts =>
+ {outcome = NONE, used_facts = used_facts, used_from = used_from, run_time = run_time,
+ preplay = preplay, message = message, message_tail = message_tail}
+ | NONE => result)
+ end
+
+fun get_minimizing_prover ctxt mode do_learn name params minimize_command
+ problem =
+ get_prover ctxt mode name params minimize_command problem
+ |> maybe_minimize ctxt mode do_learn name params problem
+
+fun run_minimize (params as {provers, ...}) do_learn i refs state =
+ let
+ val ctxt = Proof.context_of state
+ val {goal, facts = chained_ths, ...} = Proof.goal state
+ val reserved = reserved_isar_keyword_table ()
+ val css = clasimpset_rule_table_of ctxt
+ val facts = refs |> maps (map (apsnd single) o fact_of_ref ctxt reserved chained_ths css)
+ in
+ (case subgoal_count state of
+ 0 => Output.urgent_message "No subgoal!"
+ | n => (case provers of
+ [] => error "No prover is set."
+ | prover :: _ =>
+ (kill_provers ();
+ minimize_facts do_learn prover params false i n state goal NONE facts
+ |> (fn (_, (preplay, message, message_tail)) =>
+ message (Lazy.force preplay) ^ message_tail
+ |> Output.urgent_message))))
+ end
+
+end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Jan 31 10:23:32 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,423 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
- Author: Jasmin Blanchette, TU Muenchen
- Author: Steffen Juilf Smolka, TU Muenchen
-
-Isar proof reconstruction from ATP proofs.
-*)
-
-signature SLEDGEHAMMER_RECONSTRUCT =
-sig
- type atp_step_name = ATP_Proof.atp_step_name
- type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
- type 'a atp_proof = 'a ATP_Proof.atp_proof
- type stature = ATP_Problem_Generate.stature
- type one_line_params = Sledgehammer_Reconstructor.one_line_params
-
- type isar_params =
- bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
-
- val proof_text : Proof.context -> bool -> bool option -> (unit -> isar_params) -> int ->
- one_line_params -> string
-end;
-
-structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT =
-struct
-
-open ATP_Util
-open ATP_Problem
-open ATP_Proof
-open ATP_Problem_Generate
-open ATP_Proof_Reconstruct
-open Sledgehammer_Util
-open Sledgehammer_Reconstructor
-open Sledgehammer_Proof
-open Sledgehammer_Annotate
-open Sledgehammer_Print
-open Sledgehammer_Preplay
-open Sledgehammer_Compress
-open Sledgehammer_Try0
-open Sledgehammer_Minimize_Isar
-
-structure String_Redirect = ATP_Proof_Redirect(
- type key = atp_step_name
- val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s')
- val string_of = fst)
-
-open String_Redirect
-
-val e_skolemize_rules = ["skolemize", "shift_quantors"]
-val spass_pirate_datatype_rule = "DT"
-val vampire_skolemisation_rule = "skolemisation"
-(* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *)
-val z3_skolemize_rule = "sk"
-val z3_th_lemma_rule = "th-lemma"
-
-val skolemize_rules =
- e_skolemize_rules @ [spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule]
-
-val is_skolemize_rule = member (op =) skolemize_rules
-val is_arith_rule = String.isPrefix z3_th_lemma_rule
-val is_datatype_rule = String.isPrefix spass_pirate_datatype_rule
-
-fun raw_label_of_num num = (num, 0)
-
-fun label_of_clause [(num, _)] = raw_label_of_num num
- | label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0)
-
-fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss)
- | add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names))
-
-(* No "real" literals means only type information (tfree_tcs, clsrel, or clsarity). *)
-fun is_only_type_information t = t aconv @{prop True}
-
-(* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in
- type information. *)
-fun add_line_pass1 (line as (name, role, t, rule, [])) lines =
- (* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or
- definitions. *)
- if role = Lemma orelse role = Conjecture orelse role = Negated_Conjecture orelse
- role = Hypothesis orelse is_arith_rule rule then
- line :: lines
- else if role = Axiom then
- (* Facts are not proof lines. *)
- lines |> is_only_type_information t ? map (replace_dependencies_in_line (name, []))
- else
- map (replace_dependencies_in_line (name, [])) lines
- | add_line_pass1 line lines = line :: lines
-
-fun add_lines_pass2 res [] = rev res
- | add_lines_pass2 res ((name, role, t, rule, deps) :: lines) =
- let
- val is_last_line = null lines
-
- fun looks_interesting () =
- not (is_only_type_information t) andalso null (Term.add_tvars t [])
- andalso length deps >= 2 andalso not (can the_single lines)
-
- fun is_skolemizing_line (_, _, _, rule', deps') =
- is_skolemize_rule rule' andalso member (op =) deps' name
- fun is_before_skolemize_rule () = exists is_skolemizing_line lines
- in
- if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse
- is_datatype_rule rule orelse is_last_line orelse looks_interesting () orelse
- is_before_skolemize_rule () then
- add_lines_pass2 ((name, role, t, rule, deps) :: res) lines
- else
- add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines)
- end
-
-val add_labels_of_proof =
- steps_of_proof
- #> fold_isar_steps (byline_of_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I))
-
-fun kill_useless_labels_in_proof proof =
- let
- val used_ls = add_labels_of_proof proof []
-
- fun kill_label l = if member (op =) used_ls l then l else no_label
- fun kill_assms assms = map (apfst kill_label) assms
-
- fun kill_step (Prove (qs, xs, l, t, subproofs, by)) =
- Prove (qs, xs, kill_label l, t, map kill_proof subproofs, by)
- | kill_step step = step
- and kill_proof (Proof (fix, assms, steps)) =
- Proof (fix, kill_assms assms, map kill_step steps)
- in
- kill_proof proof
- end
-
-val assume_prefix = "a"
-val have_prefix = "f"
-
-val relabel_proof =
- let
- fun fresh_label depth prefix (accum as (l, subst, next)) =
- if l = no_label then
- accum
- else
- let val l' = (replicate_string (depth + 1) prefix, next) in
- (l', (l, l') :: subst, next + 1)
- end
-
- fun relabel_facts subst = apfst (maps (the_list o AList.lookup (op =) subst))
-
- fun relabel_assm depth (l, t) (subst, next) =
- let val (l, subst, next) = (l, subst, next) |> fresh_label depth assume_prefix in
- ((l, t), (subst, next))
- end
-
- fun relabel_assms subst depth assms = fold_map (relabel_assm depth) assms (subst, 1) ||> fst
-
- fun relabel_steps _ _ _ [] = []
- | relabel_steps subst depth next (Prove (qs, xs, l, t, sub, by) :: steps) =
- let
- val (l, subst, next) = (l, subst, next) |> fresh_label depth have_prefix
- val sub = relabel_proofs subst depth sub
- val by = apfst (relabel_facts subst) by
- in
- Prove (qs, xs, l, t, sub, by) :: relabel_steps subst depth next steps
- end
- | relabel_steps subst depth next (step :: steps) =
- step :: relabel_steps subst depth next steps
- and relabel_proof subst depth (Proof (fix, assms, steps)) =
- let val (assms, subst) = relabel_assms subst depth assms in
- Proof (fix, assms, relabel_steps subst depth 1 steps)
- end
- and relabel_proofs subst depth = map (relabel_proof subst (depth + 1))
- in
- relabel_proof [] 0
- end
-
-val chain_direct_proof =
- let
- fun chain_qs_lfs NONE lfs = ([], lfs)
- | chain_qs_lfs (SOME l0) lfs =
- if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs)
- fun chain_step lbl (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), methss))) =
- let val (qs', lfs) = chain_qs_lfs lbl lfs in
- Prove (qs' @ qs, xs, l, t, chain_proofs subproofs, ((lfs, gfs), methss))
- end
- | chain_step _ step = step
- and chain_steps _ [] = []
- | chain_steps (prev as SOME _) (i :: is) =
- chain_step prev i :: chain_steps (label_of_step i) is
- | chain_steps _ (i :: is) = i :: chain_steps (label_of_step i) is
- and chain_proof (Proof (fix, assms, steps)) =
- Proof (fix, assms, chain_steps (try (List.last #> fst) assms) steps)
- and chain_proofs proofs = map (chain_proof) proofs
- in
- chain_proof
- end
-
-type isar_params =
- bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm
-
-val arith_methodss =
- [[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
- Metis_Method], [Meson_Method]]
-val datatype_methodss = [[Simp_Size_Method, Simp_Method]]
-val metislike_methodss =
- [[Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
- Force_Method], [Meson_Method]]
-val rewrite_methodss =
- [[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method], [Meson_Method]]
-val skolem_methodss = [[Metis_Method, Blast_Method], [Meson_Method]]
-
-fun isar_proof_text ctxt debug isar_proofs isar_params
- (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
- let
- fun isar_proof_of () =
- let
- val SOME (verbose, metis_type_enc, metis_lam_trans, preplay_timeout, compress_isar,
- try0_isar, atp_proof, goal) = try isar_params ()
-
- val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
- val (_, ctxt) =
- params
- |> map (fn (s, T) => (Binding.name s, SOME T, NoSyn))
- |> (fn fixes => ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes)
-
- val do_preplay = preplay_timeout <> Time.zeroTime
- val try0_isar = try0_isar andalso do_preplay
-
- val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
- fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
-
- fun get_role keep_role ((num, _), role, t, rule, _) =
- if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE
-
- val atp_proof =
- atp_proof
- |> rpair [] |-> fold_rev add_line_pass1
- |> add_lines_pass2 []
-
- val conjs =
- map_filter (fn (name, role, _, _, _) =>
- if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE)
- atp_proof
- val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof
- val lems =
- map_filter (get_role (curry (op =) Lemma)) atp_proof
- |> map (fn ((l, t), rule) =>
- let
- val (skos, methss) =
- if is_skolemize_rule rule then (skolems_of t, skolem_methodss)
- else if is_arith_rule rule then ([], arith_methodss)
- else ([], rewrite_methodss)
- in
- Prove ([], skos, l, t, [], (([], []), methss))
- end)
-
- val bot = atp_proof |> List.last |> #1
-
- val refute_graph =
- atp_proof
- |> map (fn (name, _, _, _, from) => (from, name))
- |> make_refute_graph bot
- |> fold (Atom_Graph.default_node o rpair ()) conjs
-
- val axioms = axioms_of_refute_graph refute_graph conjs
-
- val tainted = tainted_atoms_of_refute_graph refute_graph conjs
- val is_clause_tainted = exists (member (op =) tainted)
- val steps =
- Symtab.empty
- |> fold (fn (name as (s, _), role, t, rule, _) =>
- Symtab.update_new (s, (rule, t
- |> (if is_clause_tainted [name] then
- HOLogic.dest_Trueprop
- #> role <> Conjecture ? s_not
- #> fold exists_of (map Var (Term.add_vars t []))
- #> HOLogic.mk_Trueprop
- else
- I))))
- atp_proof
-
- val rule_of_clause_id = fst o the o Symtab.lookup steps o fst
-
- fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> close_form
- | prop_of_clause names =
- let
- val lits = map (HOLogic.dest_Trueprop o snd)
- (map_filter (Symtab.lookup steps o fst) names)
- in
- (case List.partition (can HOLogic.dest_not) lits of
- (negs as _ :: _, pos as _ :: _) =>
- s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos)
- | _ => fold (curry s_disj) lits @{term False})
- end
- |> HOLogic.mk_Trueprop |> close_form
-
- fun maybe_show outer c = (outer andalso eq_set (op =) (c, conjs)) ? cons Show
-
- fun isar_steps outer predecessor accum [] =
- accum
- |> (if tainted = [] then
- cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
- ((the_list predecessor, []), metislike_methodss)))
- else
- I)
- |> rev
- | isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) =
- let
- val l = label_of_clause c
- val t = prop_of_clause c
- val rule = rule_of_clause_id id
- val skolem = is_skolemize_rule rule
-
- fun prove sub by = Prove (maybe_show outer c [], [], l, t, sub, by)
- fun do_rest l step = isar_steps outer (SOME l) (step :: accum) infs
-
- val deps = fold add_fact_of_dependencies gamma no_facts
- val methss =
- if is_arith_rule rule then arith_methodss
- else if is_datatype_rule rule then datatype_methodss
- else metislike_methodss
- val by = (deps, methss)
- in
- if is_clause_tainted c then
- (case gamma of
- [g] =>
- if skolem andalso is_clause_tainted g then
- let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in
- isar_steps outer (SOME l) [prove [subproof] (no_facts, skolem_methodss)] infs
- end
- else
- do_rest l (prove [] by)
- | _ => do_rest l (prove [] by))
- else
- do_rest l (if skolem then Prove ([], skolems_of t, l, t, [], by) else prove [] by)
- end
- | isar_steps outer predecessor accum (Cases cases :: infs) =
- let
- fun isar_case (c, subinfs) =
- isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs
- val c = succedent_of_cases cases
- val l = label_of_clause c
- val t = prop_of_clause c
- val step =
- Prove (maybe_show outer c [], [], l, t,
- map isar_case (filter_out (null o snd) cases),
- ((the_list predecessor, []), metislike_methodss))
- in
- isar_steps outer (SOME l) (step :: accum) infs
- end
- and isar_proof outer fix assms lems infs =
- Proof (fix, assms, lems @ isar_steps outer NONE [] infs)
-
- val (preplay_interface as {overall_preplay_outcome, ...}, isar_proof) =
- refute_graph
-(*
- |> tap (tracing o prefix "Refute graph: " o string_of_refute_graph)
-*)
- |> redirect_graph axioms tainted bot
-(*
- |> tap (tracing o prefix "Direct proof: " o string_of_direct_proof)
-*)
- |> isar_proof true params assms lems
- |> postprocess_remove_unreferenced_steps I
- |> relabel_proof_canonically
- |> `(proof_preplay_interface debug ctxt metis_type_enc metis_lam_trans do_preplay
- preplay_timeout)
-
- val (play_outcome, isar_proof) =
- isar_proof
- |> compress_proof (if isar_proofs = SOME true then compress_isar else 1000.0)
- preplay_interface
- |> try0_isar ? try0 preplay_timeout preplay_interface
- |> postprocess_remove_unreferenced_steps (try0_isar ? min_deps_of_step preplay_interface)
- |> `overall_preplay_outcome
- ||> (chain_direct_proof #> kill_useless_labels_in_proof #> relabel_proof)
-
- val isar_text =
- string_of_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count isar_proof
- in
- (case isar_text of
- "" =>
- if isar_proofs = SOME true then
- "\nNo structured proof available (proof too simple)."
- else
- ""
- | _ =>
- let
- val msg =
- (if verbose then
- let val num_steps = add_proof_steps (steps_of_proof isar_proof) 0 in
- [string_of_int num_steps ^ " step" ^ plural_s num_steps]
- end
- else
- []) @
- (if do_preplay then [string_of_play_outcome play_outcome] else [])
- in
- "\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^
- Active.sendback_markup [Markup.padding_command] isar_text
- end)
- end
-
- val one_line_proof = one_line_proof_text 0 one_line_params
- val isar_proof =
- if debug then
- isar_proof_of ()
- else
- (case try isar_proof_of () of
- SOME s => s
- | NONE =>
- if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "")
- in one_line_proof ^ isar_proof end
-
-fun isar_proof_would_be_a_good_idea (reconstr, play) =
- (case play of
- Played _ => reconstr = SMT
- | Play_Timed_Out _ => true
- | Play_Failed => true
- | Not_Played => false)
-
-fun proof_text ctxt debug isar_proofs isar_params num_chained
- (one_line_params as (preplay, _, _, _, _, _)) =
- (if isar_proofs = SOME true orelse
- (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
- isar_proof_text ctxt debug isar_proofs isar_params
- else
- one_line_proof_text num_chained) one_line_params
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Fri Jan 31 10:23:32 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,302 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_run.ML
- Author: Fabian Immler, TU Muenchen
- Author: Makarius
- Author: Jasmin Blanchette, TU Muenchen
-
-Sledgehammer's heart.
-*)
-
-signature SLEDGEHAMMER_RUN =
-sig
- type fact = Sledgehammer_Fact.fact
- type fact_override = Sledgehammer_Fact.fact_override
- type minimize_command = Sledgehammer_Reconstructor.minimize_command
- type mode = Sledgehammer_Prover.mode
- type params = Sledgehammer_Prover.params
-
- val someN : string
- val noneN : string
- val timeoutN : string
- val unknownN : string
- val string_of_factss : (string * fact list) list -> string
- val run_sledgehammer : params -> mode -> (string -> unit) option -> int -> fact_override ->
- ((string * string list) list -> string -> minimize_command) -> Proof.state ->
- bool * (string * Proof.state)
-end;
-
-structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
-struct
-
-open ATP_Util
-open ATP_Problem_Generate
-open ATP_Proof
-open ATP_Proof_Reconstruct
-open Sledgehammer_Util
-open Sledgehammer_Fact
-open Sledgehammer_Prover
-open Sledgehammer_Minimize
-open Sledgehammer_MaSh
-
-val someN = "some"
-val noneN = "none"
-val timeoutN = "timeout"
-val unknownN = "unknown"
-
-val ordered_outcome_codes = [someN, unknownN, timeoutN, noneN]
-
-fun max_outcome_code codes =
- NONE
- |> fold (fn candidate =>
- fn accum as SOME _ => accum
- | NONE => if member (op =) codes candidate then SOME candidate
- else NONE)
- ordered_outcome_codes
- |> the_default unknownN
-
-fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i
- n goal =
- (quote name,
- (if verbose then
- " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
- else
- "") ^
- " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^
- (if blocking then "."
- else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
-
-fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, expect, ...}) mode
- output_result minimize_command only learn
- {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _} name =
- let
- val ctxt = Proof.context_of state
-
- val hard_timeout = time_mult 3.0 timeout
- val _ = spying spy (fn () => (state, subgoal, name, "Launched"));
- val birth_time = Time.now ()
- val death_time = Time.+ (birth_time, hard_timeout)
- val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name)
- val num_facts = length facts |> not only ? Integer.min max_facts
-
- fun desc () = prover_description ctxt params name num_facts subgoal subgoal_count goal
-
- val problem =
- {comment = comment, state = state, goal = goal, subgoal = subgoal,
- subgoal_count = subgoal_count,
- factss = factss
- |> map (apsnd ((not (is_ho_atp ctxt name)
- ? filter_out (fn ((_, (_, Induction)), _) => true
- | _ => false))
- #> take num_facts))}
-
- fun print_used_facts used_facts used_from =
- tag_list 1 used_from
- |> map (fn (j, fact) => fact |> apsnd (K j))
- |> filter_used_facts false used_facts
- |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
- |> commas
- |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
- " proof (of " ^ string_of_int (length facts) ^ "): ") "."
- |> Output.urgent_message
-
- fun spying_str_of_res ({outcome = NONE, used_facts, used_from, ...} : prover_result) =
- let
- val num_used_facts = length used_facts
-
- fun find_indices facts =
- tag_list 1 facts
- |> map (fn (j, fact) => fact |> apsnd (K j))
- |> filter_used_facts false used_facts
- |> distinct (eq_fst (op =))
- |> map (prefix "@" o string_of_int o snd)
-
- fun filter_info (fact_filter, facts) =
- let
- val indices = find_indices facts
- (* "Int.max" is there for robustness -- it shouldn't be necessary *)
- val unknowns = replicate (Int.max (0, num_used_facts - length indices)) "?"
- in
- (commas (indices @ unknowns), fact_filter)
- end
-
- val filter_infos =
- map filter_info (("actual", used_from) :: factss)
- |> AList.group (op =)
- |> map (fn (indices, fact_filters) => commas fact_filters ^ ": " ^ indices)
- in
- "Success: Found proof with " ^ string_of_int num_used_facts ^
- " of " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts ^
- (if num_used_facts = 0 then "" else ": " ^ commas filter_infos)
- end
- | spying_str_of_res {outcome = SOME failure, ...} =
- "Failure: " ^ string_of_atp_failure failure
-
- fun really_go () =
- problem
- |> get_minimizing_prover ctxt mode learn name params minimize_command
- |> verbose
- ? tap (fn {outcome = NONE, used_facts as _ :: _, used_from, ...} =>
- print_used_facts used_facts used_from
- | _ => ())
- |> spy
- ? tap (fn res => spying spy (fn () => (state, subgoal, name, spying_str_of_res res)))
- |> (fn {outcome, preplay, message, message_tail, ...} =>
- (if outcome = SOME ATP_Proof.TimedOut then timeoutN
- else if is_some outcome then noneN
- else someN, fn () => message (Lazy.force preplay) ^ message_tail))
-
- fun go () =
- let
- val (outcome_code, message) =
- if debug then
- really_go ()
- else
- (really_go ()
- handle ERROR msg => (unknownN, fn () => "Error: " ^ msg ^ "\n")
- | exn =>
- if Exn.is_interrupt exn then
- reraise exn
- else
- (unknownN, fn () => "Internal error:\n" ^
- ML_Compiler.exn_message exn ^ "\n"))
- val _ =
- (* The "expect" argument is deliberately ignored if the prover is
- missing so that the "Metis_Examples" can be processed on any
- machine. *)
- if expect = "" orelse outcome_code = expect orelse
- not (is_prover_installed ctxt name) then
- ()
- else if blocking then
- error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
- else
- warning ("Unexpected outcome: " ^ quote outcome_code ^ ".");
- in (outcome_code, message) end
- in
- if mode = Auto_Try then
- let val (outcome_code, message) = TimeLimit.timeLimit timeout go () in
- (outcome_code,
- state
- |> outcome_code = someN
- ? Proof.goal_message (fn () =>
- Pretty.mark Markup.information (Pretty.str (message ()))))
- end
- else if blocking then
- let
- val (outcome_code, message) = TimeLimit.timeLimit hard_timeout go ()
- val outcome =
- if outcome_code = someN orelse mode = Normal then
- quote name ^ ": " ^ message ()
- else ""
- val _ =
- if outcome <> "" andalso is_some output_result then
- the output_result outcome
- else
- outcome
- |> Async_Manager.break_into_chunks
- |> List.app Output.urgent_message
- in (outcome_code, state) end
- else
- (Async_Manager.thread SledgehammerN birth_time death_time (desc ())
- ((fn (outcome_code, message) =>
- (verbose orelse outcome_code = someN,
- message ())) o go);
- (unknownN, state))
- end
-
-val auto_try_max_facts_divisor = 2 (* FUDGE *)
-
-fun string_of_facts facts =
- "Including " ^ string_of_int (length facts) ^
- " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
- (facts |> map (fst o fst) |> space_implode " ") ^ "."
-
-fun string_of_factss factss =
- if forall (null o snd) factss then
- "Found no relevant facts."
- else case factss of
- [(_, facts)] => string_of_facts facts
- | _ =>
- factss
- |> map (fn (filter, facts) => quote filter ^ ": " ^ string_of_facts facts)
- |> space_implode "\n\n"
-
-fun run_sledgehammer (params as {debug, verbose, spy, blocking, provers, max_facts, ...}) mode
- output_result i (fact_override as {only, ...}) minimize_command state =
- if null provers then
- error "No prover is set."
- else case subgoal_count state of
- 0 =>
- ((if blocking then error else Output.urgent_message) "No subgoal!"; (false, (noneN, state)))
- | n =>
- let
- val _ = Proof.assert_backward state
- val print =
- if mode = Normal andalso is_none output_result then Output.urgent_message else K ()
- val state = state |> Proof.map_context (Config.put SMT_Config.verbose debug)
- val ctxt = Proof.context_of state
- val {facts = chained, goal, ...} = Proof.goal state
- val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
- val ho_atp = exists (is_ho_atp ctxt) provers
- val reserved = reserved_isar_keyword_table ()
- val css = clasimpset_rule_table_of ctxt
- val all_facts =
- nearly_all_facts ctxt ho_atp fact_override reserved css chained hyp_ts
- concl_t
- val _ = () |> not blocking ? kill_provers
- val _ = case find_first (not o is_prover_supported ctxt) provers of
- SOME name => error ("No such prover: " ^ name ^ ".")
- | NONE => ()
- val _ = print "Sledgehammering..."
- val _ = spying spy (fn () => (state, i, "***", "Starting " ^ @{make_string} mode ^ " mode"))
-
- val spying_str_of_factss =
- commas o map (fn (filter, facts) => filter ^ ": " ^ string_of_int (length facts))
-
- fun get_factss provers =
- let
- val max_max_facts =
- case max_facts of
- SOME n => n
- | NONE =>
- 0 |> fold (Integer.max o default_max_facts_of_prover ctxt) provers
- |> mode = Auto_Try ? (fn n => n div auto_try_max_facts_divisor)
- val _ = spying spy (fn () => (state, i, "All",
- "Filtering " ^ string_of_int (length all_facts) ^ " facts"));
- in
- all_facts
- |> relevant_facts ctxt params (hd provers) max_max_facts fact_override hyp_ts concl_t
- |> tap (fn factss => if verbose then print (string_of_factss factss) else ())
- |> spy ? tap (fn factss => spying spy (fn () =>
- (state, i, "All", "Selected facts: " ^ spying_str_of_factss factss)))
- end
-
- fun launch_provers state =
- let
- val factss = get_factss provers
- val problem =
- {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
- factss = factss}
- val learn = mash_learn_proof ctxt params (prop_of goal) all_facts
- val launch = launch_prover params mode output_result minimize_command only learn
- in
- if mode = Auto_Try then
- (unknownN, state)
- |> fold (fn prover => fn accum as (outcome_code, _) =>
- if outcome_code = someN then accum
- else launch problem prover)
- provers
- else
- provers
- |> (if blocking then Par_List.map else map) (launch problem #> fst)
- |> max_outcome_code |> rpair state
- end
-
- fun maybe f (accum as (outcome_code, _)) =
- accum |> (mode = Normal orelse outcome_code <> someN) ? f
- in
- (if blocking then launch_provers state
- else (Future.fork (tap (fn () => launch_provers state)); (unknownN, state)))
- handle TimeLimit.TimeOut => (print "Sledgehammer ran out of time."; (unknownN, state))
- end
- |> `(fn (outcome_code, _) => outcome_code = someN)
-
-end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Fri Jan 31 10:23:32 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-(* Title: HOL/Tools/Sledgehammer/sledgehammer_try0.ML
- Author: Steffen Juilf Smolka, TU Muenchen
- Author: Jasmin Blanchette, TU Muenchen
-
-Try replacing calls to metis with calls to other proof methods to speed up proofs, eliminate
-dependencies, and repair broken proof steps.
-*)
-
-signature SLEDGEHAMMER_TRY0 =
-sig
- type isar_proof = Sledgehammer_Proof.isar_proof
- type preplay_interface = Sledgehammer_Preplay.preplay_interface
-
- val try0 : Time.time -> preplay_interface -> isar_proof -> isar_proof
-end;
-
-structure Sledgehammer_Try0 : SLEDGEHAMMER_TRY0 =
-struct
-
-open Sledgehammer_Util
-open Sledgehammer_Reconstructor
-open Sledgehammer_Proof
-open Sledgehammer_Preplay
-
-fun variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, methss))) =
- map (fn meth => Prove (qs, xs, l, t, subproofs, (facts, [[meth]]))) (tl (flat methss))
- | variants_of_step _ = raise Fail "Sledgehammer_Try0: variants_of_step"
-
-val slack = seconds 0.05
-
-fun try0_step _ _ (step as Let _) = step
- | try0_step preplay_timeout
- ({get_preplay_outcome, set_preplay_outcome, preplay_quietly, ...} : preplay_interface)
- (step as Prove (_, _, l, _, _, _)) =
- let
- val timeout =
- (case get_preplay_outcome l of
- Played time => Time.+ (time, slack)
- | _ => preplay_timeout)
-
- fun try_variant variant =
- (case preplay_quietly timeout variant of
- result as Played _ => SOME (variant, result)
- | _ => NONE)
- in
- (case Par_List.get_some try_variant (variants_of_step step) of
- SOME (step', result) => (set_preplay_outcome l result; step')
- | NONE => step)
- end
-
-val try0 = map_isar_steps oo try0_step
-
-end;