Agda.Compiler.Epic.AuxAST

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

Documentation

type Var = String

type Tag = Int

type Comment = String

type Inline = Bool

data Fun

Constructors

Fun

Fields

funInline :: Inline

funName :: Var

funComment :: Comment

funArgs :: [Var]

funExpr :: Expr

EpicFun

Fields

funName :: Var

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

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

Smart constructor for applications to avoid empty applications

subst

Arguments

:: Var

Substitute this ...

-> Var

with this ...

-> Expr

in this.

-> Expr

Substitution

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

fv :: Expr -> [Var]

Get the free variables in an expression

pairwiseFilter :: [Bool] -> [a] -> [a]

Filter a list using a list of Bools specifying what to keep.