module Agda.Compiler.Epic.Erasure where
import Control.Applicative
import Control.Monad.State
import Data.Map(Map)
import qualified Data.Map as M
import Data.Maybe
import Agda.Compiler.Epic.AuxAST
import Agda.Compiler.Epic.CompileState
import Agda.TypeChecking.Monad.Base (MonadTCM)
data Relevancy
= Irr
| Rel
| DontKnow
deriving (Eq, Ord, Show)
isIrr :: Relevancy -> Bool
isIrr Irr = True
isIrr Rel = False
isIrr DontKnow = True
isRel :: Relevancy -> Bool
isRel = not . isIrr
(&&-) :: Relevancy -> Relevancy -> Relevancy
Rel &&- _ = Rel
_ &&- Rel = Rel
DontKnow &&- a = a
a &&- DontKnow = a
Irr &&- Irr = Irr
data ErasureState = ErasureState
{ relevancies :: Map Var [Relevancy]
, funs :: Map Var Fun
}
type Erasure = StateT ErasureState
erasure :: MonadTCM m => [Fun] -> Compile m [Fun]
erasure fs = do
rels <- flip evalStateT (ErasureState M.empty M.empty) $ do
mapM_ initiate fs
fu <- gets funs
M.mapKeys (fromJust . flip M.lookup fu) <$> step
fmap concat $ mapM (\f -> check f (M.lookup f rels)) fs
where
check :: MonadTCM m => Fun -> Maybe [Relevancy] -> Compile m [Fun]
check f (Just rs) | any isIrr rs && not (funInline f) = do
f' <- newName
let args' = pairwiseFilter (map isRel rs) (funArgs f)
subs = pairwiseFilter (map isIrr rs) (funArgs f)
e' = foldr (\v e -> subst v "primUnit" e) (funExpr f) subs
return [ Fun { funInline = True
, funName = funName f
, funComment = funComment f
, funArgs = funArgs f
, funExpr = App f' $ map Var args'
}
, Fun { funInline = False
, funName = f'
, funComment = funComment f ++ " [ERASED]"
, funArgs = args'
, funExpr = e'
}
]
check f _ = return [f]
initiate :: Monad m => Fun -> Erasure m ()
initiate f@(Fun _ name _ args _) =
modify $ \s -> s { relevancies = M.insert name (replicate (length args) DontKnow) (relevancies s)
, funs = M.insert name f (funs s)
}
initiate (EpicFun {}) = return ()
relevant :: (Functor m, Monad m) => Var -> Expr -> Erasure m Relevancy
relevant var expr = case expr of
Var v | v == var -> return Rel
| otherwise -> return Irr
Lit _l -> return Irr
Lam _ e -> relevant var e
Con _ _ es -> relevants var es
App v es | v == var -> return Rel
| otherwise -> do
mvrs <- gets (M.lookup v . relevancies)
case mvrs of
Nothing -> relevants var es
Just vrs -> relevants var
$ pairwiseFilter (map isRel vrs ++ repeat True ) es
Case e brs -> (&&-) <$> relevant var e <*> relevants var (map brExpr brs)
If a b c -> relevants var [a,b,c]
Let _ e1 e2 -> (&&-) <$> relevant var e1 <*> relevant var e2
Lazy e -> relevant var e
UNIT -> return Irr
IMPOSSIBLE -> return Irr
where
relevants :: (Functor m, Monad m) => Var -> [Expr] -> Erasure m Relevancy
relevants v es = foldM (\x y -> return $ x &&- y) Irr =<< mapM (relevant v) es
step :: (Monad m, Functor m) => Erasure m (Map Var [Relevancy])
step = do
s <- get
rels <- forM (M.toList (relevancies s)) $ \(v, _) -> do
let f = fromJust $ M.lookup v (funs s)
(,) v <$> mapM (flip relevant (funExpr f)) (funArgs f)
let relsm = M.fromList rels
if relevancies s == relsm
then return relsm
else do
put s {relevancies = relsm}
step