Agda-2.5.2: 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 #

Memoisation keys.

Instances

Eq MemoKey # 

Methods

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

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

Show MemoKey # 
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 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.

token :: Parser tok (MaybePlaceholder tok) #

Parses a single token.

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

Parses a token satisfying the given predicate.

tok :: (Eq tok, Show tok) => MaybePlaceholder tok -> Parser tok (MaybePlaceholder tok) #

Parses a given token.

annotate :: (Doc -> Doc) -> Parser tok a -> Parser tok a #

Uses the given function to modify the printed representation (if any) of the given parser.

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.