{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# 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
    , flatten
    , size
    , Flatten
    , InnerType
    , arrayelems
    )
  where

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

-- | 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) = 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 forall a. Eq a => a -> a -> Bool
== Int
typelen = forall t (n :: Nat). [t] -> Array n t
Array [t]
xs
         | Bool
otherwise          = forall a. HasCallStack => String -> a
error String
errmsg
  where
    datalen :: Int
datalen = forall (t :: * -> *) a. Foldable t => t a -> Int
length [t]
xs
    typelen :: Int
typelen = forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
    errmsg :: String
errmsg = String
"Length of data (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
datalen forall a. [a] -> [a] -> [a]
++
             String
") does not match length of type (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
typelen forall a. [a] -> [a] -> [a]
++ String
")."

-- | Association between an array and the type of the elements it contains.
{-# DEPRECATED InnerType "This type family is deprecated in Copilot 3.11." #-}
type family InnerType x where
  InnerType (Array _ x) = InnerType x
  InnerType x           = x

-- | Flattening or conversion of arrays to lists.
{-# DEPRECATED Flatten "This class is deprecated in Copilot 3.11." #-}
{-# DEPRECATED flatten "This function is deprecated in Copilot 3.11." #-}
class Flatten a b where
  -- | Flatten an array to a list.
  flatten :: Array n a -> [b]

-- | Flattening of plain arrays.
instance Flatten a a where
  flatten :: forall (n :: Nat). Array n a -> [a]
flatten (Array [a]
xs) = [a]
xs

-- | Flattening of nested arrays.
instance Flatten a b => Flatten (Array n a) b where
  flatten :: forall (n :: Nat). Array n (Array n a) -> [b]
flatten (Array [Array n a]
xss) = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b (n :: Nat). Flatten a b => Array n a -> [b]
flatten [Array n a]
xss

-- | This instance is deprecated in Copilot 3.11.
instance Foldable (Array n) where
  foldr :: forall a b. (a -> b -> b) -> b -> Array n a -> b
foldr a -> b -> b
f b
base (Array [a]
xs) = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> b -> b
f b
base [a]
xs

-- | Total number of elements in a possibly nested array.
{-# DEPRECATED size "This function is deprecated in Copilot 3.11." #-}
size :: forall a n b. (Flatten a b, b ~ InnerType a) => Array n a -> Int
size :: forall a (n :: Nat) b.
(Flatten a b, b ~ InnerType a) =>
Array n a -> Int
size Array n a
xs = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ (forall a b (n :: Nat). Flatten a b => Array n a -> [b]
flatten Array n a
xs :: [b])

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