{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE StrictData #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
module Data.Array.Nested.Shaped.Shape where

import Control.DeepSeq (NFData(..))
import Data.Array.Shape qualified as O
import Data.Coerce (coerce)
import Data.Foldable qualified as Foldable
import Data.Functor.Const
import Data.Functor.Product qualified as Fun
import Data.Kind (Constraint, Type)
import Data.Monoid (Sum(..))
import Data.Proxy
import Data.Type.Equality
import GHC.Exts (withDict)
import GHC.Generics (Generic)
import GHC.IsList (IsList)
import GHC.IsList qualified as IsList
import GHC.TypeLits

import Data.Array.Nested.Mixed.Shape
import Data.Array.Nested.Permutation
import Data.Array.Nested.Types


-- * Shaped lists

-- | Note: The 'KnownNat' constraint on '(::$)' is deprecated and should be
-- removed in a future release.
type role ListS nominal representational
type ListS :: [Nat] -> (Nat -> Type) -> Type
data ListS sh f where
  ZS :: ListS '[] f
  -- TODO: when the KnownNat constraint is removed, restore listsIndex to sanity
  (::$) :: forall n sh {f}. KnownNat n => f n -> ListS sh f -> ListS (n : sh) f
deriving instance (forall n. Eq (f n)) => Eq (ListS sh f)
deriving instance (forall n. Ord (f n)) => Ord (ListS sh f)
infixr 3 ::$

#ifdef OXAR_DEFAULT_SHOW_INSTANCES
deriving instance (forall n. Show (f n)) => Show (ListS sh f)
#else
instance (forall n. Show (f n)) => Show (ListS sh f) where
  showsPrec :: Int -> ListS sh f -> ShowS
showsPrec Int
_ = (forall (n :: Nat). f n -> ShowS) -> ListS sh f -> ShowS
forall (sh :: [Nat]) (f :: Nat -> Type).
(forall (n :: Nat). f n -> ShowS) -> ListS sh f -> ShowS
listsShow f n -> ShowS
forall (n :: Nat). f n -> ShowS
forall a. Show a => a -> ShowS
shows
#endif

instance (forall m. NFData (f m)) => NFData (ListS n f) where
  rnf :: ListS n f -> ()
rnf ListS n f
ZS = ()
  rnf (f n
x ::$ ListS sh f
l) = f n -> ()
forall a. NFData a => a -> ()
rnf f n
x () -> () -> ()
forall a b. a -> b -> b
`seq` ListS sh f -> ()
forall a. NFData a => a -> ()
rnf ListS sh f
l

data UnconsListSRes f sh1 =
  forall n sh. (KnownNat n, n : sh ~ sh1) => UnconsListSRes (ListS sh f) (f n)
listsUncons :: ListS sh1 f -> Maybe (UnconsListSRes f sh1)
listsUncons :: forall (sh1 :: [Nat]) (f :: Nat -> Type).
ListS sh1 f -> Maybe (UnconsListSRes f sh1)
listsUncons (f n
x ::$ ListS sh f
sh') = UnconsListSRes f sh1 -> Maybe (UnconsListSRes f sh1)
forall a. a -> Maybe a
Just (ListS sh f -> f n -> UnconsListSRes f sh1
forall (f :: Nat -> Type) (sh1 :: [Nat]) (n :: Nat) (sh :: [Nat]).
(KnownNat n, (n : sh) ~ sh1) =>
ListS sh f -> f n -> UnconsListSRes f sh1
UnconsListSRes ListS sh f
sh' f n
x)
listsUncons ListS sh1 f
ZS = Maybe (UnconsListSRes f sh1)
forall a. Maybe a
Nothing

-- | This checks only whether the types are equal; if the elements of the list
-- are not singletons, their values may still differ. This corresponds to
-- 'testEquality', except on the penultimate type parameter.
listsEqType :: TestEquality f => ListS sh f -> ListS sh' f -> Maybe (sh :~: sh')
listsEqType :: forall (f :: Nat -> Type) (sh :: [Nat]) (sh' :: [Nat]).
TestEquality f =>
ListS sh f -> ListS sh' f -> Maybe (sh :~: sh')
listsEqType ListS sh f
ZS ListS sh' f
ZS = (sh :~: sh') -> Maybe (sh :~: sh')
forall a. a -> Maybe a
Just sh :~: sh
sh :~: sh'
forall {k} (a :: k). a :~: a
Refl
listsEqType (f n
n ::$ ListS sh f
sh) (f n
m ::$ ListS sh f
sh')
  | Just n :~: n
Refl <- f n -> f n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat). f a -> f b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality f n
n f n
m
  , Just sh :~: sh
Refl <- ListS sh f -> ListS sh f -> Maybe (sh :~: sh)
forall (f :: Nat -> Type) (sh :: [Nat]) (sh' :: [Nat]).
TestEquality f =>
ListS sh f -> ListS sh' f -> Maybe (sh :~: sh')
listsEqType ListS sh f
sh ListS sh f
sh'
  = (sh :~: sh') -> Maybe (sh :~: sh')
forall a. a -> Maybe a
Just sh :~: sh
sh :~: sh'
forall {k} (a :: k). a :~: a
Refl
listsEqType ListS sh f
_ ListS sh' f
_ = Maybe (sh :~: sh')
forall a. Maybe a
Nothing

-- | This checks whether the two lists actually contain equal values. This is
-- more than 'testEquality', and corresponds to @geq@ from @Data.GADT.Compare@
-- in the @some@ package (except on the penultimate type parameter).
listsEqual :: (TestEquality f, forall n. Eq (f n)) => ListS sh f -> ListS sh' f -> Maybe (sh :~: sh')
listsEqual :: forall (f :: Nat -> Type) (sh :: [Nat]) (sh' :: [Nat]).
(TestEquality f, forall (n :: Nat). Eq (f n)) =>
ListS sh f -> ListS sh' f -> Maybe (sh :~: sh')
listsEqual ListS sh f
ZS ListS sh' f
ZS = (sh :~: sh') -> Maybe (sh :~: sh')
forall a. a -> Maybe a
Just sh :~: sh
sh :~: sh'
forall {k} (a :: k). a :~: a
Refl
listsEqual (f n
n ::$ ListS sh f
sh) (f n
m ::$ ListS sh f
sh')
  | Just n :~: n
Refl <- f n -> f n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat). f a -> f b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality f n
n f n
m
  , f n
n f n -> f n -> Bool
forall a. Eq a => a -> a -> Bool
== f n
f n
m
  , Just sh :~: sh
Refl <- ListS sh f -> ListS sh f -> Maybe (sh :~: sh)
forall (f :: Nat -> Type) (sh :: [Nat]) (sh' :: [Nat]).
(TestEquality f, forall (n :: Nat). Eq (f n)) =>
ListS sh f -> ListS sh' f -> Maybe (sh :~: sh')
listsEqual ListS sh f
sh ListS sh f
sh'
  = (sh :~: sh') -> Maybe (sh :~: sh')
forall a. a -> Maybe a
Just sh :~: sh
sh :~: sh'
forall {k} (a :: k). a :~: a
Refl
listsEqual ListS sh f
_ ListS sh' f
_ = Maybe (sh :~: sh')
forall a. Maybe a
Nothing

listsFmap :: (forall n. f n -> g n) -> ListS sh f -> ListS sh g
listsFmap :: forall (f :: Nat -> Type) (g :: Nat -> Type) (sh :: [Nat]).
(forall (n :: Nat). f n -> g n) -> ListS sh f -> ListS sh g
listsFmap forall (n :: Nat). f n -> g n
_ ListS sh f
ZS = ListS sh g
ListS '[] g
forall (f :: Nat -> Type). ListS '[] f
ZS
listsFmap forall (n :: Nat). f n -> g n
f (f n
x ::$ ListS sh f
xs) = f n -> g n
forall (n :: Nat). f n -> g n
f f n
x g n -> ListS sh g -> ListS (n : sh) g
forall (n :: Nat) (sh :: [Nat]) {f :: Nat -> Type}.
KnownNat n =>
f n -> ListS sh f -> ListS (n : sh) f
::$ (forall (n :: Nat). f n -> g n) -> ListS sh f -> ListS sh g
forall (f :: Nat -> Type) (g :: Nat -> Type) (sh :: [Nat]).
(forall (n :: Nat). f n -> g n) -> ListS sh f -> ListS sh g
listsFmap f n -> g n
forall (n :: Nat). f n -> g n
f ListS sh f
xs

listsFold :: Monoid m => (forall n. f n -> m) -> ListS sh f -> m
listsFold :: forall m (f :: Nat -> Type) (sh :: [Nat]).
Monoid m =>
(forall (n :: Nat). f n -> m) -> ListS sh f -> m
listsFold forall (n :: Nat). f n -> m
_ ListS sh f
ZS = m
forall a. Monoid a => a
mempty
listsFold forall (n :: Nat). f n -> m
f (f n
x ::$ ListS sh f
xs) = f n -> m
forall (n :: Nat). f n -> m
f f n
x m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (forall (n :: Nat). f n -> m) -> ListS sh f -> m
forall m (f :: Nat -> Type) (sh :: [Nat]).
Monoid m =>
(forall (n :: Nat). f n -> m) -> ListS sh f -> m
listsFold f n -> m
forall (n :: Nat). f n -> m
f ListS sh f
xs

listsShow :: forall sh f. (forall n. f n -> ShowS) -> ListS sh f -> ShowS
listsShow :: forall (sh :: [Nat]) (f :: Nat -> Type).
(forall (n :: Nat). f n -> ShowS) -> ListS sh f -> ShowS
listsShow forall (n :: Nat). f n -> ShowS
f ListS sh f
l = String -> ShowS
showString String
"[" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ListS sh f -> ShowS
forall (sh' :: [Nat]). String -> ListS sh' f -> ShowS
go String
"" ListS sh f
l ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"]"
  where
    go :: String -> ListS sh' f -> ShowS
    go :: forall (sh' :: [Nat]). String -> ListS sh' f -> ShowS
go String
_ ListS sh' f
ZS = ShowS
forall a. a -> a
id
    go String
prefix (f n
x ::$ ListS sh f
xs) = String -> ShowS
showString String
prefix ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f n -> ShowS
forall (n :: Nat). f n -> ShowS
f f n
x ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ListS sh f -> ShowS
forall (sh' :: [Nat]). String -> ListS sh' f -> ShowS
go String
"," ListS sh f
xs

listsLength :: ListS sh f -> Int
listsLength :: forall (sh :: [Nat]) (f :: Nat -> Type). ListS sh f -> Int
listsLength = Sum Int -> Int
forall a. Sum a -> a
getSum (Sum Int -> Int) -> (ListS sh f -> Sum Int) -> ListS sh f -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (n :: Nat). f n -> Sum Int) -> ListS sh f -> Sum Int
forall m (f :: Nat -> Type) (sh :: [Nat]).
Monoid m =>
(forall (n :: Nat). f n -> m) -> ListS sh f -> m
listsFold (\f n
_ -> Int -> Sum Int
forall a. a -> Sum a
Sum Int
1)

listsRank :: ListS sh f -> SNat (Rank sh)
listsRank :: forall (sh :: [Nat]) (f :: Nat -> Type).
ListS sh f -> SNat (Rank sh)
listsRank ListS sh f
ZS = SNat 0
SNat (Rank sh)
forall (n :: Nat). KnownNat n => SNat n
SNat
listsRank (f n
_ ::$ ListS sh f
sh) = SNat (Rank sh) -> SNat (Rank sh + 1)
forall (n :: Nat). SNat n -> SNat (n + 1)
snatSucc (ListS sh f -> SNat (Rank sh)
forall (sh :: [Nat]) (f :: Nat -> Type).
ListS sh f -> SNat (Rank sh)
listsRank ListS sh f
sh)

listsToList :: ListS sh (Const i) -> [i]
listsToList :: forall (sh :: [Nat]) i. ListS sh (Const i) -> [i]
listsToList ListS sh (Const i)
ZS = []
listsToList (Const i
i ::$ ListS sh (Const i)
is) = i
i i -> [i] -> [i]
forall a. a -> [a] -> [a]
: ListS sh (Const i) -> [i]
forall (sh :: [Nat]) i. ListS sh (Const i) -> [i]
listsToList ListS sh (Const i)
is

listsHead :: ListS (n : sh) f -> f n
listsHead :: forall (n :: Nat) (sh :: [Nat]) (f :: Nat -> Type).
ListS (n : sh) f -> f n
listsHead (f n
i ::$ ListS sh f
_) = f n
f n
i

listsTail :: ListS (n : sh) f -> ListS sh f
listsTail :: forall (n :: Nat) (sh :: [Nat]) (f :: Nat -> Type).
ListS (n : sh) f -> ListS sh f
listsTail (f n
_ ::$ ListS sh f
sh) = ListS sh f
ListS sh f
sh

listsInit :: ListS (n : sh) f -> ListS (Init (n : sh)) f
listsInit :: forall (n :: Nat) (sh :: [Nat]) (f :: Nat -> Type).
ListS (n : sh) f -> ListS (Init (n : sh)) f
listsInit (f n
n ::$ sh :: ListS sh f
sh@(f n
_ ::$ ListS sh f
_)) = f n
n f n -> ListS (Init (n : sh)) f -> ListS (n : Init (n : sh)) f
forall (n :: Nat) (sh :: [Nat]) {f :: Nat -> Type}.
KnownNat n =>
f n -> ListS sh f -> ListS (n : sh) f
::$ ListS (n : sh) f -> ListS (Init (n : sh)) f
forall (n :: Nat) (sh :: [Nat]) (f :: Nat -> Type).
ListS (n : sh) f -> ListS (Init (n : sh)) f
listsInit ListS sh f
ListS (n : sh) f
sh
listsInit (f n
_ ::$ ListS sh f
ZS) = ListS '[] f
ListS (Init (n : sh)) f
forall (f :: Nat -> Type). ListS '[] f
ZS

listsLast :: ListS (n : sh) f -> f (Last (n : sh))
listsLast :: forall (n :: Nat) (sh :: [Nat]) (f :: Nat -> Type).
ListS (n : sh) f -> f (Last (n : sh))
listsLast (f n
_ ::$ sh :: ListS sh f
sh@(f n
_ ::$ ListS sh f
_)) = ListS (n : sh) f -> f (Last (n : sh))
forall (n :: Nat) (sh :: [Nat]) (f :: Nat -> Type).
ListS (n : sh) f -> f (Last (n : sh))
listsLast ListS sh f
ListS (n : sh) f
sh
listsLast (f n
n ::$ ListS sh f
ZS) = f n
f (Last (n : sh))
n

listsAppend :: ListS sh f -> ListS sh' f -> ListS (sh ++ sh') f
listsAppend :: forall (sh :: [Nat]) (f :: Nat -> Type) (sh' :: [Nat]).
ListS sh f -> ListS sh' f -> ListS (sh ++ sh') f
listsAppend ListS sh f
ZS ListS sh' f
idx' = ListS sh' f
ListS (sh ++ sh') f
idx'
listsAppend (f n
i ::$ ListS sh f
idx) ListS sh' f
idx' = f n
i f n -> ListS (sh ++ sh') f -> ListS (n : (sh ++ sh')) f
forall (n :: Nat) (sh :: [Nat]) {f :: Nat -> Type}.
KnownNat n =>
f n -> ListS sh f -> ListS (n : sh) f
::$ ListS sh f -> ListS sh' f -> ListS (sh ++ sh') f
forall (sh :: [Nat]) (f :: Nat -> Type) (sh' :: [Nat]).
ListS sh f -> ListS sh' f -> ListS (sh ++ sh') f
listsAppend ListS sh f
idx ListS sh' f
idx'

listsZip :: ListS sh f -> ListS sh g -> ListS sh (Fun.Product f g)
listsZip :: forall (sh :: [Nat]) (f :: Nat -> Type) (g :: Nat -> Type).
ListS sh f -> ListS sh g -> ListS sh (Product f g)
listsZip ListS sh f
ZS ListS sh g
ZS = ListS sh (Product f g)
ListS '[] (Product f g)
forall (f :: Nat -> Type). ListS '[] f
ZS
listsZip (f n
i ::$ ListS sh f
is) (g n
j ::$ ListS sh g
js) =
  f n -> g n -> Product f g n
forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k).
f a -> g a -> Product f g a
Fun.Pair f n
i g n
g n
j Product f g n
-> ListS sh (Product f g) -> ListS (n : sh) (Product f g)
forall (n :: Nat) (sh :: [Nat]) {f :: Nat -> Type}.
KnownNat n =>
f n -> ListS sh f -> ListS (n : sh) f
::$ ListS sh f -> ListS sh g -> ListS sh (Product f g)
forall (sh :: [Nat]) (f :: Nat -> Type) (g :: Nat -> Type).
ListS sh f -> ListS sh g -> ListS sh (Product f g)
listsZip ListS sh f
is ListS sh g
ListS sh g
js

listsZipWith :: (forall a. f a -> g a -> h a) -> ListS sh f -> ListS sh g
             -> ListS sh h
listsZipWith :: forall (f :: Nat -> Type) (g :: Nat -> Type) (h :: Nat -> Type)
       (sh :: [Nat]).
(forall (a :: Nat). f a -> g a -> h a)
-> ListS sh f -> ListS sh g -> ListS sh h
listsZipWith forall (a :: Nat). f a -> g a -> h a
_ ListS sh f
ZS ListS sh g
ZS = ListS sh h
ListS '[] h
forall (f :: Nat -> Type). ListS '[] f
ZS
listsZipWith forall (a :: Nat). f a -> g a -> h a
f (f n
i ::$ ListS sh f
is) (g n
j ::$ ListS sh g
js) =
  f n -> g n -> h n
forall (a :: Nat). f a -> g a -> h a
f f n
i g n
g n
j h n -> ListS sh h -> ListS (n : sh) h
forall (n :: Nat) (sh :: [Nat]) {f :: Nat -> Type}.
KnownNat n =>
f n -> ListS sh f -> ListS (n : sh) f
::$ (forall (a :: Nat). f a -> g a -> h a)
-> ListS sh f -> ListS sh g -> ListS sh h
forall (f :: Nat -> Type) (g :: Nat -> Type) (h :: Nat -> Type)
       (sh :: [Nat]).
(forall (a :: Nat). f a -> g a -> h a)
-> ListS sh f -> ListS sh g -> ListS sh h
listsZipWith f a -> g a -> h a
forall (a :: Nat). f a -> g a -> h a
f ListS sh f
is ListS sh g
ListS sh g
js

listsTakeLenPerm :: forall f is sh. Perm is -> ListS sh f -> ListS (TakeLen is sh) f
listsTakeLenPerm :: forall (f :: Nat -> Type) (is :: [Nat]) (sh :: [Nat]).
Perm is -> ListS sh f -> ListS (TakeLen is sh) f
listsTakeLenPerm Perm is
PNil ListS sh f
_ = ListS '[] f
ListS (TakeLen is sh) f
forall (f :: Nat -> Type). ListS '[] f
ZS
listsTakeLenPerm (SNat a
_ `PCons` Perm l
is) (f n
n ::$ ListS sh f
sh) = f n
n f n -> ListS (TakeLen l sh) f -> ListS (n : TakeLen l sh) f
forall (n :: Nat) (sh :: [Nat]) {f :: Nat -> Type}.
KnownNat n =>
f n -> ListS sh f -> ListS (n : sh) f
::$ Perm l -> ListS sh f -> ListS (TakeLen l sh) f
forall (f :: Nat -> Type) (is :: [Nat]) (sh :: [Nat]).
Perm is -> ListS sh f -> ListS (TakeLen is sh) f
listsTakeLenPerm Perm l
is ListS sh f
sh
listsTakeLenPerm (SNat a
_ `PCons` Perm l
_) ListS sh f
ZS = String -> ListS (TakeLen (a : l) '[]) f
forall a. HasCallStack => String -> a
error String
"Permutation longer than shape"

listsDropLenPerm :: forall f is sh. Perm is -> ListS sh f -> ListS (DropLen is sh) f
listsDropLenPerm :: forall (f :: Nat -> Type) (is :: [Nat]) (sh :: [Nat]).
Perm is -> ListS sh f -> ListS (DropLen is sh) f
listsDropLenPerm Perm is
PNil ListS sh f
sh = ListS sh f
ListS (DropLen is sh) f
sh
listsDropLenPerm (SNat a
_ `PCons` Perm l
is) (f n
_ ::$ ListS sh f
sh) = Perm l -> ListS sh f -> ListS (DropLen l sh) f
forall (f :: Nat -> Type) (is :: [Nat]) (sh :: [Nat]).
Perm is -> ListS sh f -> ListS (DropLen is sh) f
listsDropLenPerm Perm l
is ListS sh f
sh
listsDropLenPerm (SNat a
_ `PCons` Perm l
_) ListS sh f
ZS = String -> ListS (DropLen (a : l) '[]) f
forall a. HasCallStack => String -> a
error String
"Permutation longer than shape"

listsPermute :: forall f is sh. Perm is -> ListS sh f -> ListS (Permute is sh) f
listsPermute :: forall (f :: Nat -> Type) (is :: [Nat]) (sh :: [Nat]).
Perm is -> ListS sh f -> ListS (Permute is sh) f
listsPermute Perm is
PNil ListS sh f
_ = ListS '[] f
ListS (Permute is sh) f
forall (f :: Nat -> Type). ListS '[] f
ZS
listsPermute (SNat a
i `PCons` (Perm l
is :: Perm is')) (ListS sh f
sh :: ListS sh f) =
  case Proxy l
-> Proxy sh
-> SNat a
-> ListS sh f
-> (f (Index a sh), SNat (Index a sh))
forall {k} {k} (f :: Nat -> Type) (i :: Nat) (is :: k)
       (sh :: [Nat]) (shT :: k).
Proxy is
-> Proxy shT
-> SNat i
-> ListS sh f
-> (f (Index i sh), SNat (Index i sh))
listsIndex (forall (t :: [Nat]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @is') (forall (t :: [Nat]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @sh) SNat a
i ListS sh f
sh of
    (f (Index a sh)
item, SNat (Index a sh)
SNat) -> f (Index a sh)
item f (Index a sh)
-> ListS (Permute l sh) f -> ListS (Index a sh : Permute l sh) f
forall (n :: Nat) (sh :: [Nat]) {f :: Nat -> Type}.
KnownNat n =>
f n -> ListS sh f -> ListS (n : sh) f
::$ Perm l -> ListS sh f -> ListS (Permute l sh) f
forall (f :: Nat -> Type) (is :: [Nat]) (sh :: [Nat]).
Perm is -> ListS sh f -> ListS (Permute is sh) f
listsPermute Perm l
is ListS sh f
sh

-- TODO: remove this SNat when the KnownNat constaint in ListS is removed
listsIndex :: forall f i is sh shT. Proxy is -> Proxy shT -> SNat i -> ListS sh f -> (f (Index i sh), SNat (Index i sh))
listsIndex :: forall {k} {k} (f :: Nat -> Type) (i :: Nat) (is :: k)
       (sh :: [Nat]) (shT :: k).
Proxy is
-> Proxy shT
-> SNat i
-> ListS sh f
-> (f (Index i sh), SNat (Index i sh))
listsIndex Proxy is
_ Proxy shT
_ SNat i
SZ (f n
n ::$ ListS sh f
_) = (f n
f (Index i sh)
n, SNat n
SNat (Index i sh)
forall (n :: Nat). KnownNat n => SNat n
SNat)
listsIndex Proxy is
p Proxy shT
pT (SS (SNat n
i :: SNat i')) ((f n
_ :: f n) ::$ (ListS sh f
sh :: ListS sh' f))
  | Index (n + 1) (n : sh) :~: Index n sh
Refl <- Proxy n
-> Proxy n -> Proxy sh -> Index (n + 1) (n : sh) :~: Index n sh
forall {k} (i :: Nat) (a :: k) (l :: [k]).
Proxy i
-> Proxy a -> Proxy l -> Index (i + 1) (a : l) :~: Index i l
lemIndexSucc (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @i') (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) (forall (t :: [Nat]). Proxy t
forall {k} (t :: k). Proxy t
Proxy @sh')
  = Proxy is
-> Proxy shT
-> SNat n
-> ListS sh f
-> (f (Index n sh), SNat (Index n sh))
forall {k} {k} (f :: Nat -> Type) (i :: Nat) (is :: k)
       (sh :: [Nat]) (shT :: k).
Proxy is
-> Proxy shT
-> SNat i
-> ListS sh f
-> (f (Index i sh), SNat (Index i sh))
listsIndex Proxy is
p Proxy shT
pT SNat n
i ListS sh f
sh
listsIndex Proxy is
_ Proxy shT
_ SNat i
_ ListS sh f
ZS = String -> (f (Index i '[]), SNat (Index i '[]))
forall a. HasCallStack => String -> a
error String
"Index into empty shape"

listsPermutePrefix :: forall f is sh. Perm is -> ListS sh f -> ListS (PermutePrefix is sh) f
listsPermutePrefix :: forall (f :: Nat -> Type) (is :: [Nat]) (sh :: [Nat]).
Perm is -> ListS sh f -> ListS (PermutePrefix is sh) f
listsPermutePrefix Perm is
perm ListS sh f
sh = ListS (Permute is (TakeLen is sh)) f
-> ListS (DropLen is sh) f
-> ListS (Permute is (TakeLen is sh) ++ DropLen is sh) f
forall (sh :: [Nat]) (f :: Nat -> Type) (sh' :: [Nat]).
ListS sh f -> ListS sh' f -> ListS (sh ++ sh') f
listsAppend (Perm is
-> ListS (TakeLen is sh) f -> ListS (Permute is (TakeLen is sh)) f
forall (f :: Nat -> Type) (is :: [Nat]) (sh :: [Nat]).
Perm is -> ListS sh f -> ListS (Permute is sh) f
listsPermute Perm is
perm (Perm is -> ListS sh f -> ListS (TakeLen is sh) f
forall (f :: Nat -> Type) (is :: [Nat]) (sh :: [Nat]).
Perm is -> ListS sh f -> ListS (TakeLen is sh) f
listsTakeLenPerm Perm is
perm ListS sh f
sh)) (Perm is -> ListS sh f -> ListS (DropLen is sh) f
forall (f :: Nat -> Type) (is :: [Nat]) (sh :: [Nat]).
Perm is -> ListS sh f -> ListS (DropLen is sh) f
listsDropLenPerm Perm is
perm ListS sh f
sh)

-- * Shaped indices

-- | An index into a shape-typed array.
type role IxS nominal representational
type IxS :: [Nat] -> Type -> Type
newtype IxS sh i = IxS (ListS sh (Const i))
  deriving (IxS sh i -> IxS sh i -> Bool
(IxS sh i -> IxS sh i -> Bool)
-> (IxS sh i -> IxS sh i -> Bool) -> Eq (IxS sh i)
forall (sh :: [Nat]) i. Eq i => IxS sh i -> IxS sh i -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (sh :: [Nat]) i. Eq i => IxS sh i -> IxS sh i -> Bool
== :: IxS sh i -> IxS sh i -> Bool
$c/= :: forall (sh :: [Nat]) i. Eq i => IxS sh i -> IxS sh i -> Bool
/= :: IxS sh i -> IxS sh i -> Bool
Eq, Eq (IxS sh i)
Eq (IxS sh i) =>
(IxS sh i -> IxS sh i -> Ordering)
-> (IxS sh i -> IxS sh i -> Bool)
-> (IxS sh i -> IxS sh i -> Bool)
-> (IxS sh i -> IxS sh i -> Bool)
-> (IxS sh i -> IxS sh i -> Bool)
-> (IxS sh i -> IxS sh i -> IxS sh i)
-> (IxS sh i -> IxS sh i -> IxS sh i)
-> Ord (IxS sh i)
IxS sh i -> IxS sh i -> Bool
IxS sh i -> IxS sh i -> Ordering
IxS sh i -> IxS sh i -> IxS sh i
forall (sh :: [Nat]) i. Ord i => Eq (IxS sh i)
forall (sh :: [Nat]) i. Ord i => IxS sh i -> IxS sh i -> Bool
forall (sh :: [Nat]) i. Ord i => IxS sh i -> IxS sh i -> Ordering
forall (sh :: [Nat]) i. Ord i => IxS sh i -> IxS sh i -> IxS sh i
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: forall (sh :: [Nat]) i. Ord i => IxS sh i -> IxS sh i -> Ordering
compare :: IxS sh i -> IxS sh i -> Ordering
$c< :: forall (sh :: [Nat]) i. Ord i => IxS sh i -> IxS sh i -> Bool
< :: IxS sh i -> IxS sh i -> Bool
$c<= :: forall (sh :: [Nat]) i. Ord i => IxS sh i -> IxS sh i -> Bool
<= :: IxS sh i -> IxS sh i -> Bool
$c> :: forall (sh :: [Nat]) i. Ord i => IxS sh i -> IxS sh i -> Bool
> :: IxS sh i -> IxS sh i -> Bool
$c>= :: forall (sh :: [Nat]) i. Ord i => IxS sh i -> IxS sh i -> Bool
>= :: IxS sh i -> IxS sh i -> Bool
$cmax :: forall (sh :: [Nat]) i. Ord i => IxS sh i -> IxS sh i -> IxS sh i
max :: IxS sh i -> IxS sh i -> IxS sh i
$cmin :: forall (sh :: [Nat]) i. Ord i => IxS sh i -> IxS sh i -> IxS sh i
min :: IxS sh i -> IxS sh i -> IxS sh i
Ord, (forall x. IxS sh i -> Rep (IxS sh i) x)
-> (forall x. Rep (IxS sh i) x -> IxS sh i) -> Generic (IxS sh i)
forall (sh :: [Nat]) i x. Rep (IxS sh i) x -> IxS sh i
forall (sh :: [Nat]) i x. IxS sh i -> Rep (IxS sh i) x
forall x. Rep (IxS sh i) x -> IxS sh i
forall x. IxS sh i -> Rep (IxS sh i) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (sh :: [Nat]) i x. IxS sh i -> Rep (IxS sh i) x
from :: forall x. IxS sh i -> Rep (IxS sh i) x
$cto :: forall (sh :: [Nat]) i x. Rep (IxS sh i) x -> IxS sh i
to :: forall x. Rep (IxS sh i) x -> IxS sh i
Generic)

pattern ZIS :: forall sh i. () => sh ~ '[] => IxS sh i
pattern $mZIS :: forall {r} {sh :: [Nat]} {i}.
IxS sh i -> ((sh ~ '[]) => r) -> ((# #) -> r) -> r
$bZIS :: forall (sh :: [Nat]) i. (sh ~ '[]) => IxS sh i
ZIS = IxS ZS

-- | Note: The 'KnownNat' constraint on '(:.$)' is deprecated and should be
-- removed in a future release.
pattern (:.$)
  :: forall {sh1} {i}.
     forall n sh. (KnownNat n, n : sh ~ sh1)
  => i -> IxS sh i -> IxS sh1 i
pattern i $m:.$ :: forall {r} {sh1 :: [Nat]} {i}.
IxS sh1 i
-> (forall {n :: Nat} {sh :: [Nat]}.
    (KnownNat n, (n : sh) ~ sh1) =>
    i -> IxS sh i -> r)
-> ((# #) -> r)
-> r
$b:.$ :: forall {sh1 :: [Nat]} {i} (n :: Nat) (sh :: [Nat]).
(KnownNat n, (n : sh) ~ sh1) =>
i -> IxS sh i -> IxS sh1 i
:.$ shl <- IxS (listsUncons -> Just (UnconsListSRes (IxS -> shl) (getConst -> i)))
  where i
i :.$ IxS ListS sh (Const i)
shl = ListS sh1 (Const i) -> IxS sh1 i
forall (sh :: [Nat]) i. ListS sh (Const i) -> IxS sh i
IxS (i -> Const i n
forall {k} a (b :: k). a -> Const a b
Const i
i Const i n -> ListS sh (Const i) -> ListS (n : sh) (Const i)
forall (n :: Nat) (sh :: [Nat]) {f :: Nat -> Type}.
KnownNat n =>
f n -> ListS sh f -> ListS (n : sh) f
::$ ListS sh (Const i)
shl)
infixr 3 :.$

{-# COMPLETE ZIS, (:.$) #-}

-- For convenience, this contains regular 'Int's instead of bounded integers
-- (traditionally called \"@Fin@\").
type IIxS sh = IxS sh Int

#ifdef OXAR_DEFAULT_SHOW_INSTANCES
deriving instance Show i => Show (IxS sh i)
#else
instance Show i => Show (IxS sh i) where
  showsPrec :: Int -> IxS sh i -> ShowS
showsPrec Int
_ (IxS ListS sh (Const i)
l) = (forall (n :: Nat). Const i n -> ShowS)
-> ListS sh (Const i) -> ShowS
forall (sh :: [Nat]) (f :: Nat -> Type).
(forall (n :: Nat). f n -> ShowS) -> ListS sh f -> ShowS
listsShow (\(Const i
i) -> i -> ShowS
forall a. Show a => a -> ShowS
shows i
i) ListS sh (Const i)
l
#endif

instance Functor (IxS sh) where
  fmap :: forall a b. (a -> b) -> IxS sh a -> IxS sh b
fmap a -> b
f (IxS ListS sh (Const a)
l) = ListS sh (Const b) -> IxS sh b
forall (sh :: [Nat]) i. ListS sh (Const i) -> IxS sh i
IxS ((forall (n :: Nat). Const a n -> Const b n)
-> ListS sh (Const a) -> ListS sh (Const b)
forall (f :: Nat -> Type) (g :: Nat -> Type) (sh :: [Nat]).
(forall (n :: Nat). f n -> g n) -> ListS sh f -> ListS sh g
listsFmap (b -> Const b n
forall {k} a (b :: k). a -> Const a b
Const (b -> Const b n) -> (Const a n -> b) -> Const a n -> Const b n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f (a -> b) -> (Const a n -> a) -> Const a n -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const a n -> a
forall {k} a (b :: k). Const a b -> a
getConst) ListS sh (Const a)
l)

instance Foldable (IxS sh) where
  foldMap :: forall m a. Monoid m => (a -> m) -> IxS sh a -> m
foldMap a -> m
f (IxS ListS sh (Const a)
l) = (forall (n :: Nat). Const a n -> m) -> ListS sh (Const a) -> m
forall m (f :: Nat -> Type) (sh :: [Nat]).
Monoid m =>
(forall (n :: Nat). f n -> m) -> ListS sh f -> m
listsFold (a -> m
f (a -> m) -> (Const a n -> a) -> Const a n -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const a n -> a
forall {k} a (b :: k). Const a b -> a
getConst) ListS sh (Const a)
l

instance NFData i => NFData (IxS sh i)

ixsLength :: IxS sh i -> Int
ixsLength :: forall (sh :: [Nat]) a. IxS sh a -> Int
ixsLength (IxS ListS sh (Const i)
l) = ListS sh (Const i) -> Int
forall (sh :: [Nat]) (f :: Nat -> Type). ListS sh f -> Int
listsLength ListS sh (Const i)
l

ixsRank :: IxS sh i -> SNat (Rank sh)
ixsRank :: forall (sh :: [Nat]) i. IxS sh i -> SNat (Rank sh)
ixsRank (IxS ListS sh (Const i)
l) = ListS sh (Const i) -> SNat (Rank sh)
forall (sh :: [Nat]) (f :: Nat -> Type).
ListS sh f -> SNat (Rank sh)
listsRank ListS sh (Const i)
l

ixsZero :: ShS sh -> IIxS sh
ixsZero :: forall (sh :: [Nat]). ShS sh -> IIxS sh
ixsZero ShS sh
ZSS = IxS sh Int
forall (sh :: [Nat]) i. (sh ~ '[]) => IxS sh i
ZIS
ixsZero (SNat n
_ :$$ ShS sh
sh) = Int
0 Int -> IxS sh Int -> IxS sh Int
forall {sh1 :: [Nat]} {i} (n :: Nat) (sh :: [Nat]).
(KnownNat n, (n : sh) ~ sh1) =>
i -> IxS sh i -> IxS sh1 i
:.$ ShS sh -> IxS sh Int
forall (sh :: [Nat]). ShS sh -> IIxS sh
ixsZero ShS sh
sh

ixsHead :: IxS (n : sh) i -> i
ixsHead :: forall (n :: Nat) (sh :: [Nat]) i. IxS (n : sh) i -> i
ixsHead (IxS ListS (n : sh) (Const i)
list) = Const i n -> i
forall {k} a (b :: k). Const a b -> a
getConst (ListS (n : sh) (Const i) -> Const i n
forall (n :: Nat) (sh :: [Nat]) (f :: Nat -> Type).
ListS (n : sh) f -> f n
listsHead ListS (n : sh) (Const i)
list)

ixsTail :: IxS (n : sh) i -> IxS sh i
ixsTail :: forall (n :: Nat) (sh :: [Nat]) i. IxS (n : sh) i -> IxS sh i
ixsTail (IxS ListS (n : sh) (Const i)
list) = ListS sh (Const i) -> IxS sh i
forall (sh :: [Nat]) i. ListS sh (Const i) -> IxS sh i
IxS (ListS (n : sh) (Const i) -> ListS sh (Const i)
forall (n :: Nat) (sh :: [Nat]) (f :: Nat -> Type).
ListS (n : sh) f -> ListS sh f
listsTail ListS (n : sh) (Const i)
list)

ixsInit :: IxS (n : sh) i -> IxS (Init (n : sh)) i
ixsInit :: forall (n :: Nat) (sh :: [Nat]) i.
IxS (n : sh) i -> IxS (Init (n : sh)) i
ixsInit (IxS ListS (n : sh) (Const i)
list) = ListS (Init (n : sh)) (Const i) -> IxS (Init (n : sh)) i
forall (sh :: [Nat]) i. ListS sh (Const i) -> IxS sh i
IxS (ListS (n : sh) (Const i) -> ListS (Init (n : sh)) (Const i)
forall (n :: Nat) (sh :: [Nat]) (f :: Nat -> Type).
ListS (n : sh) f -> ListS (Init (n : sh)) f
listsInit ListS (n : sh) (Const i)
list)

ixsLast :: IxS (n : sh) i -> i
ixsLast :: forall (n :: Nat) (sh :: [Nat]) i. IxS (n : sh) i -> i
ixsLast (IxS ListS (n : sh) (Const i)
list) = Const i (Last (n : sh)) -> i
forall {k} a (b :: k). Const a b -> a
getConst (ListS (n : sh) (Const i) -> Const i (Last (n : sh))
forall (n :: Nat) (sh :: [Nat]) (f :: Nat -> Type).
ListS (n : sh) f -> f (Last (n : sh))
listsLast ListS (n : sh) (Const i)
list)

-- TODO: this takes a ShS because there are KnownNats inside IxS.
ixsCast :: ShS sh' -> IxS sh i -> IxS sh' i
ixsCast :: forall (sh' :: [Nat]) (sh :: [Nat]) i.
ShS sh' -> IxS sh i -> IxS sh' i
ixsCast ShS sh'
ZSS IxS sh i
ZIS = IxS sh' i
forall (sh :: [Nat]) i. (sh ~ '[]) => IxS sh i
ZIS
ixsCast (SNat n
_ :$$ ShS sh
sh) (i
i :.$ IxS sh i
idx) = i
i i -> IxS sh i -> IxS sh' i
forall {sh1 :: [Nat]} {i} (n :: Nat) (sh :: [Nat]).
(KnownNat n, (n : sh) ~ sh1) =>
i -> IxS sh i -> IxS sh1 i
:.$ ShS sh -> IxS sh i -> IxS sh i
forall (sh' :: [Nat]) (sh :: [Nat]) i.
ShS sh' -> IxS sh i -> IxS sh' i
ixsCast ShS sh
sh IxS sh i
idx
ixsCast ShS sh'
_ IxS sh i
_ = String -> IxS sh' i
forall a. HasCallStack => String -> a
error String
"ixsCast: ranks don't match"

ixsAppend :: forall sh sh' i. IxS sh i -> IxS sh' i -> IxS (sh ++ sh') i
ixsAppend :: forall (sh :: [Nat]) (sh' :: [Nat]) i.
IxS sh i -> IxS sh' i -> IxS (sh ++ sh') i
ixsAppend = (ListS sh (Const i)
 -> ListS sh' (Const i) -> ListS (sh ++ sh') (Const i))
-> IxS sh i -> IxS sh' i -> IxS (sh ++ sh') i
forall a b. Coercible a b => a -> b
coerce (forall (sh :: [Nat]) (f :: Nat -> Type) (sh' :: [Nat]).
ListS sh f -> ListS sh' f -> ListS (sh ++ sh') f
listsAppend @_ @(Const i))

ixsZip :: IxS n i -> IxS n j -> IxS n (i, j)
ixsZip :: forall (n :: [Nat]) i j. IxS n i -> IxS n j -> IxS n (i, j)
ixsZip IxS n i
ZIS IxS n j
ZIS = IxS n (i, j)
forall (sh :: [Nat]) i. (sh ~ '[]) => IxS sh i
ZIS
ixsZip (i
i :.$ IxS sh i
is) (j
j :.$ IxS sh j
js) = (i
i, j
j) (i, j) -> IxS sh (i, j) -> IxS n (i, j)
forall {sh1 :: [Nat]} {i} (n :: Nat) (sh :: [Nat]).
(KnownNat n, (n : sh) ~ sh1) =>
i -> IxS sh i -> IxS sh1 i
:.$ IxS sh i -> IxS sh j -> IxS sh (i, j)
forall (n :: [Nat]) i j. IxS n i -> IxS n j -> IxS n (i, j)
ixsZip IxS sh i
is IxS sh j
IxS sh j
js

ixsZipWith :: (i -> j -> k) -> IxS n i -> IxS n j -> IxS n k
ixsZipWith :: forall i j k (n :: [Nat]).
(i -> j -> k) -> IxS n i -> IxS n j -> IxS n k
ixsZipWith i -> j -> k
_ IxS n i
ZIS IxS n j
ZIS = IxS n k
forall (sh :: [Nat]) i. (sh ~ '[]) => IxS sh i
ZIS
ixsZipWith i -> j -> k
f (i
i :.$ IxS sh i
is) (j
j :.$ IxS sh j
js) = i -> j -> k
f i
i j
j k -> IxS sh k -> IxS n k
forall {sh1 :: [Nat]} {i} (n :: Nat) (sh :: [Nat]).
(KnownNat n, (n : sh) ~ sh1) =>
i -> IxS sh i -> IxS sh1 i
:.$ (i -> j -> k) -> IxS sh i -> IxS sh j -> IxS sh k
forall i j k (n :: [Nat]).
(i -> j -> k) -> IxS n i -> IxS n j -> IxS n k
ixsZipWith i -> j -> k
f IxS sh i
is IxS sh j
IxS sh j
js

ixsPermutePrefix :: forall i is sh. Perm is -> IxS sh i -> IxS (PermutePrefix is sh) i
ixsPermutePrefix :: forall i (is :: [Nat]) (sh :: [Nat]).
Perm is -> IxS sh i -> IxS (PermutePrefix is sh) i
ixsPermutePrefix = (Perm is
 -> ListS sh (Const i)
 -> ListS (Permute is (TakeLen is sh) ++ DropLen is sh) (Const i))
-> Perm is
-> IxS sh i
-> IxS (Permute is (TakeLen is sh) ++ DropLen is sh) i
forall a b. Coercible a b => a -> b
coerce (forall (f :: Nat -> Type) (is :: [Nat]) (sh :: [Nat]).
Perm is -> ListS sh f -> ListS (PermutePrefix is sh) f
listsPermutePrefix @(Const i))


-- * Shaped shapes

-- | The shape of a shape-typed array given as a list of 'SNat' values.
--
-- Note that because the shape of a shape-typed array is known statically, you
-- can also retrieve the array shape from a 'KnownShS' dictionary.
type role ShS nominal
type ShS :: [Nat] -> Type
newtype ShS sh = ShS (ListS sh SNat)
  deriving (ShS sh -> ShS sh -> Bool
(ShS sh -> ShS sh -> Bool)
-> (ShS sh -> ShS sh -> Bool) -> Eq (ShS sh)
forall (sh :: [Nat]). ShS sh -> ShS sh -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (sh :: [Nat]). ShS sh -> ShS sh -> Bool
== :: ShS sh -> ShS sh -> Bool
$c/= :: forall (sh :: [Nat]). ShS sh -> ShS sh -> Bool
/= :: ShS sh -> ShS sh -> Bool
Eq, Eq (ShS sh)
Eq (ShS sh) =>
(ShS sh -> ShS sh -> Ordering)
-> (ShS sh -> ShS sh -> Bool)
-> (ShS sh -> ShS sh -> Bool)
-> (ShS sh -> ShS sh -> Bool)
-> (ShS sh -> ShS sh -> Bool)
-> (ShS sh -> ShS sh -> ShS sh)
-> (ShS sh -> ShS sh -> ShS sh)
-> Ord (ShS sh)
ShS sh -> ShS sh -> Bool
ShS sh -> ShS sh -> Ordering
ShS sh -> ShS sh -> ShS sh
forall (sh :: [Nat]). Eq (ShS sh)
forall (sh :: [Nat]). ShS sh -> ShS sh -> Bool
forall (sh :: [Nat]). ShS sh -> ShS sh -> Ordering
forall (sh :: [Nat]). ShS sh -> ShS sh -> ShS sh
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: forall (sh :: [Nat]). ShS sh -> ShS sh -> Ordering
compare :: ShS sh -> ShS sh -> Ordering
$c< :: forall (sh :: [Nat]). ShS sh -> ShS sh -> Bool
< :: ShS sh -> ShS sh -> Bool
$c<= :: forall (sh :: [Nat]). ShS sh -> ShS sh -> Bool
<= :: ShS sh -> ShS sh -> Bool
$c> :: forall (sh :: [Nat]). ShS sh -> ShS sh -> Bool
> :: ShS sh -> ShS sh -> Bool
$c>= :: forall (sh :: [Nat]). ShS sh -> ShS sh -> Bool
>= :: ShS sh -> ShS sh -> Bool
$cmax :: forall (sh :: [Nat]). ShS sh -> ShS sh -> ShS sh
max :: ShS sh -> ShS sh -> ShS sh
$cmin :: forall (sh :: [Nat]). ShS sh -> ShS sh -> ShS sh
min :: ShS sh -> ShS sh -> ShS sh
Ord, (forall x. ShS sh -> Rep (ShS sh) x)
-> (forall x. Rep (ShS sh) x -> ShS sh) -> Generic (ShS sh)
forall (sh :: [Nat]) x. Rep (ShS sh) x -> ShS sh
forall (sh :: [Nat]) x. ShS sh -> Rep (ShS sh) x
forall x. Rep (ShS sh) x -> ShS sh
forall x. ShS sh -> Rep (ShS sh) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (sh :: [Nat]) x. ShS sh -> Rep (ShS sh) x
from :: forall x. ShS sh -> Rep (ShS sh) x
$cto :: forall (sh :: [Nat]) x. Rep (ShS sh) x -> ShS sh
to :: forall x. Rep (ShS sh) x -> ShS sh
Generic)

pattern ZSS :: forall sh. () => sh ~ '[] => ShS sh
pattern $mZSS :: forall {r} {sh :: [Nat]}.
ShS sh -> ((sh ~ '[]) => r) -> ((# #) -> r) -> r
$bZSS :: forall (sh :: [Nat]). (sh ~ '[]) => ShS sh
ZSS = ShS ZS

pattern (:$$)
  :: forall {sh1}.
     forall n sh. (KnownNat n, n : sh ~ sh1)
  => SNat n -> ShS sh -> ShS sh1
pattern i $m:$$ :: forall {r} {sh1 :: [Nat]}.
ShS sh1
-> (forall {n :: Nat} {sh :: [Nat]}.
    (KnownNat n, (n : sh) ~ sh1) =>
    SNat n -> ShS sh -> r)
-> ((# #) -> r)
-> r
$b:$$ :: forall {sh1 :: [Nat]} (n :: Nat) (sh :: [Nat]).
(KnownNat n, (n : sh) ~ sh1) =>
SNat n -> ShS sh -> ShS sh1
:$$ shl <- ShS (listsUncons -> Just (UnconsListSRes (ShS -> shl) i))
  where SNat n
i :$$ ShS ListS sh SNat
shl = ListS sh1 SNat -> ShS sh1
forall (sh :: [Nat]). ListS sh SNat -> ShS sh
ShS (SNat n
i SNat n -> ListS sh SNat -> ListS (n : sh) SNat
forall (n :: Nat) (sh :: [Nat]) {f :: Nat -> Type}.
KnownNat n =>
f n -> ListS sh f -> ListS (n : sh) f
::$ ListS sh SNat
shl)

infixr 3 :$$

{-# COMPLETE ZSS, (:$$) #-}

#ifdef OXAR_DEFAULT_SHOW_INSTANCES
deriving instance Show (ShS sh)
#else
instance Show (ShS sh) where
  showsPrec :: Int -> ShS sh -> ShowS
showsPrec Int
_ (ShS ListS sh SNat
l) = (forall (n :: Nat). SNat n -> ShowS) -> ListS sh SNat -> ShowS
forall (sh :: [Nat]) (f :: Nat -> Type).
(forall (n :: Nat). f n -> ShowS) -> ListS sh f -> ShowS
listsShow (Integer -> ShowS
forall a. Show a => a -> ShowS
shows (Integer -> ShowS) -> (SNat n -> Integer) -> SNat n -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat n -> Integer
forall (n :: Nat). SNat n -> Integer
fromSNat) ListS sh SNat
l
#endif

instance NFData (ShS sh) where
  rnf :: ShS sh -> ()
rnf (ShS ListS sh SNat
ZS) = ()
  rnf (ShS (SNat n
SNat ::$ ListS sh SNat
l)) = ShS sh -> ()
forall a. NFData a => a -> ()
rnf (ListS sh SNat -> ShS sh
forall (sh :: [Nat]). ListS sh SNat -> ShS sh
ShS ListS sh SNat
l)

instance TestEquality ShS where
  testEquality :: forall (a :: [Nat]) (b :: [Nat]). ShS a -> ShS b -> Maybe (a :~: b)
testEquality (ShS ListS a SNat
l1) (ShS ListS b SNat
l2) = ListS a SNat -> ListS b SNat -> Maybe (a :~: b)
forall (f :: Nat -> Type) (sh :: [Nat]) (sh' :: [Nat]).
TestEquality f =>
ListS sh f -> ListS sh' f -> Maybe (sh :~: sh')
listsEqType ListS a SNat
l1 ListS b SNat
l2

-- | @'shsEqual' = 'testEquality'@. (Because 'ShS' is a singleton, types are
-- equal if and only if values are equal.)
shsEqual :: ShS sh -> ShS sh' -> Maybe (sh :~: sh')
shsEqual :: forall (a :: [Nat]) (b :: [Nat]). ShS a -> ShS b -> Maybe (a :~: b)
shsEqual = ShS sh -> ShS sh' -> Maybe (sh :~: sh')
forall (a :: [Nat]) (b :: [Nat]). ShS a -> ShS b -> Maybe (a :~: b)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality

shsLength :: ShS sh -> Int
shsLength :: forall (sh :: [Nat]). ShS sh -> Int
shsLength (ShS ListS sh SNat
l) = ListS sh SNat -> Int
forall (sh :: [Nat]) (f :: Nat -> Type). ListS sh f -> Int
listsLength ListS sh SNat
l

shsRank :: ShS sh -> SNat (Rank sh)
shsRank :: forall (sh :: [Nat]). ShS sh -> SNat (Rank sh)
shsRank (ShS ListS sh SNat
l) = ListS sh SNat -> SNat (Rank sh)
forall (sh :: [Nat]) (f :: Nat -> Type).
ListS sh f -> SNat (Rank sh)
listsRank ListS sh SNat
l

shsSize :: ShS sh -> Int
shsSize :: forall (sh :: [Nat]). ShS sh -> Int
shsSize ShS sh
ZSS = Int
1
shsSize (SNat n
n :$$ ShS sh
sh) = SNat n -> Int
forall (n :: Nat). SNat n -> Int
fromSNat' SNat n
n Int -> Int -> Int
forall a. Num a => a -> a -> a
* ShS sh -> Int
forall (sh :: [Nat]). ShS sh -> Int
shsSize ShS sh
sh

shsToList :: ShS sh -> [Int]
shsToList :: forall (sh :: [Nat]). ShS sh -> [Int]
shsToList ShS sh
ZSS = []
shsToList (SNat n
sn :$$ ShS sh
sh) = SNat n -> Int
forall (n :: Nat). SNat n -> Int
fromSNat' SNat n
sn Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: ShS sh -> [Int]
forall (sh :: [Nat]). ShS sh -> [Int]
shsToList ShS sh
sh

shsHead :: ShS (n : sh) -> SNat n
shsHead :: forall (n :: Nat) (sh :: [Nat]). ShS (n : sh) -> SNat n
shsHead (ShS ListS (n : sh) SNat
list) = ListS (n : sh) SNat -> SNat n
forall (n :: Nat) (sh :: [Nat]) (f :: Nat -> Type).
ListS (n : sh) f -> f n
listsHead ListS (n : sh) SNat
list

shsTail :: ShS (n : sh) -> ShS sh
shsTail :: forall (n :: Nat) (sh :: [Nat]). ShS (n : sh) -> ShS sh
shsTail (ShS ListS (n : sh) SNat
list) = ListS sh SNat -> ShS sh
forall (sh :: [Nat]). ListS sh SNat -> ShS sh
ShS (ListS (n : sh) SNat -> ListS sh SNat
forall (n :: Nat) (sh :: [Nat]) (f :: Nat -> Type).
ListS (n : sh) f -> ListS sh f
listsTail ListS (n : sh) SNat
list)

shsInit :: ShS (n : sh) -> ShS (Init (n : sh))
shsInit :: forall (n :: Nat) (sh :: [Nat]).
ShS (n : sh) -> ShS (Init (n : sh))
shsInit (ShS ListS (n : sh) SNat
list) = ListS (Init (n : sh)) SNat -> ShS (Init (n : sh))
forall (sh :: [Nat]). ListS sh SNat -> ShS sh
ShS (ListS (n : sh) SNat -> ListS (Init (n : sh)) SNat
forall (n :: Nat) (sh :: [Nat]) (f :: Nat -> Type).
ListS (n : sh) f -> ListS (Init (n : sh)) f
listsInit ListS (n : sh) SNat
list)

shsLast :: ShS (n : sh) -> SNat (Last (n : sh))
shsLast :: forall (n :: Nat) (sh :: [Nat]).
ShS (n : sh) -> SNat (Last (n : sh))
shsLast (ShS ListS (n : sh) SNat
list) = ListS (n : sh) SNat -> SNat (Last (n : sh))
forall (n :: Nat) (sh :: [Nat]) (f :: Nat -> Type).
ListS (n : sh) f -> f (Last (n : sh))
listsLast ListS (n : sh) SNat
list

shsAppend :: forall sh sh'. ShS sh -> ShS sh' -> ShS (sh ++ sh')
shsAppend :: forall (sh :: [Nat]) (sh' :: [Nat]).
ShS sh -> ShS sh' -> ShS (sh ++ sh')
shsAppend = (ListS sh SNat -> ListS sh' SNat -> ListS (sh ++ sh') SNat)
-> ShS sh -> ShS sh' -> ShS (sh ++ sh')
forall a b. Coercible a b => a -> b
coerce (forall (sh :: [Nat]) (f :: Nat -> Type) (sh' :: [Nat]).
ListS sh f -> ListS sh' f -> ListS (sh ++ sh') f
listsAppend @_ @SNat)

shsTakeLen :: Perm is -> ShS sh -> ShS (TakeLen is sh)
shsTakeLen :: forall (is :: [Nat]) (sh :: [Nat]).
Perm is -> ShS sh -> ShS (TakeLen is sh)
shsTakeLen = (Perm is -> ListS sh SNat -> ListS (TakeLen is sh) SNat)
-> Perm is -> ShS sh -> ShS (TakeLen is sh)
forall a b. Coercible a b => a -> b
coerce (forall (f :: Nat -> Type) (is :: [Nat]) (sh :: [Nat]).
Perm is -> ListS sh f -> ListS (TakeLen is sh) f
listsTakeLenPerm @SNat)

shsPermute :: Perm is -> ShS sh -> ShS (Permute is sh)
shsPermute :: forall (is :: [Nat]) (sh :: [Nat]).
Perm is -> ShS sh -> ShS (Permute is sh)
shsPermute = (Perm is -> ListS sh SNat -> ListS (Permute is sh) SNat)
-> Perm is -> ShS sh -> ShS (Permute is sh)
forall a b. Coercible a b => a -> b
coerce (forall (f :: Nat -> Type) (is :: [Nat]) (sh :: [Nat]).
Perm is -> ListS sh f -> ListS (Permute is sh) f
listsPermute @SNat)

shsIndex :: Proxy is -> Proxy shT -> SNat i -> ShS sh -> SNat (Index i sh)
shsIndex :: forall {k} {k} (is :: k) (shT :: k) (i :: Nat) (sh :: [Nat]).
Proxy is -> Proxy shT -> SNat i -> ShS sh -> SNat (Index i sh)
shsIndex Proxy is
pis Proxy shT
pshT SNat i
i ShS sh
sh = SNat (Index i sh) -> SNat (Index i sh)
forall a b. Coercible a b => a -> b
coerce ((SNat (Index i sh), SNat (Index i sh)) -> SNat (Index i sh)
forall a b. (a, b) -> a
fst (forall {k} {k} (f :: Nat -> Type) (i :: Nat) (is :: k)
       (sh :: [Nat]) (shT :: k).
Proxy is
-> Proxy shT
-> SNat i
-> ListS sh f
-> (f (Index i sh), SNat (Index i sh))
forall (f :: Nat -> Type) (i :: Nat) (is :: k) (sh :: [Nat])
       (shT :: k).
Proxy is
-> Proxy shT
-> SNat i
-> ListS sh f
-> (f (Index i sh), SNat (Index i sh))
listsIndex @SNat Proxy is
pis Proxy shT
pshT SNat i
i (ShS sh -> ListS sh SNat
forall a b. Coercible a b => a -> b
coerce ShS sh
sh)))

shsPermutePrefix :: forall is sh. Perm is -> ShS sh -> ShS (PermutePrefix is sh)
shsPermutePrefix :: forall (is :: [Nat]) (sh :: [Nat]).
Perm is -> ShS sh -> ShS (PermutePrefix is sh)
shsPermutePrefix = (Perm is
 -> ListS sh SNat
 -> ListS (Permute is (TakeLen is sh) ++ DropLen is sh) SNat)
-> Perm is
-> ShS sh
-> ShS (Permute is (TakeLen is sh) ++ DropLen is sh)
forall a b. Coercible a b => a -> b
coerce (forall (f :: Nat -> Type) (is :: [Nat]) (sh :: [Nat]).
Perm is -> ListS sh f -> ListS (PermutePrefix is sh) f
listsPermutePrefix @SNat)

type family Product sh where
  Product '[] = 1
  Product (n : ns) = n * Product ns

shsProduct :: ShS sh -> SNat (Product sh)
shsProduct :: forall (sh :: [Nat]). ShS sh -> SNat (Product sh)
shsProduct ShS sh
ZSS = SNat 1
SNat (Product sh)
forall (n :: Nat). KnownNat n => SNat n
SNat
shsProduct (SNat n
n :$$ ShS sh
sh) = SNat n
n SNat n -> SNat (Product sh) -> SNat (n * Product sh)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n * m)
`snatMul` ShS sh -> SNat (Product sh)
forall (sh :: [Nat]). ShS sh -> SNat (Product sh)
shsProduct ShS sh
sh

-- | Evidence for the static part of a shape. This pops up only when you are
-- polymorphic in the element type of an array.
type KnownShS :: [Nat] -> Constraint
class KnownShS sh where knownShS :: ShS sh
instance KnownShS '[] where knownShS :: ShS '[]
knownShS = ShS '[]
forall (sh :: [Nat]). (sh ~ '[]) => ShS sh
ZSS
instance (KnownNat n, KnownShS sh) => KnownShS (n : sh) where knownShS :: ShS (n : sh)
knownShS = SNat n
forall (n :: Nat). KnownNat n => SNat n
natSing SNat n -> ShS sh -> ShS (n : sh)
forall {sh1 :: [Nat]} (n :: Nat) (sh :: [Nat]).
(KnownNat n, (n : sh) ~ sh1) =>
SNat n -> ShS sh -> ShS sh1
:$$ ShS sh
forall (sh :: [Nat]). KnownShS sh => ShS sh
knownShS

withKnownShS :: forall sh r. ShS sh -> (KnownShS sh => r) -> r
withKnownShS :: forall (sh :: [Nat]) r. ShS sh -> (KnownShS sh => r) -> r
withKnownShS = forall (cls :: Constraint) meth r.
WithDict cls meth =>
meth -> (cls => r) -> r
withDict @(KnownShS sh)

shsKnownShS :: ShS sh -> Dict KnownShS sh
shsKnownShS :: forall (sh :: [Nat]). ShS sh -> Dict KnownShS sh
shsKnownShS ShS sh
ZSS = Dict KnownShS sh
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
shsKnownShS (SNat n
SNat :$$ ShS sh
sh) | Dict KnownShS sh
Dict <- ShS sh -> Dict KnownShS sh
forall (sh :: [Nat]). ShS sh -> Dict KnownShS sh
shsKnownShS ShS sh
sh = Dict KnownShS sh
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict

shsOrthotopeShape :: ShS sh -> Dict O.Shape sh
shsOrthotopeShape :: forall (sh :: [Nat]). ShS sh -> Dict Shape sh
shsOrthotopeShape ShS sh
ZSS = Dict Shape sh
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict
shsOrthotopeShape (SNat n
SNat :$$ ShS sh
sh) | Dict Shape sh
Dict <- ShS sh -> Dict Shape sh
forall (sh :: [Nat]). ShS sh -> Dict Shape sh
shsOrthotopeShape ShS sh
sh = Dict Shape sh
forall {k} (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict

-- | This function is a hack made possible by the 'KnownNat' inside 'ListS'.
-- This function may be removed in a future release.
shsFromListS :: ListS sh f -> ShS sh
shsFromListS :: forall (sh :: [Nat]) (f :: Nat -> Type). ListS sh f -> ShS sh
shsFromListS ListS sh f
ZS = ShS sh
forall (sh :: [Nat]). (sh ~ '[]) => ShS sh
ZSS
shsFromListS (f n
_ ::$ ListS sh f
l) = SNat n
forall (n :: Nat). KnownNat n => SNat n
SNat SNat n -> ShS sh -> ShS sh
forall {sh1 :: [Nat]} (n :: Nat) (sh :: [Nat]).
(KnownNat n, (n : sh) ~ sh1) =>
SNat n -> ShS sh -> ShS sh1
:$$ ListS sh f -> ShS sh
forall (sh :: [Nat]) (f :: Nat -> Type). ListS sh f -> ShS sh
shsFromListS ListS sh f
l

-- | This function is a hack made possible by the 'KnownNat' inside 'IxS'. This
-- function may be removed in a future release.
shsFromIxS :: IxS sh i -> ShS sh
shsFromIxS :: forall (sh :: [Nat]) i. IxS sh i -> ShS sh
shsFromIxS (IxS ListS sh (Const i)
l) = ListS sh (Const i) -> ShS sh
forall (sh :: [Nat]) (f :: Nat -> Type). ListS sh f -> ShS sh
shsFromListS ListS sh (Const i)
l


-- | Untyped: length is checked at runtime.
instance KnownShS sh => IsList (ListS sh (Const i)) where
  type Item (ListS sh (Const i)) = i
  fromList :: [Item (ListS sh (Const i))] -> ListS sh (Const i)
fromList [Item (ListS sh (Const i))]
topl = ShS sh -> [i] -> ListS sh (Const i)
forall (sh' :: [Nat]). ShS sh' -> [i] -> ListS sh' (Const i)
go (forall (sh :: [Nat]). KnownShS sh => ShS sh
knownShS @sh) [i]
[Item (ListS sh (Const i))]
topl
    where
      go :: ShS sh' -> [i] -> ListS sh' (Const i)
      go :: forall (sh' :: [Nat]). ShS sh' -> [i] -> ListS sh' (Const i)
go ShS sh'
ZSS [] = ListS sh' (Const i)
ListS '[] (Const i)
forall (f :: Nat -> Type). ListS '[] f
ZS
      go (SNat n
_ :$$ ShS sh
sh) (i
i : [i]
is) = i -> Const i n
forall {k} a (b :: k). a -> Const a b
Const i
i Const i n -> ListS sh (Const i) -> ListS (n : sh) (Const i)
forall (n :: Nat) (sh :: [Nat]) {f :: Nat -> Type}.
KnownNat n =>
f n -> ListS sh f -> ListS (n : sh) f
::$ ShS sh -> [i] -> ListS sh (Const i)
forall (sh' :: [Nat]). ShS sh' -> [i] -> ListS sh' (Const i)
go ShS sh
sh [i]
is
      go ShS sh'
_ [i]
_ = String -> ListS sh' (Const i)
forall a. HasCallStack => String -> a
error (String -> ListS sh' (Const i)) -> String -> ListS sh' (Const i)
forall a b. (a -> b) -> a -> b
$ String
"IsList(ListS): Mismatched list length (type says "
                         String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (ShS sh -> Int
forall (sh :: [Nat]). ShS sh -> Int
shsLength (forall (sh :: [Nat]). KnownShS sh => ShS sh
knownShS @sh)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", list has length "
                         String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([i] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [i]
[Item (ListS sh (Const i))]
topl) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  toList :: ListS sh (Const i) -> [Item (ListS sh (Const i))]
toList = ListS sh (Const i) -> [i]
ListS sh (Const i) -> [Item (ListS sh (Const i))]
forall (sh :: [Nat]) i. ListS sh (Const i) -> [i]
listsToList

-- | Very untyped: only length is checked (at runtime), index bounds are __not checked__.
instance KnownShS sh => IsList (IxS sh i) where
  type Item (IxS sh i) = i
  fromList :: [Item (IxS sh i)] -> IxS sh i
fromList = ListS sh (Const i) -> IxS sh i
forall (sh :: [Nat]) i. ListS sh (Const i) -> IxS sh i
IxS (ListS sh (Const i) -> IxS sh i)
-> ([i] -> ListS sh (Const i)) -> [i] -> IxS sh i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [i] -> ListS sh (Const i)
[Item (ListS sh (Const i))] -> ListS sh (Const i)
forall l. IsList l => [Item l] -> l
IsList.fromList
  toList :: IxS sh i -> [Item (IxS sh i)]
toList = IxS sh i -> [i]
IxS sh i -> [Item (IxS sh i)]
forall a. IxS sh a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
Foldable.toList

-- | Untyped: length and values are checked at runtime.
instance KnownShS sh => IsList (ShS sh) where
  type Item (ShS sh) = Int
  fromList :: [Item (ShS sh)] -> ShS sh
fromList [Item (ShS sh)]
topl = ListS sh SNat -> ShS sh
forall (sh :: [Nat]). ListS sh SNat -> ShS sh
ShS (ShS sh -> [Int] -> ListS sh SNat
forall (sh' :: [Nat]). ShS sh' -> [Int] -> ListS sh' SNat
go (forall (sh :: [Nat]). KnownShS sh => ShS sh
knownShS @sh) [Int]
[Item (ShS sh)]
topl)
    where
      go :: ShS sh' -> [Int] -> ListS sh' SNat
      go :: forall (sh' :: [Nat]). ShS sh' -> [Int] -> ListS sh' SNat
go ShS sh'
ZSS [] = ListS sh' SNat
ListS '[] SNat
forall (f :: Nat -> Type). ListS '[] f
ZS
      go (SNat n
sn :$$ ShS sh
sh) (Int
i : [Int]
is)
        | Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== SNat n -> Int
forall (n :: Nat). SNat n -> Int
fromSNat' SNat n
sn = SNat n
sn SNat n -> ListS sh SNat -> ListS (n : sh) SNat
forall (n :: Nat) (sh :: [Nat]) {f :: Nat -> Type}.
KnownNat n =>
f n -> ListS sh f -> ListS (n : sh) f
::$ ShS sh -> [Int] -> ListS sh SNat
forall (sh' :: [Nat]). ShS sh' -> [Int] -> ListS sh' SNat
go ShS sh
sh [Int]
is
        | Bool
otherwise = String -> ListS sh' SNat
forall a. HasCallStack => String -> a
error (String -> ListS sh' SNat) -> String -> ListS sh' SNat
forall a b. (a -> b) -> a -> b
$ String
"IsList(ShS): Value does not match typing (type says "
                                String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (SNat n -> Int
forall (n :: Nat). SNat n -> Int
fromSNat' SNat n
sn) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", list contains " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
      go ShS sh'
_ [Int]
_ = String -> ListS sh' SNat
forall a. HasCallStack => String -> a
error (String -> ListS sh' SNat) -> String -> ListS sh' SNat
forall a b. (a -> b) -> a -> b
$ String
"IsList(ShS): Mismatched list length (type says "
                         String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (ShS sh -> Int
forall (sh :: [Nat]). ShS sh -> Int
shsLength (forall (sh :: [Nat]). KnownShS sh => ShS sh
knownShS @sh)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", list has length "
                         String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Int] -> Int
forall a. [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length [Int]
[Item (ShS sh)]
topl) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  toList :: ShS sh -> [Item (ShS sh)]
toList = ShS sh -> [Int]
ShS sh -> [Item (ShS sh)]
forall (sh :: [Nat]). ShS sh -> [Int]
shsToList