Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Compiler.Epic.Primitive
Description
Change constructors and cases on builtins and natish datatypes to use primitive data
Synopsis
data PrimTransform = PrimTF {
mapCon :: Map QName Var
translateCase :: Expr -> [Branch] -> Expr
}
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
data PrimTransform Source
Constructors
PrimTF
mapCon :: Map QName Var
translateCase :: Expr -> [Branch] -> Expr
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
primNatCaseZSSource
:: ExprExpression that is cased on
-> ExprExpression for the zero branch
-> VarVariable that is bound in suc branch
-> ExprExpression used for suc branch
-> ExprResult?
Corresponds to a case for natural numbers
primNatCaseZDSource
:: ExprExpression that is cased on
-> ExprZero branch
-> ExprDefault branch
-> ExprResult?
Corresponds to a case with a zero and default branch
boolPrimTF :: [QName] -> PrimTransformSource
Translation to primitive bool functions
primFun :: MonadTCM m => [PrimTransform] -> Fun -> Compile m FunSource
Change all the primitives in the function using the PrimTransform
primExpr :: MonadTCM m => [PrimTransform] -> Expr -> Compile m ExprSource
Change all the primitives in an expression using PrimTransform
Produced by Haddock version 2.6.1