It would be nice to have:
reLex : (check : q -> Maybe p) -> ∀[ Parser P v ] -> ∀[ Parser Q v ]
where P and Q are essentially the same parameters except that P
has p as the token type while Q has q, which is larger.
My current use case: I want the user to provide a parser munching characters
but I'd like to use it in a context where a lexer has been run and some special
characters have been recognised as special. So I have:
data TOK = A | B | C Char
and I'd like reLex to run a modified view that takes check into account
so that the client's anyTok only succeeds if the TOK has the shape C c.
It would be nice to have:
where
PandQare essentially the same parameters except thatPhas
pas the token type whileQhasq, which is larger.My current use case: I want the user to provide a parser munching characters
but I'd like to use it in a context where a lexer has been run and some special
characters have been recognised as special. So I have:
and I'd like
reLexto run a modifiedviewthat takescheckinto accountso that the client's
anyTokonly succeeds if theTOKhas the shapeC c.