# HG changeset patch # User blanchet # Date 1391031274 -3600 # Node ID 948e8b7ea82f0150143d49f2ab76025dcdcfa4f1 # Parent f3ac344284ff02e0e95918f190cb167c53efcdc9 correctly handle exceptions arising from (experimental) Isar proof code diff -r f3ac344284ff -r 948e8b7ea82f src/HOL/Tools/Sledgehammer/sledgehammer_print.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Wed Jan 29 20:11:38 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Wed Jan 29 22:34:34 2014 +0100 @@ -122,9 +122,7 @@ fun add_suffix suffix (s, ctxt) = (s ^ suffix, ctxt) fun of_indent ind = replicate_string (ind * indent_size) " " - fun of_moreover ind = of_indent ind ^ "moreover\n" - fun of_label l = if l = no_label then "" else string_of_label l ^ ": " fun of_obtain qs nr = @@ -136,7 +134,6 @@ "") ^ "obtain" fun of_show_have qs = if member (op =) qs Show then "show" else "have" - fun of_thus_hence qs = if member (op =) qs Show then "thus" else "hence" fun of_have qs nr = diff -r f3ac344284ff -r 948e8b7ea82f src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jan 29 20:11:38 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Jan 29 22:34:34 2014 +0100 @@ -799,8 +799,8 @@ |> introduce_spass_skolem |> factify_atp_proof fact_names hyp_ts concl_t in - (debug, verbose, metis_type_enc, metis_lam_trans, preplay_timeout, - isar_compress, isar_try0, atp_proof, goal) + (verbose, metis_type_enc, metis_lam_trans, preplay_timeout, isar_compress, + isar_try0, atp_proof, goal) end val one_line_params = (preplay, proof_banner mode name, used_facts, @@ -808,7 +808,7 @@ 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 debug isar_proofs isar_params num_chained one_line_params end, (if verbose then "\nATP real CPU time: " ^ string_of_time run_time ^ "." else "") ^ (if important_message <> "" then diff -r f3ac344284ff -r 948e8b7ea82f src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jan 29 20:11:38 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jan 29 22:34:34 2014 +0100 @@ -14,10 +14,9 @@ type one_line_params = Sledgehammer_Reconstructor.one_line_params type isar_params = - bool * bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm + bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm - val isar_proof_text : Proof.context -> bool option -> isar_params -> one_line_params -> string - val proof_text : Proof.context -> bool option -> (unit -> isar_params) -> int -> + val proof_text : Proof.context -> bool -> bool option -> (unit -> isar_params) -> int -> one_line_params -> string end; @@ -192,7 +191,7 @@ end type isar_params = - bool * bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm + bool * string * string * Time.time * real * bool * (term, string) atp_step list * thm val arith_methodss = [[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method, @@ -205,29 +204,29 @@ [[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method], [Meson_Method]] val skolem_methodss = [[Metis_Method, Blast_Method], [Metis_New_Skolem_Method], [Meson_Method]] -fun isar_proof_text ctxt isar_proofs - (debug, verbose, metis_type_enc, metis_lam_trans, preplay_timeout, isar_compress, isar_try0, - atp_proof, goal) +fun isar_proof_text ctxt debug isar_proofs isar_params (one_line_params as (_, _, _, _, subgoal, subgoal_count)) = let - val (params, _, concl_t) = strip_subgoal goal subgoal ctxt - val (_, ctxt) = - params - |> map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) - |> (fn fixes => ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes) - val one_line_proof = one_line_proof_text 0 one_line_params - - val do_preplay = preplay_timeout <> Time.zeroTime - val isar_try0 = isar_try0 andalso do_preplay - - val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem - fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev - - fun get_role keep_role ((num, _), role, t, rule, _) = - if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE - fun isar_proof_of () = let + val SOME (verbose, metis_type_enc, metis_lam_trans, preplay_timeout, isar_compress, + isar_try0, atp_proof, goal) = try isar_params () + + val (params, _, concl_t) = strip_subgoal goal subgoal ctxt + val (_, ctxt) = + params + |> map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) + |> (fn fixes => ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes) + + val do_preplay = preplay_timeout <> Time.zeroTime + val isar_try0 = isar_try0 andalso do_preplay + + val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem + fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev + + fun get_role keep_role ((num, _), role, t, rule, _) = + if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE + val atp_proof = atp_proof |> rpair [] |-> fold_rev add_line_pass1 @@ -398,6 +397,7 @@ end) end + val one_line_proof = one_line_proof_text 0 one_line_params val isar_proof = if debug then isar_proof_of () @@ -415,11 +415,11 @@ | Play_Failed => true | Not_Played => false) -fun proof_text ctxt isar_proofs isar_params num_chained +fun proof_text ctxt debug isar_proofs isar_params num_chained (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 debug isar_proofs isar_params else one_line_proof_text num_chained) one_line_params