Agda-2.2.10: A dependently typed functional programming language and proof assistant

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

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.