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

Agda.Compiler.Epic.AuxAST

Description

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

Synopsis

Documentation

type Var = String

type Tag = Int

type Inline = Bool

data Fun

Constructors

Fun 
EpicFun 

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

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

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.