Copilot.Core.Type

Typing for Core.

All expressions and streams in Core are accompanied by a representation of the types of the underlying expressions used or carried by the streams. This information is needed by the compiler to generate code, since it must initialize variables and equivalent representations for those types in the target languages.

Documentation

data Type :: * -> * where

A Type representing the types of expressions or values handled by Copilot Core.

Note that both arrays and structs use dependently typed features. In the former, the length of the array is part of the type. In the latter, the names of the fields are part of the type.

Constructors

Bool :: Type Bool

Int8 :: Type Int8

Int16 :: Type Int16

Int32 :: Type Int32

Int64 :: Type Int64

Word8 :: Type Word8

Word16 :: Type Word16

Word32 :: Type Word32

Word64 :: Type Word64

Float :: Type Float

Double :: Type Double

Array :: forall n t. (KnownNat n, Typed t, Typed (InnerType t), Flatten t (InnerType t)) => Type t -> Type (Array n t)

Struct :: (Typed a, Struct a) => a -> Type a

Instances

EqualType Type

Defined in Copilot.Core.Type

Methods

(=~=) :: Type a -> Type b -> Maybe (Equal a b)

class (Show a, Typeable a) => Typed a where

A typed expression, from which we can obtain the two type representations used by Copilot: Type and SimpleType.

Minimal complete definition

typeOf

Methods

typeOf :: Type a

simpleType :: Type a -> SimpleType

Instances

Typed Bool

Defined in Copilot.Core.Type

Methods

typeOf :: Type Bool

simpleType :: Type Bool -> SimpleType

Typed Double

Defined in Copilot.Core.Type

Methods

typeOf :: Type Double

simpleType :: Type Double -> SimpleType

Typed Float

Defined in Copilot.Core.Type

Methods

typeOf :: Type Float

simpleType :: Type Float -> SimpleType

Typed Int8

Defined in Copilot.Core.Type

Methods

typeOf :: Type Int8

simpleType :: Type Int8 -> SimpleType

Typed Int16

Defined in Copilot.Core.Type

Methods

typeOf :: Type Int16

simpleType :: Type Int16 -> SimpleType

Typed Int32

Defined in Copilot.Core.Type

Methods

typeOf :: Type Int32

simpleType :: Type Int32 -> SimpleType

Typed Int64

Defined in Copilot.Core.Type

Methods

typeOf :: Type Int64

simpleType :: Type Int64 -> SimpleType

Typed Word8

Defined in Copilot.Core.Type

Methods

typeOf :: Type Word8

simpleType :: Type Word8 -> SimpleType

Typed Word16

Defined in Copilot.Core.Type

Methods

typeOf :: Type Word16

simpleType :: Type Word16 -> SimpleType

Typed Word32

Defined in Copilot.Core.Type

Methods

typeOf :: Type Word32

simpleType :: Type Word32 -> SimpleType

Typed Word64

Defined in Copilot.Core.Type

Methods

typeOf :: Type Word64

simpleType :: Type Word64 -> SimpleType

(Typeable t, Typed t, KnownNat n, Flatten t (InnerType t), Typed (InnerType t)) => Typed (Array n t)

Defined in Copilot.Core.Type

Methods

typeOf :: Type (Array n t)

simpleType :: Type (Array n t) -> SimpleType

data UType

A untyped type (no phantom type).

Constructors

forall a.Typeable a => UType

Fields

• uTypeType :: Type a

Instances

Eq UType

Defined in Copilot.Core.Type

Methods

(==) :: UType -> UType -> Bool

(/=) :: UType -> UType -> Bool

data SimpleType where

A simple, monomorphic representation of types that facilitates putting variables in heterogeneous lists and environments in spite of their types being different.

Constructors

SBool :: SimpleType

SInt8 :: SimpleType

SInt16 :: SimpleType

SInt32 :: SimpleType

SInt64 :: SimpleType

SWord8 :: SimpleType

SWord16 :: SimpleType

SWord32 :: SimpleType

SWord64 :: SimpleType

SFloat :: SimpleType

SDouble :: SimpleType

SArray :: Type t -> SimpleType

SStruct :: SimpleType

Instances

Eq SimpleType

Type equality, used to help type inference.

Defined in Copilot.Core.Type

Methods

(==) :: SimpleType -> SimpleType -> Bool

(/=) :: SimpleType -> SimpleType -> Bool

tysize :: forall n t. KnownNat n => Type (Array n t) -> Int

Return the total (nested) size of an array from its type

tylength :: forall n t. KnownNat n => Type (Array n t) -> Int

Return the length of an array from its type

data Value a

The field of a struct, together with a representation of its type.

Constructors

forall s t.(Typeable t, KnownSymbol s, Show t) => Value (Type t) (Field s t)

toValues :: Struct a => a -> [Value a]

Transforms all the struct's fields into a list of values.

data Field (s :: Symbol) t

A field in a struct. The name of the field is a literal at the type level.

Constructors

Field t

Instances

(KnownSymbol s, Show t) => Show (Field s t)

Defined in Copilot.Core.Type

Methods

showsPrec :: Int -> Field s t -> ShowS

show :: Field s t -> String

showList :: [Field s t] -> ShowS

typename :: Struct a => a -> String

Returns the name of struct in the target language.

class Struct a

The value of that is a product or struct, defined as a constructor with several fields.

Minimal complete definition

typename, toValues

fieldname :: forall s t. KnownSymbol s => Field s t -> String

Extract the name of a field.

accessorname :: forall a s t. (Struct a, KnownSymbol s) => (a -> Field s t) -> String

Extract the name of an accessor (a function that returns a field of a struct).

Orphan instances

(Typed t, Struct t) => Show t

Methods

showsPrec :: Int -> t -> ShowS

show :: t -> String

showList :: [t] -> ShowS