|
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 |
|
|
|
Documentation |
|
|
|
|
|
|
|
|
|
Irrelevancy and
|
|
|
|
|
|
|
|
Try to find as many unused variables as possible
|
|
|
Initiate a function's relevancies (all DontKnow)
|
|
|
Calculate if a variable is relevant in an expression
|
|
|
Try to find a fixpoint for all the functions relevancy.
|
|
Produced by Haddock version 2.6.1 |