DDC.Core.Parser

Core language parser.

Documentation

type Parser n a = Parser (Tok n) a

A parser of core language tokens.

Modules

pModule :: (Ord n, Pretty n) => Parser n (Module () n)

Parse a core module.

Expressions

pExp :: Ord n => Parser n (Exp () n)

Parse a core language expression.

pExpApp :: Ord n => Parser n (Exp () n)

pExpAtom :: Ord n => Parser n (Exp () n)

Parse a variable, constructor or parenthesised expression.

Types

pType :: Ord n => Parser n (Type n)

Parse a type.

pTypeApp :: Ord n => Parser n (Type n)

Parse a type application.

pTypeAtom :: Ord n => Parser n (Type n)

Parse a variable, constructor or parenthesised type.

Witnesses

pWitness :: Ord n => Parser n (Witness n)

Parse a witness expression.

pWitnessApp :: Ord n => Parser n (Witness n)

Parse a witness application.

pWitnessAtom :: Ord n => Parser n (Witness n)

Parse a variable, constructor or parenthesised witness.

Constructors

pCon :: Parser n n

Parse a constructor name.

pLit :: Parser n n

Parse a literal

Variables

pBinder :: Ord n => Parser n (Binder n)

Parse a binder.

pIndex :: Parser n Int

Parse a deBruijn index

pVar :: Parser n n

Parse a variable.

pName :: Parser n n

Parse a constructor or variable name.

Raw Tokens

pTok :: TokAtom -> Parser n ()

Parse an atomic token.

pTokAs :: TokAtom -> a -> Parser n a

Parse an atomic token and return some value.