# HG changeset patch # User blanchet # Date 1384886184 -3600 # Node ID d023838eb2529463bbc4f2bdf5818c263a0de8b7 # Parent 096f7d45216479a300afd98f63978ce84e2f605c more refactoring to accommodate SMT proofs diff -r 096f7d452164 -r d023838eb252 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Nov 19 18:38:25 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Nov 19 19:36:24 2013 +0100 @@ -36,12 +36,6 @@ Proof.context -> bool -> int Symtab.table -> (string, string, (string, string) atp_term, string) atp_formula -> term - (* FIXME: eliminate *) - val resolve_fact : (string * 'a) list vector -> string list -> (string * 'a) list - val resolve_conjecture : string list -> int list - val is_fact : (string * 'a) list vector -> string list -> bool - val is_conjecture : string list -> bool - val used_facts_in_atp_proof : Proof.context -> (string * stature) list vector -> string atp_proof -> (string * stature) list @@ -50,9 +44,10 @@ string list option val lam_trans_of_atp_proof : string atp_proof -> string -> string val is_typed_helper_used_in_atp_proof : string atp_proof -> bool - val termify_atp_proof : - Proof.context -> string Symtab.table -> (string * term) list -> + val termify_atp_proof : Proof.context -> string Symtab.table -> (string * term) list -> int Symtab.table -> string atp_proof -> (term, string) atp_step list + val factify_atp_proof : (string * 'a) list vector -> term list -> term -> + (term, string) atp_step list -> (term, string) atp_step list end; structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT = @@ -538,4 +533,28 @@ #> map (decode_line ctxt lifted sym_tab) #> repair_waldmeister_endgame +fun factify_atp_proof fact_names hyp_ts concl_t atp_proof = + let + fun factify_step ((num, ss), role, t, rule, deps) = + let + val (ss', role', t') = + (case resolve_conjecture ss of + [j] => + if j = length hyp_ts then ([], Conjecture, concl_t) else ([], Hypothesis, nth hyp_ts j) + | _ => + (case resolve_fact fact_names ss of + [] => (ss, Plain, t) + | facts => (map fst facts, Axiom, t))) + in + ((num, ss'), role', t', rule, deps) + end + + val atp_proof = map factify_step atp_proof + val names = map #1 atp_proof + + fun repair_dep (num, ss) = (num, the_default ss (AList.lookup (op =) names num)) + fun repair_deps (name, role, t, rule, deps) = (name, role, t, rule, map repair_dep deps) + + in map repair_deps atp_proof end + end; diff -r 096f7d452164 -r d023838eb252 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Nov 19 18:38:25 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Nov 19 19:36:24 2013 +0100 @@ -844,10 +844,13 @@ if is_typed_helper_used_in_atp_proof atp_proof then full_typesN else partial_typesN val metis_lam_trans = lam_trans_of_atp_proof atp_proof default_metis_lam_trans - val atp_proof = atp_proof |> termify_atp_proof ctxt pool lifted sym_tab + val atp_proof = + atp_proof + |> termify_atp_proof ctxt pool lifted sym_tab + |> factify_atp_proof fact_names hyp_ts concl_t in (debug, verbose, metis_type_enc, metis_lam_trans, preplay_timeout, - isar_compress, isar_try0, fact_names, atp_proof, goal) + isar_compress, isar_try0, atp_proof, goal) end val one_line_params = (preplay, proof_banner mode name, used_facts, diff -r 096f7d452164 -r d023838eb252 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Nov 19 18:38:25 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Nov 19 19:36:24 2013 +0100 @@ -13,8 +13,8 @@ type one_line_params = Sledgehammer_Reconstructor.one_line_params type isar_params = - bool * bool * string * string * Time.time option * real * bool * (string * stature) list vector - * (term, string) atp_step list * thm + bool * bool * string * string * Time.time option * real * bool * (term, string) atp_step list * + thm val isar_proof_text : Proof.context -> bool option -> isar_params -> one_line_params -> string @@ -52,13 +52,8 @@ fun label_of_clause [(num, _)] = raw_label_of_num num | label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0) -fun add_fact_of_dependencies fact_names (names as [(_, ss)]) = - if is_fact fact_names ss then - apsnd (union (op =) (map fst (resolve_fact fact_names ss))) - else - apfst (insert (op =) (label_of_clause names)) - | add_fact_of_dependencies _ names = - apfst (insert (op =) (label_of_clause names)) +fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss) + | add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names)) fun replace_one_dependency (old, new) dep = if is_same_atp_step dep old then new else [dep] @@ -76,12 +71,12 @@ (* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in type information.*) -fun add_line fact_names (name as (_, ss), role, t, rule, []) lines = +fun add_line (name as (_, ss), role, t, rule, []) lines = (* No dependencies: fact, conjecture, or (for Vampire) internal facts or definitions. *) - if is_conjecture ss then + if role = Conjecture orelse role = Hypothesis then (name, role, t, rule, []) :: lines - else if is_fact fact_names ss then + else if role = Axiom then (* Facts are not proof lines. *) if is_only_type_information t then map (replace_dependencies_in_line (name, [])) lines @@ -89,7 +84,7 @@ lines else map (replace_dependencies_in_line (name, [])) lines - | add_line _ (line as (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 @@ -114,12 +109,9 @@ val is_skolemize_rule = member (op =) [e_skolemize_rule, vampire_skolemisation_rule] -fun add_desired_line fact_names (name as (_, ss), role, t, rule, deps) - (j, lines) = +fun add_desired_line (name as (_, ss), role, t, rule, deps) (j, lines) = (j + 1, - if is_fact fact_names ss orelse - is_conjecture ss orelse - is_skolemize_rule rule orelse + if role <> Plain orelse is_skolemize_rule rule orelse (* the last line must be kept *) j = 0 orelse (not (is_only_type_information t) andalso @@ -217,13 +209,15 @@ and chain_proofs proofs = map (chain_proof) proofs in chain_proof end +fun maybe_mk_Trueprop t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop + type isar_params = - bool * bool * string * string * Time.time option * real * bool * (string * stature) list vector - * (term, string) atp_step list * thm + bool * bool * string * string * Time.time option * real * bool * (term, string) atp_step list * + thm fun isar_proof_text ctxt isar_proofs (debug, verbose, metis_type_enc, metis_lam_trans, preplay_timeout, isar_compress, - isar_try0, fact_names, atp_proof, goal) + isar_try0, atp_proof, goal) (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = let val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt @@ -240,26 +234,15 @@ let val atp_proof = atp_proof - |> rpair [] |-> fold_rev (add_line fact_names) + |> rpair [] |-> fold_rev add_line |> rpair [] |-> fold_rev add_nontrivial_line |> rpair (0, []) - |-> fold_rev (add_desired_line fact_names) + |-> fold_rev add_desired_line |> snd - val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts) - val conjs = - atp_proof |> map_filter - (fn (name as (_, ss), _, _, _, []) => - if member (op =) ss conj_name then SOME name else NONE - | _ => NONE) + val conjs = atp_proof |> map_filter (try (fn (name, Conjecture, _, _, []) => name)) val assms = - atp_proof |> map_filter - (fn ((num, ss), _, _, _, []) => - (case resolve_conjecture ss of - [j] => - if j = length hyp_ts then NONE - else SOME (raw_label_of_num num, nth hyp_ts j) - | _ => NONE) - | _ => NONE) + atp_proof + |> map_filter (try (fn ((num, _), Hypothesis, t, _, []) => (raw_label_of_num num, t))) val bot = atp_proof |> List.last |> #1 val refute_graph = atp_proof @@ -280,16 +263,12 @@ I)))) atp_proof fun is_clause_skolemize_rule [(s, _)] = - Option.map (is_skolemize_rule o fst) (Symtab.lookup steps s) = - SOME true + 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 [(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) - |> snd |> HOLogic.mk_Trueprop |> close_form) + fun prop_of_clause [(num, _)] = + Symtab.lookup steps num |> the |> snd |> maybe_mk_Trueprop |> close_form | prop_of_clause names = let val lits = map snd (map_filter (Symtab.lookup steps o fst) names) @@ -320,7 +299,7 @@ let val l = label_of_clause c val t = prop_of_clause c - val by = By ((fold (add_fact_of_dependencies fact_names) gamma no_facts), MetisM) + val by = By (fold add_fact_of_dependencies gamma no_facts, MetisM) fun prove sub by = Prove (maybe_show outer c [], Fix [], l, t, sub, by) fun do_rest l step = do_steps outer (SOME l) (step :: accum) infs in