Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone





data MemoKey Source #


Eq MemoKey Source # 


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

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

Generic MemoKey Source # 

Associated Types

type Rep MemoKey :: * -> * #


from :: MemoKey -> Rep MemoKey x #

to :: Rep MemoKey x -> MemoKey #

Hashable MemoKey Source # 


hashWithSalt :: Int -> MemoKey -> Int #

hash :: MemoKey -> Int #

type Rep MemoKey Source # 
type Rep MemoKey = D1 (MetaData "MemoKey" "Agda.Syntax.Concrete.Operators.Parser" "Agda-" 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 "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 #

sat' :: (e -> Bool) -> Parser e e Source #

data ExprView e Source #


LocalV QName 
WildV e 
OtherV e 
AppV e (NamedArg e) 
OpAppV QName (Set Name) [NamedArg (MaybePlaceholder (OpApp e))]

The QName is possibly ambiguous, but it must correspond to one of the names in the set.

HiddenArgV (Named_ e) 
InstanceArgV (Named_ e) 
LamV [LamBinding] e 
ParenV e 


parse :: IsExpr e => (ParseSections, Parser e a) -> [e] -> [a] Source #

Runs a parser. If sections should be parsed, then identifiers with at least two name parts are split up into multiple tokens, using PositionInName to record the tokens' original positions within their respective identifiers.

Parser combinators

partP :: IsExpr e => [Name] -> RawName -> Parser e Range Source #

Parse a specific identifier as a NamePart

atLeastTwoParts :: IsExpr e => Parser e Name Source #

Parses a split-up, unqualified name consisting of at least two name parts.

The parser does not check that underscores and other name parts alternate. The range of the resulting name is the range of the first name part that is not an underscore.

wildOrUnqualifiedName :: IsExpr e => Parser e (Maybe Name) Source #

Either a wildcard (_), or an unqualified name (possibly containing multiple name parts).

data NK k :: * where Source #

A singleton type for NotationKind (except for the constructor NoNotation).

opP :: forall e k. IsExpr e => ParseSections -> Parser e e -> NewNotation -> NK k -> Parser e (OperatorType k e) Source #

Parse the "operator part" of the given notation.

Normal holes (but not binders) at the beginning and end are ignored.

If the notation does not contain any binders, then a section notation is allowed.

argsP :: IsExpr e => Parser e e -> Parser e [NamedArg e] Source #

appP :: IsExpr e => Parser e e -> Parser e [NamedArg e] -> Parser e e Source #

atomP :: IsExpr e => (QName -> Bool) -> Parser e e Source #