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

Agda.Compiler.Epic.AuxAST

Contents

Description

Intermediate abstract syntax tree used in the compiler. Pretty close to Epic syntax.

Synopsis

Documentation

data Lit Source

Instances

data Branch Source

Constructors

Branch 

Fields

brTag :: Tag
 
brName :: QName
 
brVars :: [Var]
 
brExpr :: Expr
 
BrInt 

Fields

brInt :: Int
 
brExpr :: Expr
 
Default 

Fields

brExpr :: Expr
 

Instances

Some smart constructors

lett :: Var -> Expr -> Expr -> ExprSource

Smart constructor for let expressions to avoid unneceessary lets

lazy :: Expr -> ExprSource

Some things are pointless to make lazy

casee :: Expr -> [Branch] -> ExprSource

If casing on the same expression in a sub-expression, we know what branch to pick

apps :: Var -> [Expr] -> ExprSource

Smart constructor for applications to avoid empty applications

Substitution

substSource

Arguments

:: Var

Substitute this ...

-> Var

with this ...

-> Expr

in this.

-> Expr 

Substitution

substs :: [(Var, Var)] -> Expr -> ExprSource

fv :: Expr -> [Var]Source

Get the free variables in an expression