--- 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;
--- 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