--- a/src/HOL/Tools/ATP/atp_proof.ML Thu Sep 16 14:26:09 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Thu Sep 16 15:16:08 2010 +0200
@@ -11,6 +11,12 @@
type 'a fo_term = 'a ATP_Problem.fo_term
type 'a uniform_formula = 'a ATP_Problem.uniform_formula
+ datatype failure =
+ Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
+ OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
+ MalformedInput | MalformedOutput | Interrupted | InternalError |
+ UnknownError
+
type step_name = string * string option
datatype 'a step =
@@ -20,6 +26,13 @@
type 'a proof = 'a uniform_formula step list
val strip_spaces : (char -> bool) -> string -> string
+ val string_for_failure : failure -> string
+ val extract_important_message : string -> string
+ val extract_known_failure :
+ (failure * string) list -> string -> failure option
+ val extract_tstplike_proof_and_outcome :
+ bool -> int -> (string * string) list -> (failure * string) list -> string
+ -> string * failure option
val is_same_step : step_name * step_name -> bool
val atp_proof_from_tstplike_string : string -> string proof
val map_term_names_in_atp_proof :
@@ -30,6 +43,13 @@
structure ATP_Proof : ATP_PROOF =
struct
+open ATP_Problem
+
+datatype failure =
+ Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
+ SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | MalformedInput |
+ MalformedOutput | Interrupted | InternalError | UnknownError
+
fun strip_spaces_in_list _ [] = []
| strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1]
| strip_spaces_in_list is_evil [c1, c2] =
@@ -51,7 +71,85 @@
fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char
-open ATP_Problem
+val missing_message_tail =
+ " appears to be missing. You will need to install it if you want to run \
+ \ATPs remotely."
+
+fun string_for_failure Unprovable = "The ATP problem is unprovable."
+ | string_for_failure IncompleteUnprovable =
+ "The ATP cannot prove the problem."
+ | string_for_failure CantConnect = "Can't connect to remote server."
+ | string_for_failure TimedOut = "Timed out."
+ | string_for_failure OutOfResources = "The ATP ran out of resources."
+ | string_for_failure SpassTooOld =
+ "Isabelle requires a more recent version of SPASS with support for the \
+ \TPTP syntax. To install it, download and extract the package \
+ \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
+ \\"spass-3.7\" directory's absolute path to " ^
+ quote (Path.implode (Path.expand (Path.appends
+ (Path.variable "ISABELLE_HOME_USER" ::
+ map Path.basic ["etc", "components"])))) ^
+ " on a line of its own."
+ | string_for_failure VampireTooOld =
+ "Isabelle requires a more recent version of Vampire. To install it, follow \
+ \the instructions from the Sledgehammer manual (\"isabelle doc\
+ \ sledgehammer\")."
+ | string_for_failure NoPerl = "Perl" ^ missing_message_tail
+ | string_for_failure NoLibwwwPerl =
+ "The Perl module \"libwww-perl\"" ^ missing_message_tail
+ | string_for_failure MalformedInput =
+ "The ATP problem is malformed. Please report this to the Isabelle \
+ \developers."
+ | string_for_failure MalformedOutput = "The ATP output is malformed."
+ | string_for_failure Interrupted = "The ATP was interrupted."
+ | string_for_failure InternalError = "An internal ATP error occurred."
+ | string_for_failure UnknownError = "An unknown ATP error occurred."
+
+fun extract_delimited (begin_delim, end_delim) output =
+ output |> first_field begin_delim |> the |> snd
+ |> first_field end_delim |> the |> fst
+ |> first_field "\n" |> the |> snd
+ handle Option.Option => ""
+
+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 pairself (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_failure known_failures output =
+ known_failures
+ |> find_first (fn (_, pattern) => String.isSubstring pattern output)
+ |> Option.map fst
+
+fun extract_tstplike_proof_and_outcome complete res_code proof_delims
+ known_failures output =
+ case extract_known_failure known_failures output of
+ NONE => (case extract_tstplike_proof proof_delims output of
+ "" => ("", SOME (if res_code = 0 andalso output = "" then
+ Interrupted
+ else
+ UnknownError))
+ | tstplike_proof => if res_code = 0 then (tstplike_proof, NONE)
+ else ("", SOME UnknownError))
+ | SOME failure =>
+ ("", SOME (if failure = IncompleteUnprovable andalso complete then
+ Unprovable
+ else
+ failure))
fun mk_anot (AConn (ANot, [phi])) = phi
| mk_anot phi = AConn (ANot, [phi])
--- a/src/HOL/Tools/ATP/atp_systems.ML Thu Sep 16 14:26:09 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Sep 16 15:16:08 2010 +0200
@@ -7,11 +7,7 @@
signature ATP_SYSTEMS =
sig
- datatype failure =
- Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
- OutOfResources | SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl |
- MalformedInput | MalformedOutput | Interrupted | InternalError |
- UnknownError
+ type failure = ATP_Proof.failure
type prover_config =
{exec: string * string,
@@ -24,9 +20,6 @@
explicit_forall: bool,
use_conjecture_for_hypotheses: bool}
- val string_for_failure : failure -> string
- val known_failure_in_output :
- string -> (failure * string) list -> failure option
val add_prover: string * prover_config -> theory -> theory
val get_prover: theory -> string -> prover_config
val available_atps: theory -> unit
@@ -38,12 +31,9 @@
structure ATP_Systems : ATP_SYSTEMS =
struct
-(* prover configuration *)
+open ATP_Proof
-datatype failure =
- Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
- SpassTooOld | VampireTooOld | NoPerl | NoLibwwwPerl | MalformedInput |
- MalformedOutput | Interrupted | InternalError | UnknownError
+(* prover configuration *)
type prover_config =
{exec: string * string,
@@ -56,44 +46,6 @@
explicit_forall: bool,
use_conjecture_for_hypotheses: bool}
-val missing_message_tail =
- " appears to be missing. You will need to install it if you want to run \
- \ATPs remotely."
-
-fun string_for_failure Unprovable = "The ATP problem is unprovable."
- | string_for_failure IncompleteUnprovable =
- "The ATP cannot prove the problem."
- | string_for_failure CantConnect = "Can't connect to remote server."
- | string_for_failure TimedOut = "Timed out."
- | string_for_failure OutOfResources = "The ATP ran out of resources."
- | string_for_failure SpassTooOld =
- "Isabelle requires a more recent version of SPASS with support for the \
- \TPTP syntax. To install it, download and extract the package \
- \\"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and add the \
- \\"spass-3.7\" directory's absolute path to " ^
- quote (Path.implode (Path.expand (Path.appends
- (Path.variable "ISABELLE_HOME_USER" ::
- map Path.basic ["etc", "components"])))) ^
- " on a line of its own."
- | string_for_failure VampireTooOld =
- "Isabelle requires a more recent version of Vampire. To install it, follow \
- \the instructions from the Sledgehammer manual (\"isabelle doc\
- \ sledgehammer\")."
- | string_for_failure NoPerl = "Perl" ^ missing_message_tail
- | string_for_failure NoLibwwwPerl =
- "The Perl module \"libwww-perl\"" ^ missing_message_tail
- | string_for_failure MalformedInput =
- "The ATP problem is malformed. Please report this to the Isabelle \
- \developers."
- | string_for_failure MalformedOutput = "The ATP output is malformed."
- | string_for_failure Interrupted = "The ATP was interrupted."
- | string_for_failure InternalError = "An internal ATP error occurred."
- | string_for_failure UnknownError = "An unknown ATP error occurred."
-
-fun known_failure_in_output output =
- find_first (fn (_, pattern) => String.isSubstring pattern output)
- #> Option.map fst
-
val known_perl_failures =
[(CantConnect, "HTTP error"),
(NoPerl, "env: perl"),
@@ -124,6 +76,7 @@
fun to_secs bonus time = (Time.toMilliseconds time + bonus + 999) div 1000
+
(* E prover *)
(* Give older versions of E an extra second, because the "eproof" script wrongly
@@ -163,6 +116,8 @@
val e = ("e", e_config)
+(* SPASS *)
+
(* The "-VarWeight=3" option helps the higher-order problems, probably by
counteracting the presence of "hAPP". *)
val spass_config : prover_config =
@@ -226,11 +181,11 @@
fun get_systems () =
case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
- (answer, 0) => split_lines answer
- | (answer, _) =>
- error (case known_failure_in_output answer known_perl_failures of
+ (output, 0) => split_lines output
+ | (output, _) =>
+ error (case extract_known_failure known_perl_failures output of
SOME failure => string_for_failure failure
- | NONE => perhaps (try (unsuffix "\n")) answer ^ ".")
+ | NONE => perhaps (try (unsuffix "\n")) output ^ ".")
fun refresh_systems_on_tptp () =
Synchronized.change systems (fn _ => get_systems ())
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Sep 16 14:26:09 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Sep 16 15:16:08 2010 +0200
@@ -62,6 +62,7 @@
struct
open ATP_Problem
+open ATP_Proof
open ATP_Systems
open Metis_Clauses
open Sledgehammer_Util
@@ -135,47 +136,6 @@
|> Exn.release
|> tap (after path)
-fun extract_delimited (begin_delim, end_delim) output =
- output |> first_field begin_delim |> the |> snd
- |> first_field end_delim |> the |> fst
- |> first_field "\n" |> the |> snd
- handle Option.Option => ""
-
-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 pairself (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_tstplike_proof_and_outcome complete res_code proof_delims
- known_failures output =
- case known_failure_in_output output known_failures of
- NONE => (case extract_tstplike_proof proof_delims output of
- "" => ("", SOME (if res_code = 0 andalso output = "" then
- Interrupted
- else
- UnknownError))
- | tstplike_proof => if res_code = 0 then (tstplike_proof, NONE)
- else ("", SOME UnknownError))
- | SOME failure =>
- ("", SOME (if failure = IncompleteUnprovable andalso complete then
- Unprovable
- else
- failure))
-
fun extract_clause_sequence output =
let
val tokens_of = String.tokens (not o Char.isAlphaNum)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Sep 16 14:26:09 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Sep 16 15:16:08 2010 +0200
@@ -20,7 +20,6 @@
structure Sledgehammer_Minimize : SLEDGEHAMMER_MINIMIZE =
struct
-open ATP_Systems
open Sledgehammer_Util
open Sledgehammer_Filter
open Sledgehammer_Translate
@@ -29,9 +28,9 @@
(* wrapper for calling external prover *)
-fun string_for_failure Unprovable = "Unprovable."
- | string_for_failure TimedOut = "Timed out."
- | string_for_failure Interrupted = "Interrupted."
+fun string_for_failure ATP_Proof.Unprovable = "Unprovable."
+ | string_for_failure ATP_Proof.TimedOut = "Timed out."
+ | string_for_failure ATP_Proof.Interrupted = "Interrupted."
| string_for_failure _ = "Unknown error."
fun n_theorems names =