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