| Safe Haskell | None |
|---|
Agda.Compiler.Epic.Primitive
Description
Change constructors and cases on builtins and natish datatypes to use primitive data
- data PrimTransform = PrimTF {}
- prZero :: Var
- prNatEquality :: Var
- prPred :: Var
- prFalse :: Var
- prTrue :: Var
- prSuc :: Var
- primitivise :: [Fun] -> Compile TCM [Fun]
- initialPrims :: Compile TCM ()
- getBuiltins :: Compile TCM [PrimTransform]
- defName :: Term -> QName
- head'' :: [t] -> t -> t
- natPrimTF :: ForcedArgs -> [QName] -> PrimTransform
- primNatCaseZS :: Expr -> Expr -> Var -> Expr -> Expr
- primNatCaseZD :: Expr -> Expr -> Expr -> Expr
- boolPrimTF :: [QName] -> PrimTransform
- primFun :: [PrimTransform] -> Fun -> Compile TCM Fun
- primExpr :: [PrimTransform] -> Expr -> Compile TCM Expr
Documentation
data PrimTransform Source
primitivise :: [Fun] -> Compile TCM [Fun]Source
Change constructors and cases on builtins and natish datatypes to use primitive data
initialPrims :: Compile TCM ()Source
Map primitive constructors to primitive tags
getBuiltins :: Compile TCM [PrimTransform]Source
Build transforms using the names of builtins
natPrimTF :: ForcedArgs -> [QName] -> PrimTransformSource
Translation to primitive integer functions
Arguments
| :: Expr | Expression that is cased on |
| -> Expr | Expression for the zero branch |
| -> Var | Variable that is bound in suc branch |
| -> Expr | Expression used for suc branch |
| -> Expr | Result? |
Corresponds to a case for natural numbers
Corresponds to a case with a zero and default branch
boolPrimTF :: [QName] -> PrimTransformSource
Translation to primitive bool functions