Agda.Compiler.Epic.AuxAST

Contents

• Some smart constructors
• Substitution

Description

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

Some smart constructors

Substitution