{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Copilot.Core.Type.Array
( Array
, array
, arrayElems
, arrayelems
)
where
import Data.Proxy (Proxy (..))
import GHC.TypeLits (KnownNat, Nat, natVal)
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
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
")."
arrayElems :: Array n a -> [a]
arrayElems :: forall (n :: Nat) a. Array n a -> [a]
arrayElems (Array [a]
xs) = [a]
xs
{-# DEPRECATED arrayelems "Use ArrayElems instead." #-}
arrayelems :: Array n a -> [a]
arrayelems :: forall (n :: Nat) a. Array n a -> [a]
arrayelems = forall (n :: Nat) a. Array n a -> [a]
arrayElems