Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Compiler.Epic.Erasure
Description

Some arguments to functions (types in particular) will not be used in the body. Wouldn't it be useful if these wasn't passed around at all? Fear not, we here perform some analysis and try to remove as many of these occurences as possible.

We employ the worker/wrapper transform, so if f x1 .. xn = e and we notice that some is not needed we create: f' xj .. xk = e [xi := unit] and f x1 .. xn = f' xj .. xk. i.e we erase them in f' and replace by unit, and the original f function calls the new f'. The idea is that f should be inlined and then peace on earth.

Synopsis
data Relevancy
= Irr
| Rel
| DontKnow
isIrr :: Relevancy -> Bool
isRel :: Relevancy -> Bool
(&&-) :: Relevancy -> Relevancy -> Relevancy
data ErasureState = ErasureState {
relevancies :: Map Var [Relevancy]
funs :: Map Var Fun
}
type Erasure = StateT ErasureState
erasure :: MonadTCM m => [Fun] -> Compile m [Fun]
initiate :: Monad m => Fun -> Erasure m ()
relevant :: (Functor m, Monad m) => Var -> Expr -> Erasure m Relevancy
step :: (Monad m, Functor m) => Erasure m (Map Var [Relevancy])
Documentation
data Relevancy Source
Constructors
Irr
Rel
DontKnow
isIrr :: Relevancy -> BoolSource
isRel :: Relevancy -> BoolSource
(&&-) :: Relevancy -> Relevancy -> RelevancySource
Irrelevancy and
data ErasureState Source
Constructors
ErasureState
relevancies :: Map Var [Relevancy]
funs :: Map Var Fun
type Erasure = StateT ErasureStateSource
erasure :: MonadTCM m => [Fun] -> Compile m [Fun]Source
Try to find as many unused variables as possible
initiate :: Monad m => Fun -> Erasure m ()Source
Initiate a function's relevancies (all DontKnow)
relevant :: (Functor m, Monad m) => Var -> Expr -> Erasure m RelevancySource
Calculate if a variable is relevant in an expression
step :: (Monad m, Functor m) => Erasure m (Map Var [Relevancy])Source
Try to find a fixpoint for all the functions relevancy.
Produced by Haddock version 2.6.1