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