# HG changeset patch # User blanchet # Date 1391160212 -3600 # Node ID 824c48a539c9db3209ccfd888c2cb40b5f0f445d # Parent 1ee776da8da752ab25af9f44b509b9e696592cb6 renamed many Sledgehammer ML files to clarify structure diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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)) = diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Sledgehammer.thy --- 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 diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- /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; diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML --- 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; diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- 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" diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML --- 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; diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- /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; diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer_isar_annotate.ML --- /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; diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML --- /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; diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML --- /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; diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- /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 ";" "\" "\" assms) (* Syntax.pretty_term!? *) + val concl = concl |> Syntax.pretty_term ctxt + val trace_list = [] + |> cons concl + |> nr_of_assms > 0 ? cons (Pretty.str "\") + |> 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; diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer_isar_print.ML --- /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; diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML --- /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; diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer_isar_try0.ML --- /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; diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- 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 = diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- 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; diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer_minimize_isar.ML --- 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; diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- 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 ";" "\" "\" assms) (* Syntax.pretty_term!? *) - val concl = concl |> Syntax.pretty_term ctxt - val trace_list = [] - |> cons concl - |> nr_of_assms > 0 ? cons (Pretty.str "\") - |> 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; diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer_print.ML --- 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; diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML --- 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; diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML --- 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 diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- /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; diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- 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; diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- 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; diff -r 1ee776da8da7 -r 824c48a539c9 src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML --- 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;