Agda-2.5.4.1: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.Syntax.Concrete.Operators.Parser.Monad

Description

The parser monad used by the operator parser

Synopsis

Documentation

data MemoKey Source #

Memoisation keys.

Instances
Eq MemoKey Source # 
Instance details

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

Methods

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

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

Show MemoKey Source # 
Instance details

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

Generic MemoKey Source # 
Instance details

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

Associated Types

type Rep MemoKey :: * -> * #

Methods

from :: MemoKey -> Rep MemoKey x #

to :: Rep MemoKey x -> MemoKey #

Hashable MemoKey Source # 
Instance details

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

Methods

hashWithSalt :: Int -> MemoKey -> Int

hash :: MemoKey -> Int

type Rep MemoKey Source # 
Instance details

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

type Rep MemoKey = D1 (MetaData "MemoKey" "Agda.Syntax.Concrete.Operators.Parser.Monad" "Agda-2.5.4.1-DCwfU9KUJFOKGtr3wTwnOb" 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 :: * -> *) :+: (C1 (MetaCons "AppK" PrefixI False) (U1 :: * -> *) :+: C1 (MetaCons "NonfixK" PrefixI False) (U1 :: * -> *))))

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

The parser monad.

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

memoiseIfPrinting :: MemoKey -> Parser tok tok -> Parser tok tok Source #

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 Source #

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