copilot-core-4.6.1: An intermediate representation for Copilot.

Copyright | (c) 2011 National Institute of Aerospace / Galois Inc.
Safe Haskell | Trustworthy
Language | Haskell2010

Copilot.Core.Type

Contents

- Orphan instances

Description

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.

Synopsis

- data Type a where
  - 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 :: Nat) t. (KnownNat n, Typed t) => Type t -> Type (Array n t)
  - Struct :: forall a. (Typed a, Struct a) => a -> Type a
- class (Show a, Typeable a) => Typed a where
  - typeOf :: Type a
  - simpleType :: Type a -> SimpleType
- typeOfDefault :: (Typed a, Struct a, Generic a, GTypedStruct (Rep a)) => Type a
- data UType = Typeable a => UType (Type a)
- data SimpleType where
  - SBool :: SimpleType
  - SInt8 :: SimpleType
  - SInt16 :: SimpleType
  - SInt32 :: SimpleType
  - SInt64 :: SimpleType
  - SWord8 :: SimpleType
  - SWord16 :: SimpleType
  - SWord32 :: SimpleType
  - SWord64 :: SimpleType
  - SFloat :: SimpleType
  - SDouble :: SimpleType
  - SArray :: forall t. Type t -> SimpleType
  - SStruct :: SimpleType
- typeSize :: forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
- typeLength :: forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int
- data Value a = (Typeable t, KnownSymbol s, Show t) => Value (Type t) (Field s t)
- toValues :: Struct a => a -> [Value a]
- toValuesDefault :: (Generic a, GStruct (Rep a)) => a -> [Value a]
- data Field (s :: Symbol) t = Field t
- typeName :: Struct a => a -> String
- typeNameDefault :: (Generic a, GDatatype (Rep a)) => a -> String
- class Struct a
- fieldName :: forall (s :: Symbol) t. KnownSymbol s => Field s t -> String
- accessorName :: forall a (s :: Symbol) t. (Struct a, KnownSymbol s) => (a -> Field s t) -> String
- updateField :: Struct a => a -> Value t -> a
- updateFieldDefault :: (Generic a, GStruct (Rep a)) => a -> Value t -> a

# Documentation

data Type a where Source #

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 :: Nat) t. (KnownNat n, Typed t) => Type t -> Type (Array n t) |
Struct :: forall a. (Typed a, Struct a) => a -> Type a |

#### Instances

Instances details

TestEquality Type Source # |
Instance details Defined in Copilot.Core.Type Methods testEquality :: Type a -> Type b -> Maybe (a :~: b) Source #
Show (Type a) Source # |
Instance details Defined in Copilot.Core.Type Methods showsPrec :: Int -> Type a -> ShowS Source # show :: Type a -> String Source # showList :: [Type a] -> ShowS Source #

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

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 Source #

simpleType :: Type a -> SimpleType Source #

#### Instances

Instances details

Typed Int16 Source # |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Int16 Source # simpleType :: Type Int16 -> SimpleType Source #
Typed Int32 Source # |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Int32 Source # simpleType :: Type Int32 -> SimpleType Source #
Typed Int64 Source # |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Int64 Source # simpleType :: Type Int64 -> SimpleType Source #
Typed Int8 Source # |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Int8 Source # simpleType :: Type Int8 -> SimpleType Source #
Typed Word16 Source # |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Word16 Source # simpleType :: Type Word16 -> SimpleType Source #
Typed Word32 Source # |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Word32 Source # simpleType :: Type Word32 -> SimpleType Source #
Typed Word64 Source # |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Word64 Source # simpleType :: Type Word64 -> SimpleType Source #
Typed Word8 Source # |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Word8 Source # simpleType :: Type Word8 -> SimpleType Source #
Typed Bool Source # |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Bool Source # simpleType :: Type Bool -> SimpleType Source #
Typed Double Source # |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Double Source # simpleType :: Type Double -> SimpleType Source #
Typed Float Source # |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type Float Source # simpleType :: Type Float -> SimpleType Source #
(Typeable t, Typed t, KnownNat n) => Typed (Array n t) Source # |
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type (Array n t) Source # simpleType :: Type (Array n t) -> SimpleType Source #

typeOfDefault :: (Typed a, Struct a, Generic a, GTypedStruct (Rep a)) => Type a Source #

A default implementation of `typeOf` that leverages `Generic`. In order to use this, make sure you derive a `Generic` instance for your data type and then define ``typeOf` = `typeOfDefault`` in its `Typed` instance.

data UType Source #

A untyped type (no phantom type).

Constructors

Typeable a => UType (Type a) |

#### Instances

Instances details

Eq UType Source # |
Instance details Defined in Copilot.Core.Type Methods (==) :: UType -> UType -> Bool Source # (/=) :: UType -> UType -> Bool Source #

data SimpleType where Source #

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 :: forall t. Type t -> SimpleType |
SStruct :: SimpleType |

#### Instances

Instances details

Eq SimpleType Source # | Type equality, used to help type inference.
Instance details Defined in Copilot.Core.Type Methods (==) :: SimpleType -> SimpleType -> Bool Source # (/=) :: SimpleType -> SimpleType -> Bool Source #

typeSize :: forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int Source #

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

typeLength :: forall (n :: Nat) t. KnownNat n => Type (Array n t) -> Int Source #

Return the length of an array from its type

data Value a Source #

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

Constructors

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

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

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

toValuesDefault :: (Generic a, GStruct (Rep a)) => a -> [Value a] Source #

A default implementation of `toValues` that leverages `Generic`. In order to use this, make sure you derive a `Generic` instance for your data type and then define ``toValues` = `toValuesDefault`` in its `Struct` instance.

data Field (s :: Symbol) t Source #

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

Constructors

Field t |

#### Instances

Instances details

(KnownSymbol s, Show t) => Show (Field s t) Source # |
Instance details Defined in Copilot.Core.Type Methods showsPrec :: Int -> Field s t -> ShowS Source # show :: Field s t -> String Source # showList :: [Field s t] -> ShowS Source #

typeName :: Struct a => a -> String Source #

Returns the name of struct in the target language.

typeNameDefault :: (Generic a, GDatatype (Rep a)) => a -> String Source #

A default implementation of `typeName` that leverages `Generic`. In order to use this, make sure you derive a `Generic` instance for your data type and then define ``typeName` = `typeNameDefault`` in its `Struct` instance.

This generates a struct name that consists of the name of the original Haskell data type, but converted to snake_case.

class Struct a Source #

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

Minimal complete definition

typeName, toValues

fieldName :: forall (s :: Symbol) t. KnownSymbol s => Field s t -> String Source #

Extract the name of a field.

accessorName :: forall a (s :: Symbol) t. (Struct a, KnownSymbol s) => (a -> Field s t) -> String Source #

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

updateField :: Struct a => a -> Value t -> a Source #

Update the value of a struct field. This is only used by the Copilot interpreter.

If you do not plan to use the interpreter, you can omit an implementation of this method. If you do so, it is recommended that you derive a `Generic` instance for the struct data type. This is because in a future release, the default implementation of `updateField` (which will be picked if there is not a manually written implementation) will be changed to require a `Generic` instance.

In order to implement `updateField`, pick one of the following approaches:

- Derive a `Generic` instance for the struct data type and then define ``updateField` = `updateFieldDefault`` in the `Struct` instance.
- Manually implement `updateField` by doing the following for each `Field` in a struct:

1. Check that the name of the `Field` matches the name of the supplied `Value` (using `sameSymbol`).
2. Check that the type of the `Field` matches the `Type` of the supplied `Value` (using `testEquality`).
3. If both (1) and (2) succeed, update the corresponding struct field using a record update.

For a complete end-to-end example that demonstrates how to manually implement `updateField` and use it in the Copilot interpreter, see the `examples/StructsUpdateField.hs` example in the `copilot` library.

updateFieldDefault :: (Generic a, GStruct (Rep a)) => a -> Value t -> a Source #

A default implementation of `updateField` that leverages `Generic`. In order to use this, make sure you derive a `Generic` instance for your data type and then define ``updateField` = `updateFieldDefault`` in its `Struct` instance.

# Orphan instances

(Typed t, Struct t) => Show t Source # |
Instance details Methods showsPrec :: Int -> t -> ShowS Source # show :: t -> String Source # showList :: [t] -> ShowS Source #