SMR.Source.Parser

Documentation

type Parser s p a = Parser (Located Token) (Expected (Located Token) s p) a

data Config s p

Constructors

Config

Fields

• configReadSym :: Text -> Maybe s
• configReadPrm :: Text -> Maybe p

parseDecls :: Config s p -> [Located Token] -> Either (ParseError (Located Token) (Expected (Located Token) s p)) [Decl s p]

parseExp :: Config s p -> [Located Token] -> Either (ParseError (Located Token) (Expected (Located Token) s p)) (Exp s p)

Parse a complete expression from the given list of tokens.

pDecls :: Config s p -> Parser s p [Decl s p]

pDecl :: Config s p -> Parser s p (Decl s p)

pExp :: Config s p -> Parser s p (Exp s p)

pExpApp :: Config s p -> Parser s p (Exp s p)

Parser for an application.

pExpAtom :: Config s p -> Parser s p (Exp s p)

Parser for an atomic expression.

pParam :: Parser s p Param

Parser for a function parameter.

pTrain :: Config s p -> Parser s p [Car s p]

Parser for a substitution train. The cars are produced in reverse order.

pTrainCar :: Config s p -> Parser s p (Car s p)

Parse a single car in the train.

pCarSimRec :: Config s p -> Parser s p (Car s p)

Parser for a substitution environment.

Snv ::= '[' Bind*, ']'

pBind :: Config s p -> Parser s p (SnvBind s p)

Parser for a binding.

Bind ::= Name '=' Exp | Name ^ Nat '=' Exp

pUps :: Parser s p Ups

Parser for an ups.

Ups ::= '{' Bump*, '}'

pBump :: Parser s p UpsBump

Parser for a bump.

Bump ::= Name : Nat | Name ^ Nat : Nat

pNat :: Parser s p Integer

Parser for a natural number.

pNameOfSpace :: Space -> Parser s p Text

Parser for a name in the given space.

pName :: Parser s p (Space, Text)

Parser for a name of any space.

pEnd :: Parser s p ()

Parser for the end of input token.

pPunc :: Char -> Parser s p ()

Parser for a punctuation character.