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