ModuleAgda-2.7.0.1Haskell2010

Agda.Syntax.Concrete.Operators.Parser.Monad

The parser monad used by the operator parser

datadata MemoKey

Memoisation keys.

Instances5Eq, Show, Generic, Hashable, Rep

Eq MemoKeyDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Operators.Parser.Monad
Show MemoKeyDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Operators.Parser.Monad
Generic MemoKeyDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Operators.Parser.Monad
Hashable MemoKeyDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Operators.Parser.Monad
type Rep MemoKey = D1 ('MetaData "MemoKey" "Agda.Syntax.Concrete.Operators.Parser.Monad" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" 'False) ((C1 ('MetaCons "NodeK" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PrecedenceKey)) :+: (C1 ('MetaCons "PostLeftsK" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PrecedenceKey)) :+: C1 ('MetaCons "PreRightsK" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PrecedenceKey)))) :+: (C1 ('MetaCons "TopK" 'PrefixI 'False) U1 :+: (C1 ('MetaCons "AppK" 'PrefixI 'False) U1 :+: C1 ('MetaCons "NonfixK" 'PrefixI 'False) U1)))Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Operators.Parser.Monad

typetype PrecedenceKey = Either PrecedenceLevel PrecedenceLevel

typetype Parser tok a = Parser MemoKey tok (MaybePlaceholder tok) a

The parser monad.

valueparse :: Parser tok a -> [MaybePlaceholder tok] -> [a]

Runs the parser.

valuesat' :: (MaybePlaceholder tok -> Maybe a) -> Parser tok a

Parses a token satisfying the given predicate. The computed value is returned.

valuesat :: (MaybePlaceholder tok -> Bool) -> Parser tok (MaybePlaceholder tok)

Parses a token satisfying the given predicate.

valuedoc :: Doc -> Parser tok a -> Parser tok a

Uses the given document as the printed representation of the given parser. The document's precedence is taken to be atomP.

valuememoise :: MemoKey -> Parser tok tok -> Parser tok tok

Memoises the given parser.

Every memoised parser must be annotated with a unique key. (Parametrised parsers must use distinct keys for distinct inputs.)

valuememoiseIfPrinting :: MemoKey -> Parser tok tok -> Parser tok tok

Memoises the given parser, but only if printing, not if parsing.

Every memoised parser must be annotated with a unique key. (Parametrised parsers must use distinct keys for distinct inputs.)

valuegrammar :: Parser tok a -> Doc

Tries to print the parser, or returns empty, depending on the implementation. This function might not terminate.