{-# 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)