- MkParameters : (Tok : Type) ->
(Toks : Nat ->
Type) ->
(recordToken : Tok ->
m ()) ->
Parameters m
- m
is the monad the parser uses.
- Tok
Type of tokens
- Toks
Type of sized input (~ Vec Tok)
- recordToken
The action allowing us to track consumed tokens
- MkParser : (runParser : LTE m
n ->
Toks p
m ->
mn (Success (Toks p)
a
m)) ->
Parser mn
p
a
n
- mn
the monad used for parsing
- p
the parameters
- a
the type of value produced
- n
an upper bound on the size of the inputs it can deal with
- MkTPT : (runTPT : StateT (Position,
List an)
(ResultT e
m)
a) ->
TParsecT e
an
m
a
- e
the errors the parser may raise
- an
the annotations the user can put on subparses
- m
the monad the transformer acts upon
- a
the type of values it returns
- record Parameters m
A parser is parametrised by some types and type constructors.
They are grouped in a Parameters record.
- m
is the monad the parser uses.
- MkParameters : (Tok : Type) ->
(Toks : Nat ->
Type) ->
(recordToken : Tok ->
m ()) ->
Parameters m
- m
is the monad the parser uses.
- Tok
Type of tokens
- Toks
Type of sized input (~ Vec Tok)
- recordToken
The action allowing us to track consumed tokens
- Tok : (rec : Parameters m) ->
Type
Type of tokens
- Toks : (rec : Parameters m) ->
Nat ->
Type
Type of sized input (~ Vec Tok)
- recordToken : (rec : Parameters m) ->
Tok rec ->
m ()
The action allowing us to track consumed tokens
- record Parser mn p a n
A parser is the ability to, given an input, return a computation for
a success.
- mn
the monad used for parsing
- p
the parameters
- a
the type of value produced
- n
an upper bound on the size of the inputs it can deal with
- MkParser : (runParser : LTE m
n ->
Toks p
m ->
mn (Success (Toks p)
a
m)) ->
Parser mn
p
a
n
- mn
the monad used for parsing
- p
the parameters
- a
the type of value produced
- n
an upper bound on the size of the inputs it can deal with
- runParser : (rec : Parser mn
p
a
n) ->
LTE m
n ->
Toks p
m ->
mn (Success (Toks p)
a
m)
- TParsecM : (e : Type) ->
(an : Type) ->
Type ->
Type
- record TParsecT e an m a
TParsecT is the monad transformer one would typically use when defining
an instrumented parser
- e
the errors the parser may raise
- an
the annotations the user can put on subparses
- m
the monad the transformer acts upon
- a
the type of values it returns
- MkTPT : (runTPT : StateT (Position,
List an)
(ResultT e
m)
a) ->
TParsecT e
an
m
a
- e
the errors the parser may raise
- an
the annotations the user can put on subparses
- m
the monad the transformer acts upon
- a
the type of values it returns
- runTPT : (rec : TParsecT e
an
m
a) ->
StateT (Position,
List an)
(ResultT e
m)
a
- TParsecU : Type ->
Type
- chars : Monad m =>
Parameters (TParsecT e
a
m)
Specialized versions of Parameters and TParsecT for common use cases
- commit : Functor mn =>
All (Parser (TParsecT e
an
mn)
p
a :->
Parser (TParsecT e
an
mn)
p
a)
- commitT : Functor m =>
TParsecT e
a
m
x ->
TParsecT e
a
m
x
Commiting to a branch makes all the failures in that branch hard failures
that we cannot recover from
- getAnnotations : Monad m =>
TParsecT e
a
m
(List a)
- getPosition : Monad m =>
TParsecT e
a
m
Position
- recordChar : Monad m =>
Char ->
TParsecT e
a
m
()
- sizedtok : (tok : Type) ->
Parameters TParsecU
- withAnnotation : Monad m =>
a ->
TParsecT e
a
m
x ->
TParsecT e
a
m
x