DDC.Source.Tetra.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

Modules

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

Parse a source tetra 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 :: Eq (Tok n) => ParsecT [Token (Tok n)] (ParserState (Tok n)) Identity n

Parse a constructor name.

pLit :: Eq (Tok n) => ParsecT [Token (Tok n)] (ParserState (Tok n)) Identity n

Parse a literal.

Variables

pBinder :: (Ord n, Eq (Tok n)) => ParsecT [Token (Tok n)] (ParserState (Tok n)) Identity (Binder n)

Parse a binder.

pIndex :: Eq (Tok n) => ParsecT [Token (Tok n)] (ParserState (Tok n)) Identity Int

Parse a deBruijn index.

pVar :: Eq (Tok n) => ParsecT [Token (Tok n)] (ParserState (Tok n)) Identity n

Parse a variable.

pName :: Eq (Tok n) => ParsecT [Token (Tok n)] (ParserState (Tok n)) Identity 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.