Safe Haskell | None |
---|---|
Language | Haskell2010 |
Agda.Syntax.Concrete.Operators.Parser.Monad
Description
The parser monad used by the operator parser
Synopsis
- data MemoKey
- = NodeK (Either Integer Integer)
- | PostLeftsK (Either Integer Integer)
- | PreRightsK (Either Integer Integer)
- | TopK
- | AppK
- | NonfixK
- type Parser tok a = Parser MemoKey tok (MaybePlaceholder tok) a
- parse :: forall tok a. Parser tok a -> [MaybePlaceholder tok] -> [a]
- sat' :: (MaybePlaceholder tok -> Maybe a) -> Parser tok a
- sat :: (MaybePlaceholder tok -> Bool) -> Parser tok (MaybePlaceholder tok)
- doc :: Doc -> Parser tok a -> Parser tok a
- memoise :: MemoKey -> Parser tok tok -> Parser tok tok
- memoiseIfPrinting :: MemoKey -> Parser tok tok -> Parser tok tok
- grammar :: Parser tok a -> Doc
Documentation
Memoisation keys.
Constructors
NodeK (Either Integer Integer) | |
PostLeftsK (Either Integer Integer) | |
PreRightsK (Either Integer Integer) | |
TopK | |
AppK | |
NonfixK |
Instances
Eq MemoKey Source # | |
Show MemoKey Source # | |
Generic MemoKey Source # | |
Hashable MemoKey Source # | |
Defined in Agda.Syntax.Concrete.Operators.Parser.Monad | |
type Rep MemoKey Source # | |
Defined in Agda.Syntax.Concrete.Operators.Parser.Monad type Rep MemoKey = D1 (MetaData "MemoKey" "Agda.Syntax.Concrete.Operators.Parser.Monad" "Agda-2.6.0.1-B0t7sLPZhcP4jvj0wGvNPO" False) ((C1 (MetaCons "NodeK" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Either Integer Integer))) :+: (C1 (MetaCons "PostLeftsK" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Either Integer Integer))) :+: C1 (MetaCons "PreRightsK" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 (Either Integer Integer))))) :+: (C1 (MetaCons "TopK" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "AppK" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "NonfixK" PrefixI False) (U1 :: Type -> Type)))) |
parse :: forall tok a. Parser tok a -> [MaybePlaceholder tok] -> [a] Source #
Runs the parser.
sat' :: (MaybePlaceholder tok -> Maybe a) -> Parser tok a Source #
Parses a token satisfying the given predicate. The computed value is returned.
sat :: (MaybePlaceholder tok -> Bool) -> Parser tok (MaybePlaceholder tok) Source #
Parses a token satisfying the given predicate.
doc :: Doc -> Parser tok a -> Parser tok a Source #
Uses the given document as the printed representation of the
given parser. The document's precedence is taken to be atomP
.
memoise :: MemoKey -> Parser tok tok -> Parser tok tok Source #
Memoises the given parser.
Every memoised parser must be annotated with a unique key. (Parametrised parsers must use distinct keys for distinct inputs.)