# HG changeset patch # User blanchet # Date 1502803705 -7200 # Node ID 745a43ff2d5f9a4fbab8c15474801c437b1a5438 # Parent d14e7666d785a97c28636f81dd0b24d6c0b11319 extended TSTP type parser + tuned messages diff -r d14e7666d785 -r 745a43ff2d5f src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Tue Aug 15 15:07:37 2017 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Aug 15 15:28:25 2017 +0200 @@ -173,41 +173,41 @@ "" val missing_message_tail = - " appears to be missing; you will need to install it if you want to invoke \ - \remote provers" + " appears to be missing. You will need to install it if you want to invoke \ + \remote provers." fun from_lemmas [] = "" | from_lemmas ss = " from " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) -fun string_of_atp_failure MaybeUnprovable = "The generated problem is maybe unprovable" - | string_of_atp_failure Unprovable = "The generated problem is unprovable" - | string_of_atp_failure GaveUp = "The prover gave up" +fun string_of_atp_failure MaybeUnprovable = "The generated problem is maybe unprovable." + | string_of_atp_failure Unprovable = "The generated problem is unprovable." + | string_of_atp_failure GaveUp = "The prover gave up." | string_of_atp_failure ProofMissing = - "The prover claims the conjecture is a theorem but did not provide a proof" + "The prover claims the conjecture is a theorem but did not provide a proof." | string_of_atp_failure ProofIncomplete = - "The prover claims the conjecture is a theorem but provided an incomplete proof" + "The prover claims the conjecture is a theorem but provided an incomplete proof." | string_of_atp_failure ProofUnparsable = - "The prover claims the conjecture is a theorem but provided an unparsable proof" + "The prover claims the conjecture is a theorem but provided an unparsable proof." | string_of_atp_failure (UnsoundProof (false, ss)) = "The prover derived \"False\"" ^ from_lemmas ss ^ - "; specify a sound type encoding or omit the \"type_enc\" option" + ". Specify a sound type encoding or omit the \"type_enc\" option." | string_of_atp_failure (UnsoundProof (true, ss)) = "The prover derived \"False\"" ^ from_lemmas ss ^ ", which could be due to inconsistent axioms (including \"sorry\"s) or to \ - \a bug in Sledgehammer" - | string_of_atp_failure CantConnect = "Cannot connect to server" - | string_of_atp_failure TimedOut = "Timed out" + \a bug in Sledgehammer." + | string_of_atp_failure CantConnect = "Cannot connect to server." + | string_of_atp_failure TimedOut = "Timed out." | string_of_atp_failure Inappropriate = - "The generated problem lies outside the prover's scope" - | string_of_atp_failure OutOfResources = "The prover ran out of resources" + "The generated problem lies outside the prover's scope." + | string_of_atp_failure OutOfResources = "The prover ran out of resources." | string_of_atp_failure NoPerl = "Perl" ^ missing_message_tail | string_of_atp_failure NoLibwwwPerl = "The Perl module \"libwww-perl\"" ^ missing_message_tail - | string_of_atp_failure MalformedInput = "The generated problem is malformed" - | string_of_atp_failure MalformedOutput = "The prover output is malformed" - | string_of_atp_failure Interrupted = "The prover was interrupted" - | string_of_atp_failure Crashed = "The prover crashed" - | string_of_atp_failure InternalError = "An internal prover error occurred" + | string_of_atp_failure MalformedInput = "The generated problem is malformed." + | string_of_atp_failure MalformedOutput = "The prover output is malformed." + | string_of_atp_failure Interrupted = "The prover was interrupted." + | string_of_atp_failure Crashed = "The prover crashed." + | string_of_atp_failure InternalError = "An internal prover error occurred." | string_of_atp_failure (UnknownError s) = "A prover error occurred" ^ (if s = "" then ". (Pass the \"verbose\" option for details.)" @@ -343,9 +343,13 @@ and parse_classes x = (parse_class ::: Scan.repeat ($$ "&" |-- parse_class)) x fun parse_type x = - (scan_general_id -- Scan.optional ($$ "{" |-- parse_classes --| $$ "}") [] - -- Scan.optional ($$ "(" |-- parse_types --| $$ ")") [] - >> AType) x + (($$ "(" |-- parse_type --| $$ ")" + || (scan_general_id -- Scan.optional ($$ "{" |-- parse_classes --| $$ "}") []) + -- Scan.optional ($$ "(" |-- parse_types --| $$ ")") [] + >> AType) + -- Scan.option ($$ tptp_fun_type |-- parse_type) + >> (fn (a, NONE) => a + | (a, SOME b) => AFun (a, b))) x and parse_types x = (parse_type ::: Scan.repeat ($$ "," |-- parse_type)) x (* We currently half ignore types. *) @@ -498,12 +502,6 @@ val parse_ho_quantifier = parse_one_in_list [tptp_ho_forall, tptp_ho_exists, tptp_hilbert_choice, tptp_hilbert_the] -fun parse_thf0_type x = - (($$ "(" |-- parse_thf0_type --| $$ ")" || scan_general_id >> (fn t => AType ((t, []), []))) - -- Scan.option ($$ tptp_fun_type |-- parse_thf0_type) - >> (fn (a, NONE) => a - | (a, SOME b) => AFun (a, b))) x - fun mk_ho_of_fo_quant q = if q = tptp_forall then tptp_ho_forall else if q = tptp_exists then tptp_ho_exists @@ -521,13 +519,13 @@ ATerm ((x, ty), map remove_thf_app arg) | remove_thf_app (AAbs (((x, ty), arg), t)) = AAbs (((x, ty), remove_thf_app arg), t) -fun parse_thf0_typed_var x = - (Scan.repeat (scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_thf0_type) +fun parse_typed_var x = + (Scan.repeat (scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_type) --| Scan.option (Scan.this_string ",")) - || $$ "(" |-- parse_thf0_typed_var --| $$ ")") x + || $$ "(" |-- parse_typed_var --| $$ ")") x fun parse_simple_thf0_term x = - (parse_fo_quantifier -- ($$ "[" |-- parse_thf0_typed_var --| $$ "]" --| $$ ":") -- parse_thf0_term + (parse_fo_quantifier -- ($$ "[" |-- parse_typed_var --| $$ "]" --| $$ ":") -- parse_thf0_term >> (fn ((q, ys), t) => fold_rev (fn (var, ty) => fn r => @@ -538,7 +536,7 @@ else I)) ys t) || Scan.this_string tptp_not |-- parse_thf0_term >> mk_app (mk_simple_aterm tptp_not) - || scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_thf0_type) + || scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_type) >> (fn (var, typ_opt) => ATerm ((var, the_list typ_opt), [])) || parse_ho_quantifier >> mk_simple_aterm || $$ "(" |-- parse_thf0_term --| $$ ")"