Agda-2.2.10: A dependently typed functional programming language and proof assistant Source code Contents Index

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] -> PrimTransform Source

Translation to primitive integer functions

primNatCaseZS Source

:: 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

primNatCaseZD Source

:: Expr Expression that is cased on -> Expr Zero branch -> Expr Default branch -> Expr Result? Corresponds to a case with a zero and default branch

boolPrimTF :: [QName] -> PrimTransform Source

Translation to primitive bool functions

primFun :: MonadTCM m => [PrimTransform] -> Fun -> Compile m Fun Source

Change all the primitives in the function using the PrimTransform

primExpr :: MonadTCM m => [PrimTransform] -> Expr -> Compile m Expr Source

Change all the primitives in an expression using PrimTransform

Produced by Haddock version 2.6.1