Agda-2.3.0: 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 :: [Fun] -> Compile TCM [Fun]

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

initialPrims :: Compile TCM ()

Map primitive constructors to primitive tags

getBuiltins :: Compile TCM [PrimTransform]

Build transforms using the names of builtins

natPrimTF :: ForcedArgs -> [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 :: [PrimTransform] -> Fun -> Compile TCM Fun

Change all the primitives in the function using the PrimTransform

primExpr :: [PrimTransform] -> Expr -> Compile TCM Expr

Change all the primitives in an expression using PrimTransform