# HG changeset patch # User smolkas # Date 1361186187 -3600 # Node ID 0d5f8812856f5344ea1f069f1b455984a5b019e7 # Parent 06689dbfe072e47741c6b9a2e7cf7725b81c4f38 split isar_step into isar_step, fix, assms; made isar_proof explicit; register fixed variables in ctxt and auto_fix terms to avoid superfluous annotations diff -r 06689dbfe072 -r 0d5f8812856f src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Mon Feb 18 12:16:02 2013 +0100 +++ b/src/HOL/Sledgehammer.thy Mon Feb 18 12:16:27 2013 +0100 @@ -19,7 +19,7 @@ ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML" ML_file "Tools/Sledgehammer/sledgehammer_preplay.ML" ML_file "Tools/Sledgehammer/sledgehammer_compress.ML" -ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML" +ML_file "Tools/Sledgehammer/sledgehammer_reconstruct.ML" ML_file "Tools/Sledgehammer/sledgehammer_provers.ML" ML_file "Tools/Sledgehammer/sledgehammer_minimize.ML" ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML" diff -r 06689dbfe072 -r 0d5f8812856f src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML Mon Feb 18 12:16:02 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_annotate.ML Mon Feb 18 12:16:27 2013 +0100 @@ -2,7 +2,7 @@ Author: Jasmin Blanchette, TU Muenchen Author: Steffen Juilf Smolka, TU Muenchen -Supplement term with explicit type constraints that show up as +Supplement term with explicit type constraints that show up as type annotations when printing the term. *) diff -r 06689dbfe072 -r 0d5f8812856f src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Mon Feb 18 12:16:02 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Mon Feb 18 12:16:27 2013 +0100 @@ -7,11 +7,11 @@ signature SLEDGEHAMMER_COMPRESS = sig - type isar_step = Sledgehammer_Proof.isar_step + type isar_proof = Sledgehammer_Proof.isar_proof type preplay_time = Sledgehammer_Preplay.preplay_time val compress_proof : bool -> Proof.context -> string -> string -> bool -> Time.time option - -> real -> isar_step list -> isar_step list * (bool * preplay_time) + -> real -> isar_proof -> isar_proof * (bool * preplay_time) end structure Sledgehammer_Compress : SLEDGEHAMMER_COMPRESS = @@ -68,38 +68,37 @@ val metis_fail = fn () => !metis_fail end - (* compress proof on top level - do not compress subproofs *) - fun compress_top_level on_top_level ctxt proof = + (* compress top level steps - do not compress subproofs *) + fun compress_top_level on_top_level ctxt steps = 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 + (* proof step vector *) + val step_vect = steps |> map SOME |> Vector.fromList + val n = Vector.length step_vect + val n_metis = add_metis_steps_top_level steps 0 val target_n_metis = Real.fromInt n_metis / isar_compress |> Real.round - (* table for mapping from (top-level-)label to proof position *) - fun update_table (i, Assume (l, _)) = Label_Table.update_new (l, i) + (* table for mapping from (top-level-)label to step_vect position *) + fun update_table (i, Prove (_, 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 label_index_table = fold_index update_table steps Label_Table.empty val lookup_indices = map_filter (Label_Table.lookup label_index_table) - (* proof references *) - fun refs (Obtain (_, _, _, _, By_Metis (subproofs, (lfs, _)))) = - maps (maps refs) subproofs @ lookup_indices lfs - | refs (Prove (_, _, _, By_Metis (subproofs, (lfs, _)))) = - maps (maps refs) subproofs @ lookup_indices lfs - | refs _ = [] + (* proof step references *) + fun refs step = + (case byline_of_step step of + NONE => [] + | SOME (By_Metis (subproofs, (lfs, _))) => + maps (steps_of_proof #> maps refs) subproofs @ lookup_indices lfs) val refed_by_vect = Vector.tabulate (n, K []) - |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) proof + |> fold_index (fn (i, step) => fold (update (cons i)) (refs step)) steps |> 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 + fun add_if_cand step_vect (i, [j]) = + (case (the (get i step_vect), the (get j step_vect)) of (Prove (_, _, t, By_Metis _), Prove (_, _, _, By_Metis _)) => cons (Term.size_of_term t, i) | (Prove (_, _, t, By_Metis _), Obtain (_, _, _, _, By_Metis _)) => @@ -107,7 +106,7 @@ | _ => I) | add_if_cand _ _ = I val cand_tab = - v_fold_index (add_if_cand proof_vect) refed_by_vect [] + v_fold_index (add_if_cand step_vect) refed_by_vect [] |> Inttab.make_list (* cache metis preplay times in lazy time vector *) @@ -119,7 +118,7 @@ #> try_metis debug type_enc lam_trans ctxt preplay_timeout #> handle_metis_fail #> Lazy.lazy) - proof_vect + step_vect fun sum_up_time lazy_time_vector = Vector.foldl @@ -127,17 +126,16 @@ zero_preplay_time lazy_time_vector (* Merging *) - fun merge (Prove (_, label1, _, By_Metis (subproofs1, (lfs1, gfs1)))) - step2 = + fun merge (Prove (_, lbl1, _, By_Metis (subproofs1, (lfs1, gfs1)))) step2 = let val (step_constructor, (subproofs2, (lfs2, gfs2))) = (case step2 of - Prove (qs2, label2, t, By_Metis x) => - (fn by => Prove (qs2, label2, t, by), x) - | Obtain (qs2, xs, label2, t, By_Metis x) => - (fn by => Obtain (qs2, xs, label2, t, by), x) + Prove (qs2, lbl2, t, By_Metis x) => + (fn by => Prove (qs2, lbl2, t, by), x) + | Obtain (qs2, xs, lbl2, t, By_Metis x) => + (fn by => Obtain (qs2, xs, lbl2, t, by), x) | _ => error "sledgehammer_compress: unmergeable Isar steps" ) - val lfs = remove (op =) label1 lfs2 |> union (op =) lfs1 + val lfs = remove (op =) lbl1 lfs2 |> union (op =) lfs1 val gfs = union (op =) gfs1 gfs2 val subproofs = subproofs1 @ subproofs2 in step_constructor (By_Metis (subproofs, (lfs, gfs))) end @@ -166,45 +164,45 @@ end)) - fun merge_steps metis_time proof_vect refed_by cand_tab n' n_metis' = + fun merge_steps metis_time step_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, + (fn (NONE, steps) => steps | (SOME s, steps) => s :: steps) + [] step_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 + val s1 = get i step_vect |> the + val s2 = get j step_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' + merge_steps metis_time step_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) + fold (add_if_cand step_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 + val step_vect = step_vect |> replace NONE i |> replace s j in - merge_steps metis_time proof_vect refed_by cand_tab (n' - 1) + merge_steps metis_time step_vect refed_by cand_tab (n' - 1) (n_metis' - 1) end end in - merge_steps metis_time proof_vect refed_by_vect cand_tab n n_metis + merge_steps metis_time step_vect refed_by_vect cand_tab n n_metis end - fun do_proof on_top_level ctxt proof = + fun do_proof on_top_level ctxt (Proof (fix, assms,steps)) = let (* Enrich context with top-level facts *) val thy = Proof_Context.theory_of ctxt @@ -212,21 +210,25 @@ 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 + fun enrich_with_step (Prove (_, 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 + val enrich_with_steps = fold enrich_with_step + fun enrich_with_assms (Assume assms) = + fold (uncurry enrich_with_fact) assms + val rich_ctxt = + ctxt |> enrich_with_assms assms |> enrich_with_steps steps - (* compress subproofs and top-levl proof *) - val ((proof, top_level_time), lower_level_time) = - proof |> do_subproofs rich_ctxt + (* compress subproofs and top-levl steps *) + val ((steps, top_level_time), lower_level_time) = + steps |> do_subproofs rich_ctxt |>> compress_top_level on_top_level rich_ctxt in - (proof, add_preplay_time lower_level_time top_level_time) + (Proof (fix, assms, steps), + add_preplay_time lower_level_time top_level_time) end - and do_subproofs ctxt proof = + and do_subproofs ctxt subproofs = let fun compress_each_and_collect_time compress subproofs = let fun f_m proof time = compress proof ||> add_preplay_time time @@ -238,7 +240,7 @@ in (Prove (qs, l, t, By_Metis(subproofs, facts)), time) end | compress atomic_step = (atomic_step, zero_preplay_time) in - compress_each_and_collect_time compress proof + compress_each_and_collect_time compress subproofs end in do_proof true ctxt proof diff -r 06689dbfe072 -r 0d5f8812856f src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Mon Feb 18 12:16:02 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Mon Feb 18 12:16:27 2013 +0100 @@ -50,23 +50,25 @@ (* lookup facts in context *) fun resolve_fact_names ctxt names = - names + (names |>> map string_for_label |> op @ - |> maps (thms_of_name ctxt) + |> maps (thms_of_name ctxt)) + handle ERROR msg => error ("preplay error: " ^ msg) (* *) fun thm_of_term ctxt = Skip_Proof.make_thm (Proof_Context.theory_of ctxt) -fun fact_of_subproof ctxt proof = +fun fact_of_proof ctxt (Proof (Fix fixed_frees, Assume assms, steps)) = let - val (fixed_frees, assms, concl) = split_proof proof + val concl = (case try List.last steps of + SOME (Prove (_, _, t, _)) => t + | _ => error "preplay error: malformed subproof") val var_idx = maxidx_of_term concl + 1 fun var_of_free (x, T) = Var((x, var_idx), T) val substitutions = map (`var_of_free #> swap #> apfst Free) fixed_frees - val assms = assms |> map snd in - Logic.list_implies(assms, concl) + Logic.list_implies (assms |> map snd, concl) |> subst_free substitutions |> thm_of_term ctxt end @@ -78,7 +80,7 @@ (case step of Prove (_, _, t, By_Metis (subproofs, fact_names)) => (t, subproofs, fact_names, false) - | Obtain (_, xs, _, t, By_Metis (subproofs, fact_names)) => + | Obtain (_, Fix xs, _, t, By_Metis (subproofs, fact_names)) => (* proof obligation: !!thesis. (!!x. A x ==> thesis) ==> thesis (see ~~/src/Pure/Isar/obtain.ML) *) let @@ -98,7 +100,7 @@ end | _ => raise ZEROTIME) val facts = - map (fact_of_subproof ctxt) subproofs @ + map (fact_of_proof ctxt) subproofs @ resolve_fact_names ctxt fact_names val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug |> obtain ? Config.put Metis_Tactic.new_skolem true diff -r 06689dbfe072 -r 0d5f8812856f src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Mon Feb 18 12:16:02 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Mon Feb 18 12:16:27 2013 +0100 @@ -9,83 +9,84 @@ signature SLEDGEHAMMER_PROOF = sig type label = string * int - val no_label : label type facts = label list * string list - val no_facts : facts datatype isar_qualifier = Show | Then - datatype isar_step = - Fix of (string * typ) list | + datatype fix = Fix of (string * typ) list + datatype assms = Assume of (label * term) list + + datatype isar_proof = + Proof of fix * assms * isar_step list + and isar_step = 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 + Prove of isar_qualifier list * label * term * byline | + Obtain of isar_qualifier list * fix * label * term * byline and byline = - By_Metis of isar_step list list * facts + By_Metis of isar_proof list * facts + + val no_label : label + val no_facts : facts val string_for_label : label -> string - val metis_steps_top_level : isar_step list -> int - val metis_steps_total : isar_step list -> int - val term_of_assm : isar_step -> term - val term_of_prove : isar_step -> term - val split_proof : - isar_step list -> (string * typ) list * (label * term) list * term + val fix_of_proof : isar_proof -> fix + val assms_of_proof : isar_proof -> assms + val steps_of_proof : isar_proof -> isar_step list + + val label_of_step : isar_step -> label option + val byline_of_step : isar_step -> byline option + + val add_metis_steps_top_level : isar_step list -> int -> int + val add_metis_steps : isar_step list -> int -> int end structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF = struct type label = string * int -val no_label = ("", ~1) type facts = label list * string list -val no_facts = ([],[]) datatype isar_qualifier = Show | Then -datatype isar_step = - Fix of (string * typ) list | +datatype fix = Fix of (string * typ) list +datatype assms = Assume of (label * term) list + +datatype isar_proof = + Proof of fix * assms * isar_step list +and isar_step = 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 + Prove of isar_qualifier list * label * term * byline | + Obtain of isar_qualifier list * fix * label * term * byline and byline = - By_Metis of isar_step list list * facts + By_Metis of isar_proof list * facts + +val no_label = ("", ~1) +val no_facts = ([],[]) fun string_for_label (s, num) = s ^ string_of_int num -fun metis_steps_top_level proof = - fold (fn Obtain _ => Integer.add 1 | Prove _ => Integer.add 1 | _ => I) - proof 0 -fun metis_steps_total proof = - let - fun add_substeps subproofs i = - Integer.add (fold Integer.add (map metis_steps_total subproofs) i) - in - fold - (fn Obtain (_, _, _, _, By_Metis (subproofs, _)) => add_substeps subproofs 1 - | Prove (_, _, _, By_Metis (subproofs, _)) => add_substeps subproofs 1 - | _ => I) - proof 0 - end +fun fix_of_proof (Proof (fix, _, _)) = fix +fun assms_of_proof (Proof (_, assms, _)) = assms +fun steps_of_proof (Proof (_, _, steps)) = steps +(*fun map_steps_of_proof f (Proof (fix, assms, steps)) = + Proof(fix, assms, f steps)*) + +fun label_of_step (Obtain (_, _, l, _, _)) = SOME l + | label_of_step (Prove (_, l, _, _)) = SOME l + | label_of_step _ = NONE -fun term_of_assm (Assume (_, t)) = t - | term_of_assm _ = error "sledgehammer proof: unexpected constructor" -fun term_of_prove (Prove (_, _, t, _)) = t - | term_of_prove _ = error "sledgehammer proof: unexpected constructor" +fun byline_of_step (Obtain (_, _, _, _, byline)) = SOME byline + | byline_of_step (Prove (_, _, _, byline)) = SOME byline + | byline_of_step _ = NONE + +val add_metis_steps_top_level = + fold (byline_of_step #> (fn SOME (By_Metis _) => Integer.add 1 | _ => I)) -fun split_proof proof = - let - fun split_step step (fixes, assms, _) = - (case step of - Fix xs => (xs@fixes, assms, step) - | Assume a => (fixes, a::assms, step) - | _ => (fixes, assms, step)) - val (fixes, assms, concl) = - fold split_step proof ([], [], Let (Term.dummy, Term.dummy)) (* FIXME: hack *) - in - (rev fixes, rev assms, term_of_prove concl) - end +fun add_metis_steps steps = + fold (byline_of_step + #> (fn SOME (By_Metis (subproofs, _)) => + Integer.add 1 #> add_substeps subproofs + | _ => I)) steps +and add_substeps subproofs = fold (steps_of_proof #> add_metis_steps) subproofs end diff -r 06689dbfe072 -r 0d5f8812856f src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Feb 18 12:16:02 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Feb 18 12:16:27 2013 +0100 @@ -457,158 +457,190 @@ val indent_size = 2 -fun string_for_proof ctxt type_enc lam_trans i n = +fun string_for_proof ctxt type_enc lam_trans i n proof = let - fun maybe_show qs = if member (op =) qs Show then "show" else "have" + 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_free (s, T) = - maybe_quote s ^ " :: " ^ - maybe_quote (simplify_spaces (with_vanilla_print_mode - (Syntax.string_of_typ ctxt) T)) - val of_frees = space_implode " and " o map of_free - fun maybe_moreover ind qs nr_subproofs = - if member (op =) qs Then andalso nr_subproofs > 0 - then of_indent ind ^ "moreover\n" - else "" + fun of_moreover ind = of_indent ind ^ "moreover\n" fun of_label l = if l = no_label then "" else string_for_label l ^ ": " - fun of_have qs nr_subproofs = - if (member (op =) qs Then andalso nr_subproofs>0) orelse (nr_subproofs>1) - then "ultimately " ^ maybe_show qs - else - (if member (op =) qs Then orelse nr_subproofs>0 then - if member (op =) qs Show then "thus" else "hence" - else - maybe_show qs) - fun of_obtain qs xs = - (if member (op =) qs Then then "then " else "") ^ "obtain " ^ - of_frees xs ^ " where" - val of_term = - annotate_types ctxt - #> with_vanilla_print_mode (Syntax.string_of_term ctxt) - #> simplify_spaces - #> maybe_quote + 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_prove 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 ^ (annotate_types ctxt term + |> with_vanilla_print_mode (Syntax.string_of_term ctxt) + |> simplify_spaces + |> maybe_quote), + ctxt |> Variable.auto_fixes term) val reconstr = Metis (type_enc, lam_trans) fun of_metis ind options (ls, ss) = "\n" ^ of_indent (ind + 1) ^ options ^ reconstructor_command reconstr 1 1 [] 0 (ls |> sort_distinct (prod_ord string_ord int_ord), ss |> sort_distinct string_ord) - and of_step ind (Fix xs) = of_indent ind ^ "fix " ^ of_frees xs ^ "\n" - | of_step ind (Let (t1, t2)) = - of_indent ind ^ "let " ^ of_term t1 ^ " = " ^ of_term t2 ^ "\n" - | of_step ind (Assume (l, t)) = - of_indent ind ^ "assume " ^ of_label l ^ of_term t ^ "\n" - | of_step ind (Obtain (qs, xs, l, t, By_Metis (subproofs, facts))) = (* FIXME *) - maybe_moreover ind qs (length subproofs) ^ - of_subproofs ind subproofs ^ - of_indent ind ^ of_obtain qs xs ^ " " ^ - of_label l ^ of_term t ^ - (* The new skolemizer puts the arguments in the same order as the ATPs - (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding - Vampire). *) - of_metis ind "using [[metis_new_skolem]] " facts ^ "\n" - | of_step ind (Prove (qs, l, t, By_Metis (subproofs, facts))) = - maybe_moreover ind qs (length subproofs) ^ - of_subproofs ind subproofs ^ - of_prove ind qs (length subproofs) l t facts - and of_steps prefix suffix ind steps = - let val s = implode (map (of_step ind) steps) in + 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 options = + add_suffix (of_label l) + #> add_term t + #> add_suffix (of_metis ind options facts ^ "\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_block ind proof = of_steps "{ " " }" (ind + 1) proof - and of_subproofs ind subproofs = - subproofs - |> map (of_block ind) - |> space_implode (of_indent ind ^ "moreover\n") - and of_prove ind qs nr_subproofs l t facts = - of_indent ind ^ of_have qs nr_subproofs ^ " " ^ of_label l ^ of_term t ^ - of_metis ind "" facts ^ "\n" + 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, l, t, By_Metis (subproofs, facts))) = + add_step_pre ind qs subproofs + #> add_suffix (of_prove qs (length subproofs) ^ " ") + #> add_step_post ind l t facts "" + | add_step ind (Obtain (qs, Fix xs, l, t, + By_Metis (subproofs, facts))) = + add_step_pre ind qs subproofs + #> add_suffix (of_obtain qs (length subproofs) ^ " ") + #> add_frees xs + #> add_suffix " where " + (* The new skolemizer puts the arguments in the same order as the ATPs + (E and Vampire -- but see also "atp_proof_reconstruct.ML" regarding + Vampire). *) + #> add_step_post ind l t facts "using [[metis_new_skolem]] " + and add_steps ind steps = + fold (add_step ind) steps + and of_proof ind ctxt (Proof (Fix xs, Assume assms, steps)) = + ("", ctxt) + |> add_fix ind xs + |> add_assms ind assms + |> add_steps ind steps + |> fst + in (* One-step proofs are pointless; better use the Metis one-liner directly. *) - and of_proof [Prove (_, _, _, By_Metis ([], _))] = "" - | of_proof proof = - (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ - of_indent 0 ^ "proof -\n" ^ of_steps "" "" 1 proof ^ of_indent 0 ^ - (if n <> 1 then "next" else "qed") - in of_proof end + case proof of + Proof (Fix [], Assume [], [Prove (_, _, _, By_Metis ([], _))]) => "" + | _ => (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 -fun add_labels_of_step (Obtain (_, _, _, _, By_Metis (subproofs, (ls, _)))) = - union (op =) (add_labels_of_proofs subproofs ls) - | add_labels_of_step (Prove (_, _, _, By_Metis (subproofs, (ls, _)))) = - union (op =) (add_labels_of_proofs subproofs ls) - | add_labels_of_step _ = I -and add_labels_of_proof proof = fold add_labels_of_step proof +fun add_labels_of_step step = + (case byline_of_step step of + NONE => I + | SOME (By_Metis (subproofs, (ls, _))) => + union (op =) (add_labels_of_proofs subproofs ls)) +and add_labels_of_proof proof = fold add_labels_of_step (steps_of_proof proof) and add_labels_of_proofs proofs = fold add_labels_of_proof proofs fun kill_useless_labels_in_proof proof = let val used_ls = add_labels_of_proof 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_Metis (subproofs, facts))) = + fun do_assms (Assume assms) = Assume (map (apfst do_label) assms) + fun do_step (Obtain (qs, xs, l, t, By_Metis (subproofs, facts))) = Obtain (qs, xs, do_label l, t, By_Metis (map do_proof subproofs, facts)) | do_step (Prove (qs, l, t, By_Metis (subproofs, facts))) = Prove (qs, do_label l, t, By_Metis (map do_proof subproofs, facts)) | do_step step = step - and do_proof proof = map do_step proof + and do_proof (Proof (fix, assms, steps)) = + Proof (fix, do_assms assms, map do_step steps) in do_proof proof end fun prefix_for_depth n = replicate_string (n + 1) val relabel_proof = let - fun fresh_label depth (old as (l, subst, next_have)) = + fun fresh_label depth prefix (old as (l, subst, next)) = 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) + let val l' = (prefix_for_depth depth prefix, next) in + (l', (l, l') :: subst, next + 1) end fun do_facts subst = apfst (maps (the_list o AList.lookup (op =) subst)) - fun do_byline subst depth nexts (By_Metis (subproofs, facts)) = - By_Metis - (map (do_proof subst (depth + 1) (1, 1)) subproofs, 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) :: 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) :: - do_proof ((l, l') :: subst) depth (next_assum + 1, next_have) proof - end - | do_proof subst depth (nexts as (next_assum, next_have)) - (Obtain (qs, xs, l, t, by) :: proof) = + fun do_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 do_assms subst depth (Assume assms) = + fold_map (do_assm depth) assms (subst, 1) + |> apfst Assume + |> apsnd fst + fun do_steps _ _ _ [] = [] + | do_steps subst depth next (Obtain (qs, xs, l, t, by) :: steps) = let - val (l, subst, next_have) = (l, subst, next_have) |> fresh_label depth - val by = by |> do_byline subst depth nexts + val (l, subst, next) = + (l, subst, next) |> fresh_label depth have_prefix + val by = by |> do_byline subst depth in - Obtain (qs, xs, l, t, by) :: - do_proof subst depth (next_assum, next_have) proof + Obtain (qs, xs, l, t, by) :: do_steps subst depth next steps end - | do_proof subst depth (nexts as (next_assum, next_have)) - (Prove (qs, l, t, by) :: proof) = + | do_steps subst depth next (Prove (qs, l, t, by) :: steps) = let - val (l, subst, next_have) = (l, subst, next_have) |> fresh_label depth - val by = by |> do_byline subst depth nexts + val (l, subst, next) = + (l, subst, next) |> fresh_label depth have_prefix + val by = by |> do_byline subst depth in - Prove (qs, l, t, by) :: - do_proof subst depth (next_assum, next_have) proof + Prove (qs, l, t, by) :: do_steps subst depth next steps end - | do_proof subst depth nexts (step :: proof) = - step :: do_proof subst depth nexts proof - in do_proof [] 0 (1, 1) end + | do_steps subst depth next (step :: steps) = + step :: do_steps subst depth next steps + and do_proof subst depth (Proof (fix, assms, steps)) = + let val (assms, subst) = do_assms subst depth assms in + Proof (fix, assms, do_steps subst depth 1 steps) + end + and do_byline subst depth (By_Metis (subproofs, facts)) = + By_Metis (do_proofs subst depth subproofs, do_facts subst facts) + and do_proofs subst depth = map (do_proof subst (depth + 1)) + in do_proof [] 0 end val chain_direct_proof = let - fun label_of (Assume (l, _)) = SOME l - | label_of (Obtain (_, _, l, _, _)) = SOME l - | label_of (Prove (_, l, _, _)) = SOME l - | label_of _ = NONE fun do_qs_lfs NONE lfs = ([], lfs) | do_qs_lfs (SOME l0) lfs = if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) @@ -621,16 +653,18 @@ end | chain_step lbl (Prove (qs, l, t, By_Metis (subproofs, (lfs, gfs)))) = let val (qs', lfs) = do_qs_lfs lbl lfs in - Prove (qs' @ qs, l, t, - By_Metis (chain_proofs subproofs, (lfs, gfs))) + Prove (qs' @ qs, l, t, By_Metis (chain_proofs subproofs, (lfs, gfs))) end | chain_step _ step = step - and chain_proof _ [] = [] - | chain_proof (prev as SOME _) (i :: is) = - chain_step prev i :: chain_proof (label_of i) is - | chain_proof _ (i :: is) = i :: chain_proof (label_of i) is - and chain_proofs proofs = map (chain_proof NONE) proofs - in chain_proof NONE end + 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, Assume assms, steps)) = + Proof (fix, Assume 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 * bool * Time.time option * real * string Symtab.table @@ -676,7 +710,7 @@ (case resolve_conjecture ss of [j] => if j = length hyp_ts then NONE - else SOME (Assume (raw_label_for_name name, nth hyp_ts j)) + else SOME (raw_label_for_name name, nth hyp_ts j) | _ => NONE) | _ => NONE) fun dep_of_step (Definition_Step _) = NONE @@ -691,7 +725,7 @@ val steps = Symtab.empty |> fold (fn Definition_Step _ => I (* FIXME *) - | Inference_Step (name as (s, ss), role, t, rule, _) => + | Inference_Step (name as (s, _), role, t, rule, _) => Symtab.update_new (s, (rule, t |> (if is_clause_tainted [name] then s_maybe_not role @@ -705,7 +739,7 @@ | 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)] = + fun prop_of_clause [(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 steps s) @@ -722,22 +756,16 @@ | _ => fold (curry s_disj) lits @{term False} end |> HOLogic.mk_Trueprop |> close_form - fun isar_proof_of_direct_proof outer predecessor accum [] = - rev accum |> outer ? (append assms - #> not (null params) ? cons (Fix params)) - | isar_proof_of_direct_proof outer predecessor accum (inf :: infs) = - let - fun maybe_show outer c = - (outer andalso length c = 1 andalso subset (op =) (c, conjs)) - ? cons Show - fun do_rest lbl step = - isar_proof_of_direct_proof outer lbl (step :: accum) infs - 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 - in - case inf of - Have (gamma, c) => + fun isar_proof_of_direct_proof infs = + let + fun maybe_show outer c = + (outer andalso length c = 1 andalso subset (op =) (c, conjs)) + ? cons Show + 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 do_steps _ _ accum [] = rev accum + | do_steps outer _ accum (Have (gamma, c) :: infs) = let val l = label_of_clause c val t = prop_of_clause c @@ -745,7 +773,9 @@ By_Metis ([], (fold (add_fact_from_dependencies fact_names) gamma no_facts)) - fun prove outer = Prove (maybe_show outer c [], l, t, by) + fun prove by = Prove (maybe_show outer c [], l, t, by) + fun do_rest lbl step = + do_steps outer (SOME lbl) (step :: accum) infs in if is_clause_tainted c then case gamma of @@ -754,36 +784,40 @@ is_clause_tainted g then let val subproof = - Fix (skolems_of (prop_of_clause g)) :: rev accum + Proof (Fix (skolems_of (prop_of_clause g)), + Assume [], rev accum) in - isar_proof_of_direct_proof outer l - [Prove (maybe_show outer c [], - label_of_clause c, prop_of_clause c, - By_Metis ([subproof], no_facts))] [] + do_steps outer (SOME l) + [prove (By_Metis ([subproof], no_facts))] [] end else - do_rest l (prove outer) - | _ => do_rest l (prove outer) + do_rest l (prove by) + | _ => do_rest l (prove by) else if is_clause_skolemize_rule c then - do_rest l (Obtain ([], skolems_of t, l, t, by)) + do_rest l (Obtain ([], Fix (skolems_of t), l, t, by)) else - do_rest l (prove outer) + do_rest l (prove by) end - | Cases cases => + | do_steps outer predecessor accum (Cases cases :: infs) = let fun do_case (c, infs) = - Assume (label_of_clause c, prop_of_clause c) :: - isar_proof_of_direct_proof false no_label [] infs + do_proof false [] [(label_of_clause c, prop_of_clause c)] infs 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, By_Metis + (map do_case cases, (the_list predecessor, [])))) in - do_rest l - (Prove (maybe_show outer c [], - l, prop_of_clause c, - By_Metis (map do_case cases, ([predecessor], [])))) + do_steps outer (SOME l) (step :: accum) infs end - end + and do_proof outer fix assms infs = + Proof (Fix fix, Assume assms, do_steps outer NONE [] infs) + in + do_proof true params assms infs + end + val cleanup_labels_in_proof = chain_direct_proof #> kill_useless_labels_in_proof @@ -791,7 +825,7 @@ val (isar_proof, (preplay_fail, preplay_time)) = refute_graph |> redirect_graph axioms tainted bot - |> isar_proof_of_direct_proof true no_label [] + |> isar_proof_of_direct_proof |> (if not preplay andalso isar_compress <= 1.0 then rpair (false, (true, seconds 0.0)) else @@ -818,9 +852,11 @@ 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 + let + val num_steps = add_metis_steps (steps_of_proof isar_proof) 0 + in + [string_of_int num_steps ^ " step" ^ plural_s num_steps] + end else []) in