Agda.Compiler.Epic.Erasure

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.

Documentation

data Relevancy

Constructors

Irr

Rel

DontKnow

Instances

Eq Relevancy

Ord Relevancy

Show Relevancy

isIrr :: Relevancy -> Bool

isRel :: Relevancy -> Bool

(&&-) :: Relevancy -> Relevancy -> Relevancy

Irrelevancy and

data ErasureState

Constructors

ErasureState

Fields

relevancies :: Map Var [Relevancy]

funs :: Map Var Fun

type Erasure = StateT ErasureState

erasure :: MonadTCM m => [Fun] -> Compile m [Fun]

Try to find as many unused variables as possible

initiate :: Monad m => Fun -> Erasure m ()

Initiate a function's relevancies (all DontKnow)

relevant :: (Functor m, Monad m) => Var -> Expr -> Erasure m Relevancy

Calculate if a variable is relevant in an expression

step :: (Monad m, Functor m) => Erasure m (Map Var [Relevancy])

Try to find a fixpoint for all the functions relevancy.