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

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

Copilot.Core.Type.Array

Description

Implementation of an array that uses type literals to store length. No explicit indexing is used for the input data. Supports arbitrary nesting of arrays.

Synopsis

- data Array (n :: Nat) t
- array :: forall (n :: Nat) t. KnownNat n => [t] -> Array n t
- arrayElems :: forall (n :: Nat) a. Array n a -> [a]
- arrayUpdate :: forall (n :: Nat) a. Array n a -> Int -> a -> Array n a

# Documentation

data Array (n :: Nat) t Source #

Implementation of an array that uses type literals to store length.

#### Instances

Instances details

(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 #
Show t => Show (Array n t) Source # |
Instance details Defined in Copilot.Core.Type.Array Methods showsPrec :: Int -> Array n t -> ShowS Source # show :: Array n t -> String Source # showList :: [Array n t] -> ShowS Source #

array :: forall (n :: Nat) t. KnownNat n => [t] -> Array n t Source #

Smart array constructor that only type checks if the length of the given list matches the length of the array at type level.

arrayElems :: forall (n :: Nat) a. Array n a -> [a] Source #

Return the elements of an array.

arrayUpdate :: forall (n :: Nat) a. Array n a -> Int -> a -> Array n a Source #

Update element of array to given element.

PRE: the second argument denotes a valid index in the array.