--- a/src/HOL/TPTP/TPTP_Parser/ml_yacc_lib.ML Thu Dec 31 20:40:28 2015 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/ml_yacc_lib.ML Thu Dec 31 20:57:00 2015 +0100
@@ -58,29 +58,29 @@
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
+ 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
+ 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
@@ -97,14 +97,14 @@
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.
+ 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
+ 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
@@ -113,46 +113,46 @@
signature TOKEN =
sig
- structure LrTable : LR_TABLE
+ structure LrTable : LR_TABLE
datatype ('a,'b) token = TOKEN of LrTable.term * ('a * 'b * 'b)
- val sameToken : ('a,'b) token * ('a,'b) token -> bool
+ 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
+ structure Stream: STREAM
+ structure LrTable : LR_TABLE
+ structure Token : TOKEN
- sharing LrTable = Token.LrTable
+ sharing LrTable = Token.LrTable
- exception ParseError
+ 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)
+ 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
@@ -169,12 +169,12 @@
signature LEXER =
sig
structure UserDeclarations :
- sig
- type ('a,'b) token
- type pos
- type svalue
- end
- val makeLexer : (int -> string) -> unit ->
+ sig
+ type ('a,'b) token
+ type pos
+ type svalue
+ end
+ val makeLexer : (int -> string) -> unit ->
(UserDeclarations.svalue,UserDeclarations.pos) UserDeclarations.token
end
@@ -185,13 +185,13 @@
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 ->
+ 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
@@ -208,57 +208,57 @@
sig
(* the type of line numbers *)
- type pos
+ type pos
- (* the type of semantic values *)
+ (* the type of semantic values *)
- type svalue
+ type svalue
(* the type of the user-supplied argument to the parser *)
- type arg
+ 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.
- *)
+ (* 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
+ type result
- structure LrTable : LR_TABLE
- structure Token : TOKEN
- sharing Token.LrTable = LrTable
+ 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 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 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 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
+ 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 *)
+ (* table is the LR table for the parser *)
- val table : LrTable.table
+ val table : LrTable.table
end
(* signature PARSER is the signature that most user parsers created by
@@ -268,42 +268,42 @@
signature PARSER =
sig
structure Token : TOKEN
- structure Stream : STREAM
- exception ParseError
+ structure Stream : STREAM
+ exception ParseError
- (* type pos is the type of line numbers *)
+ (* type pos is the type of line numbers *)
- type pos
+ type pos
- (* type result is the type of the result from the parser *)
+ (* type result is the type of the result from the parser *)
- type result
+ 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 arg
+
+ (* type svalue is the type of semantic values for the semantic value
+ stack
+ *)
- type svalue
+ type svalue
- (* val makeLexer is used to create a stream of tokens for the parser *)
+ (* val makeLexer is used to create a stream of tokens for the parser *)
- val makeLexer : (int -> string) ->
- (svalue,pos) Token.token Stream.stream
+ val makeLexer : (int -> string) ->
+ (svalue,pos) Token.token Stream.stream
- (* val parse takes a stream of tokens and a function to TextIO.print
- errors and returns a value of type result and a stream containing
- the unused tokens
- *)
+ (* val parse takes a stream of tokens and a function to TextIO.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 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
+ 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
@@ -313,23 +313,23 @@
signature ARG_PARSER =
sig
structure Token : TOKEN
- structure Stream : STREAM
- exception ParseError
+ structure Stream : STREAM
+ exception ParseError
- type arg
- type lexarg
- type pos
- type result
- type svalue
+ 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 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
+ val sameToken : (svalue,pos) Token.token * (svalue,pos) Token.token ->
+ bool
end
@@ -345,14 +345,14 @@
*)
functor Join(structure Lex : LEXER
- structure ParserData: PARSER_DATA
- structure LrParser : LR_PARSER
- sharing ParserData.LrTable = LrParser.LrTable
- sharing ParserData.Token = LrParser.Token
- sharing type Lex.UserDeclarations.svalue = ParserData.svalue
- sharing type Lex.UserDeclarations.pos = ParserData.pos
- sharing type Lex.UserDeclarations.token = ParserData.Token.token)
- : PARSER =
+ structure ParserData: PARSER_DATA
+ structure LrParser : LR_PARSER
+ sharing ParserData.LrTable = LrParser.LrTable
+ sharing ParserData.Token = LrParser.Token
+ sharing type Lex.UserDeclarations.svalue = ParserData.svalue
+ sharing type Lex.UserDeclarations.pos = ParserData.pos
+ sharing type Lex.UserDeclarations.token = ParserData.Token.token)
+ : PARSER =
struct
structure Token = ParserData.Token
structure Stream = LrParser.Stream
@@ -365,20 +365,20 @@
type svalue = ParserData.svalue
val makeLexer = LrParser.Stream.streamify o Lex.makeLexer
val parse = fn (lookahead,lexer,error,arg) =>
- (fn (a,b) => (ParserData.Actions.extract a,b))
+ (fn (a,b) => (ParserData.Actions.extract a,b))
(LrParser.parse {table = ParserData.table,
- lexer=lexer,
- lookahead=lookahead,
- saction = ParserData.Actions.actions,
- arg=arg,
- void= ParserData.Actions.void,
- ec = {is_keyword = ParserData.EC.is_keyword,
- noShift = ParserData.EC.noShift,
- preferred_change = ParserData.EC.preferred_change,
- errtermvalue = ParserData.EC.errtermvalue,
- error=error,
- showTerminal = ParserData.EC.showTerminal,
- terms = ParserData.EC.terms}}
+ lexer=lexer,
+ lookahead=lookahead,
+ saction = ParserData.Actions.actions,
+ arg=arg,
+ void= ParserData.Actions.void,
+ ec = {is_keyword = ParserData.EC.is_keyword,
+ noShift = ParserData.EC.noShift,
+ preferred_change = ParserData.EC.preferred_change,
+ errtermvalue = ParserData.EC.errtermvalue,
+ error=error,
+ showTerminal = ParserData.EC.showTerminal,
+ terms = ParserData.EC.terms}}
)
val sameToken = Token.sameToken
end
@@ -389,14 +389,14 @@
*)
functor JoinWithArg(structure Lex : ARG_LEXER
- structure ParserData: PARSER_DATA
- structure LrParser : LR_PARSER
- sharing ParserData.LrTable = LrParser.LrTable
- sharing ParserData.Token = LrParser.Token
- sharing type Lex.UserDeclarations.svalue = ParserData.svalue
- sharing type Lex.UserDeclarations.pos = ParserData.pos
- sharing type Lex.UserDeclarations.token = ParserData.Token.token)
- : ARG_PARSER =
+ structure ParserData: PARSER_DATA
+ structure LrParser : LR_PARSER
+ sharing ParserData.LrTable = LrParser.LrTable
+ sharing ParserData.Token = LrParser.Token
+ sharing type Lex.UserDeclarations.svalue = ParserData.svalue
+ sharing type Lex.UserDeclarations.pos = ParserData.pos
+ sharing type Lex.UserDeclarations.token = ParserData.Token.token)
+ : ARG_PARSER =
struct
structure Token = ParserData.Token
structure Stream = LrParser.Stream
@@ -410,22 +410,22 @@
type svalue = ParserData.svalue
val makeLexer = fn s => fn arg =>
- LrParser.Stream.streamify (Lex.makeLexer s arg)
+ LrParser.Stream.streamify (Lex.makeLexer s arg)
val parse = fn (lookahead,lexer,error,arg) =>
- (fn (a,b) => (ParserData.Actions.extract a,b))
+ (fn (a,b) => (ParserData.Actions.extract a,b))
(LrParser.parse {table = ParserData.table,
- lexer=lexer,
- lookahead=lookahead,
- saction = ParserData.Actions.actions,
- arg=arg,
- void= ParserData.Actions.void,
- ec = {is_keyword = ParserData.EC.is_keyword,
- noShift = ParserData.EC.noShift,
- preferred_change = ParserData.EC.preferred_change,
- errtermvalue = ParserData.EC.errtermvalue,
- error=error,
- showTerminal = ParserData.EC.showTerminal,
- terms = ParserData.EC.terms}}
+ lexer=lexer,
+ lookahead=lookahead,
+ saction = ParserData.Actions.actions,
+ arg=arg,
+ void= ParserData.Actions.void,
+ ec = {is_keyword = ParserData.EC.is_keyword,
+ noShift = ParserData.EC.noShift,
+ preferred_change = ParserData.EC.preferred_change,
+ errtermvalue = ParserData.EC.errtermvalue,
+ error=error,
+ showTerminal = ParserData.EC.showTerminal,
+ terms = ParserData.EC.terms}}
)
val sameToken = Token.sameToken
end;
@@ -435,60 +435,60 @@
(* ML-Yacc Parser Generator (c) 1989 Andrew W. Appel, David R. Tarditi *)
structure LrTable : LR_TABLE =
struct
- open Array List
- infix 9 sub
- datatype ('a,'b) pairlist = EMPTY
- | PAIR of 'a * 'b * ('a,'b) pairlist
- datatype term = T of int
- datatype nonterm = NT of int
- datatype state = STATE of int
- datatype action = SHIFT of state
- | REDUCE of int (* rulenum from grammar *)
- | ACCEPT
- | ERROR
- exception Goto of state * nonterm
- type table = {states: int, rules : int,initialState: state,
- action: ((term,action) pairlist * action) array,
- goto : (nonterm,state) pairlist array}
- val numStates = fn ({states,...} : table) => states
- val numRules = fn ({rules,...} : table) => rules
- val describeActions =
- fn ({action,...} : table) =>
- fn (STATE s) => action sub s
- val describeGoto =
- fn ({goto,...} : table) =>
- fn (STATE s) => goto sub s
- fun findTerm (T term,row,default) =
- let fun find (PAIR (T key,data,r)) =
- if key < term then find r
- else if key=term then data
- else default
- | find EMPTY = default
- in find row
- end
- fun findNonterm (NT nt,row) =
- let fun find (PAIR (NT key,data,r)) =
- if key < nt then find r
- else if key=nt then SOME data
- else NONE
- | find EMPTY = NONE
- in find row
- end
- val action = fn ({action,...} : table) =>
- fn (STATE state,term) =>
- let val (row,default) = action sub state
- in findTerm(term,row,default)
- end
- val goto = fn ({goto,...} : table) =>
- fn (a as (STATE state,nonterm)) =>
- case findNonterm(nonterm,goto sub state)
- of SOME state => state
- | NONE => raise (Goto a)
- val initialState = fn ({initialState,...} : table) => initialState
- val mkLrTable = fn {actions,gotos,initialState,numStates,numRules} =>
- ({action=actions,goto=gotos,
- states=numStates,
- rules=numRules,
+ open Array List
+ infix 9 sub
+ datatype ('a,'b) pairlist = EMPTY
+ | PAIR of 'a * 'b * ('a,'b) pairlist
+ datatype term = T of int
+ datatype nonterm = NT of int
+ datatype state = STATE of int
+ datatype action = SHIFT of state
+ | REDUCE of int (* rulenum from grammar *)
+ | ACCEPT
+ | ERROR
+ exception Goto of state * nonterm
+ type table = {states: int, rules : int,initialState: state,
+ action: ((term,action) pairlist * action) array,
+ goto : (nonterm,state) pairlist array}
+ val numStates = fn ({states,...} : table) => states
+ val numRules = fn ({rules,...} : table) => rules
+ val describeActions =
+ fn ({action,...} : table) =>
+ fn (STATE s) => action sub s
+ val describeGoto =
+ fn ({goto,...} : table) =>
+ fn (STATE s) => goto sub s
+ fun findTerm (T term,row,default) =
+ let fun find (PAIR (T key,data,r)) =
+ if key < term then find r
+ else if key=term then data
+ else default
+ | find EMPTY = default
+ in find row
+ end
+ fun findNonterm (NT nt,row) =
+ let fun find (PAIR (NT key,data,r)) =
+ if key < nt then find r
+ else if key=nt then SOME data
+ else NONE
+ | find EMPTY = NONE
+ in find row
+ end
+ val action = fn ({action,...} : table) =>
+ fn (STATE state,term) =>
+ let val (row,default) = action sub state
+ in findTerm(term,row,default)
+ end
+ val goto = fn ({goto,...} : table) =>
+ fn (a as (STATE state,nonterm)) =>
+ case findNonterm(nonterm,goto sub state)
+ of SOME state => state
+ | NONE => raise (Goto a)
+ val initialState = fn ({initialState,...} : table) => initialState
+ val mkLrTable = fn {actions,gotos,initialState,numStates,numRules} =>
+ ({action=actions,goto=gotos,
+ states=numStates,
+ rules=numRules,
initialState=initialState} : table)
end;
@@ -507,7 +507,7 @@
fun get(Unsynchronized.ref(EVAL t)) = t
| get(s as Unsynchronized.ref(UNEVAL f)) =
- let val t = (f(), Unsynchronized.ref(UNEVAL f)) in s := EVAL t; t end
+ let val t = (f(), Unsynchronized.ref(UNEVAL f)) in s := EVAL t; t end
fun streamify f = Unsynchronized.ref(UNEVAL f)
fun cons(a,s) = Unsynchronized.ref(EVAL(a,s))
@@ -522,10 +522,10 @@
routine added to it. The routine used is described in detail in this
article:
- 'A Practical Method for LR and LL Syntactic Error Diagnosis and
- Recovery', by M. Burke and G. Fisher, ACM Transactions on
- Programming Langauges and Systems, Vol. 9, No. 2, April 1987,
- pp. 164-197.
+ 'A Practical Method for LR and LL Syntactic Error Diagnosis and
+ Recovery', by M. Burke and G. Fisher, ACM Transactions on
+ Programming Langauges and Systems, Vol. 9, No. 2, April 1987,
+ pp. 164-197.
This program is an implementation is the partial, deferred method discussed
in the article. The algorithm and data structures used in the program
@@ -541,60 +541,60 @@
Data Structures:
----------------
-
- * The parser:
+
+ * The parser:
- The state stack has the type
+ The state stack has the type
- (state * (semantic value * line # * line #)) list
+ (state * (semantic value * line # * line #)) list
- The parser keeps a queue of (state stack * lexer pair). A lexer pair
- consists of a terminal * value pair and a lexer. This allows the
- parser to reconstruct the states for terminals to the left of a
- syntax error, and attempt to make error corrections there.
+ The parser keeps a queue of (state stack * lexer pair). A lexer pair
+ consists of a terminal * value pair and a lexer. This allows the
+ parser to reconstruct the states for terminals to the left of a
+ syntax error, and attempt to make error corrections there.
- The queue consists of a pair of lists (x,y). New additions to
- the queue are cons'ed onto y. The first element of x is the top
- of the queue. If x is nil, then y is reversed and used
- in place of x.
+ The queue consists of a pair of lists (x,y). New additions to
+ the queue are cons'ed onto y. The first element of x is the top
+ of the queue. If x is nil, then y is reversed and used
+ in place of x.
Algorithm:
----------
- * The steady-state parser:
+ * The steady-state parser:
- This parser keeps the length of the queue of state stacks at
- a steady state by always removing an element from the front when
- another element is placed on the end.
+ This parser keeps the length of the queue of state stacks at
+ a steady state by always removing an element from the front when
+ another element is placed on the end.
- It has these arguments:
+ It has these arguments:
- stack: current stack
- queue: value of the queue
- lexPair ((terminal,value),lex stream)
+ stack: current stack
+ queue: value of the queue
+ lexPair ((terminal,value),lex stream)
- When SHIFT is encountered, the state to shift to and the value are
- are pushed onto the state stack. The state stack and lexPair are
- placed on the queue. The front element of the queue is removed.
+ When SHIFT is encountered, the state to shift to and the value are
+ are pushed onto the state stack. The state stack and lexPair are
+ placed on the queue. The front element of the queue is removed.
- When REDUCTION is encountered, the rule is applied to the current
- stack to yield a triple (nonterm,value,new stack). A new
- stack is formed by adding (goto(top state of stack,nonterm),value)
- to the stack.
+ When REDUCTION is encountered, the rule is applied to the current
+ stack to yield a triple (nonterm,value,new stack). A new
+ stack is formed by adding (goto(top state of stack,nonterm),value)
+ to the stack.
- When ACCEPT is encountered, the top value from the stack and the
- lexer are returned.
+ When ACCEPT is encountered, the top value from the stack and the
+ lexer are returned.
- When an ERROR is encountered, fixError is called. FixError
- takes the arguments to the parser, fixes the error if possible and
+ When an ERROR is encountered, fixError is called. FixError
+ takes the arguments to the parser, fixes the error if possible and
returns a new set of arguments.
- * The distance-parser:
+ * The distance-parser:
- This parser includes an additional argument distance. It pushes
- elements on the queue until it has parsed distance tokens, or an
- ACCEPT or ERROR occurs. It returns a stack, lexer, the number of
- tokens left unparsed, a queue, and an action option.
+ This parser includes an additional argument distance. It pushes
+ elements on the queue until it has parsed distance tokens, or an
+ ACCEPT or ERROR occurs. It returns a stack, lexer, the number of
+ tokens left unparsed, a queue, and an action option.
*)
signature FIFO =
@@ -609,7 +609,7 @@
it wastes space in the release version.
functor ParserGen(structure LrTable : LR_TABLE
- structure Stream : STREAM) : LR_PARSER =
+ structure Stream : STREAM) : LR_PARSER =
*)
structure LrParser :> LR_PARSER =
@@ -620,10 +620,10 @@
fun eqT (LrTable.T i, LrTable.T i') = i = i'
structure Token : TOKEN =
- struct
- structure LrTable = LrTable
- datatype ('a,'b) token = TOKEN of LrTable.term * ('a * 'b * 'b)
- val sameToken = fn (TOKEN(t,_),TOKEN(t',_)) => eqT (t,t')
+ struct
+ structure LrTable = LrTable
+ datatype ('a,'b) token = TOKEN of LrTable.term * ('a * 'b * 'b)
+ val sameToken = fn (TOKEN(t,_),TOKEN(t',_)) => eqT (t,t')
end
open LrTable
@@ -636,13 +636,13 @@
structure Fifo :> FIFO =
struct
- type 'a queue = ('a list * 'a list)
- val empty = (nil,nil)
- exception Empty
- fun get(a::x, y) = (a, (x,y))
- | get(nil, nil) = raise Empty
- | get(nil, y) = get(rev y, nil)
- fun put(a,(x,y)) = (x,a::y)
+ type 'a queue = ('a list * 'a list)
+ val empty = (nil,nil)
+ exception Empty
+ fun get(a::x, y) = (a, (x,y))
+ | get(nil, nil) = raise Empty
+ | get(nil, y) = get(rev y, nil)
+ fun put(a,(x,y)) = (x,a::y)
end
type ('a,'b) elem = (state * ('a * 'b * 'b))
@@ -650,29 +650,29 @@
type ('a,'b) lexv = ('a,'b) token
type ('a,'b) lexpair = ('a,'b) lexv * (('a,'b) lexv Stream.stream)
type ('a,'b) distanceParse =
- ('a,'b) lexpair *
- ('a,'b) stack *
- (('a,'b) stack * ('a,'b) lexpair) Fifo.queue *
- int ->
- ('a,'b) lexpair *
- ('a,'b) stack *
- (('a,'b) stack * ('a,'b) lexpair) Fifo.queue *
- int *
- action option
+ ('a,'b) lexpair *
+ ('a,'b) stack *
+ (('a,'b) stack * ('a,'b) lexpair) Fifo.queue *
+ int ->
+ ('a,'b) lexpair *
+ ('a,'b) stack *
+ (('a,'b) stack * ('a,'b) lexpair) Fifo.queue *
+ int *
+ action option
type ('a,'b) ecRecord =
- {is_keyword : term -> bool,
+ {is_keyword : term -> bool,
preferred_change : (term list * term list) list,
- error : string * 'b * 'b -> unit,
- errtermvalue : term -> 'a,
- terms : term list,
- showTerminal : term -> string,
- noShift : term -> bool}
+ error : string * 'b * 'b -> unit,
+ errtermvalue : term -> 'a,
+ terms : term list,
+ showTerminal : term -> string,
+ noShift : term -> bool}
local
-
- val println = fn s => (TextIO.print s; TextIO.print "\n")
- val showState = fn (STATE s) => "STATE " ^ (Int.toString s)
+
+ val println = fn s => (TextIO.print s; TextIO.print "\n")
+ val showState = fn (STATE s) => "STATE " ^ (Int.toString s)
in
fun printStack(stack: ('a,'b) stack, n: int) =
case stack
@@ -683,11 +683,11 @@
| nil => ()
fun prAction showTerminal
- (stack as (state,_) :: _, next as (TOKEN (term,_),_), action) =
+ (stack as (state,_) :: _, next as (TOKEN (term,_),_), action) =
(println "Parse: state stack:";
printStack(stack, 0);
TextIO.print(" state="
- ^ showState state
+ ^ showState state
^ " next="
^ showTerminal term
^ " action="
@@ -696,206 +696,206 @@
of SHIFT state => println ("SHIFT " ^ (showState state))
| REDUCE i => println ("REDUCE " ^ (Int.toString i))
| ERROR => println "ERROR"
- | ACCEPT => println "ACCEPT")
+ | ACCEPT => println "ACCEPT")
| prAction _ (_,_,action) = ()
end
(* ssParse: parser which maintains the queue of (state * lexvalues) in a
- steady-state. It takes a table, showTerminal function, saction
- function, and fixError function. It parses until an ACCEPT is
- encountered, or an exception is raised. When an error is encountered,
- fixError is called with the arguments of parseStep (lexv,stack,and
- queue). It returns the lexv, and a new stack and queue adjusted so
- that the lexv can be parsed *)
-
+ steady-state. It takes a table, showTerminal function, saction
+ function, and fixError function. It parses until an ACCEPT is
+ encountered, or an exception is raised. When an error is encountered,
+ fixError is called with the arguments of parseStep (lexv,stack,and
+ queue). It returns the lexv, and a new stack and queue adjusted so
+ that the lexv can be parsed *)
+
val ssParse =
fn (table,showTerminal,saction,fixError,arg) =>
- let val prAction = prAction showTerminal
- val action = LrTable.action table
- val goto = LrTable.goto table
- fun parseStep(args as
- (lexPair as (TOKEN (terminal, value as (_,leftPos,_)),
- lexer
- ),
- stack as (state,_) :: _,
- queue)) =
- let val nextAction = action (state,terminal)
- val _ = if DEBUG1 then prAction(stack,lexPair,nextAction)
- else ()
- in case nextAction
- of SHIFT s =>
- let val newStack = (s,value) :: stack
- val newLexPair = Stream.get lexer
- val (_,newQueue) =Fifo.get(Fifo.put((newStack,newLexPair),
- queue))
- in parseStep(newLexPair,(s,value)::stack,newQueue)
- end
- | REDUCE i =>
- (case saction(i,leftPos,stack,arg)
- of (nonterm,value,stack as (state,_) :: _) =>
- parseStep(lexPair,(goto(state,nonterm),value)::stack,
- queue)
- | _ => raise (ParseImpossible 197))
- | ERROR => parseStep(fixError args)
- | ACCEPT =>
- (case stack
- of (_,(topvalue,_,_)) :: _ =>
- let val (token,restLexer) = lexPair
- in (topvalue,Stream.cons(token,restLexer))
- end
- | _ => raise (ParseImpossible 202))
- end
- | parseStep _ = raise (ParseImpossible 204)
- in parseStep
- end
+ let val prAction = prAction showTerminal
+ val action = LrTable.action table
+ val goto = LrTable.goto table
+ fun parseStep(args as
+ (lexPair as (TOKEN (terminal, value as (_,leftPos,_)),
+ lexer
+ ),
+ stack as (state,_) :: _,
+ queue)) =
+ let val nextAction = action (state,terminal)
+ val _ = if DEBUG1 then prAction(stack,lexPair,nextAction)
+ else ()
+ in case nextAction
+ of SHIFT s =>
+ let val newStack = (s,value) :: stack
+ val newLexPair = Stream.get lexer
+ val (_,newQueue) =Fifo.get(Fifo.put((newStack,newLexPair),
+ queue))
+ in parseStep(newLexPair,(s,value)::stack,newQueue)
+ end
+ | REDUCE i =>
+ (case saction(i,leftPos,stack,arg)
+ of (nonterm,value,stack as (state,_) :: _) =>
+ parseStep(lexPair,(goto(state,nonterm),value)::stack,
+ queue)
+ | _ => raise (ParseImpossible 197))
+ | ERROR => parseStep(fixError args)
+ | ACCEPT =>
+ (case stack
+ of (_,(topvalue,_,_)) :: _ =>
+ let val (token,restLexer) = lexPair
+ in (topvalue,Stream.cons(token,restLexer))
+ end
+ | _ => raise (ParseImpossible 202))
+ end
+ | parseStep _ = raise (ParseImpossible 204)
+ in parseStep
+ end
(* distanceParse: parse until n tokens are shifted, or accept or
- error are encountered. Takes a table, showTerminal function, and
- semantic action function. Returns a parser which takes a lexPair
- (lex result * lexer), a state stack, a queue, and a distance
- (must be > 0) to parse. The parser returns a new lex-value, a stack
- with the nth token shifted on top, a queue, a distance, and action
- option. *)
+ error are encountered. Takes a table, showTerminal function, and
+ semantic action function. Returns a parser which takes a lexPair
+ (lex result * lexer), a state stack, a queue, and a distance
+ (must be > 0) to parse. The parser returns a new lex-value, a stack
+ with the nth token shifted on top, a queue, a distance, and action
+ option. *)
val distanceParse =
fn (table,showTerminal,saction,arg) =>
- let val prAction = prAction showTerminal
- val action = LrTable.action table
- val goto = LrTable.goto table
- fun parseStep(lexPair,stack,queue,0) = (lexPair,stack,queue,0,NONE)
- | parseStep(lexPair as (TOKEN (terminal, value as (_,leftPos,_)),
- lexer
- ),
- stack as (state,_) :: _,
- queue,distance) =
- let val nextAction = action(state,terminal)
- val _ = if DEBUG1 then prAction(stack,lexPair,nextAction)
- else ()
- in case nextAction
- of SHIFT s =>
- let val newStack = (s,value) :: stack
- val newLexPair = Stream.get lexer
- in parseStep(newLexPair,(s,value)::stack,
- Fifo.put((newStack,newLexPair),queue),distance-1)
- end
- | REDUCE i =>
- (case saction(i,leftPos,stack,arg)
- of (nonterm,value,stack as (state,_) :: _) =>
- parseStep(lexPair,(goto(state,nonterm),value)::stack,
- queue,distance)
- | _ => raise (ParseImpossible 240))
- | ERROR => (lexPair,stack,queue,distance,SOME nextAction)
- | ACCEPT => (lexPair,stack,queue,distance,SOME nextAction)
- end
- | parseStep _ = raise (ParseImpossible 242)
- in parseStep : ('_a,'_b) distanceParse
- end
+ let val prAction = prAction showTerminal
+ val action = LrTable.action table
+ val goto = LrTable.goto table
+ fun parseStep(lexPair,stack,queue,0) = (lexPair,stack,queue,0,NONE)
+ | parseStep(lexPair as (TOKEN (terminal, value as (_,leftPos,_)),
+ lexer
+ ),
+ stack as (state,_) :: _,
+ queue,distance) =
+ let val nextAction = action(state,terminal)
+ val _ = if DEBUG1 then prAction(stack,lexPair,nextAction)
+ else ()
+ in case nextAction
+ of SHIFT s =>
+ let val newStack = (s,value) :: stack
+ val newLexPair = Stream.get lexer
+ in parseStep(newLexPair,(s,value)::stack,
+ Fifo.put((newStack,newLexPair),queue),distance-1)
+ end
+ | REDUCE i =>
+ (case saction(i,leftPos,stack,arg)
+ of (nonterm,value,stack as (state,_) :: _) =>
+ parseStep(lexPair,(goto(state,nonterm),value)::stack,
+ queue,distance)
+ | _ => raise (ParseImpossible 240))
+ | ERROR => (lexPair,stack,queue,distance,SOME nextAction)
+ | ACCEPT => (lexPair,stack,queue,distance,SOME nextAction)
+ end
+ | parseStep _ = raise (ParseImpossible 242)
+ in parseStep : ('_a,'_b) distanceParse
+ end
(* mkFixError: function to create fixError function which adjusts parser state
so that parse may continue in the presence of an error *)
fun mkFixError({is_keyword,terms,errtermvalue,
- preferred_change,noShift,
- showTerminal,error,...} : ('_a,'_b) ecRecord,
- distanceParse : ('_a,'_b) distanceParse,
- minAdvance,maxAdvance)
+ preferred_change,noShift,
+ showTerminal,error,...} : ('_a,'_b) ecRecord,
+ distanceParse : ('_a,'_b) distanceParse,
+ minAdvance,maxAdvance)
(lexv as (TOKEN (term,value as (_,leftPos,_)),_),stack,queue) =
let val _ = if DEBUG2 then
- error("syntax error found at " ^ (showTerminal term),
- leftPos,leftPos)
- else ()
+ error("syntax error found at " ^ (showTerminal term),
+ leftPos,leftPos)
+ else ()
fun tokAt(t,p) = TOKEN(t,(errtermvalue t,p,p))
- val minDelta = 3
+ val minDelta = 3
- (* pull all the state * lexv elements from the queue *)
+ (* pull all the state * lexv elements from the queue *)
- val stateList =
- let fun f q = let val (elem,newQueue) = Fifo.get q
- in elem :: (f newQueue)
- end handle Fifo.Empty => nil
- in f queue
- end
+ val stateList =
+ let fun f q = let val (elem,newQueue) = Fifo.get q
+ in elem :: (f newQueue)
+ end handle Fifo.Empty => nil
+ in f queue
+ end
- (* now number elements of stateList, giving distance from
- error token *)
+ (* now number elements of stateList, giving distance from
+ error token *)
- val (_, numStateList) =
- List.foldr (fn (a,(num,r)) => (num+1,(a,num)::r)) (0, []) stateList
+ val (_, numStateList) =
+ List.foldr (fn (a,(num,r)) => (num+1,(a,num)::r)) (0, []) stateList
- (* Represent the set of potential changes as a linked list.
+ (* Represent the set of potential changes as a linked list.
- Values of datatype Change hold information about a potential change.
+ Values of datatype Change hold information about a potential change.
- oper = oper to be applied
- pos = the # of the element in stateList that would be altered.
- distance = the number of tokens beyond the error token which the
- change allows us to parse.
- new = new terminal * value pair at that point
- orig = original terminal * value pair at the point being changed.
- *)
+ oper = oper to be applied
+ pos = the # of the element in stateList that would be altered.
+ distance = the number of tokens beyond the error token which the
+ change allows us to parse.
+ new = new terminal * value pair at that point
+ orig = original terminal * value pair at the point being changed.
+ *)
- datatype ('a,'b) change = CHANGE of
- {pos : int, distance : int, leftPos: 'b, rightPos: 'b,
- new : ('a,'b) lexv list, orig : ('a,'b) lexv list}
+ datatype ('a,'b) change = CHANGE of
+ {pos : int, distance : int, leftPos: 'b, rightPos: 'b,
+ new : ('a,'b) lexv list, orig : ('a,'b) lexv list}
val showTerms = String.concat o map (fn TOKEN(t,_) => " " ^ showTerminal t)
- val printChange = fn c =>
- let val CHANGE {distance,new,orig,pos,...} = c
- in (TextIO.print ("{distance= " ^ (Int.toString distance));
- TextIO.print (",orig ="); TextIO.print(showTerms orig);
- TextIO.print (",new ="); TextIO.print(showTerms new);
- TextIO.print (",pos= " ^ (Int.toString pos));
- TextIO.print "}\n")
- end
+ val printChange = fn c =>
+ let val CHANGE {distance,new,orig,pos,...} = c
+ in (TextIO.print ("{distance= " ^ (Int.toString distance));
+ TextIO.print (",orig ="); TextIO.print(showTerms orig);
+ TextIO.print (",new ="); TextIO.print(showTerms new);
+ TextIO.print (",pos= " ^ (Int.toString pos));
+ TextIO.print "}\n")
+ end
- val printChangeList = app printChange
+ val printChangeList = app printChange
(* parse: given a lexPair, a stack, and the distance from the error
token, return the distance past the error token that we are able to parse.*)
- fun parse (lexPair,stack,queuePos : int) =
- case distanceParse(lexPair,stack,Fifo.empty,queuePos+maxAdvance+1)
+ fun parse (lexPair,stack,queuePos : int) =
+ case distanceParse(lexPair,stack,Fifo.empty,queuePos+maxAdvance+1)
of (_,_,_,distance,SOME ACCEPT) =>
- if maxAdvance-distance-1 >= 0
- then maxAdvance
- else maxAdvance-distance-1
- | (_,_,_,distance,_) => maxAdvance - distance - 1
+ if maxAdvance-distance-1 >= 0
+ then maxAdvance
+ else maxAdvance-distance-1
+ | (_,_,_,distance,_) => maxAdvance - distance - 1
(* catList: concatenate results of scanning list *)
- fun catList l f = List.foldr (fn(a,r)=> f a @ r) [] l
+ fun catList l f = List.foldr (fn(a,r)=> f a @ r) [] l
fun keywordsDelta new = if List.exists (fn(TOKEN(t,_))=>is_keyword t) new
- then minDelta else 0
+ then minDelta else 0
fun tryChange{lex,stack,pos,leftPos,rightPos,orig,new} =
- let val lex' = List.foldr (fn (t',p)=>(t',Stream.cons p)) lex new
- val distance = parse(lex',stack,pos+length new-length orig)
- in if distance >= minAdvance + keywordsDelta new
- then [CHANGE{pos=pos,leftPos=leftPos,rightPos=rightPos,
- distance=distance,orig=orig,new=new}]
- else []
- end
+ let val lex' = List.foldr (fn (t',p)=>(t',Stream.cons p)) lex new
+ val distance = parse(lex',stack,pos+length new-length orig)
+ in if distance >= minAdvance + keywordsDelta new
+ then [CHANGE{pos=pos,leftPos=leftPos,rightPos=rightPos,
+ distance=distance,orig=orig,new=new}]
+ else []
+ end
(* tryDelete: Try to delete n terminals.
Return single-element [success] or nil.
- Do not delete unshiftable terminals. *)
+ Do not delete unshiftable terminals. *)
fun tryDelete n ((stack,lexPair as (TOKEN(term,(_,l,r)),_)),qPos) =
- let fun del(0,accum,left,right,lexPair) =
- tryChange{lex=lexPair,stack=stack,
- pos=qPos,leftPos=left,rightPos=right,
- orig=rev accum, new=[]}
- | del(n,accum,left,right,(tok as TOKEN(term,(_,_,r)),lexer)) =
- if noShift term then []
- else del(n-1,tok::accum,left,r,Stream.get lexer)
+ let fun del(0,accum,left,right,lexPair) =
+ tryChange{lex=lexPair,stack=stack,
+ pos=qPos,leftPos=left,rightPos=right,
+ orig=rev accum, new=[]}
+ | del(n,accum,left,right,(tok as TOKEN(term,(_,_,r)),lexer)) =
+ if noShift term then []
+ else del(n-1,tok::accum,left,r,Stream.get lexer)
in del(n,[],l,r,lexPair)
end
@@ -903,159 +903,159 @@
return a list of the successes *)
fun tryInsert((stack,lexPair as (TOKEN(_,(_,l,_)),_)),queuePos) =
- catList terms (fn t =>
- tryChange{lex=lexPair,stack=stack,
- pos=queuePos,orig=[],new=[tokAt(t,l)],
- leftPos=l,rightPos=l})
-
+ catList terms (fn t =>
+ tryChange{lex=lexPair,stack=stack,
+ pos=queuePos,orig=[],new=[tokAt(t,l)],
+ leftPos=l,rightPos=l})
+
(* trySubst: try to substitute tokens for the current terminal;
return a list of the successes *)
fun trySubst ((stack,lexPair as (orig as TOKEN (term,(_,l,r)),lexer)),
- queuePos) =
- if noShift term then []
- else
- catList terms (fn t =>
- tryChange{lex=Stream.get lexer,stack=stack,
- pos=queuePos,
- leftPos=l,rightPos=r,orig=[orig],
- new=[tokAt(t,r)]})
+ queuePos) =
+ if noShift term then []
+ else
+ catList terms (fn t =>
+ tryChange{lex=Stream.get lexer,stack=stack,
+ pos=queuePos,
+ leftPos=l,rightPos=r,orig=[orig],
+ new=[tokAt(t,r)]})
(* do_delete(toks,lexPair) tries to delete tokens "toks" from "lexPair".
If it succeeds, returns SOME(toks',l,r,lp), where
- toks' is the actual tokens (with positions and values) deleted,
- (l,r) are the (leftmost,rightmost) position of toks',
- lp is what remains of the stream after deletion
+ toks' is the actual tokens (with positions and values) deleted,
+ (l,r) are the (leftmost,rightmost) position of toks',
+ lp is what remains of the stream after deletion
*)
fun do_delete(nil,lp as (TOKEN(_,(_,l,_)),_)) = SOME(nil,l,l,lp)
| do_delete([t],(tok as TOKEN(t',(_,l,r)),lp')) =
- if eqT (t, t')
- then SOME([tok],l,r,Stream.get lp')
+ if eqT (t, t')
+ then SOME([tok],l,r,Stream.get lp')
else NONE
| do_delete(t::rest,(tok as TOKEN(t',(_,l,r)),lp')) =
- if eqT (t,t')
- then case do_delete(rest,Stream.get lp')
+ if eqT (t,t')
+ then case do_delete(rest,Stream.get lp')
of SOME(deleted,l',r',lp'') =>
- SOME(tok::deleted,l,r',lp'')
- | NONE => NONE
- else NONE
-
+ SOME(tok::deleted,l,r',lp'')
+ | NONE => NONE
+ else NONE
+
fun tryPreferred((stack,lexPair),queuePos) =
- catList preferred_change (fn (delete,insert) =>
- if List.exists noShift delete then [] (* should give warning at
- parser-generation time *)
+ catList preferred_change (fn (delete,insert) =>
+ if List.exists noShift delete then [] (* should give warning at
+ parser-generation time *)
else case do_delete(delete,lexPair)
of SOME(deleted,l,r,lp) =>
- tryChange{lex=lp,stack=stack,pos=queuePos,
- leftPos=l,rightPos=r,orig=deleted,
- new=map (fn t=>(tokAt(t,r))) insert}
- | NONE => [])
+ tryChange{lex=lp,stack=stack,pos=queuePos,
+ leftPos=l,rightPos=r,orig=deleted,
+ new=map (fn t=>(tokAt(t,r))) insert}
+ | NONE => [])
- val changes = catList numStateList tryPreferred @
- catList numStateList tryInsert @
- catList numStateList trySubst @
- catList numStateList (tryDelete 1) @
- catList numStateList (tryDelete 2) @
- catList numStateList (tryDelete 3)
+ val changes = catList numStateList tryPreferred @
+ catList numStateList tryInsert @
+ catList numStateList trySubst @
+ catList numStateList (tryDelete 1) @
+ catList numStateList (tryDelete 2) @
+ catList numStateList (tryDelete 3)
- val findMaxDist = fn l =>
- List.foldr (fn (CHANGE {distance,...},high) => Int.max(distance,high)) 0 l
+ val findMaxDist = fn l =>
+ List.foldr (fn (CHANGE {distance,...},high) => Int.max(distance,high)) 0 l
(* maxDist: max distance past error taken that we could parse *)
- val maxDist = findMaxDist changes
+ val maxDist = findMaxDist changes
(* remove changes which did not parse maxDist tokens past the error token *)
val changes = catList changes
- (fn(c as CHANGE{distance,...}) =>
- if distance=maxDist then [c] else [])
+ (fn(c as CHANGE{distance,...}) =>
+ if distance=maxDist then [c] else [])
in case changes
- of (l as change :: _) =>
- let fun print_msg (CHANGE {new,orig,leftPos,rightPos,...}) =
- let val s =
- case (orig,new)
- of (_::_,[]) => "deleting " ^ (showTerms orig)
- | ([],_::_) => "inserting " ^ (showTerms new)
- | _ => "replacing " ^ (showTerms orig) ^
- " with " ^ (showTerms new)
- in error ("syntax error: " ^ s,leftPos,rightPos)
- end
-
- val _ =
- (if length l > 1 andalso DEBUG2 then
- (TextIO.print "multiple fixes possible; could fix it by:\n";
- app print_msg l;
- TextIO.print "chosen correction:\n")
- else ();
- print_msg change)
+ of (l as change :: _) =>
+ let fun print_msg (CHANGE {new,orig,leftPos,rightPos,...}) =
+ let val s =
+ case (orig,new)
+ of (_::_,[]) => "deleting " ^ (showTerms orig)
+ | ([],_::_) => "inserting " ^ (showTerms new)
+ | _ => "replacing " ^ (showTerms orig) ^
+ " with " ^ (showTerms new)
+ in error ("syntax error: " ^ s,leftPos,rightPos)
+ end
+
+ val _ =
+ (if length l > 1 andalso DEBUG2 then
+ (TextIO.print "multiple fixes possible; could fix it by:\n";
+ app print_msg l;
+ TextIO.print "chosen correction:\n")
+ else ();
+ print_msg change)
- (* findNth: find nth queue entry from the error
- entry. Returns the Nth queue entry and the portion of
- the queue from the beginning to the nth-1 entry. The
- error entry is at the end of the queue.
+ (* findNth: find nth queue entry from the error
+ entry. Returns the Nth queue entry and the portion of
+ the queue from the beginning to the nth-1 entry. The
+ error entry is at the end of the queue.
- Examples:
+ Examples:
- queue = a b c d e
- findNth 0 = (e,a b c d)
- findNth 1 = (d,a b c)
- *)
+ queue = a b c d e
+ findNth 0 = (e,a b c d)
+ findNth 1 = (d,a b c)
+ *)
- val findNth = fn n =>
- let fun f (h::t,0) = (h,rev t)
- | f (h::t,n) = f(t,n-1)
- | f (nil,_) = let exception FindNth
- in raise FindNth
- end
- in f (rev stateList,n)
- end
-
- val CHANGE {pos,orig,new,...} = change
- val (last,queueFront) = findNth pos
- val (stack,lexPair) = last
+ val findNth = fn n =>
+ let fun f (h::t,0) = (h,rev t)
+ | f (h::t,n) = f(t,n-1)
+ | f (nil,_) = let exception FindNth
+ in raise FindNth
+ end
+ in f (rev stateList,n)
+ end
+
+ val CHANGE {pos,orig,new,...} = change
+ val (last,queueFront) = findNth pos
+ val (stack,lexPair) = last
- val lp1 = List.foldl(fn (_,(_,r)) => Stream.get r) lexPair orig
- val lp2 = List.foldr(fn(t,r)=>(t,Stream.cons r)) lp1 new
+ val lp1 = List.foldl(fn (_,(_,r)) => Stream.get r) lexPair orig
+ val lp2 = List.foldr(fn(t,r)=>(t,Stream.cons r)) lp1 new
- val restQueue =
- Fifo.put((stack,lp2),
- List.foldl Fifo.put Fifo.empty queueFront)
+ val restQueue =
+ Fifo.put((stack,lp2),
+ List.foldl Fifo.put Fifo.empty queueFront)
- val (lexPair,stack,queue,_,_) =
- distanceParse(lp2,stack,restQueue,pos)
+ val (lexPair,stack,queue,_,_) =
+ distanceParse(lp2,stack,restQueue,pos)
- in (lexPair,stack,queue)
- end
- | nil => (error("syntax error found at " ^ (showTerminal term),
- leftPos,leftPos); raise ParseError)
+ in (lexPair,stack,queue)
+ end
+ | nil => (error("syntax error found at " ^ (showTerminal term),
+ leftPos,leftPos); raise ParseError)
end
val parse = fn {arg,table,lexer,saction,void,lookahead,
- ec=ec as {showTerminal,...} : ('_a,'_b) ecRecord} =>
- let val distance = 15 (* defer distance tokens *)
- val minAdvance = 1 (* must parse at least 1 token past error *)
- val maxAdvance = Int.max(lookahead,0)(* max distance for parse check *)
- val lexPair = Stream.get lexer
- val (TOKEN (_,(_,leftPos,_)),_) = lexPair
- val startStack = [(initialState table,(void,leftPos,leftPos))]
- val startQueue = Fifo.put((startStack,lexPair),Fifo.empty)
- val distanceParse = distanceParse(table,showTerminal,saction,arg)
- val fixError = mkFixError(ec,distanceParse,minAdvance,maxAdvance)
- val ssParse = ssParse(table,showTerminal,saction,fixError,arg)
- fun loop (lexPair,stack,queue,_,SOME ACCEPT) =
- ssParse(lexPair,stack,queue)
- | loop (lexPair,stack,queue,0,_) = ssParse(lexPair,stack,queue)
- | loop (lexPair,stack,queue,distance,SOME ERROR) =
- let val (lexPair,stack,queue) = fixError(lexPair,stack,queue)
- in loop (distanceParse(lexPair,stack,queue,distance))
- end
- | loop _ = let exception ParseInternal
- in raise ParseInternal
- end
- in loop (distanceParse(lexPair,startStack,startQueue,distance))
- end
+ ec=ec as {showTerminal,...} : ('_a,'_b) ecRecord} =>
+ let val distance = 15 (* defer distance tokens *)
+ val minAdvance = 1 (* must parse at least 1 token past error *)
+ val maxAdvance = Int.max(lookahead,0)(* max distance for parse check *)
+ val lexPair = Stream.get lexer
+ val (TOKEN (_,(_,leftPos,_)),_) = lexPair
+ val startStack = [(initialState table,(void,leftPos,leftPos))]
+ val startQueue = Fifo.put((startStack,lexPair),Fifo.empty)
+ val distanceParse = distanceParse(table,showTerminal,saction,arg)
+ val fixError = mkFixError(ec,distanceParse,minAdvance,maxAdvance)
+ val ssParse = ssParse(table,showTerminal,saction,fixError,arg)
+ fun loop (lexPair,stack,queue,_,SOME ACCEPT) =
+ ssParse(lexPair,stack,queue)
+ | loop (lexPair,stack,queue,0,_) = ssParse(lexPair,stack,queue)
+ | loop (lexPair,stack,queue,distance,SOME ERROR) =
+ let val (lexPair,stack,queue) = fixError(lexPair,stack,queue)
+ in loop (distanceParse(lexPair,stack,queue,distance))
+ end
+ | loop _ = let exception ParseInternal
+ in raise ParseInternal
+ end
+ in loop (distanceParse(lexPair,startStack,startQueue,distance))
+ end
end;
;