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