factored out TSTP/SPASS/Vampire proof parsing;
authorblanchet
Thu Sep 16 11:12:08 2010 +0200 (2010-09-16)
changeset 3945270a57e40f795
parent 39451 8893562a954b
child 39453 1740a2d6bef9
factored out TSTP/SPASS/Vampire proof parsing;
from "Sledgehammer_Reconstructo" to a new module "ATP_Proof"
src/HOL/IsaMakefile
src/HOL/Sledgehammer.thy
src/HOL/Tools/ATP/atp_problem.ML
src/HOL/Tools/ATP/atp_proof.ML
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
     1.1 --- a/src/HOL/IsaMakefile	Thu Sep 16 09:59:32 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Thu Sep 16 11:12:08 2010 +0200
     1.3 @@ -268,6 +268,7 @@
     1.4    $(SRC)/Tools/Metis/metis.ML \
     1.5    Tools/async_manager.ML \
     1.6    Tools/ATP/atp_problem.ML \
     1.7 +  Tools/ATP/atp_proof.ML \
     1.8    Tools/ATP/atp_systems.ML \
     1.9    Tools/choice_specification.ML \
    1.10    Tools/int_arith.ML \
     2.1 --- a/src/HOL/Sledgehammer.thy	Thu Sep 16 09:59:32 2010 +0200
     2.2 +++ b/src/HOL/Sledgehammer.thy	Thu Sep 16 11:12:08 2010 +0200
     2.3 @@ -11,6 +11,7 @@
     2.4  imports Plain Hilbert_Choice
     2.5  uses
     2.6    ("Tools/ATP/atp_problem.ML")
     2.7 +  ("Tools/ATP/atp_proof.ML")
     2.8    ("Tools/ATP/atp_systems.ML")
     2.9    ("~~/src/Tools/Metis/metis.ML")
    2.10    ("Tools/Sledgehammer/clausifier.ML")
    2.11 @@ -92,6 +93,7 @@
    2.12  done
    2.13  
    2.14  use "Tools/ATP/atp_problem.ML"
    2.15 +use "Tools/ATP/atp_proof.ML"
    2.16  use "Tools/ATP/atp_systems.ML"
    2.17  setup ATP_Systems.setup
    2.18  
     3.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Sep 16 09:59:32 2010 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Sep 16 11:12:08 2010 +0200
     3.3 @@ -2,7 +2,7 @@
     3.4      Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     3.5      Author:     Jasmin Blanchette, TU Muenchen
     3.6  
     3.7 -TPTP syntax.
     3.8 +Abstract representation of ATP problems and TPTP syntax.
     3.9  *)
    3.10  
    3.11  signature ATP_PROBLEM =
    3.12 @@ -20,10 +20,10 @@
    3.13    type 'a problem = (string * 'a problem_line list) list
    3.14  
    3.15    val timestamp : unit -> string
    3.16 -  val is_tptp_variable : string -> bool
    3.17 -  val strings_for_tptp_problem :
    3.18 +  val is_atp_variable : string -> bool
    3.19 +  val tptp_strings_for_atp_problem :
    3.20      bool -> (string * string problem_line list) list -> string list
    3.21 -  val nice_tptp_problem :
    3.22 +  val nice_atp_problem :
    3.23      bool -> ('a * (string * string) problem_line list) list
    3.24      -> ('a * string problem_line list) list
    3.25         * (string Symtab.table * string Symtab.table) option
    3.26 @@ -90,7 +90,7 @@
    3.27      "fof(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n    (" ^
    3.28      string_for_formula phi ^ ")).\n"
    3.29    end
    3.30 -fun strings_for_tptp_problem use_conjecture_for_hypotheses problem =
    3.31 +fun tptp_strings_for_atp_problem use_conjecture_for_hypotheses problem =
    3.32    "% This file was generated by Isabelle (most likely Sledgehammer)\n\
    3.33    \% " ^ timestamp () ^ "\n" ::
    3.34    maps (fn (_, []) => []
    3.35 @@ -99,7 +99,7 @@
    3.36             map (string_for_problem_line use_conjecture_for_hypotheses) lines)
    3.37         problem
    3.38  
    3.39 -fun is_tptp_variable s = Char.isUpper (String.sub (s, 0))
    3.40 +fun is_atp_variable s = Char.isUpper (String.sub (s, 0))
    3.41  
    3.42  
    3.43  (** Nice names **)
    3.44 @@ -163,7 +163,7 @@
    3.45  fun nice_problem problem =
    3.46    pool_map (fn (heading, lines) =>
    3.47                 pool_map nice_problem_line lines #>> pair heading) problem
    3.48 -fun nice_tptp_problem readable_names problem =
    3.49 +fun nice_atp_problem readable_names problem =
    3.50    nice_problem problem (empty_name_pool readable_names)
    3.51  
    3.52  end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Sep 16 11:12:08 2010 +0200
     4.3 @@ -0,0 +1,262 @@
     4.4 +(*  Title:      HOL/Tools/ATP/atp_proof.ML
     4.5 +    Author:     Lawrence C. Paulson, Cambridge University Computer Laboratory
     4.6 +    Author:     Claire Quigley, Cambridge University Computer Laboratory
     4.7 +    Author:     Jasmin Blanchette, TU Muenchen
     4.8 +
     4.9 +Abstract representation of ATP proofs and TSTP/SPASS/Vampire syntax.
    4.10 +*)
    4.11 +
    4.12 +signature ATP_PROOF =
    4.13 +sig
    4.14 +  type 'a fo_term = 'a ATP_Problem.fo_term
    4.15 +  type ('a, 'b) formula = ('a, 'b) ATP_Problem.formula
    4.16 +
    4.17 +  datatype step_name = Str of string * string | Num of string
    4.18 +
    4.19 +  datatype ('a, 'b, 'c) step =
    4.20 +    Definition of step_name * 'a * 'b |
    4.21 +    Inference of step_name * 'c * step_name list
    4.22 +
    4.23 +  type string_formula = (string, string fo_term) formula
    4.24 +  type string_step =
    4.25 +      (string_formula, string_formula, string_formula) step
    4.26 +
    4.27 +  val step_num : step_name -> string
    4.28 +  val is_same_step : step_name * step_name -> bool
    4.29 +  val atp_proof_from_tstplike_string :
    4.30 +    string Symtab.table -> string -> string_step list
    4.31 +end;
    4.32 +
    4.33 +structure ATP_Proof : ATP_PROOF =
    4.34 +struct
    4.35 +
    4.36 +(*### FIXME: DUPLICATED FROM SLEDGEHAMMER_UTIL *)
    4.37 +fun strip_spaces_in_list _ [] = []
    4.38 +  | strip_spaces_in_list _ [c1] = if Char.isSpace c1 then [] else [str c1]
    4.39 +  | strip_spaces_in_list is_evil [c1, c2] =
    4.40 +    strip_spaces_in_list is_evil [c1] @ strip_spaces_in_list is_evil [c2]
    4.41 +  | strip_spaces_in_list is_evil (c1 :: c2 :: c3 :: cs) =
    4.42 +    if Char.isSpace c1 then
    4.43 +      strip_spaces_in_list is_evil (c2 :: c3 :: cs)
    4.44 +    else if Char.isSpace c2 then
    4.45 +      if Char.isSpace c3 then
    4.46 +        strip_spaces_in_list is_evil (c1 :: c3 :: cs)
    4.47 +      else
    4.48 +        str c1 :: (if forall is_evil [c1, c3] then [" "] else []) @
    4.49 +        strip_spaces_in_list is_evil (c3 :: cs)
    4.50 +    else
    4.51 +      str c1 :: strip_spaces_in_list is_evil (c2 :: c3 :: cs)
    4.52 +fun strip_spaces is_evil =
    4.53 +  implode o strip_spaces_in_list is_evil o String.explode
    4.54 +
    4.55 +fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
    4.56 +val strip_spaces_except_between_ident_chars = strip_spaces is_ident_char
    4.57 +
    4.58 +open ATP_Problem
    4.59 +
    4.60 +fun mk_anot (AConn (ANot, [phi])) = phi
    4.61 +  | mk_anot phi = AConn (ANot, [phi])
    4.62 +fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
    4.63 +
    4.64 +datatype step_name = Str of string * string | Num of string
    4.65 +
    4.66 +fun step_num (Str (num, _)) = num
    4.67 +  | step_num (Num num) = num
    4.68 +
    4.69 +val is_same_step = op = o pairself step_num
    4.70 +
    4.71 +fun step_name_ord p =
    4.72 +  let val q = pairself step_num p in
    4.73 +    (* The "unprefix" part is to cope with remote Vampire's output. The proper
    4.74 +       solution would be to perform a topological sort, e.g. using the nice
    4.75 +       "Graph" functor. *)
    4.76 +    case pairself (Int.fromString o perhaps (try (unprefix "f"))) q of
    4.77 +      (NONE, NONE) => string_ord q
    4.78 +    | (NONE, SOME _) => LESS
    4.79 +    | (SOME _, NONE) => GREATER
    4.80 +    | (SOME i, SOME j) => int_ord (i, j)
    4.81 +  end
    4.82 +
    4.83 +datatype ('a, 'b, 'c) step =
    4.84 +  Definition of step_name * 'a * 'b |
    4.85 +  Inference of step_name * 'c * step_name list
    4.86 +
    4.87 +type string_formula = (string, string fo_term) formula
    4.88 +type string_step =
    4.89 +    (string_formula, string_formula, string_formula) step
    4.90 +
    4.91 +fun step_name (Definition (name, _, _)) = name
    4.92 +  | step_name (Inference (name, _, _)) = name
    4.93 +
    4.94 +(**** PARSING OF TSTP FORMAT ****)
    4.95 +
    4.96 +(*Strings enclosed in single quotes, e.g. filenames*)
    4.97 +val scan_general_id =
    4.98 +  $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode
    4.99 +  || Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig
   4.100 +     >> (fn (ss1, ss2) => implode ss1 ^ implode ss2)
   4.101 +
   4.102 +fun repair_name _ "$true" = "c_True"
   4.103 +  | repair_name _ "$false" = "c_False"
   4.104 +  | repair_name _ "$$e" = "c_equal" (* seen in Vampire proofs *)
   4.105 +  | repair_name _ "equal" = "c_equal" (* needed by SPASS? *)
   4.106 +  | repair_name pool s =
   4.107 +    case Symtab.lookup pool s of
   4.108 +      SOME s' => s'
   4.109 +    | NONE =>
   4.110 +      if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then
   4.111 +        "c_equal" (* seen in Vampire proofs *)
   4.112 +      else
   4.113 +        s
   4.114 +(* Generalized first-order terms, which include file names, numbers, etc. *)
   4.115 +fun parse_annotation strict x =
   4.116 +  ((scan_general_id ::: Scan.repeat ($$ " " |-- scan_general_id)
   4.117 +      >> (strict ? filter (is_some o Int.fromString)))
   4.118 +   -- Scan.optional (parse_annotation strict) [] >> op @
   4.119 +   || $$ "(" |-- parse_annotations strict --| $$ ")"
   4.120 +   || $$ "[" |-- parse_annotations strict --| $$ "]") x
   4.121 +and parse_annotations strict x =
   4.122 +  (Scan.optional (parse_annotation strict
   4.123 +                  ::: Scan.repeat ($$ "," |-- parse_annotation strict)) []
   4.124 +   >> flat) x
   4.125 +
   4.126 +(* Vampire proof lines sometimes contain needless information such as "(0:3)",
   4.127 +   which can be hard to disambiguate from function application in an LL(1)
   4.128 +   parser. As a workaround, we extend the TPTP term syntax with such detritus
   4.129 +   and ignore it. *)
   4.130 +fun parse_vampire_detritus x =
   4.131 +  (scan_general_id |-- $$ ":" --| scan_general_id >> K []) x
   4.132 +
   4.133 +fun parse_term pool x =
   4.134 +  ((scan_general_id >> repair_name pool)
   4.135 +    -- Scan.optional ($$ "(" |-- (parse_vampire_detritus || parse_terms pool)
   4.136 +                      --| $$ ")") []
   4.137 +    --| Scan.optional ($$ "(" |-- parse_vampire_detritus --| $$ ")") []
   4.138 +   >> ATerm) x
   4.139 +and parse_terms pool x =
   4.140 +  (parse_term pool ::: Scan.repeat ($$ "," |-- parse_term pool)) x
   4.141 +
   4.142 +fun parse_atom pool =
   4.143 +  parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "="
   4.144 +                                  -- parse_term pool)
   4.145 +  >> (fn (u1, NONE) => AAtom u1
   4.146 +       | (u1, SOME (NONE, u2)) => AAtom (ATerm ("c_equal", [u1, u2]))
   4.147 +       | (u1, SOME (SOME _, u2)) =>
   4.148 +         mk_anot (AAtom (ATerm ("c_equal", [u1, u2]))))
   4.149 +
   4.150 +fun fo_term_head (ATerm (s, _)) = s
   4.151 +
   4.152 +(* TPTP formulas are fully parenthesized, so we don't need to worry about
   4.153 +   operator precedence. *)
   4.154 +fun parse_formula pool x =
   4.155 +  (($$ "(" |-- parse_formula pool --| $$ ")"
   4.156 +    || ($$ "!" >> K AForall || $$ "?" >> K AExists)
   4.157 +       --| $$ "[" -- parse_terms pool --| $$ "]" --| $$ ":"
   4.158 +       -- parse_formula pool
   4.159 +       >> (fn ((q, ts), phi) => AQuant (q, map fo_term_head ts, phi))
   4.160 +    || $$ "~" |-- parse_formula pool >> mk_anot
   4.161 +    || parse_atom pool)
   4.162 +   -- Scan.option ((Scan.this_string "=>" >> K AImplies
   4.163 +                    || Scan.this_string "<=>" >> K AIff
   4.164 +                    || Scan.this_string "<~>" >> K ANotIff
   4.165 +                    || Scan.this_string "<=" >> K AIf
   4.166 +                    || $$ "|" >> K AOr || $$ "&" >> K AAnd)
   4.167 +                   -- parse_formula pool)
   4.168 +   >> (fn (phi1, NONE) => phi1
   4.169 +        | (phi1, SOME (c, phi2)) => mk_aconn c (phi1, phi2))) x
   4.170 +
   4.171 +val parse_tstp_extra_arguments =
   4.172 +  Scan.optional ($$ "," |-- parse_annotation false
   4.173 +                 --| Scan.option ($$ "," |-- parse_annotations false)) []
   4.174 +
   4.175 +(* Syntax: (fof|cnf)\(<num>, <formula_role>, <formula> <extra_arguments>\).
   4.176 +   The <num> could be an identifier, but we assume integers. *)
   4.177 + fun parse_tstp_line pool =
   4.178 +   ((Scan.this_string "fof" || Scan.this_string "cnf") -- $$ "(")
   4.179 +     |-- scan_general_id --| $$ "," -- Symbol.scan_id --| $$ ","
   4.180 +     -- parse_formula pool -- parse_tstp_extra_arguments --| $$ ")" --| $$ "."
   4.181 +    >> (fn (((num, role), phi), deps) =>
   4.182 +           let
   4.183 +             val (name, deps) =
   4.184 +               case deps of
   4.185 +                 ["file", _, s] => (Str (num, s), [])
   4.186 +               | _ => (Num num, deps)
   4.187 +           in
   4.188 +             case role of
   4.189 +               "definition" =>
   4.190 +               (case phi of
   4.191 +                  AConn (AIff, [phi1 as AAtom _, phi2]) =>
   4.192 +                  Definition (name, phi1, phi2)
   4.193 +                | AAtom (ATerm ("c_equal", _)) =>
   4.194 +                  (* Vampire's equality proxy axiom *)
   4.195 +                  Inference (name, phi, map Num deps)
   4.196 +                | _ => raise Fail "malformed definition")
   4.197 +             | _ => Inference (name, phi, map Num deps)
   4.198 +           end)
   4.199 +
   4.200 +(**** PARSING OF VAMPIRE OUTPUT ****)
   4.201 +
   4.202 +(* Syntax: <num>. <formula> <annotation> *)
   4.203 +fun parse_vampire_line pool =
   4.204 +  scan_general_id --| $$ "." -- parse_formula pool -- parse_annotation true
   4.205 +  >> (fn ((num, phi), deps) => Inference (Num num, phi, map Num deps))
   4.206 +
   4.207 +(**** PARSING OF SPASS OUTPUT ****)
   4.208 +
   4.209 +(* SPASS returns clause references of the form "x.y". We ignore "y", whose role
   4.210 +   is not clear anyway. *)
   4.211 +val parse_dot_name = scan_general_id --| $$ "." --| scan_general_id
   4.212 +
   4.213 +val parse_spass_annotations =
   4.214 +  Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name
   4.215 +                                         --| Scan.option ($$ ","))) []
   4.216 +
   4.217 +(* It is not clear why some literals are followed by sequences of stars and/or
   4.218 +   pluses. We ignore them. *)
   4.219 +fun parse_decorated_atom pool =
   4.220 +  parse_atom pool --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
   4.221 +
   4.222 +fun mk_horn ([], []) = AAtom (ATerm ("c_False", []))
   4.223 +  | mk_horn ([], pos_lits) = foldr1 (mk_aconn AOr) pos_lits
   4.224 +  | mk_horn (neg_lits, []) = mk_anot (foldr1 (mk_aconn AAnd) neg_lits)
   4.225 +  | mk_horn (neg_lits, pos_lits) =
   4.226 +    mk_aconn AImplies (foldr1 (mk_aconn AAnd) neg_lits,
   4.227 +                       foldr1 (mk_aconn AOr) pos_lits)
   4.228 +
   4.229 +fun parse_horn_clause pool =
   4.230 +  Scan.repeat (parse_decorated_atom pool) --| $$ "|" --| $$ "|"
   4.231 +    -- Scan.repeat (parse_decorated_atom pool) --| $$ "-" --| $$ ">"
   4.232 +    -- Scan.repeat (parse_decorated_atom pool)
   4.233 +  >> (mk_horn o apfst (op @))
   4.234 +
   4.235 +(* Syntax: <num>[0:<inference><annotations>]
   4.236 +   <atoms> || <atoms> -> <atoms>. *)
   4.237 +fun parse_spass_line pool =
   4.238 +  scan_general_id --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
   4.239 +    -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
   4.240 +  >> (fn ((num, deps), u) => Inference (Num num, u, map Num deps))
   4.241 +
   4.242 +fun parse_line pool =
   4.243 +  parse_tstp_line pool || parse_vampire_line pool || parse_spass_line pool
   4.244 +fun parse_lines pool = Scan.repeat1 (parse_line pool)
   4.245 +fun parse_proof pool =
   4.246 +  fst o Scan.finite Symbol.stopper
   4.247 +            (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
   4.248 +                            (parse_lines pool)))
   4.249 +  o explode o strip_spaces_except_between_ident_chars (*### FIXME: why isn't strip_spaces enough?*)
   4.250 +
   4.251 +fun clean_up_dependency seen dep = find_first (curry is_same_step dep) seen
   4.252 +fun clean_up_dependencies _ [] = []
   4.253 +  | clean_up_dependencies seen ((step as Definition (name, _, _)) :: steps) =
   4.254 +    step :: clean_up_dependencies (name :: seen) steps
   4.255 +  | clean_up_dependencies seen (Inference (name, u, deps) :: steps) =
   4.256 +    Inference (name, u, map_filter (clean_up_dependency seen) deps) ::
   4.257 +    clean_up_dependencies (name :: seen) steps
   4.258 +
   4.259 +fun atp_proof_from_tstplike_string pool =
   4.260 +  suffix "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
   4.261 +  #> parse_proof pool
   4.262 +  #> sort (step_name_ord o pairself step_name)
   4.263 +  #> clean_up_dependencies []
   4.264 +
   4.265 +end;
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Sep 16 09:59:32 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Sep 16 11:12:08 2010 +0200
     5.3 @@ -40,7 +40,7 @@
     5.4       used_thm_names: (string * locality) list,
     5.5       atp_run_time_in_msecs: int,
     5.6       output: string,
     5.7 -     proof: string,
     5.8 +     tstplike_proof: string,
     5.9       axiom_names: (string * locality) list vector,
    5.10       conjecture_shape: int list list}
    5.11    type prover = params -> minimize_command -> problem -> prover_result
    5.12 @@ -111,7 +111,7 @@
    5.13     used_thm_names: (string * locality) list,
    5.14     atp_run_time_in_msecs: int,
    5.15     output: string,
    5.16 -   proof: string,
    5.17 +   tstplike_proof: string,
    5.18     axiom_names: (string * locality) list vector,
    5.19     conjecture_shape: int list list}
    5.20  
    5.21 @@ -153,23 +153,23 @@
    5.22             |> space_implode "\n " |> quote
    5.23  
    5.24  (* Splits by the first possible of a list of delimiters. *)
    5.25 -fun extract_proof delims output =
    5.26 +fun extract_tstplike_proof delims output =
    5.27    case pairself (find_first (fn s => String.isSubstring s output))
    5.28                  (ListPair.unzip delims) of
    5.29      (SOME begin_delim, SOME end_delim) =>
    5.30      extract_delimited (begin_delim, end_delim) output
    5.31    | _ => ""
    5.32  
    5.33 -fun extract_proof_and_outcome complete res_code proof_delims known_failures
    5.34 -                              output =
    5.35 +fun extract_tstplike_proof_and_outcome complete res_code proof_delims
    5.36 +                                       known_failures output =
    5.37    case known_failure_in_output output known_failures of
    5.38 -    NONE => (case extract_proof proof_delims output of
    5.39 +    NONE => (case extract_tstplike_proof proof_delims output of
    5.40               "" => ("", SOME (if res_code = 0 andalso output = "" then
    5.41                                  Interrupted
    5.42                                else
    5.43                                   UnknownError))
    5.44 -           | proof => if res_code = 0 then (proof, NONE)
    5.45 -                      else ("", SOME UnknownError))
    5.46 +           | tstplike_proof => if res_code = 0 then (tstplike_proof, NONE)
    5.47 +                               else ("", SOME UnknownError))
    5.48    | SOME failure =>
    5.49      ("", SOME (if failure = IncompleteUnprovable andalso complete then
    5.50                   Unprovable
    5.51 @@ -297,16 +297,16 @@
    5.52                         else
    5.53                           I)
    5.54                    |>> (if measure_run_time then split_time else rpair 0)
    5.55 -                val (proof, outcome) =
    5.56 -                  extract_proof_and_outcome complete res_code proof_delims
    5.57 -                                            known_failures output
    5.58 -              in (output, msecs, proof, outcome) end
    5.59 +                val (tstplike_proof, outcome) =
    5.60 +                  extract_tstplike_proof_and_outcome complete res_code
    5.61 +                      proof_delims known_failures output
    5.62 +              in (output, msecs, tstplike_proof, outcome) end
    5.63              val readable_names = debug andalso overlord
    5.64              val (problem, pool, conjecture_offset, axiom_names) =
    5.65                prepare_problem ctxt readable_names explicit_forall full_types
    5.66                                explicit_apply hyp_ts concl_t axioms
    5.67 -            val ss = strings_for_tptp_problem use_conjecture_for_hypotheses
    5.68 -                                              problem
    5.69 +            val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses
    5.70 +                                                  problem
    5.71              val _ = File.write_list probfile ss
    5.72              val conjecture_shape =
    5.73                conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1
    5.74 @@ -322,8 +322,8 @@
    5.75                |> run_twice
    5.76                   ? (fn (_, msecs0, _, SOME _) =>
    5.77                         run true (Time.- (timeout, Timer.checkRealTimer timer))
    5.78 -                       |> (fn (output, msecs, proof, outcome) =>
    5.79 -                              (output, msecs0 + msecs, proof, outcome))
    5.80 +                       |> (fn (output, msecs, tstplike_proof, outcome) =>
    5.81 +                              (output, msecs0 + msecs, tstplike_proof, outcome))
    5.82                       | result => result)
    5.83            in ((pool, conjecture_shape, axiom_names), result) end
    5.84          else
    5.85 @@ -339,7 +339,7 @@
    5.86        else
    5.87          File.write (Path.explode (Path.implode probfile ^ "_proof")) output
    5.88      val ((pool, conjecture_shape, axiom_names),
    5.89 -         (output, msecs, proof, outcome)) =
    5.90 +         (output, msecs, tstplike_proof, outcome)) =
    5.91        with_path cleanup export run_on problem_path_name
    5.92      val (conjecture_shape, axiom_names) =
    5.93        repair_conjecture_shape_and_theorem_names output conjecture_shape
    5.94 @@ -352,8 +352,8 @@
    5.95          NONE =>
    5.96          proof_text isar_proof
    5.97              (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
    5.98 -            (banner, full_types, minimize_command, proof, axiom_names, goal,
    5.99 -             subgoal)
   5.100 +            (banner, full_types, minimize_command, tstplike_proof, axiom_names,
   5.101 +             goal, subgoal)
   5.102          |>> (fn message =>
   5.103                  message ^ (if verbose then
   5.104                               "\nATP real CPU time: " ^ string_of_int msecs ^
   5.105 @@ -369,8 +369,8 @@
   5.106    in
   5.107      {outcome = outcome, message = message, pool = pool,
   5.108       used_thm_names = used_thm_names, atp_run_time_in_msecs = msecs,
   5.109 -     output = output, proof = proof, axiom_names = axiom_names,
   5.110 -     conjecture_shape = conjecture_shape}
   5.111 +     output = output, tstplike_proof = tstplike_proof,
   5.112 +     axiom_names = axiom_names, conjecture_shape = conjecture_shape}
   5.113    end
   5.114  
   5.115  fun get_prover_fun thy name = prover_fun false name (get_prover thy name)
     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Sep 16 09:59:32 2010 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Sep 16 11:12:08 2010 +0200
     6.3 @@ -117,7 +117,7 @@
     6.4           val new_timeout =
     6.5             Int.min (msecs, Time.toMilliseconds time + fudge_msecs)
     6.6             |> Time.fromMilliseconds
     6.7 -         val (min_thms, {proof, axiom_names, ...}) =
     6.8 +         val (min_thms, {tstplike_proof, axiom_names, ...}) =
     6.9             sublinear_minimize (do_test new_timeout)
    6.10                 (filter_used_facts used_thm_names axioms) ([], result)
    6.11           val n = length min_thms
    6.12 @@ -130,8 +130,8 @@
    6.13           (SOME min_thms,
    6.14            proof_text isar_proof
    6.15                (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
    6.16 -              ("Minimized command", full_types, K "", proof, axiom_names, goal,
    6.17 -               i) |> fst)
    6.18 +              ("Minimized command", full_types, K "", tstplike_proof,
    6.19 +               axiom_names, goal, i) |> fst)
    6.20         end
    6.21       | {outcome = SOME TimedOut, ...} =>
    6.22         (NONE, "Timeout: You can increase the time limit using the \"timeout\" \
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Sep 16 09:59:32 2010 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Sep 16 11:12:08 2010 +0200
     7.3 @@ -26,6 +26,7 @@
     7.4  struct
     7.5  
     7.6  open ATP_Problem
     7.7 +open ATP_Proof
     7.8  open Metis_Clauses
     7.9  open Sledgehammer_Util
    7.10  open Sledgehammer_Filter
    7.11 @@ -58,31 +59,21 @@
    7.12    | s_iff (t1, @{const True}) = t1
    7.13    | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
    7.14  
    7.15 -fun mk_anot (AConn (ANot, [phi])) = phi
    7.16 -  | mk_anot phi = AConn (ANot, [phi])
    7.17 -fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
    7.18 -
    7.19  fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
    7.20  fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t
    7.21  
    7.22 -datatype raw_step_name = Str of string * string | Num of string
    7.23 -
    7.24 -fun raw_step_num (Str (num, _)) = num
    7.25 -  | raw_step_num (Num num) = num
    7.26 -
    7.27 -fun same_raw_step s t = raw_step_num s = raw_step_num t
    7.28 -
    7.29 -fun raw_step_name_ord p =
    7.30 -  let val q = pairself raw_step_num p in
    7.31 -    (* The "unprefix" part is to cope with remote Vampire's output. The proper
    7.32 -       solution would be to perform a topological sort, e.g. using the nice
    7.33 -       "Graph" functor. *)
    7.34 -    case pairself (Int.fromString o perhaps (try (unprefix "f"))) q of
    7.35 -      (NONE, NONE) => string_ord q
    7.36 -    | (NONE, SOME _) => LESS
    7.37 -    | (SOME _, NONE) => GREATER
    7.38 -    | (SOME i, SOME j) => int_ord (i, j)
    7.39 -  end
    7.40 +fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) =
    7.41 +    Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
    7.42 +  | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
    7.43 +    Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
    7.44 +  | negate_term (@{const HOL.implies} $ t1 $ t2) =
    7.45 +    @{const HOL.conj} $ t1 $ negate_term t2
    7.46 +  | negate_term (@{const HOL.conj} $ t1 $ t2) =
    7.47 +    @{const HOL.disj} $ negate_term t1 $ negate_term t2
    7.48 +  | negate_term (@{const HOL.disj} $ t1 $ t2) =
    7.49 +    @{const HOL.conj} $ negate_term t1 $ negate_term t2
    7.50 +  | negate_term (@{const Not} $ t) = t
    7.51 +  | negate_term t = @{const Not} $ t
    7.52  
    7.53  fun index_in_shape x = find_index (exists (curry (op =) x))
    7.54  fun resolve_axiom axiom_names (Str (_, s)) =
    7.55 @@ -113,188 +104,6 @@
    7.56      resolve_conjecture conjecture_shape (Str (num, "")) (* HACK *)
    7.57  val is_conjecture = not o null oo resolve_conjecture
    7.58  
    7.59 -fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) =
    7.60 -    Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t')
    7.61 -  | negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
    7.62 -    Const (@{const_name All}, T) $ Abs (s, T', negate_term t')
    7.63 -  | negate_term (@{const HOL.implies} $ t1 $ t2) =
    7.64 -    @{const HOL.conj} $ t1 $ negate_term t2
    7.65 -  | negate_term (@{const HOL.conj} $ t1 $ t2) =
    7.66 -    @{const HOL.disj} $ negate_term t1 $ negate_term t2
    7.67 -  | negate_term (@{const HOL.disj} $ t1 $ t2) =
    7.68 -    @{const HOL.conj} $ negate_term t1 $ negate_term t2
    7.69 -  | negate_term (@{const Not} $ t) = t
    7.70 -  | negate_term t = @{const Not} $ t
    7.71 -
    7.72 -datatype ('a, 'b, 'c) raw_step =
    7.73 -  Definition of raw_step_name * 'a * 'b |
    7.74 -  Inference of raw_step_name * 'c * raw_step_name list
    7.75 -
    7.76 -(**** PARSING OF TSTP FORMAT ****)
    7.77 -
    7.78 -(*Strings enclosed in single quotes, e.g. filenames*)
    7.79 -val scan_general_id =
    7.80 -  $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode
    7.81 -  || Scan.repeat ($$ "$") -- Scan.many1 Symbol.is_letdig
    7.82 -     >> (fn (ss1, ss2) => implode ss1 ^ implode ss2)
    7.83 -
    7.84 -fun repair_name _ "$true" = "c_True"
    7.85 -  | repair_name _ "$false" = "c_False"
    7.86 -  | repair_name _ "$$e" = "c_equal" (* seen in Vampire proofs *)
    7.87 -  | repair_name _ "equal" = "c_equal" (* needed by SPASS? *)
    7.88 -  | repair_name pool s =
    7.89 -    case Symtab.lookup pool s of
    7.90 -      SOME s' => s'
    7.91 -    | NONE =>
    7.92 -      if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then
    7.93 -        "c_equal" (* seen in Vampire proofs *)
    7.94 -      else
    7.95 -        s
    7.96 -(* Generalized first-order terms, which include file names, numbers, etc. *)
    7.97 -fun parse_annotation strict x =
    7.98 -  ((scan_general_id ::: Scan.repeat ($$ " " |-- scan_general_id)
    7.99 -      >> (strict ? filter (is_some o Int.fromString)))
   7.100 -   -- Scan.optional (parse_annotation strict) [] >> op @
   7.101 -   || $$ "(" |-- parse_annotations strict --| $$ ")"
   7.102 -   || $$ "[" |-- parse_annotations strict --| $$ "]") x
   7.103 -and parse_annotations strict x =
   7.104 -  (Scan.optional (parse_annotation strict
   7.105 -                  ::: Scan.repeat ($$ "," |-- parse_annotation strict)) []
   7.106 -   >> flat) x
   7.107 -
   7.108 -(* Vampire proof lines sometimes contain needless information such as "(0:3)",
   7.109 -   which can be hard to disambiguate from function application in an LL(1)
   7.110 -   parser. As a workaround, we extend the TPTP term syntax with such detritus
   7.111 -   and ignore it. *)
   7.112 -fun parse_vampire_detritus x =
   7.113 -  (scan_general_id |-- $$ ":" --| scan_general_id >> K []) x
   7.114 -
   7.115 -fun parse_term pool x =
   7.116 -  ((scan_general_id >> repair_name pool)
   7.117 -    -- Scan.optional ($$ "(" |-- (parse_vampire_detritus || parse_terms pool)
   7.118 -                      --| $$ ")") []
   7.119 -    --| Scan.optional ($$ "(" |-- parse_vampire_detritus --| $$ ")") []
   7.120 -   >> ATerm) x
   7.121 -and parse_terms pool x =
   7.122 -  (parse_term pool ::: Scan.repeat ($$ "," |-- parse_term pool)) x
   7.123 -
   7.124 -fun parse_atom pool =
   7.125 -  parse_term pool -- Scan.option (Scan.option ($$ "!") --| $$ "="
   7.126 -                                  -- parse_term pool)
   7.127 -  >> (fn (u1, NONE) => AAtom u1
   7.128 -       | (u1, SOME (NONE, u2)) => AAtom (ATerm ("c_equal", [u1, u2]))
   7.129 -       | (u1, SOME (SOME _, u2)) =>
   7.130 -         mk_anot (AAtom (ATerm ("c_equal", [u1, u2]))))
   7.131 -
   7.132 -fun fo_term_head (ATerm (s, _)) = s
   7.133 -
   7.134 -(* TPTP formulas are fully parenthesized, so we don't need to worry about
   7.135 -   operator precedence. *)
   7.136 -fun parse_formula pool x =
   7.137 -  (($$ "(" |-- parse_formula pool --| $$ ")"
   7.138 -    || ($$ "!" >> K AForall || $$ "?" >> K AExists)
   7.139 -       --| $$ "[" -- parse_terms pool --| $$ "]" --| $$ ":"
   7.140 -       -- parse_formula pool
   7.141 -       >> (fn ((q, ts), phi) => AQuant (q, map fo_term_head ts, phi))
   7.142 -    || $$ "~" |-- parse_formula pool >> mk_anot
   7.143 -    || parse_atom pool)
   7.144 -   -- Scan.option ((Scan.this_string "=>" >> K AImplies
   7.145 -                    || Scan.this_string "<=>" >> K AIff
   7.146 -                    || Scan.this_string "<~>" >> K ANotIff
   7.147 -                    || Scan.this_string "<=" >> K AIf
   7.148 -                    || $$ "|" >> K AOr || $$ "&" >> K AAnd)
   7.149 -                   -- parse_formula pool)
   7.150 -   >> (fn (phi1, NONE) => phi1
   7.151 -        | (phi1, SOME (c, phi2)) => mk_aconn c (phi1, phi2))) x
   7.152 -
   7.153 -val parse_tstp_extra_arguments =
   7.154 -  Scan.optional ($$ "," |-- parse_annotation false
   7.155 -                 --| Scan.option ($$ "," |-- parse_annotations false)) []
   7.156 -
   7.157 -(* Syntax: (fof|cnf)\(<num>, <formula_role>, <formula> <extra_arguments>\).
   7.158 -   The <num> could be an identifier, but we assume integers. *)
   7.159 - fun parse_tstp_line pool =
   7.160 -   ((Scan.this_string "fof" || Scan.this_string "cnf") -- $$ "(")
   7.161 -     |-- scan_general_id --| $$ "," -- Symbol.scan_id --| $$ ","
   7.162 -     -- parse_formula pool -- parse_tstp_extra_arguments --| $$ ")" --| $$ "."
   7.163 -    >> (fn (((num, role), phi), deps) =>
   7.164 -           let
   7.165 -             val (name, deps) =
   7.166 -               case deps of
   7.167 -                 ["file", _, s] => (Str (num, s), [])
   7.168 -               | _ => (Num num, deps)
   7.169 -           in
   7.170 -             case role of
   7.171 -               "definition" =>
   7.172 -               (case phi of
   7.173 -                  AConn (AIff, [phi1 as AAtom _, phi2]) =>
   7.174 -                  Definition (name, phi1, phi2)
   7.175 -                | AAtom (ATerm ("c_equal", _)) =>
   7.176 -                  (* Vampire's equality proxy axiom *)
   7.177 -                  Inference (name, phi, map Num deps)
   7.178 -                | _ => raise Fail "malformed definition")
   7.179 -             | _ => Inference (name, phi, map Num deps)
   7.180 -           end)
   7.181 -
   7.182 -(**** PARSING OF VAMPIRE OUTPUT ****)
   7.183 -
   7.184 -(* Syntax: <num>. <formula> <annotation> *)
   7.185 -fun parse_vampire_line pool =
   7.186 -  scan_general_id --| $$ "." -- parse_formula pool -- parse_annotation true
   7.187 -  >> (fn ((num, phi), deps) => Inference (Num num, phi, map Num deps))
   7.188 -
   7.189 -(**** PARSING OF SPASS OUTPUT ****)
   7.190 -
   7.191 -(* SPASS returns clause references of the form "x.y". We ignore "y", whose role
   7.192 -   is not clear anyway. *)
   7.193 -val parse_dot_name = scan_general_id --| $$ "." --| scan_general_id
   7.194 -
   7.195 -val parse_spass_annotations =
   7.196 -  Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name
   7.197 -                                         --| Scan.option ($$ ","))) []
   7.198 -
   7.199 -(* It is not clear why some literals are followed by sequences of stars and/or
   7.200 -   pluses. We ignore them. *)
   7.201 -fun parse_decorated_atom pool =
   7.202 -  parse_atom pool --| Scan.repeat ($$ "*" || $$ "+" || $$ " ")
   7.203 -
   7.204 -fun mk_horn ([], []) = AAtom (ATerm ("c_False", []))
   7.205 -  | mk_horn ([], pos_lits) = foldr1 (mk_aconn AOr) pos_lits
   7.206 -  | mk_horn (neg_lits, []) = mk_anot (foldr1 (mk_aconn AAnd) neg_lits)
   7.207 -  | mk_horn (neg_lits, pos_lits) =
   7.208 -    mk_aconn AImplies (foldr1 (mk_aconn AAnd) neg_lits,
   7.209 -                       foldr1 (mk_aconn AOr) pos_lits)
   7.210 -
   7.211 -fun parse_horn_clause pool =
   7.212 -  Scan.repeat (parse_decorated_atom pool) --| $$ "|" --| $$ "|"
   7.213 -    -- Scan.repeat (parse_decorated_atom pool) --| $$ "-" --| $$ ">"
   7.214 -    -- Scan.repeat (parse_decorated_atom pool)
   7.215 -  >> (mk_horn o apfst (op @))
   7.216 -
   7.217 -(* Syntax: <num>[0:<inference><annotations>]
   7.218 -   <atoms> || <atoms> -> <atoms>. *)
   7.219 -fun parse_spass_line pool =
   7.220 -  scan_general_id --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
   7.221 -    -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
   7.222 -  >> (fn ((num, deps), u) => Inference (Num num, u, map Num deps))
   7.223 -
   7.224 -fun parse_line pool =
   7.225 -  parse_tstp_line pool || parse_vampire_line pool || parse_spass_line pool
   7.226 -fun parse_lines pool = Scan.repeat1 (parse_line pool)
   7.227 -fun parse_proof pool =
   7.228 -  fst o Scan.finite Symbol.stopper
   7.229 -            (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
   7.230 -                            (parse_lines pool)))
   7.231 -  o explode o strip_spaces_except_between_ident_chars
   7.232 -
   7.233 -fun clean_up_dependencies _ [] = []
   7.234 -  | clean_up_dependencies seen ((step as Definition (name, _, _)) :: steps) =
   7.235 -    step :: clean_up_dependencies (name :: seen) steps
   7.236 -  | clean_up_dependencies seen (Inference (name, u, deps) :: steps) =
   7.237 -    Inference (name, u,
   7.238 -             map_filter (fn dep => find_first (same_raw_step dep) seen) deps) ::
   7.239 -    clean_up_dependencies (name :: seen) steps
   7.240 -
   7.241  (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
   7.242  
   7.243  exception FO_TERM of string fo_term list
   7.244 @@ -411,7 +220,7 @@
   7.245                  case strip_prefix_and_unascii schematic_var_prefix a of
   7.246                    SOME b => Var ((b, 0), T)
   7.247                  | NONE =>
   7.248 -                  if is_tptp_variable a then
   7.249 +                  if is_atp_variable a then
   7.250                      Var ((repair_atp_variable_name Char.toLower a, 0), T)
   7.251                    else
   7.252                      (* Skolem constants? *)
   7.253 @@ -537,7 +346,7 @@
   7.254  val is_only_type_information = curry (op aconv) HOLogic.true_const
   7.255  
   7.256  fun replace_one_dependency (old, new) dep =
   7.257 -  if raw_step_num dep = raw_step_num old then new else [dep]
   7.258 +  if is_same_step (dep, old) then new else [dep]
   7.259  fun replace_dependencies_in_line _ (line as Definition _) = line
   7.260    | replace_dependencies_in_line p (Inference (name, t, deps)) =
   7.261      Inference (name, t, fold (union (op =) o replace_one_dependency p) deps [])
   7.262 @@ -620,12 +429,13 @@
   7.263        | aux line (s :: rest) = aux (s :: line) rest
   7.264    in aux [] o explode end
   7.265  
   7.266 +(* ### FIXME: Can do better *)
   7.267  (* A list consisting of the first number in each line is returned. For TSTP,
   7.268     interesting lines have the form "fof(108, axiom, ...)", where the number
   7.269     (108) is extracted. For SPASS, lines have the form "108[0:Inp] ...", where
   7.270     the first number (108) is extracted. For Vampire, we look for
   7.271     "108. ... [input]". *)
   7.272 -fun used_facts_in_atp_proof axiom_names atp_proof =
   7.273 +fun used_facts_in_tstplike_proof axiom_names tstplike_proof =
   7.274    let
   7.275      val tokens_of =
   7.276        String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
   7.277 @@ -648,7 +458,7 @@
   7.278             "input" => resolve_axiom axiom_names (Num num)
   7.279           | _ => [])
   7.280        | do_line _ = []
   7.281 -  in atp_proof |> split_proof_lines |> maps (do_line o tokens_of) end
   7.282 +  in tstplike_proof |> split_proof_lines |> maps (do_line o tokens_of) end
   7.283  
   7.284  val indent_size = 2
   7.285  val no_label = ("", ~1)
   7.286 @@ -662,9 +472,9 @@
   7.287  fun raw_label_for_name conjecture_shape name =
   7.288    case resolve_conjecture conjecture_shape name of
   7.289      [j] => (conjecture_prefix, j)
   7.290 -  | _ => case Int.fromString (raw_step_num name) of
   7.291 +  | _ => case Int.fromString (step_num name) of
   7.292             SOME j => (raw_prefix, j)
   7.293 -         | NONE => (raw_prefix ^ raw_step_num name, 0)
   7.294 +         | NONE => (raw_prefix ^ step_num name, 0)
   7.295  
   7.296  fun metis_using [] = ""
   7.297    | metis_using ls =
   7.298 @@ -690,14 +500,15 @@
   7.299        Markup.markup Markup.sendback command ^ "."
   7.300  
   7.301  fun used_facts axiom_names =
   7.302 -  used_facts_in_atp_proof axiom_names
   7.303 +  used_facts_in_tstplike_proof axiom_names
   7.304    #> List.partition (curry (op =) Chained o snd)
   7.305    #> pairself (sort_distinct (string_ord o pairself fst))
   7.306  
   7.307 -fun metis_proof_text (banner, full_types, minimize_command, atp_proof,
   7.308 -                      axiom_names, goal, i) =
   7.309 +fun metis_proof_text (banner, full_types, minimize_command,
   7.310 +                      tstplike_proof, axiom_names, goal, i) =
   7.311    let
   7.312 -    val (chained_lemmas, other_lemmas) = used_facts axiom_names atp_proof
   7.313 +    val (chained_lemmas, other_lemmas) =
   7.314 +      used_facts axiom_names tstplike_proof
   7.315      val n = Logic.count_prems (prop_of goal)
   7.316    in
   7.317      (metis_line banner full_types i n (map fst other_lemmas) ^
   7.318 @@ -713,16 +524,16 @@
   7.319  type label = string * int
   7.320  type facts = label list * string list
   7.321  
   7.322 -datatype qualifier = Show | Then | Moreover | Ultimately
   7.323 +datatype isar_qualifier = Show | Then | Moreover | Ultimately
   7.324  
   7.325 -datatype step =
   7.326 +datatype isar_step =
   7.327    Fix of (string * typ) list |
   7.328    Let of term * term |
   7.329    Assume of label * term |
   7.330 -  Have of qualifier list * label * term * byline
   7.331 +  Have of isar_qualifier list * label * term * byline
   7.332  and byline =
   7.333    ByMetis of facts |
   7.334 -  CaseSplit of step list list * facts
   7.335 +  CaseSplit of isar_step list list * facts
   7.336  
   7.337  fun smart_case_split [] facts = ByMetis facts
   7.338    | smart_case_split proofs facts = CaseSplit (proofs, facts)
   7.339 @@ -743,17 +554,12 @@
   7.340            ByMetis (fold (add_fact_from_dependency conjecture_shape axiom_names)
   7.341                          deps ([], [])))
   7.342  
   7.343 -fun raw_step_name (Definition (name, _, _)) = name
   7.344 -  | raw_step_name (Inference (name, _, _)) = name
   7.345 -
   7.346 -fun proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
   7.347 -                         atp_proof conjecture_shape axiom_names params frees =
   7.348 +fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees isar_shrink_factor
   7.349 +        tstplike_proof conjecture_shape axiom_names params frees =
   7.350    let
   7.351      val lines =
   7.352 -      atp_proof ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
   7.353 -      |> parse_proof pool
   7.354 -      |> sort (raw_step_name_ord o pairself raw_step_name)
   7.355 -      |> clean_up_dependencies []
   7.356 +      tstplike_proof
   7.357 +      |> atp_proof_from_tstplike_string pool
   7.358        |> decode_lines ctxt full_types tfrees
   7.359        |> rpair [] |-> fold_rev (add_line conjecture_shape axiom_names)
   7.360        |> rpair [] |-> fold_rev add_nontrivial_line
   7.361 @@ -1049,14 +855,13 @@
   7.362      and do_proof [Have (_, _, _, ByMetis _)] = ""
   7.363        | do_proof proof =
   7.364          (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
   7.365 -        do_indent 0 ^ "proof -\n" ^
   7.366 -        do_steps "" "" 1 proof ^
   7.367 -        do_indent 0 ^ (if n <> 1 then "next" else "qed")
   7.368 +        do_indent 0 ^ "proof -\n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^
   7.369 +        (if n <> 1 then "next" else "qed")
   7.370    in do_proof end
   7.371  
   7.372  fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   7.373 -                    (other_params as (_, full_types, _, atp_proof, axiom_names,
   7.374 -                                      goal, i)) =
   7.375 +                    (other_params as (_, full_types, _, tstplike_proof,
   7.376 +                                      axiom_names, goal, i)) =
   7.377    let
   7.378      val (params, hyp_ts, concl_t) = strip_subgoal goal i
   7.379      val frees = fold Term.add_frees (concl_t :: hyp_ts) []
   7.380 @@ -1064,9 +869,9 @@
   7.381      val n = Logic.count_prems (prop_of goal)
   7.382      val (one_line_proof, lemma_names) = metis_proof_text other_params
   7.383      fun isar_proof_for () =
   7.384 -      case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor
   7.385 -                                atp_proof conjecture_shape axiom_names params
   7.386 -                                frees
   7.387 +      case isar_proof_from_tstplike_proof pool ctxt full_types tfrees
   7.388 +               isar_shrink_factor tstplike_proof conjecture_shape axiom_names
   7.389 +               params frees
   7.390             |> redirect_proof hyp_ts concl_t
   7.391             |> kill_duplicate_assumptions_in_proof
   7.392             |> then_chain_proof
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Sep 16 09:59:32 2010 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Sep 16 11:12:08 2010 +0200
     8.3 @@ -376,7 +376,7 @@
     8.4  type const_info = {min_arity: int, max_arity: int, sub_level: bool}
     8.5  
     8.6  fun consider_term top_level (ATerm ((s, _), ts)) =
     8.7 -  (if is_tptp_variable s then
     8.8 +  (if is_atp_variable s then
     8.9       I
    8.10     else
    8.11       let val n = length ts in
    8.12 @@ -468,7 +468,7 @@
    8.13  fun close_universally phi =
    8.14    let
    8.15      fun term_vars bounds (ATerm (name as (s, _), tms)) =
    8.16 -        (is_tptp_variable s andalso not (member (op =) bounds name))
    8.17 +        (is_atp_variable s andalso not (member (op =) bounds name))
    8.18            ? insert (op =) name
    8.19          #> fold (term_vars bounds) tms
    8.20      fun formula_vars bounds (AQuant (_, xs, phi)) =
    8.21 @@ -524,7 +524,7 @@
    8.22         ("Conjectures", conjecture_lines),
    8.23         ("Type variables", tfree_lines)]
    8.24        |> repair_problem thy explicit_forall full_types explicit_apply
    8.25 -    val (problem, pool) = nice_tptp_problem readable_names problem
    8.26 +    val (problem, pool) = nice_atp_problem readable_names problem
    8.27      val conjecture_offset =
    8.28        length axiom_lines + length class_rel_lines + length arity_lines
    8.29        + length helper_lines