src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML

 open Sledgehammer_Fact_Filter
 open Sledgehammer_TPTP_Format
 
 type minimize_command = string list -> string
 
-fun is_ident_char c = Char.isAlphaNum c orelse c = #"_"
-fun is_head_digit s = Char.isDigit (String.sub (s, 0))
-
 val index_in_shape : int -> int list list -> int =
   find_index o exists o curry (op =)
-fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names
+fun is_axiom_clause_number thm_names num =
+  num > 0 andalso num <= Vector.length thm_names andalso
+  Vector.sub (thm_names, num - 1) <> ""
 fun is_conjecture_clause_number conjecture_shape num =
   index_in_shape num conjecture_shape >= 0
 
 fun smart_lambda v t =
   Abs (case v of

   Definition of 'a * 'b * 'c |
   Inference of 'a * 'd * 'e list
 
 (**** PARSING OF TSTP FORMAT ****)
 
-fun strip_spaces_in_list [] = ""
-  | strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1
-  | strip_spaces_in_list [c1, c2] =
-    strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2]
-  | strip_spaces_in_list (c1 :: c2 :: c3 :: cs) =
-    if Char.isSpace c1 then
-      strip_spaces_in_list (c2 :: c3 :: cs)
-    else if Char.isSpace c2 then
-      if Char.isSpace c3 then
-        strip_spaces_in_list (c1 :: c3 :: cs)
-      else
-        str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^
-        strip_spaces_in_list (c3 :: cs)
-    else
-      str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs)
-val strip_spaces = strip_spaces_in_list o String.explode
-
 (* Syntax trees, either term list or formulae *)
 datatype node = IntLeaf of int | StrNode of string * node list
 
 fun str_leaf s = StrNode (s, [])
 
 fun scons (x, y) = StrNode ("cons", [x, y])
 val slist_of = List.foldl scons (str_leaf "nil")
 
 (*Strings enclosed in single quotes, e.g. filenames*)
 val parse_quoted = $$ "'" |-- Scan.repeat (~$$ "'") --| $$ "'" >> implode;
-
-(*Integer constants, typically proof line numbers*)
-val parse_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
 
 val parse_dollar_name =
   Scan.repeat ($$ "$") -- Symbol.scan_id >> (fn (ss, s) => implode ss ^ s)
 
 (* needed for SPASS's output format *)

 (* Generalized first-order terms, which include file names, numbers, etc. *)
 (* The "x" argument is not strictly necessary, but without it Poly/ML loops
    forever at compile time. *)
 fun parse_term pool x =
      (parse_quoted >> str_leaf
-   || parse_integer >> IntLeaf
+   || scan_integer >> IntLeaf
    || (parse_dollar_name >> repair_name pool)
       -- Scan.optional ($$ "(" |-- parse_terms pool --| $$ ")") [] >> StrNode
    || $$ "(" |-- parse_term pool --| $$ ")"
    || $$ "[" |-- Scan.optional (parse_terms pool) [] --| $$ "]" >> slist_of) x
 and parse_terms pool x =

 (* Syntax: cnf(<num>, <formula_role>, <cnf_formula> <annotations>).
    The <num> could be an identifier, but we assume integers. *)
 fun finish_tstp_definition_line (num, (u, us)) = Definition (num, u, us)
 fun finish_tstp_inference_line ((num, us), deps) = Inference (num, us, deps)
 fun parse_tstp_line pool =
-     ((Scan.this_string "fof" -- $$ "(") |-- parse_integer --| $$ ","
+     ((Scan.this_string "fof" -- $$ "(") |-- scan_integer --| $$ ","
        --| Scan.this_string "definition" --| $$ "," -- parse_definition pool
        --| parse_tstp_annotations --| $$ ")" --| $$ "."
       >> finish_tstp_definition_line)
-  || ((Scan.this_string "cnf" -- $$ "(") |-- parse_integer --| $$ ","
+  || ((Scan.this_string "cnf" -- $$ "(") |-- scan_integer --| $$ ","
        --| Symbol.scan_id --| $$ "," -- parse_clause pool
        -- parse_tstp_annotations --| $$ ")" --| $$ "."
       >> finish_tstp_inference_line)
 
 (**** PARSING OF SPASS OUTPUT ****)
 
 (* SPASS returns clause references of the form "x.y". We ignore "y", whose role
    is not clear anyway. *)
-val parse_dot_name = parse_integer --| $$ "." --| parse_integer
+val parse_dot_name = scan_integer --| $$ "." --| scan_integer
 
 val parse_spass_annotations =
   Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name
                                          --| Scan.option ($$ ","))) []
 

 
 (* Syntax: <num>[0:<inference><annotations>]
    <cnf_formulas> || <cnf_formulas> -> <cnf_formulas>. *)
 fun finish_spass_line ((num, deps), us) = Inference (num, us, deps)
 fun parse_spass_line pool =
-  parse_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
+  scan_integer --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
   -- parse_spass_annotations --| $$ "]" -- parse_horn_clause pool --| $$ "."
   >> finish_spass_line
 
 fun parse_line pool = parse_tstp_line pool || parse_spass_line pool
 fun parse_lines pool = Scan.repeat1 (parse_line pool)

    number (108) is extracted.
    SPASS: Lines have the form "108[0:Inp] ...", where the first number (108) is
    extracted. *)
 fun extract_formula_numbers_in_atp_proof atp_proof =
   let
-    val tokens_of = String.tokens (not o is_ident_char)
+    val tokens_of = String.tokens (not o Char.isAlphaNum)
     fun extract_num ("fof" :: num :: "axiom" :: _) = Int.fromString num
       | extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num
       | extract_num _ = NONE
   in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end