# HG changeset patch # User blanchet # Date 1284642968 -7200 # Node ID 2416666e6f94820d29dc4b5a54163b0efa8cb35f # Parent 13c8577e1783026007d0bda2eb133492285a50b5 refactoring: move ATP proof and error extraction code to "ATP_Proof" module diff -r 13c8577e1783 -r 2416666e6f94 src/HOL/Tools/ATP/atp_proof.ML --- 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]) diff -r 13c8577e1783 -r 2416666e6f94 src/HOL/Tools/ATP/atp_systems.ML --- 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 ()) diff -r 13c8577e1783 -r 2416666e6f94 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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) diff -r 13c8577e1783 -r 2416666e6f94 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML --- 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 =