src/HOL/Tools/ATP/atp_proof.ML
author blanchet
Tue May 15 13:06:15 2012 +0200 (2012-05-15)
changeset 47926 c6d5418ee770
parent 47921 fc26d5538868
child 47927 c35238d19bb9
permissions -rw-r--r--
fixed Waldmeister commutativity hack
blanchet@39452
     1
(*  Title:      HOL/Tools/ATP/atp_proof.ML
blanchet@39452
     2
    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
blanchet@39452
     3
    Author:     Claire Quigley, Cambridge University Computer Laboratory
blanchet@39452
     4
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@39452
     5
blanchet@42876
     6
Abstract representation of ATP proofs and TSTP/SPASS syntax.
blanchet@39452
     7
*)
blanchet@39452
     8
blanchet@39452
     9
signature ATP_PROOF =
blanchet@39452
    10
sig
nik@43678
    11
  type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
blanchet@42531
    12
  type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
blanchet@42943
    13
  type 'a problem = 'a ATP_Problem.problem
blanchet@39452
    14
blanchet@42965
    15
  exception UNRECOGNIZED_ATP_PROOF of unit
blanchet@42965
    16
blanchet@39491
    17
  datatype failure =
blanchet@42587
    18
    Unprovable |
blanchet@43050
    19
    GaveUp |
blanchet@42587
    20
    ProofMissing |
blanchet@42882
    21
    ProofIncomplete |
blanchet@44915
    22
    UnsoundProof of bool * string list |
blanchet@42587
    23
    CantConnect |
blanchet@42587
    24
    TimedOut |
blanchet@42953
    25
    Inappropriate |
blanchet@42587
    26
    OutOfResources |
blanchet@42587
    27
    NoPerl |
blanchet@42587
    28
    NoLibwwwPerl |
blanchet@42587
    29
    MalformedInput |
blanchet@42587
    30
    MalformedOutput |
blanchet@42587
    31
    Interrupted |
blanchet@42587
    32
    Crashed |
blanchet@42587
    33
    InternalError |
blanchet@42587
    34
    UnknownError of string
blanchet@39491
    35
blanchet@45551
    36
  type step_name = string * string list
blanchet@39452
    37
blanchet@39453
    38
  datatype 'a step =
blanchet@47774
    39
    Definition_Step of step_name * 'a * 'a |
blanchet@47774
    40
    Inference_Step of step_name * 'a * string * step_name list
blanchet@39452
    41
nik@43678
    42
  type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list
blanchet@39452
    43
blanchet@41259
    44
  val short_output : bool -> string -> string
blanchet@41744
    45
  val string_for_failure : failure -> string
blanchet@39491
    46
  val extract_important_message : string -> string
blanchet@39491
    47
  val extract_known_failure :
blanchet@39491
    48
    (failure * string) list -> string -> failure option
blanchet@39491
    49
  val extract_tstplike_proof_and_outcome :
blanchet@43473
    50
    bool -> bool -> (string * string) list -> (failure * string) list -> string
blanchet@43473
    51
    -> string * failure option
blanchet@42968
    52
  val is_same_atp_step : step_name -> step_name -> bool
blanchet@42961
    53
  val scan_general_id : string list -> string * string list
blanchet@42961
    54
  val parse_formula :
nik@43678
    55
    string list -> (string, 'a, (string, 'a) ho_term) formula * string list
blanchet@43481
    56
  val atp_proof_from_tstplike_proof :
blanchet@43481
    57
    string problem -> string -> string -> string proof
blanchet@42968
    58
  val clean_up_atp_proof_dependencies : string proof -> string proof
blanchet@39454
    59
  val map_term_names_in_atp_proof :
blanchet@39454
    60
    (string -> string) -> string proof -> string proof
blanchet@39454
    61
  val nasty_atp_proof : string Symtab.table -> string proof -> string proof
blanchet@39452
    62
end;
blanchet@39452
    63
blanchet@39452
    64
structure ATP_Proof : ATP_PROOF =
blanchet@39452
    65
struct
blanchet@39452
    66
blanchet@43085
    67
open ATP_Util
blanchet@39491
    68
open ATP_Problem
blanchet@39491
    69
blanchet@42965
    70
exception UNRECOGNIZED_ATP_PROOF of unit
blanchet@42965
    71
blanchet@39491
    72
datatype failure =
blanchet@42587
    73
  Unprovable |
blanchet@43050
    74
  GaveUp |
blanchet@42587
    75
  ProofMissing |
blanchet@42882
    76
  ProofIncomplete |
blanchet@44915
    77
  UnsoundProof of bool * string list |
blanchet@42587
    78
  CantConnect |
blanchet@42587
    79
  TimedOut |
blanchet@42953
    80
  Inappropriate |
blanchet@42587
    81
  OutOfResources |
blanchet@42587
    82
  NoPerl |
blanchet@42587
    83
  NoLibwwwPerl |
blanchet@42587
    84
  MalformedInput |
blanchet@42587
    85
  MalformedOutput |
blanchet@42587
    86
  Interrupted |
blanchet@42587
    87
  Crashed |
blanchet@42587
    88
  InternalError |
blanchet@42587
    89
  UnknownError of string
blanchet@39491
    90
blanchet@41259
    91
fun elide_string threshold s =
blanchet@41259
    92
  if size s > threshold then
blanchet@41259
    93
    String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^
blanchet@41259
    94
    String.extract (s, size s - (threshold + 1) div 2 + 6, NONE)
blanchet@41259
    95
  else
blanchet@41259
    96
    s
blanchet@41259
    97
fun short_output verbose output =
blanchet@42060
    98
  if verbose then
blanchet@42060
    99
    if output = "" then "No details available" else elide_string 1000 output
blanchet@42060
   100
  else
blanchet@42060
   101
    ""
blanchet@41259
   102
blanchet@41744
   103
val missing_message_tail =
blanchet@41744
   104
  " appears to be missing. You will need to install it if you want to invoke \
blanchet@41744
   105
  \remote provers."
blanchet@39491
   106
blanchet@42876
   107
fun involving [] = ""
blanchet@43005
   108
  | involving ss =
blanchet@43029
   109
    "involving " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) ^
blanchet@43029
   110
    " "
blanchet@42876
   111
blanchet@47506
   112
fun string_for_failure Unprovable = "The generated problem is unprovable."
blanchet@43050
   113
  | string_for_failure GaveUp = "The prover gave up."
blanchet@41744
   114
  | string_for_failure ProofMissing =
blanchet@41744
   115
    "The prover claims the conjecture is a theorem but did not provide a proof."
blanchet@42882
   116
  | string_for_failure ProofIncomplete =
blanchet@42882
   117
    "The prover claims the conjecture is a theorem but provided an incomplete \
blanchet@46427
   118
    \(or unparsable) proof."
blanchet@44915
   119
  | string_for_failure (UnsoundProof (false, ss)) =
blanchet@43823
   120
    "The prover found a type-unsound proof " ^ involving ss ^
blanchet@43823
   121
    "(or, less likely, your axioms are inconsistent). Specify a sound type \
blanchet@43823
   122
    \encoding or omit the \"type_enc\" option."
blanchet@44915
   123
  | string_for_failure (UnsoundProof (true, ss)) =
blanchet@42876
   124
    "The prover found a type-unsound proof " ^ involving ss ^
blanchet@42876
   125
    "even though a supposedly type-sound encoding was used (or, less likely, \
blanchet@43465
   126
    \your axioms are inconsistent). Please report this to the Isabelle \
blanchet@43465
   127
    \developers."
blanchet@41744
   128
  | string_for_failure CantConnect = "Cannot connect to remote server."
blanchet@41744
   129
  | string_for_failure TimedOut = "Timed out."
blanchet@42953
   130
  | string_for_failure Inappropriate =
blanchet@47506
   131
    "The generated problem lies outside the prover's scope."
blanchet@41744
   132
  | string_for_failure OutOfResources = "The prover ran out of resources."
blanchet@41744
   133
  | string_for_failure NoPerl = "Perl" ^ missing_message_tail
blanchet@41744
   134
  | string_for_failure NoLibwwwPerl =
blanchet@41744
   135
    "The Perl module \"libwww-perl\"" ^ missing_message_tail
blanchet@41744
   136
  | string_for_failure MalformedInput =
blanchet@41744
   137
    "The generated problem is malformed. Please report this to the Isabelle \
blanchet@41744
   138
    \developers."
blanchet@41744
   139
  | string_for_failure MalformedOutput = "The prover output is malformed."
blanchet@43085
   140
  | string_for_failure Interrupted = "The prover was interrupted."
blanchet@41744
   141
  | string_for_failure Crashed = "The prover crashed."
blanchet@41744
   142
  | string_for_failure InternalError = "An internal prover error occurred."
blanchet@41744
   143
  | string_for_failure (UnknownError string) =
blanchet@41744
   144
    "A prover error occurred" ^
blanchet@41334
   145
    (if string = "" then ". (Pass the \"verbose\" option for details.)"
blanchet@41334
   146
     else ":\n" ^ string)
blanchet@39491
   147
blanchet@39491
   148
fun extract_delimited (begin_delim, end_delim) output =
blanchet@39491
   149
  output |> first_field begin_delim |> the |> snd
blanchet@39491
   150
         |> first_field end_delim |> the |> fst
blanchet@39491
   151
         |> first_field "\n" |> the |> snd
blanchet@39491
   152
  handle Option.Option => ""
blanchet@39491
   153
blanchet@39491
   154
val tstp_important_message_delims =
blanchet@39491
   155
  ("% SZS start RequiredInformation", "% SZS end RequiredInformation")
blanchet@39491
   156
blanchet@39491
   157
fun extract_important_message output =
blanchet@39491
   158
  case extract_delimited tstp_important_message_delims output of
blanchet@39491
   159
    "" => ""
blanchet@39491
   160
  | s => s |> space_explode "\n" |> filter_out (curry (op =) "")
blanchet@39491
   161
           |> map (perhaps (try (unprefix "%")))
blanchet@39491
   162
           |> map (perhaps (try (unprefix " ")))
blanchet@39491
   163
           |> space_implode "\n " |> quote
blanchet@39491
   164
blanchet@39491
   165
(* Splits by the first possible of a list of delimiters. *)
blanchet@39491
   166
fun extract_tstplike_proof delims output =
blanchet@39491
   167
  case pairself (find_first (fn s => String.isSubstring s output))
blanchet@39491
   168
                (ListPair.unzip delims) of
blanchet@39491
   169
    (SOME begin_delim, SOME end_delim) =>
blanchet@39491
   170
    extract_delimited (begin_delim, end_delim) output
blanchet@39491
   171
  | _ => ""
blanchet@39491
   172
blanchet@39491
   173
fun extract_known_failure known_failures output =
blanchet@39491
   174
  known_failures
blanchet@39491
   175
  |> find_first (fn (_, pattern) => String.isSubstring pattern output)
blanchet@39491
   176
  |> Option.map fst
blanchet@39491
   177
blanchet@43473
   178
fun extract_tstplike_proof_and_outcome verbose complete proof_delims
blanchet@42848
   179
                                       known_failures output =
blanchet@42882
   180
  case (extract_tstplike_proof proof_delims output,
blanchet@42882
   181
        extract_known_failure known_failures output) of
blanchet@42882
   182
    (_, SOME ProofIncomplete) => ("", SOME ProofIncomplete)
blanchet@43246
   183
  | ("", SOME ProofMissing) => ("", NONE)
blanchet@42882
   184
  | ("", SOME failure) =>
blanchet@43050
   185
    ("", SOME (if failure = GaveUp andalso complete then Unprovable
blanchet@42882
   186
               else failure))
blanchet@43246
   187
  | ("", NONE) => ("", SOME (UnknownError (short_output verbose output)))
blanchet@42882
   188
  | (tstplike_proof, _) => (tstplike_proof, NONE)
blanchet@39452
   189
blanchet@45551
   190
type step_name = string * string list
blanchet@39452
   191
blanchet@42968
   192
fun is_same_atp_step (s1, _) (s2, _) = s1 = s2
blanchet@42968
   193
blanchet@42968
   194
val vampire_fact_prefix = "f"
blanchet@39452
   195
blanchet@39452
   196
fun step_name_ord p =
blanchet@39455
   197
  let val q = pairself fst p in
blanchet@39452
   198
    (* The "unprefix" part is to cope with remote Vampire's output. The proper
blanchet@39452
   199
       solution would be to perform a topological sort, e.g. using the nice
blanchet@39452
   200
       "Graph" functor. *)
blanchet@42968
   201
    case pairself (Int.fromString
blanchet@42968
   202
                   o perhaps (try (unprefix vampire_fact_prefix))) q of
blanchet@39452
   203
      (NONE, NONE) => string_ord q
blanchet@39452
   204
    | (NONE, SOME _) => LESS
blanchet@39452
   205
    | (SOME _, NONE) => GREATER
blanchet@39452
   206
    | (SOME i, SOME j) => int_ord (i, j)
blanchet@39452
   207
  end
blanchet@39452
   208
blanchet@39453
   209
datatype 'a step =
blanchet@47774
   210
  Definition_Step of step_name * 'a * 'a |
blanchet@47774
   211
  Inference_Step of step_name * 'a * string * step_name list
blanchet@39452
   212
nik@43678
   213
type 'a proof = ('a, 'a, ('a, 'a) ho_term) formula step list
blanchet@39452
   214
blanchet@47774
   215
fun step_name (Definition_Step (name, _, _)) = name
blanchet@47774
   216
  | step_name (Inference_Step (name, _, _, _)) = name
blanchet@39452
   217
blanchet@39452
   218
(**** PARSING OF TSTP FORMAT ****)
blanchet@39452
   219
blanchet@42536
   220
(* Strings enclosed in single quotes (e.g., file names) *)
blanchet@39452
   221
val scan_general_id =
blanchet@47917
   222
  $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode
blanchet@39452
   223
  || Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig
blanchet@39452
   224
     >> (fn (ss1, ss2) => implode ss1 ^ implode ss2)
blanchet@39452
   225
blanchet@45235
   226
val skip_term =
blanchet@45208
   227
  let
blanchet@45235
   228
    fun skip _ accum [] = (accum, [])
blanchet@45235
   229
      | skip 0 accum (ss as "," :: _) = (accum, ss)
blanchet@45235
   230
      | skip 0 accum (ss as ")" :: _) = (accum, ss)
blanchet@45235
   231
      | skip 0 accum (ss as "]" :: _) = (accum, ss)
blanchet@45235
   232
      | skip n accum ((s as "(") :: ss) = skip (n + 1) (s :: accum) ss
blanchet@45235
   233
      | skip n accum ((s as "[") :: ss) = skip (n + 1) (s :: accum) ss
blanchet@45235
   234
      | skip n accum ((s as "]") :: ss) = skip (n - 1) (s :: accum) ss
blanchet@45235
   235
      | skip n accum ((s as ")") :: ss) = skip (n - 1) (s :: accum) ss
blanchet@45235
   236
      | skip n accum (s :: ss) = skip n (s :: accum) ss
blanchet@45235
   237
  in skip 0 [] #>> (rev #> implode) end
blanchet@45208
   238
blanchet@45208
   239
datatype source =
blanchet@45208
   240
  File_Source of string * string option |
blanchet@45209
   241
  Inference_Source of string * string list
blanchet@45208
   242
blanchet@45235
   243
val dummy_phi = AAtom (ATerm ("", []))
blanchet@45235
   244
val dummy_inference = Inference_Source ("", [])
blanchet@45235
   245
blanchet@47917
   246
(* "skip_term" is there to cope with Waldmeister nonsense such as
blanchet@47917
   247
   "theory(equality)". *)
blanchet@47917
   248
val parse_dependency = scan_general_id --| skip_term
blanchet@47917
   249
val parse_dependencies =
blanchet@47917
   250
  parse_dependency ::: Scan.repeat ($$ "," |-- parse_dependency)
blanchet@45208
   251
blanchet@45208
   252
fun parse_source x =
blanchet@45208
   253
  (Scan.this_string "file" |-- $$ "(" |-- scan_general_id --
blanchet@45208
   254
     Scan.option ($$ "," |-- scan_general_id) --| $$ ")"
blanchet@45208
   255
     >> File_Source
blanchet@45209
   256
   || Scan.this_string "inference" |-- $$ "(" |-- scan_general_id
blanchet@45235
   257
        --| skip_term --| $$ "," --| skip_term --| $$ "," --| $$ "["
blanchet@45209
   258
        -- parse_dependencies --| $$ "]" --| $$ ")"
blanchet@45235
   259
       >> Inference_Source
blanchet@45235
   260
   || skip_term >> K dummy_inference) x
blanchet@39452
   261
blanchet@42966
   262
fun list_app (f, args) =
blanchet@42968
   263
  fold (fn arg => fn f => ATerm (tptp_app, [f, arg])) args f
blanchet@42966
   264
blanchet@45881
   265
(* We currently ignore TFF and THF types. *)
blanchet@42968
   266
fun parse_type_stuff x =
blanchet@42968
   267
  Scan.repeat (($$ tptp_has_type || $$ tptp_fun_type) |-- parse_arg) x
blanchet@42968
   268
and parse_arg x =
blanchet@42968
   269
  ($$ "(" |-- parse_term --| $$ ")" --| parse_type_stuff
blanchet@42968
   270
   || scan_general_id --| parse_type_stuff
blanchet@42968
   271
        -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") []
blanchet@42968
   272
      >> ATerm) x
blanchet@45881
   273
and parse_term x =
blanchet@42968
   274
  (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) >> list_app) x
blanchet@42966
   275
and parse_terms x =
blanchet@42966
   276
  (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
blanchet@39452
   277
blanchet@39598
   278
fun parse_atom x =
blanchet@42968
   279
  (parse_term -- Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal
blanchet@42968
   280
                              -- parse_term)
blanchet@39598
   281
   >> (fn (u1, NONE) => AAtom u1
blanchet@45881
   282
        | (u1, SOME (neg, u2)) =>
blanchet@45881
   283
          AAtom (ATerm ("equal", [u1, u2])) |> is_some neg ? mk_anot)) x
blanchet@39452
   284
blanchet@39452
   285
(* TPTP formulas are fully parenthesized, so we don't need to worry about
blanchet@39452
   286
   operator precedence. *)
blanchet@42605
   287
fun parse_literal x =
blanchet@42968
   288
  ((Scan.repeat ($$ tptp_not) >> length)
blanchet@42605
   289
      -- ($$ "(" |-- parse_formula --| $$ ")"
blanchet@42605
   290
          || parse_quantified_formula
blanchet@42605
   291
          || parse_atom)
blanchet@42605
   292
      >> (fn (n, phi) => phi |> n mod 2 = 1 ? mk_anot)) x
blanchet@42605
   293
and parse_formula x =
blanchet@42605
   294
  (parse_literal
blanchet@43163
   295
   -- Scan.option ((Scan.this_string tptp_implies
blanchet@43163
   296
                    || Scan.this_string tptp_iff
blanchet@43163
   297
                    || Scan.this_string tptp_not_iff
blanchet@43163
   298
                    || Scan.this_string tptp_if
blanchet@43163
   299
                    || $$ tptp_or
blanchet@43163
   300
                    || $$ tptp_and) -- parse_formula)
blanchet@39452
   301
   >> (fn (phi1, NONE) => phi1
blanchet@43163
   302
        | (phi1, SOME (c, phi2)) =>
blanchet@43163
   303
          if c = tptp_implies then mk_aconn AImplies phi1 phi2
blanchet@43163
   304
          else if c = tptp_iff then mk_aconn AIff phi1 phi2
blanchet@43163
   305
          else if c = tptp_not_iff then mk_anot (mk_aconn AIff phi1 phi2)
blanchet@43163
   306
          else if c = tptp_if then mk_aconn AImplies phi2 phi1
blanchet@43163
   307
          else if c = tptp_or then mk_aconn AOr phi1 phi2
blanchet@43163
   308
          else if c = tptp_and then mk_aconn AAnd phi1 phi2
blanchet@43163
   309
          else raise Fail ("impossible connective " ^ quote c))) x
blanchet@42605
   310
and parse_quantified_formula x =
blanchet@42968
   311
  (($$ tptp_forall >> K AForall || $$ tptp_exists >> K AExists)
blanchet@42605
   312
   --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal
blanchet@42605
   313
   >> (fn ((q, ts), phi) =>
blanchet@42966
   314
          (* We ignore TFF and THF types for now. *)
blanchet@45881
   315
          AQuant (q, map (fn ATerm (s, _) => (s, NONE)) ts, phi))) x
blanchet@39452
   316
blanchet@39452
   317
val parse_tstp_extra_arguments =
blanchet@45235
   318
  Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term))
blanchet@45235
   319
                dummy_inference
blanchet@39452
   320
blanchet@42943
   321
val waldmeister_conjecture = "conjecture_1"
blanchet@42943
   322
blanchet@42536
   323
val tofof_fact_prefix = "fof_"
blanchet@41203
   324
blanchet@42943
   325
fun is_same_term subst tm1 tm2 =
blanchet@42943
   326
  let
blanchet@42943
   327
    fun do_term_pair _ NONE = NONE
blanchet@42943
   328
      | do_term_pair (ATerm (s1, tm1), ATerm (s2, tm2)) (SOME subst) =
blanchet@42998
   329
        case pairself is_tptp_variable (s1, s2) of
blanchet@42943
   330
          (true, true) =>
blanchet@42943
   331
          (case AList.lookup (op =) subst s1 of
blanchet@42943
   332
             SOME s2' => if s2' = s2 then SOME subst else NONE
blanchet@42943
   333
           | NONE =>
blanchet@42943
   334
             if null (AList.find (op =) subst s2) then SOME ((s1, s2) :: subst)
blanchet@42943
   335
             else NONE)
blanchet@42943
   336
        | (false, false) =>
blanchet@42943
   337
          if s1 = s2 andalso length tm1 = length tm2 then
blanchet@42943
   338
            SOME subst |> fold do_term_pair (tm1 ~~ tm2)
blanchet@42943
   339
          else
blanchet@42943
   340
            NONE
blanchet@42943
   341
        | _ => NONE
blanchet@42943
   342
  in SOME subst |> do_term_pair (tm1, tm2) |> is_some end
blanchet@42943
   343
blanchet@47921
   344
fun is_same_formula comm subst (AQuant (q1, xs1, phi1)) (AQuant (q2, xs2, phi2)) =
blanchet@42943
   345
    q1 = q2 andalso length xs1 = length xs2 andalso
blanchet@47921
   346
    is_same_formula comm ((map fst xs1 ~~ map fst xs2) @ subst) phi1 phi2
blanchet@47921
   347
  | is_same_formula comm subst (AConn (c1, phis1)) (AConn (c2, phis2)) =
blanchet@42943
   348
    c1 = c2 andalso length phis1 = length phis2 andalso
blanchet@47921
   349
    forall (uncurry (is_same_formula comm subst)) (phis1 ~~ phis2)
blanchet@47926
   350
  | is_same_formula comm subst (AAtom (tm1 as ATerm ("equal", [tm11, tm12])))
blanchet@47926
   351
                    (AAtom tm2) =
blanchet@47926
   352
    is_same_term subst tm1 tm2 orelse
blanchet@47921
   353
    (comm andalso is_same_term subst (ATerm ("equal", [tm12, tm11])) tm2)
blanchet@47921
   354
  | is_same_formula _ subst (AAtom tm1) (AAtom tm2) = is_same_term subst tm1 tm2
blanchet@47921
   355
  | is_same_formula _ _ _ _ = false
blanchet@42943
   356
blanchet@42943
   357
fun matching_formula_line_identifier phi (Formula (ident, _, phi', _, _)) =
blanchet@47921
   358
    if is_same_formula true [] phi phi' then SOME (ident, phi') else NONE
blanchet@42943
   359
  | matching_formula_line_identifier _ _ = NONE
blanchet@42943
   360
blanchet@42943
   361
fun find_formula_in_problem problem phi =
blanchet@42943
   362
  problem |> maps snd |> map_filter (matching_formula_line_identifier phi)
blanchet@45551
   363
          |> try (single o hd) |> the_default []
blanchet@42943
   364
blanchet@47921
   365
fun commute_eq (AAtom (ATerm (s, tms))) = AAtom (ATerm (s, rev tms))
blanchet@47921
   366
  | commute_eq t = raise Fail "expected equation"
blanchet@47921
   367
blanchet@42962
   368
(* Syntax: (cnf|fof|tff|thf)\(<num>, <formula_role>,
blanchet@42962
   369
            <formula> <extra_arguments>\).
blanchet@39452
   370
   The <num> could be an identifier, but we assume integers. *)
blanchet@42943
   371
fun parse_tstp_line problem =
blanchet@42968
   372
  ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof
blanchet@42968
   373
    || Scan.this_string tptp_tff || Scan.this_string tptp_thf) -- $$ "(")
blanchet@42943
   374
    |-- scan_general_id --| $$ "," -- Symbol.scan_id --| $$ ","
blanchet@45235
   375
    -- (parse_formula || skip_term >> K dummy_phi) -- parse_tstp_extra_arguments
blanchet@45235
   376
    --| $$ ")" --| $$ "."
blanchet@42943
   377
   >> (fn (((num, role), phi), deps) =>
blanchet@42943
   378
          let
blanchet@47921
   379
            val ((name, phi), rule, deps) =
blanchet@42943
   380
              (* Waldmeister isn't exactly helping. *)
blanchet@42943
   381
              case deps of
blanchet@45208
   382
                File_Source (_, SOME s) =>
blanchet@47921
   383
                (if s = waldmeister_conjecture then
blanchet@47921
   384
                   case find_formula_in_problem problem (mk_anot phi) of
blanchet@47921
   385
                     (* Waldmeister hack: Get the original orientation of the
blanchet@47921
   386
                        equation to avoid confusing Isar. *)
blanchet@47921
   387
                     [(s, phi')] =>
blanchet@47921
   388
                     ((num, [s]),
blanchet@47926
   389
                      phi |> not (is_same_formula false [] (mk_anot phi) phi')
blanchet@47921
   390
                             ? commute_eq)
blanchet@47921
   391
                   | _ => ((num, []), phi)
blanchet@47921
   392
                 else
blanchet@47921
   393
                   ((num, [s |> perhaps (try (unprefix tofof_fact_prefix))]),
blanchet@47921
   394
                    phi),
blanchet@47921
   395
                 "", [])
blanchet@45208
   396
              | File_Source _ =>
blanchet@47921
   397
                (((num, phi |> find_formula_in_problem problem |> map fst),
blanchet@47921
   398
                  phi), "", [])
blanchet@47921
   399
              | Inference_Source (rule, deps) => (((num, []), phi), rule, deps)
blanchet@47787
   400
            fun mk_step () =
blanchet@47787
   401
              Inference_Step (name, phi, rule, map (rpair []) deps)
blanchet@42943
   402
          in
blanchet@42943
   403
            case role of
blanchet@42943
   404
              "definition" =>
blanchet@42943
   405
              (case phi of
blanchet@42943
   406
                 AConn (AIff, [phi1 as AAtom _, phi2]) =>
blanchet@47774
   407
                 Definition_Step (name, phi1, phi2)
blanchet@42943
   408
               | AAtom (ATerm ("equal", _)) =>
blanchet@42943
   409
                 (* Vampire's equality proxy axiom *)
blanchet@47774
   410
                 Inference_Step (name, phi, rule, map (rpair []) deps)
blanchet@47787
   411
               | _ => mk_step ())
blanchet@47787
   412
            | _ => mk_step ()
blanchet@42943
   413
          end)
blanchet@39452
   414
blanchet@39452
   415
(**** PARSING OF SPASS OUTPUT ****)
blanchet@39452
   416
blanchet@39452
   417
(* SPASS returns clause references of the form "x.y". We ignore "y", whose role
blanchet@39452
   418
   is not clear anyway. *)
blanchet@39452
   419
val parse_dot_name = scan_general_id --| $$ "." --| scan_general_id
blanchet@39452
   420
blanchet@39452
   421
val parse_spass_annotations =
blanchet@39452
   422
  Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name
blanchet@39452
   423
                                         --| Scan.option ($$ ","))) []
blanchet@39452
   424
blanchet@39452
   425
(* It is not clear why some literals are followed by sequences of stars and/or
blanchet@39452
   426
   pluses. We ignore them. *)
blanchet@39602
   427
fun parse_decorated_atom x =
blanchet@39602
   428
  (parse_atom --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")) x
blanchet@39452
   429
blanchet@39452
   430
fun mk_horn ([], []) = AAtom (ATerm ("c_False", []))
blanchet@42943
   431
  | mk_horn ([], pos_lits) = foldr1 (uncurry (mk_aconn AOr)) pos_lits
blanchet@42943
   432
  | mk_horn (neg_lits, []) = mk_anot (foldr1 (uncurry (mk_aconn AAnd)) neg_lits)
blanchet@39452
   433
  | mk_horn (neg_lits, pos_lits) =
blanchet@42943
   434
    mk_aconn AImplies (foldr1 (uncurry (mk_aconn AAnd)) neg_lits)
blanchet@42943
   435
                      (foldr1 (uncurry (mk_aconn AOr)) pos_lits)
blanchet@39452
   436
blanchet@39645
   437
fun parse_horn_clause x =
blanchet@39645
   438
  (Scan.repeat parse_decorated_atom --| $$ "|" --| $$ "|"
blanchet@39645
   439
     -- Scan.repeat parse_decorated_atom --| $$ "-" --| $$ ">"
blanchet@39645
   440
     -- Scan.repeat parse_decorated_atom
blanchet@39645
   441
   >> (mk_horn o apfst (op @))) x
blanchet@39452
   442
blanchet@46427
   443
fun resolve_spass_num (SOME names) _ _ = names
blanchet@46427
   444
  | resolve_spass_num NONE spass_names num =
blanchet@46427
   445
    case Int.fromString num of
blanchet@46427
   446
      SOME j => if j > 0 andalso j <= Vector.length spass_names then
blanchet@46427
   447
                  Vector.sub (spass_names, j - 1)
blanchet@46427
   448
                else
blanchet@46427
   449
                  []
blanchet@46427
   450
    | NONE => []
blanchet@43481
   451
blanchet@46390
   452
val parse_spass_debug =
blanchet@46390
   453
  Scan.option ($$ "(" |-- Scan.repeat (scan_general_id --| Scan.option ($$ ","))
blanchet@46390
   454
               --| $$ ")")
blanchet@46390
   455
blanchet@46427
   456
(* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms>.
blanchet@46427
   457
           derived from formulae <ident>* *)
blanchet@45162
   458
fun parse_spass_line spass_names =
blanchet@46390
   459
  parse_spass_debug |-- scan_general_id --| $$ "[" --| $$ "0" --| $$ ":"
blanchet@46390
   460
    -- Symbol.scan_id -- parse_spass_annotations --| $$ "]"
blanchet@46390
   461
    -- parse_horn_clause --| $$ "."
blanchet@46427
   462
    -- Scan.option (Scan.this_string "derived from formulae "
blanchet@46451
   463
                    |-- Scan.repeat (scan_general_id --| Scan.option ($$ " ")))
blanchet@46427
   464
  >> (fn ((((num, rule), deps), u), names) =>
blanchet@47774
   465
         Inference_Step ((num, resolve_spass_num names spass_names num), u,
blanchet@47774
   466
             rule, map (swap o `(resolve_spass_num NONE spass_names)) deps))
blanchet@45162
   467
blanchet@45162
   468
(* Syntax: <name> *)
blanchet@45203
   469
fun parse_satallax_line x =
blanchet@45203
   470
  (scan_general_id --| Scan.option ($$ " ")
blanchet@47774
   471
   >> (fn s => Inference_Step ((s, [s]), dummy_phi, "", []))) x
blanchet@43481
   472
blanchet@43481
   473
fun parse_line problem spass_names =
blanchet@45203
   474
  parse_tstp_line problem || parse_spass_line spass_names || parse_satallax_line
blanchet@43481
   475
fun parse_proof problem spass_names tstp =
blanchet@44784
   476
  tstp |> strip_spaces_except_between_idents
blanchet@43481
   477
       |> raw_explode
blanchet@43481
   478
       |> Scan.finite Symbol.stopper
blanchet@43481
   479
              (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
blanchet@43481
   480
                              (Scan.repeat1 (parse_line problem spass_names))))
blanchet@43481
   481
       |> fst
blanchet@43481
   482
blanchet@43481
   483
(** SPASS's FLOTTER hack **)
blanchet@43481
   484
blanchet@43481
   485
(* This is a hack required for keeping track of facts after they have been
blanchet@43481
   486
   clausified by SPASS's FLOTTER preprocessor. The "ATP/scripts/spass" script is
blanchet@43481
   487
   also part of this hack. *)
blanchet@43481
   488
blanchet@43481
   489
val set_ClauseFormulaRelationN = "set_ClauseFormulaRelation"
blanchet@43481
   490
blanchet@43481
   491
fun extract_clause_sequence output =
blanchet@43481
   492
  let
blanchet@43481
   493
    val tokens_of = String.tokens (not o Char.isAlphaNum)
blanchet@43481
   494
    fun extract_num ("clause" :: (ss as _ :: _)) = Int.fromString (List.last ss)
blanchet@43481
   495
      | extract_num _ = NONE
blanchet@43481
   496
  in output |> split_lines |> map_filter (extract_num o tokens_of) end
blanchet@39452
   497
blanchet@43481
   498
fun is_head_digit s = Char.isDigit (String.sub (s, 0))
blanchet@43481
   499
val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
blanchet@43481
   500
blanchet@43481
   501
val parse_clause_formula_pair =
blanchet@43481
   502
  $$ "(" |-- scan_integer --| $$ ","
blanchet@43481
   503
  -- (Symbol.scan_id ::: Scan.repeat ($$ "," |-- Symbol.scan_id)) --| $$ ")"
blanchet@43481
   504
  --| Scan.option ($$ ",")
blanchet@43481
   505
val parse_clause_formula_relation =
blanchet@43481
   506
  Scan.this_string set_ClauseFormulaRelationN |-- $$ "("
blanchet@43481
   507
  |-- Scan.repeat parse_clause_formula_pair
blanchet@43481
   508
val extract_clause_formula_relation =
blanchet@43481
   509
  Substring.full #> Substring.position set_ClauseFormulaRelationN
blanchet@43481
   510
  #> snd #> Substring.position "." #> fst #> Substring.string
blanchet@43481
   511
  #> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
blanchet@43481
   512
  #> fst
blanchet@39452
   513
blanchet@43481
   514
fun extract_spass_name_vector output =
blanchet@43481
   515
  (if String.isSubstring set_ClauseFormulaRelationN output then
blanchet@43481
   516
     let
blanchet@43481
   517
       val num_seq = extract_clause_sequence output
blanchet@43481
   518
       val name_map = extract_clause_formula_relation output
blanchet@43481
   519
       val name_seq = num_seq |> map (these o AList.lookup (op =) name_map)
blanchet@43481
   520
     in name_seq end
blanchet@43481
   521
   else
blanchet@43481
   522
     [])
blanchet@43481
   523
  |> Vector.fromList
blanchet@43481
   524
blanchet@43481
   525
fun atp_proof_from_tstplike_proof _ _ "" = []
blanchet@43481
   526
  | atp_proof_from_tstplike_proof problem output tstp =
blanchet@43481
   527
    tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
blanchet@43481
   528
    |> parse_proof problem (extract_spass_name_vector output)
blanchet@42449
   529
    |> sort (step_name_ord o pairself step_name)
blanchet@42968
   530
blanchet@42968
   531
fun clean_up_dependencies _ [] = []
blanchet@47774
   532
  | clean_up_dependencies seen
blanchet@47774
   533
                          ((step as Definition_Step (name, _, _)) :: steps) =
blanchet@42968
   534
    step :: clean_up_dependencies (name :: seen) steps
blanchet@47774
   535
  | clean_up_dependencies seen (Inference_Step (name, u, rule, deps) :: steps) =
blanchet@47774
   536
    Inference_Step (name, u, rule,
blanchet@47774
   537
        map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) ::
blanchet@42968
   538
    clean_up_dependencies (name :: seen) steps
blanchet@42968
   539
blanchet@42975
   540
fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof
blanchet@39452
   541
blanchet@39454
   542
fun map_term_names_in_term f (ATerm (s, ts)) =
blanchet@39454
   543
  ATerm (f s, map (map_term_names_in_term f) ts)
blanchet@39454
   544
fun map_term_names_in_formula f (AQuant (q, xs, phi)) =
blanchet@39454
   545
    AQuant (q, xs, map_term_names_in_formula f phi)
blanchet@39454
   546
  | map_term_names_in_formula f (AConn (c, phis)) =
blanchet@39454
   547
    AConn (c, map (map_term_names_in_formula f) phis)
blanchet@39454
   548
  | map_term_names_in_formula f (AAtom t) = AAtom (map_term_names_in_term f t)
blanchet@47774
   549
fun map_term_names_in_step f (Definition_Step (name, phi1, phi2)) =
blanchet@47774
   550
    Definition_Step (name, map_term_names_in_formula f phi1,
blanchet@47774
   551
                     map_term_names_in_formula f phi2)
blanchet@47774
   552
  | map_term_names_in_step f (Inference_Step (name, phi, rule, deps)) =
blanchet@47774
   553
    Inference_Step (name, map_term_names_in_formula f phi, rule, deps)
blanchet@39454
   554
fun map_term_names_in_atp_proof f = map (map_term_names_in_step f)
blanchet@39454
   555
blanchet@39454
   556
fun nasty_name pool s = s |> Symtab.lookup pool |> the_default s
blanchet@39454
   557
fun nasty_atp_proof pool =
blanchet@39454
   558
  if Symtab.is_empty pool then I
blanchet@39454
   559
  else map_term_names_in_atp_proof (nasty_name pool)
blanchet@39454
   560
blanchet@39452
   561
end;