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

Safe HaskellNone
LanguageHaskell98

Agda.Compiler.Epic.Primitive

Description

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

Synopsis

Documentation

data PrimTransform Source

Constructors

PrimTF 

Fields

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

primitivise :: [Fun] -> Compile TCM [Fun] Source

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

initialPrims :: Compile TCM () Source

Map primitive constructors to primitive tags

getBuiltins :: Compile TCM [PrimTransform] Source

Build transforms using the names of builtins

natPrimTF :: ForcedArgs -> [QName] -> PrimTransform Source

Translation to primitive integer functions

primNatCaseZS Source

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 Source

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 Source

Translation to primitive bool functions

primFun :: [PrimTransform] -> Fun -> Compile TCM Fun Source

Change all the primitives in the function using the PrimTransform

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

Change all the primitives in an expression using PrimTransform