src/HOL/Tools/ATP/atp_proof.ML
changeset 51998 f732a674db1b
parent 51881 475c2eab2d7c
child 52031 9a9238342963
equal deleted inserted replaced
51997:8dbe623a7804 51998:f732a674db1b
    39   type 'a step = step_name * formula_role * 'a * string * step_name list
    39   type 'a step = step_name * formula_role * 'a * string * step_name list
    40 
    40 
    41   type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list
    41   type 'a proof = ('a, 'a, ('a, 'a) ho_term, 'a) formula step list
    42 
    42 
    43   val short_output : bool -> string -> string
    43   val short_output : bool -> string -> string
    44   val string_for_failure : failure -> string
    44   val string_of_failure : failure -> string
    45   val extract_important_message : string -> string
    45   val extract_important_message : string -> string
    46   val extract_known_failure :
    46   val extract_known_failure :
    47     (failure * string) list -> string -> failure option
    47     (failure * string) list -> string -> failure option
    48   val extract_tstplike_proof_and_outcome :
    48   val extract_tstplike_proof_and_outcome :
    49     bool -> (string * string) list -> (failure * string) list -> string
    49     bool -> (string * string) list -> (failure * string) list -> string
   103 fun involving [] = ""
   103 fun involving [] = ""
   104   | involving ss =
   104   | involving ss =
   105     "involving " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) ^
   105     "involving " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) ^
   106     " "
   106     " "
   107 
   107 
   108 fun string_for_failure Unprovable = "The generated problem is unprovable."
   108 fun string_of_failure Unprovable = "The generated problem is unprovable."
   109   | string_for_failure GaveUp = "The prover gave up."
   109   | string_of_failure GaveUp = "The prover gave up."
   110   | string_for_failure ProofMissing =
   110   | string_of_failure ProofMissing =
   111     "The prover claims the conjecture is a theorem but did not provide a proof."
   111     "The prover claims the conjecture is a theorem but did not provide a proof."
   112   | string_for_failure ProofIncomplete =
   112   | string_of_failure ProofIncomplete =
   113     "The prover claims the conjecture is a theorem but provided an incomplete \
   113     "The prover claims the conjecture is a theorem but provided an incomplete \
   114     \(or unparsable) proof."
   114     \(or unparsable) proof."
   115   | string_for_failure (UnsoundProof (false, ss)) =
   115   | string_of_failure (UnsoundProof (false, ss)) =
   116     "The prover found an unsound proof " ^ involving ss ^
   116     "The prover found an unsound proof " ^ involving ss ^
   117     "(or, less likely, your axioms are inconsistent). Specify a sound type \
   117     "(or, less likely, your axioms are inconsistent). Specify a sound type \
   118     \encoding or omit the \"type_enc\" option."
   118     \encoding or omit the \"type_enc\" option."
   119   | string_for_failure (UnsoundProof (true, ss)) =
   119   | string_of_failure (UnsoundProof (true, ss)) =
   120     "The prover found an unsound proof " ^ involving ss ^
   120     "The prover found an unsound proof " ^ involving ss ^
   121     "(or, less likely, your axioms are inconsistent). Please report this to \
   121     "(or, less likely, your axioms are inconsistent). Please report this to \
   122     \the Isabelle developers."
   122     \the Isabelle developers."
   123   | string_for_failure CantConnect = "Cannot connect to remote server."
   123   | string_of_failure CantConnect = "Cannot connect to remote server."
   124   | string_for_failure TimedOut = "Timed out."
   124   | string_of_failure TimedOut = "Timed out."
   125   | string_for_failure Inappropriate =
   125   | string_of_failure Inappropriate =
   126     "The generated problem lies outside the prover's scope."
   126     "The generated problem lies outside the prover's scope."
   127   | string_for_failure OutOfResources = "The prover ran out of resources."
   127   | string_of_failure OutOfResources = "The prover ran out of resources."
   128   | string_for_failure OldSPASS =
   128   | string_of_failure OldSPASS =
   129     "The version of SPASS you are using is obsolete. Please upgrade to \
   129     "The version of SPASS you are using is obsolete. Please upgrade to \
   130     \SPASS 3.8ds. To install it, download and extract the package \
   130     \SPASS 3.8ds. To install it, download and extract the package \
   131     \\"http://www21.in.tum.de/~blanchet/spass-3.8ds.tar.gz\" and add the \
   131     \\"http://www21.in.tum.de/~blanchet/spass-3.8ds.tar.gz\" and add the \
   132     \\"spass-3.8ds\" directory's absolute path to " ^
   132     \\"spass-3.8ds\" directory's absolute path to " ^
   133     quote (Path.implode (Path.expand (Path.appends
   133     quote (Path.implode (Path.expand (Path.appends
   134                (Path.variable "ISABELLE_HOME_USER" ::
   134                (Path.variable "ISABELLE_HOME_USER" ::
   135                 map Path.basic ["etc", "components"])))) ^
   135                 map Path.basic ["etc", "components"])))) ^
   136     " on a line of its own."
   136     " on a line of its own."
   137   | string_for_failure NoPerl = "Perl" ^ missing_message_tail
   137   | string_of_failure NoPerl = "Perl" ^ missing_message_tail
   138   | string_for_failure NoLibwwwPerl =
   138   | string_of_failure NoLibwwwPerl =
   139     "The Perl module \"libwww-perl\"" ^ missing_message_tail
   139     "The Perl module \"libwww-perl\"" ^ missing_message_tail
   140   | string_for_failure MalformedInput =
   140   | string_of_failure MalformedInput =
   141     "The generated problem is malformed. Please report this to the Isabelle \
   141     "The generated problem is malformed. Please report this to the Isabelle \
   142     \developers."
   142     \developers."
   143   | string_for_failure MalformedOutput = "The prover output is malformed."
   143   | string_of_failure MalformedOutput = "The prover output is malformed."
   144   | string_for_failure Interrupted = "The prover was interrupted."
   144   | string_of_failure Interrupted = "The prover was interrupted."
   145   | string_for_failure Crashed = "The prover crashed."
   145   | string_of_failure Crashed = "The prover crashed."
   146   | string_for_failure InternalError = "An internal prover error occurred."
   146   | string_of_failure InternalError = "An internal prover error occurred."
   147   | string_for_failure (UnknownError string) =
   147   | string_of_failure (UnknownError s) =
   148     "A prover error occurred" ^
   148     "A prover error occurred" ^
   149     (if string = "" then ". (Pass the \"verbose\" option for details.)"
   149     (if s = "" then ". (Pass the \"verbose\" option for details.)"
   150      else ":\n" ^ string)
   150      else ":\n" ^ s)
   151 
   151 
   152 fun extract_delimited (begin_delim, end_delim) output =
   152 fun extract_delimited (begin_delim, end_delim) output =
   153   output |> first_field begin_delim |> the |> snd
   153   output |> first_field begin_delim |> the |> snd
   154          |> first_field end_delim |> the |> fst
   154          |> first_field end_delim |> the |> fst
   155          |> perhaps (try (first_field "\n" #> the #> snd))
   155          |> perhaps (try (first_field "\n" #> the #> snd))