# HG changeset patch # User blanchet # Date 1361366477 -3600 # Node ID f176855a1ee2ba095d2988f7f8acaaaba40681c7 # Parent 260cb10aac4bb2208a87901436adc60a994cacc3 tuning (removed redundant datatype) diff -r 260cb10aac4b -r f176855a1ee2 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Wed Feb 20 14:10:51 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Feb 20 14:21:17 2013 +0100 @@ -36,9 +36,7 @@ UnknownError of string type step_name = string * string list - - datatype 'a step = - Inference_Step of step_name * formula_role * 'a * string * step_name list + type 'a step = step_name * formula_role * 'a * string * step_name list type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list @@ -209,13 +207,10 @@ | (SOME i, SOME j) => int_ord (i, j) end -datatype 'a step = - Inference_Step of step_name * formula_role * 'a * string * step_name list +type 'a step = step_name * formula_role * 'a * string * step_name list type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list -fun step_name (Inference_Step (name, _, _, _, _)) = name - (**** PARSING OF TSTP FORMAT ****) (* Strings enclosed in single quotes (e.g., file names) *) @@ -418,16 +413,14 @@ phi), "", []) | Inference_Source (rule, deps) => (((num, []), phi), rule, deps) fun mk_step () = - Inference_Step (name, role_of_tptp_string role, phi, rule, - map (rpair []) deps) + (name, role_of_tptp_string role, phi, rule, map (rpair []) deps) in case role_of_tptp_string role of Definition => (case phi of AAtom (ATerm (("equal", []), _)) => (* Vampire's equality proxy axiom *) - Inference_Step (name, Definition, phi, rule, - map (rpair []) deps) + (name, Definition, phi, rule, map (rpair []) deps) | _ => mk_step ()) | _ => mk_step () end) @@ -473,8 +466,7 @@ -- Scan.option (Scan.this_string "derived from formulae " |-- Scan.repeat (scan_general_id --| Scan.option ($$ " "))) >> (fn ((((num, rule), deps), u), names) => - Inference_Step ((num, these names), Unknown, u, rule, - map (rpair []) deps))) x + ((num, these names), Unknown, u, rule, map (rpair []) deps))) x val satallax_coreN = "__satallax_core" (* arbitrary *) val z3_tptp_coreN = "__z3_tptp_core" (* arbitrary *) @@ -483,14 +475,12 @@ fun parse_z3_tptp_line x = (scan_general_id --| $$ "," --| $$ "[" -- parse_dependencies --| $$ "]" >> (fn (name, names) => - Inference_Step (("", name :: names), Unknown, dummy_phi, - z3_tptp_coreN, []))) x + (("", name :: names), Unknown, dummy_phi, z3_tptp_coreN, []))) x (* Syntax: *) fun parse_satallax_line x = (scan_general_id --| Scan.option ($$ " ") - >> (fn s => Inference_Step ((s, [s]), Unknown, dummy_phi, satallax_coreN, - []))) x + >> (fn s => ((s, [s]), Unknown, dummy_phi, satallax_coreN, []))) x fun parse_line problem = parse_tstp_line problem || parse_spass_line || parse_z3_tptp_line @@ -507,13 +497,12 @@ | atp_proof_from_tstplike_proof problem tstp = tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) |> parse_proof problem - |> sort (step_name_ord o pairself step_name) + |> sort (step_name_ord o pairself #1) fun clean_up_dependencies _ [] = [] - | clean_up_dependencies seen - (Inference_Step (name, role, u, rule, deps) :: steps) = - Inference_Step (name, role, u, rule, - map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) :: + | clean_up_dependencies seen ((name, role, u, rule, deps) :: steps) = + (name, role, u, rule, + map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) :: clean_up_dependencies (name :: seen) steps fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof @@ -525,8 +514,8 @@ AQuant (q, map (apfst f) xs, do_formula phi) | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis) | do_formula (AAtom t) = AAtom (do_term t) - fun do_step (Inference_Step (name, role, phi, rule, deps)) = - Inference_Step (name, role, do_formula phi, rule, deps) + fun do_step (name, role, phi, rule, deps) = + (name, role, do_formula phi, rule, deps) in map do_step end fun nasty_name pool s = s |> Symtab.lookup pool |> the_default s diff -r 260cb10aac4b -r f176855a1ee2 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Feb 20 14:10:51 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Feb 20 14:21:17 2013 +0100 @@ -119,8 +119,7 @@ val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix) fun is_axiom_used_in_proof pred = - exists (fn Inference_Step ((_, ss), _, _, _, []) => exists pred ss - | _ => false) + exists (fn ((_, ss), _, _, _, []) => exists pred ss) fun lam_trans_from_atp_proof atp_proof default = case (is_axiom_used_in_proof is_combinator_def atp_proof, @@ -155,7 +154,7 @@ 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)) = +fun add_fact ctxt fact_names ((_, ss), _, _, rule, deps) = (if rule = leo2_extcnf_equal_neg_rule then insert (op =) (ext_name ctxt, (Global, General)) else if rule = leo2_unfold_def_rule then @@ -322,13 +321,13 @@ | aux t = t in aux end -fun decode_line sym_tab (Inference_Step (name, role, u, rule, deps)) ctxt = +fun decode_line sym_tab (name, role, u, rule, deps) ctxt = let val thy = Proof_Context.theory_of ctxt val t = u |> prop_from_atp ctxt true sym_tab |> uncombine_term thy |> infer_formula_types ctxt in - (Inference_Step (name, role, t, rule, deps), + ((name, role, t, rule, deps), fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt) end fun decode_lines ctxt sym_tab lines = @@ -336,10 +335,8 @@ fun replace_one_dependency (old, new) dep = if is_same_atp_step dep old then new else [dep] -fun replace_dependencies_in_line p - (Inference_Step (name, role, t, rule, deps)) = - Inference_Step (name, role, t, rule, - fold (union (op =) o replace_one_dependency p) deps []) +fun replace_dependencies_in_line p (name, role, t, rule, deps) = + (name, role, t, rule, fold (union (op =) o replace_one_dependency p) deps []) (* No "real" literals means only type information (tfree_tcs, clsrel, or clsarity). *) @@ -347,17 +344,16 @@ fun s_maybe_not role = role <> Conjecture ? s_not -fun is_same_inference (role, t) (Inference_Step (_, role', t', _, _)) = - s_maybe_not role t aconv s_maybe_not role' t' +fun is_same_inference (role, t) (_, role', t', _, _) = + s_maybe_not role t aconv s_maybe_not role' t' (* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in type information.*) -fun add_line fact_names (Inference_Step (name as (_, ss), role, t, rule, [])) - lines = +fun add_line fact_names (name as (_, ss), role, t, rule, []) lines = (* No dependencies: fact, conjecture, or (for Vampire) internal facts or definitions. *) if is_conjecture ss then - Inference_Step (name, role, t, rule, []) :: lines + (name, role, t, rule, []) :: lines else if is_fact fact_names ss then (* Facts are not proof lines. *) if is_only_type_information t then @@ -366,30 +362,30 @@ lines else map (replace_dependencies_in_line (name, [])) lines - | add_line _ (line as Inference_Step (name, role, t, _, _)) lines = + | add_line _ (line as (name, role, t, _, _)) lines = (* Type information will be deleted later; skip repetition test. *) if is_only_type_information t then line :: lines (* Is there a repetition? If so, replace later line by earlier one. *) else case take_prefix (not o is_same_inference (role, t)) lines of (_, []) => line :: lines - | (pre, Inference_Step (name', _, _, _, _) :: post) => + | (pre, (name', _, _, _, _) :: post) => line :: pre @ map (replace_dependencies_in_line (name', [name])) post val waldmeister_conjecture_num = "1.0.0.0" val repair_waldmeister_endgame = let - fun do_tail (Inference_Step (name, _, t, rule, deps)) = - Inference_Step (name, Negated_Conjecture, s_not t, rule, deps) + fun do_tail (name, _, t, rule, deps) = + (name, Negated_Conjecture, s_not t, rule, deps) fun do_body [] = [] - | do_body ((line as Inference_Step ((num, _), _, _, _, _)) :: lines) = + | do_body ((line as ((num, _), _, _, _, _)) :: lines) = if num = waldmeister_conjecture_num then map do_tail (line :: lines) else line :: do_body lines in do_body end (* Recursively delete empty lines (type information) from the proof. *) -fun add_nontrivial_line (line as Inference_Step (name, _, t, _, [])) lines = +fun add_nontrivial_line (line as (name, _, t, _, [])) lines = if is_only_type_information t then delete_dependency name lines else line :: lines | add_nontrivial_line line lines = line :: lines @@ -408,8 +404,8 @@ val is_skolemize_rule = member (op =) [e_skolemize_rule, vampire_skolemisation_rule] -fun add_desired_line fact_names frees - (Inference_Step (name as (_, ss), role, t, rule, deps)) (j, lines) = +fun add_desired_line fact_names frees (name as (_, ss), role, t, rule, deps) + (j, lines) = (j + 1, if is_fact fact_names ss orelse is_conjecture ss orelse @@ -422,7 +418,7 @@ length deps >= 2 andalso (* kill next to last line, which usually results in a trivial step *) j <> 1) then - Inference_Step (name, role, t, rule, deps) :: lines (* keep line *) + (name, role, t, rule, deps) :: lines (* keep line *) else map (replace_dependencies_in_line (name, deps)) lines) (* drop line *) @@ -669,20 +665,19 @@ val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts) val conjs = atp_proof |> map_filter - (fn Inference_Step (name as (_, ss), _, _, _, []) => + (fn (name as (_, ss), _, _, _, []) => if member (op =) ss conj_name then SOME name else NONE | _ => NONE) val assms = atp_proof |> map_filter - (fn Inference_Step (name as (_, ss), _, _, _, []) => + (fn (name as (_, ss), _, _, _, []) => (case resolve_conjecture ss of [j] => if j = length hyp_ts then NONE else SOME (raw_label_for_name name, nth hyp_ts j) | _ => NONE) | _ => NONE) - fun dep_of_step (Inference_Step (name, _, _, _, from)) = - SOME (from, name) + fun dep_of_step (name, _, _, _, from) = SOME (from, name) val refute_graph = atp_proof |> map_filter dep_of_step |> make_refute_graph val axioms = axioms_of_refute_graph refute_graph conjs @@ -691,7 +686,7 @@ val bot = atp_proof |> List.last |> dep_of_step |> the |> snd val steps = Symtab.empty - |> fold (fn Inference_Step (name as (s, _), role, t, rule, _) => + |> fold (fn (name as (s, _), role, t, rule, _) => Symtab.update_new (s, (rule, t |> (if is_clause_tainted [name] then s_maybe_not role