diff -r 5d9aab0c609c -r 6431a93ffeb6 src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/base.sig --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/base.sig Fri Mar 09 15:39:00 2012 +0000 @@ -0,0 +1,299 @@ +(* ML-Yacc Parser Generator (c) 1989 Andrew W. Appel, David R. Tarditi *) + +(* base.sig: Base signature file for SML-Yacc. This file contains signatures + that must be loaded before any of the files produced by ML-Yacc are loaded +*) + +(* STREAM: signature for a lazy stream.*) + +signature STREAM = + sig type 'xa stream + val streamify : (unit -> '_a) -> '_a stream + val cons : '_a * '_a stream -> '_a stream + val get : '_a stream -> '_a * '_a stream + end + +(* LR_TABLE: signature for an LR Table. + + The list of actions and gotos passed to mkLrTable must be ordered by state + number. The values for state 0 are the first in the list, the values for + state 1 are next, etc. +*) + +signature LR_TABLE = + sig + datatype ('a,'b) pairlist = EMPTY | PAIR of 'a * 'b * ('a,'b) pairlist + datatype state = STATE of int + datatype term = T of int + datatype nonterm = NT of int + datatype action = SHIFT of state + | REDUCE of int + | ACCEPT + | ERROR + type table + + val numStates : table -> int + val numRules : table -> int + val describeActions : table -> state -> + (term,action) pairlist * action + val describeGoto : table -> state -> (nonterm,state) pairlist + val action : table -> state * term -> action + val goto : table -> state * nonterm -> state + val initialState : table -> state + exception Goto of state * nonterm + + val mkLrTable : {actions : ((term,action) pairlist * action) array, + gotos : (nonterm,state) pairlist array, + numStates : int, numRules : int, + initialState : state} -> table + end + +(* TOKEN: signature revealing the internal structure of a token. This signature + TOKEN distinct from the signature {parser name}_TOKENS produced by ML-Yacc. + The {parser name}_TOKENS structures contain some types and functions to + construct tokens from values and positions. + + The representation of token was very carefully chosen here to allow the + polymorphic parser to work without knowing the types of semantic values + or line numbers. + + This has had an impact on the TOKENS structure produced by SML-Yacc, which + is a structure parameter to lexer functors. We would like to have some + type 'a token which functions to construct tokens would create. A + constructor function for a integer token might be + + INT: int * 'a * 'a -> 'a token. + + This is not possible because we need to have tokens with the representation + given below for the polymorphic parser. + + Thus our constructur functions for tokens have the form: + + INT: int * 'a * 'a -> (svalue,'a) token + + This in turn has had an impact on the signature that lexers for SML-Yacc + must match and the types that a user must declare in the user declarations + section of lexers. +*) + +signature TOKEN = + sig + structure LrTable : LR_TABLE + datatype ('a,'b) token = TOKEN of LrTable.term * ('a * 'b * 'b) + val sameToken : ('a,'b) token * ('a,'b) token -> bool + end + +(* LR_PARSER: signature for a polymorphic LR parser *) + +signature LR_PARSER = + sig + structure Stream: STREAM + structure LrTable : LR_TABLE + structure Token : TOKEN + + sharing LrTable = Token.LrTable + + exception ParseError + + val parse : {table : LrTable.table, + lexer : ('_b,'_c) Token.token Stream.stream, + arg: 'arg, + saction : int * + '_c * + (LrTable.state * ('_b * '_c * '_c)) list * + 'arg -> + LrTable.nonterm * + ('_b * '_c * '_c) * + ((LrTable.state *('_b * '_c * '_c)) list), + void : '_b, + ec : { is_keyword : LrTable.term -> bool, + noShift : LrTable.term -> bool, + preferred_change : (LrTable.term list * LrTable.term list) list, + errtermvalue : LrTable.term -> '_b, + showTerminal : LrTable.term -> string, + terms: LrTable.term list, + error : string * '_c * '_c -> unit + }, + lookahead : int (* max amount of lookahead used in *) + (* error correction *) + } -> '_b * + (('_b,'_c) Token.token Stream.stream) + end + +(* LEXER: a signature that most lexers produced for use with SML-Yacc's + output will match. The user is responsible for declaring type token, + type pos, and type svalue in the UserDeclarations section of a lexer. + + Note that type token is abstract in the lexer. This allows SML-Yacc to + create a TOKENS signature for use with lexers produced by ML-Lex that + treats the type token abstractly. Lexers that are functors parametrized by + a Tokens structure matching a TOKENS signature cannot examine the structure + of tokens. +*) + +signature LEXER = + sig + structure UserDeclarations : + sig + type ('a,'b) token + type pos + type svalue + end + val makeLexer : (int -> string) -> unit -> + (UserDeclarations.svalue,UserDeclarations.pos) UserDeclarations.token + end + +(* ARG_LEXER: the %arg option of ML-Lex allows users to produce lexers which + also take an argument before yielding a function from unit to a token +*) + +signature ARG_LEXER = + sig + structure UserDeclarations : + sig + type ('a,'b) token + type pos + type svalue + type arg + end + val makeLexer : (int -> string) -> UserDeclarations.arg -> unit -> + (UserDeclarations.svalue,UserDeclarations.pos) UserDeclarations.token + end + +(* PARSER_DATA: the signature of ParserData structures in {parser name}LrValsFun + produced by SML-Yacc. All such structures match this signature. + + The {parser name}LrValsFun produces a structure which contains all the values + except for the lexer needed to call the polymorphic parser mentioned + before. + +*) + +signature PARSER_DATA = + sig + (* the type of line numbers *) + + type pos + + (* the type of semantic values *) + + type svalue + + (* the type of the user-supplied argument to the parser *) + type arg + + (* the intended type of the result of the parser. This value is + produced by applying extract from the structure Actions to the + final semantic value resultiing from a parse. + *) + + type result + + structure LrTable : LR_TABLE + structure Token : TOKEN + sharing Token.LrTable = LrTable + + (* structure Actions contains the functions which mantain the + semantic values stack in the parser. Void is used to provide + a default value for the semantic stack. + *) + + structure Actions : + sig + val actions : int * pos * + (LrTable.state * (svalue * pos * pos)) list * arg-> + LrTable.nonterm * (svalue * pos * pos) * + ((LrTable.state *(svalue * pos * pos)) list) + val void : svalue + val extract : svalue -> result + end + + (* structure EC contains information used to improve error + recovery in an error-correcting parser *) + + structure EC : + sig + val is_keyword : LrTable.term -> bool + val noShift : LrTable.term -> bool + val preferred_change : (LrTable.term list * LrTable.term list) list + val errtermvalue : LrTable.term -> svalue + val showTerminal : LrTable.term -> string + val terms: LrTable.term list + end + + (* table is the LR table for the parser *) + + val table : LrTable.table + end + +(* signature PARSER is the signature that most user parsers created by + SML-Yacc will match. +*) + +signature PARSER = + sig + structure Token : TOKEN + structure Stream : STREAM + exception ParseError + + (* type pos is the type of line numbers *) + + type pos + + (* type result is the type of the result from the parser *) + + type result + + (* the type of the user-supplied argument to the parser *) + type arg + + (* type svalue is the type of semantic values for the semantic value + stack + *) + + type svalue + + (* val makeLexer is used to create a stream of tokens for the parser *) + + val makeLexer : (int -> string) -> + (svalue,pos) Token.token Stream.stream + + (* val parse takes a stream of tokens and a function to print + errors and returns a value of type result and a stream containing + the unused tokens + *) + + val parse : int * ((svalue,pos) Token.token Stream.stream) * + (string * pos * pos -> unit) * arg -> + result * (svalue,pos) Token.token Stream.stream + + val sameToken : (svalue,pos) Token.token * (svalue,pos) Token.token -> + bool + end + +(* signature ARG_PARSER is the signature that will be matched by parsers whose + lexer takes an additional argument. +*) + +signature ARG_PARSER = + sig + structure Token : TOKEN + structure Stream : STREAM + exception ParseError + + type arg + type lexarg + type pos + type result + type svalue + + val makeLexer : (int -> string) -> lexarg -> + (svalue,pos) Token.token Stream.stream + val parse : int * ((svalue,pos) Token.token Stream.stream) * + (string * pos * pos -> unit) * arg -> + result * (svalue,pos) Token.token Stream.stream + + val sameToken : (svalue,pos) Token.token * (svalue,pos) Token.token -> + bool + end +