src/HOL/Tools/ATP/recon_parse.ML
author haftmann
Fri Feb 10 09:09:07 2006 +0100 (2006-02-10)
changeset 19008 14c1b2f5dda4
parent 18443 a1d53af4c4c7
permissions -rw-r--r--
improved code generator devarification
     1 (*  ID:         $Id$
     2     Author:     Claire Quigley
     3     Copyright   2004  University of Cambridge
     4 *)
     5 
     6 (* Parsing functions *)
     7 
     8 (* Auxiliary functions *)
     9 
    10 structure Recon_Parse =
    11 struct
    12 
    13 open ReconTranslateProof;
    14 
    15 exception NOPARSE_WORD
    16 exception NOPARSE_NUM
    17 fun to_upper s = String.translate (Char.toString o Char.toUpper) s;
    18 
    19 fun string2int s =
    20   (case Int.fromString s of SOME i => i
    21   | NONE => error "string -> int failed");
    22 
    23 
    24 (* Parser combinators *)
    25 
    26 exception Noparse;
    27 
    28 fun (parser1 ++ parser2) input =
    29       let
    30         val (result1, rest1) = parser1 input
    31         val (result2, rest2) = parser2 rest1
    32       in
    33         ((result1, result2), rest2)
    34       end;
    35 
    36 fun many parser input =
    37       let   (* Tree * token list*)
    38         val (result, next) = parser input
    39         val (results, rest) = many parser next
    40       in
    41         ((result::results), rest)
    42       end
    43       handle Noparse => ([], input)
    44 |            NOPARSE_WORD => ([], input)
    45 |            NOPARSE_NUM  => ([], input);
    46 
    47 
    48 
    49 fun (parser >> treatment) input =
    50       let
    51         val (result, rest) = parser input
    52       in
    53         (treatment result, rest)
    54       end;
    55 
    56 fun (parser1 || parser2) input = parser1 input
    57 handle Noparse => parser2 input;
    58 
    59 infixr 8 ++; infixr 7 >>; infixr 6 ||;
    60 
    61 fun some p [] = raise Noparse
    62   | some p (h::t) = if p h then (h, t) else raise Noparse;
    63 
    64 fun a tok = some (fn item => item = tok);
    65 
    66 fun finished input = if input = [] then (0, input) else raise Noparse;
    67 
    68 
    69   (* Parsing the output from gandalf *)
    70 datatype token = Word of string
    71                | Number of int
    72                | Other of string
    73 
    74 
    75       exception NOCUT
    76       fun remove_prefix [] l = l
    77         | remove_prefix (h::t) [] = error "can't remove prefix"
    78         | remove_prefix (h::t) (h'::t') = remove_prefix t t'
    79       fun ccut t [] = raise NOCUT
    80         | ccut t s =
    81             if is_prefix (op =) t s then ([], remove_prefix t s) else
    82               let val (a, b) = ccut t (tl s) in ((hd s)::a, b) end
    83       fun cut t s =
    84         let
    85           val t' = explode t
    86           val s' = explode s
    87           val (a, b) = ccut t' s'
    88         in
    89           (implode a, implode b)
    90         end
    91     
    92       fun cut_exists t s
    93           = let val (a, b) = cut t s in true end handle NOCUT => false
    94 
    95       fun cut_before t s = let val (a, b) = cut t s in (a, t ^ b) end
    96       fun cut_after t s = let val (a, b) = cut t s in (a ^ t, b) end
    97     
    98 
    99     fun kill_lines 0 = Library.I
   100       | kill_lines n = kill_lines (n - 1) o snd o cut_after "\n";
   101 
   102 
   103 fun several p = many (some p)
   104       fun collect (h, t) = h ^ (fold_rev (fn s1 => fn s2 => s1 ^ s2) t "")
   105   
   106       fun lower_letter s = ("a" <= s) andalso (s <= "z")
   107       fun upper_letter s = ("A" <= s) andalso (s <= "Z")
   108       fun digit s = ("0" <= s) andalso (s <= "9")
   109       fun letter s = lower_letter s orelse upper_letter s
   110       fun alpha s = letter s orelse (s = "_")
   111       fun alphanum s = alpha s orelse digit s
   112       fun space s = (s = " ") orelse (s = "\n") orelse (s = "\t")
   113       (* FIX this is stopping it picking up numbers *)
   114       val word = (some alpha ++ several alphanum) >> (Word o collect)
   115       val number =
   116             (some digit ++ several digit) >> (Number o string2int o collect)
   117       val other = some (K true) >> Other
   118       
   119       val token = (word || number || other) ++ several space >> fst
   120       val tokens = (several space ++ many token) >> snd
   121       val alltokens = (tokens ++ finished) >> fst
   122     
   123      (* val lex = fst ( alltokens ( (map str)  explode))*)
   124      fun lex s =  alltokens  (explode s)
   125 
   126 
   127 (************************************************************)
   128 
   129 (**************************************************)
   130 (* Code to parse SPASS proofs                     *)
   131 (**************************************************)
   132 
   133 datatype Tree = Leaf of string
   134                 | Branch of Tree * Tree
   135 
   136    
   137       fun number ((Number n)::rest) = (n, rest)
   138         | number _ = raise NOPARSE_NUM
   139       fun word ((Word w)::rest) = (w, rest)
   140         | word _ = raise NOPARSE_WORD
   141 
   142       fun other_char ( (Other p)::rest) = (p, rest)
   143       | other_char _ =raise NOPARSE_WORD
   144      
   145       val number_list =
   146         (number ++ many number)
   147         >> (fn (a, b) => (a::b))
   148      
   149       val term_num =
   150         (number ++ (a (Other ".")) ++ number) >> (fn (a, (_, c)) => (a, c))
   151 
   152 
   153       val term_num_list = (term_num ++ many (a (Other ",") ++ term_num >> snd)
   154 			   >> (fn (a, b) => (a::b)))
   155 
   156       val axiom = (a (Word "Inp"))
   157             >> (fn (_) => Axiom)
   158       
   159       
   160       val binary = (a (Word "Res")) ++ (a (Other ":"))
   161                    ++ term_num ++ (a (Other ","))
   162                    ++ term_num
   163             >> (fn (_, (_, (c, (_, e)))) => Binary (c, e))
   164       
   165 
   166 
   167       val factor = (a (Word "Fac")) ++ (a (Other ":")) 
   168                     ++ term_num ++ (a (Other ",")) 
   169                     ++ term_num
   170             >> (fn (_, (_, (c, (_, e)))) =>  Factor ((fst c), (snd c),(snd e)))
   171      
   172       val para  = (a (Word "SPm")) ++ (a (Other ":"))
   173                    ++ term_num ++ (a (Other ","))
   174                    ++ term_num
   175             >> (fn (_, (_, (c, (_, e)))) => Para (c, e))
   176       
   177       val super_l  = (a (Word "SpL")) ++ (a (Other ":"))
   178                    ++ term_num ++ (a (Other ","))
   179                    ++ term_num
   180             >> (fn (_, (_, (c, (_, e)))) => Super_l (c, e))
   181 
   182 
   183       val super_r  = (a (Word "SpR")) ++ (a (Other ":"))
   184                    ++ term_num ++ (a (Other ","))
   185                    ++ term_num
   186             >> (fn (_, (_, (c, (_, e)))) => Super_r (c, e))
   187 
   188 
   189       val aed = (a (Word "AED")) ++ (a (Other ":")) ++ term_num
   190                  >> (fn (_, (_, c)) => Obvious ((fst c),(snd c)))
   191 
   192       val rewrite = (a (Word "Rew")) ++ (a (Other ":")) 
   193                     ++ term_num_list
   194             >> (fn (_, (_, (c))) =>  Rewrite (c))
   195 
   196 
   197       val mrr = (a (Word "MRR")) ++ (a (Other ":"))
   198                    ++ term_num ++ (a (Other ","))
   199                    ++ term_num
   200             >> (fn (_, (_, (c, (_, e)))) => MRR (c, e))
   201 
   202       val ssi = (a (Word "SSi")) ++ (a (Other ":"))
   203                    ++ term_num ++ (a (Other ","))
   204                    ++ term_num
   205             >> (fn (_, (_, (c, (_, e)))) => SortSimp (c, e))
   206 
   207     val unc = (a (Word "UnC")) ++ (a (Other ":"))
   208                    ++ term_num ++ (a (Other ","))
   209                    ++ term_num
   210             >> (fn (_, (_, (c, (_, e)))) => UnitConf (c, e))
   211 
   212 
   213 
   214       val obv = (a (Word "Obv")) ++ (a (Other ":")) ++ term_num
   215                  >> (fn (_, (_, c)) => Obvious ((fst c),(snd c)))
   216 
   217       val eqres = (a (Word "EqR")) ++ (a (Other ":")) ++ term_num
   218                  >> (fn (_, (_, c)) => EqualRes ((fst c),(snd c)))
   219    
   220       val con = (a (Word "Con")) ++ (a (Other ":")) ++ term_num
   221                  >> (fn (_, (_, c)) => Condense ((fst c),(snd c)))
   222 
   223 (*
   224       val hyper = a (Word "hyper")
   225                   ++ many ((a (Other ",") ++ number) >> snd)
   226                   >> (Hyper o snd)
   227 *)
   228      (* val method = axiom ||binary || factor || para || hyper*)
   229 
   230       val method = axiom || binary || factor || para ||super_l || super_r || rewrite || mrr || obv || aed || ssi || unc|| con
   231 
   232       val binary_s = a (Word "binary_s") ++ a (Other ",") ++ term_num
   233             >> (fn (_, (_, a)) => Binary_s a)
   234       val factor_s = a (Word "factor_s")
   235             >> (fn _ => Factor_s ())
   236       val demod_s = a (Word "demod")
   237                     ++ (many ((a (Other ",") ++ term_num) >> snd))
   238             >> (fn (_, a) => Demod_s a)
   239 
   240       val hyper_s = a (Word "hyper_s")
   241                     ++ many ((a (Other ",") ++ number) >> snd)
   242                     >> (Hyper_s o snd)
   243       val simp_method = binary_s || factor_s || demod_s || hyper_s
   244       val simp = a (Other ",") ++ simp_method >> snd
   245       val simps = many simp
   246  
   247 
   248       val justification =
   249            a (Other "[") ++number ++ a (Other ":") ++ method ++ a (Other "]")
   250                  >> (fn (_,(_, (_,(b, _)))) => b)
   251 
   252      
   253 exception NOTERM
   254 
   255 (* FIX - should change the stars and pluses to many rather than explicit patterns *)
   256 
   257 fun trim_prefix a b =
   258   let val n = String.size a 
   259   in  String.substring (b, n, (size b) - n)  end;
   260   
   261 
   262 (* FIX - add the other things later *)
   263 fun remove_typeinfo x  =  
   264     if String.isPrefix ResClause.fixed_var_prefix x
   265     then trim_prefix ResClause.fixed_var_prefix x
   266     else if String.isPrefix ResClause.schematic_var_prefix x
   267     then trim_prefix ResClause.schematic_var_prefix x
   268     else if String.isPrefix ResClause.const_prefix x
   269     then trim_prefix ResClause.const_prefix x
   270     else if String.isPrefix ResClause.tfree_prefix x
   271     then ""
   272     else if String.isPrefix ResClause.tvar_prefix x
   273     then ""
   274     else if String.isPrefix ResClause.tconst_prefix x
   275     then ""
   276     else x;                                               
   277 
   278 fun term input = (  ntermlist ++ a (Other "-") ++ a (Other ">") ++ ptermlist >>(fn (a,(_,(_,b))) =>  (a@b))
   279                   ) input
   280 
   281 (* pterms are terms from the rhs of the -> in the spass proof.  *)
   282 (* they should have a "~" in front of them so that they match with *)
   283 (* positive terms in the meta-clause *)
   284 (* nterm are terms from the lhs of the spass proof, and shouldn't *)
   285 (* "~"s added  word ++ a (Other "(") ++ arglist ++ a (Other ")") >> (fn (a,(_,(b,_ ))) =>  (a^" "^b)) *)
   286 
   287 and  pterm input = (
   288            peqterm >> (fn (a) => a)
   289         
   290          || word ++ a (Other "(") ++ arglist ++  a (Other ")") ++ a (Other "*")++ a (Other "*") ++ a (Other "+")
   291            >> (fn (a, (_,(b, (_,(_,_))))) =>  ("~"^" "^(remove_typeinfo a)^" "^b))
   292          
   293         || word ++ a (Other "(") ++ arglist ++  a (Other ")") ++ a (Other "*") ++ a (Other "+")
   294            >> (fn ( a, (_,(b, (_,(_,_))))) =>  ("~"^" "^(remove_typeinfo a)^" "^b))
   295         
   296         || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*")
   297            >> (fn ( a, (_,(b, (_,(_,_))))) =>  ("~"^" "^(remove_typeinfo a)^" "^b))
   298         
   299 	|| word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*")
   300            >> (fn (a, (_,(b, (_,_)))) =>  ("~"^" "^(remove_typeinfo a)^" "^b))
   301 
   302         || word ++ a (Other "(") ++  arglist ++ a (Other ")") 
   303            >> (fn ( a, (_,(b,_ ))) => ("~"^" "^(remove_typeinfo a)^" "^b))
   304 
   305         || word ++ a (Other "*") >> (fn (w,b) => "~"^" "^(remove_typeinfo w))
   306 
   307         || word                  >> (fn w => "~"^" "^(remove_typeinfo w))) input
   308 
   309 and  nterm input =
   310     
   311        (  
   312            neqterm >> (fn (a) => a)
   313 
   314         || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
   315            >> (fn ( a, (_,(b, (_,(_,_))))) =>  ((remove_typeinfo a)^" "^b))
   316 
   317         || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "+")
   318            >> (fn ( a, (_,(b, (_,(_,_))))) =>  ((remove_typeinfo a)^" "^b))
   319         
   320         || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*") ++ a (Other "*")
   321            >> (fn ( a, (_,(b, (_,(_,_))))) =>  ((remove_typeinfo a)^" "^b))
   322         
   323 	|| word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*")
   324            >> (fn ( a, (_,(b, (_,_)))) =>  ((remove_typeinfo a)^" "^b))
   325 
   326         || word ++ a (Other "(") ++ arglist ++ a (Other ")") 
   327            >> (fn (a, (_,(b,_ ))) => ((remove_typeinfo a)^" "^b))
   328 
   329         || word ++ a (Other "*") >> (fn (w,b) =>  (remove_typeinfo w)) 
   330         || word                  >> (fn w =>  (remove_typeinfo w)) 
   331          ) input 
   332 
   333 
   334 and peqterm input =(
   335  
   336          a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   337          ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
   338             >> (fn (_,(_,(a,(_,(b,(_,(_,(_,_)))))))) => (a^" ~= "^b))
   339 
   340       || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   341           ++ a (Other "*") ++ a (Other "+")
   342             >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" ~= "^b))
   343 
   344       || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   345          ++ a (Other "*") ++ a (Other "*")
   346             >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" ~= "^b))
   347 
   348       || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   349          ++ a (Other "*") 
   350             >> (fn (_,(_,(a,(_,(b,(_,_)))))) => (a^" ~= "^b))
   351 
   352 
   353        ||a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   354             >> (fn (_,(_,(a,(_,(b,_))))) => (a^" ~= "^b))) input
   355 
   356 
   357 
   358 and neqterm input =(
   359  
   360          a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   361          ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
   362             >> (fn (_,(_,(a,(_,(b,(_,(_,(_,_)))))))) => (a^" = "^b))
   363 
   364       || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   365           ++ a (Other "*") ++ a (Other "+")
   366             >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" = "^b))
   367 
   368       || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   369          ++ a (Other "*") ++ a (Other "*")
   370             >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" = "^b))
   371 
   372       || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   373          ++ a (Other "*") 
   374             >> (fn (_,(_,(a,(_,(b,(_,_)))))) => (a^" = "^b))
   375 
   376 
   377        ||a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   378             >> (fn (_,(_,(a,(_,(b,_))))) => (a^" = "^b))) input
   379 
   380 
   381 
   382 and ptermlist input = (many  pterm
   383                       >> (fn (a) => (a))) input
   384 
   385 and ntermlist input = (many  nterm
   386                       >> (fn (a) => (a))) input
   387 
   388 (*and arglist input = (    nterm >> (fn (a) => (a))
   389                      ||  nterm ++ many (a (Other ",") ++ nterm >> snd)
   390                       >> (fn (a, b) => (a^" "^(space_implode " " b)))) input*)
   391 
   392 and arglist input = (   nterm ++ many (a (Other ",") ++ nterm >> snd)
   393                       >> (fn (a, b) => (a^" "^(space_implode " " b))) 
   394                       ||    nterm >> (fn (a) => (a)))input
   395 
   396  val clause =  term
   397 
   398 (* not entirely sure nterm is right here, but I don't think you get negative things before the ||s *)
   399  val line = number ++ justification ++ many( nterm) ++ a (Other "|") ++ 
   400             a (Other "|") ++ clause ++ a (Other ".")
   401           >> (fn (a, (z, (w, (_,( _, (c, _)))))) => (a, z,(w@ c)))
   402        
   403  val lines = many line
   404  val alllines = (lines ++ finished) >> fst
   405     
   406  val parse = fst o alllines
   407 
   408 end;