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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Concrete.Operators.Parser.Monad

Description

The parser monad used by the operator parser

Synopsis

- data MemoKey
  - = NodeK PrecedenceKey
  - | PostLeftsK PrecedenceKey
  - | PreRightsK PrecedenceKey
  - | TopK
  - | AppK
  - | NonfixK
- type PrecedenceKey = Either PrecedenceLevel PrecedenceLevel
- type Parser tok a = Parser MemoKey tok (MaybePlaceholder tok) a
- parse :: 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

data MemoKey Source #

Memoisation keys.

Constructors

NodeK PrecedenceKey |
PostLeftsK PrecedenceKey |
PreRightsK PrecedenceKey |
TopK |
AppK |
NonfixK |

#### Instances

Instances details

Generic MemoKey Source # |

Instance details

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

Associated Types

type Rep MemoKey |

Instance details

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

type Rep MemoKey = D1 ('MetaData "MemoKey" "Agda.Syntax.Concrete.Operators.Parser.Monad" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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))))

Methods

from :: MemoKey -> Rep MemoKey x Source #

to :: Rep MemoKey x -> MemoKey Source #

Show MemoKey Source # |
Instance details Defined in Agda.Syntax.Concrete.Operators.Parser.Monad Methods showsPrec :: Int -> MemoKey -> ShowS Source # show :: MemoKey -> String Source # showList :: [MemoKey] -> ShowS Source #
Eq MemoKey Source # |
Instance details Defined in Agda.Syntax.Concrete.Operators.Parser.Monad Methods (==) :: MemoKey -> MemoKey -> Bool Source # (/=) :: MemoKey -> MemoKey -> Bool Source #
Hashable MemoKey Source # |
Instance details Defined in Agda.Syntax.Concrete.Operators.Parser.Monad Methods hashWithSalt :: Int -> MemoKey -> Int Source # hash :: MemoKey -> Int Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

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

The parser monad.

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