# HG changeset patch # User blanchet # Date 1319053232 -7200 # Node ID 0e5e56e32bc07fb6efd630a9b233d8a095e8336c # Parent 9a00f9cc87072dfa127de0ed0bc7ee4501998e42 cleaner LEO-II extensionality step detection diff -r 9a00f9cc8707 -r 0e5e56e32bc0 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Wed Oct 19 21:40:32 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Oct 19 21:40:32 2011 +0200 @@ -39,7 +39,7 @@ datatype 'a step = Definition of step_name * 'a * 'a | - Inference of step_name * 'a * step_name list + Inference of step_name * 'a * string * step_name list type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list @@ -223,12 +223,12 @@ datatype 'a step = Definition of step_name * 'a * 'a | - Inference of step_name * 'a * step_name list + Inference of step_name * 'a * string * step_name list type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list fun step_name (Definition (name, _, _)) = name - | step_name (Inference (name, _, _)) = name + | step_name (Inference (name, _, _, _)) = name (**** PARSING OF TSTP FORMAT ****) @@ -264,7 +264,7 @@ datatype source = File_Source of string * string option | - Inference_Source of string list + Inference_Source of string * string list fun parse_dependencies x = (scan_general_id ::: Scan.repeat ($$ "," |-- scan_general_id)) x @@ -273,10 +273,9 @@ (Scan.this_string "file" |-- $$ "(" |-- scan_general_id -- Scan.option ($$ "," |-- scan_general_id) --| $$ ")" >> File_Source - || (Scan.this_string "inference" |-- $$ "(" |-- scan_general_id - --| skip_formula --| $$ ",") - ::: (skip_formula |-- $$ "," |-- $$ "[" |-- parse_dependencies --| $$ "]" - --| $$ ")") + || Scan.this_string "inference" |-- $$ "(" |-- scan_general_id + --| skip_formula --| $$ "," --| skip_formula --| $$ "," --| $$ "[" + -- parse_dependencies --| $$ "]" --| $$ ")" >> Inference_Source) x fun list_app (f, args) = @@ -348,7 +347,7 @@ val parse_tstp_extra_arguments = Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_formula)) - (Inference_Source []) + (Inference_Source ("", [])) val waldmeister_conjecture = "conjecture_1" @@ -404,7 +403,7 @@ --| $$ "." >> (fn (((num, role), phi), deps) => let - val (name, deps) = + val (name, rule, deps) = (* Waldmeister isn't exactly helping. *) case deps of File_Source (_, SOME s) => @@ -412,11 +411,11 @@ if s = waldmeister_conjecture then find_formula_in_problem problem (mk_anot phi) else - SOME [s |> perhaps (try (unprefix tofof_fact_prefix))]), + SOME [s |> perhaps (try (unprefix tofof_fact_prefix))]), "", []) | File_Source _ => - ((num, find_formula_in_problem problem phi), []) - | Inference_Source deps => ((num, NONE), deps) + ((num, find_formula_in_problem problem phi), "", []) + | Inference_Source (rule, deps) => ((num, NONE), rule, deps) in case role of "definition" => @@ -425,9 +424,9 @@ Definition (name, phi1, phi2) | AAtom (ATerm ("equal", _)) => (* Vampire's equality proxy axiom *) - Inference (name, phi, map (rpair NONE) deps) + Inference (name, phi, rule, map (rpair NONE) deps) | _ => raise UNRECOGNIZED_ATP_PROOF ()) - | _ => Inference (name, phi, map (rpair NONE) deps) + | _ => Inference (name, phi, rule, map (rpair NONE) deps) end) (**** PARSING OF SPASS OUTPUT ****) @@ -468,16 +467,16 @@ (* Syntax: [0:] || -> . *) fun parse_spass_line spass_names = - scan_general_id --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id + scan_general_id --| $$ "[" --| $$ "0" --| $$ ":" -- Symbol.scan_id -- parse_spass_annotations --| $$ "]" -- parse_horn_clause --| $$ "." - >> (fn ((num, deps), u) => - Inference ((num, resolve_spass_num spass_names num), u, + >> (fn (((num, rule), deps), u) => + Inference ((num, resolve_spass_num spass_names num), u, rule, map (swap o `(resolve_spass_num spass_names)) deps)) (* Syntax: *) fun parse_satallax_line x = (scan_general_id --| Scan.option ($$ " ") - >> (fn s => Inference ((s, SOME [s]), dummy_phi, []))) x + >> (fn s => Inference ((s, SOME [s]), dummy_phi, "", []))) x fun parse_line problem spass_names = parse_tstp_line problem || parse_spass_line spass_names || parse_satallax_line @@ -540,8 +539,8 @@ fun clean_up_dependencies _ [] = [] | clean_up_dependencies seen ((step as Definition (name, _, _)) :: steps) = step :: clean_up_dependencies (name :: seen) steps - | clean_up_dependencies seen (Inference (name, u, deps) :: steps) = - Inference (name, u, + | clean_up_dependencies seen (Inference (name, u, rule, deps) :: steps) = + Inference (name, u, rule, map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) :: clean_up_dependencies (name :: seen) steps @@ -558,8 +557,8 @@ fun map_term_names_in_step f (Definition (name, phi1, phi2)) = Definition (name, map_term_names_in_formula f phi1, map_term_names_in_formula f phi2) - | map_term_names_in_step f (Inference (name, phi, deps)) = - Inference (name, map_term_names_in_formula f phi, deps) + | map_term_names_in_step f (Inference (name, phi, rule, deps)) = + Inference (name, map_term_names_in_formula f phi, rule, deps) fun map_term_names_in_atp_proof f = map (map_term_names_in_step f) fun nasty_name pool s = s |> Symtab.lookup pool |> the_default s diff -r 9a00f9cc8707 -r 0e5e56e32bc0 src/HOL/Tools/ATP/atp_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Oct 19 21:40:32 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML Wed Oct 19 21:40:32 2011 +0200 @@ -148,13 +148,10 @@ else isa_ext -fun add_fact _ facts_offset fact_names (Inference (name, _, [])) = +fun add_fact _ facts_offset fact_names (Inference (name, _, _, [])) = union (op =) (resolve_fact facts_offset fact_names name) - | add_fact ctxt _ _ (Inference (_, _, deps)) = - if AList.defined (op =) deps leo2_ext then - insert (op =) (ext_name ctxt, General) - else - I + | add_fact ctxt _ _ (Inference (_, _, rule, _)) = + if rule = leo2_ext then insert (op =) (ext_name ctxt, General) else I | add_fact _ _ _ _ = I fun used_facts_in_atp_proof ctxt facts_offset fact_names atp_proof = @@ -162,7 +159,7 @@ else fold (add_fact ctxt facts_offset fact_names) atp_proof [] fun is_conjecture_used_in_proof conjecture_shape = - exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name + exists (fn Inference (name, _, _, []) => is_conjecture conjecture_shape name | _ => false) (* (quasi-)underapproximation of the truth *) @@ -186,7 +183,7 @@ end fun uses_typed_helpers typed_helpers = - exists (fn Inference (name, _, []) => is_typed_helper typed_helpers name + exists (fn Inference (name, _, _, []) => is_typed_helper typed_helpers name | _ => false) @@ -558,16 +555,16 @@ (Definition (name, t1, t2), fold Variable.declare_term (maps Misc_Legacy.term_frees [t1, t2]) ctxt) end - | decode_line sym_tab (Inference (name, u, deps)) ctxt = + | decode_line sym_tab (Inference (name, u, rule, deps)) ctxt = let val t = u |> uncombined_etc_prop_from_atp ctxt true sym_tab in - (Inference (name, t, deps), + (Inference (name, t, rule, deps), fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt) end fun decode_lines ctxt sym_tab lines = fst (fold_map (decode_line sym_tab) lines ctxt) fun is_same_inference _ (Definition _) = false - | is_same_inference t (Inference (_, t', _)) = t aconv t' + | is_same_inference t (Inference (_, t', _, _)) = t aconv t' (* No "real" literals means only type information (tfree_tcs, clsrel, or clsarity). *) @@ -576,13 +573,14 @@ fun replace_one_dependency (old, new) dep = if is_same_atp_step dep old then new else [dep] fun replace_dependencies_in_line _ (line as Definition _) = line - | replace_dependencies_in_line p (Inference (name, t, deps)) = - Inference (name, t, fold (union (op =) o replace_one_dependency p) deps []) + | replace_dependencies_in_line p (Inference (name, t, rule, deps)) = + Inference (name, t, rule, + fold (union (op =) o replace_one_dependency p) deps []) (* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in type information.*) fun add_line _ _ (line as Definition _) lines = line :: lines - | add_line conjecture_shape fact_names (Inference (name, t, [])) lines = + | add_line conjecture_shape fact_names (Inference (name, t, rule, [])) lines = (* No dependencies: fact, conjecture, or (for Vampire) internal facts or definitions. *) if is_fact fact_names name then @@ -592,31 +590,31 @@ (* Is there a repetition? If so, replace later line by earlier one. *) else case take_prefix (not o is_same_inference t) lines of (_, []) => lines (* no repetition of proof line *) - | (pre, Inference (name', _, _) :: post) => + | (pre, Inference (name', _, _, _) :: post) => pre @ map (replace_dependencies_in_line (name', [name])) post | _ => raise Fail "unexpected inference" else if is_conjecture conjecture_shape name then - Inference (name, s_not t, []) :: lines + Inference (name, s_not t, rule, []) :: lines else map (replace_dependencies_in_line (name, [])) lines - | add_line _ _ (Inference (name, t, deps)) lines = + | add_line _ _ (Inference (name, t, rule, deps)) lines = (* Type information will be deleted later; skip repetition test. *) if is_only_type_information t then - Inference (name, t, deps) :: lines + Inference (name, t, rule, deps) :: 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 (name, t, deps) :: lines - | (pre, Inference (name', t', _) :: post) => - Inference (name, t', deps) :: + (_, []) => Inference (name, t, rule, deps) :: lines + | (pre, Inference (name', t', rule, _) :: post) => + Inference (name, t', rule, deps) :: pre @ map (replace_dependencies_in_line (name', [name])) post | _ => raise Fail "unexpected inference" (* Recursively delete empty lines (type information) from the proof. *) -fun add_nontrivial_line (Inference (name, t, [])) lines = +fun add_nontrivial_line (line as Inference (name, t, _, [])) lines = if is_only_type_information t then delete_dependency name lines - else Inference (name, t, []) :: lines + else line :: lines | add_nontrivial_line line lines = line :: lines and delete_dependency name lines = fold_rev add_nontrivial_line @@ -630,7 +628,7 @@ fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) = (j, line :: map (replace_dependencies_in_line (name, [])) lines) | add_desired_line isar_shrink_factor conjecture_shape fact_names frees - (Inference (name, t, deps)) (j, lines) = + (Inference (name, t, rule, deps)) (j, lines) = (j + 1, if is_fact fact_names name orelse is_conjecture conjecture_shape name orelse @@ -642,7 +640,7 @@ length deps >= 2 andalso j mod isar_shrink_factor = 0 andalso (* kill next to last line, which usually results in a trivial step *) j <> 1) then - Inference (name, t, deps) :: lines (* keep line *) + Inference (name, t, rule, deps) :: lines (* keep line *) else map (replace_dependencies_in_line (name, deps)) lines) (* drop line *) @@ -675,10 +673,10 @@ apfst (insert (op =) (raw_label_for_name conjecture_shape name)) fun step_for_line _ _ _ _ (Definition (_, t1, t2)) = Let (t1, t2) - | step_for_line conjecture_shape _ _ _ (Inference (name, t, [])) = + | step_for_line conjecture_shape _ _ _ (Inference (name, t, _, [])) = Assume (raw_label_for_name conjecture_shape name, t) | step_for_line conjecture_shape facts_offset fact_names j - (Inference (name, t, deps)) = + (Inference (name, t, _, deps)) = Have (if j = 1 then [Show] else [], raw_label_for_name conjecture_shape name, fold_rev forall_of (map Var (Term.add_vars t [])) t,