DDC.Core.Parser

Core language parser.

Documentation

type Parser n a = Parser (Tok n) a

A parser of core language tokens.

data Context

Configuration and information from the context. Used for context sensitive parsing.

Constructors

Context

Fields

contextTrackedEffects :: Bool

contextTrackedClosures :: Bool

contextFunctionalEffects :: Bool

contextFunctionalClosures :: Bool

contextOfProfile :: Profile n -> Context

Slurp an initital Context from a Profile

Modules

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

Parse a core module.

Expressions

pExp :: Ord n => Context -> Parser n (Exp SourcePos n)

Parse a core language expression.

pExpApp :: Ord n => Context -> Parser n (Exp SourcePos n)

pExpAtom :: Ord n => Context -> Parser n (Exp SourcePos n)

Parse a variable, constructor or parenthesised expression.

Types

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

Parse a type.

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

Parse a type application.

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

Parse a variable, constructor or parenthesised type.

Witnesses

pWitness :: Ord n => Context -> Parser n (Witness SourcePos n)

Parse a witness expression.

pWitnessApp :: Ord n => Context -> Parser n (Witness SourcePos n)

Parse a witness application.

pWitnessAtom :: Ord n => Context -> Parser n (Witness SourcePos 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.