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

Safe HaskellSafe-Infered

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

head'' :: [t] -> t -> tSource

natPrimTF :: ForcedArgs -> [QName] -> PrimTransformSource

Translation to primitive integer functions

primNatCaseZSSource

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

primNatCaseZDSource

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] -> PrimTransformSource

Translation to primitive bool functions

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

Change all the primitives in the function using the PrimTransform

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

Change all the primitives in an expression using PrimTransform