module Agda.Compiler.Epic.ForceConstrs where
import Control.Applicative
import Agda.Compiler.Epic.AuxAST
import Agda.Compiler.Epic.CompileState
import Agda.Compiler.Epic.Interface
import qualified Agda.Syntax.Common as Common
import qualified Agda.Syntax.Internal as T
import Agda.TypeChecking.Monad (TCM)
#include "undefined.h"
import Agda.Utils.Impossible
makeForcedArgs :: T.Type -> ForcedArgs
makeForcedArgs (T.El _ term) = case T.ignoreSharing term of
T.Pi arg ab -> isRel arg : makeForcedArgs (T.unAbs ab)
_ -> []
where
isRel :: Common.Dom T.Type -> Forced
isRel arg = case Common.getRelevance arg of
Common.Relevant -> NotForced
Common.Irrelevant -> Forced
Common.UnusedArg -> Forced
Common.NonStrict -> Forced
Common.Forced{} -> Forced
forceConstrs :: [Fun] -> Compile TCM [Fun]
forceConstrs fs = mapM forceFun fs
forceFun :: Fun -> Compile TCM Fun
forceFun e@(EpicFun{}) = return e
forceFun (Fun inline name qname comment args expr) =
Fun inline name qname comment args <$> forceExpr expr
where
forceExpr :: Expr -> Compile TCM Expr
forceExpr expr = case expr of
Var v -> return $ Var v
Lit l -> return $ Lit l
Lam v e -> Lam v <$> forceExpr e
Con tag q es -> do
forcArgs <- getForcedArgs q
return $ Con tag q $ notForced forcArgs es
App v es -> App v <$> mapM forceExpr es
Case e bs -> Case <$> forceExpr e <*> mapM forceBranch bs
Let v e e' -> lett v <$> forceExpr e <*> forceExpr e'
If a b c -> If <$> forceExpr a <*> forceExpr b <*> forceExpr c
Lazy e -> Lazy <$> forceExpr e
UNIT -> return expr
IMPOSSIBLE -> return expr
forceBranch :: Branch -> Compile TCM Branch
forceBranch br = case br of
Branch tag name vars e -> do
ir <- getForcedArgs name
let vs = notForced ir vars
subs = forced ir vars
e'' <- if all (`notElem` fv e) subs
then return e
else __IMPOSSIBLE__
Branch tag name vs <$> forceExpr e''
BrInt i e -> BrInt i <$> forceExpr e
Default e -> Default <$> forceExpr e