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

Safe Haskell | None

Agda.Compiler.Epic.AuxAST

Contents

- Some smart constructors
- Substitution

Description

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

Synopsis

- type Comment = String
- type Inline = Bool
- data Fun
  - = Fun {
    - funInline :: Inline
    - funName :: Var
    - funQName :: Maybe QName
    - funComment :: Comment
    - funArgs :: [Var]
    - funExpr :: Expr
    }
  - | EpicFun {
    - funName :: Var
    - funQName :: Maybe QName
    - funComment :: Comment
    - funEpicCode :: String
    }
- data Lit
  - = LInt Integer
  - | LChar Char
  - | LString String
  - | LFloat Double
- data Expr
  - = 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
- data Branch
  - = Branch {
    - brTag :: Tag
    - brName :: QName
    - brVars :: [Var]
    - brExpr :: Expr
    }
  - | BrInt {
    - brInt :: Int
    - brExpr :: Expr
    }
  - | Default {
    - brExpr :: Expr
    }
- getBrVars :: Branch -> [Var]
- lett :: Var -> Expr -> Expr -> Expr
- lazy :: Expr -> Expr
- casee :: Expr -> [Branch] -> Expr
- apps :: Var -> [Expr] -> Expr
- subst :: Var -> Var -> Expr -> Expr
- substs :: [(Var, Var)] -> Expr -> Expr
- substBranch :: Var -> Var -> Branch -> Branch
- fv :: Expr -> [Var]

# 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