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

Safe HaskellNone
LanguageHaskell98

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