Change constructors and cases on builtins and natish datatypes to use primitive data
- data PrimTransform = PrimTF {}
- prZero, prNatEquality, prPred, prFalse, prTrue, prSuc :: Var
- primitivise :: [Fun] -> Compile TCM [Fun]
- initialPrims :: Compile TCM ()
- getBuiltins :: Compile TCM [PrimTransform]
- 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
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
:: 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