ivory-0.1.0.3: Safe embedded C programming.

Safe HaskellNone
LanguageHaskell2010

Ivory.Language

Contents

Synopsis

Kinds

data Area k Source

The kind of memory-area types.

Constructors

Struct Symbol 
Array Nat (Area k) 
CArray (Area k) 
Stored k

This is lifting for a *-kinded type

data Proc k Source

The kind of procedures.

Constructors

[k] :-> k 

Types

class IvoryType t Source

The connection between Haskell and Ivory types.

Minimal complete definition

ivoryType

Instances

class IvoryArea a Source

Guard the inhabitants of the Area type, as not all *s are Ivory *s.

Minimal complete definition

ivoryArea

Instances

IvoryType a => IvoryArea (Stored * a) Source 
(ANat len, IvoryArea area) => IvoryArea (Array * len area) Source 

class IvoryType t => IvoryVar t Source

Lifting a variable name.

Minimal complete definition

wrapVar, unwrapExpr

Instances

class IvoryVar t => IvoryExpr t Source

Unwrapping for Ivory expressions.

Minimal complete definition

wrapExpr

Instances

data OpaqueType Source

An opaque type that can never be implemented.

Instances

Non-null References

class IvoryRef ref Source

Minimal complete definition

unwrapRef

Instances

data ConstRef s a Source

Instances

class IvoryVar a => IvoryStore a Source

Things that can be safely stored in references.

Instances

data Ref s a Source

A non-null pointer to a memory area.

Instances

refToPtr :: IvoryArea area => Ref s area -> Ptr s area Source

Convert a reference to a pointer. This direction is safe as we know that the reference is a non-null pointer.

constRef :: IvoryArea area => Ref s area -> ConstRef s area Source

Turn a reference into a constant reference.

deref :: forall eff ref s a. (IvoryStore a, IvoryVar a, IvoryVar (ref s (Stored a)), IvoryRef ref) => ref s (Stored a) -> Ivory eff a Source

Dereferenceing.

store :: forall eff s a. IvoryStore a => Ref s (Stored a) -> a -> Ivory eff () Source

refCopy :: forall eff sTo ref sFrom a. (IvoryRef ref, IvoryVar (Ref sTo a), IvoryVar (ref sFrom a), IvoryArea a) => Ref sTo a -> ref sFrom a -> Ivory eff () Source

Memory copy. Emits an assertion that the two references are unequal.

Stack Allocation

class IvoryVar e => IvoryInit e where Source

Initializers for Stored things.

Minimal complete definition

Nothing

Methods

ival :: e -> Init (Stored e) Source

Instances

data Init area Source

class IvoryVar a => IvoryZeroVal a where Source

Methods

izeroval :: Init (Stored a) Source

Instances

class IvoryZero area where Source

Zero initializers. The semantics of Ivory is that initializers must be compatible with C semantics of initializing to 0 for globals in .bss.

Methods

izero :: Init area Source

Instances

IvoryStruct sym => IvoryZero (Struct * sym) Source 
IvoryZeroVal a => IvoryZero (Stored * a) Source 
(IvoryZero area, IvoryArea area, ANat len) => IvoryZero (Array * len area) Source 

iarray :: forall len area. (IvoryArea area, ANat len) => [Init area] -> Init (Array len area) Source

data InitStruct sym Source

Instances

(.=) :: Label sym area -> Init area -> InitStruct sym Source

istruct :: forall sym. IvoryStruct sym => [InitStruct sym] -> Init (Struct sym) Source

local :: forall eff s area. (IvoryArea area, GetAlloc eff ~ Scope s) => Init area -> Ivory eff (Ref (Stack s) area) Source

Stack allocation

SizeOf

class IvorySizeOf t Source

Instances

IvorySizeOf (Struct * sym) Source 
IvoryType area => IvorySizeOf (Stored * area) Source 
(ANat len, IvorySizeOf area) => IvorySizeOf (Array * len area) Source 

sizeOf :: (IvoryArea t, IvorySizeOf t, IvoryExpr a, Num a) => Proxy t -> a Source

Get the size of an ivory type.

Nullable Pointers

data Ptr s a Source

Pointers (nullable references).

Instances

IvoryArea area => IvoryExpr (Ptr s area) Source 
IvoryArea area => IvoryVar (Ptr s area) Source 
IvoryArea area => IvoryType (Ptr s area) Source 
IvoryArea area => IvoryEq (Ptr s area) Source 
IvoryArea a => IvoryStore (Ptr Global a) Source 
IvoryArea area => IvoryZeroVal (Ptr Global area) Source 
IvoryArea area => IvoryInit (Ptr Global area) Source 

nullPtr :: IvoryArea area => Ptr s area Source

Booleans

data IBool Source

Instances

true :: IBool Source

false :: IBool Source

Characters

data IChar Source

Instances

char :: Char -> IChar Source

Constant strings

data IString Source

Instances

Dynamic bounded-length strings

class (ANat (Capacity a), IvoryStruct (StructName a), IvoryArea a, a ~ Struct (StructName a)) => IvoryString a where Source

Associated Types

type Capacity a :: Nat Source

Methods

stringDataL :: Label (StructName a) (Array (Capacity a) (Stored Uint8)) Source

stringLengthL :: Label (StructName a) (Stored IxRep) Source

Signed Integers

data Sint8 Source

8-bit integers.

Instances

data Sint16 Source

16-bit integers.

Instances

data Sint32 Source

32-bit integers.

Instances

data Sint64 Source

64-bit integers.

Instances

Unsigned Integers

data Uint8 Source

8-bit words.

Instances

data Uint16 Source

16-bit words.

Instances

data Uint32 Source

32-bit words.

Instances

data Uint64 Source

64-bit words.

Instances

Floating-point Numbers

data IFloat Source

Instances

data IDouble Source

Instances

isnan :: forall a. (IvoryVar a, Floating a) => a -> IBool Source

NaN testing.

isinf :: forall a. (IvoryVar a, Floating a) => a -> IBool Source

Infinite testing.

roundF :: IvoryFloat a => a -> a Source

Round a floating point number.

ceilF :: IvoryFloat a => a -> a Source

Take the ceiling of a floating point number.

floorF :: IvoryFloat a => a -> a Source

Take the floor of a floating point number.

atan2F :: IvoryFloat a => a -> a -> a Source

The arctangent function of two arguments.

ifloat :: Float -> IFloat Source

idouble :: Double -> IDouble Source

Effects

data Effects Source

The effect context for Ivory operations.

Constructors

Effects ReturnEff BreakEff AllocEff 

data BreakEff Source

Loop break effect.

Constructors

Break 
NoBreak 

type family GetBreaks effs :: BreakEff Source

Retrieve any Breaks effect present.

Instances

type GetBreaks (Effects r b a) = b Source 

type family AllowBreak effs :: Effects Source

Add the Break effect into an effect context.

Instances

type AllowBreak (Effects r b a) = Effects r Break a Source 

type family ClearBreak effs :: Effects Source

Remove any Break effect present.

Instances

type ClearBreak (Effects r b a) = Effects r NoBreak a Source 

noBreak :: Ivory (ClearBreak eff) a -> Ivory eff a Source

data ReturnEff Source

Function return effect.

Constructors

forall t . Returns t 
NoReturn 

type family GetReturn effs :: ReturnEff Source

Retrieve any Return effect present.

Instances

type GetReturn (Effects r b a) = r Source 

type family ClearReturn effs :: Effects Source

Remove any Return effects present.

Instances

noReturn :: Ivory (ClearReturn eff) a -> Ivory eff a Source

data AllocEff Source

Stack allocation effect.

Constructors

forall s . Scope s 
NoAlloc 

type family GetAlloc effs :: AllocEff Source

Retrieve the current allocation effect.

Instances

type GetAlloc (Effects r b a) = a Source 

type family ClearAlloc effs :: Effects Source

Remove any allocation effect currently present.

Instances

type ClearAlloc (Effects r b a) = Effects r b NoAlloc Source 

noAlloc :: (innerEff ~ ClearAlloc outerEff) => Ivory innerEff a -> Ivory outerEff a Source

type AllocEffects s = Effects NoReturn NoBreak (Scope s) Source

type ProcEffects s t = Effects (Returns t) NoBreak (Scope s) Source

type NoEffects = Effects NoReturn NoBreak NoAlloc Source

Language

Monadic Interface

data Ivory eff a Source

Instances

Monad (Ivory eff) Source 
Functor (Ivory eff) Source 
Applicative (Ivory eff) Source 
FreshName (Ivory eff) Source 
IvoryType r => IvoryCall_ ((:->) * ([] *) r) eff (Ivory eff ()) Source 
IvoryVar r => IvoryCall ((:->) * ([] *) r) eff (Ivory eff r) Source 

data RefScope Source

Definition scopes for values.

Constructors

Global

Globally allocated

forall s . Stack s

Stack allocated

Subexpression naming

assign :: forall eff a. IvoryExpr a => a -> Ivory eff a Source

Sub-expression naming.

Constants

extern :: forall t. IvoryExpr t => Sym -> String -> t Source

Import an externally defined constant by providing a global name.

inclSym :: IvoryExpr t => t -> ModuleDef Source

Import an externally-defined symbol.

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

class (IvoryExpr a, IvoryOrd a, Num a) => IvoryIntegral a where Source

Integral, without the baggage from Haskell (i.e., supertypes of Real and Enum). Defines Euclidian division (rather than truncated division). See http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.74.8522. Notable properties, beyond the normal div/rem properties, are that

The remainder is always non-negative. For d1 < 0, d0 iDiv (-d1) == -(d0 iDiv d1). For d1 < 0, d0 .% (-d1) == d0 .% d1.

N.B. mod and rem are equal if both args are positive, and C has no mod operator (only rem). In Haskell and C, both mod and rem may return negative values. Furthermore, before C99, the result of rem is implementation-defined.

Minimal complete definition

Nothing

Methods

iDiv :: a -> a -> a Source

Euclidean division.

(.%) :: a -> a -> a Source

Euclidean remainder.

Instances

(./) :: IvoryIntegral a => a -> a -> a Source

Comparisons

class IvoryExpr a => IvoryEq a where Source

Minimal complete definition

Nothing

Methods

(==?) :: a -> a -> IBool infix 4 Source

(/=?) :: a -> a -> IBool infix 4 Source

Instances

class IvoryEq a => IvoryOrd a where Source

Minimal complete definition

Nothing

Methods

(>?) :: a -> a -> IBool infix 4 Source

(>=?) :: a -> a -> IBool infix 4 Source

(<?) :: a -> a -> IBool infix 4 Source

(<=?) :: a -> a -> IBool infix 4 Source

Instances

Boolean operators

iNot :: IBool -> IBool Source

(.&&) :: IBool -> IBool -> IBool infixr 3 Source

(.||) :: IBool -> IBool -> IBool infixr 2 Source

Bit operators

class (Num a, IvoryExpr a) => IvoryBits a where Source

Minimal complete definition

iBitSize

Methods

(.&) :: a -> a -> a Source

(.|) :: a -> a -> a Source

(.^) :: a -> a -> a Source

iComplement :: a -> a Source

iBitSize :: a -> Int Source

iShiftL :: a -> a -> a Source

iShiftR :: a -> a -> a Source

Instances

extractByte :: BitCast a Uint8 => a -> (Uint8, a) Source

Extract the least significant byte from an integer. This returns the two values (x & 0xFF, x >> 8), with the first value safely casted to an 8-bit integer.

This is convenient to use with a state monad and "sets", such as:

fst $ runState x $ do
  a <- sets extractByte
  b <- sets extractByte
  return (a, b)

class (IvoryBits a, IvoryBits b) => BitSplit a b | a -> b where Source

Extraction of the upper or lower half of a bit type into the next smallest bit type.

Methods

ubits :: a -> b Source

lbits :: a -> b Source

Instances

class (IvoryBits a, IvoryBits b) => BitCast a b where Source

A narrowing cast from one bit type to another. This explicitly discards the upper bits of the input value to return a smaller type, and is only defined for unsigned integers.

Methods

bitCast :: a -> b Source

Instances

class (IvoryBits unsigned, IvoryEq unsigned, IvoryExpr signed, Num signed, IvoryIntegral unsigned, Bounded unsigned, Bounded signed, IvoryOrd signed) => TwosComplementCast unsigned signed | signed -> unsigned, unsigned -> signed where Source

Re-interpret the bits of an unsigned integer as though they were a signed number in two's complement representation.

Minimal complete definition

Nothing

Methods

twosComplementCast :: unsigned -> signed Source

twosComplementRep :: signed -> unsigned Source

Instances

Bit data

bit types

data Bits n Source

A wrapper for an Ivory type that can hold an "n" bit unsigned integer.

Instances

IvoryRep (BitRep n) => IvoryExpr (Bits n) Source 
IvoryRep (BitRep n) => IvoryVar (Bits n) Source 
IvoryRep (BitRep n) => IvoryType (Bits n) Source 
IvoryRep (BitRep n) => IvoryEq (Bits n) Source 
IvoryRep (BitRep n) => IvoryStore (Bits n) Source 
IvoryRep (BitRep n) => IvoryZeroVal (Bits n) Source 
IvoryRep (BitRep n) => IvoryInit (Bits n) Source 
(ANat n, IvoryRep (BitRep n)) => BitData (Bits n) Source

Identity instance of BitData for the base "Bits n" type.

type BitSize (Bits n) = n Source 
type BitType (Bits n) = Bits n Source 

type Bit = Bits 1 Source

Bit is a type alias for "Bits 1".

data BitArray n a Source

An array of "n" bit data elements of type "a".

Instances

(ANat n, ANat (ArraySize n a), BitData a, IvoryRep (BitRep (ArraySize n a))) => BitData (BitArray n a) Source 
type BitType (BitArray n a) = Bits (ArraySize n a) Source 

type family BitRep n :: * Source

Type function: "BitRep (n :: Nat)" returns an Ivory type given a bit size as a type-level natural. Instances of this type family for bits [1..64] are generated using Template Haskell.

Instances

type BitRep 1 = Uint8 Source 
type BitRep 2 = Uint8 Source 
type BitRep 3 = Uint8 Source 
type BitRep 4 = Uint8 Source 
type BitRep 5 = Uint8 Source 
type BitRep 6 = Uint8 Source 
type BitRep 7 = Uint8 Source 
type BitRep 8 = Uint8 Source 
type BitRep 9 = Uint16 Source 
type BitRep 10 = Uint16 Source 
type BitRep 11 = Uint16 Source 
type BitRep 12 = Uint16 Source 
type BitRep 13 = Uint16 Source 
type BitRep 14 = Uint16 Source 
type BitRep 15 = Uint16 Source 
type BitRep 16 = Uint16 Source 
type BitRep 17 = Uint32 Source 
type BitRep 18 = Uint32 Source 
type BitRep 19 = Uint32 Source 
type BitRep 20 = Uint32 Source 
type BitRep 21 = Uint32 Source 
type BitRep 22 = Uint32 Source 
type BitRep 23 = Uint32 Source 
type BitRep 24 = Uint32 Source 
type BitRep 25 = Uint32 Source 
type BitRep 26 = Uint32 Source 
type BitRep 27 = Uint32 Source 
type BitRep 28 = Uint32 Source 
type BitRep 29 = Uint32 Source 
type BitRep 30 = Uint32 Source 
type BitRep 31 = Uint32 Source 
type BitRep 32 = Uint32 Source 
type BitRep 33 = Uint64 Source 
type BitRep 34 = Uint64 Source 
type BitRep 35 = Uint64 Source 
type BitRep 36 = Uint64 Source 
type BitRep 37 = Uint64 Source 
type BitRep 38 = Uint64 Source 
type BitRep 39 = Uint64 Source 
type BitRep 40 = Uint64 Source 
type BitRep 41 = Uint64 Source 
type BitRep 42 = Uint64 Source 
type BitRep 43 = Uint64 Source 
type BitRep 44 = Uint64 Source 
type BitRep 45 = Uint64 Source 
type BitRep 46 = Uint64 Source 
type BitRep 47 = Uint64 Source 
type BitRep 48 = Uint64 Source 
type BitRep 49 = Uint64 Source 
type BitRep 50 = Uint64 Source 
type BitRep 51 = Uint64 Source 
type BitRep 52 = Uint64 Source 
type BitRep 53 = Uint64 Source 
type BitRep 54 = Uint64 Source 
type BitRep 55 = Uint64 Source 
type BitRep 56 = Uint64 Source 
type BitRep 57 = Uint64 Source 
type BitRep 58 = Uint64 Source 
type BitRep 59 = Uint64 Source 
type BitRep 60 = Uint64 Source 
type BitRep 61 = Uint64 Source 
type BitRep 62 = Uint64 Source 
type BitRep 63 = Uint64 Source 
type BitRep 64 = Uint64 Source 

repToBits :: forall n. (ANat n, IvoryRep (BitRep n)) => BitRep n -> Bits n Source

Convert an Ivory value to a bit value. If the input value contains out of range bits, they will be ignored.

bitsToRep :: Bits n -> BitRep n Source

Convert a bit value to an Ivory value.

zeroBits :: IvoryRep (BitRep n) => Bits n Source

Return a bit value of all zeros of the given size.

bitLength :: forall a n. ANat n => BitArray n a -> Int Source

Return the number of elements in a BitArray.

bitIx :: forall a n. (BitData a, ANat n, ANat (BitSize a), ANat (ArraySize n a)) => Int -> BitDataField (BitArray n a) a Source

Return a BitDataField that accesses the "n"th element of a BitArray. This can be composed with other field accessors using "#>".

bit data

class (ANat (BitSize (BitType a)), IvoryRep (BitDataRep a), BitType a ~ Bits (BitSize (BitType a))) => BitData a where Source

Class of bit data types defined by the "bitdata" quasiquoter.

Methods

toBits :: a -> BitType a Source

Convert a bit data type to its raw bit value. This is always well defined and should be exported.

fromBits :: BitType a -> a Source

Convert a raw bit value to a bit data type. All values may not be well defined with respect to the original set of bit data constructors. For now, we allow these "junk" values to be created, but that may change in the future (perhaps by implementing a checked, Ivory run-time conversion).

Instances

(ANat n, IvoryRep (BitRep n)) => BitData (Bits n) Source

Identity instance of BitData for the base "Bits n" type.

(ANat n, ANat (ArraySize n a), BitData a, IvoryRep (BitRep (ArraySize n a))) => BitData (BitArray n a) Source 

data BitDataField a b Source

Description of a bit field defined by the "bitdata" quasiquoter. Each field defined in the record syntax will generate a top-level definition of BitDataField.

This constructor must remain unexported so that only fields checked by the quasiquoter are created.

Instances

type BitDataRep a = BitRep (BitSize (BitType a)) Source

The Ivory type that stores the actual value for a bit data type.

This is a shorthand to simplify the constraints on functions that take arguments of the BitData class.

bit data conversions

toRep :: BitData a => a -> BitDataRep a Source

Convert a bit data value to its Ivory representation.

fromRep :: BitData a => BitDataRep a -> a Source

Convert a raw Ivory type to a bit data type. If the input value is too large, the out of range upper bits will be masked off.

bit data field operations

setBitDataBit :: BitData a => BitDataField a Bit -> a -> a Source

Set a single-bit field in a bit data value.

clearBitDataBit :: BitData a => BitDataField a Bit -> a -> a Source

Clear a single-bit field in a bit data value.

getBitDataField :: (BitData a, BitData b, BitCast (BitDataRep a) (BitDataRep b)) => BitDataField a b -> a -> b Source

Extract a field from a bit data definition. Returns the value as the type defined on the right hand side of the field definition in the "bitdata" quasiquoter.

setBitDataField :: (BitData a, BitData b, SafeCast (BitDataRep b) (BitDataRep a)) => BitDataField a b -> a -> b -> a Source

Set a field from a bit data definition.

bit data operators

(#!) :: forall a n. (BitData a, ANat n, ANat (BitSize a), ANat (ArraySize n a), BitCast (BitRep (ArraySize n a)) (BitDataRep a), IvoryRep (BitRep (ArraySize n a))) => BitArray n a -> Int -> a Source

Return the "n"th element of a BitArray.

(#.) :: (BitData a, BitData b, BitCast (BitDataRep a) (BitDataRep b)) => a -> BitDataField a b -> b Source

Infix operator to read a bit data field. (like Data.Lens.^.)

(#>) :: BitDataField a b -> BitDataField b c -> BitDataField a c Source

Bit data field composition. (like Control.Category.>>>)

bit actions

data BitDataM d a Source

An action that modifies a bit data value of type "d" and returns a "a" in the "Ivory s r" monad. Values of this type are passed as the "body" argument to "withBits" etc.

Instances

runBits :: BitData d => BitDataRep d -> BitDataM d a -> (a, BitDataRep d, [String]) Source

Execute a bitdata action given an initial value, returning the new bitdata value and the result of the action.

withBits :: BitData d => BitDataRep d -> BitDataM d () -> BitDataRep d Source

Execute a bitdata action given an initial value, returning the new bitdata value.

withBitsRef :: BitData d => Ref s1 (Stored (BitDataRep d)) -> BitDataM d a -> Ivory eff a Source

Execute a bit data action given a reference to a value, writing the resulting value back to the reference upon completion and returning the result of the action.

clear :: BitData d => BitDataM d () Source

Clear the value of the current bit data value.

setBit :: BitData d => BitDataField d Bit -> BitDataM d () Source

Set a single bit field in the current bit data value.

clearBit :: BitData d => BitDataField d Bit -> BitDataM d () Source

Clear a single bit.

setField :: (BitData d, BitData b, SafeCast (BitDataRep b) (BitDataRep d)) => BitDataField d b -> b -> BitDataM d () Source

Set a field to a value.

bitToBool :: Bit -> IBool Source

Convert a single bit bitdata to an Ivory boolean.

boolToBit :: IBool -> Bit Source

Convert an Ivory boolean to a single bit.

External memory areas

data MemArea area Source

Externally defined memory areas.

Instances

area :: forall area. (IvoryArea area, IvoryZero area) => Sym -> Maybe (Init area) -> MemArea area Source

Define a global constant. Requires an IvoryZero constraint to ensure the area has an initializers, but does not explicilty initialize to 0 so that the value is placed in the .bss section.

importArea :: IvoryArea area => Sym -> String -> MemArea area Source

Import an external symbol from a header.

data ConstMemArea area Source

Instances

constArea :: forall area. IvoryArea area => Sym -> Init area -> ConstMemArea area Source

Constant memory area definition.

importConstArea :: IvoryArea area => Sym -> String -> ConstMemArea area Source

Import an external symbol from a header.

class IvoryAddrOf mem ref | mem -> ref, ref -> mem where Source

Turn a memory area into a reference.

Methods

addrOf :: IvoryArea area => mem area -> ref Global area Source

Instances

Procedures

data Def proc Source

Procedure definitions.

Instances

Eq (Def proc) Source 
Ord (Def proc) Source 
Show (Def proc) Source 
ProcType proc => IvoryType (Def proc) Source 

data ProcPtr sig Source

Procedure pointers

Instances

ProcType proc => IvoryVar (ProcPtr proc) Source 
ProcType proc => IvoryType (ProcPtr proc) Source 
ProcType proc => IvoryInit (ProcPtr proc) Source 

procPtr :: ProcType sig => Def sig -> ProcPtr sig Source

proc :: forall proc impl. IvoryProcDef proc impl => Sym -> impl -> Def proc Source

Procedure definition.

voidProc :: IvoryProcDef (args :-> ()) impl => Sym -> impl -> Def (args :-> ()) Source

Type inference can usually determine the argument types of an Ivory procedure, but for void procedures there's often nothing to constrain the return type. This function is a type-constrained version of proc that just forces the return type to be '()'.

importProc :: forall proc. ProcType proc => Sym -> String -> Def proc Source

Import a function from a C header.

data Body r Source

Instances

WrapIvory Body Source 
IvoryType ret => IvoryProcDef ((:->) * ([] *) ret) (Body ret) Source 
type Return Body = () Source 

body :: IvoryType r => (forall s. Ivory (ProcEffects s r) ()) -> Body r Source

importFrom :: String -> ImportFrom a Source

Pre/Post-Conditions

requires :: (Requires c, WrapIvory m, IvoryType r) => c -> m r -> m r Source

checkStored :: (CheckStored c, IvoryVar a, IvoryRef ref, IvoryVar (ref s (Stored a))) => ref s (Stored a) -> (a -> c) -> Cond Source

ensures :: (Ensures c, WrapIvory m, IvoryVar r) => (r -> c) -> m r -> m r Source

ensures_ :: (Ensures c, WrapIvory m) => c -> m () -> m () Source

Assumption/Assertion statements

assert :: forall a eff. IvoryExpr a => a -> Ivory eff () Source

assume :: forall a eff. IvoryExpr a => a -> Ivory eff () Source

Structures

class (IvoryArea (Struct sym), ASymbol sym) => IvoryStruct sym where Source

Methods

structDef :: StructDef sym Source

data StructDef sym Source

(~>) :: forall ref s sym field. (IvoryStruct sym, IvoryRef ref, IvoryExpr (ref s (Struct sym)), IvoryExpr (ref s field)) => ref s (Struct sym) -> Label sym field -> ref s field Source

Label indexing in a structure.

data Label sym field Source

Struct field labels.

Instances

Eq (Label sym field) Source 

type ASymbol s = KnownSymbol s Source

Arrays

(!) :: forall s len area ref. (ANat len, IvoryArea area, IvoryRef ref, IvoryExpr (ref s (Array len area)), IvoryExpr (ref s area)) => ref s (Array len area) -> Ix len -> ref s area Source

Array indexing.

fromIx :: ANat n => Ix n -> IxRep Source

toIx :: forall a n. (SafeCast a IxRep, ANat n) => a -> Ix n Source

Casting from a bounded Ivory expression to an index. This is safe, although the value may be truncated. Furthermore, indexes are always positive.

data Ix n Source

Values in the range 0 .. n-1.

Instances

ANat n => Num (Ix n) Source 
ANat n => IvoryExpr (Ix n) Source 
ANat n => IvoryVar (Ix n) Source 
ANat n => IvoryType (Ix n) Source 
ANat n => IvoryOrd (Ix n) Source 
ANat n => IvoryEq (Ix n) Source 
ANat n => IvoryStore (Ix n) Source 
ANat n => IvoryZeroVal (Ix n) Source 
ANat len => IvoryInit (Ix len) Source 
(ANat n, IvoryIntegral to, Default to) => SafeCast (Ix n) to Source 

ixSize :: forall n. ANat n => Ix n -> Integer Source

The number of elements that an index covers.

arrayLen :: forall s len area n ref. (Num n, ANat len, IvoryArea area, IvoryRef ref) => ref s (Array len area) -> n Source

toCArray :: forall s len area rep ref. (ANat len, ToCArray area rep, IvoryRef ref, IvoryExpr (ref s (Array len area)), IvoryExpr (ref s (CArray rep))) => ref s (Array len area) -> ref s (CArray rep) Source

Convert from a checked array to one that can be given to a c function.

type ANat n = KnownNat n Source

fromTypeNat :: KnownNat i => proxy (i :: Nat) -> Integer Source

The integer associated with a type-nat.

Looping

for :: forall eff n a. ANat n => Ix n -> (Ix n -> Ivory (AllowBreak eff) a) -> Ivory eff () Source

Run the computation n times, where n :: Ix m, 0 <= n <= m. Indexes increment from 0 to n-1 inclusively.

times :: forall eff n a. ANat n => Ix n -> (Ix n -> Ivory (AllowBreak eff) a) -> Ivory eff () Source

Run the computation n times, where n :: Ix m, 0 <= n <= m. Indexes decrement from n-1 to 0 inclusively.

breakOut :: (GetBreaks eff ~ Break) => Ivory eff () Source

arrayMap :: forall eff n a. ANat n => (Ix n -> Ivory (AllowBreak eff) a) -> Ivory eff () Source

forever :: Ivory (AllowBreak eff) () -> Ivory eff () Source

Call

call :: forall proc eff impl. IvoryCall proc eff impl => Def proc -> impl Source

Direct calls.

indirect :: forall proc eff impl. IvoryCall proc eff impl => ProcPtr proc -> impl Source

Indirect calls.

call_ :: forall proc eff impl. IvoryCall_ proc eff impl => Def proc -> impl Source

Direct calls, ignoring the result.

indirect_ :: forall proc eff impl. IvoryCall_ proc eff impl => ProcPtr proc -> impl Source

Indirect calls, ignoring the result.

Conditional Branching

ifte_ :: IBool -> Ivory eff a -> Ivory eff b -> Ivory eff () Source

If-then-else.

(?) :: IvoryExpr a => IBool -> (a, a) -> a Source

Conditional expressions.

withRef :: IvoryArea area => Ptr as area -> (Ref as area -> Ivory eff t) -> Ivory eff f -> Ivory eff () Source

Unwrap a pointer, and use it as a reference.

Return

ret :: (GetReturn eff ~ Returns r, IvoryVar r) => r -> Ivory eff () Source

Primitive return from function.

retVoid :: (GetReturn eff ~ Returns ()) => Ivory eff () Source

Primitive void return from function.

Type-safe casting.

class (IvoryExpr from, IvoryExpr to) => SafeCast from to where Source

Statically safe casts.

Minimal complete definition

Nothing

Methods

safeCast :: from -> to Source

Instances

SafeCast Sint64 Sint64 Source 
SafeCast Sint64 IDouble Source 
SafeCast Sint32 Sint64 Source 
SafeCast Sint32 Sint32 Source 
SafeCast Sint32 IDouble Source 
SafeCast Sint32 IFloat Source 
SafeCast Sint16 Sint64 Source 
SafeCast Sint16 Sint32 Source 
SafeCast Sint16 Sint16 Source 
SafeCast Sint16 IDouble Source 
SafeCast Sint16 IFloat Source 
SafeCast Sint8 Sint64 Source 
SafeCast Sint8 Sint32 Source 
SafeCast Sint8 Sint16 Source 
SafeCast Sint8 Sint8 Source 
SafeCast Sint8 IDouble Source 
SafeCast Sint8 IFloat Source 
SafeCast Uint64 Uint64 Source 
SafeCast Uint64 IDouble Source 
SafeCast Uint32 Sint64 Source 
SafeCast Uint32 Uint64 Source 
SafeCast Uint32 Uint32 Source 
SafeCast Uint32 IDouble Source 
SafeCast Uint32 IFloat Source 
SafeCast Uint16 Sint64 Source 
SafeCast Uint16 Sint32 Source 
SafeCast Uint16 Uint64 Source 
SafeCast Uint16 Uint32 Source 
SafeCast Uint16 Uint16 Source 
SafeCast Uint16 IDouble Source 
SafeCast Uint16 IFloat Source 
SafeCast Uint8 Sint64 Source 
SafeCast Uint8 Sint32 Source 
SafeCast Uint8 Sint16 Source 
SafeCast Uint8 Uint64 Source 
SafeCast Uint8 Uint32 Source 
SafeCast Uint8 Uint16 Source 
SafeCast Uint8 Uint8 Source 
SafeCast Uint8 IDouble Source 
SafeCast Uint8 IFloat Source 
SafeCast IChar IChar Source 
SafeCast IBool Sint64 Source 
SafeCast IBool Sint32 Source 
SafeCast IBool Sint16 Source 
SafeCast IBool Sint8 Source 
SafeCast IBool Uint64 Source 
SafeCast IBool Uint32 Source 
SafeCast IBool Uint16 Source 
SafeCast IBool Uint8 Source 
SafeCast IBool IChar Source 
SafeCast IBool IBool Source 
SafeCast IBool IDouble Source 
SafeCast IBool IFloat Source 
SafeCast IDouble IDouble Source 
SafeCast IFloat IDouble Source 
SafeCast IFloat IFloat Source 
(ANat n, IvoryIntegral to, Default to) => SafeCast (Ix n) to Source 

class (IvoryExpr from, IvoryExpr to, Default to) => RuntimeCast from to Source

Casts requiring runtime checks.

Minimal complete definition

inBounds

Instances

(Bounded from, Bounded to, IvoryOrd from, IvoryOrd to, IvoryExpr from, IvoryExpr to, Default from, Default to, SafeCast to from) => RuntimeCast from to Source 
(Default to, Bounded to, IvoryIntegral to, SafeCast to IDouble) => RuntimeCast IDouble to Source 
(Default to, Bounded to, IvoryIntegral to, SafeCast to IFloat) => RuntimeCast IFloat to Source

Casting from a floating to a Integral type always results in truncation.

class Default a Source

Default values for expression types.

Minimal complete definition

defaultVal

Instances

castWith :: RuntimeCast from to => to -> from -> to Source

Cast with a default value if the casted value is too large.

castDefault :: (Default to, RuntimeCast from to) => from -> to Source

`CastWith 0` for types for which 0 is defined.

class (IvoryExpr from, IvoryExpr to) => SignCast from to where Source

SignCast takes a unsigned number into its signed form iff safe, otherwise 0, and same with signed into unsigned

Methods

signCast :: from -> to Source

Instances

Module Definitions

data Module Source

Instances

moduleName :: Module -> String Source

package :: String -> ModuleDef -> Module Source

Package the module up. Default visibility is public.

type ModuleDef = ModuleM () Source

incl :: Def a -> ModuleDef Source

Include a defintion in the module.

depend :: Module -> ModuleDef Source

Add a dependency on another module.

defStruct :: forall sym. (IvoryStruct sym, ASymbol sym) => Proxy sym -> ModuleDef Source

Include the definition of a structure in the module.

defStringType :: forall str. IvoryString str => Proxy str -> ModuleDef Source

Include the definition of a string type's structure.

defMemArea :: IvoryArea area => MemArea area -> ModuleDef Source

Include the definition of a memory area.

defConstMemArea :: IvoryArea area => ConstMemArea area -> ModuleDef Source

Include the definition of a constant memory area.

private :: ModuleDef -> ModuleDef Source

Start a block of definitions that should not be put in the header.

public :: ModuleDef -> ModuleDef Source

Start a block of definitions should be put in the header. This is the default, and this function is just included to complement private.

Quasiquoters

ivory :: QuasiQuoter Source

Quasiquoter for defining Ivory statements in C-like syntax. No module generated.

ivoryFile :: QuasiQuoter Source

Parse a file. Use

ivoryFile|foo.ivory|]

To parse file ```foo.ivory``` Generates a module definition by default with a module name that is constructed from the filename and path such that

"diradirbfoobar.ivory"

has a module name

diradirbfoobar

Like quoteFile except we also process the filename.

ivoryBlk :: QuasiQuoter Source

Quasiquoter for defining blocks of Ivory statements.

Utilities

data Proxy a Source

Constructors

Proxy 

comment :: String -> Ivory eff () Source

module Ivory.Language.Coroutine