src/HOL/Tools/ATP/recon_parse.ML
author paulson
Mon Oct 10 15:35:29 2005 +0200 (2005-10-10)
changeset 17819 1241e5d31d5b
parent 17488 67376a311a2b
child 18443 a1d53af4c4c7
permissions -rw-r--r--
small tidy-up of utility functions
     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 is_prefix [] l = true
    77         | is_prefix (h::t) [] = false
    78         | is_prefix (h::t) (h'::t') = (h = h') andalso is_prefix t t'
    79       fun remove_prefix [] l = l
    80         | remove_prefix (h::t) [] = error "can't remove prefix"
    81         | remove_prefix (h::t) (h'::t') = remove_prefix t t'
    82       fun ccut t [] = raise NOCUT
    83         | ccut t s =
    84             if is_prefix t s then ([], remove_prefix t s) else
    85               let val (a, b) = ccut t (tl s) in ((hd s)::a, b) end
    86       fun cut t s =
    87         let
    88           val t' = explode t
    89           val s' = explode s
    90           val (a, b) = ccut t' s'
    91         in
    92           (implode a, implode b)
    93         end
    94     
    95       fun cut_exists t s
    96           = let val (a, b) = cut t s in true end handle NOCUT => false
    97 
    98       fun cut_before t s = let val (a, b) = cut t s in (a, t ^ b) end
    99       fun cut_after t s = let val (a, b) = cut t s in (a ^ t, b) end
   100     
   101 
   102     fun kill_lines 0 = Library.I
   103       | kill_lines n = kill_lines (n - 1) o snd o cut_after "\n";
   104 
   105 
   106 fun several p = many (some p)
   107       fun collect (h, t) = h ^ (fold_rev (fn s1 => fn s2 => s1 ^ s2) t "")
   108   
   109       fun lower_letter s = ("a" <= s) andalso (s <= "z")
   110       fun upper_letter s = ("A" <= s) andalso (s <= "Z")
   111       fun digit s = ("0" <= s) andalso (s <= "9")
   112       fun letter s = lower_letter s orelse upper_letter s
   113       fun alpha s = letter s orelse (s = "_")
   114       fun alphanum s = alpha s orelse digit s
   115       fun space s = (s = " ") orelse (s = "\n") orelse (s = "\t")
   116       (* FIX this is stopping it picking up numbers *)
   117       val word = (some alpha ++ several alphanum) >> (Word o collect)
   118       val number =
   119             (some digit ++ several digit) >> (Number o string2int o collect)
   120       val other = some (K true) >> Other
   121       
   122       val token = (word || number || other) ++ several space >> fst
   123       val tokens = (several space ++ many token) >> snd
   124       val alltokens = (tokens ++ finished) >> fst
   125     
   126      (* val lex = fst ( alltokens ( (map str)  explode))*)
   127      fun lex s =  alltokens  (explode s)
   128 
   129 
   130 (************************************************************)
   131 
   132 (**************************************************)
   133 (* Code to parse SPASS proofs                     *)
   134 (**************************************************)
   135 
   136 datatype Tree = Leaf of string
   137                 | Branch of Tree * Tree
   138 
   139    
   140       fun number ((Number n)::rest) = (n, rest)
   141         | number _ = raise NOPARSE_NUM
   142       fun word ((Word w)::rest) = (w, rest)
   143         | word _ = raise NOPARSE_WORD
   144 
   145       fun other_char ( (Other p)::rest) = (p, rest)
   146       | other_char _ =raise NOPARSE_WORD
   147      
   148       val number_list =
   149         (number ++ many number)
   150         >> (fn (a, b) => (a::b))
   151      
   152       val term_num =
   153         (number ++ (a (Other ".")) ++ number) >> (fn (a, (_, c)) => (a, c))
   154 
   155 
   156       val term_num_list = (term_num ++ many (a (Other ",") ++ term_num >> snd)
   157 			   >> (fn (a, b) => (a::b)))
   158 
   159       val axiom = (a (Word "Inp"))
   160             >> (fn (_) => Axiom)
   161       
   162       
   163       val binary = (a (Word "Res")) ++ (a (Other ":"))
   164                    ++ term_num ++ (a (Other ","))
   165                    ++ term_num
   166             >> (fn (_, (_, (c, (_, e)))) => Binary (c, e))
   167       
   168 
   169 
   170       val factor = (a (Word "Fac")) ++ (a (Other ":")) 
   171                     ++ term_num ++ (a (Other ",")) 
   172                     ++ term_num
   173             >> (fn (_, (_, (c, (_, e)))) =>  Factor ((fst c), (snd c),(snd e)))
   174      
   175       val para  = (a (Word "SPm")) ++ (a (Other ":"))
   176                    ++ term_num ++ (a (Other ","))
   177                    ++ term_num
   178             >> (fn (_, (_, (c, (_, e)))) => Para (c, e))
   179       
   180       val super_l  = (a (Word "SpL")) ++ (a (Other ":"))
   181                    ++ term_num ++ (a (Other ","))
   182                    ++ term_num
   183             >> (fn (_, (_, (c, (_, e)))) => Super_l (c, e))
   184 
   185 
   186       val super_r  = (a (Word "SpR")) ++ (a (Other ":"))
   187                    ++ term_num ++ (a (Other ","))
   188                    ++ term_num
   189             >> (fn (_, (_, (c, (_, e)))) => Super_r (c, e))
   190 
   191 
   192       val aed = (a (Word "AED")) ++ (a (Other ":")) ++ term_num
   193                  >> (fn (_, (_, c)) => Obvious ((fst c),(snd c)))
   194 
   195       val rewrite = (a (Word "Rew")) ++ (a (Other ":")) 
   196                     ++ term_num_list
   197             >> (fn (_, (_, (c))) =>  Rewrite (c))
   198 
   199 
   200       val mrr = (a (Word "MRR")) ++ (a (Other ":"))
   201                    ++ term_num ++ (a (Other ","))
   202                    ++ term_num
   203             >> (fn (_, (_, (c, (_, e)))) => MRR (c, e))
   204 
   205       val ssi = (a (Word "SSi")) ++ (a (Other ":"))
   206                    ++ term_num ++ (a (Other ","))
   207                    ++ term_num
   208             >> (fn (_, (_, (c, (_, e)))) => SortSimp (c, e))
   209 
   210     val unc = (a (Word "UnC")) ++ (a (Other ":"))
   211                    ++ term_num ++ (a (Other ","))
   212                    ++ term_num
   213             >> (fn (_, (_, (c, (_, e)))) => UnitConf (c, e))
   214 
   215 
   216 
   217       val obv = (a (Word "Obv")) ++ (a (Other ":")) ++ term_num
   218                  >> (fn (_, (_, c)) => Obvious ((fst c),(snd c)))
   219 
   220       val eqres = (a (Word "EqR")) ++ (a (Other ":")) ++ term_num
   221                  >> (fn (_, (_, c)) => EqualRes ((fst c),(snd c)))
   222    
   223       val con = (a (Word "Con")) ++ (a (Other ":")) ++ term_num
   224                  >> (fn (_, (_, c)) => Condense ((fst c),(snd c)))
   225 
   226 (*
   227       val hyper = a (Word "hyper")
   228                   ++ many ((a (Other ",") ++ number) >> snd)
   229                   >> (Hyper o snd)
   230 *)
   231      (* val method = axiom ||binary || factor || para || hyper*)
   232 
   233       val method = axiom || binary || factor || para ||super_l || super_r || rewrite || mrr || obv || aed || ssi || unc|| con
   234 
   235       val binary_s = a (Word "binary_s") ++ a (Other ",") ++ term_num
   236             >> (fn (_, (_, a)) => Binary_s a)
   237       val factor_s = a (Word "factor_s")
   238             >> (fn _ => Factor_s ())
   239       val demod_s = a (Word "demod")
   240                     ++ (many ((a (Other ",") ++ term_num) >> snd))
   241             >> (fn (_, a) => Demod_s a)
   242 
   243       val hyper_s = a (Word "hyper_s")
   244                     ++ many ((a (Other ",") ++ number) >> snd)
   245                     >> (Hyper_s o snd)
   246       val simp_method = binary_s || factor_s || demod_s || hyper_s
   247       val simp = a (Other ",") ++ simp_method >> snd
   248       val simps = many simp
   249  
   250 
   251       val justification =
   252            a (Other "[") ++number ++ a (Other ":") ++ method ++ a (Other "]")
   253                  >> (fn (_,(_, (_,(b, _)))) => b)
   254 
   255      
   256 exception NOTERM
   257 
   258 (* FIX - should change the stars and pluses to many rather than explicit patterns *)
   259 
   260 fun trim_prefix a b =
   261   let val n = String.size a 
   262   in  String.substring (b, n, (size b) - n)  end;
   263   
   264 
   265 (* FIX - add the other things later *)
   266 fun remove_typeinfo x  =  
   267     if String.isPrefix ResClause.fixed_var_prefix x
   268     then trim_prefix ResClause.fixed_var_prefix x
   269     else if String.isPrefix ResClause.schematic_var_prefix x
   270     then trim_prefix ResClause.schematic_var_prefix x
   271     else if String.isPrefix ResClause.const_prefix x
   272     then trim_prefix ResClause.const_prefix x
   273     else if String.isPrefix ResClause.tfree_prefix x
   274     then ""
   275     else if String.isPrefix ResClause.tvar_prefix x
   276     then ""
   277     else if String.isPrefix ResClause.tconst_prefix x
   278     then ""
   279     else x;                                               
   280 
   281 fun term input = (  ntermlist ++ a (Other "-") ++ a (Other ">") ++ ptermlist >>(fn (a,(_,(_,b))) =>  (a@b))
   282                   ) input
   283 
   284 (* pterms are terms from the rhs of the -> in the spass proof.  *)
   285 (* they should have a "~" in front of them so that they match with *)
   286 (* positive terms in the meta-clause *)
   287 (* nterm are terms from the lhs of the spass proof, and shouldn't *)
   288 (* "~"s added  word ++ a (Other "(") ++ arglist ++ a (Other ")") >> (fn (a,(_,(b,_ ))) =>  (a^" "^b)) *)
   289 
   290 and  pterm input = (
   291            peqterm >> (fn (a) => a)
   292         
   293          || word ++ a (Other "(") ++ arglist ++  a (Other ")") ++ 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 "*") ++ a (Other "*")
   300            >> (fn ( a, (_,(b, (_,(_,_))))) =>  ("~"^" "^(remove_typeinfo a)^" "^b))
   301         
   302 	|| word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*")
   303            >> (fn (a, (_,(b, (_,_)))) =>  ("~"^" "^(remove_typeinfo a)^" "^b))
   304 
   305         || word ++ a (Other "(") ++  arglist ++ a (Other ")") 
   306            >> (fn ( a, (_,(b,_ ))) => ("~"^" "^(remove_typeinfo a)^" "^b))
   307 
   308         || word ++ a (Other "*") >> (fn (w,b) => "~"^" "^(remove_typeinfo w))
   309 
   310         || word                  >> (fn w => "~"^" "^(remove_typeinfo w))) input
   311 
   312 and  nterm input =
   313     
   314        (  
   315            neqterm >> (fn (a) => a)
   316 
   317         || word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ 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 "*") ++ a (Other "*")
   324            >> (fn ( a, (_,(b, (_,(_,_))))) =>  ((remove_typeinfo a)^" "^b))
   325         
   326 	|| word ++ a (Other "(") ++ arglist ++ a (Other ")") ++ a (Other "*")
   327            >> (fn ( a, (_,(b, (_,_)))) =>  ((remove_typeinfo a)^" "^b))
   328 
   329         || word ++ a (Other "(") ++ arglist ++ a (Other ")") 
   330            >> (fn (a, (_,(b,_ ))) => ((remove_typeinfo a)^" "^b))
   331 
   332         || word ++ a (Other "*") >> (fn (w,b) =>  (remove_typeinfo w)) 
   333         || word                  >> (fn w =>  (remove_typeinfo w)) 
   334          ) input 
   335 
   336 
   337 and peqterm input =(
   338  
   339          a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   340          ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
   341             >> (fn (_,(_,(a,(_,(b,(_,(_,(_,_)))))))) => (a^" ~= "^b))
   342 
   343       || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   344           ++ a (Other "*") ++ a (Other "+")
   345             >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" ~= "^b))
   346 
   347       || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   348          ++ a (Other "*") ++ a (Other "*")
   349             >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" ~= "^b))
   350 
   351       || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   352          ++ a (Other "*") 
   353             >> (fn (_,(_,(a,(_,(b,(_,_)))))) => (a^" ~= "^b))
   354 
   355 
   356        ||a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   357             >> (fn (_,(_,(a,(_,(b,_))))) => (a^" ~= "^b))) input
   358 
   359 
   360 
   361 and neqterm input =(
   362  
   363          a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   364          ++ a (Other "*") ++ a (Other "*") ++ a (Other "+")
   365             >> (fn (_,(_,(a,(_,(b,(_,(_,(_,_)))))))) => (a^" = "^b))
   366 
   367       || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   368           ++ a (Other "*") ++ a (Other "+")
   369             >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" = "^b))
   370 
   371       || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   372          ++ a (Other "*") ++ a (Other "*")
   373             >> (fn (_,(_,(a,(_,(b,(_,(_,_))))))) => (a^" = "^b))
   374 
   375       || a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   376          ++ a (Other "*") 
   377             >> (fn (_,(_,(a,(_,(b,(_,_)))))) => (a^" = "^b))
   378 
   379 
   380        ||a (Word "equal") ++  a (Other "(") ++ nterm ++ a (Other ",") ++ nterm ++ a (Other ")") 
   381             >> (fn (_,(_,(a,(_,(b,_))))) => (a^" = "^b))) input
   382 
   383 
   384 
   385 and ptermlist input = (many  pterm
   386                       >> (fn (a) => (a))) input
   387 
   388 and ntermlist input = (many  nterm
   389                       >> (fn (a) => (a))) input
   390 
   391 (*and arglist input = (    nterm >> (fn (a) => (a))
   392                      ||  nterm ++ many (a (Other ",") ++ nterm >> snd)
   393                       >> (fn (a, b) => (a^" "^(space_implode " " b)))) input*)
   394 
   395 and arglist input = (   nterm ++ many (a (Other ",") ++ nterm >> snd)
   396                       >> (fn (a, b) => (a^" "^(space_implode " " b))) 
   397                       ||    nterm >> (fn (a) => (a)))input
   398 
   399  val clause =  term
   400 
   401 (* not entirely sure nterm is right here, but I don't think you get negative things before the ||s *)
   402  val line = number ++ justification ++ many( nterm) ++ a (Other "|") ++ 
   403             a (Other "|") ++ clause ++ a (Other ".")
   404           >> (fn (a, (z, (w, (_,( _, (c, _)))))) => (a, z,(w@ c)))
   405        
   406  val lines = many line
   407  val alllines = (lines ++ finished) >> fst
   408     
   409  val parse = fst o alllines
   410 
   411 end;