# HG changeset patch # User blanchet # Date 1384879055 -3600 # Node ID f625e0e79dd1d4af8a17180071445dd28bedb6d4 # Parent 319f8659267d0d711078586503ca5c1920aa5247 refactoring diff -r 319f8659267d -r f625e0e79dd1 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Nov 19 17:12:58 2013 +0100 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Nov 19 17:37:35 2013 +0100 @@ -665,7 +665,7 @@ SMT_Solver.smt_tac ctxt thms else if full then Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN] - ATP_Proof_Reconstruct.metis_default_lam_trans ctxt thms + ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms else if String.isPrefix "metis (" (!reconstructor) then let val (type_encs, lam_trans) = @@ -674,10 +674,10 @@ |> filter Token.is_proper |> tl |> Metis_Tactic.parse_metis_options |> fst |>> the_default [ATP_Proof_Reconstruct.partial_typesN] - ||> the_default ATP_Proof_Reconstruct.metis_default_lam_trans + ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end else if !reconstructor = "metis" then - Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.metis_default_lam_trans ctxt + Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms else K all_tac diff -r 319f8659267d -r f625e0e79dd1 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Nov 19 17:12:58 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Nov 19 17:37:35 2013 +0100 @@ -10,6 +10,7 @@ sig type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula + type stature = ATP_Problem_Generate.stature type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step type 'a atp_proof = 'a ATP_Proof.atp_proof @@ -23,7 +24,7 @@ val no_type_enc : string val full_type_encs : string list val partial_type_encs : string list - val metis_default_lam_trans : string + val default_metis_lam_trans : string val metis_call : string -> string -> string val forall_of : term -> term -> term val exists_of : term -> term -> term @@ -35,6 +36,18 @@ Proof.context -> bool -> int Symtab.table -> (string, string, (string, string) atp_term, string) atp_formula -> term + 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 + val used_facts_in_unsound_atp_proof : + Proof.context -> (string * stature) list vector -> 'a atp_proof -> + 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 -> int Symtab.table -> string atp_proof -> (term, string) atp_step list @@ -70,7 +83,7 @@ fun unalias_type_enc s = AList.lookup (op =) type_enc_aliases s |> the_default [s] -val metis_default_lam_trans = combsN +val default_metis_lam_trans = combsN fun metis_call type_enc lam_trans = let @@ -80,7 +93,7 @@ [alias] => alias | _ => type_enc val opts = [] |> type_enc <> partial_typesN ? cons type_enc - |> lam_trans <> metis_default_lam_trans ? cons lam_trans + |> lam_trans <> default_metis_lam_trans ? cons lam_trans in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s @@ -345,6 +358,108 @@ | _ => raise ATP_FORMULA [phi] in repair_tvar_sorts (do_formula true phi Vartab.empty) end +fun find_first_in_list_vector vec key = + Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key + | (_, value) => value) NONE vec + +val unprefix_fact_number = space_implode "_" o tl o space_explode "_" + +fun resolve_one_named_fact fact_names s = + case try (unprefix fact_prefix) s of + SOME s' => + let val s' = s' |> unprefix_fact_number |> unascii_of in + s' |> find_first_in_list_vector fact_names |> Option.map (pair s') + end + | NONE => NONE +fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names) +fun is_fact fact_names = not o null o resolve_fact fact_names + +fun resolve_one_named_conjecture s = + case try (unprefix conjecture_prefix) s of + SOME s' => Int.fromString s' + | NONE => NONE + +val resolve_conjecture = map_filter resolve_one_named_conjecture +val is_conjecture = not o null o resolve_conjecture + +fun is_axiom_used_in_proof pred = + exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false) + +fun add_non_rec_defs fact_names accum = + Vector.foldl (fn (facts, facts') => + union (op =) (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts) + facts') + accum fact_names + +val isa_ext = Thm.get_name_hint @{thm ext} +val isa_short_ext = Long_Name.base_name isa_ext + +fun ext_name ctxt = + if Thm.eq_thm_prop (@{thm ext}, + singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then + isa_short_ext + else + isa_ext + +val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg" +val leo2_unfold_def_rule = "unfold_def" + +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 + (* LEO 1.3.3 does not record definitions properly, leading to missing + dependencies in the TSTP proof. Remove the next line once this is + fixed. *) + add_non_rec_defs fact_names + else if rule = agsyhol_coreN orelse rule = satallax_coreN then + (fn [] => + (* agsyHOL and Satallax don't include definitions in their + unsatisfiable cores, so we assume the worst and include them all + here. *) + [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names + | facts => facts) + else + I) + #> (if null deps then union (op =) (resolve_fact fact_names ss) else I) + +fun used_facts_in_atp_proof ctxt fact_names atp_proof = + if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names + else fold (add_fact ctxt fact_names) atp_proof [] + +fun used_facts_in_unsound_atp_proof _ _ [] = NONE + | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof = + let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof in + if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso + not (is_axiom_used_in_proof (is_conjecture o single) atp_proof) then + SOME (map fst used_facts) + else + NONE + end + +val ascii_of_lam_fact_prefix = ascii_of lam_fact_prefix + +(* overapproximation (good enough) *) +fun is_lam_lifted s = + String.isPrefix fact_prefix s andalso + String.isSubstring ascii_of_lam_fact_prefix s + +val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix) + +fun lam_trans_of_atp_proof atp_proof default = + case (is_axiom_used_in_proof is_combinator_def atp_proof, + is_axiom_used_in_proof is_lam_lifted atp_proof) of + (false, false) => default + | (false, true) => liftingN +(* | (true, true) => combs_and_liftingN -- not supported by "metis" *) + | (true, _) => combsN + +val is_typed_helper_name = + String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix + +fun is_typed_helper_used_in_atp_proof atp_proof = + is_axiom_used_in_proof is_typed_helper_name atp_proof + fun repair_name "$true" = "c_True" | repair_name "$false" = "c_False" | repair_name "$$e" = tptp_equal (* seen in Vampire proofs *) diff -r 319f8659267d -r f625e0e79dd1 src/HOL/Tools/Metis/metis_tactic.ML --- a/src/HOL/Tools/Metis/metis_tactic.ML Tue Nov 19 17:12:58 2013 +0100 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Tue Nov 19 17:37:35 2013 +0100 @@ -294,7 +294,7 @@ () val (schem_facts, nonschem_facts) = List.partition has_tvar facts val type_encs = override_type_encs |> the_default default_type_encs - val lam_trans = lam_trans |> the_default metis_default_lam_trans + val lam_trans = lam_trans |> the_default default_metis_lam_trans in HEADGOAL (Method.insert_tac nonschem_facts THEN' CHANGED_PROP o generic_metis_tac type_encs lam_trans ctxt diff -r 319f8659267d -r f625e0e79dd1 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Nov 19 17:12:58 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Nov 19 17:37:35 2013 +0100 @@ -367,7 +367,7 @@ [] else [("type_enc", [hd (unalias_type_enc type_enc')])]) @ - (if is_none lam_trans andalso lam_trans' = metis_default_lam_trans then + (if is_none lam_trans andalso lam_trans' = default_metis_lam_trans then [] else [("lam_trans", [lam_trans'])]) @@ -820,7 +820,7 @@ bunch_of_reconstructors needs_full_types (lam_trans_of_atp_proof atp_proof o (fn desperate => if desperate then hide_lamsN - else metis_default_lam_trans)) + else default_metis_lam_trans)) in (used_facts, Lazy.lazy (fn () => @@ -838,19 +838,24 @@ Output.urgent_message "Generating proof text..." else () - val atp_proof = (fn () => termify_atp_proof ctxt pool lifted sym_tab atp_proof) - val isar_params = - (debug, verbose, preplay_timeout, isar_compress, isar_try0, fact_names, atp_proof, - goal) + fun isar_params () = + let + val metis_type_enc = + 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 + in + (debug, verbose, metis_type_enc, metis_lam_trans, preplay_timeout, + isar_compress, isar_try0, fact_names, atp_proof, goal) + end val one_line_params = (preplay, proof_banner mode name, used_facts, - choose_minimize_command ctxt params minimize_command name - preplay, + choose_minimize_command ctxt params minimize_command name preplay, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in - proof_text ctxt isar_proofs isar_params - num_chained one_line_params + proof_text ctxt isar_proofs isar_params num_chained one_line_params end, (if verbose then "\nATP real CPU time: " ^ string_of_time run_time ^ "." @@ -1048,7 +1053,7 @@ play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal SMT (bunch_of_reconstructors false (fn desperate => - if desperate then liftingN else metis_default_lam_trans))), + if desperate then liftingN else default_metis_lam_trans))), fn preplay => let val one_line_params = @@ -1082,7 +1087,7 @@ val reconstr = if name = metisN then Metis (type_enc |> the_default (hd partial_type_encs), - lam_trans |> the_default metis_default_lam_trans) + lam_trans |> the_default default_metis_lam_trans) else if name = smtN then SMT else diff -r 319f8659267d -r f625e0e79dd1 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Nov 19 17:12:58 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Nov 19 17:37:35 2013 +0100 @@ -13,22 +13,13 @@ type one_line_params = Sledgehammer_Reconstructor.one_line_params type isar_params = - bool * bool * Time.time option * real * bool * (string * stature) list vector - * (unit -> (term, string) atp_step list) * thm + bool * bool * string * string * Time.time option * real * bool * (string * stature) list vector + * (term, string) atp_step list * thm - val lam_trans_of_atp_proof : string atp_proof -> string -> string - val is_typed_helper_used_in_atp_proof : string atp_proof -> bool - val used_facts_in_atp_proof : - Proof.context -> (string * stature) list vector -> string atp_proof -> - (string * stature) list - val used_facts_in_unsound_atp_proof : - Proof.context -> (string * stature) list vector -> 'a atp_proof -> - string list option val isar_proof_text : Proof.context -> bool option -> isar_params -> one_line_params -> string val proof_text : - Proof.context -> bool option -> isar_params -> int -> one_line_params - -> string + Proof.context -> bool option -> (unit -> isar_params) -> int -> one_line_params -> string end; structure Sledgehammer_Reconstruct : SLEDGEHAMMER_RECONSTRUCT = @@ -56,113 +47,6 @@ open String_Redirect -(** fact extraction from ATP proofs **) - -fun find_first_in_list_vector vec key = - Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key - | (_, value) => value) NONE vec - -val unprefix_fact_number = space_implode "_" o tl o space_explode "_" - -fun resolve_one_named_fact fact_names s = - case try (unprefix fact_prefix) s of - SOME s' => - let val s' = s' |> unprefix_fact_number |> unascii_of in - s' |> find_first_in_list_vector fact_names |> Option.map (pair s') - end - | NONE => NONE -fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names) -fun is_fact fact_names = not o null o resolve_fact fact_names - -fun resolve_one_named_conjecture s = - case try (unprefix conjecture_prefix) s of - SOME s' => Int.fromString s' - | NONE => NONE - -val resolve_conjecture = map_filter resolve_one_named_conjecture -val is_conjecture = not o null o resolve_conjecture - -val ascii_of_lam_fact_prefix = ascii_of lam_fact_prefix - -(* overapproximation (good enough) *) -fun is_lam_lifted s = - String.isPrefix fact_prefix s andalso - String.isSubstring ascii_of_lam_fact_prefix s - -val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix) - -fun is_axiom_used_in_proof pred = - exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false) - -fun lam_trans_of_atp_proof atp_proof default = - case (is_axiom_used_in_proof is_combinator_def atp_proof, - is_axiom_used_in_proof is_lam_lifted atp_proof) of - (false, false) => default - | (false, true) => liftingN -(* | (true, true) => combs_and_liftingN -- not supported by "metis" *) - | (true, _) => combsN - -val is_typed_helper_name = - String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix - -fun is_typed_helper_used_in_atp_proof atp_proof = - is_axiom_used_in_proof is_typed_helper_name atp_proof - -fun add_non_rec_defs fact_names accum = - Vector.foldl (fn (facts, facts') => - union (op =) (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts) - facts') - accum fact_names - -val isa_ext = Thm.get_name_hint @{thm ext} -val isa_short_ext = Long_Name.base_name isa_ext - -fun ext_name ctxt = - if Thm.eq_thm_prop (@{thm ext}, - singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then - isa_short_ext - else - isa_ext - -val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg" -val leo2_unfold_def_rule = "unfold_def" - -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 - (* LEO 1.3.3 does not record definitions properly, leading to missing - dependencies in the TSTP proof. Remove the next line once this is - fixed. *) - add_non_rec_defs fact_names - else if rule = agsyhol_coreN orelse rule = satallax_coreN then - (fn [] => - (* agsyHOL and Satallax don't include definitions in their - unsatisfiable cores, so we assume the worst and include them all - here. *) - [(ext_name ctxt, (Global, General))] |> add_non_rec_defs fact_names - | facts => facts) - else - I) - #> (if null deps then union (op =) (resolve_fact fact_names ss) else I) - -fun used_facts_in_atp_proof ctxt fact_names atp_proof = - if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names - else fold (add_fact ctxt fact_names) atp_proof [] - -fun used_facts_in_unsound_atp_proof _ _ [] = NONE - | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof = - let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof in - if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso - not (is_axiom_used_in_proof (is_conjecture o single) atp_proof) then - SOME (map fst used_facts) - else - NONE - end - - -(** Isar proof construction and manipulation **) - val assume_prefix = "a" val have_prefix = "f" val raw_prefix = "x" @@ -339,11 +223,12 @@ in chain_proof end type isar_params = - bool * bool * Time.time option * real * bool * (string * stature) list vector - * (unit -> (term, string) atp_step list) * thm + bool * bool * string * string * Time.time option * real * bool * (string * stature) list vector + * (term, string) atp_step list * thm fun isar_proof_text ctxt isar_proofs - (debug, verbose, preplay_timeout, isar_compress, isar_try0, fact_names, atp_proof, goal) + (debug, verbose, metis_type_enc, metis_lam_trans, preplay_timeout, isar_compress, + isar_try0, fact_names, atp_proof, goal) (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = let val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt @@ -354,11 +239,6 @@ ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes) val one_line_proof = one_line_proof_text 0 one_line_params - val atp_proof = atp_proof () - val type_enc = - if is_typed_helper_used_in_atp_proof atp_proof then full_typesN - else partial_typesN - val lam_trans = lam_trans_of_atp_proof atp_proof metis_default_lam_trans val do_preplay = preplay_timeout <> SOME Time.zeroTime fun isar_proof_of () = @@ -509,7 +389,7 @@ |> redirect_graph axioms tainted bot |> isar_proof_of_direct_proof |> relabel_proof_canonically - |> `(proof_preplay_interface debug ctxt type_enc lam_trans do_preplay + |> `(proof_preplay_interface debug ctxt metis_type_enc metis_lam_trans do_preplay preplay_timeout) val ((preplay_time, preplay_fail), isar_proof) = isar_proof @@ -521,8 +401,8 @@ preplay_interface |> `overall_preplay_stats ||> clean_up_labels_in_proof - val isar_text = string_of_proof ctxt type_enc lam_trans subgoal - subgoal_count isar_proof + val isar_text = + string_of_proof ctxt metis_type_enc metis_lam_trans subgoal subgoal_count isar_proof in case isar_text of "" => @@ -572,7 +452,7 @@ (one_line_params as (preplay, _, _, _, _, _)) = (if isar_proofs = SOME true orelse (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then - isar_proof_text ctxt isar_proofs isar_params + isar_proof_text ctxt isar_proofs (isar_params ()) else one_line_proof_text num_chained) one_line_params