# HG changeset patch # User paulson # Date 1168362779 -3600 # Node ID 6c0702a960763598009bd7766297fc8d71415b23 # Parent aaf5b49c9ed9b68c483b61229472962beb57fb23 More compact proof reconstruction: lines having fewer than !min_deps dependences are folded into the rest of the proof. diff -r aaf5b49c9ed9 -r 6c0702a96076 src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Tue Jan 09 15:49:39 2007 +0100 +++ b/src/HOL/Tools/res_reconstruct.ML Tue Jan 09 18:12:59 2007 +0100 @@ -33,6 +33,8 @@ (*Full proof reconstruction wanted*) val full = ref true; +val min_deps = ref 2; (*consolidate proof lines containing fewer dependencies*) + (**** PARSING OF TSTP FORMAT ****) (*Syntax trees, either termlist or formulae*) @@ -373,23 +375,32 @@ Consolidate adjacent lines that prove the same clause, since they differ only in type information.*) fun add_prfline ((lno, "axiom", t, []), lines) = (*axioms are not proof lines*) - if eq_false t then lines (*must be clsrel/clsarity: type information*) + if eq_false t (*must be clsrel/clsarity: type information, so delete refs to it*) + then map (replace_deps (lno, [])) lines else (case take_prefix (notequal t) lines of - (_,[]) => lines (*no repetition of proof line*) - | (pre, (lno',t',deps')::post) => + (_,[]) => lines (*no repetition of proof line*) + | (pre, (lno',t',deps')::post) => (*repetition: replace later line by earlier one*) pre @ map (replace_deps (lno', [lno])) post) | add_prfline ((lno, role, t, []), lines) = (*no deps: conjecture clause*) - if eq_false t then lines (*must be tfree_tcs: type information*) + if eq_false t (*must be tfree_tcs: type information, so delete refs to it*) + then map (replace_deps (lno, [])) lines else (lno, t, []) :: lines | add_prfline ((lno, role, t, deps), lines) = - (case term_tvars t of (*Delete line if it has TVars: they are forbidden in goals*) - _::_ => map (replace_deps (lno, deps)) lines - | [] => - case take_prefix (notequal t) lines of - (_,[]) => (lno, t, deps) :: lines (*no repetition of proof line*) - | (pre, (lno',t',deps')::post) => - (lno, t', deps) :: (*replace later line by earlier one*) - (pre @ map (replace_deps (lno', [lno])) post)); + case take_prefix (notequal t) lines of + (_,[]) => (lno, t, deps) :: lines (*no repetition of proof line*) + | (pre, (lno',t',deps')::post) => + (lno, t', deps) :: (*repetition: replace later line by earlier one*) + (pre @ map (replace_deps (lno', [lno])) post); + +(*TVars are forbidden in goals. Also, we don't want lines with too few dependencies. + Deleted lines are replaced by their own dependencies. Note that the previous "add_prfline" + phase may delete some dependencies, hence this phase comes later.*) +fun add_wanted_prfline ((lno, t, []), lines) = + (lno, t, []) :: lines (*conjecture clauses must be kept*) + | add_wanted_prfline ((lno, t, deps), lines) = + if not (null (term_tvars t)) orelse length deps < !min_deps + then map (replace_deps (lno, deps)) lines (*Delete line*) + else (lno, t, deps) :: lines; (*Replace numeric proof lines by strings, either from thm_names or sequential line numbers*) fun stringify_deps thm_names deps_map [] = [] @@ -411,7 +422,8 @@ fun decode_tstp_file cnfs ctxt th sgno thm_names = let val tuples = map (dest_tstp o tstp_line o explode) cnfs - val lines = foldr add_prfline [] (decode_tstp_list ctxt tuples) + val lines = foldr add_wanted_prfline [] + (foldr add_prfline [] (decode_tstp_list ctxt tuples)) val (ccls,fixes) = ResAxioms.neg_conjecture_clauses th sgno val ccls = map forall_intr_vars ccls in