| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Ivory.Language
Contents
- data Area k
- data Proc k = [k] :-> k
- class IvoryType t
- class IvoryArea a
- class IvoryType t => IvoryVar t
- class IvoryVar t => IvoryExpr t
- data OpaqueType
- class IvoryRef ref
- type ConstRef = Pointer Valid Const
- class IvoryVar a => IvoryStore a
- type Ref = Pointer Valid Mutable
- refToPtr :: IvoryArea area => Ref s area -> Ptr s area
- constRef :: IvoryArea area => Ref s area -> ConstRef s area
- deref :: forall eff ref s a. (IvoryStore a, IvoryVar a, IvoryVar (ref s (Stored a)), IvoryRef ref) => ref s (Stored a) -> Ivory eff a
- store :: forall eff s a. IvoryStore a => Ref s (Stored a) -> a -> Ivory eff ()
- 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 ()
- refZero :: forall eff s a. (IvoryZero a, IvoryArea a) => Ref s a -> Ivory eff ()
- class IvoryVar e => IvoryInit e where
- data Init area
- class IvoryVar a => IvoryZeroVal a where
- class IvoryZero area where
- iarray :: forall len area. (IvoryArea area, ANat len) => [Init area] -> Init (Array len area)
- data InitStruct sym
- (.=) :: Label sym area -> Init area -> InitStruct sym
- istruct :: forall sym. IvoryStruct sym => [InitStruct sym] -> Init (Struct sym)
- local :: forall eff s area. (IvoryArea area, GetAlloc eff ~ Scope s) => Init area -> Ivory eff (Ref (Stack s) area)
- class IvorySizeOf t
- sizeOf :: (IvoryArea t, IvorySizeOf t, IvoryExpr a, Num a) => Proxy t -> a
- type Ptr = Pointer Nullable Mutable
- nullPtr :: IvoryArea a => Pointer Nullable c s a
- data IBool
- true :: IBool
- false :: IBool
- data IChar
- char :: Char -> IChar
- data IString
- class (ANat (Capacity a), IvoryStruct (StructName a), IvoryArea a, a ~ Struct (StructName a)) => IvoryString a where
- data Sint8
- data Sint16
- data Sint32
- data Sint64
- data Uint8
- data Uint16
- data Uint32
- data Uint64
- data IFloat
- data IDouble
- isnan :: forall a. (IvoryVar a, Floating a) => a -> IBool
- isinf :: forall a. (IvoryVar a, Floating a) => a -> IBool
- roundF :: IvoryFloat a => a -> a
- ceilF :: IvoryFloat a => a -> a
- floorF :: IvoryFloat a => a -> a
- atan2F :: IvoryFloat a => a -> a -> a
- ifloat :: Float -> IFloat
- idouble :: Double -> IDouble
- data Effects = Effects ReturnEff BreakEff AllocEff
- data BreakEff
- type family GetBreaks (effs :: Effects) :: BreakEff
- type family AllowBreak (effs :: Effects) :: Effects
- type family ClearBreak (effs :: Effects) :: Effects
- noBreak :: Ivory (ClearBreak eff) a -> Ivory eff a
- data ReturnEff
- type family GetReturn (effs :: Effects) :: ReturnEff
- type family ClearReturn (effs :: Effects) :: Effects
- noReturn :: Ivory (ClearReturn eff) a -> Ivory eff a
- data AllocEff
- type family GetAlloc (effs :: Effects) :: AllocEff
- type family ClearAlloc (effs :: Effects) :: Effects
- noAlloc :: innerEff ~ ClearAlloc outerEff => Ivory innerEff a -> Ivory outerEff a
- type AllocEffects s = Effects NoReturn NoBreak (Scope s)
- type ProcEffects s t = Effects (Returns t) NoBreak (Scope s)
- type NoEffects = Effects NoReturn NoBreak NoAlloc
- data Ivory eff a
- data RefScope
- assign :: forall eff a. IvoryExpr a => a -> Ivory eff a
- extern :: forall t. IvoryExpr t => Sym -> String -> t
- inclSym :: IvoryExpr t => t -> ModuleDef
- class (IvoryExpr a, IvoryOrd a, Num a) => IvoryIntegral a where
- (./) :: IvoryIntegral a => a -> a -> a
- class IvoryExpr a => IvoryEq a where
- class IvoryEq a => IvoryOrd a where
- iNot :: IBool -> IBool
- (.&&) :: IBool -> IBool -> IBool
- (.||) :: IBool -> IBool -> IBool
- class (Num a, IvoryExpr a) => IvoryBits a where
- extractByte :: BitCast a Uint8 => a -> (Uint8, a)
- class (IvoryBits a, IvoryBits b) => BitSplit a b | a -> b where
- class (IvoryBits a, IvoryBits b) => BitCast a b where
- 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
- data Bits n
- type Bit = Bits 1
- data BitArray n a
- type family BitRep (n :: Nat) :: *
- repToBits :: forall n. (ANat n, IvoryRep (BitRep n)) => BitRep n -> Bits n
- bitsToRep :: Bits n -> BitRep n
- zeroBits :: IvoryRep (BitRep n) => Bits n
- bitLength :: forall a n. ANat n => BitArray n a -> Int
- bitIx :: forall a n. (BitData a, ANat n, ANat (BitSize a), ANat (ArraySize n a)) => Int -> BitDataField (BitArray n a) a
- class (ANat (BitSize (BitType a)), IvoryRep (BitDataRep a), BitType a ~ Bits (BitSize (BitType a))) => BitData a where
- data BitDataField a b
- type BitDataRep a = BitRep (BitSize (BitType a))
- toBits :: BitData a => a -> BitType a
- fromBits :: BitData a => BitType a -> a
- toRep :: BitData a => a -> BitDataRep a
- fromRep :: BitData a => BitDataRep a -> a
- setBitDataBit :: BitData a => BitDataField a Bit -> a -> a
- clearBitDataBit :: BitData a => BitDataField a Bit -> a -> a
- getBitDataField :: (BitData a, BitData b, BitCast (BitDataRep a) (BitDataRep b)) => BitDataField a b -> a -> b
- setBitDataField :: (BitData a, BitData b, SafeCast (BitDataRep b) (BitDataRep a)) => BitDataField a b -> a -> b -> a
- (#!) :: 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
- (#.) :: (BitData a, BitData b, BitCast (BitDataRep a) (BitDataRep b)) => a -> BitDataField a b -> b
- (#>) :: BitDataField a b -> BitDataField b c -> BitDataField a c
- data BitDataM d a
- runBits :: BitData d => BitDataRep d -> BitDataM d a -> (a, BitDataRep d, [String])
- withBits :: BitData d => BitDataRep d -> BitDataM d () -> BitDataRep d
- withBitsRef :: BitData d => Ref s1 (Stored (BitDataRep d)) -> BitDataM d a -> Ivory eff a
- clear :: BitData d => BitDataM d ()
- setBit :: BitData d => BitDataField d Bit -> BitDataM d ()
- clearBit :: BitData d => BitDataField d Bit -> BitDataM d ()
- setField :: (BitData d, BitData b, SafeCast (BitDataRep b) (BitDataRep d)) => BitDataField d b -> b -> BitDataM d ()
- bitToBool :: Bit -> IBool
- boolToBit :: IBool -> Bit
- data MemArea area
- area :: forall area. (IvoryArea area, IvoryZero area) => Sym -> Maybe (Init area) -> MemArea area
- importArea :: IvoryArea area => Sym -> String -> MemArea area
- data ConstMemArea area
- constArea :: forall area. IvoryArea area => Sym -> Init area -> ConstMemArea area
- importConstArea :: IvoryArea area => Sym -> String -> ConstMemArea area
- class IvoryAddrOf mem ref | mem -> ref, ref -> mem where
- data Def proc
- data ProcPtr sig
- procPtr :: ProcType sig => Def sig -> ProcPtr sig
- proc :: forall proc impl. IvoryProcDef proc impl => Sym -> impl -> Def proc
- voidProc :: IvoryProcDef (args :-> ()) impl => Sym -> impl -> Def (args :-> ())
- importProc :: forall proc. ProcType proc => Sym -> String -> Def proc
- data Body r
- body :: IvoryType r => (forall s. Ivory (ProcEffects s r) ()) -> Body r
- importFrom :: String -> ImportFrom a
- requires :: (Requires c, WrapIvory m, IvoryType r) => c -> m r -> m r
- checkStored :: (CheckStored c, IvoryVar a, IvoryRef ref, IvoryVar (ref s (Stored a))) => ref s (Stored a) -> (a -> c) -> Cond
- ensures :: (Ensures c, WrapIvory m, IvoryVar r) => (r -> c) -> m r -> m r
- ensures_ :: (Ensures c, WrapIvory m) => c -> m () -> m ()
- assert :: forall a eff. IvoryExpr a => a -> Ivory eff ()
- assume :: forall a eff. IvoryExpr a => a -> Ivory eff ()
- class (IvoryArea (Struct sym), ASymbol sym) => IvoryStruct sym where
- data StructDef sym
- (~>) :: 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
- data Label sym field
- type ASymbol s = KnownSymbol s
- (!) :: 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
- fromIx :: ANat n => Ix n -> IxRep
- toIx :: forall a n. (SafeCast a IxRep, ANat n) => a -> Ix n
- data Ix n
- ixSize :: forall n. ANat n => Ix n -> Integer
- arrayLen :: forall s len area n ref. (Num n, ANat len, IvoryArea area, IvoryRef ref) => ref s (Array len area) -> n
- 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)
- type ANat n = KnownNat n
- fromTypeNat :: KnownNat i => proxy (i :: Nat) -> Integer
- for :: forall eff n a. ANat n => Ix n -> (Ix n -> Ivory (AllowBreak eff) a) -> Ivory eff ()
- times :: forall eff n a. ANat n => Ix n -> (Ix n -> Ivory (AllowBreak eff) a) -> Ivory eff ()
- breakOut :: GetBreaks eff ~ Break => Ivory eff ()
- arrayMap :: forall eff n a. ANat n => (Ix n -> Ivory (AllowBreak eff) a) -> Ivory eff ()
- forever :: Ivory (AllowBreak eff) () -> Ivory eff ()
- upTo :: ANat n => Ix n -> Ix n -> (Ix n -> Ivory (AllowBreak eff) a) -> Ivory eff ()
- downTo :: ANat n => Ix n -> Ix n -> (Ix n -> Ivory (AllowBreak eff) a) -> Ivory eff ()
- call :: forall proc eff impl. IvoryCall proc eff impl => Def proc -> impl
- indirect :: forall proc eff impl. IvoryCall proc eff impl => ProcPtr proc -> impl
- call_ :: forall proc eff impl. IvoryCall_ proc eff impl => Def proc -> impl
- indirect_ :: forall proc eff impl. IvoryCall_ proc eff impl => ProcPtr proc -> impl
- ifte_ :: IBool -> Ivory eff a -> Ivory eff b -> Ivory eff ()
- (?) :: IvoryExpr a => IBool -> (a, a) -> a
- withRef :: (KnownConstancy c, IvoryArea a) => Pointer Nullable c s a -> (Pointer Valid c s a -> Ivory eff t) -> Ivory eff f -> Ivory eff ()
- ret :: (GetReturn eff ~ Returns r, IvoryVar r) => r -> Ivory eff ()
- retVoid :: GetReturn eff ~ Returns () => Ivory eff ()
- class (IvoryExpr from, IvoryExpr to) => SafeCast from to where
- class (IvoryExpr from, IvoryExpr to, Default to) => RuntimeCast from to
- class Default a
- safeCast :: SafeCast from to => from -> to
- castWith :: RuntimeCast from to => to -> from -> to
- castDefault :: (Default to, RuntimeCast from to) => from -> to
- class (IvoryExpr from, IvoryExpr to) => SignCast from to where
- signCast :: SignCast from to => from -> to
- data Module
- moduleName :: Module -> String
- package :: String -> ModuleDef -> Module
- type ModuleDef = ModuleM ()
- incl :: Def a -> ModuleDef
- depend :: Module -> ModuleDef
- dependByName :: String -> ModuleDef
- defStruct :: forall sym. (IvoryStruct sym, ASymbol sym) => Proxy sym -> ModuleDef
- defStringType :: forall str. IvoryString str => Proxy str -> ModuleDef
- defMemArea :: IvoryArea area => MemArea area -> ModuleDef
- defConstMemArea :: IvoryArea area => ConstMemArea area -> ModuleDef
- private :: ModuleDef -> ModuleDef
- public :: ModuleDef -> ModuleDef
- ivory :: QuasiQuoter
- ivoryFile :: QuasiQuoter
- ivoryBlk :: QuasiQuoter
- data Proxy a = Proxy
- comment :: String -> Ivory eff ()
- module Ivory.Language.Coroutine
Kinds
The kind of memory-area types.
Types
The connection between Haskell and Ivory types.
Minimal complete definition
Instances
| IvoryType () Source # |
|
| IvoryType OpaqueType Source # | |
| IvoryType IString Source # | |
| IvoryType IChar Source # | |
| IvoryType Sint64 Source # | |
| IvoryType Sint32 Source # | |
| IvoryType Sint16 Source # | |
| IvoryType Sint8 Source # | |
| IvoryType Uint64 Source # | |
| IvoryType Uint32 Source # | |
| IvoryType Uint16 Source # | |
| IvoryType Uint8 Source # | |
| IvoryType IBool Source # | |
| IvoryType IDouble Source # | |
| IvoryType IFloat Source # | |
| ProcType proc => IvoryType (Def proc) Source # | |
| ProcType proc => IvoryType (ProcPtr proc) Source # | |
| ANat n => IvoryType (Ix n) Source # | |
| IvoryRep (BitRep n) => IvoryType (Bits n) Source # | |
| (KnownNullability n, KnownConstancy c, IvoryArea a) => IvoryType (Pointer n c s a) Source # | |
Guard the inhabitants of the Area type, as not all *s are Ivory *s.
Minimal complete definition
class IvoryType t => IvoryVar t Source #
Lifting a variable name.
Minimal complete definition
Instances
| IvoryVar IString Source # | |
| IvoryVar IChar Source # | |
| IvoryVar Sint64 Source # | |
| IvoryVar Sint32 Source # | |
| IvoryVar Sint16 Source # | |
| IvoryVar Sint8 Source # | |
| IvoryVar Uint64 Source # | |
| IvoryVar Uint32 Source # | |
| IvoryVar Uint16 Source # | |
| IvoryVar Uint8 Source # | |
| IvoryVar IBool Source # | |
| IvoryVar IDouble Source # | |
| IvoryVar IFloat Source # | |
| ProcType proc => IvoryVar (ProcPtr proc) Source # | |
| ANat n => IvoryVar (Ix n) Source # | |
| IvoryRep (BitRep n) => IvoryVar (Bits n) Source # | |
| (KnownNullability n, KnownConstancy c, IvoryArea a) => IvoryVar (Pointer n c s a) Source # | |
class IvoryVar t => IvoryExpr t Source #
Unwrapping for Ivory expressions.
Minimal complete definition
Instances
| IvoryExpr IString Source # | |
| IvoryExpr IChar Source # | |
| IvoryExpr Sint64 Source # | |
| IvoryExpr Sint32 Source # | |
| IvoryExpr Sint16 Source # | |
| IvoryExpr Sint8 Source # | |
| IvoryExpr Uint64 Source # | |
| IvoryExpr Uint32 Source # | |
| IvoryExpr Uint16 Source # | |
| IvoryExpr Uint8 Source # | |
| IvoryExpr IBool Source # | |
| IvoryExpr IDouble Source # | |
| IvoryExpr IFloat Source # | |
| ANat n => IvoryExpr (Ix n) Source # | |
| IvoryRep (BitRep n) => IvoryExpr (Bits n) Source # | |
| (KnownNullability n, KnownConstancy c, IvoryArea a) => IvoryExpr (Pointer n c s a) Source # | |
Non-null References
TODO remove class, leave function only
Minimal complete definition
unwrapRef
class IvoryVar a => IvoryStore a Source #
Things that can be safely stored in references.
Instances
| IvoryStore IChar Source # | |
| IvoryStore Sint64 Source # | |
| IvoryStore Sint32 Source # | |
| IvoryStore Sint16 Source # | |
| IvoryStore Sint8 Source # | |
| IvoryStore Uint64 Source # | |
| IvoryStore Uint32 Source # | |
| IvoryStore Uint16 Source # | |
| IvoryStore Uint8 Source # | |
| IvoryStore IBool Source # | |
| IvoryStore IDouble Source # | |
| IvoryStore IFloat Source # | |
| ANat n => IvoryStore (Ix n) Source # | |
| IvoryRep (BitRep n) => IvoryStore (Bits n) Source # | |
| (KnownConstancy c, IvoryArea a) => IvoryStore (Pointer Nullable c Global a) Source # | |
refToPtr :: IvoryArea area => Ref s area -> Ptr s area Source #
Convert valid to nullable pointer.
TODO deprecate in favor of pointerCastToNullable
constRef :: IvoryArea area => Ref s area -> ConstRef s area Source #
Turn a reference into a constant reference.
TODO deprecate in favor of pointerCastToConst
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.
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.
refZero :: forall eff s a. (IvoryZero a, IvoryArea a) => Ref s a -> Ivory eff () Source #
Zero the memory pointed to by this reference, as long as it could have been created with a zero initializer.
Stack Allocation
class IvoryVar e => IvoryInit e where Source #
Initializers for Stored things.
Instances
| IvoryInit IChar Source # | |
| IvoryInit Sint64 Source # | |
| IvoryInit Sint32 Source # | |
| IvoryInit Sint16 Source # | |
| IvoryInit Sint8 Source # | |
| IvoryInit Uint64 Source # | |
| IvoryInit Uint32 Source # | |
| IvoryInit Uint16 Source # | |
| IvoryInit Uint8 Source # | |
| IvoryInit IBool Source # | |
| IvoryInit IDouble Source # | |
| IvoryInit IFloat Source # | |
| ProcType proc => IvoryInit (ProcPtr proc) Source # | |
| ANat len => IvoryInit (Ix len) Source # | |
| IvoryRep (BitRep n) => IvoryInit (Bits n) Source # | |
| IvoryArea area => IvoryInit (Ptr Global area) Source # | |
class IvoryVar a => IvoryZeroVal a where Source #
Minimal complete definition
Instances
| IvoryZeroVal IChar Source # | |
| IvoryZeroVal Sint64 Source # | |
| IvoryZeroVal Sint32 Source # | |
| IvoryZeroVal Sint16 Source # | |
| IvoryZeroVal Sint8 Source # | |
| IvoryZeroVal Uint64 Source # | |
| IvoryZeroVal Uint32 Source # | |
| IvoryZeroVal Uint16 Source # | |
| IvoryZeroVal Uint8 Source # | |
| IvoryZeroVal IBool Source # | |
| IvoryZeroVal IDouble Source # | |
| IvoryZeroVal IFloat Source # | |
| ANat n => IvoryZeroVal (Ix n) Source # | |
| IvoryRep (BitRep n) => IvoryZeroVal (Bits n) Source # | |
| IvoryArea area => IvoryZeroVal (Ptr Global area) Source # | |
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.
Minimal complete definition
iarray :: forall len area. (IvoryArea area, ANat len) => [Init area] -> Init (Array len area) Source #
data InitStruct sym Source #
Instances
| IvoryStruct sym => Monoid (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
Booleans
Instances
Characters
Constant strings
Dynamic bounded-length strings
class (ANat (Capacity a), IvoryStruct (StructName a), IvoryArea a, a ~ Struct (StructName a)) => IvoryString a where Source #
Minimal complete definition
Methods
stringDataL :: Label (StructName a) (Array (Capacity a) (Stored Uint8)) Source #
stringLengthL :: Label (StructName a) (Stored IxRep) Source #
Signed Integers
8-bit integers.
Instances
16-bit integers.
Instances
32-bit integers.
Instances
64-bit integers.
Instances
Unsigned Integers
8-bit words.
Instances
16-bit words.
Instances
32-bit words.
Instances
64-bit words.
Instances
Floating-point Numbers
Instances
| Floating IFloat Source # | |
| Fractional IFloat Source # | |
| Num IFloat Source # | |
| IvoryExpr IFloat Source # | |
| IvoryVar IFloat Source # | |
| IvoryType IFloat Source # | |
| IvoryOrd IFloat Source # | |
| IvoryEq IFloat Source # | |
| IvoryStore IFloat Source # | |
| IvoryFloat IFloat Source # | |
| Default IFloat Source # | |
| IvoryZeroVal IFloat Source # | |
| IvoryInit IFloat Source # | |
| (Default to, Bounded to, IvoryIntegral to, SafeCast to IFloat) => RuntimeCast IFloat to Source # | Casting from a floating to a |
| SafeCast Sint32 IFloat Source # | |
| SafeCast Sint16 IFloat Source # | |
| SafeCast Sint8 IFloat Source # | |
| SafeCast Uint32 IFloat Source # | |
| SafeCast Uint16 IFloat Source # | |
| SafeCast Uint8 IFloat Source # | |
| SafeCast IBool IFloat Source # | |
| SafeCast IFloat IDouble Source # | |
| SafeCast IFloat IFloat Source # | |
Instances
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.
Effects
The effect context for Ivory operations.
type family AllowBreak (effs :: Effects) :: Effects Source #
Add the Break effect into an effect context.
Instances
| type AllowBreak (Effects r b a) Source # | |
type family ClearBreak (effs :: Effects) :: Effects Source #
Remove any Break effect present.
Instances
| type ClearBreak (Effects r b a) Source # | |
type family ClearReturn (effs :: Effects) :: Effects Source #
Remove any Return effects present.
Instances
| type ClearReturn (Effects r b a) Source # | |
type family ClearAlloc (effs :: Effects) :: Effects Source #
Remove any allocation effect currently present.
Instances
| type ClearAlloc (Effects r b a) Source # | |
Language
Monadic Interface
Definition scopes for values.
Subexpression naming
Constants
extern :: forall t. IvoryExpr t => Sym -> String -> t Source #
Import an externally defined constant by providing a global name.
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 .
For d1 < 0, iDiv (-d1) == -(d0 iDiv d1)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.
Methods
Euclidean division.
Euclidean remainder.
(./) :: IvoryIntegral a => a -> a -> a Source #
Comparisons
class IvoryExpr a => IvoryEq a where Source #
Instances
| IvoryEq Sint64 Source # | |
| IvoryEq Sint32 Source # | |
| IvoryEq Sint16 Source # | |
| IvoryEq Sint8 Source # | |
| IvoryEq Uint64 Source # | |
| IvoryEq Uint32 Source # | |
| IvoryEq Uint16 Source # | |
| IvoryEq Uint8 Source # | |
| IvoryEq IBool Source # | |
| IvoryEq IDouble Source # | |
| IvoryEq IFloat Source # | |
| ANat n => IvoryEq (Ix n) Source # | |
| IvoryRep (BitRep n) => IvoryEq (Bits n) Source # | |
| (KnownNullability n, KnownConstancy c, IvoryArea a) => IvoryEq (Pointer n c s a) Source # | |
class IvoryEq a => IvoryOrd a where Source #
Methods
(>?) :: a -> a -> IBool infix 4 Source #
(>=?) :: a -> a -> IBool infix 4 Source #
Instances
Boolean operators
Bit operators
class (Num a, IvoryExpr a) => IvoryBits a where Source #
Minimal complete definition
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.
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.
Minimal complete definition
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.
Methods
twosComplementCast :: unsigned -> signed Source #
twosComplementRep :: signed -> unsigned Source #
Bit data
bit types
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) Source # | |
| type BitType (Bits n) Source # | |
An array of "n" bit data elements of type "a".
type family BitRep (n :: Nat) :: * 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
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.
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).
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.
XXX do not export. This constructor must remain unexported so that only fields checked by the quasiquoter are created.
Instances
| Show (BitDataField a b) Source # | |
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
toBits :: BitData a => a -> BitType a Source #
Convert a bit data type to its raw bit value. This is always well defined and should be exported.
fromBits :: BitData a => 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).
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
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.
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.
setBit :: BitData d => BitDataField d Bit -> BitDataM d () Source #
Set a single bit field in the current bit data value.
setField :: (BitData d, BitData b, SafeCast (BitDataRep b) (BitDataRep d)) => BitDataField d b -> b -> BitDataM d () Source #
Set a field to a value.
External memory areas
Externally defined memory areas.
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.
Minimal complete definition
Instances
Procedures
Procedure definitions.
Procedure pointers
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.
importFrom :: String -> ImportFrom a Source #
Pre/Post-Conditions
checkStored :: (CheckStored c, IvoryVar a, IvoryRef ref, IvoryVar (ref s (Stored a))) => ref s (Stored a) -> (a -> c) -> Cond Source #
Assumption/Assertion statements
Structures
class (IvoryArea (Struct sym), ASymbol sym) => IvoryStruct sym where Source #
Minimal complete definition
(~>) :: 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.
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.
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.
Values in the range 0 .. n-1.
Instances
| ANat n => Bounded (Ix n) Source # | |
| 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 # | |
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.
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.
Note: The definition of for may change so that no index value is
provided. (Consider using upto if you need to use the index.)
times :: forall eff n a. ANat n => Ix n -> (Ix n -> Ivory (AllowBreak eff) a) -> Ivory eff () Source #
upTo :: ANat n => Ix n -> Ix n -> (Ix n -> Ivory (AllowBreak eff) a) -> Ivory eff () Source #
Loop over the range of indexes [start, start + 1 .. end]. If
start > end, the loop body will never execute.
downTo :: ANat n => Ix n -> Ix n -> (Ix n -> Ivory (AllowBreak eff) a) -> Ivory eff () Source #
Loop over the range of indexes [end, end - 1 .. start]. If
end > start, the loop body will never execute.
Call
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
withRef :: (KnownConstancy c, IvoryArea a) => Pointer Nullable c s a -> (Pointer Valid c s a -> 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.
Type-safe casting.
class (IvoryExpr from, IvoryExpr to) => SafeCast from to where Source #
Statically safe casts.
Instances
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 |
Default values for expression types.
Minimal complete definition
defaultVal
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
Minimal complete definition
Module Definitions
moduleName :: Module -> String Source #
package :: String -> ModuleDef -> Module Source #
Package the module up. Default visibility is public.
dependByName :: String -> ModuleDef Source #
Add a dependency on another module by name. Use the same name
here that you use when you call package to build the target
module. This function is particularly useful when building mutually
dependent module structures.
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
module Ivory.Language.Coroutine