src/HOL/Tools/ATP/recon_parse.ML

Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
Will now signal if ATP has run out of time and then kill the watcher.

(*  ID:         $Id$
    Author:     Claire Quigley
    Copyright   2004  University of Cambridge
*)

(*use "Translate_Proof";*)
(* Parsing functions *)

(* Auxiliary functions *)

structure Recon_Parse =
struct

exception ASSERTION of string;

exception NOPARSE_WORD
exception NOPARSE_NUM
fun to_upper s = String.translate (Char.toString o Char.toUpper) s;

fun string2int s =
  let
    val io = Int.fromString s
  in
    case io of
      (SOME i) => i
      | _ => raise ASSERTION "string -> int failed"
  end

(* 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
      in
        ((result1, result2), rest2)
      end;

fun many parser input =
      let   (* Tree * token list*)
        val (result, next) = parser input
        val (results, rest) = many parser next
      in
        ((result::results), rest)
      end
      handle Noparse => ([], input)
|            NOPARSE_WORD => ([], input)
|            NOPARSE_NUM  => ([], input);



fun (parser >> treatment) input =
      let
        val (result, rest) = parser input
      in
        (treatment result, rest)
      end;

fun (parser1 || parser2) input = parser1 input
handle Noparse => parser2 input;

infixr 8 ++; infixr 7 >>; infixr 6 ||;

fun some p [] = raise Noparse
  | some p (h::t) = if p h then (h, t) else raise Noparse;

fun a tok = some (fn item => item = tok);

fun finished input = if input = [] then (0, input) else raise Noparse;





  (* Parsing the output from gandalf *)
datatype token = Word of string
               | Number of int
               | Other of string


      exception NOCUT
      fun is_prefix [] l = true
        | is_prefix (h::t) [] = false
        | is_prefix (h::t) (h'::t') = (h = h') andalso is_prefix t t'
      fun remove_prefix [] l = l
        | remove_prefix (h::t) [] = raise (ASSERTION "can't remove prefix")
        | remove_prefix (h::t) (h'::t') = remove_prefix t t'
      fun ccut t [] = raise NOCUT
        | ccut t s =
            if is_prefix t s then ([], remove_prefix t s) else
              let val (a, b) = ccut t (tl s) in ((hd s)::a, b) end
      fun cut t s =
        let
          val t' = explode t
          val s' = explode s
          val (a, b) = ccut t' s'
        in
          (implode a, implode b)
        end
    
      fun cut_exists t s
          = let val (a, b) = cut t s in true end handle NOCUT => false

      fun cut_before t s = let val (a, b) = cut t s in (a, t ^ b) end
      fun cut_after t s = let val (a, b) = cut t s in (a ^ t, b) end
    

    fun kill_lines 0 = Library.I
      | kill_lines n = kill_lines (n - 1) o snd o cut_after "\n";

    (*fun extract_proof s
      = if cut_exists "EMPTY CLAUSE DERIVED" s then
          (kill_lines 6
           o snd o cut_after "EMPTY CLAUSE DERIVED"
           o fst o cut_after "contradiction.\n") s
        else
          raise (GandalfError "Couldn't find a proof.")
*)

val proofstring =
"0:00:00.00 for the reduction.\
\\
\Here is a proof with depth 3, length 7 :\
\1[0:Inp] ||  -> P(xa)*.\
\2[0:Inp] ||  -> Q(xb)*.\
\3[0:Inp] || R(U)* -> .\
\4[0:Inp] || Q(U) P(V) -> R(x(V,U))*.\
\9[0:Res:4.2,3.0] || Q(U)*+ P(V)* -> .\
\11[0:Res:2.0,9.0] || P(U)* -> .\
\12[0:Res:1.0,11.0] ||  -> .\
\Formulae used in the proof :\
\\
\--------------------------SPASS-STOP------------------------------"

fun extract_proof s
      = if cut_exists "Here is a proof with" s then
          (kill_lines 0
           o snd o cut_after ":"
           o snd o cut_after "Here is a proof with"
           o fst o cut_after " ||  -> .") s
        else if cut_exists "%================== Proof: ======================" s then
          (kill_lines 0
           o snd o cut_after "%================== Proof: ======================"
           o fst o cut_before "==============  End of proof. ==================") s
        else
          raise SPASSError "Couldn't find a proof."

(*fun extract_proof s
      = if cut_exists "Here is a proof with" s then
          (kill_lines 0
           o snd o cut_after ":"
           o snd o cut_after "Here is a proof with"
           o fst o cut_after " ||  -> .") s
        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")
      fun digit s = ("0" <= s) andalso (s <= "9")
      fun letter s = lower_letter s orelse upper_letter s
      fun alpha s = letter s orelse (s = "_")
      fun alphanum s = alpha s orelse digit s
      fun space s = (s = " ") orelse (s = "\n") orelse (s = "\t")
      (* FIX this is stopping it picking up numbers *)
      val word = (some alpha ++ several alphanum) >> (Word o collect)
      val number =
            (some digit ++ several digit) >> (Number o string2int o collect)
      val other = some (K true) >> Other
      
      val token = (word || number || other) ++ several space >> fst
      val tokens = (several space ++ many token) >> snd
      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 first = hd rest
				
			          in
				    if (first = (Other "*") ) 
				    then 
					
					 linenums rest ((num_int (hd (tl rest)))::nums)
				     else
					  linenums rest ((num_int first)::nums)
			         end
                                end


(* This relies on a Vampire proof line starting "% Number" or "% * Number"*)
(* Check this is right *)

fun get_linenums proofstr = let (*val s = extract_proof proofstr*)
                                val tokens = #1(lex proofstr)
	                 
	                    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)
        | word _ = raise NOPARSE_WORD

      fun other_char ( (Other p)::rest) = (p, rest)
      | other_char _ =raise NOPARSE_WORD
     
      val number_list =
        (number ++ many number)
        >> (fn (a, b) => (a::b))
     
      val term_num =
        (number ++ (a (Other ".")) ++ number) >> (fn (a, (_, c)) => (a, c))


      val term_num_list = (term_num ++ many (a (Other ",") ++ term_num >> snd)
			   >> (fn (a, b) => (a::b)))

      val axiom = (a (Word "Inp"))
            >> (fn (_) => Axiom)
      
      
      val binary = (a (Word "Res")) ++ (a (Other ":"))
                   ++ term_num ++ (a (Other ","))
                   ++ term_num
            >> (fn (_, (_, (c, (_, e)))) => Binary (c, e))
      


      val factor = (a (Word "Fac")) ++ (a (Other ":")) 
                    ++ term_num ++ (a (Other ",")) 
                    ++ term_num
            >> (fn (_, (_, (c, (_, e)))) =>  Factor ((fst c), (snd c),(snd e)))
     
      val para  = (a (Word "SPm")) ++ (a (Other ":"))
                   ++ term_num ++ (a (Other ","))
                   ++ term_num
            >> (fn (_, (_, (c, (_, e)))) => Para (c, e))
      
      val super_l  = (a (Word "SpL")) ++ (a (Other ":"))
                   ++ term_num ++ (a (Other ","))
                   ++ term_num
            >> (fn (_, (_, (c, (_, e)))) => Super_l (c, e))


      val super_r  = (a (Word "SpR")) ++ (a (Other ":"))
                   ++ term_num ++ (a (Other ","))
                   ++ term_num
            >> (fn (_, (_, (c, (_, e)))) => Super_r (c, e))


      val aed = (a (Word "AED")) ++ (a (Other ":")) ++ term_num
                 >> (fn (_, (_, c)) => Obvious ((fst c),(snd c)))

      val rewrite = (a (Word "Rew")) ++ (a (Other ":")) 
                    ++ term_num_list
            >> (fn (_, (_, (c))) =>  Rewrite (c))


      val mrr = (a (Word "MRR")) ++ (a (Other ":"))
                   ++ term_num ++ (a (Other ","))
                   ++ term_num
            >> (fn (_, (_, (c, (_, e)))) => MRR (c, e))

      val ssi = (a (Word "SSi")) ++ (a (Other ":"))
                   ++ term_num ++ (a (Other ","))
                   ++ term_num
            >> (fn (_, (_, (c, (_, e)))) => SortSimp (c, e))

    val unc = (a (Word "UnC")) ++ (a (Other ":"))
                   ++ term_num ++ (a (Other ","))
                   ++ term_num
            >> (fn (_, (_, (c, (_, e)))) => UnitConf (c, e))



      val obv = (a (Word "Obv")) ++ (a (Other ":")) ++ term_num
                 >> (fn (_, (_, c)) => Obvious ((fst c),(snd c)))

      val eqres = (a (Word "EqR")) ++ (a (Other ":")) ++ term_num
                 >> (fn (_, (_, c)) => EqualRes ((fst c),(snd c)))
   
      val con = (a (Word "Con")) ++ (a (Other ":")) ++ term_num
                 >> (fn (_, (_, c)) => Condense ((fst c),(snd c)))

(*
      val hyper = a (Word "hyper")
                  ++ many ((a (Other ",") ++ number) >> snd)
                  >> (Hyper o snd)
*)
     (* val method = axiom ||binary || factor || para || hyper*)

      val method = axiom || binary || factor || para ||super_l || super_r || rewrite || mrr || obv || aed || ssi || unc|| con

      val binary_s = a (Word "binary_s") ++ a (Other ",") ++ term_num
            >> (fn (_, (_, a)) => Binary_s a)
      val factor_s = a (Word "factor_s")
            >> (fn _ => Factor_s ())
      val demod_s = a (Word "demod")
                    ++ (many ((a (Other ",") ++ term_num) >> snd))
            >> (fn (_, a) => Demod_s a)

      val hyper_s = a (Word "hyper_s")
                    ++ many ((a (Other ",") ++ number) >> snd)
                    >> (Hyper_s o snd)
      val simp_method = binary_s || factor_s || demod_s || hyper_s
      val simp = a (Other ",") ++ simp_method >> snd
      val simps = many simp
 

      val justification =
           a (Other "[") ++number ++ a (Other ":") ++ method ++ a (Other "]")
                 >> (fn (_,(_, (_,(b, _)))) => b)

     
exception NOTERM


fun implode_with_space [] = implode []
|   implode_with_space [x] = implode [x]
|   implode_with_space (x::[y]) = x^" "^y
|   implode_with_space (x::xs) =  (x^" "^(implode_with_space xs))

(* FIX - should change the stars and pluses to many rather than explicit patterns *)

(* FIX - add the other things later *)
fun remove_typeinfo x  =  if (String.isPrefix "v_" x )
                            then 
                                 (String.substring (x,2, ((size x) - 2)))
                            else if (String.isPrefix "V_" x )
                                 then 
                                      (String.substring (x,2, ((size x) - 2)))
                                 else if (String.isPrefix "typ_" x )
                                      then 
                                          ""
                                      else if (String.isPrefix "Typ_" x )
                                           then 
                                                ""
                                           else  if (String.isPrefix "tconst_" x )
                                                 then 
                                                      ""
                                                 else  if (String.isPrefix "const_" x )
                                                       then 
                                                            (String.substring  (x,6, ((size x) - 6)))
                                                       else
                                                           x
                                               

fun term input = (  ntermlist ++ a (Other "-") ++ a (Other ">") ++ ptermlist >>(fn (a,(_,(_,b))) =>  (a@b))
                  ) input

(* pterms are terms from the rhs of the -> in the spass proof.  *)
(* they should have a "~" in front of them so that they match with *)
(* positive terms in the meta-clause *)
(* nterm are terms from the lhs of the spass proof, and shouldn't *)
(* "~"s added  word ++ a (Other "(") ++ arglist ++ a (Other ")") >> (fn (a,(_,(b,_ ))) =>  (a^" "^b)) *)

and  pterm input = (
           peqterm >> (fn (a) => a)
        
         || word ++ a (Other "(") ++ arglist ++  a (Other ")") ++ a (Other "*")++ a (Other "*") ++ a (Other "+")
           >> (fn (a, (_,(b, (_,(_,_))))) =>  ("~"^" "^(remove_typeinfo a)^" "^b))
         
        || word ++ a (Other "(") ++ arglist ++  a (Other ")") ++ a (Other "*") ++ a (Other "+")
           >> (fn ( a, (_,(b, (_,(_,_))))) =>  ("~"^" "^(remove_typeinfo a)^" "^b))
        
        || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*")
           >> (fn ( a, (_,(b, (_,(_,_))))) =>  ("~"^" "^(remove_typeinfo a)^" "^b))
        
	|| word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*")
           >> (fn (a, (_,(b, (_,_)))) =>  ("~"^" "^(remove_typeinfo a)^" "^b))

        || word ++ a (Other "(") ++  arglist ++ a (Other ")") 
           >> (fn ( a, (_,(b,_ ))) => ("~"^" "^(remove_typeinfo a)^" "^b))

        || word ++ a (Other "*") >> (fn (w,b) => "~"^" "^(remove_typeinfo w))

        || word                  >> (fn w => "~"^" "^(remove_typeinfo w))) input

and  nterm input =
    
       (  
           neqterm >> (fn (a) => a)

        || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
           >> (fn ( a, (_,(b, (_,(_,_))))) =>  ((remove_typeinfo a)^" "^b))

        || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "+")
           >> (fn ( a, (_,(b, (_,(_,_))))) =>  ((remove_typeinfo a)^" "^b))
        
        || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*")
           >> (fn ( a, (_,(b, (_,(_,_))))) =>  ((remove_typeinfo a)^" "^b))
        
	|| word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*")
           >> (fn ( a, (_,(b, (_,_)))) =>  ((remove_typeinfo a)^" "^b))

        || word ++ a (Other "(") ++ arglist ++ a (Other ")") 
           >> (fn (a, (_,(b,_ ))) => ((remove_typeinfo a)^" "^b))

        || word ++ a (Other "*") >> (fn (w,b) =>  (remove_typeinfo w)) 
        || word                  >> (fn w =>  (remove_typeinfo w)) 
         ) input 


and peqterm input =(
 
         a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
         ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
            >> (fn (_,(_,(a,(_,(b,(_,(_,(_,_)))))))) => (a^" ~= "^b))

      || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
          ++ a (Other "*") ++ a (Other "+")
            >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" ~= "^b))

      || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
         ++ a (Other "*") ++ a (Other "*")
            >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" ~= "^b))

      || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
         ++ a (Other "*") 
            >> (fn (_,(_,(a,(_,(b,(_,_)))))) => (a^" ~= "^b))


       ||a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
            >> (fn (_,(_,(a,(_,(b,_))))) => (a^" ~= "^b))) input



and neqterm input =(
 
         a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
         ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
            >> (fn (_,(_,(a,(_,(b,(_,(_,(_,_)))))))) => (a^" = "^b))

      || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
          ++ a (Other "*") ++ a (Other "+")
            >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" = "^b))

      || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
         ++ a (Other "*") ++ a (Other "*")
            >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" = "^b))

      || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
         ++ a (Other "*") 
            >> (fn (_,(_,(a,(_,(b,(_,_)))))) => (a^" = "^b))


       ||a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
            >> (fn (_,(_,(a,(_,(b,_))))) => (a^" = "^b))) input



and ptermlist input = (many  pterm
                      >> (fn (a) => (a))) input

and ntermlist input = (many  nterm
                      >> (fn (a) => (a))) input

(*and arglist input = (    nterm >> (fn (a) => (a))
                     ||  nterm ++ many (a (Other ",") ++ nterm >> snd)
                      >> (fn (a, b) => (a^" "^(implode_with_space b)))) input*)

and arglist input = (   nterm ++ many (a (Other ",") ++ nterm >> snd)
                      >> (fn (a, b) => (a^" "^(implode_with_space b))) 
                      ||    nterm >> (fn (a) => (a)))input

 val clause =  term



 (*val line = number ++ justification ++ a (Other "|") ++ 
            a (Other "|") ++ clause ++ a (Other ".")
          >> (fn (a, (z, (_,( _, (c, _))))) => (a, z, c))*)


(* not entirely sure nterm is right here, but I don't think you get negative things before the ||s *)
 val line = number ++ justification ++ many( nterm) ++ a (Other "|") ++ 
            a (Other "|") ++ clause ++ a (Other ".")
          >> (fn (a, (z, (w, (_,( _, (c, _)))))) => (a, z,(w@ c)))
       


 val lines = many line
 val alllines = (lines ++ finished) >> fst
    
 val parse = fst o alllines
 val s = proofstring;
 
 


fun dropUntilNot ch []   = ( [])
 |   dropUntilNot ch (x::xs)  = if  not(x = ch )
                                then
                                     (x::xs)
                                else
                                     dropUntilNot ch xs


fun remove_spaces str  []  = str
|   remove_spaces str (x::[]) = if x = " " 
                                then 
                                    str 
                                else 
                                    (str^x)
|   remove_spaces str (x::xs) = 
      let val (first, rest) = ReconOrderClauses.takeUntil " " (x::xs) []
	  val (next) = dropUntilNot " " rest 
      in 
	  if next = []
	  then 
	       (str^(implode first)) 
	  else remove_spaces  (str^(implode first)^" ") next 
      end


fun remove_space_strs clsstrs = map (remove_spaces "") (map explode clsstrs)


fun all_spaces xs = List.filter  (not_equal " " ) xs

fun just_change_space []  = []
|   just_change_space ((clausenum, step, strs)::xs) =
      let val newstrs = remove_space_strs strs
      in
	 if (all_spaces newstrs = [] ) (* all type_info *)
	 then    
	    (clausenum, step, newstrs)::(just_change_space xs)
	 else 
	     (clausenum, step, newstrs)::(just_change_space xs) 
      end;

fun change_space []  = []
|   change_space ((clausenum, step, strs)::xs) = 
      let val newstrs = remove_space_strs strs
      in
	 if (all_spaces newstrs = [] ) (* all type_info *)
	 then    
	    (clausenum, step, T_info, newstrs)::(change_space xs)
	 else 
	     (clausenum, step, P_info, newstrs)::(change_space xs) 
      end

end;