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

- 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

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