src/HOL/Tools/ATP/recon_parse.ML

 
 (* Parser combinators *)
 
 exception Noparse;
 exception SPASSError of string;
+exception VampError of string;
+
 
 fun (parser1 ++ parser2) input =
       let
         val (result1, rest1) = parser1 input
         val (result2, rest2) = parser2 rest1

         else
           raise SPASSError "Couldn't find a proof."
 *)
 
 
+
+
+
 fun several p = many (some p)
       fun collect (h, t) = h ^ (Utils.itlist (fn s1 => fn s2 => s1 ^ s2) t "")
   
       fun lower_letter s = ("a" <= s) andalso (s <= "z")
       fun upper_letter s = ("A" <= s) andalso (s <= "Z")

       val alltokens = (tokens ++ finished) >> fst
     
      (* val lex = fst ( alltokens ( (map str)  explode))*)
      fun lex s =  alltokens  (explode s)
 
+
+(*********************************************************)
+(*  Temporary code to "parse" Vampire proofs             *)
+(*********************************************************)
+
+fun num_int (Number n) = n
+|   num_int _ = raise VampError "Not a number"
+
+ fun takeUntil ch [] res  = (res, [])
+ |   takeUntil ch (x::xs) res = if   x = ch 
+                                then
+                                     (res, xs)
+                                else
+                                     takeUntil ch xs (res@[x])
+       
+fun linenums [] nums = nums
+|   linenums (x::xs) nums = let val (fst, rest ) = takeUntil (Other "%") (x::xs) []
+                                in 
+				  if rest = [] 
+				  then 
+				      nums
+				  else
+			          let val num = hd rest
+                                      val int_of = num_int num
+	
+			          in
+				     linenums rest (int_of::nums)
+			         end
+                                end
+
+fun get_linenums proofstr = let val s = extract_proof proofstr
+                                val tokens = #1(lex s)
+	                 
+	                    in
+		                rev (linenums tokens [])
+		            end
+
+(************************************************************)
+(************************************************************)
+
+
+(**************************************************)
+(* Code to parse SPASS proofs                     *)
+(**************************************************)
+
 datatype Tree = Leaf of string
                 | Branch of Tree * Tree
-
-
 
    
       fun number ((Number n)::rest) = (n, rest)
         | number _ = raise NOPARSE_NUM
       fun word ((Word w)::rest) = (w, rest)