src/HOL/TPTP/TPTP_Parser/ml_yacc_lib.ML
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 46844 5d9aab0c609c
child 56281 03c3d1a7c3b8
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
46844
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     1
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     2
(******************************************************************)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     3
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     4
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     5
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     6
(******************************************************************)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     7
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     8
print_depth 0;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
     9
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    10
(*
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    11
  This file is generated from the contents of ML-Yacc's lib directory.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    12
  ML-Yacc's COPYRIGHT-file contents follow:
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    13
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    14
  ML-YACC COPYRIGHT NOTICE, LICENSE AND DISCLAIMER.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    15
  
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    16
  Copyright 1989, 1990 by David R. Tarditi Jr. and Andrew W. Appel
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    17
  
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    18
  Permission to use, copy, modify, and distribute this software and its
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    19
  documentation for any purpose and without fee is hereby granted,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    20
  provided that the above copyright notice appear in all copies and that
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    21
  both the copyright notice and this permission notice and warranty
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    22
  disclaimer appear in supporting documentation, and that the names of
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    23
  David R. Tarditi Jr. and Andrew W. Appel not be used in advertising
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    24
  or publicity pertaining to distribution of the software without
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    25
  specific, written prior permission.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    26
  
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    27
  David R. Tarditi Jr. and Andrew W. Appel disclaim all warranties with regard to
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    28
  this software, including all implied warranties of merchantability and fitness.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    29
  In no event shall David R. Tarditi Jr. and Andrew W. Appel be liable for any
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    30
  special, indirect or consequential damages or any damages whatsoever resulting
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    31
  from loss of use, data or profits, whether in an action of contract, negligence
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    32
  or other tortious action, arising out of or in connection with the use or
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    33
  performance of this software.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    34
*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    35
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    36
(**** Original file: base.sig ****)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    37
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    38
(* ML-Yacc Parser Generator (c) 1989 Andrew W. Appel, David R. Tarditi *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    39
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    40
(* base.sig: Base signature file for SML-Yacc.  This file contains signatures
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    41
   that must be loaded before any of the files produced by ML-Yacc are loaded
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    42
*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    43
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    44
(* STREAM: signature for a lazy stream.*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    45
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    46
signature STREAM =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    47
 sig type 'xa stream
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    48
     val streamify : (unit -> '_a) -> '_a stream
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    49
     val cons : '_a * '_a stream -> '_a stream
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    50
     val get : '_a stream -> '_a * '_a stream
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    51
 end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    52
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    53
(* LR_TABLE: signature for an LR Table.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    54
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    55
   The list of actions and gotos passed to mkLrTable must be ordered by state
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    56
   number. The values for state 0 are the first in the list, the values for
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    57
    state 1 are next, etc.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    58
*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    59
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    60
signature LR_TABLE =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    61
    sig
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    62
        datatype ('a,'b) pairlist = EMPTY | PAIR of 'a * 'b * ('a,'b) pairlist
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    63
	datatype state = STATE of int
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    64
	datatype term = T of int
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    65
	datatype nonterm = NT of int
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    66
	datatype action = SHIFT of state
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    67
			| REDUCE of int
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    68
			| ACCEPT
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    69
			| ERROR
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    70
	type table
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    71
	
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    72
	val numStates : table -> int
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    73
	val numRules : table -> int
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    74
	val describeActions : table -> state ->
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    75
				(term,action) pairlist * action
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    76
	val describeGoto : table -> state -> (nonterm,state) pairlist
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    77
	val action : table -> state * term -> action
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    78
	val goto : table -> state * nonterm -> state
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    79
	val initialState : table -> state
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    80
	exception Goto of state * nonterm
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    81
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    82
	val mkLrTable : {actions : ((term,action) pairlist * action) array,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    83
			 gotos : (nonterm,state) pairlist array,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    84
			 numStates : int, numRules : int,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    85
			 initialState : state} -> table
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    86
    end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    87
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    88
(* TOKEN: signature revealing the internal structure of a token. This signature
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    89
   TOKEN distinct from the signature {parser name}_TOKENS produced by ML-Yacc.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    90
   The {parser name}_TOKENS structures contain some types and functions to
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    91
    construct tokens from values and positions.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    92
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    93
   The representation of token was very carefully chosen here to allow the
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    94
   polymorphic parser to work without knowing the types of semantic values
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    95
   or line numbers.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    96
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    97
   This has had an impact on the TOKENS structure produced by SML-Yacc, which
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    98
   is a structure parameter to lexer functors.  We would like to have some
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
    99
   type 'a token which functions to construct tokens would create.  A
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   100
   constructor function for a integer token might be
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   101
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   102
	  INT: int * 'a * 'a -> 'a token.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   103
 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   104
   This is not possible because we need to have tokens with the representation
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   105
   given below for the polymorphic parser.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   106
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   107
   Thus our constructur functions for tokens have the form:
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   108
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   109
	  INT: int * 'a * 'a -> (svalue,'a) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   110
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   111
   This in turn has had an impact on the signature that lexers for SML-Yacc
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   112
   must match and the types that a user must declare in the user declarations
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   113
   section of lexers.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   114
*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   115
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   116
signature TOKEN =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   117
    sig
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   118
	structure LrTable : LR_TABLE
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   119
        datatype ('a,'b) token = TOKEN of LrTable.term * ('a * 'b * 'b)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   120
	val sameToken : ('a,'b) token * ('a,'b) token -> bool
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   121
    end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   122
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   123
(* LR_PARSER: signature for a polymorphic LR parser *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   124
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   125
signature LR_PARSER =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   126
    sig
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   127
	structure Stream: STREAM
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   128
	structure LrTable : LR_TABLE
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   129
	structure Token : TOKEN
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   130
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   131
	sharing LrTable = Token.LrTable
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   132
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   133
	exception ParseError
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   134
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   135
	val parse : {table : LrTable.table,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   136
		     lexer : ('_b,'_c) Token.token Stream.stream,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   137
		     arg: 'arg,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   138
		     saction : int *
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   139
			       '_c *
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   140
				(LrTable.state * ('_b * '_c * '_c)) list * 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   141
				'arg ->
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   142
				     LrTable.nonterm *
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   143
				     ('_b * '_c * '_c) *
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   144
				     ((LrTable.state *('_b * '_c * '_c)) list),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   145
		     void : '_b,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   146
		     ec : { is_keyword : LrTable.term -> bool,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   147
			    noShift : LrTable.term -> bool,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   148
			    preferred_change : (LrTable.term list * LrTable.term list) list,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   149
			    errtermvalue : LrTable.term -> '_b,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   150
			    showTerminal : LrTable.term -> string,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   151
			    terms: LrTable.term list,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   152
			    error : string * '_c * '_c -> unit
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   153
			   },
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   154
		     lookahead : int  (* max amount of lookahead used in *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   155
				      (* error correction *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   156
			} -> '_b *
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   157
			     (('_b,'_c) Token.token Stream.stream)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   158
    end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   159
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   160
(* LEXER: a signature that most lexers produced for use with SML-Yacc's
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   161
   output will match.  The user is responsible for declaring type token,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   162
   type pos, and type svalue in the UserDeclarations section of a lexer.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   163
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   164
   Note that type token is abstract in the lexer.  This allows SML-Yacc to
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   165
   create a TOKENS signature for use with lexers produced by ML-Lex that
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   166
   treats the type token abstractly.  Lexers that are functors parametrized by
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   167
   a Tokens structure matching a TOKENS signature cannot examine the structure
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   168
   of tokens.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   169
*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   170
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   171
signature LEXER =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   172
   sig
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   173
       structure UserDeclarations :
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   174
	   sig
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   175
	        type ('a,'b) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   176
		type pos
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   177
		type svalue
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   178
	   end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   179
	val makeLexer : (int -> string) -> unit -> 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   180
         (UserDeclarations.svalue,UserDeclarations.pos) UserDeclarations.token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   181
   end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   182
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   183
(* ARG_LEXER: the %arg option of ML-Lex allows users to produce lexers which
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   184
   also take an argument before yielding a function from unit to a token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   185
*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   186
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   187
signature ARG_LEXER =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   188
   sig
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   189
       structure UserDeclarations :
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   190
	   sig
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   191
	        type ('a,'b) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   192
		type pos
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   193
		type svalue
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   194
		type arg
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   195
	   end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   196
	val makeLexer : (int -> string) -> UserDeclarations.arg -> unit -> 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   197
         (UserDeclarations.svalue,UserDeclarations.pos) UserDeclarations.token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   198
   end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   199
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   200
(* PARSER_DATA: the signature of ParserData structures in {parser name}LrValsFun
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   201
   produced by  SML-Yacc.  All such structures match this signature.  
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   202
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   203
   The {parser name}LrValsFun produces a structure which contains all the values
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   204
   except for the lexer needed to call the polymorphic parser mentioned
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   205
   before.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   206
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   207
*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   208
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   209
signature PARSER_DATA =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   210
   sig
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   211
        (* the type of line numbers *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   212
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   213
	type pos
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   214
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   215
	(* the type of semantic values *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   216
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   217
	type svalue
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   218
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   219
         (* the type of the user-supplied argument to the parser *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   220
 	type arg
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   221
 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   222
	(* the intended type of the result of the parser.  This value is
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   223
	   produced by applying extract from the structure Actions to the
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   224
	   final semantic value resultiing from a parse.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   225
	 *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   226
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   227
	type result
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   228
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   229
	structure LrTable : LR_TABLE
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   230
	structure Token : TOKEN
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   231
	sharing Token.LrTable = LrTable
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   232
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   233
	(* structure Actions contains the functions which mantain the
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   234
	   semantic values stack in the parser.  Void is used to provide
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   235
	   a default value for the semantic stack.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   236
	 *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   237
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   238
	structure Actions : 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   239
	  sig
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   240
	      val actions : int * pos *
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   241
		   (LrTable.state * (svalue * pos * pos)) list * arg->
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   242
		         LrTable.nonterm * (svalue * pos * pos) *
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   243
			 ((LrTable.state *(svalue * pos * pos)) list)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   244
	      val void : svalue
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   245
	      val extract : svalue -> result
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   246
	  end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   247
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   248
	(* structure EC contains information used to improve error
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   249
	   recovery in an error-correcting parser *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   250
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   251
	structure EC :
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   252
	   sig
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   253
	     val is_keyword : LrTable.term -> bool
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   254
	     val noShift : LrTable.term -> bool
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   255
 	     val preferred_change : (LrTable.term list * LrTable.term list) list
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   256
	     val errtermvalue : LrTable.term -> svalue
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   257
	     val showTerminal : LrTable.term -> string
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   258
	     val terms: LrTable.term list
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   259
	   end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   260
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   261
	(* table is the LR table for the parser *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   262
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   263
	val table : LrTable.table
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   264
    end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   265
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   266
(* signature PARSER is the signature that most user parsers created by 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   267
   SML-Yacc will match.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   268
*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   269
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   270
signature PARSER =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   271
    sig
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   272
        structure Token : TOKEN
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   273
	structure Stream : STREAM
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   274
	exception ParseError
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   275
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   276
	(* type pos is the type of line numbers *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   277
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   278
	type pos
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   279
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   280
	(* type result is the type of the result from the parser *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   281
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   282
	type result
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   283
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   284
         (* the type of the user-supplied argument to the parser *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   285
 	type arg
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   286
	
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   287
	(* type svalue is the type of semantic values for the semantic value
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   288
	   stack
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   289
	 *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   290
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   291
	type svalue
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   292
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   293
	(* val makeLexer is used to create a stream of tokens for the parser *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   294
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   295
	val makeLexer : (int -> string) ->
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   296
			 (svalue,pos) Token.token Stream.stream
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   297
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   298
	(* val parse takes a stream of tokens and a function to TextIO.print
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   299
	   errors and returns a value of type result and a stream containing
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   300
	   the unused tokens
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   301
	 *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   302
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   303
	val parse : int * ((svalue,pos) Token.token Stream.stream) *
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   304
		    (string * pos * pos -> unit) * arg ->
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   305
				result * (svalue,pos) Token.token Stream.stream
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   306
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   307
	val sameToken : (svalue,pos) Token.token * (svalue,pos) Token.token ->
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   308
				bool
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   309
     end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   310
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   311
(* signature ARG_PARSER is the signature that will be matched by parsers whose
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   312
    lexer takes an additional argument.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   313
*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   314
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   315
signature ARG_PARSER = 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   316
    sig
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   317
        structure Token : TOKEN
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   318
	structure Stream : STREAM
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   319
	exception ParseError
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   320
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   321
	type arg
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   322
	type lexarg
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   323
	type pos
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   324
	type result
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   325
	type svalue
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   326
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   327
	val makeLexer : (int -> string) -> lexarg ->
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   328
			 (svalue,pos) Token.token Stream.stream
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   329
	val parse : int * ((svalue,pos) Token.token Stream.stream) *
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   330
		    (string * pos * pos -> unit) * arg ->
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   331
				result * (svalue,pos) Token.token Stream.stream
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   332
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   333
	val sameToken : (svalue,pos) Token.token * (svalue,pos) Token.token ->
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   334
				bool
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   335
     end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   336
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   337
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   338
(**** Original file: join.sml ****)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   339
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   340
(* ML-Yacc Parser Generator (c) 1989 Andrew W. Appel, David R. Tarditi *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   341
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   342
(* functor Join creates a user parser by putting together a Lexer structure,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   343
   an LrValues structure, and a polymorphic parser structure.  Note that
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   344
   the Lexer and LrValues structure must share the type pos (i.e. the type
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   345
   of line numbers), the type svalues for semantic values, and the type
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   346
   of tokens.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   347
*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   348
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   349
functor Join(structure Lex : LEXER
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   350
	     structure ParserData: PARSER_DATA
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   351
	     structure LrParser : LR_PARSER
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   352
	     sharing ParserData.LrTable = LrParser.LrTable
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   353
	     sharing ParserData.Token = LrParser.Token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   354
	     sharing type Lex.UserDeclarations.svalue = ParserData.svalue
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   355
	     sharing type Lex.UserDeclarations.pos = ParserData.pos
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   356
	     sharing type Lex.UserDeclarations.token = ParserData.Token.token)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   357
		 : PARSER =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   358
struct
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   359
    structure Token = ParserData.Token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   360
    structure Stream = LrParser.Stream
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   361
 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   362
    exception ParseError = LrParser.ParseError
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   363
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   364
    type arg = ParserData.arg
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   365
    type pos = ParserData.pos
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   366
    type result = ParserData.result
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   367
    type svalue = ParserData.svalue
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   368
    val makeLexer = LrParser.Stream.streamify o Lex.makeLexer
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   369
    val parse = fn (lookahead,lexer,error,arg) =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   370
	(fn (a,b) => (ParserData.Actions.extract a,b))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   371
     (LrParser.parse {table = ParserData.table,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   372
	        lexer=lexer,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   373
		lookahead=lookahead,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   374
		saction = ParserData.Actions.actions,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   375
		arg=arg,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   376
		void= ParserData.Actions.void,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   377
	        ec = {is_keyword = ParserData.EC.is_keyword,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   378
		      noShift = ParserData.EC.noShift,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   379
		      preferred_change = ParserData.EC.preferred_change,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   380
		      errtermvalue = ParserData.EC.errtermvalue,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   381
		      error=error,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   382
		      showTerminal = ParserData.EC.showTerminal,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   383
		      terms = ParserData.EC.terms}}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   384
      )
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   385
     val sameToken = Token.sameToken
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   386
end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   387
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   388
(* functor JoinWithArg creates a variant of the parser structure produced 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   389
   above.  In this case, the makeLexer take an additional argument before
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   390
   yielding a value of type unit -> (svalue,pos) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   391
 *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   392
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   393
functor JoinWithArg(structure Lex : ARG_LEXER
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   394
	     structure ParserData: PARSER_DATA
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   395
	     structure LrParser : LR_PARSER
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   396
	     sharing ParserData.LrTable = LrParser.LrTable
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   397
	     sharing ParserData.Token = LrParser.Token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   398
	     sharing type Lex.UserDeclarations.svalue = ParserData.svalue
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   399
	     sharing type Lex.UserDeclarations.pos = ParserData.pos
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   400
	     sharing type Lex.UserDeclarations.token = ParserData.Token.token)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   401
		 : ARG_PARSER  =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   402
struct
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   403
    structure Token = ParserData.Token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   404
    structure Stream = LrParser.Stream
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   405
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   406
    exception ParseError = LrParser.ParseError
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   407
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   408
    type arg = ParserData.arg
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   409
    type lexarg = Lex.UserDeclarations.arg
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   410
    type pos = ParserData.pos
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   411
    type result = ParserData.result
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   412
    type svalue = ParserData.svalue
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   413
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   414
    val makeLexer = fn s => fn arg =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   415
		 LrParser.Stream.streamify (Lex.makeLexer s arg)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   416
    val parse = fn (lookahead,lexer,error,arg) =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   417
	(fn (a,b) => (ParserData.Actions.extract a,b))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   418
     (LrParser.parse {table = ParserData.table,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   419
	        lexer=lexer,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   420
		lookahead=lookahead,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   421
		saction = ParserData.Actions.actions,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   422
		arg=arg,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   423
		void= ParserData.Actions.void,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   424
	        ec = {is_keyword = ParserData.EC.is_keyword,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   425
		      noShift = ParserData.EC.noShift,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   426
		      preferred_change = ParserData.EC.preferred_change,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   427
		      errtermvalue = ParserData.EC.errtermvalue,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   428
		      error=error,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   429
		      showTerminal = ParserData.EC.showTerminal,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   430
		      terms = ParserData.EC.terms}}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   431
      )
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   432
    val sameToken = Token.sameToken
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   433
end;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   434
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   435
(**** Original file: lrtable.sml ****)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   436
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   437
(* ML-Yacc Parser Generator (c) 1989 Andrew W. Appel, David R. Tarditi *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   438
structure LrTable : LR_TABLE = 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   439
    struct
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   440
	open Array List
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   441
	infix 9 sub
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   442
	datatype ('a,'b) pairlist = EMPTY
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   443
				  | PAIR of 'a * 'b * ('a,'b) pairlist
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   444
	datatype term = T of int
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   445
	datatype nonterm = NT of int
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   446
	datatype state = STATE of int
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   447
	datatype action = SHIFT of state
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   448
			| REDUCE of int (* rulenum from grammar *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   449
			| ACCEPT
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   450
			| ERROR
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   451
	exception Goto of state * nonterm
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   452
	type table = {states: int, rules : int,initialState: state,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   453
		      action: ((term,action) pairlist * action) array,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   454
		      goto :  (nonterm,state) pairlist array}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   455
	val numStates = fn ({states,...} : table) => states
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   456
	val numRules = fn ({rules,...} : table) => rules
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   457
	val describeActions =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   458
	   fn ({action,...} : table) => 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   459
	           fn (STATE s) => action sub s
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   460
	val describeGoto =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   461
	   fn ({goto,...} : table) =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   462
	           fn (STATE s) => goto sub s
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   463
	fun findTerm (T term,row,default) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   464
	    let fun find (PAIR (T key,data,r)) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   465
		       if key < term then find r
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   466
		       else if key=term then data
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   467
		       else default
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   468
		   | find EMPTY = default
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   469
	    in find row
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   470
	    end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   471
	fun findNonterm (NT nt,row) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   472
	    let fun find (PAIR (NT key,data,r)) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   473
		       if key < nt then find r
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   474
		       else if key=nt then SOME data
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   475
		       else NONE
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   476
		   | find EMPTY = NONE
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   477
	    in find row
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   478
	    end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   479
	val action = fn ({action,...} : table) =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   480
		fn (STATE state,term) =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   481
		  let val (row,default) = action sub state
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   482
		  in findTerm(term,row,default)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   483
		  end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   484
	val goto = fn ({goto,...} : table) =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   485
			fn (a as (STATE state,nonterm)) =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   486
			  case findNonterm(nonterm,goto sub state)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   487
			  of SOME state => state
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   488
			   | NONE => raise (Goto a)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   489
	val initialState = fn ({initialState,...} : table) => initialState
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   490
	val mkLrTable = fn {actions,gotos,initialState,numStates,numRules} =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   491
	     ({action=actions,goto=gotos,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   492
	       states=numStates,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   493
	       rules=numRules,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   494
               initialState=initialState} : table)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   495
end;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   496
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   497
(**** Original file: stream.sml ****)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   498
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   499
(* ML-Yacc Parser Generator (c) 1989 Andrew W. Appel, David R. Tarditi *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   500
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   501
(* Stream: a structure implementing a lazy stream.  The signature STREAM
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   502
   is found in base.sig *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   503
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   504
structure Stream :> STREAM =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   505
struct
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   506
   datatype 'a str = EVAL of 'a * 'a str Unsynchronized.ref | UNEVAL of (unit->'a)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   507
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   508
   type 'a stream = 'a str Unsynchronized.ref
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   509
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   510
   fun get(Unsynchronized.ref(EVAL t)) = t
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   511
     | get(s as Unsynchronized.ref(UNEVAL f)) = 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   512
	    let val t = (f(), Unsynchronized.ref(UNEVAL f)) in s := EVAL t; t end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   513
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   514
   fun streamify f = Unsynchronized.ref(UNEVAL f)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   515
   fun cons(a,s) = Unsynchronized.ref(EVAL(a,s))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   516
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   517
end;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   518
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   519
(**** Original file: parser2.sml ****)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   520
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   521
(* ML-Yacc Parser Generator (c) 1989 Andrew W. Appel, David R. Tarditi *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   522
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   523
(* parser.sml:  This is a parser driver for LR tables with an error-recovery
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   524
   routine added to it.  The routine used is described in detail in this
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   525
   article:
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   526
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   527
	'A Practical Method for LR and LL Syntactic Error Diagnosis and
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   528
	 Recovery', by M. Burke and G. Fisher, ACM Transactions on
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   529
	 Programming Langauges and Systems, Vol. 9, No. 2, April 1987,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   530
	 pp. 164-197.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   531
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   532
    This program is an implementation is the partial, deferred method discussed
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   533
    in the article.  The algorithm and data structures used in the program
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   534
    are described below.  
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   535
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   536
    This program assumes that all semantic actions are delayed.  A semantic
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   537
    action should produce a function from unit -> value instead of producing the
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   538
    normal value.  The parser returns the semantic value on the top of the
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   539
    stack when accept is encountered.  The user can deconstruct this value
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   540
    and apply the unit -> value function in it to get the answer.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   541
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   542
    It also assumes that the lexer is a lazy stream.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   543
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   544
    Data Structures:
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   545
    ----------------
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   546
	
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   547
	* The parser:
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   548
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   549
	   The state stack has the type
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   550
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   551
		 (state * (semantic value * line # * line #)) list
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   552
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   553
	   The parser keeps a queue of (state stack * lexer pair).  A lexer pair
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   554
	 consists of a terminal * value pair and a lexer.  This allows the 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   555
	 parser to reconstruct the states for terminals to the left of a
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   556
	 syntax error, and attempt to make error corrections there.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   557
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   558
	   The queue consists of a pair of lists (x,y).  New additions to
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   559
	 the queue are cons'ed onto y.  The first element of x is the top
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   560
	 of the queue.  If x is nil, then y is reversed and used
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   561
	 in place of x.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   562
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   563
    Algorithm:
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   564
    ----------
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   565
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   566
	* The steady-state parser:  
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   567
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   568
	    This parser keeps the length of the queue of state stacks at
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   569
	a steady state by always removing an element from the front when
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   570
	another element is placed on the end.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   571
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   572
	    It has these arguments:
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   573
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   574
	   stack: current stack
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   575
	   queue: value of the queue
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   576
	   lexPair ((terminal,value),lex stream)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   577
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   578
	When SHIFT is encountered, the state to shift to and the value are
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   579
	are pushed onto the state stack.  The state stack and lexPair are
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   580
	placed on the queue.  The front element of the queue is removed.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   581
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   582
	When REDUCTION is encountered, the rule is applied to the current
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   583
	stack to yield a triple (nonterm,value,new stack).  A new
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   584
	stack is formed by adding (goto(top state of stack,nonterm),value)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   585
	to the stack.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   586
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   587
	When ACCEPT is encountered, the top value from the stack and the
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   588
	lexer are returned.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   589
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   590
	When an ERROR is encountered, fixError is called.  FixError
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   591
	takes the arguments to the parser, fixes the error if possible and
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   592
        returns a new set of arguments.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   593
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   594
	* The distance-parser:
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   595
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   596
	This parser includes an additional argument distance.  It pushes
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   597
	elements on the queue until it has parsed distance tokens, or an
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   598
	ACCEPT or ERROR occurs.  It returns a stack, lexer, the number of
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   599
	tokens left unparsed, a queue, and an action option.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   600
*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   601
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   602
signature FIFO = 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   603
  sig type 'a queue
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   604
      val empty : 'a queue
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   605
      exception Empty
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   606
      val get : 'a queue -> 'a * 'a queue
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   607
      val put : 'a * 'a queue -> 'a queue
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   608
  end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   609
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   610
(* drt (12/15/89) -- the functor should be used in development work, but
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   611
   it wastes space in the release version.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   612
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   613
functor ParserGen(structure LrTable : LR_TABLE
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   614
		  structure Stream : STREAM) : LR_PARSER =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   615
*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   616
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   617
structure LrParser :> LR_PARSER =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   618
   struct
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   619
      structure LrTable = LrTable
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   620
      structure Stream = Stream
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   621
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   622
      fun eqT (LrTable.T i, LrTable.T i') = i = i'
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   623
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   624
      structure Token : TOKEN =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   625
	struct
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   626
	    structure LrTable = LrTable
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   627
	    datatype ('a,'b) token = TOKEN of LrTable.term * ('a * 'b * 'b)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   628
	    val sameToken = fn (TOKEN(t,_),TOKEN(t',_)) => eqT (t,t')
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   629
        end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   630
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   631
      open LrTable
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   632
      open Token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   633
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   634
      val DEBUG1 = false
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   635
      val DEBUG2 = false
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   636
      exception ParseError
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   637
      exception ParseImpossible of int
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   638
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   639
      structure Fifo :> FIFO =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   640
        struct
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   641
	  type 'a queue = ('a list * 'a list)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   642
	  val empty = (nil,nil)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   643
	  exception Empty
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   644
	  fun get(a::x, y) = (a, (x,y))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   645
	    | get(nil, nil) = raise Empty
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   646
	    | get(nil, y) = get(rev y, nil)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   647
 	  fun put(a,(x,y)) = (x,a::y)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   648
        end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   649
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   650
      type ('a,'b) elem = (state * ('a * 'b * 'b))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   651
      type ('a,'b) stack = ('a,'b) elem list
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   652
      type ('a,'b) lexv = ('a,'b) token
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   653
      type ('a,'b) lexpair = ('a,'b) lexv * (('a,'b) lexv Stream.stream)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   654
      type ('a,'b) distanceParse =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   655
		 ('a,'b) lexpair *
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   656
		 ('a,'b) stack * 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   657
		 (('a,'b) stack * ('a,'b) lexpair) Fifo.queue *
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   658
		 int ->
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   659
		   ('a,'b) lexpair *
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   660
		   ('a,'b) stack * 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   661
		   (('a,'b) stack * ('a,'b) lexpair) Fifo.queue *
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   662
		   int *
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   663
		   action option
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   664
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   665
      type ('a,'b) ecRecord =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   666
	 {is_keyword : term -> bool,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   667
          preferred_change : (term list * term list) list,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   668
	  error : string * 'b * 'b -> unit,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   669
	  errtermvalue : term -> 'a,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   670
	  terms : term list,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   671
	  showTerminal : term -> string,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   672
	  noShift : term -> bool}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   673
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   674
      local 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   675
	 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   676
	 val println = fn s => (TextIO.print s; TextIO.print "\n")
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   677
	 val showState = fn (STATE s) => "STATE " ^ (Int.toString s)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   678
      in
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   679
        fun printStack(stack: ('a,'b) stack, n: int) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   680
         case stack
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   681
           of (state,_) :: rest =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   682
                 (TextIO.print("\t" ^ Int.toString n ^ ": ");
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   683
                  println(showState state);
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   684
                  printStack(rest, n+1))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   685
            | nil => ()
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   686
                
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   687
        fun prAction showTerminal
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   688
		 (stack as (state,_) :: _, next as (TOKEN (term,_),_), action) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   689
             (println "Parse: state stack:";
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   690
              printStack(stack, 0);
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   691
              TextIO.print("       state="
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   692
                         ^ showState state	
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   693
                         ^ " next="
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   694
                         ^ showTerminal term
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   695
                         ^ " action="
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   696
                        );
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   697
              case action
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   698
                of SHIFT state => println ("SHIFT " ^ (showState state))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   699
                 | REDUCE i => println ("REDUCE " ^ (Int.toString i))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   700
                 | ERROR => println "ERROR"
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   701
		 | ACCEPT => println "ACCEPT")
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   702
        | prAction _ (_,_,action) = ()
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   703
     end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   704
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   705
    (* ssParse: parser which maintains the queue of (state * lexvalues) in a
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   706
	steady-state.  It takes a table, showTerminal function, saction
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   707
	function, and fixError function.  It parses until an ACCEPT is
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   708
	encountered, or an exception is raised.  When an error is encountered,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   709
	fixError is called with the arguments of parseStep (lexv,stack,and
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   710
	queue).  It returns the lexv, and a new stack and queue adjusted so
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   711
	that the lexv can be parsed *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   712
	
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   713
    val ssParse =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   714
      fn (table,showTerminal,saction,fixError,arg) =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   715
	let val prAction = prAction showTerminal
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   716
	    val action = LrTable.action table
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   717
	    val goto = LrTable.goto table
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   718
	    fun parseStep(args as
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   719
			 (lexPair as (TOKEN (terminal, value as (_,leftPos,_)),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   720
				      lexer
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   721
				      ),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   722
			  stack as (state,_) :: _,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   723
			  queue)) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   724
	      let val nextAction = action (state,terminal)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   725
	          val _ = if DEBUG1 then prAction(stack,lexPair,nextAction)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   726
			  else ()
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   727
	      in case nextAction
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   728
		 of SHIFT s =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   729
		  let val newStack = (s,value) :: stack
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   730
		      val newLexPair = Stream.get lexer
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   731
		      val (_,newQueue) =Fifo.get(Fifo.put((newStack,newLexPair),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   732
							    queue))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   733
		  in parseStep(newLexPair,(s,value)::stack,newQueue)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   734
		  end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   735
		 | REDUCE i =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   736
		     (case saction(i,leftPos,stack,arg)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   737
		      of (nonterm,value,stack as (state,_) :: _) =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   738
		          parseStep(lexPair,(goto(state,nonterm),value)::stack,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   739
				    queue)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   740
		       | _ => raise (ParseImpossible 197))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   741
		 | ERROR => parseStep(fixError args)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   742
		 | ACCEPT => 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   743
			(case stack
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   744
			 of (_,(topvalue,_,_)) :: _ =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   745
				let val (token,restLexer) = lexPair
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   746
				in (topvalue,Stream.cons(token,restLexer))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   747
				end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   748
			  | _ => raise (ParseImpossible 202))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   749
	      end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   750
	    | parseStep _ = raise (ParseImpossible 204)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   751
	in parseStep
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   752
	end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   753
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   754
    (*  distanceParse: parse until n tokens are shifted, or accept or
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   755
	error are encountered.  Takes a table, showTerminal function, and
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   756
	semantic action function.  Returns a parser which takes a lexPair
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   757
	(lex result * lexer), a state stack, a queue, and a distance
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   758
	(must be > 0) to parse.  The parser returns a new lex-value, a stack
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   759
	with the nth token shifted on top, a queue, a distance, and action
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   760
	option. *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   761
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   762
    val distanceParse =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   763
      fn (table,showTerminal,saction,arg) =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   764
	let val prAction = prAction showTerminal
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   765
	    val action = LrTable.action table
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   766
	    val goto = LrTable.goto table
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   767
	    fun parseStep(lexPair,stack,queue,0) = (lexPair,stack,queue,0,NONE)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   768
	      | parseStep(lexPair as (TOKEN (terminal, value as (_,leftPos,_)),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   769
				      lexer
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   770
				     ),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   771
			  stack as (state,_) :: _,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   772
			  queue,distance) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   773
	      let val nextAction = action(state,terminal)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   774
	          val _ = if DEBUG1 then prAction(stack,lexPair,nextAction)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   775
			  else ()
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   776
	      in case nextAction
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   777
		 of SHIFT s =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   778
		  let val newStack = (s,value) :: stack
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   779
		      val newLexPair = Stream.get lexer
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   780
		  in parseStep(newLexPair,(s,value)::stack,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   781
			       Fifo.put((newStack,newLexPair),queue),distance-1)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   782
		  end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   783
		 | REDUCE i =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   784
		    (case saction(i,leftPos,stack,arg)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   785
		      of (nonterm,value,stack as (state,_) :: _) =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   786
		         parseStep(lexPair,(goto(state,nonterm),value)::stack,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   787
				 queue,distance)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   788
		      | _ => raise (ParseImpossible 240))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   789
		 | ERROR => (lexPair,stack,queue,distance,SOME nextAction)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   790
		 | ACCEPT => (lexPair,stack,queue,distance,SOME nextAction)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   791
	      end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   792
	   | parseStep _ = raise (ParseImpossible 242)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   793
	in parseStep : ('_a,'_b) distanceParse 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   794
	end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   795
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   796
(* mkFixError: function to create fixError function which adjusts parser state
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   797
   so that parse may continue in the presence of an error *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   798
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   799
fun mkFixError({is_keyword,terms,errtermvalue,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   800
	      preferred_change,noShift,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   801
	      showTerminal,error,...} : ('_a,'_b) ecRecord,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   802
	     distanceParse : ('_a,'_b) distanceParse,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   803
	     minAdvance,maxAdvance) 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   804
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   805
            (lexv as (TOKEN (term,value as (_,leftPos,_)),_),stack,queue) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   806
    let val _ = if DEBUG2 then
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   807
			error("syntax error found at " ^ (showTerminal term),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   808
			      leftPos,leftPos)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   809
		else ()
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   810
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   811
        fun tokAt(t,p) = TOKEN(t,(errtermvalue t,p,p))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   812
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   813
	val minDelta = 3
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   814
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   815
	(* pull all the state * lexv elements from the queue *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   816
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   817
	val stateList = 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   818
	   let fun f q = let val (elem,newQueue) = Fifo.get q
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   819
			 in elem :: (f newQueue)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   820
			 end handle Fifo.Empty => nil
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   821
	   in f queue
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   822
	   end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   823
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   824
	(* now number elements of stateList, giving distance from
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   825
	   error token *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   826
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   827
	val (_, numStateList) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   828
	      List.foldr (fn (a,(num,r)) => (num+1,(a,num)::r)) (0, []) stateList
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   829
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   830
	(* Represent the set of potential changes as a linked list.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   831
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   832
	   Values of datatype Change hold information about a potential change.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   833
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   834
	   oper = oper to be applied
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   835
	   pos = the # of the element in stateList that would be altered.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   836
	   distance = the number of tokens beyond the error token which the
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   837
	     change allows us to parse.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   838
	   new = new terminal * value pair at that point
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   839
	   orig = original terminal * value pair at the point being changed.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   840
	 *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   841
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   842
	datatype ('a,'b) change = CHANGE of
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   843
	   {pos : int, distance : int, leftPos: 'b, rightPos: 'b,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   844
	    new : ('a,'b) lexv list, orig : ('a,'b) lexv list}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   845
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   846
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   847
         val showTerms = String.concat o map (fn TOKEN(t,_) => " " ^ showTerminal t)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   848
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   849
	 val printChange = fn c =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   850
	  let val CHANGE {distance,new,orig,pos,...} = c
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   851
	  in (TextIO.print ("{distance= " ^ (Int.toString distance));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   852
	      TextIO.print (",orig ="); TextIO.print(showTerms orig);
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   853
	      TextIO.print (",new ="); TextIO.print(showTerms new);
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   854
	      TextIO.print (",pos= " ^ (Int.toString pos));
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   855
	      TextIO.print "}\n")
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   856
	  end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   857
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   858
	val printChangeList = app printChange
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   859
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   860
(* parse: given a lexPair, a stack, and the distance from the error
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   861
   token, return the distance past the error token that we are able to parse.*)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   862
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   863
	fun parse (lexPair,stack,queuePos : int) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   864
	    case distanceParse(lexPair,stack,Fifo.empty,queuePos+maxAdvance+1)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   865
             of (_,_,_,distance,SOME ACCEPT) => 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   866
		        if maxAdvance-distance-1 >= 0 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   867
			    then maxAdvance 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   868
			    else maxAdvance-distance-1
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   869
	      | (_,_,_,distance,_) => maxAdvance - distance - 1
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   870
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   871
(* catList: concatenate results of scanning list *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   872
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   873
	fun catList l f = List.foldr (fn(a,r)=> f a @ r) [] l
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   874
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   875
        fun keywordsDelta new = if List.exists (fn(TOKEN(t,_))=>is_keyword t) new
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   876
	               then minDelta else 0
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   877
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   878
        fun tryChange{lex,stack,pos,leftPos,rightPos,orig,new} =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   879
	     let val lex' = List.foldr (fn (t',p)=>(t',Stream.cons p)) lex new
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   880
		 val distance = parse(lex',stack,pos+length new-length orig)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   881
	      in if distance >= minAdvance + keywordsDelta new 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   882
		   then [CHANGE{pos=pos,leftPos=leftPos,rightPos=rightPos,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   883
				distance=distance,orig=orig,new=new}] 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   884
		   else []
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   885
	     end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   886
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   887
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   888
(* tryDelete: Try to delete n terminals.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   889
              Return single-element [success] or nil.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   890
	      Do not delete unshiftable terminals. *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   891
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   892
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   893
    fun tryDelete n ((stack,lexPair as (TOKEN(term,(_,l,r)),_)),qPos) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   894
	let fun del(0,accum,left,right,lexPair) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   895
	          tryChange{lex=lexPair,stack=stack,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   896
			    pos=qPos,leftPos=left,rightPos=right,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   897
			    orig=rev accum, new=[]}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   898
	      | del(n,accum,left,right,(tok as TOKEN(term,(_,_,r)),lexer)) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   899
		   if noShift term then []
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   900
		   else del(n-1,tok::accum,left,r,Stream.get lexer)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   901
         in del(n,[],l,r,lexPair)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   902
        end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   903
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   904
(* tryInsert: try to insert tokens before the current terminal;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   905
       return a list of the successes  *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   906
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   907
        fun tryInsert((stack,lexPair as (TOKEN(_,(_,l,_)),_)),queuePos) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   908
	       catList terms (fn t =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   909
		 tryChange{lex=lexPair,stack=stack,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   910
			   pos=queuePos,orig=[],new=[tokAt(t,l)],
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   911
			   leftPos=l,rightPos=l})
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   912
			      
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   913
(* trySubst: try to substitute tokens for the current terminal;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   914
       return a list of the successes  *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   915
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   916
        fun trySubst ((stack,lexPair as (orig as TOKEN (term,(_,l,r)),lexer)),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   917
		      queuePos) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   918
	      if noShift term then []
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   919
	      else
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   920
		  catList terms (fn t =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   921
		      tryChange{lex=Stream.get lexer,stack=stack,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   922
				pos=queuePos,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   923
				leftPos=l,rightPos=r,orig=[orig],
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   924
				new=[tokAt(t,r)]})
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   925
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   926
     (* do_delete(toks,lexPair) tries to delete tokens "toks" from "lexPair".
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   927
         If it succeeds, returns SOME(toks',l,r,lp), where
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   928
	     toks' is the actual tokens (with positions and values) deleted,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   929
	     (l,r) are the (leftmost,rightmost) position of toks', 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   930
	     lp is what remains of the stream after deletion 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   931
     *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   932
        fun do_delete(nil,lp as (TOKEN(_,(_,l,_)),_)) = SOME(nil,l,l,lp)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   933
          | do_delete([t],(tok as TOKEN(t',(_,l,r)),lp')) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   934
	       if eqT (t, t')
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   935
		   then SOME([tok],l,r,Stream.get lp')
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   936
                   else NONE
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   937
          | do_delete(t::rest,(tok as TOKEN(t',(_,l,r)),lp')) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   938
	       if eqT (t,t')
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   939
		   then case do_delete(rest,Stream.get lp')
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   940
                         of SOME(deleted,l',r',lp'') =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   941
			       SOME(tok::deleted,l,r',lp'')
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   942
			  | NONE => NONE
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   943
		   else NONE
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   944
			     
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   945
        fun tryPreferred((stack,lexPair),queuePos) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   946
	    catList preferred_change (fn (delete,insert) =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   947
	       if List.exists noShift delete then [] (* should give warning at
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   948
						 parser-generation time *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   949
               else case do_delete(delete,lexPair)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   950
                     of SOME(deleted,l,r,lp) => 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   951
			    tryChange{lex=lp,stack=stack,pos=queuePos,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   952
				      leftPos=l,rightPos=r,orig=deleted,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   953
				      new=map (fn t=>(tokAt(t,r))) insert}
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   954
		      | NONE => [])
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   955
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   956
	val changes = catList numStateList tryPreferred @
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   957
	                catList numStateList tryInsert @
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   958
			  catList numStateList trySubst @
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   959
			    catList numStateList (tryDelete 1) @
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   960
			      catList numStateList (tryDelete 2) @
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   961
			        catList numStateList (tryDelete 3)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   962
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   963
	val findMaxDist = fn l => 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   964
	  List.foldr (fn (CHANGE {distance,...},high) => Int.max(distance,high)) 0 l
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   965
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   966
(* maxDist: max distance past error taken that we could parse *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   967
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   968
	val maxDist = findMaxDist changes
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   969
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   970
(* remove changes which did not parse maxDist tokens past the error token *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   971
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   972
        val changes = catList changes 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   973
	      (fn(c as CHANGE{distance,...}) => 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   974
		  if distance=maxDist then [c] else [])
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   975
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   976
      in case changes 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   977
	  of (l as change :: _) =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   978
	      let fun print_msg (CHANGE {new,orig,leftPos,rightPos,...}) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   979
		  let val s = 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   980
		      case (orig,new)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   981
			  of (_::_,[]) => "deleting " ^ (showTerms orig)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   982
	                   | ([],_::_) => "inserting " ^ (showTerms new)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   983
			   | _ => "replacing " ^ (showTerms orig) ^
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   984
				 " with " ^ (showTerms new)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   985
		  in error ("syntax error: " ^ s,leftPos,rightPos)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   986
		  end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   987
		   
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   988
		  val _ = 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   989
		      (if length l > 1 andalso DEBUG2 then
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   990
			   (TextIO.print "multiple fixes possible; could fix it by:\n";
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   991
			    app print_msg l;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   992
			    TextIO.print "chosen correction:\n")
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   993
		       else ();
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   994
		       print_msg change)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   995
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   996
		  (* findNth: find nth queue entry from the error
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   997
		   entry.  Returns the Nth queue entry and the  portion of
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   998
		   the queue from the beginning to the nth-1 entry.  The
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
   999
		   error entry is at the end of the queue.
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1000
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1001
		   Examples:
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1002
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1003
		   queue = a b c d e
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1004
		   findNth 0 = (e,a b c d)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1005
		   findNth 1 =  (d,a b c)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1006
		   *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1007
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1008
		  val findNth = fn n =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1009
		      let fun f (h::t,0) = (h,rev t)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1010
			    | f (h::t,n) = f(t,n-1)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1011
			    | f (nil,_) = let exception FindNth
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1012
					  in raise FindNth
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1013
					  end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1014
		      in f (rev stateList,n)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1015
		      end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1016
		
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1017
		  val CHANGE {pos,orig,new,...} = change
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1018
		  val (last,queueFront) = findNth pos
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1019
		  val (stack,lexPair) = last
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1020
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1021
		  val lp1 = List.foldl(fn (_,(_,r)) => Stream.get r) lexPair orig
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1022
		  val lp2 = List.foldr(fn(t,r)=>(t,Stream.cons r)) lp1 new
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1023
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1024
		  val restQueue = 
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1025
		      Fifo.put((stack,lp2),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1026
			       List.foldl Fifo.put Fifo.empty queueFront)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1027
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1028
		  val (lexPair,stack,queue,_,_) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1029
		      distanceParse(lp2,stack,restQueue,pos)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1030
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1031
	      in (lexPair,stack,queue)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1032
	      end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1033
	| nil => (error("syntax error found at " ^ (showTerminal term),
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1034
			leftPos,leftPos); raise ParseError)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1035
    end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1036
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1037
   val parse = fn {arg,table,lexer,saction,void,lookahead,
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1038
		   ec=ec as {showTerminal,...} : ('_a,'_b) ecRecord} =>
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1039
	let val distance = 15   (* defer distance tokens *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1040
	    val minAdvance = 1  (* must parse at least 1 token past error *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1041
	    val maxAdvance = Int.max(lookahead,0)(* max distance for parse check *)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1042
	    val lexPair = Stream.get lexer
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1043
	    val (TOKEN (_,(_,leftPos,_)),_) = lexPair
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1044
	    val startStack = [(initialState table,(void,leftPos,leftPos))]
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1045
	    val startQueue = Fifo.put((startStack,lexPair),Fifo.empty)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1046
	    val distanceParse = distanceParse(table,showTerminal,saction,arg)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1047
	    val fixError = mkFixError(ec,distanceParse,minAdvance,maxAdvance)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1048
	    val ssParse = ssParse(table,showTerminal,saction,fixError,arg)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1049
	    fun loop (lexPair,stack,queue,_,SOME ACCEPT) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1050
		   ssParse(lexPair,stack,queue)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1051
	      | loop (lexPair,stack,queue,0,_) = ssParse(lexPair,stack,queue)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1052
	      | loop (lexPair,stack,queue,distance,SOME ERROR) =
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1053
		 let val (lexPair,stack,queue) = fixError(lexPair,stack,queue)
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1054
		 in loop (distanceParse(lexPair,stack,queue,distance))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1055
		 end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1056
	      | loop _ = let exception ParseInternal
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1057
			 in raise ParseInternal
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1058
			 end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1059
	in loop (distanceParse(lexPair,startStack,startQueue,distance))
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1060
	end
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1061
 end;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1062
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1063
;
5d9aab0c609c added tptp parser;
sultana
parents:
diff changeset
  1064
print_depth 10;