ddc-source-tetra-0.4.3.1: DDC/Source/Tetra/Parser/Exp.hs
{-# LANGUAGE TypeFamilies #-}
-- | Parser for Source Tetra expressions.
module DDC.Source.Tetra.Parser.Exp
( pExp
, pExpAppSP
, pExpAtomSP
, pLetsSP, pClauseSP
, pType
, pTypeApp
, pTypeAtomSP)
where
import DDC.Source.Tetra.Parser.Type
import DDC.Source.Tetra.Parser.Witness
import DDC.Source.Tetra.Parser.Base
import DDC.Source.Tetra.Exp
import DDC.Source.Tetra.Prim as S
import DDC.Core.Lexer.Tokens
import Control.Monad.Except
import Data.Maybe
import qualified DDC.Control.Parser as P
import qualified Data.Text as Text
type SP = SourcePos
-- Exp --------------------------------------------------------------------------------------------
pExp :: Parser Exp
pExp = fmap snd pExpWhereSP
-- An expression that may have a trailing where clause.
pExpWhereSP :: Parser (SP, Exp)
pExpWhereSP
= do (sp1, xx) <- pExpAppSP
P.choice
[ do -- x where GROUP
sp <- pKey EWhere
pSym SBraceBra
cls <- liftM (map snd)
$ P.sepEndBy1 pClauseSP (pSym SSemiColon)
pSym SBraceKet
return (sp1, XWhere sp xx cls)
, do return (sp1, xx) ]
-- An application of a function to its arguments,
-- or a plain expression with no arguments.
pExpAppSP :: Parser (SP, Exp)
pExpAppSP
= do (spF, (xF, xsArg)) <- pExpAppsSP
case xsArg of
[] -> return (spF, xF)
_ -> return (spF, XDefix spF (xF : xsArg))
<?> "an expression or application"
-- An application of a function to its arguments,
-- or a plan expression with no arguments.
pExpAppsSP :: Parser (SP, (Exp, [Exp]))
pExpAppsSP
= do (spF, xFun) <- pExpFrontSP
xsArg <- pExpArgsSP pExpAtomSP
return (spF, (xFun, xsArg))
-- A list of arguments.
pExpArgsSP :: Parser (SP, Exp) -> Parser [Exp]
pExpArgsSP pX
= P.choice
[ do -- After an infix operator we allow the next expression
-- to be a compound expression rather than an atom.
-- This allows code like (f x $ λy. g x y) as in Haskell.
(UName txOp, sp) <- pBoundNameOpSP
xsMore <- pExpArgsSP pExpFrontSP
return (XInfixOp sp (Text.unpack txOp) : xsMore)
-- Some arguments.
, do (_, xsArg) <- pExpArgsSpecSP pX
xsMore <- pExpArgsSP pExpAtomSP
return (xsArg ++ xsMore)
-- No more arguments.
, do return []
]
-- Comp, Witness or Spec arguments.
pExpArgsSpecSP :: Parser (SP, Exp) -> Parser (SP, [Exp])
pExpArgsSpecSP pX
= P.choice
-- [Type]
[ do sp <- pSym SSquareBra
t <- pType
pSym SSquareKet
return (sp, [XType t])
-- [: Type0 Type0 ... :]
, do sp <- pSym SSquareColonBra
ts <- fmap (fst . unzip) $ P.many1 pTypeAtomSP
pSym SSquareColonKet
return (sp, [XType t | t <- ts])
-- { Witness }
, do sp <- pSym SBraceBra
w <- pWitness
pSym SBraceKet
return (sp, [XWitness w])
-- {: Witness0 Witness0 ... :}
, do sp <- pSym SBraceColonBra
ws <- P.many1 pWitnessAtom
pSym SBraceColonKet
return (sp, [XWitness w | w <- ws])
-- Exp0
, do (sp, x) <- pX
return (sp, [x])
]
<?> "a type, witness or expression argument"
-- | Parse a compound Source Tetra expression.
-- The first token determines the form of the expression.
pExpFrontSP :: Parser (SP, Exp)
pExpFrontSP
= P.choice
-- Level-0 lambda abstractions
-- \(x1 x2 ... : Type) (y1 y2 ... : Type) ... . Exp
-- \x1 x2 : Type. Exp
-- \x1 x2. Exp
[ do sp <- P.choice
[ pSym SLambda
, pSym SBackSlash ]
pts <- P.choice
[ P.try
$ fmap concat $ P.many1
$ do pSym SRoundBra
ps <- P.many1 pPat
pTok (KOp ":")
t <- pType
pSym SRoundKet
return [(p, Just t) | p <- ps]
, do ps <- P.many1 pPatAtom
return [(p, Nothing) | p <- ps]
]
pSym SArrowDashRight
xBody <- pExp
return (sp, XAnnot sp $ foldr (\(p, mt) -> XLamPat sp p mt) xBody pts)
-- Level-1 lambda abstractions.
-- /\(x1 x2 ... : Type) (y1 y2 ... : Type) ... . Exp
, do sp <- P.choice
[ pSym SBigLambda
, pSym SBigLambdaSlash ]
bs <- P.choice
[ fmap concat $ P.many1
$ do pSym SRoundBra
bs' <- P.many1 pBind
pTok (KOp ":")
t <- pType
pSym SRoundKet
return $ map (\b -> XBindVarMT b (Just t)) bs'
, do bs' <- P.many1 pBind
return $ map (\b -> XBindVarMT b Nothing) bs'
]
pSym SArrowDashRight
xBody <- pExp
return (sp, XAnnot sp $ foldr XLAM xBody bs)
-- let expression
, do (lts, sp) <- pLetsSP
pTok (KKeyword EIn)
x2 <- pExp
return (sp, XAnnot sp $ XLet lts x2)
-- Sugar for a let-expression.
-- do { Stmt;+ }
, do sp <- pKey EDo
pSym SBraceBra
xx <- pStmts
pSym SBraceKet
return (sp, xx)
-- case Exp of { Alt;+ }
, do sp <- pKey ECase
x <- pExp
pKey EOf
pSym SBraceBra
alts <- P.sepEndBy1 pAltCase (pSym SSemiColon)
pSym SBraceKet
return (sp, XAnnot sp $ XCase x alts)
-- match { | EXP = EXP | EXP = EXP ... }
-- Sugar for cascaded case expressions case-expression.
, do sp <- pKey EMatch
pSym SBraceBra
gxs <- liftM (map (AAltMatch . snd))
$ P.sepEndBy1 (pGuardedExpSP (pSym SEquals))
(pSym SSemiColon)
let xError
= makeXErrorDefault
(Text.pack $ sourcePosSource sp)
(fromIntegral $ sourcePosLine sp)
pSym SBraceKet
return (sp, XAnnot sp $ XMatch sp gxs xError)
, do -- if-then-else
-- Sugar for a case-expression.
sp <- pTokSP (KKeyword EIf)
x1 <- pExp
pTok (KKeyword EThen)
x2 <- pExp
pTok (KKeyword EElse)
x3 <- pExp
return (sp, XAnnot sp $ XCase x1
[ AAltCase PTrue [GExp x2]
, AAltCase PDefault [GExp x3]])
-- weakeff [Type] in Exp
, do sp <- pTokSP (KKeyword EWeakEff)
pSym SSquareBra
t <- pType
pSym SSquareKet
pKey EIn
x <- pExp
return (sp, XAnnot sp $ XCast (CastWeakenEffect t) x)
-- purify Witness in Exp
, do sp <- pKey EPurify
w <- pWitness
pTok (KKeyword EIn)
x <- pExp
return (sp, XAnnot sp $ XCast (CastPurify w) x)
-- box Exp
, do sp <- pKey EBox
x <- pExp
return (sp, XAnnot sp $ XCast CastBox x)
-- run Exp
, do sp <- pKey ERun
x <- pExp
return (sp, XAnnot sp $ XCast CastRun x)
-- ATOM
, do pExpAtomSP
]
<?> "an expression"
-- | Parse a variable, constructor or parenthesised expression,
-- also returning source position.
pExpAtomSP :: Parser (SP, Exp)
pExpAtomSP
= P.choice
[
-- ( Exp2 )
do pSym SRoundBra
(sp, t) <- pExpWhereSP
pSym SRoundKet
return (sp, t)
-- Infix operator used as a variable.
, do (UName tx, sp) <- pBoundNameOpVarSP
return (sp, XInfixVar sp (Text.unpack tx))
-- Infix operator used nekkid.
, do (UName tx, sp) <- pBoundNameOpSP
return (sp, XInfixOp sp (Text.unpack tx))
-- The unit data constructor.
, do sp <- pTokSP (KBuiltin BDaConUnit)
return (sp, XCon dcUnit)
-- Named algebraic constructors.
, do (con, sp) <- pDaConBoundNameSP
return (sp, XCon (DaConBound con))
-- Literals.
-- We just fill-in the type with a hole for now, and leave it to
-- We also set the literal as being algebraic, which may not be
-- true (as for Floats). The spreader also needs to fix this.
, do (lit, sp) <- pDaConBoundLitSP
return (sp, XCon (DaConPrim lit (TVar UHole)))
-- Primitive names.
, do (nPrim, sp) <- pPrimValSP
return (sp, XPrim nPrim)
-- Named variables.
, do (u, sp) <- pBoundNameSP
return (sp, XVar u)
-- Debruijn indices
, do (u, sp) <- pBoundIxSP
return (sp, XVar u)
]
<?> "a variable, constructor, or parenthesised type"
-- Alternatives -----------------------------------------------------------------------------------
-- Case alternatives.
pAltCase :: Parser AltCase
pAltCase
= do p <- pPat
P.choice
[ do -- Desugar case guards while we're here.
spgxs <- P.many1 (pGuardedExpSP (pSym SArrowDashRight))
let gxs = map snd spgxs
return $ AAltCase p gxs
, do pSym SArrowDashRight
x <- pExp
return $ AAltCase p [GExp x] ]
-- Patterns.
pPat :: Parser Pat
pPat
= P.choice
[ -- Con Bind Bind ...
do nCon <- pDaConBoundName
ps <- P.many pPatAtom
return $ PData (DaConBound nCon) ps
-- Atom
, do p <- pPatAtom
return p
]
<?> "a pattern"
pPatAtom :: Parser Pat
pPatAtom
= P.choice
[ do -- ( PAT )
pSym SRoundBra
p <- pPat
pSym SRoundKet
return $ p
-- Wildcard
-- Try this case before the following one for binders
-- so that '_' is parsed as the default pattern,
-- rather than a wildcard binder.
, do pSym SUnderscore
return $ PDefault
-- Var
, do b <- pBind
P.choice
[ do _ <- pSym SAt
p <- pPatAtom
return $ PAt b p
, do return $ PVar b
]
-- Lit
, do nLit <- pDaConBoundLit
return $ PData (DaConPrim nLit (TBot S.KData)) []
-- Named algebraic constructors.
, do nCon <- pDaConBoundName
return $ PData (DaConBound nCon) []
-- 'Unit'
, do pTok (KBuiltin BDaConUnit)
return $ PData dcUnit []
]
<?> "a pattern"
-- Bindings ---------------------------------------------------------------------------------------
pLetsSP :: Parser (Lets, SP)
pLetsSP
= P.choice
[ -- non-recursive let
do sp <- pKey ELet
l <- liftM snd $ pClauseSP
return (LGroup [l], sp)
-- recursive let
, do sp <- pKey ELetRec
pSym SBraceBra
ls <- liftM (map snd)
$ P.sepEndBy1 pClauseSP (pSym SSemiColon)
pSym SBraceKet
return (LGroup ls, sp)
-- Private region binding.
-- private Binder+ (with { Binder : Type ... })? in Exp
, do sp <- pKey EPrivate
-- new private region names.
bs <- P.manyTill pBind
$ P.try
$ P.lookAhead
$ P.choice [pKey EIn, pKey EWith]
-- Witness types.
r <- pLetWits bs Nothing
return (r, sp)
-- Extend an existing region.
-- extend Binder+ using Type (with { Binder : Type ...})? in Exp
, do sp <- pTokSP (KKeyword EExtend)
-- parent region
t <- pType
pTok (KKeyword EUsing)
-- new private region names.
bs <- P.manyTill pBind
$ P.try $ P.lookAhead
$ P.choice
[ pTok (KKeyword EUsing)
, pTok (KKeyword EWith)
, pTok (KKeyword EIn) ]
-- witness types
r <- pLetWits bs (Just t)
return (r, sp)
]
pLetWits :: [Bind] -> Maybe Type -> Parser Lets
pLetWits bs mParent
= P.choice
[ do pKey EWith
pSym SBraceBra
wits <- P.sepBy (P.choice
[ -- Named witness binder.
do b <- pBind
pTok (KOp ":")
t <- pTypeApp
return (b, t)
-- Ambient witness binding, used for capabilities.
, do t <- pTypeApp
return (BNone, t)
])
(pSym SSemiColon)
pSym SBraceKet
return (LPrivate bs mParent wits)
, do return (LPrivate bs mParent [])
]
-- | A binding for let expression.
pClauseSP :: Parser (SP, Clause)
pClauseSP
= do -- Name of the binding.
(b, sp0) <- pBindNameSP
P.choice
[ do -- Either
-- 1) a definition with a signature and some clauses.
-- foo : Nat -> Nat = ...
-- 2) foo : Nat -> Nat
--
_ <- pTokSP (KOp ":")
t <- pType
P.choice
[ do
gxs <- pTermGuardedExps (pSym SEquals)
return (sp0, SLet sp0 (XBindVarMT b (Just t)) [] gxs)
, do return (sp0, SSig sp0 b t)
]
, do -- Non-function binding with no type signature.
gxs <- pTermGuardedExps (pSym SEquals)
return (sp0, SLet sp0 (XBindVarMT b Nothing) [] gxs)
, do -- Binding using function syntax.
ps <- fmap concat $ P.many pParamsSP
P.choice
[ do -- Function syntax with a return type.
-- We can make the full type sig for the let-bound variable.
-- Binder Param1 Param2 .. ParamN : Type = Exp
sp <- pTokSP (KOp ":")
tBody <- pType
gxs <- pTermGuardedExps (pSym SEquals)
let t = funTypeOfParams ps tBody
return (sp, SLet sp (XBindVarMT b (Just t)) ps gxs)
-- Function syntax with no return type.
-- We can't make the type sig for the let-bound variable.
, do gxs <- pTermGuardedExps (pSym SEquals)
return (sp0, SLet sp0 (XBindVarMT b Nothing) ps gxs)
]
]
-- Function parameters.
pParamsSP :: Parser [Param]
pParamsSP
= P.choice
-- Type parameter
-- [BIND1 BIND2 .. BINDN : TYPE]
[ do pSym SSquareBra
bs <- P.many1 pBind
pTok (KOp ":")
t <- pType
pSym SSquareKet
return [ MType b (Just t) | b <- bs]
-- Witness parameter
-- {BIND : TYPE}
, do pSym SBraceBra
b <- pBind
pTok (KOp ":")
t <- pType
pSym SBraceKet
return [ MWitness b (Just t) ]
-- Value pattern with type annotations.
-- (BIND1 BIND2 .. BINDN : TYPE)
, do pSym SRoundBra
ps <- P.choice
[ P.try $ do
ps <- P.many1 pPatAtom
pTok (KOp ":")
t <- pType
return [ MValue p (Just t) | p <- ps ]
, do p <- pPat
return [ MValue p Nothing ]
]
pSym SRoundKet
return ps
, do -- Value parameter without a type annotation.
p <- pPatAtom
return [MValue p Nothing]
]
<?> "a function parameter"
-- and the type of the body.
funTypeOfParams
:: [Param] -- ^ Spec of parameters.
-> Type -- ^ Type of body.
-> Type -- ^ Type of whole function.
funTypeOfParams [] tBody
= tBody
funTypeOfParams (p:ps) tBody
= case p of
MType b mt
-> let k = fromMaybe (TBot S.KData) mt
in TApp (TCon (TyConForall k)) (TAbs b k $ funTypeOfParams ps tBody)
MWitness _ mt
-> let k = fromMaybe (TBot S.KData) mt
in TImpl k $ funTypeOfParams ps tBody
MValue _ mt
-> let k = fromMaybe (TBot S.KData) mt
in TFun k $ funTypeOfParams ps tBody
-- Guards -----------------------------------------------------------------------------------------
-- | Parse either the terminating char and a single expression,
-- or some guarded expressions.
pTermGuardedExps
:: Parser SP -- ^ Parser for char between guards and exp
-> Parser [GuardedExp]
pTermGuardedExps pTerm
= P.choice
[ do _ <- pTerm
xBody <- pExp
return [GExp xBody]
, do fmap (map snd)
$ P.many1 $ pGuardedExpSP pTerm
]
-- | An guarded expression,
-- like | EXP1 = EXP2.
pGuardedExpSP
:: Parser SP -- ^ Parser for char between and of guards and exp.
-- usually -> or =
-> Parser (SP, GuardedExp)
pGuardedExpSP pTermSP
= pGuardExp (pSym SBar)
where pGuardExp pSepSP
= P.choice
[ do sp <- pSepSP
g <- pGuard
gx <- liftM snd $ pGuardExp (pSym SComma)
return (sp, GGuard g gx)
, do sp <- pTermSP
x <- pExp
return (sp, GExp x) ]
pGuard
= P.choice
[ P.try $
do p <- pPat
pSym SArrowDashLeft
x <- pExp
return $ GPat p x
, do g <- pExp
return $ GPred g
, do pKey EOtherwise
return GDefault ]
-- Statements -------------------------------------------------------------------------------------
-- These are statements inside a do expression.
--
-- A 'do' block behaves much the same way as a 'let' expression,
-- except we can write effectful statements without binding the
-- result to anything.
--
-- We currently desugar do expressions to let-expressions in the parser.
--
-- | Represent a statement inside a do block.
data Stmt
-- | Let-binding or type signature.
= StmtClause SP Clause
-- | Case match.
| StmtMatch SP Pat Exp Exp
-- | Plain statement without binding the result.
| StmtNone SP Exp
-- | Parse a single statement.
pStmt :: Parser Stmt
pStmt
= P.choice
[ -- Clause;
-- We need the 'try' because the function and argument names at the front
-- of a clause can also be parsed as a function application in a statement.
P.try $
do (sp, c) <- pClauseSP
return $ StmtClause sp c
-- Pat <- Exp else Exp ;
-- Sugar for a case-expression.
-- We need the 'try' because the PAT can also be parsed
-- as a function name in a non-binding statement.
, P.try $
do p <- pPat
sp <- pSym SArrowDashLeft
x1 <- pExp
pTok (KKeyword EElse)
x2 <- pExp
return $ StmtMatch sp p x1 x2
-- Exp
, do (sp, x) <- pExpWhereSP
return $ StmtNone sp x
]
-- | Parse some statements.
pStmts :: Parser Exp
pStmts
= do -- Parse statements in the block.
stmts <- P.sepEndBy1 pStmt (pSym SSemiColon)
-- As in Haskell, we require do blocks to end with a statement
-- that gives the overall value.
case makeStmts [] stmts of
Nothing -> P.unexpected "do-block must end with a statement"
Just x -> return x
-- | Make an expression from some statements.
-- We collect consecutive clauses into the same clause group,
-- so that we can define functions with multiple clauses at the top
-- level of a 'do' expression.
makeStmts :: [Clause] -> [Stmt] -> Maybe Exp
makeStmts clsAcc ss
= let
-- Wrap the clauses we're carrying around the given
-- body expression.
dropClauses xBody
= case clsAcc of
[] -> xBody
[SLet sp bmt [] [GExp x]]
-> XAnnot sp $ XLet (LLet bmt x) xBody
_ -> XLet (LGroup clsAcc) xBody
in
case ss of
[StmtNone _ x]
-> Just $ dropClauses
$ x
StmtNone sp x1 : rest
| Just x2 <- makeStmts [] rest
-> Just $ XAnnot sp
$ dropClauses
$ XLet (LLet (XBindVarMT BNone Nothing) x1) x2
StmtClause _ cl : rest
-> case clsAcc of
-- Start accumulating successive clauses.
[] -> makeStmts (clsAcc ++ [cl]) rest
(cl1 : _)
-- If this clause is for the same function as
-- the previous one then we'll collect it into
-- at letrec at this point.
| bindOfClause cl1 == bindOfClause cl
-> makeStmts (clsAcc ++ [cl]) rest
-- Otherwise make a standard let-expression.
_ | Just x3 <- makeStmts [] rest
-> case cl of
(SLet sp bmt [] [GExp x])
-> Just $ XAnnot sp
$ dropClauses
$ XLet (LLet bmt x) x3
_ -> Nothing
| otherwise
-> Nothing
StmtMatch sp p x1 x2 : rest
| Just x3 <- makeStmts [] rest
-> Just $ XAnnot sp
$ dropClauses
$ XCase x1
[ AAltCase p [GExp x3]
, AAltCase PDefault [GExp x2] ]
_ -> Nothing