Agda.Compiler.Epic.AuxAST

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

Documentation

type Comment = String

type Inline = Bool

data Fun

Constructors

Fun

Fields

funInline :: Inline

funName :: Var

funQName :: Maybe QName

funComment :: Comment

funArgs :: [Var]

funExpr :: Expr

EpicFun

Fields

funName :: Var

funQName :: Maybe QName

funComment :: Comment

funEpicCode :: String

Instances

Eq Fun

Ord Fun

Show Fun

data Lit

Constructors

LInt Integer

LChar Char

LString String

LFloat Double

Instances

Eq Lit

Ord Lit

Show Lit

data Expr

Constructors

Var Var

Lit Lit

Lam Var Expr

Con Tag QName [Expr]

App Var [Expr]

Case Expr [Branch]

If Expr Expr Expr

Let Var Expr Expr

Lazy Expr

UNIT

IMPOSSIBLE

Instances

Eq Expr

Ord Expr

Show Expr

data Branch

Constructors

Branch

Fields

brTag :: Tag

brName :: QName

brVars :: [Var]

brExpr :: Expr

BrInt

Fields

brInt :: Int

brExpr :: Expr

Default

Fields

brExpr :: Expr

Instances

Eq Branch

Ord Branch

Show Branch

getBrVars :: Branch -> [Var]

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

substBranch :: Var -> Var -> Branch -> Branch

fv :: Expr -> [Var]

Get the free variables in an expression