src/HOL/Tools/ATP/recon_parse.ML
author paulson
Thu Apr 21 15:05:24 2005 +0200 (2005-04-21)
changeset 15789 4cb16144c81b
parent 15688 adf0ba6353f3
child 15919 b30a35432f5a
permissions -rw-r--r--
added hearder lines and deleted some redundant material
     1 (*  ID:         $Id$
     2     Author:     Claire Quigley
     3     Copyright   2004  University of Cambridge
     4 *)
     5 
     6 (*use "Translate_Proof";*)
     7 (* Parsing functions *)
     8 
     9 (* Auxiliary functions *)
    10 
    11 structure Recon_Parse =
    12 struct
    13 
    14 exception ASSERTION of string;
    15 
    16 exception NOPARSE_WORD
    17 exception NOPARSE_NUM
    18 fun to_upper s = String.translate (Char.toString o Char.toUpper) s;
    19 
    20 fun string2int s =
    21   let
    22     val io = Int.fromString s
    23   in
    24     case io of
    25       (SOME i) => i
    26       | _ => raise ASSERTION "string -> int failed"
    27   end
    28 
    29 (* Parser combinators *)
    30 
    31 exception Noparse;
    32 exception SPASSError of string;
    33 
    34 fun (parser1 ++ parser2) input =
    35       let
    36         val (result1, rest1) = parser1 input
    37         val (result2, rest2) = parser2 rest1
    38       in
    39         ((result1, result2), rest2)
    40       end;
    41 
    42 fun many parser input =
    43       let   (* Tree * token list*)
    44         val (result, next) = parser input
    45         val (results, rest) = many parser next
    46       in
    47         ((result::results), rest)
    48       end
    49       handle Noparse => ([], input)
    50 |            NOPARSE_WORD => ([], input)
    51 |            NOPARSE_NUM  => ([], input);
    52 
    53 
    54 
    55 fun (parser >> treatment) input =
    56       let
    57         val (result, rest) = parser input
    58       in
    59         (treatment result, rest)
    60       end;
    61 
    62 fun (parser1 || parser2) input = parser1 input
    63 handle Noparse => parser2 input;
    64 
    65 infixr 8 ++; infixr 7 >>; infixr 6 ||;
    66 
    67 fun some p [] = raise Noparse
    68   | some p (h::t) = if p h then (h, t) else raise Noparse;
    69 
    70 fun a tok = some (fn item => item = tok);
    71 
    72 fun finished input = if input = [] then (0, input) else raise Noparse;
    73 
    74 
    75 
    76 
    77 
    78   (* Parsing the output from gandalf *)
    79 datatype token = Word of string
    80                | Number of int
    81                | Other of string
    82 
    83 
    84       exception NOCUT
    85       fun is_prefix [] l = true
    86         | is_prefix (h::t) [] = false
    87         | is_prefix (h::t) (h'::t') = (h = h') andalso is_prefix t t'
    88       fun remove_prefix [] l = l
    89         | remove_prefix (h::t) [] = raise (ASSERTION "can't remove prefix")
    90         | remove_prefix (h::t) (h'::t') = remove_prefix t t'
    91       fun ccut t [] = raise NOCUT
    92         | ccut t s =
    93             if is_prefix t s then ([], remove_prefix t s) else
    94               let val (a, b) = ccut t (tl s) in ((hd s)::a, b) end
    95       fun cut t s =
    96         let
    97           val t' = explode t
    98           val s' = explode s
    99           val (a, b) = ccut t' s'
   100         in
   101           (implode a, implode b)
   102         end
   103     
   104       fun cut_exists t s
   105           = let val (a, b) = cut t s in true end handle NOCUT => false
   106 
   107       fun cut_before t s = let val (a, b) = cut t s in (a, t ^ b) end
   108       fun cut_after t s = let val (a, b) = cut t s in (a ^ t, b) end
   109     
   110 
   111     fun kill_lines 0 = Library.I
   112       | kill_lines n = kill_lines (n - 1) o snd o cut_after "\n";
   113 
   114     (*fun extract_proof s
   115       = if cut_exists "EMPTY CLAUSE DERIVED" s then
   116           (kill_lines 6
   117            o snd o cut_after "EMPTY CLAUSE DERIVED"
   118            o fst o cut_after "contradiction.\n") s
   119         else
   120           raise (GandalfError "Couldn't find a proof.")
   121 *)
   122 
   123 val proofstring =
   124 "0:00:00.00 for the reduction.\
   125 \\
   126 \Here is a proof with depth 3, length 7 :\
   127 \1[0:Inp] ||  -> P(xa)*.\
   128 \2[0:Inp] ||  -> Q(xb)*.\
   129 \3[0:Inp] || R(U)* -> .\
   130 \4[0:Inp] || Q(U) P(V) -> R(x(V,U))*.\
   131 \9[0:Res:4.2,3.0] || Q(U)*+ P(V)* -> .\
   132 \11[0:Res:2.0,9.0] || P(U)* -> .\
   133 \12[0:Res:1.0,11.0] ||  -> .\
   134 \Formulae used in the proof :\
   135 \\
   136 \--------------------------SPASS-STOP------------------------------"
   137 
   138 
   139 fun extract_proof s
   140       = if cut_exists "Here is a proof with" s then
   141           (kill_lines 0
   142            o snd o cut_after ":"
   143            o snd o cut_after "Here is a proof with"
   144            o fst o cut_after " ||  -> .") s
   145         else
   146           raise SPASSError "Couldn't find a proof."
   147 
   148 
   149 
   150 fun several p = many (some p)
   151       fun collect (h, t) = h ^ (Utils.itlist (fn s1 => fn s2 => s1 ^ s2) t "")
   152   
   153       fun lower_letter s = ("a" <= s) andalso (s <= "z")
   154       fun upper_letter s = ("A" <= s) andalso (s <= "Z")
   155       fun digit s = ("0" <= s) andalso (s <= "9")
   156       fun letter s = lower_letter s orelse upper_letter s
   157       fun alpha s = letter s orelse (s = "_")
   158       fun alphanum s = alpha s orelse digit s
   159       fun space s = (s = " ") orelse (s = "\n") orelse (s = "\t")
   160       (* FIX this is stopping it picking up numbers *)
   161       val word = (some alpha ++ several alphanum) >> (Word o collect)
   162       val number =
   163             (some digit ++ several digit) >> (Number o string2int o collect)
   164       val other = some (K true) >> Other
   165       
   166       val token = (word || number || other) ++ several space >> fst
   167       val tokens = (several space ++ many token) >> snd
   168       val alltokens = (tokens ++ finished) >> fst
   169     
   170      (* val lex = fst ( alltokens ( (map str)  explode))*)
   171      fun lex s =  alltokens  (explode s)
   172 
   173 datatype Tree = Leaf of string
   174                 | Branch of Tree * Tree
   175 
   176 
   177 
   178    
   179       fun number ((Number n)::rest) = (n, rest)
   180         | number _ = raise NOPARSE_NUM
   181       fun word ((Word w)::rest) = (w, rest)
   182         | word _ = raise NOPARSE_WORD
   183 
   184       fun other_char ( (Other p)::rest) = (p, rest)
   185       | other_char _ =raise NOPARSE_WORD
   186      
   187       val number_list =
   188         (number ++ many number)
   189         >> (fn (a, b) => (a::b))
   190      
   191       val term_num =
   192         (number ++ (a (Other ".")) ++ number) >> (fn (a, (_, c)) => (a, c))
   193 
   194       val axiom = (a (Word "Inp"))
   195             >> (fn (_) => Axiom)
   196       
   197       
   198       val binary = (a (Word "Res")) ++ (a (Other ":"))
   199                    ++ term_num ++ (a (Other ","))
   200                    ++ term_num
   201             >> (fn (_, (_, (c, (_, e)))) => Binary (c, e))
   202       
   203 
   204 
   205       val factor = (a (Word "Fac")) ++ (a (Other ":")) 
   206                     ++ term_num ++ (a (Other ",")) 
   207                     ++ term_num
   208             >> (fn (_, (_, (c, (_, e)))) =>  Factor ((fst c), (snd c),(snd e)))
   209      
   210       val para  = (a (Word "SPm")) ++ (a (Other ":"))
   211                    ++ term_num ++ (a (Other ","))
   212                    ++ term_num
   213             >> (fn (_, (_, (c, (_, e)))) => Para (c, e))
   214       
   215       val rewrite = (a (Word "Rew")) ++ (a (Other ":")) 
   216                     ++ term_num ++ (a (Other ",")) 
   217                     ++ term_num
   218             >> (fn (_, (_, (c, (_, e)))) =>  Rewrite (c, e))
   219 
   220 
   221       val mrr = (a (Word "MRR")) ++ (a (Other ":"))
   222                    ++ term_num ++ (a (Other ","))
   223                    ++ term_num
   224             >> (fn (_, (_, (c, (_, e)))) => MRR (c, e))
   225 
   226 
   227       val obv = (a (Word "Obv")) ++ (a (Other ":")) ++ term_num
   228                  >> (fn (_, (_, c)) => Obvious ((fst c),(snd c)))
   229      
   230 (*
   231       val hyper = a (Word "hyper")
   232                   ++ many ((a (Other ",") ++ number) >> snd)
   233                   >> (Hyper o snd)
   234 *)
   235      (* val method = axiom ||binary || factor || para || hyper*)
   236 
   237       val method = axiom || binary || factor || para || rewrite || mrr || obv
   238       val binary_s = a (Word "binary_s") ++ a (Other ",") ++ term_num
   239             >> (fn (_, (_, a)) => Binary_s a)
   240       val factor_s = a (Word "factor_s")
   241             >> (fn _ => Factor_s ())
   242       val demod_s = a (Word "demod")
   243                     ++ (many ((a (Other ",") ++ term_num) >> snd))
   244             >> (fn (_, a) => Demod_s a)
   245 
   246       val hyper_s = a (Word "hyper_s")
   247                     ++ many ((a (Other ",") ++ number) >> snd)
   248                     >> (Hyper_s o snd)
   249       val simp_method = binary_s || factor_s || demod_s || hyper_s
   250       val simp = a (Other ",") ++ simp_method >> snd
   251       val simps = many simp
   252  
   253 
   254       val justification =
   255            a (Other "[") ++number ++ a (Other ":") ++ method ++ a (Other "]")
   256                  >> (fn (_,(_, (_,(b, _)))) => b)
   257 
   258      
   259 exception NOTERM
   260 
   261 
   262 fun implode_with_space [] = implode []
   263 |   implode_with_space [x] = implode [x]
   264 |   implode_with_space (x::[y]) = x^" "^y
   265 |   implode_with_space (x::xs) =  (x^" "^(implode_with_space xs))
   266 
   267 (* FIX - should change the stars and pluses to many rather than explicit patterns *)
   268 
   269 (* FIX - add the other things later *)
   270 fun remove_typeinfo x  =  if (String.isPrefix "v_" x )
   271                             then 
   272                                  (String.substring (x,2, ((size x) - 2)))
   273                             else if (String.isPrefix "V_" x )
   274                                  then 
   275                                       (String.substring (x,2, ((size x) - 2)))
   276                                  else if (String.isPrefix "typ_" x )
   277                                       then 
   278                                           ""
   279                                       else if (String.isPrefix "Typ_" x )
   280                                            then 
   281                                                 ""
   282                                            else  if (String.isPrefix "tconst_" x )
   283                                                  then 
   284                                                       ""
   285                                                  else  if (String.isPrefix "const_" x )
   286                                                        then 
   287                                                             (String.substring  (x,6, ((size x) - 6)))
   288                                                        else
   289                                                            x
   290                                                
   291 
   292 fun term input = (  ntermlist ++ a (Other "-") ++ a (Other ">") ++ ptermlist >>(fn (a,(_,(_,b))) =>  (a@b))
   293                   ) input
   294 
   295 (* pterms are terms from the rhs of the -> in the spass proof.  *)
   296 (* they should have a "~" in front of them so that they match with *)
   297 (* positive terms in the meta-clause *)
   298 (* nterm are terms from the lhs of the spass proof, and shouldn't *)
   299 (* "~"s added  word ++ a (Other "(") ++ arglist ++ a (Other ")") >> (fn (a,(_,(b,_ ))) =>  (a^" "^b)) *)
   300 
   301 and  pterm input = (
   302            peqterm >> (fn (a) => a)
   303         
   304          || word ++ a (Other "(") ++ arglist ++  a (Other ")") ++ a (Other "*")++ a (Other "*") ++ a (Other "+")
   305            >> (fn (a, (_,(b, (_,(_,_))))) =>  ("~"^" "^(remove_typeinfo a)^" "^b))
   306          
   307         || word ++ a (Other "(") ++ arglist ++  a (Other ")") ++ a (Other "*") ++ a (Other "+")
   308            >> (fn ( a, (_,(b, (_,(_,_))))) =>  ("~"^" "^(remove_typeinfo a)^" "^b))
   309         
   310         || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*")
   311            >> (fn ( a, (_,(b, (_,(_,_))))) =>  ("~"^" "^(remove_typeinfo a)^" "^b))
   312         
   313 	|| word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*")
   314            >> (fn (a, (_,(b, (_,_)))) =>  ("~"^" "^(remove_typeinfo a)^" "^b))
   315 
   316         || word ++ a (Other "(") ++  arglist ++ a (Other ")") 
   317            >> (fn ( a, (_,(b,_ ))) => ("~"^" "^(remove_typeinfo a)^" "^b))
   318 
   319         || word >> (fn w => "~"^" "^(remove_typeinfo w))) input
   320 
   321 and  nterm input =
   322     
   323        (  
   324            neqterm >> (fn (a) => a)
   325 
   326         || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
   327            >> (fn ( a, (_,(b, (_,(_,_))))) =>  ((remove_typeinfo a)^" "^b))
   328 
   329         || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "+")
   330            >> (fn ( a, (_,(b, (_,(_,_))))) =>  ((remove_typeinfo a)^" "^b))
   331         
   332         || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*")
   333            >> (fn ( a, (_,(b, (_,(_,_))))) =>  ((remove_typeinfo a)^" "^b))
   334         
   335 	|| word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*")
   336            >> (fn ( a, (_,(b, (_,_)))) =>  ((remove_typeinfo a)^" "^b))
   337 
   338         || word ++ a (Other "(") ++ arglist ++ a (Other ")") 
   339            >> (fn (a, (_,(b,_ ))) => ((remove_typeinfo a)^" "^b))
   340 
   341         || word >> (fn w =>  (remove_typeinfo w)) ) input 
   342 
   343 
   344 and peqterm input =(
   345  
   346          a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   347          ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
   348             >> (fn (_,(_,(a,(_,(b,(_,(_,(_,_)))))))) => (a^" ~= "^b))
   349 
   350       || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   351           ++ a (Other "*") ++ a (Other "+")
   352             >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" ~= "^b))
   353 
   354       || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   355          ++ a (Other "*") ++ a (Other "*")
   356             >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" ~= "^b))
   357 
   358       || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   359          ++ a (Other "*") 
   360             >> (fn (_,(_,(a,(_,(b,(_,_)))))) => (a^" ~= "^b))
   361 
   362 
   363        ||a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   364             >> (fn (_,(_,(a,(_,(b,_))))) => (a^" ~= "^b))) input
   365 
   366 
   367 
   368 and neqterm input =(
   369  
   370          a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   371          ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
   372             >> (fn (_,(_,(a,(_,(b,(_,(_,(_,_)))))))) => (a^" = "^b))
   373 
   374       || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   375           ++ a (Other "*") ++ a (Other "+")
   376             >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" = "^b))
   377 
   378       || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   379          ++ a (Other "*") ++ a (Other "*")
   380             >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" = "^b))
   381 
   382       || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   383          ++ a (Other "*") 
   384             >> (fn (_,(_,(a,(_,(b,(_,_)))))) => (a^" = "^b))
   385 
   386 
   387        ||a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   388             >> (fn (_,(_,(a,(_,(b,_))))) => (a^" = "^b))) input
   389 
   390 
   391 
   392 and ptermlist input = (many  pterm
   393                       >> (fn (a) => (a))) input
   394 
   395 and ntermlist input = (many  nterm
   396                       >> (fn (a) => (a))) input
   397 
   398 (*and arglist input = (    nterm >> (fn (a) => (a))
   399                      ||  nterm ++ many (a (Other ",") ++ nterm >> snd)
   400                       >> (fn (a, b) => (a^" "^(implode_with_space b)))) input*)
   401 
   402 and arglist input = (   nterm ++ many (a (Other ",") ++ nterm >> snd)
   403                       >> (fn (a, b) => (a^" "^(implode_with_space b))) 
   404                       ||    nterm >> (fn (a) => (a)))input
   405 
   406  val clause =  term
   407 
   408  val line = number ++ justification ++ a (Other "|") ++ 
   409             a (Other "|") ++ clause ++ a (Other ".")
   410           >> (fn (a, (z, (_,( _, (c, _))))) => (a, z, c))
   411     
   412  val lines = many line
   413  val alllines = (lines ++ finished) >> fst
   414     
   415  val parse = fst o alllines
   416  val s = proofstring;
   417  
   418  
   419 
   420 
   421 fun dropUntilNot ch []   = ( [])
   422  |   dropUntilNot ch (x::xs)  = if  not(x = ch )
   423                                 then
   424                                      (x::xs)
   425                                 else
   426                                      dropUntilNot ch xs
   427 
   428 
   429 
   430 
   431 
   432 fun remove_spaces str  []  = str
   433 |   remove_spaces str (x::[]) = if x = " " 
   434                                 then 
   435                                     str 
   436                                 else 
   437                                     (str^x)
   438 |   remove_spaces str (x::xs) = let val (first, rest) = takeUntil " " (x::xs) []
   439                                     val (next) = dropUntilNot " " rest 
   440                                 in 
   441                                     if next = []
   442                                     then 
   443                                          (str^(implode first)) 
   444                                     else remove_spaces  (str^(implode first)^" ") next 
   445                                 end
   446 
   447 
   448 fun remove_space_strs clsstrs = map (remove_spaces "") (map explode clsstrs)
   449 
   450 
   451 fun all_spaces xs = List.filter  (not_equal " " ) xs
   452 
   453 fun just_change_space []  = []
   454 |   just_change_space ((clausenum, step, strs)::xs) = let val newstrs = remove_space_strs strs
   455                                                  in
   456                                                     if (all_spaces newstrs = [] ) (* all type_info *)                                                    then    
   457                                                        (clausenum, step, newstrs)::(just_change_space xs)
   458                                                     else 
   459                                                         (clausenum, step, newstrs)::(just_change_space xs) 
   460                                                  end
   461 
   462 
   463 
   464 
   465 fun change_space []  = []
   466 |   change_space ((clausenum, step, strs)::xs) = let val newstrs = remove_space_strs strs
   467                                                  in
   468                                                     if (all_spaces newstrs = [] ) (* all type_info *)
   469                                                     then    
   470                                                        (clausenum, step, T_info, newstrs)::(change_space xs)
   471                                                     else 
   472                                                         (clausenum, step, P_info, newstrs)::(change_space xs) 
   473                                                  end
   474 
   475 end;