# HG changeset patch # User wenzelm # Date 1357161376 -3600 # Node ID 97f951edca46fa81d12722957e68933dd0a6c132 # Parent adbbe04b7c752fa3b92ca99a7b8bc11a564a58f4# Parent 20beafe66748568a5207ac0919c467ff75c90e36 merged diff -r 20beafe66748 -r 97f951edca46 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Jan 02 21:55:57 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Jan 02 22:16:16 2013 +0100 @@ -77,8 +77,13 @@ |> lam_trans <> metis_default_lam_trans ? cons lam_trans in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end -fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t -fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t +fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s + | term_name' t = "" + +fun lambda' v = Term.lambda_name (term_name' v, v) + +fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda' v t +fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda' v t fun make_tfree ctxt w = let val ww = "'" ^ w in @@ -123,10 +128,10 @@ | add_type_constraint false (cl, TVar (ix, _)) = add_var (ix, cl) | add_type_constraint _ _ = I -fun repair_variable_name f s = +fun repair_var_name s = let fun subscript_name s n = s ^ nat_subscript n - val s = String.map f s + val s = String.map Char.toLower s in case space_explode "_" s of [_] => (case take_suffix Char.isDigit (String.explode s) of @@ -235,6 +240,8 @@ end | NONE => (* a free or schematic variable *) let + fun fresh_up s = + [(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst val term_ts = map (do_term [] NONE) us val ts = term_ts @ extra_ts val T = @@ -248,8 +255,10 @@ case unprefix_and_unascii schematic_var_prefix s of SOME s => Var ((s, var_index), T) | NONE => - Var ((s |> textual ? repair_variable_name Char.toLower, - var_index), T) + if textual andalso not (is_tptp_variable s) then + Free (s |> textual ? (repair_var_name #> fresh_up), T) + else + Var ((s |> textual ? repair_var_name, var_index), T) in list_comb (t, ts) end in do_term [] end @@ -294,7 +303,7 @@ (* FIXME: TFF *) #>> quantify_over_var (case q of AForall => forall_of | AExists => exists_of) - (s |> textual ? repair_variable_name Char.toLower) + (s |> textual ? repair_var_name) | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not | AConn (c, [phi1, phi2]) => do_formula (pos |> c = AImplies ? not) phi1 diff -r 20beafe66748 -r 97f951edca46 src/HOL/Tools/ATP/atp_proof_redirect.ML --- a/src/HOL/Tools/ATP/atp_proof_redirect.ML Wed Jan 02 21:55:57 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_redirect.ML Wed Jan 02 22:16:16 2013 +0100 @@ -41,7 +41,6 @@ val direct_graph : direct_sequent list -> direct_graph val redirect_graph : atom list -> atom list -> ref_graph -> direct_proof val succedent_of_cases : (clause * direct_inference list) list -> clause - val chain_direct_proof : direct_proof -> direct_proof val string_of_direct_proof : direct_proof -> string end; @@ -186,19 +185,6 @@ in s_cases cases @ redirect (succedent_of_cases cases) proved seqs end in redirect [] axioms seqs end -val chain_direct_proof = - let - fun chain_inf cl0 (seq as Have (cs, c)) = - seq - | chain_inf _ (Cases cases) = Cases (map chain_case cases) - and chain_case (c, is) = (c, chain_proof (SOME c) is) - and chain_proof _ [] = [] - | chain_proof (SOME prev) (i :: is) = - chain_inf prev i :: chain_proof (SOME (succedent_of_inference i)) is - | chain_proof _ (i :: is) = - i :: chain_proof (SOME (succedent_of_inference i)) is - in chain_proof NONE end - fun indent 0 = "" | indent n = " " ^ indent (n - 1) diff -r 20beafe66748 -r 97f951edca46 src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed Jan 02 21:55:57 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Wed Jan 02 22:16:16 2013 +0100 @@ -17,6 +17,8 @@ Fix of (string * typ) list | Let of term * term | Assume of label * term | + Obtain of + isar_qualifier list * (string * typ) list * label * term * byline | Prove of isar_qualifier list * label * term * byline and byline = By_Metis of facts | @@ -27,7 +29,7 @@ val metis_steps_total : isar_step list -> int end -structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF = +structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF = struct type label = string * int @@ -39,6 +41,7 @@ Fix of (string * typ) list | Let of term * term | Assume of label * term | + Obtain of isar_qualifier list * (string * typ) list * label * term * byline | Prove of isar_qualifier list * label * term * byline and byline = By_Metis of facts | @@ -46,12 +49,14 @@ fun string_for_label (s, num) = s ^ string_of_int num -val inc = curry op+ -fun metis_steps_top_level proof = fold (fn Prove _ => inc 1 | _ => I) proof 0 -fun metis_steps_total proof = - fold (fn Prove (_,_,_, By_Metis _) => inc 1 - | Prove (_,_,_, Case_Split (cases, _)) => - inc (fold (inc o metis_steps_total) cases 1) +fun metis_steps_top_level proof = + fold (fn Obtain _ => Integer.add 1 | Prove _ => Integer.add 1 | _ => I) + proof 0 +fun metis_steps_total proof = + fold (fn Obtain _ => Integer.add 1 + | Prove (_, _, _, By_Metis _) => Integer.add 1 + | Prove (_, _, _, Case_Split (cases, _)) => + Integer.add (fold (Integer.add o metis_steps_total) cases 1) | _ => I) proof 0 end diff -r 20beafe66748 -r 97f951edca46 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jan 02 21:55:57 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jan 02 22:16:16 2013 +0100 @@ -150,13 +150,13 @@ else isa_ext -val leo2_ext = "extcnf_equal_neg" -val leo2_unfold_def = "unfold_def" +val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg" +val leo2_unfold_def_rule = "unfold_def" fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, _, rule, deps)) = - (if rule = leo2_ext then + (if rule = leo2_extcnf_equal_neg_rule then insert (op =) (ext_name ctxt, (Global, General)) - else if rule = leo2_unfold_def then + else if rule = leo2_unfold_def_rule then (* LEO 1.3.3 does not record definitions properly, leading to missing dependencies in the TSTP proof. Remove the next line once this is fixed. *) @@ -389,19 +389,18 @@ Inference_Step (name, role, t, rule, []) :: lines else map (replace_dependencies_in_line (name, [])) lines - | add_line _ (Inference_Step (name, role, t, rule, deps)) lines = + | add_line _ (line as Inference_Step (name, role, t, rule, deps)) lines = (* Type information will be deleted later; skip repetition test. *) if is_only_type_information t then - Inference_Step (name, role, t, rule, deps) :: lines + line :: lines (* Is there a repetition? If so, replace later line by earlier one. *) else case take_prefix (not o is_same_inference t) lines of (* FIXME: Doesn't this code risk conflating proofs involving different types? *) - (_, []) => Inference_Step (name, role, t, rule, deps) :: lines - | (pre, Inference_Step (name', role, t', rule, _) :: post) => - Inference_Step (name, role, t', rule, deps) :: - pre @ map (replace_dependencies_in_line (name', [name])) post - | _ => raise Fail "unexpected inference" + (_, []) => line :: lines + | (pre, Inference_Step (name', _, _, _, _) :: post) => + line :: pre @ map (replace_dependencies_in_line (name', [name])) post + | _ => raise Fail "unexpected inference" val waldmeister_conjecture_num = "1.0.0.0" @@ -431,6 +430,12 @@ fun is_bad_free frees (Free x) = not (member (op =) frees x) | is_bad_free _ _ = false +val e_skolemize_rule = "skolemize" +val vampire_skolemisation_rule = "skolemisation" + +val is_skolemize_rule = + member (op =) [e_skolemize_rule, vampire_skolemisation_rule] + fun add_desired_line _ _ (line as Definition_Step (name, _, _)) (j, lines) = (j, line :: map (replace_dependencies_in_line (name, [])) lines) | add_desired_line fact_names frees @@ -438,6 +443,7 @@ (j + 1, if is_fact fact_names ss orelse is_conjecture ss orelse + is_skolemize_rule rule orelse (* the last line must be kept *) j = 0 orelse (not (is_only_type_information t) andalso @@ -467,13 +473,16 @@ if member (op =) qs Show then "thus" else "hence" else if member (op =) qs Show then "show" else "have") + fun do_obtain qs xs = + (if member (op =) qs Then then "then " else "") ^ "obtain " ^ + (space_implode " " (map fst xs)) ^ " where" val do_term = annotate_types ctxt #> with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces #> maybe_quote val reconstr = Metis (type_enc, lam_trans) - fun do_facts ind (ls, ss) = + fun do_metis ind (ls, ss) = "\n" ^ do_indent (ind + 1) ^ reconstructor_command reconstr 1 1 [] 0 (ls |> sort_distinct (prod_ord string_ord int_ord), @@ -484,14 +493,17 @@ do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n" | do_step ind (Assume (l, t)) = do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n" + | do_step ind (Obtain (qs, xs, l, t, By_Metis facts)) = + do_indent ind ^ do_obtain qs xs ^ " " ^ + do_label l ^ do_term t ^ do_metis ind facts ^ "\n" | do_step ind (Prove (qs, l, t, By_Metis facts)) = do_indent ind ^ do_have qs ^ " " ^ - do_label l ^ do_term t ^ do_facts ind facts ^ "\n" + do_label l ^ do_term t ^ do_metis ind facts ^ "\n" | do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) = implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind) proofs) ^ do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ - do_facts ind facts ^ "\n" + do_metis ind facts ^ "\n" and do_steps prefix suffix ind steps = let val s = implode (map (do_step ind) steps) in replicate_string (ind * indent_size - size prefix) " " ^ prefix ^ @@ -509,7 +521,8 @@ (if n <> 1 then "next" else "qed") in do_proof end -fun used_labels_of_step (Prove (_, _, _, by)) = +fun used_labels_of_step (Obtain (_, _, _, _, By_Metis (ls, _))) = ls + | used_labels_of_step (Prove (_, _, _, by)) = (case by of By_Metis (ls, _) => ls | Case_Split (proofs, (ls, _)) => @@ -522,6 +535,7 @@ val used_ls = used_labels_of proof fun do_label l = if member (op =) used_ls l then l else no_label fun do_step (Assume (l, t)) = Assume (do_label l, t) + | do_step (Obtain (qs, xs, l, t, by)) = Obtain (qs, xs, do_label l, t, by) | do_step (Prove (qs, l, t, by)) = Prove (qs, do_label l, t, case by of @@ -535,60 +549,77 @@ val relabel_proof = let - fun aux _ _ _ [] = [] - | aux subst depth (next_assum, next_have) (Assume (l, t) :: proof) = + fun fresh_label depth (old as (l, subst, next_have)) = + if l = no_label then + old + else + let val l' = (prefix_for_depth depth have_prefix, next_have) in + (l', (l, l') :: subst, next_have + 1) + end + fun do_facts subst = + apfst (maps (the_list o AList.lookup (op =) subst)) + fun do_byline subst depth by = + case by of + By_Metis facts => By_Metis (do_facts subst facts) + | Case_Split (proofs, facts) => + Case_Split (map (do_proof subst (depth + 1) (1, 1)) proofs, + do_facts subst facts) + and do_proof _ _ _ [] = [] + | do_proof subst depth (next_assum, next_have) (Assume (l, t) :: proof) = if l = no_label then - Assume (l, t) :: aux subst depth (next_assum, next_have) proof + Assume (l, t) :: do_proof subst depth (next_assum, next_have) proof else let val l' = (prefix_for_depth depth assume_prefix, next_assum) in Assume (l', t) :: - aux ((l, l') :: subst) depth (next_assum + 1, next_have) proof + do_proof ((l, l') :: subst) depth (next_assum + 1, next_have) proof end - | aux subst depth (next_assum, next_have) + | do_proof subst depth (next_assum, next_have) + (Obtain (qs, xs, l, t, by) :: proof) = + let + val (l, subst, next_have) = (l, subst, next_have) |> fresh_label depth + val by = by |> do_byline subst depth + in + Obtain (qs, xs, l, t, by) :: + do_proof subst depth (next_assum, next_have) proof + end + | do_proof subst depth (next_assum, next_have) (Prove (qs, l, t, by) :: proof) = let - val (l', subst, next_have) = - if l = no_label then - (l, subst, next_have) - else - let val l' = (prefix_for_depth depth have_prefix, next_have) in - (l', (l, l') :: subst, next_have + 1) - end - val relabel_facts = - apfst (maps (the_list o AList.lookup (op =) subst)) - val by = - case by of - By_Metis facts => By_Metis (relabel_facts facts) - | Case_Split (proofs, facts) => - Case_Split (map (aux subst (depth + 1) (1, 1)) proofs, - relabel_facts facts) + val (l, subst, next_have) = (l, subst, next_have) |> fresh_label depth + val by = by |> do_byline subst depth in - Prove (qs, l', t, by) :: aux subst depth (next_assum, next_have) proof + Prove (qs, l, t, by) :: + do_proof subst depth (next_assum, next_have) proof end - | aux subst depth nextp (step :: proof) = - step :: aux subst depth nextp proof - in aux [] 0 (1, 1) end + | do_proof subst depth nextp (step :: proof) = + step :: do_proof subst depth nextp proof + in do_proof [] 0 (1, 1) end val chain_direct_proof = let - fun succedent_of_step (Prove (_, label, _, _)) = SOME label - | succedent_of_step (Assume (label, _)) = SOME label - | succedent_of_step _ = NONE - fun chain_inf (SOME label0) - (step as Prove (qs, label, t, By_Metis (lfs, gfs))) = - if member (op =) lfs label0 then - Prove (Then :: qs, label, t, - By_Metis (filter_out (curry (op =) label0) lfs, gfs)) + fun label_of (Assume (l, _)) = SOME l + | label_of (Obtain (_, _, l, _, _)) = SOME l + | label_of (Prove (_, l, _, _)) = SOME l + | label_of _ = NONE + fun chain_step (SOME l0) + (step as Obtain (qs, xs, l, t, By_Metis (lfs, gfs))) = + if member (op =) lfs l0 then + Obtain (Then :: qs, xs, l, t, By_Metis (lfs |> remove (op =) l0, gfs)) else step - | chain_inf _ (Prove (qs, label, t, Case_Split (proofs, facts))) = - Prove (qs, label, t, Case_Split ((map (chain_proof NONE) proofs), facts)) - | chain_inf _ step = step + | chain_step (SOME l0) + (step as Prove (qs, l, t, By_Metis (lfs, gfs))) = + if member (op =) lfs l0 then + Prove (Then :: qs, l, t, By_Metis (lfs |> remove (op =) l0, gfs)) + else + step + | chain_step _ (Prove (qs, l, t, Case_Split (proofs, facts))) = + Prove (qs, l, t, Case_Split ((map (chain_proof NONE) proofs), facts)) + | chain_step _ step = step and chain_proof _ [] = [] | chain_proof (prev as SOME _) (i :: is) = - chain_inf prev i :: chain_proof (succedent_of_step i) is - | chain_proof _ (i :: is) = - i :: chain_proof (succedent_of_step i) is + chain_step prev i :: chain_proof (label_of i) is + | chain_proof _ (i :: is) = i :: chain_proof (label_of i) is in chain_proof NONE end type isar_params = @@ -644,25 +675,32 @@ val ref_graph = atp_proof |> map_filter dep_of_step |> make_ref_graph val axioms = axioms_of_ref_graph ref_graph conjs val tainted = tainted_atoms_of_ref_graph ref_graph conjs - val props = + val steps = Symtab.empty |> fold (fn Definition_Step _ => I (* FIXME *) - | Inference_Step (name as (s, ss), role, t, _, _) => - Symtab.update_new (s, - if member (op = o apsnd fst) tainted s then - t |> role <> Conjecture ? s_not - |> fold exists_of (map Var (Term.add_vars t [])) - else - t)) + | Inference_Step (name as (s, ss), role, t, rule, _) => + Symtab.update_new (s, (rule, + t |> (if member (op = o apsnd fst) tainted s then + (role <> Conjecture ? s_not) + #> fold exists_of (map Var (Term.add_vars t [])) + else + I)))) atp_proof - (* The assumptions and conjecture are props; the rest are bools. *) + fun is_clause_skolemize_rule [(s, _)] = + Option.map (is_skolemize_rule o fst) (Symtab.lookup steps s) = + SOME true + | is_clause_skolemize_rule _ = false + (* The assumptions and conjecture are "prop"s; the other formulas are + "bool"s. *) fun prop_of_clause [name as (s, ss)] = (case resolve_conjecture ss of [j] => if j = length hyp_ts then concl_t else nth hyp_ts j - | _ => the_default @{term False} (Symtab.lookup props s) - |> HOLogic.mk_Trueprop |> close_form) + | _ => the_default ("", @{term False}) (Symtab.lookup steps s) + |> snd |> HOLogic.mk_Trueprop |> close_form) | prop_of_clause names = - let val lits = map_filter (Symtab.lookup props o fst) names in + let + val lits = map snd (map_filter (Symtab.lookup steps o fst) names) + in case List.partition (can HOLogic.dest_not) lits of (negs as _ :: _, pos as _ :: _) => HOLogic.mk_imp @@ -674,12 +712,24 @@ fun maybe_show outer c = (outer andalso length c = 1 andalso subset (op =) (c, conjs)) ? cons Show - fun do_have outer qs (gamma, c) = - Prove (maybe_show outer c qs, label_of_clause c, prop_of_clause c, - By_Metis (fold (add_fact_from_dependencies fact_names) gamma - ([], []))) - fun do_inf outer (Have z) = do_have outer [] z - | do_inf outer (Cases cases) = + fun isar_step_of_direct_inf outer (Have (gamma, c)) = + let + val l = label_of_clause c + val t = prop_of_clause c + val by = + By_Metis (fold (add_fact_from_dependencies fact_names) gamma + ([], [])) + in + if is_clause_skolemize_rule c then + let + val xs = + Term.add_frees t [] + |> filter_out (Variable.is_declared ctxt o fst) + in Obtain ([], xs, l, t, by) end + else + Prove (maybe_show outer c [], l, t, by) + end + | isar_step_of_direct_inf outer (Cases cases) = let val c = succedent_of_cases cases in Prove (maybe_show outer c [Ultimately], label_of_clause c, prop_of_clause c, @@ -687,18 +737,18 @@ end and do_case outer (c, infs) = Assume (label_of_clause c, prop_of_clause c) :: - map (do_inf outer) infs + map (isar_step_of_direct_inf outer) infs val (isar_proof, (preplay_fail, ext_time)) = ref_graph |> redirect_graph axioms tainted - |> map (do_inf true) + |> map (isar_step_of_direct_inf true) |> append assms |> (if not preplay andalso isar_shrink <= 1.0 then - pair (false, (true, seconds 0.0)) #> swap + rpair (false, (true, seconds 0.0)) else shrink_proof debug ctxt type_enc lam_trans preplay - preplay_timeout - (if isar_proofs then isar_shrink else 1000.0)) + preplay_timeout + (if isar_proofs then isar_shrink else 1000.0)) (* |>> reorder_proof_to_minimize_jumps (* ? *) *) |>> chain_direct_proof |>> kill_useless_labels_in_proof @@ -711,22 +761,23 @@ case isar_text of "" => if isar_proofs then - "\nNo structured proof available (proof too short)." + "\nNo structured proof available (proof too simple)." else "" | _ => - let - val msg = - (if preplay then - [if preplay_fail - then "may fail" + let + val msg = + (if preplay then + [if preplay_fail then "may fail" else string_from_ext_time ext_time] - else []) - @ - (if verbose then - [let val num_steps = metis_steps_total isar_proof - in string_of_int num_steps ^ plural_s num_steps end] - else []) + else + []) @ + (if verbose then + let val num_steps = metis_steps_total isar_proof in + [string_of_int num_steps ^ " step" ^ plural_s num_steps] + end + else + []) in "\n\nStructured proof " ^ (commas msg |> not (null msg) ? enclose "(" ")") diff -r 20beafe66748 -r 97f951edca46 src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Wed Jan 02 21:55:57 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML Wed Jan 02 22:16:16 2013 +0100 @@ -8,7 +8,7 @@ signature SLEDGEHAMMER_SHRINK = sig type isar_step = Sledgehammer_Proof.isar_step - val shrink_proof : + val shrink_proof : bool -> Proof.context -> string -> string -> bool -> Time.time option -> real -> isar_step list -> isar_step list * (bool * (bool * Time.time)) end @@ -58,225 +58,220 @@ (* Main function for shrinking proofs *) fun shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout isar_shrink proof = -let - (* 60 seconds seems like a good interpreation of "no timeout" *) - val preplay_timeout = preplay_timeout |> the_default (seconds 60.0) + let + (* 60 seconds seems like a good interpreation of "no timeout" *) + val preplay_timeout = preplay_timeout |> the_default (seconds 60.0) + + (* handle metis preplay fail *) + local + open Unsynchronized + val metis_fail = ref false + in + fun handle_metis_fail try_metis () = + try_metis () handle _ => (metis_fail := true; SOME Time.zeroTime) + fun get_time lazy_time = + if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time + val metis_fail = fn () => !metis_fail + end - (* handle metis preplay fail *) - local - open Unsynchronized - val metis_fail = ref false - in - fun handle_metis_fail try_metis () = - try_metis () handle _ => (metis_fail := true; SOME Time.zeroTime) - fun get_time lazy_time = - if !metis_fail then SOME Time.zeroTime else Lazy.force lazy_time - val metis_fail = fn () => !metis_fail - end - - (* Shrink top level proof - do not shrink case splits *) - fun shrink_top_level on_top_level ctxt proof = - let - (* proof vector *) - val proof_vect = proof |> map SOME |> Vector.fromList - val n = Vector.length proof_vect - val n_metis = metis_steps_top_level proof - val target_n_metis = Real.fromInt n_metis / isar_shrink |> Real.round + (* Shrink top level proof - do not shrink case splits *) + fun shrink_top_level on_top_level ctxt proof = + let + (* proof vector *) + val proof_vect = proof |> map SOME |> Vector.fromList + val n = Vector.length proof_vect + val n_metis = metis_steps_top_level proof + val target_n_metis = Real.fromInt n_metis / isar_shrink |> Real.round - (* table for mapping from (top-level-)label to proof position *) - fun update_table (i, Assume (label, _)) = - Label_Table.update_new (label, i) - | update_table (i, Prove (_, label, _, _)) = - Label_Table.update_new (label, i) - | update_table _ = I - val label_index_table = fold_index update_table proof Label_Table.empty + (* table for mapping from (top-level-)label to proof position *) + fun update_table (i, Assume (l, _)) = Label_Table.update_new (l, i) + | update_table (i, Obtain (_, _, l, _, _)) = Label_Table.update_new (l, i) + | update_table (i, Prove (_, l, _, _)) = Label_Table.update_new (l, i) + | update_table _ = I + val label_index_table = fold_index update_table proof Label_Table.empty + val filter_refs = map_filter (Label_Table.lookup label_index_table) - (* proof references *) - fun refs (Prove (_, _, _, By_Metis (lfs, _))) = - map_filter (Label_Table.lookup label_index_table) lfs - | refs (Prove (_, _, _, Case_Split (cases, (lfs, _)))) = - map_filter (Label_Table.lookup label_index_table) lfs - @ maps (maps refs) cases - | refs _ = [] - val refed_by_vect = - Vector.tabulate (n, (fn _ => [])) - |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) proof - |> Vector.map rev (* after rev, indices are sorted in ascending order *) - - (* candidates for elimination, use table as priority queue (greedy - algorithm) *) - fun add_if_cand proof_vect (i, [j]) = - (case (the (get i proof_vect), the (get j proof_vect)) of - (Prove (_, _, t, By_Metis _), Prove (_, _, _, By_Metis _)) => - cons (Term.size_of_term t, i) - | _ => I) - | add_if_cand _ _ = I - val cand_tab = - v_fold_index (add_if_cand proof_vect) refed_by_vect [] - |> Inttab.make_list + (* proof references *) + fun refs (Obtain (_, _, _, _, By_Metis (lfs, _))) = filter_refs lfs + | refs (Prove (_, _, _, By_Metis (lfs, _))) = filter_refs lfs + | refs (Prove (_, _, _, Case_Split (cases, (lfs, _)))) = + filter_refs lfs @ maps (maps refs) cases + | refs _ = [] + val refed_by_vect = + Vector.tabulate (n, (fn _ => [])) + |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) proof + |> Vector.map rev (* after rev, indices are sorted in ascending order *) - (* Metis Preplaying *) - fun resolve_fact_names names = - names - |>> map string_for_label - |> op @ - |> maps (thms_of_name ctxt) + (* candidates for elimination, use table as priority queue (greedy + algorithm) *) + (* TODO: consider adding "Obtain" cases *) + fun add_if_cand proof_vect (i, [j]) = + (case (the (get i proof_vect), the (get j proof_vect)) of + (Prove (_, _, t, By_Metis _), Prove (_, _, _, By_Metis _)) => + cons (Term.size_of_term t, i) + | _ => I) + | add_if_cand _ _ = I + val cand_tab = + v_fold_index (add_if_cand proof_vect) refed_by_vect [] + |> Inttab.make_list - fun try_metis timeout (succedent, Prove (_, _, t, byline)) = - if not preplay then (fn () => SOME Time.zeroTime) else - (case byline of - By_Metis fact_names => - let - val facts = resolve_fact_names fact_names - val goal = - Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t - fun tac {context = ctxt, prems = _} = - Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 - in - take_time timeout (fn () => goal tac) - end - | Case_Split (cases, fact_names) => - let - val facts = + (* Metis Preplaying *) + fun resolve_fact_names names = + names + |>> map string_for_label + |> op @ + |> maps (thms_of_name ctxt) + + (* TODO: add "Obtain" case *) + fun try_metis timeout (succedent, Prove (_, _, t, byline)) = + if not preplay then K (SOME Time.zeroTime) else + let + val make_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) + val facts = + (case byline of + By_Metis fact_names => resolve_fact_names fact_names + | Case_Split (cases, fact_names) => resolve_fact_names fact_names @ (case the succedent of - Prove (_, _, t, _) => - Skip_Proof.make_thm (Proof_Context.theory_of ctxt) t - | Assume (_, t) => - Skip_Proof.make_thm (Proof_Context.theory_of ctxt) t + Assume (_, t) => make_thm t + | Obtain (_, _, _, t, _) => make_thm t + | Prove (_, _, t, _) => make_thm t | _ => error "Internal error: unexpected succedent of case split") - :: map - (hd #> (fn Assume (_, a) => Logic.mk_implies(a, t) - | _ => error "Internal error: malformed case split") - #> Skip_Proof.make_thm (Proof_Context.theory_of ctxt)) - cases - val goal = - Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t - fun tac {context = ctxt, prems = _} = - Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 - in - take_time timeout (fn () => goal tac) - end) - | try_metis _ _ = (fn () => SOME Time.zeroTime) + :: map (hd #> (fn Assume (_, a) => Logic.mk_implies (a, t) + | _ => error "Internal error: malformed case split") + #> make_thm) + cases) + val goal = + Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] t + fun tac {context = ctxt, prems = _} = + Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 + in + take_time timeout (fn () => goal tac) + end + | try_metis _ _ = K (SOME Time.zeroTime) - val try_metis_quietly = the_default NONE oo try oo try_metis + val try_metis_quietly = the_default NONE oo try oo try_metis + + (* cache metis preplay times in lazy time vector *) + val metis_time = + v_map_index + (Lazy.lazy o handle_metis_fail o try_metis preplay_timeout + o apfst (fn i => try (the o get (i-1)) proof_vect) o apsnd the) + proof_vect + fun sum_up_time lazy_time_vector = + Vector.foldl + ((fn (SOME t, (b, ts)) => (b, Time.+(t, ts)) + | (NONE, (_, ts)) => (true, Time.+(ts, preplay_timeout))) + o apfst get_time) + no_time lazy_time_vector - (* cache metis preplay times in lazy time vector *) - val metis_time = - v_map_index - (Lazy.lazy o handle_metis_fail o try_metis preplay_timeout - o apfst (fn i => try (the o get (i-1)) proof_vect) o apsnd the) - proof_vect - fun sum_up_time lazy_time_vector = - Vector.foldl - ((fn (SOME t, (b, ts)) => (b, Time.+(t, ts)) - | (NONE, (_, ts)) => (true, Time.+(ts, preplay_timeout))) - o apfst get_time) - no_time lazy_time_vector + (* Merging *) + (* TODO: consider adding "Obtain" cases *) + fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) + (Prove (qs2, label2, t, By_Metis (lfs2, gfs2))) = + let + val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1 + val gfs = union (op =) gfs1 gfs2 + in Prove (qs2, label2, t, By_Metis (lfs, gfs)) end + | merge _ _ = error "Internal error: Unmergeable Isar steps" - (* Merging *) - fun merge (Prove (_, label1, _, By_Metis (lfs1, gfs1))) - (Prove (qs2, label2 , t, By_Metis (lfs2, gfs2))) = - let - val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1 - val gfs = union (op =) gfs1 gfs2 - in Prove (qs2, label2, t, By_Metis (lfs, gfs)) end - | merge _ _ = error "Internal error: Tring to merge unmergable isar steps" + fun try_merge metis_time (s1, i) (s2, j) = + (case get i metis_time |> Lazy.force of + NONE => (NONE, metis_time) + | SOME t1 => + (case get j metis_time |> Lazy.force of + NONE => (NONE, metis_time) + | SOME t2 => + let + val s12 = merge s1 s2 + val timeout = time_mult merge_timeout_slack (Time.+(t1, t2)) + in + case try_metis_quietly timeout (NONE, s12) () of + NONE => (NONE, metis_time) + | some_t12 => + (SOME s12, metis_time + |> replace (Time.zeroTime |> SOME |> Lazy.value) i + |> replace (Lazy.value some_t12) j) - fun try_merge metis_time (s1, i) (s2, j) = - (case get i metis_time |> Lazy.force of - NONE => (NONE, metis_time) - | SOME t1 => - (case get j metis_time |> Lazy.force of - NONE => (NONE, metis_time) - | SOME t2 => + end)) + + fun merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' = + if Inttab.is_empty cand_tab + orelse n_metis' <= target_n_metis + orelse (on_top_level andalso n'<3) + then + (Vector.foldr + (fn (NONE, proof) => proof | (SOME s, proof) => s :: proof) + [] proof_vect, + sum_up_time metis_time) + else let - val s12 = merge s1 s2 - val timeout = time_mult merge_timeout_slack (Time.+(t1, t2)) + val (i, cand_tab) = pop_max cand_tab + val j = get i refed_by |> the_single + val s1 = get i proof_vect |> the + val s2 = get j proof_vect |> the in - case try_metis_quietly timeout (NONE, s12) () of - NONE => (NONE, metis_time) - | some_t12 => - (SOME s12, metis_time - |> replace (Time.zeroTime |> SOME |> Lazy.value) i - |> replace (Lazy.value some_t12) j) - - end)) - - fun merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' = - if Inttab.is_empty cand_tab - orelse n_metis' <= target_n_metis - orelse (on_top_level andalso n'<3) - then - (Vector.foldr - (fn (NONE, proof) => proof | (SOME s, proof) => s :: proof) - [] proof_vect, - sum_up_time metis_time) - else - let - val (i, cand_tab) = pop_max cand_tab - val j = get i refed_by |> the_single - val s1 = get i proof_vect |> the - val s2 = get j proof_vect |> the - in - case try_merge metis_time (s1, i) (s2, j) of - (NONE, metis_time) => - merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' - | (s, metis_time) => - let - val refs = refs s1 - val refed_by = refed_by |> fold - (update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j)) refs - val new_candidates = - fold (add_if_cand proof_vect) - (map (fn i => (i, get i refed_by)) refs) [] - val cand_tab = add_list cand_tab new_candidates - val proof_vect = proof_vect |> replace NONE i |> replace s j - in - merge_steps metis_time proof_vect refed_by cand_tab (n' - 1) (n_metis' - 1) + case try_merge metis_time (s1, i) (s2, j) of + (NONE, metis_time) => + merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' + | (s, metis_time) => + let + val refs = refs s1 + val refed_by = refed_by |> fold + (update (Ord_List.remove int_ord i #> Ord_List.insert int_ord j)) refs + val new_candidates = + fold (add_if_cand proof_vect) + (map (fn i => (i, get i refed_by)) refs) [] + val cand_tab = add_list cand_tab new_candidates + val proof_vect = proof_vect |> replace NONE i |> replace s j + in + merge_steps metis_time proof_vect refed_by cand_tab (n' - 1) + (n_metis' - 1) + end end - end - in - merge_steps metis_time proof_vect refed_by_vect cand_tab n n_metis - end - - fun shrink_proof' on_top_level ctxt proof = - let - (* Enrich context with top-level facts *) - val thy = Proof_Context.theory_of ctxt - fun enrich_ctxt (Assume (label, t)) ctxt = - Proof_Context.put_thms false - (string_for_label label, SOME [Skip_Proof.make_thm thy t]) ctxt - | enrich_ctxt (Prove (_, label, t, _)) ctxt = - Proof_Context.put_thms false - (string_for_label label, SOME [Skip_Proof.make_thm thy t]) ctxt - | enrich_ctxt _ ctxt = ctxt - val rich_ctxt = fold enrich_ctxt proof ctxt - - (* Shrink case_splits and top-levl *) - val ((proof, top_level_time), lower_level_time) = - proof |> shrink_case_splits rich_ctxt - |>> shrink_top_level on_top_level rich_ctxt in - (proof, ext_time_add lower_level_time top_level_time) + merge_steps metis_time proof_vect refed_by_vect cand_tab n n_metis end - and shrink_case_splits ctxt proof = - let - fun shrink_each_and_collect_time shrink candidates = - let fun f_m cand time = shrink cand ||> ext_time_add time - in fold_map f_m candidates no_time end - val shrink_case_split = shrink_each_and_collect_time (shrink_proof' false ctxt) - fun shrink (Prove (qs, lbl, t, Case_Split (cases, facts))) = - let val (cases, time) = shrink_case_split cases - in (Prove (qs, lbl, t, Case_Split (cases, facts)), time) end - | shrink step = (step, no_time) - in - shrink_each_and_collect_time shrink proof - end -in - shrink_proof' true ctxt proof - |> apsnd (pair (metis_fail () ) ) -end + fun do_proof on_top_level ctxt proof = + let + (* Enrich context with top-level facts *) + val thy = Proof_Context.theory_of ctxt + (* TODO: add Skolem variables to context? *) + fun enrich_with_fact l t = + Proof_Context.put_thms false + (string_for_label l, SOME [Skip_Proof.make_thm thy t]) + fun enrich_with_step (Assume (l, t)) = enrich_with_fact l t + | enrich_with_step (Obtain (_, _, l, t, _)) = enrich_with_fact l t + | enrich_with_step (Prove (_, l, t, _)) = enrich_with_fact l t + | enrich_with_step _ = I + val rich_ctxt = fold enrich_with_step proof ctxt + + (* Shrink case_splits and top-levl *) + val ((proof, top_level_time), lower_level_time) = + proof |> do_case_splits rich_ctxt + |>> shrink_top_level on_top_level rich_ctxt + in + (proof, ext_time_add lower_level_time top_level_time) + end + + and do_case_splits ctxt proof = + let + fun shrink_each_and_collect_time shrink candidates = + let fun f_m cand time = shrink cand ||> ext_time_add time + in fold_map f_m candidates no_time end + val shrink_case_split = + shrink_each_and_collect_time (do_proof false ctxt) + fun shrink (Prove (qs, l, t, Case_Split (cases, facts))) = + let val (cases, time) = shrink_case_split cases + in (Prove (qs, l, t, Case_Split (cases, facts)), time) end + | shrink step = (step, no_time) + in + shrink_each_and_collect_time shrink proof + end + in + do_proof true ctxt proof + |> apsnd (pair (metis_fail ())) + end end