--- 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 --| $$ ")"