Agda-2.2.10: A dependently typed functional programming language and proof assistant Source code Contents Index

Agda.Compiler.Epic.LambdaLift

Description

Lift lambda expressions to top level definitions (Epic does not support lambdas).

Synopsis

type LL = WriterT [Fun] lambdaLift :: MonadTCM m => [Fun] -> Compile m [Fun] lambdaLiftFun :: MonadTCM m => Fun -> LL (Compile m) Fun lambdaLiftExpr :: MonadTCM m => Expr -> LL (Compile m) Expr

Documentation

type LL = WriterT [Fun] Source

LL makes it possible to emit new functions when we encounter a lambda

lambdaLift :: MonadTCM m => [Fun] -> Compile m [Fun] Source

lambda lift all the functions

lambdaLiftFun :: MonadTCM m => Fun -> LL (Compile m) Fun Source

 lift a function, this is in a LL (Writer monad)

lambdaLiftExpr :: MonadTCM m => Expr -> LL (Compile m) Expr Source

 lift an expression, put all the new definitions in the writer monad

Produced by Haddock version 2.6.1