Ivory.Language

Kinds

data Area k

data Proc k

Types

class IvoryType t

class IvoryArea a

class IvoryVar t

class IvoryExpr t

data OpaqueType

Non-null References

class IvoryRef ref

type ConstRef

class IvoryStore a

type Ref

refToPtr

constRef

deref

store

refCopy

refZero

Stack Allocation

class IvoryInit e

data Init area

class IvoryZeroVal a

class IvoryZero area

iarray

data InitStruct sym

(.=)

istruct

local

SizeOf

class IvorySizeOf t

sizeOf

Nullable Pointers

type Ptr

nullPtr

Booleans

data IBool

true

false

Characters

data IChar

char

Constant strings

data IString

Dynamic bounded-length strings

class IvoryString a

Signed Integers

data Sint8

data Sint16

data Sint32

data Sint64

Unsigned Integers

data Uint8

data Uint16

data Uint32

data Uint64

Floating-point Numbers

data IFloat

data IDouble

isnan

isinf

roundF

ceilF

floorF

atan2F

ifloat

idouble

Effects

data Effects

data BreakEff

type family GetBreaks (effs :: Effects) :: BreakEff

type family AllowBreak (effs :: Effects) :: Effects

type family ClearBreak (effs :: Effects) :: Effects

noBreak

data ReturnEff

type family GetReturn (effs :: Effects) :: ReturnEff

type family ClearReturn (effs :: Effects) :: Effects

noReturn

data AllocEff

type family GetAlloc (effs :: Effects) :: AllocEff

type family ClearAlloc (effs :: Effects) :: Effects

noAlloc

type AllocEffects s

type ProcEffects s t

type NoEffects

Language

Monadic Interface

data Ivory eff a

data RefScope

Subexpression naming

assign

Constants

extern

inclSym

Arithmetic (operators from the Num class are also provided).

class IvoryIntegral a

(./)

Comparisons

class IvoryEq a

class IvoryOrd a

Boolean operators

iNot

(.&&)

(.||)

Bit operators

class IvoryBits a

extractByte

class BitSplit a b

class BitCast a b

class TwosComplementCast unsigned signed

Bit data

bit types

data Bits n

type Bit

data BitArray n a

type family BitRep (n :: Nat) :: *

repToBits

bitsToRep

zeroBits

bitLength

bitIx

bit data

class BitData a

data BitDataField a b

type BitDataRep a

bit data conversions

toBits

fromBits

toRep

fromRep

bit data field operations

setBitDataBit

clearBitDataBit

getBitDataField

setBitDataField

bit data operators

(#!)

(#.)

(#>)

bit actions

data BitDataM d a

runBits

withBits

withBitsRef

clear

setBit

clearBit

setField

bitToBool

boolToBit

External memory areas

data MemArea area

area

importArea

data ConstMemArea area

constArea

importConstArea

class IvoryAddrOf mem ref

Procedures

data Def proc

data ProcPtr sig

procPtr

proc

voidProc

importProc

data Body r

body

importFrom

Pre/Post-Conditions

requires

checkStored

ensures

ensures_

Assumption/Assertion statements

assert

assume

Structures

class IvoryStruct sym

data StructDef sym

(~>)

data Label sym field

type ASymbol s

Arrays

(!)

fromIx

toIx

data Ix n

ixSize

arrayLen

toCArray

type ANat n

fromTypeNat

Looping

for

times

breakOut

arrayMap

forever

upTo

downTo

Call

call

indirect

call_

indirect_

Conditional Branching

ifte_

(?)

withRef

Return

ret

retVoid

Type-safe casting.

class SafeCast from to

class RuntimeCast from to

class Default a

safeCast

castWith

castDefault

class SignCast from to

signCast

Module Definitions

data Module

moduleName

package

type ModuleDef

incl

depend

dependByName

defStruct

defStringType

defMemArea

defConstMemArea

private

public

Quasiquoters

ivory

ivoryFile

ivoryBlk

Utilities

data Proxy k t

comment