diff --git a/src/HOL/Tools/ATP/atp_proof.ML b/src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML +++ b/src/HOL/Tools/ATP/atp_proof.ML @@ -1,784 +1,795 @@ (* Title: HOL/Tools/ATP/atp_proof.ML Author: Lawrence C. Paulson, Cambridge University Computer Laboratory Author: Claire Quigley, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen Author: Mathias Fleury, ENS Rennes Abstract representation of ATP proofs and TSTP/SPASS syntax. *) signature ATP_PROOF = sig type 'a atp_type = 'a ATP_Problem.atp_type type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term type atp_formula_role = ATP_Problem.atp_formula_role type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula type 'a atp_problem = 'a ATP_Problem.atp_problem exception UNRECOGNIZED_ATP_PROOF of unit datatype atp_failure = MaybeUnprovable | Unprovable | GaveUp | ProofMissing | ProofIncomplete | ProofUnparsable | + UnsoundProof of bool * string list | TimedOut | Inappropriate | OutOfResources | MalformedInput | MalformedOutput | Interrupted | Crashed | InternalError | UnknownError of string type atp_step_name = string * string list type ('a, 'b) atp_step = atp_step_name * atp_formula_role * 'a * 'b * atp_step_name list type 'a atp_proof = (('a, 'a, ('a, 'a atp_type) atp_term, 'a) atp_formula, string) atp_step list val agsyholN : string val alt_ergoN : string val cvc4N : string val eN : string val iproverN : string val leo2N : string val leo3N : string val satallaxN : string val spassN : string val vampireN : string val veritN : string val waldmeisterN : string val z3N : string val zipperpositionN : string val remote_prefix : string val dummy_fofN : string val dummy_tfxN : string val dummy_thfN : string val agsyhol_core_rule : string val spass_input_rule : string val spass_pre_skolemize_rule : string val spass_skolemize_rule : string val zipperposition_define_rule : string val short_output : bool -> string -> string val string_of_atp_failure : atp_failure -> string val extract_important_message : string -> string val extract_known_atp_failure : (atp_failure * string) list -> string -> atp_failure option val extract_tstplike_proof_and_outcome : bool -> (string * string) list -> (atp_failure * string) list -> string -> string * atp_failure option val is_same_atp_step : atp_step_name -> atp_step_name -> bool val scan_general_id : string list -> string * string list val parse_fol_formula : string list -> (string, string atp_type, (string, string atp_type) atp_term, string) atp_formula * string list val clean_up_atp_proof_dependencies : string atp_proof -> string atp_proof val map_term_names_in_atp_proof : (string -> string) -> string atp_proof -> string atp_proof val nasty_atp_proof : string Symtab.table -> string atp_proof -> string atp_proof val skip_term : string list -> string * string list val parse_hol_formula : string list -> ('a, 'b, (string, string ATP_Problem.atp_type) ATP_Problem.atp_term, 'c) ATP_Problem.atp_formula * string list val dummy_atype : string ATP_Problem.atp_type val role_of_tptp_string : string -> ATP_Problem.atp_formula_role 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 * string * (string * 'd list) list) list * string list val core_inference : 'a -> 'b -> ('b * 'b list) * ATP_Problem.atp_formula_role * ('c, 'd, (string, 'e) ATP_Problem.atp_term, 'f) ATP_Problem.atp_formula * 'a * 'g list val vampire_step_name_ord : (string * 'a) ord 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 : bool -> string -> string atp_problem -> string -> string atp_proof val atp_abduce_candidates_of_output : string -> string atp_problem -> string -> (string, string, (string, string atp_type) atp_term, string) atp_formula list end; structure ATP_Proof : ATP_PROOF = struct open ATP_Util open ATP_Problem val agsyholN = "agsyhol" val alt_ergoN = "alt_ergo" val cvc4N = "cvc4" val eN = "e" val iproverN = "iprover" val leo2N = "leo2" val leo3N = "leo3" val satallaxN = "satallax" val spassN = "spass" val vampireN = "vampire" val veritN = "verit" val waldmeisterN = "waldmeister" val z3N = "z3" val zipperpositionN = "zipperposition" val remote_prefix = "remote_" val dummy_fofN = "dummy_fof" val dummy_tfxN = "dummy_tfx" val dummy_thfN = "dummy_thf" val agsyhol_core_rule = "__agsyhol_core" (* arbitrary *) val spass_input_rule = "Inp" val spass_pre_skolemize_rule = "__Sko0" (* arbitrary *) val spass_skolemize_rule = "__Sko" (* arbitrary *) val zipperposition_define_rule = "define" (* arbitrary *) exception UNRECOGNIZED_ATP_PROOF of unit datatype atp_failure = MaybeUnprovable | Unprovable | GaveUp | ProofMissing | ProofIncomplete | ProofUnparsable | + UnsoundProof of bool * string list | TimedOut | Inappropriate | OutOfResources | MalformedInput | MalformedOutput | Interrupted | Crashed | InternalError | UnknownError of string fun short_output verbose output = if verbose then if output = "" then "No details available" else elide_string 1000 output else "" +fun from_lemmas [] = "" + | from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) + fun string_of_atp_failure MaybeUnprovable = "Problem maybe unprovable" - | string_of_atp_failure Unprovable = "Unprovable problem" + | string_of_atp_failure Unprovable = "Problem unprovable" | string_of_atp_failure GaveUp = "Gave up" | string_of_atp_failure ProofMissing = "Proof missing" | string_of_atp_failure ProofIncomplete = "Proof incomplete" | string_of_atp_failure ProofUnparsable = "Proof unparsable" + | string_of_atp_failure (UnsoundProof (false, ss)) = + "Derived the lemma \"False\"" ^ from_lemmas ss ^ + ", likely due to the use of an unsound type encoding" + | string_of_atp_failure (UnsoundProof (true, ss)) = + "Derived the lemma \"False\"" ^ from_lemmas ss ^ + ", likely due to inconsistent axioms or \"sorry\"d lemmas" | string_of_atp_failure TimedOut = "Timed out" | string_of_atp_failure Inappropriate = "Problem outside the prover's scope" | string_of_atp_failure OutOfResources = "Out of resources" | string_of_atp_failure MalformedInput = "Malformed problem" | string_of_atp_failure MalformedOutput = "Malformed output" | string_of_atp_failure Interrupted = "Interrupted" | string_of_atp_failure Crashed = "Crashed" | string_of_atp_failure InternalError = "Internal prover error" | string_of_atp_failure (UnknownError s) = "Prover error" ^ (if s = "" then " (pass the \"verbose\" option for details)" else ":\n" ^ s) fun extract_delimited (begin_delim, end_delim) output = (case first_field begin_delim output of SOME (_, tail) => (case first_field "\n" tail of SOME (_, tail') => if end_delim = "" then tail' else (case first_field end_delim tail' of SOME (body, _) => body | NONE => "") | NONE => "") | NONE => "") val tstp_important_message_delims = ("% SZS start RequiredInformation", "% SZS end RequiredInformation") fun extract_important_message output = (case extract_delimited tstp_important_message_delims output of "" => "" | s => s |> space_explode "\n" |> filter_out (curry (op =) "") |> map (perhaps (try (unprefix "%"))) |> map (perhaps (try (unprefix " "))) |> space_implode "\n " |> quote) (* Splits by the first possible of a list of delimiters. *) fun extract_tstplike_proof delims output = (case apply2 (find_first (fn s => String.isSubstring s output)) (ListPair.unzip delims) of (SOME begin_delim, SOME end_delim) => extract_delimited (begin_delim, end_delim) output | _ => "") fun extract_known_atp_failure known_failures output = known_failures |> find_first (fn (_, pattern) => String.isSubstring pattern output) |> Option.map fst fun extract_tstplike_proof_and_outcome verbose proof_delims known_failures output = let val known_atp_failure = extract_known_atp_failure known_failures output val tstplike_proof = extract_tstplike_proof proof_delims output in (case (tstplike_proof, known_atp_failure) of (_, SOME ProofIncomplete) => ("", NONE) | (_, SOME ProofUnparsable) => ("", NONE) | ("", SOME ProofMissing) => ("", NONE) | ("", NONE) => ("", SOME (UnknownError (short_output verbose output))) | res as ("", _) => res | (tstplike_proof, _) => (tstplike_proof, NONE)) end type atp_step_name = string * string list fun is_same_atp_step (s1, _) (s2, _) = s1 = s2 val vampire_fact_prefix = "f" fun vampire_step_name_ord p = let val q = apply2 fst p in (* The "unprefix" part is to cope with Vampire's output, which puts facts with names of the form "fN" where N is an integer in reverse order. *) (case apply2 (Int.fromString o perhaps (try (unprefix vampire_fact_prefix))) q of (SOME i, SOME j) => int_ord (i, j) | (SOME _, NONE) => LESS | (NONE, SOME _) => GREATER | (NONE, NONE) => string_ord q) end type ('a, 'b) atp_step = atp_step_name * atp_formula_role * 'a * 'b * atp_step_name list type 'a atp_proof = (('a, 'a, ('a, 'a atp_type) atp_term, 'a) atp_formula, string) atp_step list (**** PARSING OF TSTP FORMAT ****) (* Strings enclosed in single quotes (e.g., file names), identifiers possibly starting with "$" and possibly with "!" in them. *) val scan_general_id = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode || (Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig >> (op ^ o apply2 implode)) -- Scan.optional (Scan.repeat ($$ "!") -- Scan.many1 Symbol.is_letdig >> (op ^ o apply2 implode)) "" >> op ^ fun skip_term x = let fun skip _ accum [] = (accum, []) | skip n accum (ss as s :: ss') = if (s = "," orelse s = ".") andalso n = 0 then (accum, ss) else if member (op =) [")", "]"] s then if n = 0 then (accum, ss) else skip (n - 1) (s :: accum) ss' else if member (op =) ["(", "["] s then skip (n + 1) (s :: accum) ss' else skip n (s :: accum) ss' in (skip 0 [] #>> (rev #> implode)) x end and skip_terms x = (skip_term ::: Scan.repeat ($$ "," |-- skip_term)) x datatype source = File_Source of string * string option | Inference_Source of string * string list | Introduced_Source of string | Define_Source val dummy_phi = AAtom (ATerm (("", []), [])) val dummy_atype = AType (("", []), []) (* "skip_term" is there to cope with Waldmeister nonsense such as "theory(equality)". *) fun parse_dependency x = (parse_inference_source >> snd || scan_general_id --| skip_term >> single) x and parse_dependencies x = (Scan.repeats (Scan.option ($$ ",") |-- parse_dependency) >> (filter_out (curry (op =) "theory"))) x and parse_file_source x = (Scan.this_string "file" |-- $$ "(" |-- scan_general_id -- Scan.option ($$ "," |-- scan_general_id --| Scan.option ($$ "," |-- $$ "[" -- Scan.option scan_general_id --| $$ "]")) --| $$ ")") x and parse_inference_source x = (Scan.this_string "inference" |-- $$ "(" |-- scan_general_id --| skip_term --| $$ "," --| skip_term --| $$ "," --| $$ "[" -- parse_dependencies --| $$ "]" --| $$ ")") x and parse_introduced_source x = (Scan.this_string "introduced" |-- $$ "(" |-- scan_general_id --| Scan.option ($$ "," |-- skip_term) --| $$ ")") x and parse_define_source x = (Scan.this_string "define" |-- $$ "(" |-- skip_term --| $$ ")") x and parse_source x = (parse_file_source >> File_Source >> SOME || parse_inference_source >> Inference_Source >> SOME || parse_introduced_source >> Introduced_Source >> SOME || parse_define_source >> K Define_Source >> SOME || scan_general_id >> (fn s => SOME (Inference_Source ("", [s]))) (* for E *) || skip_term >> K NONE) x fun list_app (f, args) = fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f fun parse_class x = scan_general_id x and parse_classes x = (parse_class ::: Scan.repeat ($$ "&" |-- parse_class)) x fun parse_type x = (($$ "(" |-- parse_type --| $$ ")" || Scan.this_string tptp_pi_binder |-- $$ "[" |-- skip_terms --| $$ "]" --| $$ ":" -- parse_type >> (fn (_, ty) => ty (* currently ignoring type constructor declarations anyway *)) || (scan_general_id -- Scan.optional ($$ "{" |-- parse_classes --| $$ "}") []) -- Scan.optional ($$ "(" |-- parse_types --| $$ ")") [] >> AType) -- Scan.option (($$ tptp_app || $$ tptp_fun_type || $$ tptp_product_type) -- parse_type) >> (fn (a, NONE) => a | (a, SOME (bin_op, b)) => if bin_op = tptp_app then (case a of AType (s_clss, tys) => AType (s_clss, tys @ [b]) | _ => raise UNRECOGNIZED_ATP_PROOF ()) else if bin_op = tptp_fun_type then AFun (a, b) else if bin_op = tptp_product_type then AType ((tptp_product_type, []), [a, b]) else raise Fail "impossible case")) x and parse_types x = (parse_type ::: Scan.repeat ($$ "," |-- parse_type)) x (* We currently half ignore types. *) fun parse_fol_optional_type_signature x = (Scan.option ($$ tptp_has_type |-- parse_type) >> (fn some as SOME (AType ((s, []), [])) => if s = dfg_individual_type then NONE else some | res => res)) x and parse_fol_arg x = ($$ "(" |-- parse_fol_term --| $$ ")" --| parse_fol_optional_type_signature || scan_general_id -- parse_fol_optional_type_signature -- Scan.optional ($$ "<" |-- parse_types --| $$ ">") [] -- Scan.optional ($$ "(" |-- parse_fol_terms --| $$ ")") [] >> (fn (((s, ty_opt), tyargs), args) => if is_tptp_variable s andalso null tyargs andalso null args andalso is_some ty_opt then ATerm ((s, the_list ty_opt), []) else ATerm ((s, tyargs), args))) x and parse_fol_term x = (parse_fol_arg -- Scan.repeat ($$ tptp_app |-- parse_fol_arg) --| parse_fol_optional_type_signature >> list_app) x and parse_fol_terms x = (parse_fol_term ::: Scan.repeat ($$ "," |-- parse_fol_term)) x fun parse_fol_atom x = (parse_fol_term -- Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal -- parse_fol_term) >> (fn (u1, NONE) => AAtom u1 | (u1, SOME (neg, u2)) => AAtom (ATerm (("equal", []), [u1, u2])) |> is_some neg ? mk_anot)) x (* TPTP formulas are fully parenthesized, so we don't need to worry about operator precedence. *) fun parse_fol_literal x = ((Scan.repeat ($$ tptp_not) >> length) -- ($$ "(" |-- parse_fol_formula --| $$ ")" || parse_fol_quantified_formula || parse_fol_atom) >> (fn (n, phi) => phi |> n mod 2 = 1 ? mk_anot)) x and parse_fol_formula x = (parse_fol_literal -- Scan.option ((Scan.this_string tptp_implies || Scan.this_string tptp_iff || Scan.this_string tptp_not_iff || Scan.this_string tptp_if || $$ tptp_or || $$ tptp_and) -- parse_fol_formula) >> (fn (phi1, NONE) => phi1 | (phi1, SOME (c, phi2)) => if c = tptp_implies then mk_aconn AImplies phi1 phi2 else if c = tptp_iff then mk_aconn AIff phi1 phi2 else if c = tptp_not_iff then mk_anot (mk_aconn AIff phi1 phi2) else if c = tptp_if then mk_aconn AImplies phi2 phi1 else if c = tptp_or then mk_aconn AOr phi1 phi2 else if c = tptp_and then mk_aconn AAnd phi1 phi2 else raise Fail ("impossible connective " ^ quote c))) x and parse_fol_quantified_formula x = (($$ tptp_forall >> K AForall || $$ tptp_exists >> K AExists) --| $$ "[" -- parse_fol_terms --| $$ "]" --| $$ ":" -- parse_fol_literal >> (fn ((q, ts), phi) => AQuant (q, map (fn ATerm ((s, _), _) => (s, NONE)) ts, phi))) x val parse_tstp_extra_arguments = Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term)) NONE val waldmeister_conjecture_name = "conjecture_1" fun is_same_term subst tm1 tm2 = let fun do_term_pair (AAbs (((var1, typ1), body1), args1)) (AAbs (((var2, typ2), body2), args2)) (SOME subst) = if typ1 <> typ2 andalso length args1 = length args2 then NONE else let val ls = length subst in SOME ((var1, var2) :: subst) |> do_term_pair body1 body2 |> (fn SOME subst => SOME (nth_drop (length subst - ls - 1) subst) | NONE => NONE) |> (if length args1 = length args2 then fold2 do_term_pair args1 args2 else K NONE) end | do_term_pair (ATerm ((s1, _), args1)) (ATerm ((s2, _), args2)) (SOME subst) = (case apply2 is_tptp_variable (s1, s2) of (true, true) => (case AList.lookup (op =) subst s1 of SOME s2' => if s2' = s2 then SOME subst else NONE | NONE => if null (AList.find (op =) subst s2) then SOME ((s1, s2) :: subst) else NONE) | (false, false) => if s1 = s2 then SOME subst else NONE | _ => NONE) |> (if length args1 = length args2 then fold2 do_term_pair args1 args2 else K NONE) | do_term_pair _ _ _ = NONE in SOME subst |> do_term_pair tm1 tm2 |> is_some end fun is_same_formula comm subst (AQuant (q1, xs1, phi1)) (AQuant (q2, xs2, phi2)) = q1 = q2 andalso length xs1 = length xs2 andalso is_same_formula comm ((map fst xs1 ~~ map fst xs2) @ subst) phi1 phi2 | is_same_formula comm subst (AConn (c1, phis1)) (AConn (c2, phis2)) = c1 = c2 andalso length phis1 = length phis2 andalso forall (uncurry (is_same_formula comm subst)) (phis1 ~~ phis2) | is_same_formula comm subst (AAtom (tm1 as ATerm (("equal", tys), [tm11, tm12]))) (AAtom tm2) = is_same_term subst tm1 tm2 orelse (comm andalso is_same_term subst (ATerm (("equal", tys), [tm12, tm11])) tm2) | is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2 | is_same_formula _ _ _ _ = false fun matching_formula_line_identifier phi (Formula ((ident, _), _, phi', _, _)) = if is_same_formula true [] phi phi' then SOME (ident, phi') else NONE | matching_formula_line_identifier _ _ = NONE fun find_formula_in_problem phi = maps snd #> map_filter (matching_formula_line_identifier phi) #> try (single o hd) #> the_default [] fun commute_eq (AAtom (ATerm ((s, tys), tms))) = AAtom (ATerm ((s, tys), rev tms)) | commute_eq _ = raise Fail "expected equation" fun role_of_tptp_string "axiom" = Axiom | role_of_tptp_string "definition" = Definition | role_of_tptp_string "lemma" = Lemma | role_of_tptp_string "hypothesis" = Hypothesis | role_of_tptp_string "conjecture" = Conjecture | role_of_tptp_string "negated_conjecture" = Negated_Conjecture | role_of_tptp_string "plain" = Plain | role_of_tptp_string "type" = Type_Role | role_of_tptp_string _ = Unknown fun parse_one_in_list xs = foldl1 (op ||) (map Scan.this_string xs) val tptp_literal_binary_ops = [tptp_equal, tptp_not_equal] val tptp_nonliteral_binary_ops = [tptp_and, tptp_or, tptp_implies, tptp_iff, tptp_if, tptp_not_and, tptp_not_or, tptp_not_iff] fun parse_literal_binary_op x = (parse_one_in_list tptp_literal_binary_ops >> (fn c => if c = tptp_equal then "equal" else c)) x fun parse_nonliteral_binary_op x = (parse_one_in_list tptp_nonliteral_binary_ops >> (fn c => if c = tptp_equal then "equal" else c)) x val parse_fol_quantifier = parse_one_in_list [tptp_forall, tptp_exists, tptp_lambda, tptp_hilbert_choice, tptp_hilbert_the] val parse_hol_quantifier = parse_one_in_list [tptp_ho_forall, tptp_ho_exists, tptp_hilbert_choice, tptp_hilbert_the] fun mk_ho_of_fo_quant q = if q = tptp_forall then tptp_ho_forall else if q = tptp_exists then tptp_ho_exists else if q = tptp_hilbert_choice then tptp_hilbert_choice else if q = tptp_hilbert_the then tptp_hilbert_the else raise Fail ("unrecognized quantification: " ^ q) fun remove_hol_app (ATerm ((s, ty), args)) = if s = tptp_app then (case args of ATerm (f, xs) :: ys => remove_hol_app (ATerm (f, xs @ ys)) | AAbs ((var, phi), xs) :: ys => remove_hol_app (AAbs ((var, phi), xs @ ys))) else ATerm ((s, ty), map remove_hol_app args) | remove_hol_app (AAbs ((var, phi), args)) = AAbs ((var, remove_hol_app phi), map remove_hol_app args) fun parse_hol_typed_var x = (Scan.repeat (scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_type) --| Scan.option (Scan.this_string ",")) || $$ "(" |-- parse_hol_typed_var --| $$ ")") x fun parse_simple_hol_term x = (parse_fol_quantifier -- ($$ "[" |-- parse_hol_typed_var --| $$ "]" --| $$ ":") -- parse_hol_term >> (fn ((q, ys), t) => fold_rev (fn (var, ty) => fn r => AAbs (((var, the_default dummy_atype ty), r), []) |> (if tptp_lambda <> q then mk_app (q |> mk_ho_of_fo_quant |> mk_simple_aterm) else I)) ys t) || Scan.this_string tptp_not |-- parse_hol_term >> mk_app (mk_simple_aterm tptp_not) || scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_type) >> (fn (var, typ_opt) => ATerm ((var, the_list typ_opt), [])) || parse_hol_quantifier >> mk_simple_aterm || $$ "(" |-- parse_hol_term --| $$ ")" || parse_literal_binary_op >> mk_simple_aterm || parse_nonliteral_binary_op >> mk_simple_aterm) x and parse_applied_hol_term x = (parse_simple_hol_term -- Scan.repeat (Scan.this_string tptp_app |-- parse_simple_hol_term) >> (fn (t1, tis) => fold (fn ti => fn left => mk_app left ti) tis t1)) x and parse_literal_hol_term x = (parse_applied_hol_term -- Scan.repeat (parse_literal_binary_op -- parse_applied_hol_term) >> (fn (t1, c_ti_s) => fold (fn (c, ti) => fn left => mk_apps (mk_simple_aterm c) [left, ti]) c_ti_s t1)) x and parse_hol_term x = (parse_literal_hol_term -- Scan.repeat (parse_nonliteral_binary_op -- parse_literal_hol_term) >> (fn (t1, c_ti_s) => fold (fn (c, ti) => fn left => mk_apps (mk_simple_aterm c) [left, ti]) c_ti_s t1)) x fun parse_hol_formula x = (parse_hol_term #>> remove_hol_app #>> AAtom) x fun parse_tstp_hol_line full problem = (Scan.this_string tptp_thf -- $$ "(") |-- scan_general_id --| $$ "," -- 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, role0), phi), src) => let val role = role_of_tptp_string role0 val (name, phi, role', rule, deps) = (case src of SOME (File_Source (_, SOME s)) => if role = Definition then ((num, map fst (find_formula_in_problem phi problem)), phi, role, "", []) else ((num, [s]), phi, role, "", []) | SOME (Inference_Source (rule, deps)) => ((num, []), phi, role, rule, deps) | SOME (Introduced_Source rule) => ((num, []), phi, Definition, rule, []) | SOME Define_Source => ((num, []), phi, Definition, zipperposition_define_rule, []) | _ => ((num, [num]), phi, role, "", [])) in [(name, role', phi, rule, map (rpair []) deps)] end) fun parse_tstp_fol_line full problem = ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof || Scan.this_string tptp_tcf || Scan.this_string tptp_tff) -- $$ "(") |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ "," -- (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 val ((name, phi), role', rule, deps) = (* Waldmeister isn't exactly helping. *) (case src of SOME (File_Source (_, SOME s)) => (if s = waldmeister_conjecture_name then (case find_formula_in_problem (mk_anot phi) problem of (* Waldmeister hack: Get the original orientation of the equation to avoid confusing Isar. *) [(s, phi')] => ((num, [s]), phi |> not (is_same_formula false [] (mk_anot phi) phi') ? commute_eq) | _ => ((num, []), phi)) else ((num, [s]), phi), role, "", []) | SOME (File_Source _) => (((num, map fst (find_formula_in_problem phi problem)), phi), role, "", []) | SOME (Inference_Source (rule, deps)) => (((num, []), phi), role, rule, deps) | SOME (Introduced_Source rule) => (((num, []), phi), Definition, rule, []) | SOME Define_Source => (((num, []), phi), Definition, zipperposition_define_rule, []) | _ => (((num, [num]), phi), role, "", [])) fun mk_step () = (name, role', phi, rule, map (rpair []) deps) in [(case role' of Definition => (case phi of AAtom (ATerm (("equal", _), _)) => (* Vampire's equality proxy axiom *) (name, Definition, phi, rule, map (rpair []) deps) | _ => mk_step ()) | _ => mk_step ())] end) fun parse_tstp_line full problem = parse_tstp_fol_line full problem || parse_tstp_hol_line full problem (**** PARSING OF SPASS OUTPUT ****) (* SPASS returns clause references of the form "x.y". We ignore "y". *) val parse_dot_name = scan_general_id --| $$ "." --| scan_general_id val parse_spass_annotations = Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name --| Scan.option ($$ ","))) [] (* We ignore the stars and the pluses that follow literals. *) fun parse_decorated_atom x = (parse_fol_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")) x fun mk_horn ([], []) = AAtom (ATerm (("c_False", []), [])) | mk_horn (neg_lits, pos_lits) = foldr1 (uncurry (mk_aconn AOr)) (map mk_anot neg_lits @ pos_lits) fun parse_horn_clause x = (Scan.repeat parse_decorated_atom --| $$ "|" --| $$ "|" -- Scan.repeat parse_decorated_atom --| $$ "-" --| $$ ">" -- Scan.repeat parse_decorated_atom >> (mk_horn o apfst (op @))) x val parse_spass_debug = Scan.option ($$ "(" |-- Scan.repeat (scan_general_id --| Scan.option ($$ ",")) --| $$ ")") (* Syntax: [0:] || -> . derived from formulae * *) fun parse_spass_line x = (parse_spass_debug |-- scan_general_id --| $$ "[" --| Scan.many1 Symbol.is_digit --| $$ ":" -- Symbol.scan_ascii_id -- parse_spass_annotations --| $$ "]" -- parse_horn_clause --| $$ "." -- Scan.option (Scan.this_string "derived from formulae " |-- Scan.repeat (scan_general_id --| Scan.option ($$ " "))) >> (fn ((((num, rule), deps), u), names) => [((num, these names), Unknown, u, rule, map (rpair []) deps)])) x fun core_inference inf fact = ((fact, [fact]), Unknown, dummy_phi, inf, []) 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 full problem fun core_of_agsyhol_proof s = (case split_lines s of "The transformed problem consists of the following conjectures:" :: conj :: _ :: proof_term :: _ => SOME (unprefix " " conj :: find_enclosed "<<" ">>" proof_term) | _ => NONE) fun clean_up_dependencies _ [] = [] | clean_up_dependencies seen ((name, role, u, rule, deps) :: steps) = (name, role, u, rule, map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) :: clean_up_dependencies (name :: seen) steps fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof fun map_term_names_in_atp_proof f = let fun map_type (AType ((s, clss), tys)) = AType ((f s, map f clss), map map_type tys) | map_type (AFun (ty, ty')) = AFun (map_type ty, map_type ty') | map_type (APi (ss, ty)) = APi (map f ss, map_type ty) fun map_term (ATerm ((s, tys), ts)) = ATerm ((f s, map map_type tys), map map_term ts) | map_term (AAbs (((s, ty), tm), args)) = AAbs (((f s, map_type ty), map_term tm), map map_term args) fun map_formula (AQuant (q, xs, phi)) = AQuant (q, map (apfst f) xs, map_formula phi) | map_formula (AConn (c, phis)) = AConn (c, map map_formula phis) | map_formula (AAtom t) = AAtom (map_term t) fun map_step (name, role, phi, rule, deps) = (name, role, map_formula phi, rule, deps) in map map_step end fun nasty_name pool s = Symtab.lookup pool s |> the_default s fun nasty_atp_proof pool = not (Symtab.is_empty pool) ? map_term_names_in_atp_proof (nasty_name pool) fun string_of_list f xs = enclose "[" "]" (commas (map f xs)) fun string_of_atp_step_name (s, ss) = "(" ^ s ^ ", " ^ string_of_list I ss ^ ")" fun string_of_atp_step f g (name, role, x, y, names) = let val name' = string_of_atp_step_name name val role' = ATP_Problem.tptp_string_of_role role val x' = f x val y' = g y val names' = string_of_list string_of_atp_step_name names in "(" ^ name' ^ ", " ^ role' ^ ", " ^ x' ^ ", " ^ y' ^ ", " ^ names' ^ ")" end 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 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 full local_prover problem tstp = (case core_of_agsyhol_proof tstp of SOME facts => facts |> map (core_inference agsyhol_core_rule) | NONE => tstp |> parse_proof full local_prover problem |> local_prover = vampireN ? perhaps (try (sort (vampire_step_name_ord o apply2 #1)))) val e_symbol_prefixes = ["esk", "epred"] fun exists_name_in_term pred = let fun ex_name (ATerm ((s, _), tms)) = pred s orelse exists ex_name tms | ex_name (AAbs ((_, tm), tms)) = exists ex_name (tm :: tms) in ex_name end fun exists_name_in_formula pred phi = formula_fold NONE (fn _ => fn tm => fn ex => ex orelse exists_name_in_term pred tm) phi false fun exists_symbol_in_formula prefixes = exists_name_in_formula (fn s => exists (fn prefix => String.isPrefix prefix s) prefixes) fun atp_abduce_candidates_of_output local_prover problem output = let (* Truncate too large output to avoid memory issues. *) val max_size = 1000000 val output = if String.size output > max_size then String.substring (output, 0, max_size) else output fun fold_extract accum [] = accum | fold_extract accum (line :: lines) = if String.isSubstring "# info" line andalso String.isSubstring "negated_conjecture" line then if String.isSubstring ", 0, 0," line then (* This pattern occurs in the "info()" comment of an E clause that directly emerges from the conjecture. We don't want to tell the user that they can prove "P" by assuming "P". *) fold_extract accum lines else let val clean_line = (case space_explode "#" line of [] => "" | before_hash :: _ => before_hash) in (case try (parse_proof true local_prover problem) clean_line of SOME [(_, _, phi, _, _)] => if local_prover = eN andalso exists_symbol_in_formula e_symbol_prefixes phi then fold_extract accum lines else fold_extract (phi :: accum) lines | _ => fold_extract accum lines) end else fold_extract accum lines in fold_extract [] (split_lines output) end end; diff --git a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML @@ -1,854 +1,869 @@ (* Title: HOL/Tools/ATP/atp_proof_reconstruct.ML Author: Lawrence C. Paulson, Cambridge University Computer Laboratory Author: Claire Quigley, Cambridge University Computer Laboratory Author: Jasmin Blanchette, TU Muenchen Basic proof reconstruction from ATP proofs. *) signature ATP_PROOF_RECONSTRUCT = sig type 'a atp_type = 'a ATP_Problem.atp_type 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 stature = ATP_Problem_Generate.stature type atp_step_name = ATP_Proof.atp_step_name 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 val partial_typesN : string val no_typesN : string val really_full_type_enc : string val full_type_enc : string val partial_type_enc : string val no_type_enc : string val full_type_encs : string list val partial_type_encs : string list val default_metis_lam_trans : string val leo2_extcnf_equal_neg_rule : string val satallax_tab_rule_prefix : string val forall_of : term -> term -> term val exists_of : term -> term -> term val simplify_bool : term -> term val var_name_of_typ : typ -> string val rename_bound_vars : term -> term val type_enc_aliases : (string * string list) list val unalias_type_enc : string -> string list val term_of_atp : Proof.context -> ATP_Problem.atp_format -> ATP_Problem_Generate.type_enc -> bool -> int Symtab.table -> typ option -> (string, string atp_type) atp_term -> term val prop_of_atp : Proof.context -> ATP_Problem.atp_format -> ATP_Problem_Generate.type_enc -> bool -> int Symtab.table -> (string, string, (string, string atp_type) atp_term, string) atp_formula -> term val used_facts_in_atp_proof : Proof.context -> (string * stature) list -> string atp_proof -> (string * stature) list + val used_facts_in_unsound_atp_proof : Proof.context -> (string * stature) list -> 'a atp_proof -> + string list option val atp_proof_prefers_lifting : string atp_proof -> bool val is_typed_helper_used_in_atp_proof : string atp_proof -> bool val replace_dependencies_in_line : atp_step_name * atp_step_name list -> ('a, 'b) atp_step -> ('a, 'b) atp_step val termify_atp_proof : Proof.context -> string -> ATP_Problem.atp_format -> ATP_Problem_Generate.type_enc -> string Symtab.table -> (string * term) list -> int Symtab.table -> string atp_proof -> (term, string) atp_step list val repair_waldmeister_endgame : (term, 'a) atp_step list -> (term, 'a) atp_step list val infer_formulas_types : Proof.context -> term list -> term list val introduce_spass_skolems : (term, string) atp_step list -> (term, string) atp_step list val factify_atp_proof : (string * 'a) list -> term list -> term -> (term, string) atp_step list -> (term, string) atp_step list val termify_atp_abduce_candidate : Proof.context -> string -> ATP_Problem.atp_format -> ATP_Problem_Generate.type_enc -> string Symtab.table -> (string * term) list -> int Symtab.table -> (string, string, (string, string atp_type) atp_term, string) atp_formula -> term val top_abduce_candidates : int -> term list -> term list end; structure ATP_Proof_Reconstruct : ATP_PROOF_RECONSTRUCT = struct open ATP_Util open ATP_Problem open ATP_Proof open ATP_Problem_Generate val metisN = "metis" val full_typesN = "full_types" val partial_typesN = "partial_types" val no_typesN = "no_types" val really_full_type_enc = "mono_tags" val full_type_enc = "poly_guards_query" val partial_type_enc = "poly_args" val no_type_enc = "erased" val full_type_encs = [full_type_enc, really_full_type_enc] val partial_type_encs = partial_type_enc :: full_type_encs val type_enc_aliases = [(full_typesN, full_type_encs), (partial_typesN, partial_type_encs), (no_typesN, [no_type_enc])] fun unalias_type_enc s = AList.lookup (op =) type_enc_aliases s |> the_default [s] val default_metis_lam_trans = combsN val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg" val satallax_tab_rule_prefix = "tab_" fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s | term_name' _ = "" fun lambda' v = Term.lambda_name (term_name' v, v) fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda' v t fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda' v t fun make_tfree ctxt w = let val ww = "'" ^ w in TFree (ww, the_default \<^sort>\type\ (Variable.def_sort ctxt (ww, ~1))) end fun simplify_bool ((all as Const (\<^const_name>\All\, _)) $ Abs (s, T, t)) = let val t' = simplify_bool t in if loose_bvar1 (t', 0) then all $ Abs (s, T, t') else t' end | simplify_bool (Const (\<^const_name>\Not\, _) $ t) = s_not (simplify_bool t) | simplify_bool (Const (\<^const_name>\conj\, _) $ t $ u) = s_conj (simplify_bool t, simplify_bool u) | simplify_bool (Const (\<^const_name>\disj\, _) $ t $ u) = s_disj (simplify_bool t, simplify_bool u) | simplify_bool (Const (\<^const_name>\implies\, _) $ t $ u) = s_imp (simplify_bool t, simplify_bool u) | simplify_bool ((t as Const (\<^const_name>\HOL.eq\, _)) $ u $ v) = (case (u, v) of (Const (\<^const_name>\True\, _), _) => v | (u, Const (\<^const_name>\True\, _)) => u | (Const (\<^const_name>\False\, _), v) => s_not v | (u, Const (\<^const_name>\False\, _)) => s_not u | _ => if u aconv v then \<^Const>\True\ else t $ simplify_bool u $ simplify_bool v) | simplify_bool (t $ u) = simplify_bool t $ simplify_bool u | simplify_bool (Abs (s, T, t)) = Abs (s, T, simplify_bool t) | simplify_bool t = t fun single_letter upper s = let val s' = if String.isPrefix "o" s orelse String.isPrefix "O" s then "z" else s in String.extract (Name.desymbolize (SOME upper) (Long_Name.base_name s'), 0, SOME 1) end fun var_name_of_typ (Type (\<^type_name>\fun\, [_, T])) = if body_type T = HOLogic.boolT then "p" else "f" | var_name_of_typ (Type (\<^type_name>\set\, [T])) = let fun default () = single_letter true (var_name_of_typ T) in (case T of Type (s, [T1, T2]) => if String.isSuffix "prod" s andalso T1 = T2 then "r" else default () | _ => default ()) end | var_name_of_typ (Type (s, Ts)) = if String.isSuffix "list" s then var_name_of_typ (the_single Ts) ^ "s" else single_letter false (Long_Name.base_name s) | var_name_of_typ (TFree (s, _)) = single_letter false (perhaps (try (unprefix "'")) s) | var_name_of_typ (TVar ((s, _), T)) = var_name_of_typ (TFree (s, T)) fun rename_bound_vars (t $ u) = rename_bound_vars t $ rename_bound_vars u | rename_bound_vars (Abs (_, T, t)) = Abs (var_name_of_typ T, T, rename_bound_vars t) | rename_bound_vars t = t exception ATP_CLASS of string list exception ATP_TYPE of string atp_type list exception ATP_TERM of (string, string atp_type) atp_term list exception ATP_FORMULA of (string, string, (string, string atp_type) atp_term, string) atp_formula list exception SAME of unit fun class_of_atp_class cls = (case unprefix_and_unascii class_prefix cls of SOME s => s | NONE => raise ATP_CLASS [cls]) fun atp_type_of_atp_term (ATerm ((s, _), us)) = let val tys = map atp_type_of_atp_term us in if s = tptp_fun_type then (case tys of [ty1, ty2] => AFun (ty1, ty2) | _ => raise ATP_TYPE tys) else AType ((s, []), tys) end (* Type variables are given the basic sort "HOL.type". Some will later be constrained by information from type literals, or by type inference. *) fun typ_of_atp_type ctxt (ty as AType ((a, clss), tys)) = let val Ts = map (typ_of_atp_type ctxt) tys in (case unprefix_and_unascii native_type_prefix a of SOME b => typ_of_atp_type ctxt (atp_type_of_atp_term (unmangled_type b)) | NONE => (case unprefix_and_unascii type_const_prefix a of SOME b => Type (invert_const b, Ts) | NONE => if not (null tys) then raise ATP_TYPE [ty] (* only "tconst"s have type arguments *) else (case unprefix_and_unascii tfree_prefix a of SOME b => make_tfree ctxt b | NONE => (* The term could be an Isabelle variable or a variable from the ATP, say "X1" or "_5018". Sometimes variables from the ATP are indistinguishable from Isabelle variables, which forces us to use a type parameter in all cases. *) Type_Infer.param 0 ("'" ^ perhaps (unprefix_and_unascii tvar_prefix) a, (if null clss then \<^sort>\type\ else map class_of_atp_class clss))))) end | typ_of_atp_type ctxt (AFun (ty1, ty2)) = typ_of_atp_type ctxt ty1 --> typ_of_atp_type ctxt ty2 fun typ_of_atp_term ctxt = typ_of_atp_type ctxt o atp_type_of_atp_term (* Type class literal applied to a type. Returns triple of polarity, class, type. *) fun type_constraint_of_term ctxt (u as ATerm ((a, _), us)) = (case (unprefix_and_unascii class_prefix a, map (typ_of_atp_term ctxt) us) of (SOME b, [T]) => (b, T) | _ => raise ATP_TERM [u]) (* Accumulate type constraints in a formula: negative type literals. *) fun add_var (key, z) = Vartab.map_default (key, []) (cons z) fun add_type_constraint false (cl, TFree (a ,_)) = add_var ((a, ~1), cl) | add_type_constraint false (cl, TVar (ix, _)) = add_var (ix, cl) | add_type_constraint _ _ = I fun repair_var_name s = (case unprefix_and_unascii schematic_var_prefix s of SOME s' => s' | NONE => s) (* The number of type arguments of a constant, zero if it's monomorphic. For (instances of) Skolem pseudoconstants, this information is encoded in the constant name. *) fun robust_const_num_type_args thy s = if String.isPrefix skolem_const_prefix s then s |> Long_Name.explode |> List.last |> Int.fromString |> the else if String.isPrefix lam_lifted_prefix s then if String.isPrefix lam_lifted_poly_prefix s then 2 else 0 else (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length fun slack_fastype_of t = fastype_of t handle TERM _ => Type_Infer.anyT \<^sort>\type\ val spass_skolem_prefix = "sk" (* "skc" or "skf" *) val vampire_skolem_prefix = "sK" fun var_index_of_textual textual = if textual then 0 else 1 fun quantify_over_var textual quant_of var_s var_T t = let val vars = ((var_s, var_index_of_textual textual), var_T) :: filter (fn ((s, _), _) => s = var_s) (Term.add_vars t []) val normTs = vars |> AList.group (op =) |> map (apsnd hd) fun norm_var_types (Var (x, T)) = Var (x, the_default T (AList.lookup (op =) normTs x)) | norm_var_types t = t in t |> map_aterms norm_var_types |> fold_rev quant_of (map Var normTs) end (* This assumes that distinct names are mapped to distinct names by "Variable.variant_frees". This does not hold in general but should hold for ATP-generated Skolem function names, since these end with a digit and "variant_frees" appends letters. *) fun fresh_up ctxt s = fst (hd (Variable.variant_frees ctxt [] [(s, ())])) (* Higher-order translation. Variables are typed (although we don't use that information). Lambdas are typed. The code is similar to "term_of_atp_fo". *) fun term_of_atp_ho ctxt sym_tab = let val thy = Proof_Context.theory_of ctxt val var_index = var_index_of_textual true fun do_term opt_T u = (case u of AAbs (((var, ty), term), []) => let val typ = typ_of_atp_type ctxt ty val var_name = repair_var_name var val tm = do_term NONE term in quantify_over_var true lambda' var_name typ tm end | ATerm ((s, tys), us) => if s = "" (* special marker generated on parse error *) then error "Isar proof reconstruction failed because the ATP proof contains unparsable \ \material" else if s = tptp_equal then list_comb (Const (\<^const_name>\HOL.eq\, Type_Infer.anyT \<^sort>\type\), map (do_term NONE) us) else if s = tptp_not_equal andalso length us = 2 then \<^const>\HOL.Not\ $ list_comb (Const (\<^const_name>\HOL.eq\, Type_Infer.anyT \<^sort>\type\), map (do_term NONE) us) else if not (null us) then let val args = map (do_term NONE) us val opt_T' = SOME (map slack_fastype_of args ---> the_default dummyT opt_T) val func = do_term opt_T' (ATerm ((s, tys), [])) in foldl1 (op $) (func :: args) end else if s = tptp_or then HOLogic.disj else if s = tptp_and then HOLogic.conj else if s = tptp_implies then HOLogic.imp else if s = tptp_iff orelse s = tptp_equal then HOLogic.eq_const dummyT else if s = tptp_not_iff orelse s = tptp_not_equal then \<^term>\\x y. x \ y\ else if s = tptp_if then \<^term>\\P Q. Q \ P\ else if s = tptp_not_and then \<^term>\\P Q. \ (P \ Q)\ else if s = tptp_not_or then \<^term>\\P Q. \ (P \ Q)\ else if s = tptp_not then HOLogic.Not else if s = tptp_ho_forall then HOLogic.all_const dummyT else if s = tptp_ho_exists then HOLogic.exists_const dummyT else if s = tptp_hilbert_choice then HOLogic.choice_const dummyT else if s = tptp_hilbert_the then \<^term>\The\ else (case unprefix_and_unascii const_prefix s of SOME s' => let val ((s', _), mangled_us) = s' |> unmangled_const |>> `invert_const val num_ty_args = length us - the_default 0 (Symtab.lookup sym_tab s) val (type_us, term_us) = chop num_ty_args us |>> append mangled_us val term_ts = map (do_term NONE) term_us val Ts = map (typ_of_atp_type ctxt) tys @ map (typ_of_atp_term ctxt) type_us val T = (if not (null Ts) andalso robust_const_num_type_args thy s' = length Ts then try (Sign.const_instance thy) (s', Ts) else NONE) |> (fn SOME T => T | NONE => map slack_fastype_of term_ts ---> the_default (Type_Infer.anyT \<^sort>\type\) opt_T) val t = Const (unproxify_const s', T) in list_comb (t, term_ts) end | NONE => (* a free or schematic variable *) let val ts = map (do_term NONE) us val T = (case tys of [ty] => typ_of_atp_type ctxt ty | _ => map slack_fastype_of ts ---> (case opt_T of SOME T => T | NONE => Type_Infer.anyT \<^sort>\type\)) val t = (case unprefix_and_unascii fixed_var_prefix s of SOME s => Free (s, T) | NONE => if not (is_tptp_variable s) then Free (fresh_up ctxt s, T) else Var ((repair_var_name s, var_index), T)) in list_comb (t, ts) end)) in do_term end (* First-order translation. No types are known for variables. "Type_Infer.anyT @{sort type}" should allow them to be inferred. *) fun term_of_atp_fo ctxt textual sym_tab = let val thy = Proof_Context.theory_of ctxt (* For Metis, we use 1 rather than 0 because variable references in clauses may otherwise conflict with variable constraints in the goal. At least, type inference often fails otherwise. See also "axiom_inference" in "Metis_Reconstruct". *) val var_index = var_index_of_textual textual fun do_term extra_ts opt_T u = (case u of ATerm ((s, tys), us) => if s = "" (* special marker generated on parse error *) then error "Isar proof reconstruction failed because the ATP proof contains unparsable \ \material" else if String.isPrefix native_type_prefix s then \<^Const>\True\ (* ignore TPTP type information (needed?) *) else if s = tptp_equal then list_comb (Const (\<^const_name>\HOL.eq\, Type_Infer.anyT \<^sort>\type\), map (do_term [] NONE) us) else (case unprefix_and_unascii const_prefix s of SOME s' => let val ((s', s''), mangled_us) = s' |> unmangled_const |>> `invert_const in if s' = type_tag_name then (case mangled_us @ us of [typ_u, term_u] => do_term extra_ts (SOME (typ_of_atp_term ctxt typ_u)) term_u | _ => raise ATP_TERM us) else if s' = predicator_name then do_term [] (SOME \<^typ>\bool\) (hd us) else if s' = app_op_name then let val extra_t = do_term [] NONE (List.last us) in do_term (extra_t :: extra_ts) (case opt_T of SOME T => SOME (slack_fastype_of extra_t --> T) | NONE => NONE) (nth us (length us - 2)) end else if s' = type_guard_name then \<^Const>\True\ (* ignore type predicates *) else let val new_skolem = String.isPrefix new_skolem_const_prefix s'' val num_ty_args = length us - the_default 0 (Symtab.lookup sym_tab s) val (type_us, term_us) = chop num_ty_args us |>> append mangled_us val term_ts = map (do_term [] NONE) term_us val Ts = map (typ_of_atp_type ctxt) tys @ map (typ_of_atp_term ctxt) type_us val T = (if not (null Ts) andalso robust_const_num_type_args thy s' = length Ts then if new_skolem then SOME (Type_Infer.paramify_vars (tl Ts ---> hd Ts)) else if textual then try (Sign.const_instance thy) (s', Ts) else NONE else NONE) |> (fn SOME T => T | NONE => map slack_fastype_of term_ts ---> the_default (Type_Infer.anyT \<^sort>\type\) opt_T) val t = if new_skolem then Var ((new_skolem_var_name_of_const s'', var_index), T) else Const (unproxify_const s', T) in list_comb (t, term_ts @ extra_ts) end end | NONE => (* a free or schematic variable *) let val term_ts = map (do_term [] NONE) us (* SPASS (3.8ds) and Vampire (2.6) pass arguments to Skolem functions in reverse order, which is incompatible with "metis"'s new skolemizer. *) |> exists (fn pre => String.isPrefix pre s) [spass_skolem_prefix, vampire_skolem_prefix] ? rev val ts = term_ts @ extra_ts val T = (case tys of [ty] => typ_of_atp_type ctxt ty | _ => (case opt_T of SOME T => map slack_fastype_of term_ts ---> T | NONE => map slack_fastype_of ts ---> Type_Infer.anyT \<^sort>\type\)) val t = (case unprefix_and_unascii fixed_var_prefix s of SOME s => Free (s, T) | NONE => if textual andalso not (is_tptp_variable s) then Free (s |> textual ? fresh_up ctxt, T) else Var ((repair_var_name s, var_index), T)) in list_comb (t, ts) end)) in do_term [] end fun term_of_atp ctxt (ATP_Problem.THF _) type_enc = if ATP_Problem_Generate.is_type_enc_higher_order type_enc then K (term_of_atp_ho ctxt) else error "Unsupported Isar reconstruction" | term_of_atp ctxt _ type_enc = if not (ATP_Problem_Generate.is_type_enc_higher_order type_enc) then term_of_atp_fo ctxt else error "Unsupported Isar reconstruction" fun term_of_atom ctxt format type_enc textual sym_tab pos (u as ATerm ((s, _), _)) = if String.isPrefix class_prefix s then add_type_constraint pos (type_constraint_of_term ctxt u) #> pair \<^Const>\True\ else pair (term_of_atp ctxt format type_enc textual sym_tab (SOME \<^typ>\bool\) u) (* Update schematic type variables with detected sort constraints. It's not totally clear whether this code is necessary. *) fun repair_tvar_sorts (t, tvar_tab) = let fun do_type (Type (a, Ts)) = Type (a, map do_type Ts) | do_type (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup tvar_tab xi)) | do_type (TFree z) = TFree z fun do_term (Const (a, T)) = Const (a, do_type T) | do_term (Free (a, T)) = Free (a, do_type T) | do_term (Var (xi, T)) = Var (xi, do_type T) | do_term (t as Bound _) = t | do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t) | do_term (t1 $ t2) = do_term t1 $ do_term t2 in t |> not (Vartab.is_empty tvar_tab) ? do_term end (* Interpret an ATP formula as a HOL term, extracting sort constraints as they appear in the formula. *) fun prop_of_atp ctxt format type_enc textual sym_tab phi = let fun do_formula pos phi = (case phi of AQuant (_, [], phi) => do_formula pos phi | AQuant (q, (s, _) :: xs, phi') => do_formula pos (AQuant (q, xs, phi')) (* FIXME: TFF *) #>> quantify_over_var textual (case q of AForall => forall_of | AExists => exists_of) (repair_var_name s) dummyT | AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not | AConn (c, [phi1, phi2]) => do_formula (pos |> c = AImplies ? not) phi1 ##>> do_formula pos phi2 #>> (case c of AAnd => s_conj | AOr => s_disj | AImplies => s_imp | AIff => s_iff | ANot => raise Fail "impossible connective") | AAtom tm => term_of_atom ctxt format type_enc textual sym_tab pos tm | _ => raise ATP_FORMULA [phi]) in repair_tvar_sorts (do_formula true phi Vartab.empty) end val unprefix_fact_number = space_implode "_" o tl o space_explode "_" fun resolve_fact facts s = (case try (unprefix fact_prefix) s of SOME s' => let val s' = s' |> unprefix_fact_number |> unascii_of in AList.lookup (op =) facts s' |> Option.map (pair s') end | NONE => NONE) fun resolve_conjecture s = (case try (unprefix conjecture_prefix) s of SOME s' => Int.fromString s' | NONE => NONE) fun resolve_facts facts = map_filter (resolve_fact facts) val resolve_conjectures = map_filter resolve_conjecture fun is_axiom_used_in_proof pred = exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false) fun add_fact ctxt facts ((num, ss), _, _, rule, deps) = (if member (op =) [agsyhol_core_rule, leo2_extcnf_equal_neg_rule] rule orelse String.isPrefix satallax_tab_rule_prefix rule then insert (op =) (short_thm_name ctxt ext, (Global, General)) else I) #> (if null deps then union (op =) (resolve_facts facts (num :: ss)) else I) fun used_facts_in_atp_proof ctxt facts atp_proof = if null atp_proof then facts else fold (add_fact ctxt facts) atp_proof [] +fun used_facts_in_unsound_atp_proof _ _ [] = NONE + | used_facts_in_unsound_atp_proof ctxt facts atp_proof = + let + val used_facts = used_facts_in_atp_proof ctxt facts atp_proof + val all_global_facts = forall (fn (_, (sc, _)) => sc = Global) used_facts + val axiom_used = is_axiom_used_in_proof (is_some o resolve_conjecture) atp_proof + in + if all_global_facts andalso not axiom_used then + SOME (map fst used_facts) + else + NONE + end + val ascii_of_lam_fact_prefix = ascii_of lam_fact_prefix (* overapproximation (good enough) *) fun is_lam_lifted s = String.isPrefix fact_prefix s andalso String.isSubstring ascii_of_lam_fact_prefix s val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix) fun atp_proof_prefers_lifting atp_proof = (is_axiom_used_in_proof is_combinator_def atp_proof, is_axiom_used_in_proof is_lam_lifted atp_proof) = (false, true) val is_typed_helper_name = String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix fun is_typed_helper_used_in_atp_proof atp_proof = is_axiom_used_in_proof is_typed_helper_name atp_proof fun replace_one_dependency (old, new) dep = if is_same_atp_step dep old then new else [dep] fun replace_dependencies_in_line old_new (name, role, t, rule, deps) = (name, role, t, rule, fold (union (op =) o replace_one_dependency old_new) deps []) 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 set_var_index j = map_aterms (fn Var ((s, 0), T) => Var ((s, j), T) | t => t) fun infer_formulas_types ctxt = map_index (uncurry (fn j => set_var_index j #> Type.constraint HOLogic.boolT)) #> Syntax.check_terms (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 uncomb (t1 $ t2) = betapply (uncomb t1, uncomb t2) | uncomb (Abs (s, T, t)) = Abs (s, T, uncomb t) | uncomb (t as Const (x as (s, _))) = (case AList.lookup (op =) combinator_table s of SOME thm => thm |> Thm.prop_of |> specialize_type thy x |> Logic.dest_equals |> snd | NONE => t) | uncomb t = t in uncomb end fun unlift_aterm lifted (t as Const (s, _)) = if String.isPrefix lam_lifted_prefix s then (* FIXME: do something about the types *) (case AList.lookup (op =) lifted s of SOME t' => unlift_term lifted t' | NONE => t) else t | unlift_aterm _ t = t and unlift_term lifted = map_aterms (unlift_aterm lifted) fun termify_line _ _ _ _ _ (_, Type_Role, _, _, _) = NONE | termify_line ctxt format type_enc lifted sym_tab (name, role, u, rule, deps) = let val thy = Proof_Context.theory_of ctxt val t = u |> prop_of_atp ctxt format type_enc true sym_tab |> unlift_term lifted |> uncombine_term thy |> simplify_bool in SOME (name, role, t, rule, deps) end val waldmeister_conjecture_num = "1.0.0.0" fun repair_waldmeister_endgame proof = let fun repair_tail (name, _, \<^Const>\Trueprop for t\, rule, deps) = (name, Negated_Conjecture, \<^Const>\Trueprop for \s_not t\\, rule, deps) fun repair_body [] = [] | repair_body ((line as ((num, _), _, _, _, _)) :: lines) = if num = waldmeister_conjecture_num then map repair_tail (line :: lines) else line :: repair_body lines in repair_body proof end fun map_proof_terms f (lines : ('a * 'b * 'c * 'd * 'e) list) = map2 (fn c => fn (a, b, _, d, e) => (a, b, c, d, e)) (f (map #3 lines)) lines fun termify_atp_proof ctxt local_prover format type_enc pool lifted sym_tab = nasty_atp_proof pool #> map_term_names_in_atp_proof repair_name #> map_filter (termify_line ctxt format type_enc lifted sym_tab) #> map_proof_terms (infer_formulas_types ctxt #> map HOLogic.mk_Trueprop) #> local_prover = waldmeisterN ? repair_waldmeister_endgame fun unskolemize_spass_term skos = let val is_skolem_name = member (op =) skos fun find_argless_skolem (Free _ $ Var _) = NONE | find_argless_skolem (Free (x as (s, _))) = if is_skolem_name s then SOME x else NONE | find_argless_skolem (t $ u) = (case find_argless_skolem t of NONE => find_argless_skolem u | sk => sk) | find_argless_skolem (Abs (_, _, t)) = find_argless_skolem t | find_argless_skolem _ = NONE fun find_skolem_arg (Free (s, _) $ Var v) = if is_skolem_name s then SOME v else NONE | find_skolem_arg (t $ u) = (case find_skolem_arg t of NONE => find_skolem_arg u | v => v) | find_skolem_arg (Abs (_, _, t)) = find_skolem_arg t | find_skolem_arg _ = NONE fun kill_skolem_arg (t as Free (s, T) $ Var _) = if is_skolem_name s then Free (s, range_type T) else t | kill_skolem_arg (t $ u) = kill_skolem_arg t $ kill_skolem_arg u | kill_skolem_arg (Abs (s, T, t)) = Abs (s, T, kill_skolem_arg t) | kill_skolem_arg t = t fun find_var (Var v) = SOME v | find_var (t $ u) = (case find_var t of NONE => find_var u | v => v) | find_var (Abs (_, _, t)) = find_var t | find_var _ = NONE val safe_abstract_over = abstract_over o apsnd (incr_boundvars 1) fun unskolem_inner t = (case find_argless_skolem t of SOME (x as (s, T)) => HOLogic.exists_const T $ Abs (s, T, unskolem_inner (safe_abstract_over (Free x, t))) | NONE => (case find_skolem_arg t of SOME (v as ((s, _), T)) => let val (haves, have_nots) = HOLogic.disjuncts t |> List.partition (exists_subterm (curry (op =) (Var v))) |> apply2 (fn lits => fold (curry s_disj) lits \<^term>\False\) in s_disj (HOLogic.all_const T $ Abs (s, T, unskolem_inner (safe_abstract_over (Var v, kill_skolem_arg haves))), unskolem_inner have_nots) end | NONE => (case find_var t of SOME (v as ((s, _), T)) => HOLogic.all_const T $ Abs (s, T, unskolem_inner (safe_abstract_over (Var v, t))) | NONE => t))) fun unskolem_outer (@{const Trueprop} $ t) = @{const Trueprop} $ unskolem_outer t | unskolem_outer t = unskolem_inner t in unskolem_outer end fun rename_skolem_args t = let fun add_skolem_args (Abs (_, _, t)) = add_skolem_args t | add_skolem_args t = (case strip_comb t of (Free (s, _), args as _ :: _) => if String.isPrefix spass_skolem_prefix s then insert (op =) (s, take_prefix is_Var args) else fold add_skolem_args args | (u, args as _ :: _) => fold add_skolem_args (u :: args) | _ => I) fun subst_of_skolem (sk, args) = map_index (fn (j, Var (z, T)) => (z, Var ((sk ^ "_" ^ string_of_int j, 0), T))) args val subst = maps subst_of_skolem (add_skolem_args t []) in subst_vars ([], subst) t end fun introduce_spass_skolems proof = let fun add_skolem (Free (s, _)) = String.isPrefix spass_skolem_prefix s ? insert (op =) s | add_skolem _ = I (* union-find would be faster *) fun add_cycle [] = I | add_cycle ss = fold (fn s => Graph.default_node (s, ())) ss #> fold Graph.add_edge (ss ~~ tl ss @ [hd ss]) val (input_steps, other_steps) = List.partition (null o #5) proof (* The names of the formulas are added to the Skolem constants, to ensure that formulas giving rise to several clauses are skolemized together. *) val skoXss = map (fn ((_, ss), _, t, _, _) => Term.fold_aterms add_skolem t ss) input_steps val groups0 = Graph.strong_conn (fold add_cycle skoXss Graph.empty) val groups = filter (exists (String.isPrefix spass_skolem_prefix)) groups0 val skoXss_input_steps = skoXss ~~ input_steps fun step_name_of_group skoXs = (implode skoXs, []) fun in_group group = member (op =) group o hd fun group_of skoX = find_first (fn group => in_group group skoX) groups fun new_steps (skoXss_steps : (string list * (term, 'a) atp_step) list) group = let val name = step_name_of_group group val name0 = name |>> prefix "0" val t = (case map (snd #> #3) skoXss_steps of [t] => t | ts => ts |> map (HOLogic.dest_Trueprop #> rename_skolem_args) |> Library.foldr1 s_conj |> HOLogic.mk_Trueprop) val skos = fold (union (op =) o filter (String.isPrefix spass_skolem_prefix) o fst) skoXss_steps [] val deps = map (snd #> #1) skoXss_steps in [(name0, Unknown, unskolemize_spass_term skos t, spass_pre_skolemize_rule, deps), (name, Unknown, t, spass_skolemize_rule, [name0])] end val sko_steps = maps (fn group => new_steps (filter (in_group group o fst) skoXss_input_steps) group) groups val old_news = map_filter (fn (skoXs, (name, _, _, _, _)) => Option.map (pair name o single o step_name_of_group) (group_of skoXs)) skoXss_input_steps val repair_deps = fold replace_dependencies_in_line old_news in input_steps @ sko_steps @ map repair_deps other_steps end fun factify_atp_proof facts hyp_ts concl_t atp_proof = let fun factify_step ((num, ss), role, t, rule, deps) = let val (ss', role', t') = (case resolve_conjectures ss of [j] => if j = length hyp_ts then ([], Conjecture, concl_t) else ([], Hypothesis, close_form (nth hyp_ts j)) | _ => (case resolve_facts facts (num :: ss) of [] => (ss, if member (op =) [Definition, Lemma] role then role else Plain, t) | facts => (map fst facts, Axiom, t))) in ((num, ss'), role', t', rule, deps) end val atp_proof = map factify_step atp_proof val names = map #1 atp_proof fun repair_dep (num, ss) = (num, the_default ss (AList.lookup (op =) names num)) fun repair_deps (name, role, t, rule, deps) = (name, role, t, rule, map repair_dep deps) in map repair_deps atp_proof end fun termify_atp_abduce_candidate ctxt local_prover format type_enc pool lifted sym_tab phi = let val proof = [(("", []), Conjecture, mk_anot phi, "", [])] val new_proof = termify_atp_proof ctxt local_prover format type_enc pool lifted sym_tab proof in (case new_proof of [(_, _, phi', _, _)] => phi' | _ => error "Impossible case in termify_atp_abduce_candidate") end fun sort_top n scored_items = if n <= 0 orelse null scored_items then [] else let fun split_min accum [] (_, best_item) = (best_item, List.rev accum) | split_min accum ((score, item) :: scored_items) (best_score, best_item) = if score < best_score then split_min ((best_score, best_item) :: accum) scored_items (score, item) else split_min ((score, item) :: accum) scored_items (best_score, best_item) val (min_item, other_scored_items) = split_min [] (tl scored_items) (hd scored_items) in min_item :: sort_top (n - 1) (filter_out (equal min_item o snd) other_scored_items) |> distinct (op aconv) end fun top_abduce_candidates max_candidates candidates = let (* We prefer free variables to other constructs, so that e.g. "x \ y" is prioritized over "x \ 0". *) fun score t = Term.fold_aterms (fn t => fn score => score + (case t of Free _ => 1 | _ => 2)) t 0 (* Equations of the form "x = ..." or "... = x" or similar are too specific to be useful. Quantified formulas are also filtered out. As for "True", it may seem an odd choice for abduction, but it sometimes arises in conjunction with type class constraints, which are removed by the termifier. *) fun maybe_score t = (case t of @{prop True} => NONE | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Free _ $ _) => NONE | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ _ $ Free _) => NONE | @{const Trueprop} $ (@{const less(nat)} $ _ $ @{const zero_class.zero(nat)}) => NONE | @{const Trueprop} $ (@{const less_eq(nat)} $ _ $ @{const zero_class.zero(nat)}) => NONE | @{const Trueprop} $ (@{const less(nat)} $ _ $ @{const one_class.one(nat)}) => NONE | @{const Trueprop} $ (@{const Not} $ (@{const less(nat)} $ @{const zero_class.zero(nat)} $ _)) => NONE | @{const Trueprop} $ (@{const Not} $ (@{const less_eq(nat)} $ @{const zero_class.zero(nat)} $ _)) => NONE | @{const Trueprop} $ (@{const Not} $ (@{const less_eq(nat)} $ @{const one_class.one(nat)} $ _)) => NONE | @{const Trueprop} $ (Const (@{const_name All}, _) $ _) => NONE | @{const Trueprop} $ (Const (@{const_name Ex}, _) $ _) => NONE | _ => SOME (score t, t)) in sort_top max_candidates (map_filter maybe_score candidates) end end; diff --git a/src/HOL/Tools/ATP/atp_util.ML b/src/HOL/Tools/ATP/atp_util.ML --- a/src/HOL/Tools/ATP/atp_util.ML +++ b/src/HOL/Tools/ATP/atp_util.ML @@ -1,424 +1,423 @@ (* Title: HOL/Tools/ATP/atp_util.ML Author: Jasmin Blanchette, TU Muenchen General-purpose functions used by the ATP module. *) signature ATP_UTIL = sig val timestamp : unit -> string val hashw : word * word -> word val hashw_string : string * word -> word val hash_string : string -> int val chunk_list : int -> 'a list -> 'a list list val stringN_of_int : int -> int -> string val strip_spaces : bool -> (char -> bool) -> string -> string val strip_spaces_except_between_idents : string -> string val elide_string : int -> string -> string val find_enclosed : string -> string -> string -> string list val nat_subscript : int -> string val unquote_tvar : string -> string val maybe_quote : Keyword.keywords -> string -> string val string_of_ext_time : bool * Time.time -> string val string_of_time : Time.time -> string val type_instance : theory -> typ -> typ -> bool val type_generalization : theory -> typ -> typ -> bool val type_intersect : theory -> typ -> typ -> bool val type_equiv : theory -> typ * typ -> bool val varify_type : Proof.context -> typ -> typ val instantiate_type : theory -> typ -> typ -> typ -> typ val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ val is_type_surely_finite : Proof.context -> typ -> bool val is_type_surely_infinite : Proof.context -> bool -> typ list -> typ -> bool val s_not : term -> term val s_conj : term * term -> term val s_disj : term * term -> term val s_imp : term * term -> term val s_iff : term * term -> term val close_form : term -> term val hol_close_form_prefix : string val hol_close_form : term -> term val hol_open_form : (string -> string) -> term -> term val eta_expand : typ list -> term -> int -> term val cong_extensionalize_term : Proof.context -> term -> term val abs_extensionalize_term : Proof.context -> term -> term val unextensionalize_def : term -> term val transform_elim_prop : term -> term val specialize_type : theory -> (string * typ) -> term -> term val strip_subgoal : thm -> int -> Proof.context -> (string * typ) list * term list * term val extract_lambda_def : (term -> string * typ) -> term -> string * term val short_thm_name : Proof.context -> thm -> string val map_prod : ('a -> 'b) -> ('c -> 'd) -> 'a * 'c -> 'b * 'd val compare_length_with : 'a list -> int -> order end; structure ATP_Util : ATP_UTIL = struct fun timestamp_format time = Date.fmt "%Y-%m-%d %H:%M:%S." (Date.fromTimeLocal time) ^ (StringCvt.padLeft #"0" 3 (string_of_int (Time.toMilliseconds time - 1000 * Time.toSeconds time))) val timestamp = timestamp_format o Time.now (* This hash function is recommended in "Compilers: Principles, Techniques, and - Tools" by Aho, Sethi, and Ullman. The "hashpjw" function, which they - particularly recommend, triggers a bug in versions of Poly/ML up to 4.2.0. *) + Tools" by Aho, Sethi, and Ullman. *) fun hashw (u, w) = Word.+ (u, Word.* (0w65599, w)) fun hashw_char (c, w) = hashw (Word.fromInt (Char.ord c), w) fun hashw_string (s : string, w) = CharVector.foldl hashw_char w s fun hash_string s = Word.toInt (hashw_string (s, 0w0)) fun chunk_list _ [] = [] | chunk_list k xs = let val (xs1, xs2) = chop k xs in xs1 :: chunk_list k xs2 end fun stringN_of_int 0 _ = "" | stringN_of_int k n = stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10) fun is_spaceish c = Char.isSpace c orelse c = #"\127" (* DEL -- no idea where these come from *) fun strip_spaces skip_comments is_evil = let fun strip_c_style_comment [] accum = accum | strip_c_style_comment (#"*" :: #"/" :: cs) accum = strip_spaces_in_list true cs accum | strip_c_style_comment (_ :: cs) accum = strip_c_style_comment cs accum and strip_spaces_in_list _ [] accum = accum | strip_spaces_in_list true (#"%" :: cs) accum = strip_spaces_in_list true (cs |> drop_prefix (not_equal #"\n")) accum | strip_spaces_in_list true (#"/" :: #"*" :: cs) accum = strip_c_style_comment cs accum | strip_spaces_in_list _ [c1] accum = accum |> not (is_spaceish c1) ? cons c1 | strip_spaces_in_list skip_comments (cs as [_, _]) accum = accum |> fold (strip_spaces_in_list skip_comments o single) cs | strip_spaces_in_list skip_comments (c1 :: c2 :: c3 :: cs) accum = if is_spaceish c1 then strip_spaces_in_list skip_comments (c2 :: c3 :: cs) accum else if is_spaceish c2 then if is_spaceish c3 then strip_spaces_in_list skip_comments (c1 :: c3 :: cs) accum else strip_spaces_in_list skip_comments (c3 :: cs) (c1 :: accum |> forall is_evil [c1, c3] ? cons #" ") else strip_spaces_in_list skip_comments (c2 :: c3 :: cs) (cons c1 accum) in String.explode #> rpair [] #-> strip_spaces_in_list skip_comments #> rev #> String.implode end fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" val strip_spaces_except_between_idents = strip_spaces true is_ident_char fun elide_string threshold s = if size s > threshold then String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^ String.extract (s, size s - (threshold + 1) div 2 + 6, NONE) else s fun find_enclosed left right s = case first_field left s of SOME (_, s) => (case first_field right s of SOME (enclosed, s) => enclosed :: find_enclosed left right s | NONE => []) | NONE => [] val subscript = implode o map (prefix "\<^sub>") o raw_explode (* FIXME Symbol.explode (?) *) fun nat_subscript n = n |> string_of_int |> not (print_mode_active Print_Mode.ASCII) ? subscript val unquote_tvar = perhaps (try (unprefix "'")) val unquery_var = perhaps (try (unprefix "?")) val is_long_identifier = forall Symbol_Pos.is_identifier o Long_Name.explode fun maybe_quote keywords y = let val s = YXML.content_of y in y |> ((not (is_long_identifier (unquote_tvar s)) andalso not (is_long_identifier (unquery_var s))) orelse Keyword.is_literal keywords s) ? quote end fun string_of_ext_time (plus, time) = let val us = Time.toMicroseconds time in (if plus then "> " else "") ^ (if us < 1000 then string_of_real (Real.fromInt (us div 100) / 10.0) ^ " ms" else if us < 1000000 then signed_string_of_int (us div 1000) ^ " ms" else string_of_real (Real.fromInt (us div 100000) / 10.0) ^ " s") end val string_of_time = string_of_ext_time o pair false fun type_instance thy T T' = Sign.typ_instance thy (T, T') fun type_generalization thy T T' = Sign.typ_instance thy (T', T) fun type_intersect _ (TVar _) _ = true | type_intersect _ _ (TVar _) = true | type_intersect thy T T' = let val tvars = Term.add_tvar_namesT T [] val tvars' = Term.add_tvar_namesT T' [] val maxidx' = maxidx_of_typ T' val T = T |> exists (member (op =) tvars') tvars ? Logic.incr_tvar (maxidx' + 1) val maxidx = Integer.max (maxidx_of_typ T) maxidx' in can (Sign.typ_unify thy (T, T')) (Vartab.empty, maxidx) end val type_equiv = Sign.typ_equiv fun varify_type ctxt T = Variable.polymorphic_types ctxt [Const (\<^const_name>\undefined\, T)] |> snd |> the_single |> dest_Const |> snd (* TODO: use "Term_Subst.instantiateT" instead? *) fun instantiate_type thy T1 T1' T2 = Same.commit (Envir.subst_type_same (Sign.typ_match thy (T1, T1') Vartab.empty)) T2 handle Type.TYPE_MATCH => raise TYPE ("instantiate_type", [T1, T1'], []) fun varify_and_instantiate_type ctxt T1 T1' T2 = let val thy = Proof_Context.theory_of ctxt in instantiate_type thy (varify_type ctxt T1) T1' (varify_type ctxt T2) end fun free_constructors_of ctxt (Type (s, Ts)) = (case Ctr_Sugar.ctr_sugar_of ctxt s of SOME {ctrs, ...} => map_filter (try dest_Const o Ctr_Sugar.mk_ctr Ts) ctrs | NONE => []) | free_constructors_of _ _ = [] (* Similar to "Nitpick_HOL.bounded_exact_card_of_type". 0 means infinite type, 1 means singleton type (e.g., "unit"), and 2 means cardinality 2 or more. The specified default cardinality is returned if the cardinality of the type can't be determined. *) fun tiny_card_of_type ctxt sound assigns default_card T = let val thy = Proof_Context.theory_of ctxt val max = 2 (* 1 would be too small for the "fun" case *) fun aux slack avoid T = if member (op =) avoid T then 0 else case AList.lookup (type_equiv thy) assigns T of SOME k => k | NONE => case T of Type (\<^type_name>\fun\, [T1, T2]) => (case (aux slack avoid T1, aux slack avoid T2) of (k, 1) => if slack andalso k = 0 then 0 else 1 | (0, _) => 0 | (_, 0) => 0 | (k1, k2) => if k1 >= max orelse k2 >= max then max else Int.min (max, Integer.pow k2 k1)) | Type (\<^type_name>\set\, [T']) => aux slack avoid (T' --> \<^typ>\bool\) | \<^typ>\prop\ => 2 | \<^typ>\bool\ => 2 (* optimization *) | \<^typ>\nat\ => 0 (* optimization *) | Type ("Int.int", []) => 0 (* optimization *) | Type (s, _) => (case free_constructors_of ctxt T of constrs as _ :: _ => let val constr_cards = map (Integer.prod o map (aux slack (T :: avoid)) o binder_types o snd) constrs in if exists (curry (op =) 0) constr_cards then 0 else Int.min (max, Integer.sum constr_cards) end | [] => case Typedef.get_info ctxt s of ({abs_type, rep_type, ...}, _) :: _ => if not sound then (* We cheat here by assuming that typedef types are infinite if their underlying type is infinite. This is unsound in general but it's hard to think of a realistic example where this would not be the case. We are also slack with representation types: If a representation type has the form "sigma => tau", we consider it enough to check "sigma" for infiniteness. *) (case varify_and_instantiate_type ctxt (Logic.varifyT_global abs_type) T (Logic.varifyT_global rep_type) |> aux true avoid of 0 => 0 | 1 => 1 | _ => default_card) else default_card | [] => default_card) | TFree _ => (* Very slightly unsound: Type variables are assumed not to be constrained to cardinality 1. (In practice, the user would most likely have used "unit" directly anyway.) *) if not sound andalso default_card = 1 then 2 else default_card | TVar _ => default_card in Int.min (max, aux false [] T) end fun is_type_surely_finite ctxt T = tiny_card_of_type ctxt true [] 0 T <> 0 fun is_type_surely_infinite ctxt sound infinite_Ts T = tiny_card_of_type ctxt sound (map (rpair 0) infinite_Ts) 1 T = 0 (* Simple simplifications to ensure that sort annotations don't leave a trail of spurious "True"s. *) fun s_not \<^Const_>\All T for \Abs (s, T', t')\\ = \<^Const>\Ex T for \Abs (s, T', s_not t')\\ | s_not \<^Const_>\Ex T for \Abs (s, T', t')\\ = \<^Const>\All T for \Abs (s, T', s_not t')\\ | s_not \<^Const_>\implies for t1 t2\ = \<^Const>\conj for t1 \s_not t2\\ | s_not \<^Const_>\conj for t1 t2\ = \<^Const>\disj for \s_not t1\ \s_not t2\\ | s_not \<^Const_>\disj for t1 t2\ = \<^Const>\conj for \s_not t1\ \s_not t2\\ | s_not \<^Const_>\False\ = \<^Const>\True\ | s_not \<^Const_>\True\ = \<^Const>\False\ | s_not \<^Const_>\Not for t\ = t | s_not t = \<^Const>\Not for t\ fun s_conj (\<^Const_>\True\, t2) = t2 | s_conj (t1, \<^Const_>\True\) = t1 | s_conj (\<^Const_>\False\, _) = \<^Const>\False\ | s_conj (_, \<^Const_>\False\) = \<^Const>\False\ | s_conj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_conj (t1, t2) fun s_disj (\<^Const_>\False\, t2) = t2 | s_disj (t1, \<^Const_>\False\) = t1 | s_disj (\<^Const_>\True\, _) = \<^Const>\True\ | s_disj (_, \<^Const_>\True\) = \<^Const>\True\ | s_disj (t1, t2) = if t1 aconv t2 then t1 else HOLogic.mk_disj (t1, t2) fun s_imp (\<^Const_>\True\, t2) = t2 | s_imp (t1, \<^Const_>\False\) = s_not t1 | s_imp (\<^Const_>\False\, _) = \<^Const>\True\ | s_imp (_, \<^Const_>\True\) = \<^Const>\True\ | s_imp p = HOLogic.mk_imp p fun s_iff (\<^Const_>\True\, t2) = t2 | s_iff (t1, \<^Const_>\True\) = t1 | s_iff (\<^Const_>\False\, t2) = s_not t2 | s_iff (t1, \<^Const_>\False\) = s_not t1 | s_iff (t1, t2) = if t1 aconv t2 then \<^Const>\True\ else HOLogic.eq_const HOLogic.boolT $ t1 $ t2 fun close_form t = fold (fn ((s, i), T) => fn t' => Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t'))) (Term.add_vars t []) t val hol_close_form_prefix = "ATP." fun hol_close_form t = fold (fn ((s, i), T) => fn t' => HOLogic.all_const T $ Abs (hol_close_form_prefix ^ s, T, abstract_over (Var ((s, i), T), t'))) (Term.add_vars t []) t fun hol_open_form unprefix (t as Const (\<^const_name>\All\, _) $ Abs (s, T, t')) = (case try unprefix s of SOME s => let val names = Name.make_context (map fst (Term.add_var_names t' [])) val (s, _) = Name.variant s names in hol_open_form unprefix (subst_bound (Var ((s, 0), T), t')) end | NONE => t) | hol_open_form _ t = t fun eta_expand _ t 0 = t | eta_expand Ts (Abs (s, T, t')) n = Abs (s, T, eta_expand (T :: Ts) t' (n - 1)) | eta_expand Ts t n = fold_rev (fn T => fn t' => Abs ("x" ^ nat_subscript n, T, t')) (List.take (binder_types (fastype_of1 (Ts, t)), n)) (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0))) fun cong_extensionalize_term ctxt t = if exists_Const (fn (s, _) => s = \<^const_name>\Not\) t then t |> Skip_Proof.make_thm (Proof_Context.theory_of ctxt) |> Meson.cong_extensionalize_thm ctxt |> Thm.prop_of else t fun is_fun_equality (\<^const_name>\HOL.eq\, Type (_, [Type (\<^type_name>\fun\, _), _])) = true | is_fun_equality _ = false fun abs_extensionalize_term ctxt t = if exists_Const is_fun_equality t then t |> Thm.cterm_of ctxt |> Meson.abs_extensionalize_conv ctxt |> Thm.prop_of |> Logic.dest_equals |> snd else t fun unextensionalize_def t = (case t of \<^Const_>\Trueprop for \<^Const_>\HOL.eq _ for lhs rhs\\ => (case strip_comb lhs of (c as Const (_, T), args) => if forall is_Var args andalso not (has_duplicates (op =) args) then \<^Const>\Trueprop for \<^Const>\HOL.eq T for c \fold_rev lambda args rhs\\\ else t | _ => t) | _ => t) (* Converts an elim-rule into an equivalent theorem that does not have the predicate variable. Leaves other theorems unchanged. We simply instantiate the conclusion variable to "False". (Cf. "transform_elim_theorem" in "Meson_Clausify".) *) fun transform_elim_prop t = case Logic.strip_imp_concl t of \<^Const_>\Trueprop for \Var (z, \<^typ>\bool\)\\ => subst_Vars [(z, \<^Const>\False\)] t | Var (z, \<^Type>\prop\) => subst_Vars [(z, \<^prop>\False\)] t | _ => t fun specialize_type thy (s, T) t = let fun subst_for (Const (s', T')) = if s = s' then SOME (Sign.typ_match thy (T', T) Vartab.empty) handle Type.TYPE_MATCH => NONE else NONE | subst_for (t1 $ t2) = (case subst_for t1 of SOME x => SOME x | NONE => subst_for t2) | subst_for (Abs (_, _, t')) = subst_for t' | subst_for _ = NONE in (case subst_for t of SOME subst => Envir.subst_term_types subst t | NONE => raise Type.TYPE_MATCH) end fun strip_subgoal goal i ctxt = let val (t, (frees, params)) = Logic.goal_params (Thm.prop_of goal) i ||> (map dest_Free #> Variable.variant_frees ctxt [] #> `(map Free)) val hyp_ts = t |> Logic.strip_assums_hyp |> map (curry subst_bounds frees) val concl_t = t |> Logic.strip_assums_concl |> curry subst_bounds frees in (rev params, hyp_ts, concl_t) end fun extract_lambda_def dest_head (Const (\<^const_name>\HOL.eq\, _) $ t $ u) = let val (head, args) = strip_comb t in (head |> dest_head |> fst, fold_rev (fn t as Var ((s, _), T) => (fn u => Abs (s, T, abstract_over (t, u))) | _ => raise Fail "expected \"Var\"") args u) end | extract_lambda_def _ _ = raise Fail "malformed lifted lambda" fun short_thm_name ctxt th = let val long = Thm.get_name_hint th val short = Long_Name.base_name long in (case try (singleton (Attrib.eval_thms ctxt)) (Facts.named short, []) of SOME th' => if Thm.eq_thm_prop (th, th') then short else long | _ => long) end val map_prod = Ctr_Sugar_Util.map_prod -(* Compare the length of a list with an integer n while traversing at most n elements of the list. -*) +(* Compare the length of a list with an integer n while traversing at most n +elements of the list. *) fun compare_length_with [] n = if n < 0 then GREATER else if n = 0 then EQUAL else LESS | compare_length_with (_ :: xs) n = if n <= 0 then GREATER else compare_length_with xs (n - 1) end; diff --git a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML @@ -1,364 +1,372 @@ (* Title: HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Author: Fabian Immler, TU Muenchen Author: Makarius Author: Jasmin Blanchette, TU Muenchen ATPs as Sledgehammer provers. *) signature SLEDGEHAMMER_PROVER_ATP = sig type mode = Sledgehammer_Prover.mode type prover = Sledgehammer_Prover.prover val atp_problem_dest_dir : string Config.T val atp_proof_dest_dir : string Config.T val atp_problem_prefix : string Config.T val atp_completish : int Config.T val atp_full_names : bool Config.T val run_atp : mode -> string -> prover end; structure Sledgehammer_Prover_ATP : SLEDGEHAMMER_PROVER_ATP = struct open ATP_Util open ATP_Problem open ATP_Problem_Generate open ATP_Proof open ATP_Proof_Reconstruct open Sledgehammer_Util open Sledgehammer_Proof_Methods open Sledgehammer_Isar open Sledgehammer_ATP_Systems open Sledgehammer_Prover (* Empty string means create files in Isabelle's temporary files directory. *) val atp_problem_dest_dir = Attrib.setup_config_string \<^binding>\sledgehammer_atp_problem_dest_dir\ (K "") val atp_proof_dest_dir = Attrib.setup_config_string \<^binding>\sledgehammer_atp_proof_dest_dir\ (K "") val atp_problem_prefix = Attrib.setup_config_string \<^binding>\sledgehammer_atp_problem_prefix\ (K "prob") val atp_completish = Attrib.setup_config_int \<^binding>\sledgehammer_atp_completish\ (K 0) (* In addition to being easier to read, readable names are often much shorter, especially if types are mangled in names. This makes a difference for some provers (e.g., E). For these reason, short names are enabled by default. *) val atp_full_names = Attrib.setup_config_bool \<^binding>\sledgehammer_atp_full_names\ (K false) fun choose_type_enc strictness format good_type_enc = type_enc_of_string strictness good_type_enc |> adjust_type_enc format fun has_bound_or_var_of_type pred = exists_subterm (fn Var (_, T as Type _) => pred T | Abs (_, T as Type _, _) => pred T | _ => false) (* Unwanted equalities are those between a (bound or schematic) variable that does not properly occur in the second operand. *) val is_exhaustive_finite = let fun is_bad_equal (Var z) t = not (exists_subterm (fn Var z' => z = z' | _ => false) t) | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j)) | is_bad_equal _ _ = false fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1 fun do_formula pos t = (case (pos, t) of (_, \<^Const_>\Trueprop for t1\) => do_formula pos t1 | (true, Const (\<^const_name>\Pure.all\, _) $ Abs (_, _, t')) => do_formula pos t' | (true, Const (\<^const_name>\All\, _) $ Abs (_, _, t')) => do_formula pos t' | (false, Const (\<^const_name>\Ex\, _) $ Abs (_, _, t')) => do_formula pos t' | (_, \<^Const_>\Pure.imp for t1 t2\) => do_formula (not pos) t1 andalso (t2 = \<^prop>\False\ orelse do_formula pos t2) | (_, \<^Const_>\implies for t1 t2\) => do_formula (not pos) t1 andalso (t2 = \<^Const>\False\ orelse do_formula pos t2) | (_, \<^Const_>\Not for t1\) => do_formula (not pos) t1 | (true, \<^Const_>\disj for t1 t2\) => forall (do_formula pos) [t1, t2] | (false, \<^Const_>\conj for t1 t2\) => forall (do_formula pos) [t1, t2] | (true, Const (\<^const_name>\HOL.eq\, _) $ t1 $ t2) => do_equals t1 t2 | (true, Const (\<^const_name>\Pure.eq\, _) $ t1 $ t2) => do_equals t1 t2 | _ => false) in do_formula true end (* Facts containing variables of finite types such as "unit" or "bool" or of the form "ALL x. x = A | x = B | x = C" are likely to lead to untypable proofs for unsound type encodings. *) fun is_dangerous_prop ctxt = transform_elim_prop #> (has_bound_or_var_of_type (is_type_surely_finite ctxt) orf is_exhaustive_finite) val mono_max_privileged_facts = 10 fun suffix_of_mode Auto_Try = "_try" | suffix_of_mode Try = "_try" | suffix_of_mode Normal = "" | suffix_of_mode MaSh = "" | suffix_of_mode Minimize = "_min" (* Important messages are important but not so important that users want to see them each time. *) val important_message_keep_quotient = 25 fun run_atp mode name ({debug, verbose, overlord, abduce = abduce_max_candidates, strict, max_mono_iters, max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, minimize, slices, timeout, preplay_timeout, spy, ...} : params) ({comment, state, goal, subgoal, subgoal_count, factss, has_already_found_something, found_something} : prover_problem) slice = let val (basic_slice as (slice_size, abduce, _, _, _), ATP_Slice (good_format, good_type_enc, good_lam_trans, good_uncurried_aliases, extra)) = slice val facts = facts_of_basic_slice basic_slice factss val thy = Proof.theory_of state val ctxt = Proof.context_of state val {exec, arguments, proof_delims, known_failures, prem_role, generate_isabelle_info, good_max_mono_iters, good_max_new_mono_instances, ...} = get_atp thy name () val full_proofs = isar_proofs |> the_default (mode = Minimize) val local_name = perhaps (try (unprefix remote_prefix)) name val completish = Config.get ctxt atp_completish val atp_mode = if completish > 0 then Sledgehammer_Completish completish else Sledgehammer val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt val (problem_dest_dir, proof_dest_dir, problem_prefix) = if overlord then overlord_file_location_of_prover name |> (fn (dir, prefix) => (dir, dir, prefix)) else (Config.get ctxt atp_problem_dest_dir, Config.get ctxt atp_proof_dest_dir, Config.get ctxt atp_problem_prefix) val problem_file_name = Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^ suffix_of_mode mode ^ "_" ^ string_of_int subgoal) |> Path.ext "p" val prob_path = if problem_dest_dir = "" then File.tmp_path problem_file_name else if File.exists (Path.explode problem_dest_dir) then Path.explode problem_dest_dir + problem_file_name else error ("No such directory: " ^ quote problem_dest_dir) val executable = (case find_first (fn var => getenv var <> "") (fst exec) of SOME var => let val pref = getenv var ^ "/" val paths = map (Path.explode o prefix pref) (if ML_System.platform_is_windows then map (suffix ".exe") (snd exec) @ snd exec else snd exec); in (case find_first File.exists paths of SOME path => path | NONE => error ("Bad executable: " ^ Path.print (hd paths))) end | NONE => error ("The environment variable " ^ quote (List.last (fst exec)) ^ " is not set")) fun run () = let fun monomorphize_facts facts = let val ctxt = ctxt |> repair_monomorph_context max_mono_iters good_max_mono_iters max_new_mono_instances good_max_new_mono_instances (* pseudo-theorem involving the same constants as the subgoal *) val subgoal_th = Logic.list_implies (hyp_ts, concl_t) |> Skip_Proof.make_thm thy val rths = facts |> chop mono_max_privileged_facts |>> map (pair 1 o snd) ||> map (pair 2 o snd) |> op @ |> cons (0, subgoal_th) in Monomorph.monomorph atp_schematic_consts_of ctxt rths |> tl |> curry ListPair.zip (map fst facts) |> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths) end val strictness = if strict then Strict else Non_Strict val type_enc = choose_type_enc strictness good_format good_type_enc val run_timeout = slice_timeout slice_size slices timeout val generous_run_timeout = if mode = MaSh then one_day else if abduce then run_timeout + seconds 5.0 else run_timeout val ({elapsed, ...}, atp_problem_data as (atp_problem, _, _, _)) = Timing.timing (fn () => let val readable_names = not (Config.get ctxt atp_full_names) in facts |> not (is_type_enc_sound type_enc) ? filter_out (is_dangerous_prop ctxt o Thm.prop_of o snd) |> not (is_type_enc_polymorphic type_enc) ? monomorphize_facts |> map (apsnd Thm.prop_of) |> generate_atp_problem ctxt generate_isabelle_info good_format prem_role type_enc atp_mode good_lam_trans good_uncurried_aliases readable_names true hyp_ts concl_t end) () val () = spying spy (fn () => (state, subgoal, name, "Generating ATP problem in " ^ string_of_int (Time.toMilliseconds elapsed) ^ " ms")) val args = arguments abduce full_proofs extra run_timeout prob_path val command = space_implode " " (File.bash_path executable :: args) fun run_command () = if exec = isabelle_scala_function then let val {output, timing} = SystemOnTPTP.run_system_encoded args in (output, timing) end else let val res = Isabelle_System.bash_process (Bash.script command |> Bash.redirect) in (Process_Result.out res, Process_Result.timing_elapsed res) end val _ = atp_problem |> lines_of_atp_problem good_format (fn () => atp_problem_term_order_info atp_problem) |> (exec <> isabelle_scala_function) ? cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n")) |> File.write_list prob_path val local_name = name |> perhaps (try (unprefix remote_prefix)) 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 false local_name atp_problem) handle UNRECOGNIZED_ATP_PROOF () => (([], ""), SOME ProofUnparsable))) handle Timeout.TIMEOUT _ => (("", run_timeout), (([], ""), SOME TimedOut)) | ERROR msg => (("", Time.zeroTime), (([], ""), SOME (UnknownError msg))) val atp_abduce_candidates = if abduce andalso outcome <> NONE andalso not (has_already_found_something ()) then atp_abduce_candidates_of_output local_name atp_problem output else [] val () = spying spy (fn () => (state, subgoal, name, "Running command in " ^ string_of_int (Time.toMilliseconds run_time) ^ " ms")) - val _ = + val outcome = (case outcome of - NONE => found_something name - | _ => ()) + NONE => + (case used_facts_in_unsound_atp_proof ctxt (map fst facts) atp_proof of + SOME facts => + let + val failure = UnsoundProof (is_type_enc_sound type_enc, sort string_ord facts) + in + if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure + end + | NONE => (found_something name; NONE)) + | _ => outcome) in (atp_problem_data, (output, run_time, facts, atp_problem, tstplike_proof, atp_proof, atp_abduce_candidates, 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, _, _, _, _, _, _, _), _) = let val proof_dest_dir_path = Path.explode proof_dest_dir val make_export_file_name = Path.split_ext #> apfst (Path.explode o suffix "_proof" o Path.implode) #> swap #> uncurry Path.ext in if proof_dest_dir = "" then Output.system_message "don't export proof" else if File.exists proof_dest_dir_path then File.write (proof_dest_dir_path + make_export_file_name problem_file_name) output else error ("No such directory: " ^ quote proof_dest_dir) end val ((_, pool, lifted, sym_tab), (output, run_time, used_from, atp_problem, tstplike_proof, atp_proof, atp_abduce_candidates, outcome), (format, type_enc)) = with_cleanup clean_up run () |> tap export val important_message = if mode = Normal andalso Random.random_range 0 (important_message_keep_quotient - 1) = 0 then extract_important_message output else "" val (outcome, used_facts, preferred_methss, message) = (case outcome of NONE => let val used_facts = sort_by fst (used_facts_in_atp_proof ctxt (map fst used_from) atp_proof) val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof val preferred = Metis_Method (NONE, NONE) val preferred_methss = (preferred, if try0 then bunches_of_proof_methods ctxt smt_proofs needs_full_types (if atp_proof_prefers_lifting atp_proof then liftingN else opaque_liftingN) else [[preferred]]) in (NONE, used_facts, preferred_methss, fn preplay => let val _ = if verbose then writeln "Generating proof text..." else () 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 full_atp_proof then SOME full_typesN else NONE val metis_lam_trans = 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, full_atp_proof, goal) end val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count) val num_chained = length (#facts (Proof.goal state)) in proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params ^ (if important_message <> "" then "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message else "") end) end | SOME failure => let val max_abduce_candidates = the_default default_abduce_max_candidates abduce_max_candidates val abduce_candidates = atp_abduce_candidates |> map (termify_atp_abduce_candidate ctxt name format type_enc pool lifted sym_tab) |> top_abduce_candidates max_abduce_candidates in if null abduce_candidates then (SOME failure, [], (Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure) else (NONE, [], (Auto_Method (* dummy *), []), fn _ => abduce_text ctxt abduce_candidates) end) in {outcome = outcome, used_facts = used_facts, used_from = used_from, preferred_methss = preferred_methss, run_time = run_time, message = message} end end;