# HG changeset patch # User blanchet # Date 1644249577 -3600 # Node ID 41fd2e8f6b16a00c464e2268541062345f8a00a0 # Parent 7ff39293e265121a4b001d408b17eacd888b117c more robust TSTP proof parsing diff -r 7ff39293e265 -r 41fd2e8f6b16 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Mon Feb 07 15:26:22 2022 +0100 +++ b/src/HOL/Tools/ATP/atp_proof.ML Mon Feb 07 16:59:37 2022 +0100 @@ -86,7 +86,7 @@ string list val dummy_atype : string ATP_Problem.atp_type val role_of_tptp_string : string -> ATP_Problem.atp_formula_role - val parse_line : string -> ('a * string ATP_Problem.atp_problem_line list) list -> + val parse_line : bool -> string -> ('a * string ATP_Problem.atp_problem_line list) list -> string list -> ((string * string list) * ATP_Problem.atp_formula_role * (string, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, 'c) ATP_Problem.atp_formula @@ -97,7 +97,8 @@ val core_of_agsyhol_proof : string -> string list option val string_of_atp_step : ('a -> string) -> ('b -> string) -> ('a, 'b) atp_step -> string - val atp_proof_of_tstplike_proof : string -> string atp_problem -> string -> string atp_proof + val atp_proof_of_tstplike_proof : bool -> string -> string atp_problem -> string -> + string atp_proof end; structure ATP_Proof : ATP_PROOF = @@ -553,9 +554,10 @@ fun parse_hol_formula x = (parse_hol_term #>> remove_hol_app #>> AAtom) x -fun parse_tstp_hol_line problem = +fun parse_tstp_hol_line full problem = (Scan.this_string tptp_thf -- $$ "(") |-- scan_general_id --| $$ "," - -- Symbol.scan_ascii_id --| $$ "," -- (parse_hol_formula || skip_term >> K dummy_phi) + -- Symbol.scan_ascii_id --| $$ "," -- + (if full then parse_hol_formula || skip_term >> K dummy_phi else skip_term >> K dummy_phi) -- parse_tstp_extra_arguments --| $$ ")" --| $$ "." >> (fn (((num, role), phi), src) => @@ -575,11 +577,11 @@ [(name, role', phi, rule, map (rpair []) deps)] end) -fun parse_tstp_fol_line problem = +fun parse_tstp_fol_line full problem = ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof || Scan.this_string tptp_tff) -- $$ "(") |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ "," - -- (parse_fol_formula || skip_term >> K dummy_phi) -- parse_tstp_extra_arguments - --| $$ ")" --| $$ "." + -- (if full then parse_fol_formula || skip_term >> K dummy_phi else skip_term >> K dummy_phi) + -- parse_tstp_extra_arguments --| $$ ")" --| $$ "." >> (fn (((num, role0), phi), src) => let val role = role_of_tptp_string role0 @@ -616,7 +618,9 @@ | _ => mk_step ())] end) -fun parse_tstp_line problem = parse_tstp_fol_line problem || parse_tstp_hol_line problem +fun parse_tstp_line full problem = + parse_tstp_fol_line full problem + || parse_tstp_hol_line full problem (**** PARSING OF SPASS OUTPUT ****) @@ -654,10 +658,10 @@ fun core_inference inf fact = ((fact, [fact]), Unknown, dummy_phi, inf, []) -fun parse_line local_name problem = +fun parse_line full local_name problem = (* Satallax is handled separately, in "atp_satallax.ML". *) if local_name = spassN then parse_spass_line - else parse_tstp_line problem + else parse_tstp_line full problem fun core_of_agsyhol_proof s = (case split_lines s of @@ -711,20 +715,20 @@ "(" ^ name' ^ ", " ^ role' ^ ", " ^ x' ^ ", " ^ y' ^ ", " ^ names' ^ ")" end -fun parse_proof local_name problem = +fun parse_proof full local_name problem = strip_spaces_except_between_idents #> raw_explode #> Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) - (Scan.finite Symbol.stopper (Scan.repeats1 (parse_line local_name problem)))) - #> fst + (Scan.finite Symbol.stopper (Scan.repeats1 (parse_line full local_name problem)))) + #> (fn (proof, ss) => if null ss then proof else raise UNRECOGNIZED_ATP_PROOF ()) -fun atp_proof_of_tstplike_proof _ _ "" = [] - | atp_proof_of_tstplike_proof local_prover problem tstp = +fun atp_proof_of_tstplike_proof _ _ _ "" = [] + | atp_proof_of_tstplike_proof full local_prover problem tstp = (case core_of_agsyhol_proof tstp of SOME facts => facts |> map (core_inference agsyhol_core_rule) | NONE => - tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) - |> parse_proof local_prover problem + tstp + |> parse_proof full local_prover problem |> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o apply2 #1)))) end; diff -r 7ff39293e265 -r 41fd2e8f6b16 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Feb 07 15:26:22 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Feb 07 16:59:37 2022 +0100 @@ -160,14 +160,6 @@ fun merge data : T = AList.merge (op =) (K true) data ) -fun remotify_prover_if_supported_and_not_already_remote ctxt name = - if String.isPrefix remote_prefix name then - SOME name - else - let val remote_name = remote_prefix ^ name in - if is_prover_supported ctxt remote_name then SOME remote_name else NONE - end - (* The first ATP of the list is used by Auto Sledgehammer. *) fun default_provers_param_value ctxt = filter (is_prover_installed ctxt) (smts ctxt @ atps) \ \see also \<^system_option>\sledgehammer_provers\\ diff -r 7ff39293e265 -r 41fd2e8f6b16 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 07 15:26:22 2022 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 07 16:59:37 2022 +0100 @@ -235,18 +235,18 @@ cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n")) |> File.write_list prob_path - val ((output, run_time), (atp_proof, outcome)) = + val ((output, run_time), ((atp_proof, tstplike_proof), outcome)) = Timeout.apply generous_run_timeout run_command () |>> overlord ? (fn output => prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") output) |> (fn accum as (output, _) => (accum, extract_tstplike_proof_and_outcome verbose proof_delims known_failures output - |>> atp_proof_of_tstplike_proof (perhaps (try (unprefix remote_prefix)) name) - atp_problem - handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofUnparsable))) - handle Timeout.TIMEOUT _ => (("", run_timeout), ([], SOME TimedOut)) - | ERROR msg => (("", Time.zeroTime), ([], SOME (UnknownError msg))) + |>> `(atp_proof_of_tstplike_proof false (perhaps (try (unprefix remote_prefix)) name) + atp_problem) + handle UNRECOGNIZED_ATP_PROOF () => (([], ""), SOME ProofUnparsable))) + handle Timeout.TIMEOUT _ => (("", run_timeout), (([], ""), SOME TimedOut)) + | ERROR msg => (("", Time.zeroTime), (([], ""), SOME (UnknownError msg))) val () = spying spy (fn () => (state, subgoal, name, "Running command in " ^ @@ -265,13 +265,15 @@ | NONE => (found_proof name; NONE)) | _ => outcome) in - (atp_problem_data, (output, run_time, facts, atp_proof, outcome), (good_format, type_enc)) + (atp_problem_data, + (output, run_time, facts, atp_problem, tstplike_proof, atp_proof, outcome), + (good_format, type_enc)) end (* If the problem file has not been exported, remove it; otherwise, export the proof file too. *) fun clean_up () = if problem_dest_dir = "" then (try File.rm prob_path; ()) else () - fun export (_, (output, _, _, _, _), _) = + fun export (_, (output, _, _, _, _, _, _), _) = let val proof_dest_dir_path = Path.explode proof_dest_dir val make_export_file_name = @@ -287,7 +289,8 @@ error ("No such directory: " ^ quote proof_dest_dir) end - val ((_, pool, lifted, sym_tab), (output, run_time, used_from, atp_proof, outcome), + val ((_, pool, lifted, sym_tab), + (output, run_time, used_from, atp_problem, tstplike_proof, atp_proof, outcome), (format, type_enc)) = with_cleanup clean_up run () |> tap export @@ -305,7 +308,7 @@ val preferred_methss = (Metis_Method (NONE, NONE), bunches_of_proof_methods ctxt try0 smt_proofs needs_full_types - (if atp_proof_prefers_lifting atp_proof then liftingN else opaque_liftingN)) + (if atp_proof_prefers_lifting atp_proof then liftingN else opaque_liftingN)) in (used_facts, preferred_methss, fn preplay => @@ -314,18 +317,24 @@ fun isar_params () = let + val full_atp_proof = + atp_proof_of_tstplike_proof true (perhaps (try (unprefix remote_prefix)) name) + atp_problem tstplike_proof val metis_type_enc = - if is_typed_helper_used_in_atp_proof atp_proof then SOME full_typesN else NONE + if is_typed_helper_used_in_atp_proof full_atp_proof then + SOME full_typesN + else + NONE val metis_lam_trans = - if atp_proof_prefers_lifting atp_proof then SOME liftingN else NONE - val atp_proof = - atp_proof + if atp_proof_prefers_lifting full_atp_proof then SOME liftingN else NONE + val full_atp_proof = + full_atp_proof |> termify_atp_proof ctxt name format type_enc pool lifted sym_tab |> local_name = spassN ? introduce_spass_skolems |> factify_atp_proof (map fst used_from) hyp_ts concl_t in (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress, try0, - minimize, atp_proof, goal) + minimize, full_atp_proof, goal) end val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count)