Change constructors and cases on builtins and natish datatypes to use primitive data
- data PrimTransform = PrimTF {}
- primitivise :: MonadTCM m => [Fun] -> Compile m [Fun]
- primLists :: MonadTCM m => Compile m [Fun]
- getBuiltins :: MonadTCM m => Compile m [PrimTransform]
- natPrimTF :: IrrFilter -> [QName] -> PrimTransform
- primNatCaseZS :: Expr -> Expr -> Var -> Expr -> Expr
- primNatCaseZD :: Expr -> Expr -> Expr -> Expr
- boolPrimTF :: [QName] -> PrimTransform
- primFun :: MonadTCM m => [PrimTransform] -> Fun -> Compile m Fun
- primExpr :: MonadTCM m => [PrimTransform] -> Expr -> Compile m Expr
Documentation
primitivise :: MonadTCM m => [Fun] -> Compile m [Fun]Source
Change constructors and cases on builtins and natish datatypes to use primitive data
primLists :: MonadTCM m => Compile m [Fun]Source
Create primitive functions if list constructors are marked as builtins
getBuiltins :: MonadTCM m => Compile m [PrimTransform]Source
Build transforms using the names of builtins
natPrimTF :: IrrFilter -> [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