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

type Inline = Bool

data Fun

Instances

data Lit

Instances

data Branch

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 -> Expr

Smart constructor for let expressions to avoid unneceessary lets

lazy :: Expr -> Expr

Some things are pointless to make lazy

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

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

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

Smart constructor for applications to avoid empty applications

Substitution

subst

Arguments

:: Var

Substitute this ...

-> Var

with this ...

-> Expr

in this.

-> Expr 

Substitution

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

fv :: Expr -> [Var]

Get the free variables in an expression