    {-# LANGUAGE DataKinds           #-}
    {-# LANGUAGE GADTs               #-}
    {-# LANGUAGE Safe                #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TypeFamilies        #-}
    {-# LANGUAGE TypeOperators       #-}

    -- |
    -- Copyright: (c) 2011 National Institute of Aerospace / Galois, Inc.
    --
    -- 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.
    module Copilot.Core.Type.Array
        ( Array
        , array
        , arrayElems
        , arrayUpdate
        )
      where

    -- External imports
    import Data.Proxy   (Proxy (..))
    import GHC.TypeLits (KnownNat, Nat, natVal, type(-))

    -- | Implementation of an array that uses type literals to store length.
    data Array (n :: Nat) t where
      Array :: [t] -> Array n t

    instance Show t => Show (Array n t) where
      show :: Array n t -> String
    show (Array [t]
    xs) = [t] -> String
    forall a. Show a => a -> String
    show [t]
    xs

    -- | Smart array constructor that only type checks if the length of the given
    -- list matches the length of the array at type level.
    array :: forall n t. KnownNat n => [t] -> Array n t
    array :: forall (n :: Nat) t. KnownNat n => [t] -> Array n t
    array [t]
    xs | Int
    datalen Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    typelen = [t] -> Array n t
    forall t (n :: Nat). [t] -> Array n t
    Array [t]
    xs
             | Bool
    otherwise          = String -> Array n t
    forall a. HasCallStack => String -> a
    error String
    errmsg
      where
        datalen :: Int
    datalen = [t] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [t]
    xs
        typelen :: Int
    typelen = Integer -> Int
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Integer -> Int) -> Integer -> Int
    forall a b. (a -> b) -> a -> b
    $ Proxy n -> Integer
    forall (n :: Nat) (proxy :: Nat -> *).
    KnownNat n =>
    proxy n -> Integer
    natVal (Proxy n
    forall {k} (t :: k). Proxy t
    Proxy :: Proxy n)
        errmsg :: String
    errmsg = String
    "Length of data (" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    datalen String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++
                 String
    ") does not match length of type (" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Int -> String
    forall a. Show a => a -> String
    show Int
    typelen String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ")."

    -- | Return the elements of an array.
    arrayElems :: Array n a -> [a]
    arrayElems :: forall (n :: Nat) a. Array n a -> [a]
    arrayElems (Array [a]
    xs) = [a]
    xs

    -- | Update element of array to given element.
    --
    -- PRE: the second argument denotes a valid index in the array.
    arrayUpdate :: Array n a -> Int -> a -> Array n a
    arrayUpdate :: forall (n :: Nat) a. Array n a -> Int -> a -> Array n a
    arrayUpdate (Array []) Int
    _ a
    _ = String -> Array n a
    forall a. HasCallStack => String -> a
    error String
    errMsg
      where
        errMsg :: String
    errMsg = String
    "copilot-core: arrayUpdate: Attempt to update empty array"

    arrayUpdate (Array (a
    x:[a]
    xs)) Int
    0 a
    y = [a] -> Array n a
    forall t (n :: Nat). [t] -> Array n t
    Array (a
    ya -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    xs)

    arrayUpdate (Array (a
    x:[a]
    xs)) Int
    n a
    y =
        a -> Array (n - 1) a -> Array n a
    forall a (n :: Nat). a -> Array (n - 1) a -> Array n a
    arrayAppend a
    x (Array (n - 1) a -> Int -> a -> Array (n - 1) a
    forall (n :: Nat) a. Array n a -> Int -> a -> Array n a
    arrayUpdate ([a] -> Array (n - 1) a
    forall t (n :: Nat). [t] -> Array n t
    Array [a]
    xs) (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) a
    y)
      where
        -- | Append to an array while preserving length information at the type
        -- level.
        arrayAppend :: a -> Array (n - 1) a -> Array n a
        arrayAppend :: forall a (n :: Nat). a -> Array (n - 1) a -> Array n a
    arrayAppend a
    x (Array [a]
    xs) = [a] -> Array n a
    forall t (n :: Nat). [t] -> Array n t
    Array (a
    xa -> [a] -> [a]
    forall a. a -> [a] -> [a]
    :[a]
    xs)