Agda.Syntax.Concrete.Operators.Parser.Monad

The parser monad used by the operator parser

Documentation

data MemoKey

Memoisation keys.

Constructors

NodeK PrecedenceKey

PostLeftsK PrecedenceKey

PreRightsK PrecedenceKey

TopK

AppK

NonfixK

Instances

Generic MemoKey

Defined in Agda.Syntax.Concrete.Operators.Parser.Monad

Associated Types

type Rep MemoKey :: Type -> Type

Methods

from :: MemoKey -> Rep MemoKey x

to :: Rep MemoKey x -> MemoKey

Show MemoKey

Defined in Agda.Syntax.Concrete.Operators.Parser.Monad

Methods

showsPrec :: Int -> MemoKey -> ShowS

show :: MemoKey -> String

showList :: [MemoKey] -> ShowS

Eq MemoKey

Defined in Agda.Syntax.Concrete.Operators.Parser.Monad

Methods

(==) :: MemoKey -> MemoKey -> Bool

(/=) :: MemoKey -> MemoKey -> Bool

Hashable MemoKey

Defined in Agda.Syntax.Concrete.Operators.Parser.Monad

Methods

hashWithSalt :: Int -> MemoKey -> Int

hash :: MemoKey -> Int

type Rep MemoKey

Defined in Agda.Syntax.Concrete.Operators.Parser.Monad

type Rep MemoKey = D1 ('MetaData "MemoKey" "Agda.Syntax.Concrete.Operators.Parser.Monad" "Agda-2.6.3.20230930-inplace" 'False) ((C1 ('MetaCons "NodeK" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PrecedenceKey)) :+: (C1 ('MetaCons "PostLeftsK" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PrecedenceKey)) :+: C1 ('MetaCons "PreRightsK" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PrecedenceKey)))) :+: (C1 ('MetaCons "TopK" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "AppK" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NonfixK" 'PrefixI 'False) (U1 :: Type -> Type))))

type PrecedenceKey = Either PrecedenceLevel PrecedenceLevel

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

The parser monad.

parse :: forall tok a. Parser tok a -> [MaybePlaceholder tok] -> [a]

Runs the parser.

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

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

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

Parses a token satisfying the given predicate.

doc :: 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.

memoise :: 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.)

memoiseIfPrinting :: 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.)

grammar :: Parser tok a -> Doc

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