# HG changeset patch # User blanchet # Date 1384877578 -3600 # Node ID 319f8659267d0d711078586503ca5c1920aa5247 # Parent f7fef6b00bfea01143d95158fc3c7d564f57bed6 refactoring diff -r f7fef6b00bfe -r 319f8659267d src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Nov 19 17:07:52 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Tue Nov 19 17:12:58 2013 +0100 @@ -10,6 +10,8 @@ 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 ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step + type 'a atp_proof = 'a ATP_Proof.atp_proof val metisN : string val full_typesN : string @@ -32,6 +34,10 @@ val prop_of_atp : Proof.context -> bool -> int Symtab.table -> (string, string, (string, string) atp_term, string) atp_formula -> term + + val termify_atp_proof : + Proof.context -> string Symtab.table -> (string * term) list -> + int Symtab.table -> string atp_proof -> (term, string) atp_step list end; structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT = @@ -339,4 +345,80 @@ | _ => raise ATP_FORMULA [phi] in repair_tvar_sorts (do_formula true phi Vartab.empty) end +fun repair_name "$true" = "c_True" + | repair_name "$false" = "c_False" + | repair_name "$$e" = tptp_equal (* seen in Vampire proofs *) + | repair_name s = + if is_tptp_equal s orelse + (* seen in Vampire proofs *) + (String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then + tptp_equal + else + s + +fun infer_formula_types ctxt = + Type.constraint HOLogic.boolT + #> Syntax.check_term + (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) + +val combinator_table = + [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}), + (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def [abs_def]}), + (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def [abs_def]}), + (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def [abs_def]}), + (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def [abs_def]})] + +fun uncombine_term thy = + let + fun aux (t1 $ t2) = betapply (pairself aux (t1, t2)) + | aux (Abs (s, T, t')) = Abs (s, T, aux t') + | aux (t as Const (x as (s, _))) = + (case AList.lookup (op =) combinator_table s of + SOME thm => thm |> prop_of |> specialize_type thy x + |> Logic.dest_equals |> snd + | NONE => t) + | aux t = t + in aux end + +fun unlift_term lifted = + map_aterms (fn t as Const (s, _) => + if String.isPrefix lam_lifted_prefix s then + case AList.lookup (op =) lifted s of + SOME t => + (* FIXME: do something about the types *) + unlift_term lifted t + | NONE => t + else + t + | t => t) + +fun decode_line ctxt lifted sym_tab (name, role, u, rule, deps) = + let + val thy = Proof_Context.theory_of ctxt + val t = + u |> prop_of_atp ctxt true sym_tab + |> uncombine_term thy + |> unlift_term lifted + |> infer_formula_types ctxt + in (name, role, t, rule, deps) end + +val waldmeister_conjecture_num = "1.0.0.0" + +fun repair_waldmeister_endgame arg = + let + fun do_tail (name, _, t, rule, deps) = + (name, Negated_Conjecture, s_not t, rule, deps) + fun do_body [] = [] + | 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 arg end + +fun termify_atp_proof ctxt pool lifted sym_tab = + clean_up_atp_proof_dependencies + #> nasty_atp_proof pool + #> map_term_names_in_atp_proof repair_name + #> map (decode_line ctxt lifted sym_tab) + #> repair_waldmeister_endgame + end; diff -r f7fef6b00bfe -r 319f8659267d src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Nov 19 17:07:52 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Nov 19 17:12:58 2013 +0100 @@ -24,9 +24,6 @@ val used_facts_in_unsound_atp_proof : Proof.context -> (string * stature) list vector -> 'a atp_proof -> string list option - val termify_atp_proof : - Proof.context -> string Symtab.table -> (string * term) list -> - int Symtab.table -> string atp_proof -> (term, string) atp_step list val isar_proof_text : Proof.context -> bool option -> isar_params -> one_line_params -> string val proof_text : @@ -187,63 +184,6 @@ | add_fact_of_dependencies _ names = apfst (insert (op =) (label_of_clause names)) -fun repair_name "$true" = "c_True" - | repair_name "$false" = "c_False" - | repair_name "$$e" = tptp_equal (* seen in Vampire proofs *) - | repair_name s = - if is_tptp_equal s orelse - (* seen in Vampire proofs *) - (String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then - tptp_equal - else - s - -fun infer_formula_types ctxt = - Type.constraint HOLogic.boolT - #> Syntax.check_term - (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) - -val combinator_table = - [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}), - (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def [abs_def]}), - (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def [abs_def]}), - (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def [abs_def]}), - (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def [abs_def]})] - -fun uncombine_term thy = - let - fun aux (t1 $ t2) = betapply (pairself aux (t1, t2)) - | aux (Abs (s, T, t')) = Abs (s, T, aux t') - | aux (t as Const (x as (s, _))) = - (case AList.lookup (op =) combinator_table s of - SOME thm => thm |> prop_of |> specialize_type thy x - |> Logic.dest_equals |> snd - | NONE => t) - | aux t = t - in aux end - -fun unlift_term lifted = - map_aterms (fn t as Const (s, _) => - if String.isPrefix lam_lifted_prefix s then - case AList.lookup (op =) lifted s of - SOME t => - (* FIXME: do something about the types *) - unlift_term lifted t - | NONE => t - else - t - | t => t) - -fun decode_line ctxt lifted sym_tab (name, role, u, rule, deps) = - let - val thy = Proof_Context.theory_of ctxt - val t = - u |> prop_of_atp ctxt true sym_tab - |> uncombine_term thy - |> unlift_term lifted - |> infer_formula_types ctxt - in (name, role, t, rule, deps) end - fun replace_one_dependency (old, new) dep = if is_same_atp_step dep old then new else [dep] fun replace_dependencies_in_line p (name, role, t, rule, deps) = @@ -283,18 +223,6 @@ | (pre, (name', _, _, _, _) :: post) => line :: pre @ map (replace_dependencies_in_line (name', [name])) post -val waldmeister_conjecture_num = "1.0.0.0" - -fun repair_waldmeister_endgame arg = - let - fun do_tail (name, _, t, rule, deps) = - (name, Negated_Conjecture, s_not t, rule, deps) - fun do_body [] = [] - | 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 arg end - (* Recursively delete empty lines (type information) from the proof. *) fun add_nontrivial_line (line as (name, _, t, _, [])) lines = if is_only_type_information t then delete_dependency name lines @@ -410,13 +338,6 @@ and chain_proofs proofs = map (chain_proof) proofs in chain_proof end -fun termify_atp_proof ctxt pool lifted sym_tab = - clean_up_atp_proof_dependencies - #> nasty_atp_proof pool - #> map_term_names_in_atp_proof repair_name - #> map (decode_line ctxt lifted sym_tab) - #> repair_waldmeister_endgame - type isar_params = bool * bool * Time.time option * real * bool * (string * stature) list vector * (unit -> (term, string) atp_step list) * thm