Agda.Syntax.Concrete.Operators.Parser.Monad

The parser monad used by the operator parser

Documentation

data MemoKey

Memoisation keys.

Constructors

NodeK (Either Integer Integer)

PostLeftsK (Either Integer Integer)

PreRightsK (Either Integer Integer)

TopK

AppK

NonfixK

Instances

Eq MemoKey

Methods

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

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

Show MemoKey

Methods

showsPrec :: Int -> MemoKey -> ShowS

show :: MemoKey -> String

showList :: [MemoKey] -> ShowS

Generic MemoKey

Associated Types

type Rep MemoKey :: * -> *

Methods

from :: MemoKey -> Rep MemoKey x

to :: Rep MemoKey x -> MemoKey

Hashable MemoKey

Methods

hashWithSalt :: Int -> MemoKey -> Int

hash :: MemoKey -> Int

type Rep MemoKey

type Rep MemoKey = D1 * (MetaData "MemoKey" "Agda.Syntax.Concrete.Operators.Parser.Monad" "Agda-2.5.3-7LzUTyWQOJsDWpvzgqsgqM" False) ((:+:) * ((:+:) * (C1 * (MetaCons "NodeK" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Either Integer Integer)))) ((:+:) * (C1 * (MetaCons "PostLeftsK" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Either Integer Integer)))) (C1 * (MetaCons "PreRightsK" PrefixI False) (S1 * (MetaSel (Nothing Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 * (Either Integer Integer)))))) ((:+:) * (C1 * (MetaCons "TopK" PrefixI False) (U1 *)) ((:+:) * (C1 * (MetaCons "AppK" PrefixI False) (U1 *)) (C1 * (MetaCons "NonfixK" PrefixI False) (U1 *)))))

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.