Agda-2.2.10: A dependently typed functional programming language and proof assistant

Agda.Compiler.Epic.Primitive

Description

Change constructors and cases on builtins and natish datatypes to use primitive data

Synopsis

Documentation

data PrimTransform

Constructors

PrimTF 

Fields

mapCon :: Map QName Var
 
translateCase :: Expr -> [Branch] -> Expr
 

primitivise :: MonadTCM m => [Fun] -> Compile m [Fun]

Change constructors and cases on builtins and natish datatypes to use primitive data

primLists :: MonadTCM m => Compile m [Fun]

Create primitive functions if list constructors are marked as builtins

getBuiltins :: MonadTCM m => Compile m [PrimTransform]

Build transforms using the names of builtins

natPrimTF :: IrrFilter -> [QName] -> PrimTransform

Translation to primitive integer functions

primNatCaseZS

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

primNatCaseZD

Arguments

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

Translation to primitive bool functions

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

Change all the primitives in the function using the PrimTransform

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

Change all the primitives in an expression using PrimTransform