{-# LANGUAGE TupleSections #-}
module FreeC.LiftedIR.Converter.Expr ( liftExpr ) where
import Control.Applicative ( (<|>) )
import Control.Monad ( join, when )
import Data.Bool ( bool )
import Data.Foldable
import Data.Maybe ( fromJust, fromMaybe )
import FreeC.Environment
import FreeC.Environment.Entry ( entryAgdaIdent, entryIdent )
import FreeC.Environment.Fresh
import FreeC.Environment.LookupOrFail
( lookupAgdaFreshIdentOrFail, lookupAgdaValIdentOrFail, lookupIdentOrFail )
import FreeC.Environment.Renamer ( renameAndDefineLIRVar )
import qualified FreeC.IR.Base.Prelude as IR.Prelude
import FreeC.IR.SrcSpan ( SrcSpan(NoSrcSpan) )
import FreeC.IR.Subst
import qualified FreeC.IR.Syntax as IR
import FreeC.IR.Syntax.Name ( identFromQName )
import qualified FreeC.LiftedIR.Converter.Type as LIR
import FreeC.LiftedIR.Effect
import qualified FreeC.LiftedIR.Syntax as LIR
import FreeC.Monad.Converter
import FreeC.Monad.Reporter
( Message(Message), Severity(Internal), reportFatal )
import FreeC.Pretty ( showPretty )
liftExpr :: IR.Expr -> Converter LIR.Expr
liftExpr expr = liftExpr' expr [] []
liftExpr' :: IR.Expr -> [IR.Type] -> [IR.Expr] -> Converter LIR.Expr
liftExpr' (IR.App _ e1 e2 _) [] args = liftExpr' e1 [] (e2 : args)
liftExpr' (IR.TypeAppExpr _ e t _) typeArgs args = liftExpr' e (t : typeArgs)
args
liftExpr' (IR.Con srcSpan name _) typeArgs args = do
args' <- mapM liftExpr args
typeArgs' <- mapM LIR.liftType' typeArgs
Just typeArgArity <- inEnv $ lookupTypeArgArity IR.ValueScope name
let con = LIR.SmartCon srcSpan name
typeArgCount = length typeArgs'
when (typeArgCount /= typeArgArity)
$ reportFatal
$ Message srcSpan Internal
$ unlines [ "The constructor '"
++ showPretty name
++ "' is applied to the wrong number of type arguments."
, "Expected "
++ show typeArgArity
++ " type arguments, got "
++ show typeArgCount
++ "."
]
return $ LIR.App srcSpan con typeArgs' [] args' True
liftExpr' (IR.Var srcSpan name _) typeArgs args = do
args' <- mapM liftExpr args
agdaIdent <- lookupAgdaValIdentOrFail srcSpan name
coqIdent <- lookupIdentOrFail srcSpan IR.ValueScope name
let varName = LIR.Var srcSpan name agdaIdent coqIdent
typeArgCount = length typeArgs
maybeTypeArgArity <- inEnv $ lookupTypeArgArity IR.ValueScope name
case maybeTypeArgArity of
Just typeArgArity -> when (typeArgCount /= typeArgArity)
$ reportFatal
$ Message srcSpan Internal
$ unlines [ "The function '"
++ showPretty name
++ "' is applied to the wrong number of type arguments."
, "Expected "
++ show typeArgArity
++ " type arguments, got "
++ show typeArgCount
++ "."
]
Nothing -> when (typeArgCount /= 0)
$ reportFatal
$ Message srcSpan Internal
$ unlines [ "The variable '"
++ showPretty name
++ "' must not be applied to type arguments."
, "Got " ++ show typeArgCount ++ " type arguments."
]
function <- inEnv $ isFunction name
if function
then do
effects <- inEnv $ lookupEffects name
Just strictArgs <- inEnv $ lookupStrictArgs name
freeArgs <- inEnv $ needsFreeArgs name
Just typeArgIdents <- inEnv $ lookupTypeArgs IR.ValueScope name
Just argTypes <- inEnv $ lookupArgTypes IR.ValueScope name
Just arity <- inEnv $ lookupArity IR.ValueScope name
let typeArgNames = map (IR.UnQual . IR.Ident) typeArgIdents
subst = composeSubsts
(zipWith singleSubst typeArgNames typeArgs)
argTypes' <- mapM (LIR.liftType' . applySubst subst) argTypes
typeArgs' <- mapM LIR.liftType' typeArgs
generateBinds (zip3 args' (map Just argTypes' ++ repeat Nothing)
$ strictArgs ++ repeat False)
$ \args'' -> generateApply
(LIR.App srcSpan varName typeArgs' effects (take arity args'') freeArgs)
$ drop arity args''
else do
pureArg <- inEnv $ isPureVar name
generateApply (bool id (LIR.Pure NoSrcSpan) pureArg varName) args'
liftExpr' (IR.IntLiteral srcSpan value _) [] []
= return $ LIR.Pure srcSpan $ LIR.IntLiteral srcSpan value
liftExpr' (IR.Lambda srcSpan args rhs _) [] [] = localEnv $ do
(pats, expr) <- liftAlt' args rhs
return
$ foldr (\a b -> LIR.Pure srcSpan $ LIR.Lambda srcSpan [a] b) expr pats
liftExpr' (IR.If srcSpan cond true false _) [] [] = do
cond' <- liftExpr cond
bool' <- LIR.liftType' $ IR.TypeCon NoSrcSpan IR.Prelude.boolTypeConName
bind cond' freshBoolPrefix (Just bool')
$ \d -> LIR.If srcSpan d <$> liftExpr true <*> liftExpr false
liftExpr' (IR.Case srcSpan discriminante patterns _) [] [] = do
discriminant' <- liftExpr discriminante
bind discriminant' freshArgPrefix Nothing
$ \d -> LIR.Case srcSpan d <$> mapM liftAlt patterns
liftExpr' (IR.Undefined srcSpan _) typeArgs args = do
when (length typeArgs /= 1)
$ reportFatal
$ Message srcSpan Internal
$ unlines
[ "Error term 'undefined' is applied to the wrong number of type arguments."
, "Expected 1 type arguments, got " ++ show (length typeArgs) ++ "."
]
typeArgs' <- mapM LIR.liftType' typeArgs
args' <- mapM liftExpr args
generateApply
(LIR.App srcSpan (LIR.Undefined srcSpan) typeArgs' [Partiality] [] True)
args'
liftExpr' (IR.ErrorExpr srcSpan msg _) typeArgs args = do
when (length typeArgs /= 1)
$ reportFatal
$ Message srcSpan Internal
$ unlines
[ "Error term 'error "
++ show msg
++ "' is applied to the wrong number of type arguments."
, "Expected 1 type arguments, got " ++ show (length typeArgs) ++ "."
]
typeArgs' <- mapM LIR.liftType' typeArgs
args' <- mapM liftExpr args
generateApply (LIR.App srcSpan (LIR.ErrorExpr srcSpan) typeArgs' [Partiality]
[LIR.StringLiteral srcSpan msg] True) args'
liftExpr' (IR.Trace srcSpan msg expr _) typeArgs args = do
when (length typeArgs /= 1)
$ reportFatal
$ Message srcSpan Internal
$ unlines
[ "Effect 'trace' is applied to the wrong number of type arguments."
, "Expected 1 type arguments, got " ++ show (length typeArgs) ++ "."
]
typeArgs' <- mapM LIR.liftType' typeArgs
expr' <- liftExpr expr
args' <- mapM liftExpr args
generateApply (LIR.App srcSpan (LIR.Trace srcSpan) typeArgs' [Tracing]
[LIR.StringLiteral srcSpan msg, expr'] True) args'
liftExpr' (IR.Let _ binds expr _) [] [] = liftBinds binds expr
liftExpr' expr (_ : _) _ = reportFatal
$ Message (IR.exprSrcSpan expr) Internal
$ "Only type arguments of functions and constructors can be applied visibly."
liftExpr' expr [] args@(_ : _)
= join $ generateApply <$> liftExpr expr <*> mapM liftExpr args
liftConPat :: IR.ConPat -> LIR.ConPat
liftConPat (IR.ConPat srcSpan name) = LIR.ConPat srcSpan name
liftAlt :: IR.Alt -> Converter LIR.Alt
liftAlt (IR.Alt srcSpan conPat pats expr) = do
(pats', expr') <- liftAlt' pats expr
return $ LIR.Alt srcSpan (liftConPat conPat) pats' expr'
liftAlt' :: [IR.VarPat] -> IR.Expr -> Converter ([LIR.VarPat], LIR.Expr)
liftAlt' [] expr = ([], ) <$> liftExpr expr
liftAlt' (pat@(IR.VarPat srcSpan name varType strict) : pats) expr
= localEnv $ do
varType' <- LIR.liftVarPatType pat
var <- renameAndDefineLIRVar srcSpan strict name varType
(pats', expr') <- liftAlt' pats expr
if strict then do
var' <- freshIRQName name
expr'' <- rawBind srcSpan var' var varType expr'
pat' <- makeVarPat srcSpan var' varType'
return (pat' : pats', expr'') else do
pat' <- makeVarPat srcSpan var varType'
return (pat' : pats', expr')
makeVarPat :: SrcSpan -> IR.QName -> Maybe LIR.Type -> Converter LIR.VarPat
makeVarPat srcSpan var varType = do
let Just unqualVar = identFromQName var
valueEntry <- inEnv $ lookupEntry IR.ValueScope var
freshEntry <- inEnv $ lookupEntry IR.FreshScope var
let agdaVar = entryAgdaIdent $ fromJust (valueEntry <|> freshEntry)
let coqVar = entryIdent $ fromJust (valueEntry <|> freshEntry)
return $ LIR.VarPat srcSpan unqualVar varType agdaVar coqVar
generateApply :: LIR.Expr -> [LIR.Expr] -> Converter LIR.Expr
generateApply = foldlM $ \expr arg -> bind expr freshFuncPrefix Nothing
$ \f -> return $ LIR.App NoSrcSpan f [] [] [arg] False
guessName :: LIR.Expr -> Maybe String
guessName (LIR.Var _ name _ _) = IR.identFromQName name
guessName (LIR.Pure _ arg) = guessName arg
guessName (LIR.Bind _ arg _) = guessName arg
guessName _ = Nothing
bind :: LIR.Expr
-> String
-> Maybe LIR.Type
-> (LIR.Expr -> Converter LIR.Expr)
-> Converter LIR.Expr
bind (LIR.Pure _ arg) _ _ k = k arg
bind arg defaultPrefix argType k = localEnv $ do
argIdent <- freshIRQName $ fromMaybe defaultPrefix (guessName arg)
let Just argIdent' = identFromQName argIdent
argAgda <- lookupAgdaFreshIdentOrFail NoSrcSpan argIdent
argCoq <- lookupIdentOrFail NoSrcSpan IR.FreshScope argIdent
let pat = LIR.VarPat NoSrcSpan argIdent' argType argAgda argCoq
rhs <- LIR.Lambda NoSrcSpan [pat]
<$> k (LIR.Var NoSrcSpan argIdent argAgda argCoq)
return $ LIR.Bind NoSrcSpan arg rhs
generateBinds :: [(LIR.Expr, Maybe LIR.Type, Bool)]
-> ([LIR.Expr] -> Converter LIR.Expr)
-> Converter LIR.Expr
generateBinds [] k = k []
generateBinds ((arg, _, False) : as) k = generateBinds as $ \as' -> k
(arg : as')
generateBinds ((arg, argType, True) : as) k = bind arg freshArgPrefix argType
$ \arg' -> generateBinds as $ \as' -> k (arg' : as')
rawBind :: SrcSpan
-> IR.QName
-> IR.QName
-> Maybe IR.Type
-> LIR.Expr
-> Converter LIR.Expr
rawBind srcSpan mx x varType expr = do
mxAgda <- lookupAgdaFreshIdentOrFail srcSpan mx
mxCoq <- lookupIdentOrFail srcSpan IR.FreshScope mx
xAgda <- lookupAgdaValIdentOrFail srcSpan x
xCoq <- lookupIdentOrFail srcSpan IR.ValueScope x
varType' <- mapM LIR.liftType' varType
let mx' = LIR.Var srcSpan mx mxAgda mxCoq
Just unqualX = identFromQName x
x' = LIR.VarPat srcSpan unqualX varType' xAgda xCoq
return $ LIR.Bind srcSpan mx' $ LIR.Lambda srcSpan [x'] expr
liftBinds :: [IR.Bind] -> IR.Expr -> Converter LIR.Expr
liftBinds [] expr = liftExpr expr
liftBinds ((IR.Bind srcSpan varPat bindExpr) : bs) expr = localEnv $ do
let (IR.VarPat patSrcSpan ident varPatType isStrict) = varPat
_ <- renameAndDefineLIRVar srcSpan isStrict ident varPatType
expr' <- liftBinds bs expr
patType' <- mapM LIR.liftType varPatType
varPat' <- makeVarPat patSrcSpan (IR.varPatQName varPat) patType'
shareType' <- mapM LIR.liftType' varPatType
bindExpr' <- liftExpr bindExpr
let shareExpr = LIR.Share srcSpan bindExpr' shareType'
return $ LIR.Bind srcSpan shareExpr (LIR.Lambda srcSpan [varPat'] expr')