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