# HG changeset patch # User blanchet # Date 1384876130 -3600 # Node ID 237d5be57277e7b83a0328d9fa0da7a3682e7ee8 # Parent a220071f6708a440976173ace8f93e6c5cb3822a refactored diff -r a220071f6708 -r 237d5be57277 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Nov 19 15:45:45 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Nov 19 16:48:50 2013 +0100 @@ -838,9 +838,10 @@ 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, - pool, fact_names, lifted, sym_tab, atp_proof, goal) + (debug, verbose, preplay_timeout, isar_compress, isar_try0, fact_names, atp_proof, + goal) val one_line_params = (preplay, proof_banner mode name, used_facts, choose_minimize_command ctxt params minimize_command name diff -r a220071f6708 -r 237d5be57277 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Nov 19 15:45:45 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Nov 19 16:48:50 2013 +0100 @@ -7,14 +7,14 @@ signature SLEDGEHAMMER_RECONSTRUCT = sig + type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step type 'a atp_proof = 'a ATP_Proof.atp_proof type stature = ATP_Problem_Generate.stature - type one_line_params = Sledgehammer_Print.one_line_params + type one_line_params = Sledgehammer_Reconstructor.one_line_params type isar_params = - bool * bool * Time.time option * real * bool * string Symtab.table - * (string * stature) list vector * (string * term) list * int Symtab.table - * string atp_proof * thm + bool * bool * Time.time option * real * bool * (string * stature) list vector + * (unit -> (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 @@ -24,6 +24,9 @@ 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 : @@ -407,14 +410,19 @@ 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 Symtab.table - * (string * stature) list vector * (string * term) list * int Symtab.table - * string atp_proof * thm + bool * bool * Time.time option * real * bool * (string * stature) list vector + * (unit -> (term, string) atp_step list) * thm fun isar_proof_text ctxt isar_proofs - (debug, verbose, preplay_timeout, isar_compress, isar_try0, pool, - fact_names, lifted, sym_tab, atp_proof, goal) + (debug, verbose, 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 @@ -425,6 +433,7 @@ 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 @@ -435,11 +444,6 @@ let val atp_proof = atp_proof - |> 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 |> rpair [] |-> fold_rev (add_line fact_names) |> rpair [] |-> fold_rev add_nontrivial_line |> rpair (0, []) diff -r a220071f6708 -r 237d5be57277 src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Tue Nov 19 15:45:45 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML Tue Nov 19 16:48:50 2013 +0100 @@ -7,7 +7,6 @@ signature SLEDGEHAMMER_RECONSTRUCTOR = sig - type stature = ATP_Problem_Generate.stature datatype reconstructor = @@ -25,8 +24,7 @@ play * string * (string * stature) list * minimize_command * int * int val smtN : string - -end +end; structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR = struct @@ -49,4 +47,4 @@ val smtN = "smt" -end +end;