ivory-0.1.0.0: Safe embedded C programming.

Safe HaskellNone

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 IvoryArea a Source

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

Instances

IvoryType a => IvoryArea (Stored * a) 
IvoryArea a => IvoryArea (CArray * a) 
(IvoryStruct sym, SingI Symbol sym) => IvoryArea (Struct * sym) 
(SingI Nat len, IvoryArea area) => IvoryArea (Array * len area) 

data OpaqueType Source

An opaque type that can never be implemented.

Non-null References

data Ref s a Source

A non-null pointer to a memory area.

Instances

IvoryRef Ref 
IvoryAddrOf MemArea Ref 
IvoryArea area => IvoryExpr (Ref s area) 
IvoryArea area => IvoryVar (Ref s area) 
IvoryArea area => IvoryType (Ref s area) 

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

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 areaSource

Turn a reference into a constant reference.

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

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

data Init area Source

class IvoryZero area whereSource

Zero initializers.

Methods

izero :: Init areaSource

Instances

(Num a, IvoryInit a) => IvoryZero (Stored * a) 
IvoryZero (Stored * IChar) 
IvoryZero (Stored * IBool) 
IvoryArea area => IvoryZero (Stored * (Ptr Global area)) 
IvoryStruct sym => IvoryZero (Struct * sym) 
(IvoryZero area, IvoryArea area, SingI Nat len) => IvoryZero (Array * len area) 

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

data InitStruct sym Source

Instances

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

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

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

Get the size of an ivory type.

Nullable Pointers

data Ptr s a Source

Pointers (nullable references).

Instances

IvoryArea area => IvoryExpr (Ptr s area) 
IvoryArea area => IvoryVar (Ptr s area) 
IvoryArea area => IvoryType (Ptr s area) 
IvoryArea area => IvoryEq (Ptr s area) 
IvoryArea a => IvoryStore (Ptr Global a) 
IvoryArea area => IvoryInit (Ptr Global area) 
IvoryArea area => IvoryZero (Stored * (Ptr Global area)) 

nullPtr :: IvoryArea area => Ptr s areaSource

Booleans

Characters

Strings

Signed Integers

Unsigned Integers

Floating-point Numbers

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

NaN testing.

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

Infinite testing.

roundF :: IvoryFloat a => a -> aSource

Round a floating point number.

ceilF :: IvoryFloat a => a -> aSource

Take the ceiling of a floating point number.

floorF :: IvoryFloat a => a -> aSource

Take the floor of a floating point number.

Effects

data Effects Source

The effect context for Ivory operations.

data BreakEff Source

Loop break effect.

Constructors

Break 
NoBreak 

type family GetBreaks effs :: BreakEffSource

Retrieve any Breaks effect present.

type family AllowBreak effs :: EffectsSource

Add the Break effect into an effect context.

type family ClearBreak effs :: EffectsSource

Remove any Break effect present.

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

data ReturnEff Source

Function return effect.

Constructors

forall t . Returns t 
NoReturn 

type family GetReturn effs :: ReturnEffSource

Retrieve any Return effect present.

type family ClearReturn effs :: EffectsSource

Remove any Return effects present.

data AllocEff Source

Stack allocation effect.

Constructors

forall s . Scope s 
NoAlloc 

type family GetAlloc effs :: AllocEffSource

Retrieve the current allocation effect.

type family ClearAlloc effs :: EffectsSource

Remove any allocation effect currently present.

noAlloc :: innerEff ~ ClearAlloc outerEff => Ivory innerEff a -> Ivory outerEff aSource

Language

Monadic Interface

data Ivory eff a Source

Instances

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

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 aSource

Sub-expression naming.

Constants

extern :: IvoryExpr t => Sym -> tSource

Import and externally defined constant by providing a global name.

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

class (IvoryExpr a, Num a) => IvoryIntegral a whereSource

Integral, without the baggage from Haskell (i.e., supertypes of Real and Enum).

Methods

iDiv :: a -> a -> aSource

Has C semantics: like Haskell's quot (truncate towards 0).

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

Has C semantics: like Haskell's rem.

Comparisons

Boolean operators

Bit operators

class (Num a, IvoryExpr a) => IvoryBits a whereSource

Methods

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

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

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

iComplement :: a -> aSource

iShiftL :: a -> a -> aSource

iShiftR :: a -> a -> aSource

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 whereSource

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

Methods

ubits :: a -> bSource

lbits :: a -> bSource

class (IvoryBits a, IvoryBits b) => BitCast a b whereSource

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 -> bSource

External memory areas

data MemArea area Source

Externally defined memory areas.

area :: forall area. IvoryArea area => Sym -> Maybe (Init area) -> MemArea areaSource

Define a global constant.

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

Import an external symbol from a header.

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

Constant memory area definition.

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

Import an external symbol from a header.

class IvoryAddrOf mem ref | mem -> ref, ref -> mem whereSource

Turn a memory area into a reference.

Methods

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

Procedures

data Def proc Source

Procedure definitions.

Instances

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

data ProcPtr sig Source

Procedure pointers

Instances

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

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

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

Procedure definition.

externProc :: forall proc. ProcType proc => Sym -> Def procSource

External function reference.

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

Import a function from a C header.

data Body r Source

Instances

IvoryType ret => IvoryProcDef (:-> * ([] *) ret) (Body ret) 

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

Pre/Post-Conditions

requires :: (Requires c, IvoryType r) => c -> Body r -> Body rSource

checkStored :: forall ref s a. (IvoryVar a, IvoryRef ref, IvoryVar (ref s (Stored a))) => ref s (Stored a) -> (a -> IBool) -> CondSource

ensures :: (Ensures c, IvoryVar r) => (r -> c) -> Body r -> Body rSource

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), SingI sym) => IvoryStruct sym whereSource

Associated Types

type StructName a :: SymbolSource

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 fieldSource

Label indexing in a structure.

data Label sym field Source

Struct field labels.

Instances

Eq (Label sym field) 

Arrays

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

Array indexing.

fromIx :: SingI n => Ix n -> IxRepSource

toIx :: (IvoryExpr a, Bounded a, SingI n) => a -> Ix nSource

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

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

ixSize :: forall n. SingI n => Ix n -> IntegerSource

The number of elements that an index covers.

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

class SingI a

The class SingI provides a "smart" constructor for singleton types. There are built-in instances for the singleton types corresponding to type literals.

toCArray :: forall s len area rep ref. (SingI 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.

Strings

Looping

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

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

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

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

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

arrayMap :: forall eff n a. SingI 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 -> implSource

Direct calls.

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

Indirect calls.

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

Direct calls, ignoring the result.

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

Indirect calls, ignoring the result.

Conditional Branching

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

If-then-else.

(?) :: forall a. IvoryExpr a => IBool -> (a, a) -> aSource

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

Type-safe casting.

class (IvoryExpr from, IvoryExpr to) => SafeCast from to whereSource

Statically safe casts.

Methods

safeCast :: from -> toSource

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

Casts requiring runtime checks.

Instances

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

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

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

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

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

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

class (IvoryExpr from, IvoryExpr to) => SignCast from to whereSource

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

Methods

signCast :: from -> toSource

Module Definitions

package :: String -> ModuleDef -> ModuleSource

Package the module up. Default visibility is public.

incl :: Def a -> ModuleDefSource

Include a defintion in the module.

depend :: Module -> ModuleDefSource

Add a dependency on another module.

defStruct :: forall sym. (IvoryStruct sym, SingI sym) => Proxy sym -> ModuleDefSource

Include the definition of a structure in the module.

defStringType :: forall str. IvoryString str => Proxy str -> ModuleDefSource

Include the definition of a string type's structure.

defMemArea :: IvoryArea area => MemArea area -> ModuleDefSource

Include the definition of a memory area.

defConstMemArea :: IvoryArea area => ConstMemArea area -> ModuleDefSource

Include the definition of a constant memory area.

inclHeader :: String -> ModuleDefSource

Add a dependency on an external header.

private :: ModuleDef -> ModuleDefSource

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

public :: ModuleDef -> ModuleDefSource

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

sourceDep :: FilePath -> ModuleDefSource

Depend on an existing (object language) source file which should be copied to the user build tree as part of code generation

Utilities

data Proxy a Source

Constructors

Proxy