{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# 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.Ranked.Shape where

import Control.DeepSeq (NFData(..))
import Data.Coerce (coerce)
import Data.Foldable qualified as Foldable
import Data.Kind (Type)
import Data.Proxy
import Data.Type.Equality
import GHC.Generics (Generic)
import GHC.IsList (IsList)
import GHC.IsList qualified as IsList
import GHC.TypeLits
import GHC.TypeNats qualified as TN

import Data.Array.Nested.Lemmas
import Data.Array.Nested.Types


-- * Ranked lists

type role ListR nominal representational
type ListR :: Nat -> Type -> Type
data ListR n i where
  ZR :: ListR 0 i
  (:::) :: forall n {i}. i -> ListR n i -> ListR (n + 1) i
deriving instance Eq i => Eq (ListR n i)
deriving instance Ord i => Ord (ListR n i)
deriving instance Functor (ListR n)
deriving instance Foldable (ListR n)
infixr 3 :::

#ifdef OXAR_DEFAULT_SHOW_INSTANCES
deriving instance Show i => Show (ListR n i)
#else
instance Show i => Show (ListR n i) where
  showsPrec :: Int -> ListR n i -> ShowS
showsPrec Int
_ = (i -> ShowS) -> ListR n i -> ShowS
forall (n :: Natural) i. (i -> ShowS) -> ListR n i -> ShowS
listrShow i -> ShowS
forall a. Show a => a -> ShowS
shows
#endif

instance NFData i => NFData (ListR n i) where
  rnf :: ListR n i -> ()
rnf ListR n i
ZR = ()
  rnf (i
x ::: ListR n i
l) = i -> ()
forall a. NFData a => a -> ()
rnf i
x () -> () -> ()
forall a b. a -> b -> b
`seq` ListR n i -> ()
forall a. NFData a => a -> ()
rnf ListR n i
l

data UnconsListRRes i n1 =
  forall n. (n + 1 ~ n1) => UnconsListRRes (ListR n i) i
listrUncons :: ListR n1 i -> Maybe (UnconsListRRes i n1)
listrUncons :: forall (n1 :: Natural) i. ListR n1 i -> Maybe (UnconsListRRes i n1)
listrUncons (i
i ::: ListR n i
sh') = UnconsListRRes i n1 -> Maybe (UnconsListRRes i n1)
forall a. a -> Maybe a
Just (ListR n i -> i -> UnconsListRRes i n1
forall i (n1 :: Natural) (n :: Natural).
((n + 1) ~ n1) =>
ListR n i -> i -> UnconsListRRes i n1
UnconsListRRes ListR n i
sh' i
i)
listrUncons ListR n1 i
ZR = Maybe (UnconsListRRes i n1)
forall a. Maybe a
Nothing

-- | This checks only whether the ranks are equal, not whether the actual
-- values are.
listrEqRank :: ListR n i -> ListR n' i -> Maybe (n :~: n')
listrEqRank :: forall (n :: Natural) i (n' :: Natural).
ListR n i -> ListR n' i -> Maybe (n :~: n')
listrEqRank ListR n i
ZR ListR n' i
ZR = (n :~: n') -> Maybe (n :~: n')
forall a. a -> Maybe a
Just n :~: n
n :~: n'
forall {k} (a :: k). a :~: a
Refl
listrEqRank (i
_ ::: ListR n i
sh) (i
_ ::: ListR n i
sh')
  | Just n :~: n
Refl <- ListR n i -> ListR n i -> Maybe (n :~: n)
forall (n :: Natural) i (n' :: Natural).
ListR n i -> ListR n' i -> Maybe (n :~: n')
listrEqRank ListR n i
sh ListR n i
sh'
  = (n :~: n') -> Maybe (n :~: n')
forall a. a -> Maybe a
Just n :~: n
n :~: n'
forall {k} (a :: k). a :~: a
Refl
listrEqRank ListR n i
_ ListR n' i
_ = Maybe (n :~: n')
forall a. Maybe a
Nothing

-- | This compares the lists for value equality.
listrEqual :: Eq i => ListR n i -> ListR n' i -> Maybe (n :~: n')
listrEqual :: forall i (n :: Natural) (n' :: Natural).
Eq i =>
ListR n i -> ListR n' i -> Maybe (n :~: n')
listrEqual ListR n i
ZR ListR n' i
ZR = (n :~: n') -> Maybe (n :~: n')
forall a. a -> Maybe a
Just n :~: n
n :~: n'
forall {k} (a :: k). a :~: a
Refl
listrEqual (i
i ::: ListR n i
sh) (i
j ::: ListR n i
sh')
  | Just n :~: n
Refl <- ListR n i -> ListR n i -> Maybe (n :~: n)
forall i (n :: Natural) (n' :: Natural).
Eq i =>
ListR n i -> ListR n' i -> Maybe (n :~: n')
listrEqual ListR n i
sh ListR n i
sh'
  , i
i i -> i -> Bool
forall a. Eq a => a -> a -> Bool
== i
j
  = (n :~: n') -> Maybe (n :~: n')
forall a. a -> Maybe a
Just n :~: n
n :~: n'
forall {k} (a :: k). a :~: a
Refl
listrEqual ListR n i
_ ListR n' i
_ = Maybe (n :~: n')
forall a. Maybe a
Nothing

listrShow :: forall n i. (i -> ShowS) -> ListR n i -> ShowS
listrShow :: forall (n :: Natural) i. (i -> ShowS) -> ListR n i -> ShowS
listrShow i -> ShowS
f ListR n i
l = String -> ShowS
showString String
"[" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ListR n i -> ShowS
forall (n' :: Natural). String -> ListR n' i -> ShowS
go String
"" ListR n i
l ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ShowS
showString String
"]"
  where
    go :: String -> ListR n' i -> ShowS
    go :: forall (n' :: Natural). String -> ListR n' i -> ShowS
go String
_ ListR n' i
ZR = ShowS
forall a. a -> a
id
    go String
prefix (i
x ::: ListR n i
xs) = String -> ShowS
showString String
prefix ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. i -> ShowS
f i
x ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> ListR n i -> ShowS
forall (n' :: Natural). String -> ListR n' i -> ShowS
go String
"," ListR n i
xs

listrLength :: ListR n i -> Int
listrLength :: forall (n :: Natural) a. ListR n a -> Int
listrLength = ListR n i -> Int
forall a. ListR n a -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
length

listrRank :: ListR n i -> SNat n
listrRank :: forall (n :: Natural) i. ListR n i -> SNat n
listrRank ListR n i
ZR = SNat n
forall (n :: Natural). KnownNat n => SNat n
SNat
listrRank (i
_ ::: ListR n i
sh) = SNat n -> SNat (n + 1)
forall (n :: Natural). SNat n -> SNat (n + 1)
snatSucc (ListR n i -> SNat n
forall (n :: Natural) i. ListR n i -> SNat n
listrRank ListR n i
sh)

listrAppend :: ListR n i -> ListR m i -> ListR (n + m) i
listrAppend :: forall (n :: Natural) i (m :: Natural).
ListR n i -> ListR m i -> ListR (n + m) i
listrAppend ListR n i
ZR ListR m i
sh = ListR m i
ListR (n + m) i
sh
listrAppend (i
x ::: ListR n i
xs) ListR m i
sh = i
x i -> ListR (n + m) i -> ListR ((n + m) + 1) i
forall (n :: Natural) {i}. i -> ListR n i -> ListR (n + 1) i
::: ListR n i -> ListR m i -> ListR (n + m) i
forall (n :: Natural) i (m :: Natural).
ListR n i -> ListR m i -> ListR (n + m) i
listrAppend ListR n i
xs ListR m i
sh

listrFromList :: [i] -> (forall n. ListR n i -> r) -> r
listrFromList :: forall i r. [i] -> (forall (n :: Natural). ListR n i -> r) -> r
listrFromList [] forall (n :: Natural). ListR n i -> r
k = ListR 0 i -> r
forall (n :: Natural). ListR n i -> r
k ListR 0 i
forall i. ListR 0 i
ZR
listrFromList (i
x : [i]
xs) forall (n :: Natural). ListR n i -> r
k = [i] -> (forall (n :: Natural). ListR n i -> r) -> r
forall i r. [i] -> (forall (n :: Natural). ListR n i -> r) -> r
listrFromList [i]
xs ((forall (n :: Natural). ListR n i -> r) -> r)
-> (forall (n :: Natural). ListR n i -> r) -> r
forall a b. (a -> b) -> a -> b
$ \ListR n i
l -> ListR (n + 1) i -> r
forall (n :: Natural). ListR n i -> r
k (i
x i -> ListR n i -> ListR (n + 1) i
forall (n :: Natural) {i}. i -> ListR n i -> ListR (n + 1) i
::: ListR n i
l)

listrHead :: ListR (n + 1) i -> i
listrHead :: forall (n :: Natural) i. ListR (n + 1) i -> i
listrHead (i
i ::: ListR n i
_) = i
i
listrHead ListR (n + 1) i
ZR = String -> i
forall a. HasCallStack => String -> a
error String
"unreachable"

listrTail :: ListR (n + 1) i -> ListR n i
listrTail :: forall (n :: Natural) i. ListR (n + 1) i -> ListR n i
listrTail (i
_ ::: ListR n i
sh) = ListR n i
ListR n i
sh
listrTail ListR (n + 1) i
ZR = String -> ListR n i
forall a. HasCallStack => String -> a
error String
"unreachable"

listrInit :: ListR (n + 1) i -> ListR n i
listrInit :: forall (n :: Natural) i. ListR (n + 1) i -> ListR n i
listrInit (i
n ::: sh :: ListR n i
sh@(i
_ ::: ListR n i
_)) = i
n i -> ListR n i -> ListR (n + 1) i
forall (n :: Natural) {i}. i -> ListR n i -> ListR (n + 1) i
::: ListR (n + 1) i -> ListR n i
forall (n :: Natural) i. ListR (n + 1) i -> ListR n i
listrInit ListR n i
ListR (n + 1) i
sh
listrInit (i
_ ::: ListR n i
ZR) = ListR n i
ListR 0 i
forall i. ListR 0 i
ZR
listrInit ListR (n + 1) i
ZR = String -> ListR n i
forall a. HasCallStack => String -> a
error String
"unreachable"

listrLast :: ListR (n + 1) i -> i
listrLast :: forall (n :: Natural) i. ListR (n + 1) i -> i
listrLast (i
_ ::: sh :: ListR n i
sh@(i
_ ::: ListR n i
_)) = ListR (n + 1) i -> i
forall (n :: Natural) i. ListR (n + 1) i -> i
listrLast ListR n i
ListR (n + 1) i
sh
listrLast (i
n ::: ListR n i
ZR) = i
n
listrLast ListR (n + 1) i
ZR = String -> i
forall a. HasCallStack => String -> a
error String
"unreachable"

-- | Performs a runtime check that the lengths are identical.
listrCast :: SNat n' -> ListR n i -> ListR n' i
listrCast :: forall (n' :: Natural) (n :: Natural) i.
SNat n' -> ListR n i -> ListR n' i
listrCast = String -> SNat n' -> ListR n i -> ListR n' i
forall (n' :: Natural) (n :: Natural) i.
String -> SNat n' -> ListR n i -> ListR n' i
listrCastWithName String
"listrCast"

listrIndex :: forall k n i. (k + 1 <= n) => SNat k -> ListR n i -> i
listrIndex :: forall (k :: Natural) (n :: Natural) i.
((k + 1) <= n) =>
SNat k -> ListR n i -> i
listrIndex SNat k
SZ (i
x ::: ListR n i
_) = i
x
listrIndex (SS SNat n
i) (i
_ ::: ListR n i
xs) | (k <=? (n - 1)) :~: 'True
Refl <- Proxy k -> Proxy n -> (k <=? (n - 1)) :~: 'True
forall (k :: Natural) (n :: Natural).
((k + 1) <= n) =>
Proxy k -> Proxy n -> (k <=? (n - 1)) :~: 'True
lemLeqSuccSucc (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @k) (forall (t :: Natural). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n) = SNat n -> ListR n i -> i
forall (k :: Natural) (n :: Natural) i.
((k + 1) <= n) =>
SNat k -> ListR n i -> i
listrIndex SNat n
i ListR n i
xs
listrIndex SNat k
_ ListR n i
ZR = String -> i
forall a. HasCallStack => String -> a
error String
"k + 1 <= 0"

listrZip :: ListR n i -> ListR n j -> ListR n (i, j)
listrZip :: forall (n :: Natural) i j. ListR n i -> ListR n j -> ListR n (i, j)
listrZip ListR n i
ZR ListR n j
ZR = ListR n (i, j)
ListR 0 (i, j)
forall i. ListR 0 i
ZR
listrZip (i
i ::: ListR n i
irest) (j
j ::: ListR n j
jrest) = (i
i, j
j) (i, j) -> ListR n (i, j) -> ListR (n + 1) (i, j)
forall (n :: Natural) {i}. i -> ListR n i -> ListR (n + 1) i
::: ListR n i -> ListR n j -> ListR n (i, j)
forall (n :: Natural) i j. ListR n i -> ListR n j -> ListR n (i, j)
listrZip ListR n i
irest ListR n j
ListR n j
jrest
listrZip ListR n i
_ ListR n j
_ = String -> ListR n (i, j)
forall a. HasCallStack => String -> a
error String
"listrZip: impossible pattern needlessly required"

listrZipWith :: (i -> j -> k) -> ListR n i -> ListR n j -> ListR n k
listrZipWith :: forall i j k (n :: Natural).
(i -> j -> k) -> ListR n i -> ListR n j -> ListR n k
listrZipWith i -> j -> k
_ ListR n i
ZR ListR n j
ZR = ListR n k
ListR 0 k
forall i. ListR 0 i
ZR
listrZipWith i -> j -> k
f (i
i ::: ListR n i
irest) (j
j ::: ListR n j
jrest) =
  i -> j -> k
f i
i j
j k -> ListR n k -> ListR (n + 1) k
forall (n :: Natural) {i}. i -> ListR n i -> ListR (n + 1) i
::: (i -> j -> k) -> ListR n i -> ListR n j -> ListR n k
forall i j k (n :: Natural).
(i -> j -> k) -> ListR n i -> ListR n j -> ListR n k
listrZipWith i -> j -> k
f ListR n i
irest ListR n j
ListR n j
jrest
listrZipWith i -> j -> k
_ ListR n i
_ ListR n j
_ =
  String -> ListR n k
forall a. HasCallStack => String -> a
error String
"listrZipWith: impossible pattern needlessly required"

listrPermutePrefix :: forall i n. [Int] -> ListR n i -> ListR n i
listrPermutePrefix :: forall i (n :: Natural). [Int] -> ListR n i -> ListR n i
listrPermutePrefix = \[Int]
perm ListR n i
sh ->
  [Int]
-> (forall {n :: Natural}. ListR n Int -> ListR n i) -> ListR n i
forall i r. [i] -> (forall (n :: Natural). ListR n i -> r) -> r
listrFromList [Int]
perm ((forall {n :: Natural}. ListR n Int -> ListR n i) -> ListR n i)
-> (forall {n :: Natural}. ListR n Int -> ListR n i) -> ListR n i
forall a b. (a -> b) -> a -> b
$ \ListR n Int
sperm ->
    case (ListR n Int -> SNat n
forall (n :: Natural) i. ListR n i -> SNat n
listrRank ListR n Int
sperm, ListR n i -> SNat n
forall (n :: Natural) i. ListR n i -> SNat n
listrRank ListR n i
sh) of
      (permlen :: SNat n
permlen@SNat n
SNat, shlen :: SNat n
shlen@SNat n
SNat) -> case SNat n -> SNat n -> OrderingI n n
forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> Type)
       (proxy2 :: Natural -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat SNat n
permlen SNat n
shlen of
        OrderingI n n
LTI -> let (ListR n i
pre, ListR (n - n) i
post) = SNat n -> ListR n i -> (ListR n i, ListR (n - n) i)
forall (m :: Natural) (n' :: Natural).
(m <= n') =>
SNat m -> ListR n' i -> (ListR m i, ListR (n' - m) i)
listrSplitAt SNat n
permlen ListR n i
sh in ListR n i -> ListR (n - n) i -> ListR (n + (n - n)) i
forall (n :: Natural) i (m :: Natural).
ListR n i -> ListR m i -> ListR (n + m) i
listrAppend (SNat n -> ListR n Int -> ListR n i -> ListR n i
forall (m :: Natural) (k :: Natural).
SNat m -> ListR k Int -> ListR m i -> ListR k i
applyPermRFull SNat n
permlen ListR n Int
sperm ListR n i
pre) ListR (n - n) i
post
        OrderingI n n
EQI -> let (ListR n i
pre, ListR (n - n) i
post) = SNat n -> ListR n i -> (ListR n i, ListR (n - n) i)
forall (m :: Natural) (n' :: Natural).
(m <= n') =>
SNat m -> ListR n' i -> (ListR m i, ListR (n' - m) i)
listrSplitAt SNat n
permlen ListR n i
sh in ListR n i -> ListR (n - n) i -> ListR (n + (n - n)) i
forall (n :: Natural) i (m :: Natural).
ListR n i -> ListR m i -> ListR (n + m) i
listrAppend (SNat n -> ListR n Int -> ListR n i -> ListR n i
forall (m :: Natural) (k :: Natural).
SNat m -> ListR k Int -> ListR m i -> ListR k i
applyPermRFull SNat n
permlen ListR n Int
sperm ListR n i
pre) ListR (n - n) i
ListR (n - n) i
post
        OrderingI n n
GTI -> String -> ListR n i
forall a. HasCallStack => String -> a
error (String -> ListR n i) -> String -> ListR n i
forall a b. (a -> b) -> a -> b
$ String
"Length of permutation (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (SNat n -> Int
forall (n :: Natural). SNat n -> Int
fromSNat' SNat n
permlen) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
                       String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" > length of shape (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (SNat n -> Int
forall (n :: Natural). SNat n -> Int
fromSNat' SNat n
shlen) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  where
    listrSplitAt :: m <= n' => SNat m -> ListR n' i -> (ListR m i, ListR (n' - m) i)
    listrSplitAt :: forall (m :: Natural) (n' :: Natural).
(m <= n') =>
SNat m -> ListR n' i -> (ListR m i, ListR (n' - m) i)
listrSplitAt SNat m
SZ ListR n' i
sh = (ListR m i
ListR 0 i
forall i. ListR 0 i
ZR, ListR n' i
ListR (n' - m) i
sh)
    listrSplitAt (SS SNat n
m) (i
n ::: ListR n i
sh) = (\(ListR n i
pre, ListR (n' - m) i
post) -> (i
n i -> ListR n i -> ListR (n + 1) i
forall (n :: Natural) {i}. i -> ListR n i -> ListR (n + 1) i
::: ListR n i
pre, ListR (n' - m) i
post)) (SNat n -> ListR n i -> (ListR n i, ListR (n - n) i)
forall (m :: Natural) (n' :: Natural).
(m <= n') =>
SNat m -> ListR n' i -> (ListR m i, ListR (n' - m) i)
listrSplitAt SNat n
m ListR n i
sh)
    listrSplitAt SS{} ListR n' i
ZR = String -> (ListR m i, ListR (0 - m) i)
forall a. HasCallStack => String -> a
error String
"m' + 1 <= 0"

    applyPermRFull :: SNat m -> ListR k Int -> ListR m i -> ListR k i
    applyPermRFull :: forall (m :: Natural) (k :: Natural).
SNat m -> ListR k Int -> ListR m i -> ListR k i
applyPermRFull SNat m
_ ListR k Int
ZR ListR m i
_ = ListR k i
ListR 0 i
forall i. ListR 0 i
ZR
    applyPermRFull sm :: SNat m
sm@SNat m
SNat (Int
i ::: ListR n Int
perm) ListR m i
l =
      Natural
-> (forall {n :: Natural}. SNat n -> ListR k i) -> ListR k i
forall r. Natural -> (forall (n :: Natural). SNat n -> r) -> r
TN.withSomeSNat (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i) ((forall {n :: Natural}. SNat n -> ListR k i) -> ListR k i)
-> (forall {n :: Natural}. SNat n -> ListR k i) -> ListR k i
forall a b. (a -> b) -> a -> b
$ \si :: SNat n
si@(SNat n
SNat :: SNat idx) ->
        case SNat (n + 1) -> SNat m -> OrderingI (n + 1) m
forall (a :: Natural) (b :: Natural) (proxy1 :: Natural -> Type)
       (proxy2 :: Natural -> Type).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (forall (n :: Natural). KnownNat n => SNat n
SNat @(idx + 1)) SNat m
sm of
          OrderingI (n + 1) m
LTI -> SNat n -> ListR m i -> i
forall (k :: Natural) (n :: Natural) i.
((k + 1) <= n) =>
SNat k -> ListR n i -> i
listrIndex SNat n
si ListR m i
l i -> ListR n i -> ListR (n + 1) i
forall (n :: Natural) {i}. i -> ListR n i -> ListR (n + 1) i
::: SNat m -> ListR n Int -> ListR m i -> ListR n i
forall (m :: Natural) (k :: Natural).
SNat m -> ListR k Int -> ListR m i -> ListR k i
applyPermRFull SNat m
sm ListR n Int
perm ListR m i
l
          OrderingI (n + 1) m
EQI -> SNat n -> ListR m i -> i
forall (k :: Natural) (n :: Natural) i.
((k + 1) <= n) =>
SNat k -> ListR n i -> i
listrIndex SNat n
si ListR m i
l i -> ListR n i -> ListR (n + 1) i
forall (n :: Natural) {i}. i -> ListR n i -> ListR (n + 1) i
::: SNat m -> ListR n Int -> ListR m i -> ListR n i
forall (m :: Natural) (k :: Natural).
SNat m -> ListR k Int -> ListR m i -> ListR k i
applyPermRFull SNat m
sm ListR n Int
perm ListR m i
l
          OrderingI (n + 1) m
GTI -> String -> ListR k i
forall a. HasCallStack => String -> a
error String
"listrPermutePrefix: Index in permutation out of range"


-- * Ranked indices

-- | An index into a rank-typed array.
type role IxR nominal representational
type IxR :: Nat -> Type -> Type
newtype IxR n i = IxR (ListR n i)
  deriving (IxR n i -> IxR n i -> Bool
(IxR n i -> IxR n i -> Bool)
-> (IxR n i -> IxR n i -> Bool) -> Eq (IxR n i)
forall (n :: Natural) i. Eq i => IxR n i -> IxR n i -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (n :: Natural) i. Eq i => IxR n i -> IxR n i -> Bool
== :: IxR n i -> IxR n i -> Bool
$c/= :: forall (n :: Natural) i. Eq i => IxR n i -> IxR n i -> Bool
/= :: IxR n i -> IxR n i -> Bool
Eq, Eq (IxR n i)
Eq (IxR n i) =>
(IxR n i -> IxR n i -> Ordering)
-> (IxR n i -> IxR n i -> Bool)
-> (IxR n i -> IxR n i -> Bool)
-> (IxR n i -> IxR n i -> Bool)
-> (IxR n i -> IxR n i -> Bool)
-> (IxR n i -> IxR n i -> IxR n i)
-> (IxR n i -> IxR n i -> IxR n i)
-> Ord (IxR n i)
IxR n i -> IxR n i -> Bool
IxR n i -> IxR n i -> Ordering
IxR n i -> IxR n i -> IxR n i
forall (n :: Natural) i. Ord i => Eq (IxR n i)
forall (n :: Natural) i. Ord i => IxR n i -> IxR n i -> Bool
forall (n :: Natural) i. Ord i => IxR n i -> IxR n i -> Ordering
forall (n :: Natural) i. Ord i => IxR n i -> IxR n i -> IxR n 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 (n :: Natural) i. Ord i => IxR n i -> IxR n i -> Ordering
compare :: IxR n i -> IxR n i -> Ordering
$c< :: forall (n :: Natural) i. Ord i => IxR n i -> IxR n i -> Bool
< :: IxR n i -> IxR n i -> Bool
$c<= :: forall (n :: Natural) i. Ord i => IxR n i -> IxR n i -> Bool
<= :: IxR n i -> IxR n i -> Bool
$c> :: forall (n :: Natural) i. Ord i => IxR n i -> IxR n i -> Bool
> :: IxR n i -> IxR n i -> Bool
$c>= :: forall (n :: Natural) i. Ord i => IxR n i -> IxR n i -> Bool
>= :: IxR n i -> IxR n i -> Bool
$cmax :: forall (n :: Natural) i. Ord i => IxR n i -> IxR n i -> IxR n i
max :: IxR n i -> IxR n i -> IxR n i
$cmin :: forall (n :: Natural) i. Ord i => IxR n i -> IxR n i -> IxR n i
min :: IxR n i -> IxR n i -> IxR n i
Ord, (forall x. IxR n i -> Rep (IxR n i) x)
-> (forall x. Rep (IxR n i) x -> IxR n i) -> Generic (IxR n i)
forall (n :: Natural) i x. Rep (IxR n i) x -> IxR n i
forall (n :: Natural) i x. IxR n i -> Rep (IxR n i) x
forall x. Rep (IxR n i) x -> IxR n i
forall x. IxR n i -> Rep (IxR n i) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (n :: Natural) i x. IxR n i -> Rep (IxR n i) x
from :: forall x. IxR n i -> Rep (IxR n i) x
$cto :: forall (n :: Natural) i x. Rep (IxR n i) x -> IxR n i
to :: forall x. Rep (IxR n i) x -> IxR n i
Generic)
  deriving newtype ((forall a b. (a -> b) -> IxR n a -> IxR n b)
-> (forall a b. a -> IxR n b -> IxR n a) -> Functor (IxR n)
forall (n :: Natural) a b. a -> IxR n b -> IxR n a
forall (n :: Natural) a b. (a -> b) -> IxR n a -> IxR n b
forall a b. a -> IxR n b -> IxR n a
forall a b. (a -> b) -> IxR n a -> IxR n b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (n :: Natural) a b. (a -> b) -> IxR n a -> IxR n b
fmap :: forall a b. (a -> b) -> IxR n a -> IxR n b
$c<$ :: forall (n :: Natural) a b. a -> IxR n b -> IxR n a
<$ :: forall a b. a -> IxR n b -> IxR n a
Functor, (forall m. Monoid m => IxR n m -> m)
-> (forall m a. Monoid m => (a -> m) -> IxR n a -> m)
-> (forall m a. Monoid m => (a -> m) -> IxR n a -> m)
-> (forall a b. (a -> b -> b) -> b -> IxR n a -> b)
-> (forall a b. (a -> b -> b) -> b -> IxR n a -> b)
-> (forall b a. (b -> a -> b) -> b -> IxR n a -> b)
-> (forall b a. (b -> a -> b) -> b -> IxR n a -> b)
-> (forall a. (a -> a -> a) -> IxR n a -> a)
-> (forall a. (a -> a -> a) -> IxR n a -> a)
-> (forall a. IxR n a -> [a])
-> (forall a. IxR n a -> Bool)
-> (forall a. IxR n a -> Int)
-> (forall a. Eq a => a -> IxR n a -> Bool)
-> (forall a. Ord a => IxR n a -> a)
-> (forall a. Ord a => IxR n a -> a)
-> (forall a. Num a => IxR n a -> a)
-> (forall a. Num a => IxR n a -> a)
-> Foldable (IxR n)
forall (n :: Natural) a. Eq a => a -> IxR n a -> Bool
forall (n :: Natural) a. Num a => IxR n a -> a
forall (n :: Natural) a. Ord a => IxR n a -> a
forall (n :: Natural) m. Monoid m => IxR n m -> m
forall (n :: Natural) a. IxR n a -> Bool
forall (n :: Natural) a. IxR n a -> Int
forall (n :: Natural) a. IxR n a -> [a]
forall (n :: Natural) a. (a -> a -> a) -> IxR n a -> a
forall (n :: Natural) m a. Monoid m => (a -> m) -> IxR n a -> m
forall (n :: Natural) b a. (b -> a -> b) -> b -> IxR n a -> b
forall (n :: Natural) a b. (a -> b -> b) -> b -> IxR n a -> b
forall a. Eq a => a -> IxR n a -> Bool
forall a. Num a => IxR n a -> a
forall a. Ord a => IxR n a -> a
forall m. Monoid m => IxR n m -> m
forall a. IxR n a -> Bool
forall a. IxR n a -> Int
forall a. IxR n a -> [a]
forall a. (a -> a -> a) -> IxR n a -> a
forall m a. Monoid m => (a -> m) -> IxR n a -> m
forall b a. (b -> a -> b) -> b -> IxR n a -> b
forall a b. (a -> b -> b) -> b -> IxR n a -> b
forall (t :: Type -> Type).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall (n :: Natural) m. Monoid m => IxR n m -> m
fold :: forall m. Monoid m => IxR n m -> m
$cfoldMap :: forall (n :: Natural) m a. Monoid m => (a -> m) -> IxR n a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> IxR n a -> m
$cfoldMap' :: forall (n :: Natural) m a. Monoid m => (a -> m) -> IxR n a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> IxR n a -> m
$cfoldr :: forall (n :: Natural) a b. (a -> b -> b) -> b -> IxR n a -> b
foldr :: forall a b. (a -> b -> b) -> b -> IxR n a -> b
$cfoldr' :: forall (n :: Natural) a b. (a -> b -> b) -> b -> IxR n a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> IxR n a -> b
$cfoldl :: forall (n :: Natural) b a. (b -> a -> b) -> b -> IxR n a -> b
foldl :: forall b a. (b -> a -> b) -> b -> IxR n a -> b
$cfoldl' :: forall (n :: Natural) b a. (b -> a -> b) -> b -> IxR n a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> IxR n a -> b
$cfoldr1 :: forall (n :: Natural) a. (a -> a -> a) -> IxR n a -> a
foldr1 :: forall a. (a -> a -> a) -> IxR n a -> a
$cfoldl1 :: forall (n :: Natural) a. (a -> a -> a) -> IxR n a -> a
foldl1 :: forall a. (a -> a -> a) -> IxR n a -> a
$ctoList :: forall (n :: Natural) a. IxR n a -> [a]
toList :: forall a. IxR n a -> [a]
$cnull :: forall (n :: Natural) a. IxR n a -> Bool
null :: forall a. IxR n a -> Bool
$clength :: forall (n :: Natural) a. IxR n a -> Int
length :: forall a. IxR n a -> Int
$celem :: forall (n :: Natural) a. Eq a => a -> IxR n a -> Bool
elem :: forall a. Eq a => a -> IxR n a -> Bool
$cmaximum :: forall (n :: Natural) a. Ord a => IxR n a -> a
maximum :: forall a. Ord a => IxR n a -> a
$cminimum :: forall (n :: Natural) a. Ord a => IxR n a -> a
minimum :: forall a. Ord a => IxR n a -> a
$csum :: forall (n :: Natural) a. Num a => IxR n a -> a
sum :: forall a. Num a => IxR n a -> a
$cproduct :: forall (n :: Natural) a. Num a => IxR n a -> a
product :: forall a. Num a => IxR n a -> a
Foldable)

pattern ZIR :: forall n i. () => n ~ 0 => IxR n i
pattern $mZIR :: forall {r} {n :: Natural} {i}.
IxR n i -> ((n ~ 0) => r) -> ((# #) -> r) -> r
$bZIR :: forall (n :: Natural) i. (n ~ 0) => IxR n i
ZIR = IxR ZR

pattern (:.:)
  :: forall {n1} {i}.
     forall n. (n + 1 ~ n1)
  => i -> IxR n i -> IxR n1 i
pattern i $m:.: :: forall {r} {n1 :: Natural} {i}.
IxR n1 i
-> (forall {n :: Natural}. ((n + 1) ~ n1) => i -> IxR n i -> r)
-> ((# #) -> r)
-> r
$b:.: :: forall {n1 :: Natural} {i} (n :: Natural).
((n + 1) ~ n1) =>
i -> IxR n i -> IxR n1 i
:.: sh <- IxR (listrUncons -> Just (UnconsListRRes (IxR -> sh) i))
  where i
i :.: IxR ListR n i
sh = ListR n1 i -> IxR n1 i
forall (n :: Natural) i. ListR n i -> IxR n i
IxR (i
i i -> ListR n i -> ListR (n + 1) i
forall (n :: Natural) {i}. i -> ListR n i -> ListR (n + 1) i
::: ListR n i
sh)
infixr 3 :.:

{-# COMPLETE ZIR, (:.:) #-}

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

#ifdef OXAR_DEFAULT_SHOW_INSTANCES
deriving instance Show i => Show (IxR n i)
#else
instance Show i => Show (IxR n i) where
  showsPrec :: Int -> IxR n i -> ShowS
showsPrec Int
_ (IxR ListR n i
l) = (i -> ShowS) -> ListR n i -> ShowS
forall (n :: Natural) i. (i -> ShowS) -> ListR n i -> ShowS
listrShow i -> ShowS
forall a. Show a => a -> ShowS
shows ListR n i
l
#endif

instance NFData i => NFData (IxR sh i)

ixrLength :: IxR sh i -> Int
ixrLength :: forall (n :: Natural) a. IxR n a -> Int
ixrLength (IxR ListR sh i
l) = ListR sh i -> Int
forall (n :: Natural) a. ListR n a -> Int
listrLength ListR sh i
l

ixrRank :: IxR n i -> SNat n
ixrRank :: forall (n :: Natural) i. IxR n i -> SNat n
ixrRank (IxR ListR n i
sh) = ListR n i -> SNat n
forall (n :: Natural) i. ListR n i -> SNat n
listrRank ListR n i
sh

ixrZero :: SNat n -> IIxR n
ixrZero :: forall (n :: Natural). SNat n -> IIxR n
ixrZero SNat n
SZ = IxR n Int
forall (n :: Natural) i. (n ~ 0) => IxR n i
ZIR
ixrZero (SS SNat n
n) = Int
0 Int -> IxR n Int -> IxR n Int
forall {n1 :: Natural} {i} (n :: Natural).
((n + 1) ~ n1) =>
i -> IxR n i -> IxR n1 i
:.: SNat n -> IxR n Int
forall (n :: Natural). SNat n -> IIxR n
ixrZero SNat n
n

ixrHead :: IxR (n + 1) i -> i
ixrHead :: forall (n :: Natural) i. IxR (n + 1) i -> i
ixrHead (IxR ListR (n + 1) i
list) = ListR (n + 1) i -> i
forall (n :: Natural) i. ListR (n + 1) i -> i
listrHead ListR (n + 1) i
list

ixrTail :: IxR (n + 1) i -> IxR n i
ixrTail :: forall (n :: Natural) i. IxR (n + 1) i -> IxR n i
ixrTail (IxR ListR (n + 1) i
list) = ListR n i -> IxR n i
forall (n :: Natural) i. ListR n i -> IxR n i
IxR (ListR (n + 1) i -> ListR n i
forall (n :: Natural) i. ListR (n + 1) i -> ListR n i
listrTail ListR (n + 1) i
list)

ixrInit :: IxR (n + 1) i -> IxR n i
ixrInit :: forall (n :: Natural) i. IxR (n + 1) i -> IxR n i
ixrInit (IxR ListR (n + 1) i
list) = ListR n i -> IxR n i
forall (n :: Natural) i. ListR n i -> IxR n i
IxR (ListR (n + 1) i -> ListR n i
forall (n :: Natural) i. ListR (n + 1) i -> ListR n i
listrInit ListR (n + 1) i
list)

ixrLast :: IxR (n + 1) i -> i
ixrLast :: forall (n :: Natural) i. IxR (n + 1) i -> i
ixrLast (IxR ListR (n + 1) i
list) = ListR (n + 1) i -> i
forall (n :: Natural) i. ListR (n + 1) i -> i
listrLast ListR (n + 1) i
list

-- | Performs a runtime check that the lengths are identical.
ixrCast :: SNat n' -> IxR n i -> IxR n' i
ixrCast :: forall (n' :: Natural) (n :: Natural) i.
SNat n' -> IxR n i -> IxR n' i
ixrCast SNat n'
n (IxR ListR n i
idx) = ListR n' i -> IxR n' i
forall (n :: Natural) i. ListR n i -> IxR n i
IxR (String -> SNat n' -> ListR n i -> ListR n' i
forall (n' :: Natural) (n :: Natural) i.
String -> SNat n' -> ListR n i -> ListR n' i
listrCastWithName String
"ixrCast" SNat n'
n ListR n i
idx)

ixrAppend :: forall n m i. IxR n i -> IxR m i -> IxR (n + m) i
ixrAppend :: forall (n :: Natural) (m :: Natural) i.
IxR n i -> IxR m i -> IxR (n + m) i
ixrAppend = (ListR n i -> ListR m i -> ListR (n + m) i)
-> IxR n i -> IxR m i -> IxR (n + m) i
forall a b. Coercible a b => a -> b
coerce (forall (n :: Natural) i (m :: Natural).
ListR n i -> ListR m i -> ListR (n + m) i
listrAppend @_ @i)

ixrZip :: IxR n i -> IxR n j -> IxR n (i, j)
ixrZip :: forall (n :: Natural) i j. IxR n i -> IxR n j -> IxR n (i, j)
ixrZip (IxR ListR n i
l1) (IxR ListR n j
l2) = ListR n (i, j) -> IxR n (i, j)
forall (n :: Natural) i. ListR n i -> IxR n i
IxR (ListR n (i, j) -> IxR n (i, j)) -> ListR n (i, j) -> IxR n (i, j)
forall a b. (a -> b) -> a -> b
$ ListR n i -> ListR n j -> ListR n (i, j)
forall (n :: Natural) i j. ListR n i -> ListR n j -> ListR n (i, j)
listrZip ListR n i
l1 ListR n j
l2

ixrZipWith :: (i -> j -> k) -> IxR n i -> IxR n j -> IxR n k
ixrZipWith :: forall i j k (n :: Natural).
(i -> j -> k) -> IxR n i -> IxR n j -> IxR n k
ixrZipWith i -> j -> k
f (IxR ListR n i
l1) (IxR ListR n j
l2) = ListR n k -> IxR n k
forall (n :: Natural) i. ListR n i -> IxR n i
IxR (ListR n k -> IxR n k) -> ListR n k -> IxR n k
forall a b. (a -> b) -> a -> b
$ (i -> j -> k) -> ListR n i -> ListR n j -> ListR n k
forall i j k (n :: Natural).
(i -> j -> k) -> ListR n i -> ListR n j -> ListR n k
listrZipWith i -> j -> k
f ListR n i
l1 ListR n j
l2

ixrPermutePrefix :: forall n i. [Int] -> IxR n i -> IxR n i
ixrPermutePrefix :: forall (n :: Natural) i. [Int] -> IxR n i -> IxR n i
ixrPermutePrefix = ([Int] -> ListR n i -> ListR n i) -> [Int] -> IxR n i -> IxR n i
forall a b. Coercible a b => a -> b
coerce (forall i (n :: Natural). [Int] -> ListR n i -> ListR n i
listrPermutePrefix @i)


-- * Ranked shapes

type role ShR nominal representational
type ShR :: Nat -> Type -> Type
newtype ShR n i = ShR (ListR n i)
  deriving (ShR n i -> ShR n i -> Bool
(ShR n i -> ShR n i -> Bool)
-> (ShR n i -> ShR n i -> Bool) -> Eq (ShR n i)
forall (n :: Natural) i. Eq i => ShR n i -> ShR n i -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (n :: Natural) i. Eq i => ShR n i -> ShR n i -> Bool
== :: ShR n i -> ShR n i -> Bool
$c/= :: forall (n :: Natural) i. Eq i => ShR n i -> ShR n i -> Bool
/= :: ShR n i -> ShR n i -> Bool
Eq, Eq (ShR n i)
Eq (ShR n i) =>
(ShR n i -> ShR n i -> Ordering)
-> (ShR n i -> ShR n i -> Bool)
-> (ShR n i -> ShR n i -> Bool)
-> (ShR n i -> ShR n i -> Bool)
-> (ShR n i -> ShR n i -> Bool)
-> (ShR n i -> ShR n i -> ShR n i)
-> (ShR n i -> ShR n i -> ShR n i)
-> Ord (ShR n i)
ShR n i -> ShR n i -> Bool
ShR n i -> ShR n i -> Ordering
ShR n i -> ShR n i -> ShR n i
forall (n :: Natural) i. Ord i => Eq (ShR n i)
forall (n :: Natural) i. Ord i => ShR n i -> ShR n i -> Bool
forall (n :: Natural) i. Ord i => ShR n i -> ShR n i -> Ordering
forall (n :: Natural) i. Ord i => ShR n i -> ShR n i -> ShR n 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 (n :: Natural) i. Ord i => ShR n i -> ShR n i -> Ordering
compare :: ShR n i -> ShR n i -> Ordering
$c< :: forall (n :: Natural) i. Ord i => ShR n i -> ShR n i -> Bool
< :: ShR n i -> ShR n i -> Bool
$c<= :: forall (n :: Natural) i. Ord i => ShR n i -> ShR n i -> Bool
<= :: ShR n i -> ShR n i -> Bool
$c> :: forall (n :: Natural) i. Ord i => ShR n i -> ShR n i -> Bool
> :: ShR n i -> ShR n i -> Bool
$c>= :: forall (n :: Natural) i. Ord i => ShR n i -> ShR n i -> Bool
>= :: ShR n i -> ShR n i -> Bool
$cmax :: forall (n :: Natural) i. Ord i => ShR n i -> ShR n i -> ShR n i
max :: ShR n i -> ShR n i -> ShR n i
$cmin :: forall (n :: Natural) i. Ord i => ShR n i -> ShR n i -> ShR n i
min :: ShR n i -> ShR n i -> ShR n i
Ord, (forall x. ShR n i -> Rep (ShR n i) x)
-> (forall x. Rep (ShR n i) x -> ShR n i) -> Generic (ShR n i)
forall (n :: Natural) i x. Rep (ShR n i) x -> ShR n i
forall (n :: Natural) i x. ShR n i -> Rep (ShR n i) x
forall x. Rep (ShR n i) x -> ShR n i
forall x. ShR n i -> Rep (ShR n i) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (n :: Natural) i x. ShR n i -> Rep (ShR n i) x
from :: forall x. ShR n i -> Rep (ShR n i) x
$cto :: forall (n :: Natural) i x. Rep (ShR n i) x -> ShR n i
to :: forall x. Rep (ShR n i) x -> ShR n i
Generic)
  deriving newtype ((forall a b. (a -> b) -> ShR n a -> ShR n b)
-> (forall a b. a -> ShR n b -> ShR n a) -> Functor (ShR n)
forall (n :: Natural) a b. a -> ShR n b -> ShR n a
forall (n :: Natural) a b. (a -> b) -> ShR n a -> ShR n b
forall a b. a -> ShR n b -> ShR n a
forall a b. (a -> b) -> ShR n a -> ShR n b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (n :: Natural) a b. (a -> b) -> ShR n a -> ShR n b
fmap :: forall a b. (a -> b) -> ShR n a -> ShR n b
$c<$ :: forall (n :: Natural) a b. a -> ShR n b -> ShR n a
<$ :: forall a b. a -> ShR n b -> ShR n a
Functor, (forall m. Monoid m => ShR n m -> m)
-> (forall m a. Monoid m => (a -> m) -> ShR n a -> m)
-> (forall m a. Monoid m => (a -> m) -> ShR n a -> m)
-> (forall a b. (a -> b -> b) -> b -> ShR n a -> b)
-> (forall a b. (a -> b -> b) -> b -> ShR n a -> b)
-> (forall b a. (b -> a -> b) -> b -> ShR n a -> b)
-> (forall b a. (b -> a -> b) -> b -> ShR n a -> b)
-> (forall a. (a -> a -> a) -> ShR n a -> a)
-> (forall a. (a -> a -> a) -> ShR n a -> a)
-> (forall a. ShR n a -> [a])
-> (forall a. ShR n a -> Bool)
-> (forall a. ShR n a -> Int)
-> (forall a. Eq a => a -> ShR n a -> Bool)
-> (forall a. Ord a => ShR n a -> a)
-> (forall a. Ord a => ShR n a -> a)
-> (forall a. Num a => ShR n a -> a)
-> (forall a. Num a => ShR n a -> a)
-> Foldable (ShR n)
forall (n :: Natural) a. Eq a => a -> ShR n a -> Bool
forall (n :: Natural) a. Num a => ShR n a -> a
forall (n :: Natural) a. Ord a => ShR n a -> a
forall (n :: Natural) m. Monoid m => ShR n m -> m
forall (n :: Natural) a. ShR n a -> Bool
forall (n :: Natural) a. ShR n a -> Int
forall (n :: Natural) a. ShR n a -> [a]
forall (n :: Natural) a. (a -> a -> a) -> ShR n a -> a
forall (n :: Natural) m a. Monoid m => (a -> m) -> ShR n a -> m
forall (n :: Natural) b a. (b -> a -> b) -> b -> ShR n a -> b
forall (n :: Natural) a b. (a -> b -> b) -> b -> ShR n a -> b
forall a. Eq a => a -> ShR n a -> Bool
forall a. Num a => ShR n a -> a
forall a. Ord a => ShR n a -> a
forall m. Monoid m => ShR n m -> m
forall a. ShR n a -> Bool
forall a. ShR n a -> Int
forall a. ShR n a -> [a]
forall a. (a -> a -> a) -> ShR n a -> a
forall m a. Monoid m => (a -> m) -> ShR n a -> m
forall b a. (b -> a -> b) -> b -> ShR n a -> b
forall a b. (a -> b -> b) -> b -> ShR n a -> b
forall (t :: Type -> Type).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall (n :: Natural) m. Monoid m => ShR n m -> m
fold :: forall m. Monoid m => ShR n m -> m
$cfoldMap :: forall (n :: Natural) m a. Monoid m => (a -> m) -> ShR n a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> ShR n a -> m
$cfoldMap' :: forall (n :: Natural) m a. Monoid m => (a -> m) -> ShR n a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> ShR n a -> m
$cfoldr :: forall (n :: Natural) a b. (a -> b -> b) -> b -> ShR n a -> b
foldr :: forall a b. (a -> b -> b) -> b -> ShR n a -> b
$cfoldr' :: forall (n :: Natural) a b. (a -> b -> b) -> b -> ShR n a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> ShR n a -> b
$cfoldl :: forall (n :: Natural) b a. (b -> a -> b) -> b -> ShR n a -> b
foldl :: forall b a. (b -> a -> b) -> b -> ShR n a -> b
$cfoldl' :: forall (n :: Natural) b a. (b -> a -> b) -> b -> ShR n a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> ShR n a -> b
$cfoldr1 :: forall (n :: Natural) a. (a -> a -> a) -> ShR n a -> a
foldr1 :: forall a. (a -> a -> a) -> ShR n a -> a
$cfoldl1 :: forall (n :: Natural) a. (a -> a -> a) -> ShR n a -> a
foldl1 :: forall a. (a -> a -> a) -> ShR n a -> a
$ctoList :: forall (n :: Natural) a. ShR n a -> [a]
toList :: forall a. ShR n a -> [a]
$cnull :: forall (n :: Natural) a. ShR n a -> Bool
null :: forall a. ShR n a -> Bool
$clength :: forall (n :: Natural) a. ShR n a -> Int
length :: forall a. ShR n a -> Int
$celem :: forall (n :: Natural) a. Eq a => a -> ShR n a -> Bool
elem :: forall a. Eq a => a -> ShR n a -> Bool
$cmaximum :: forall (n :: Natural) a. Ord a => ShR n a -> a
maximum :: forall a. Ord a => ShR n a -> a
$cminimum :: forall (n :: Natural) a. Ord a => ShR n a -> a
minimum :: forall a. Ord a => ShR n a -> a
$csum :: forall (n :: Natural) a. Num a => ShR n a -> a
sum :: forall a. Num a => ShR n a -> a
$cproduct :: forall (n :: Natural) a. Num a => ShR n a -> a
product :: forall a. Num a => ShR n a -> a
Foldable)

pattern ZSR :: forall n i. () => n ~ 0 => ShR n i
pattern $mZSR :: forall {r} {n :: Natural} {i}.
ShR n i -> ((n ~ 0) => r) -> ((# #) -> r) -> r
$bZSR :: forall (n :: Natural) i. (n ~ 0) => ShR n i
ZSR = ShR ZR

pattern (:$:)
  :: forall {n1} {i}.
     forall n. (n + 1 ~ n1)
  => i -> ShR n i -> ShR n1 i
pattern i $m:$: :: forall {r} {n1 :: Natural} {i}.
ShR n1 i
-> (forall {n :: Natural}. ((n + 1) ~ n1) => i -> ShR n i -> r)
-> ((# #) -> r)
-> r
$b:$: :: forall {n1 :: Natural} {i} (n :: Natural).
((n + 1) ~ n1) =>
i -> ShR n i -> ShR n1 i
:$: sh <- ShR (listrUncons -> Just (UnconsListRRes (ShR -> sh) i))
  where i
i :$: ShR ListR n i
sh = ListR n1 i -> ShR n1 i
forall (n :: Natural) i. ListR n i -> ShR n i
ShR (i
i i -> ListR n i -> ListR (n + 1) i
forall (n :: Natural) {i}. i -> ListR n i -> ListR (n + 1) i
::: ListR n i
sh)
infixr 3 :$:

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

type IShR n = ShR n Int

#ifdef OXAR_DEFAULT_SHOW_INSTANCES
deriving instance Show i => Show (ShR n i)
#else
instance Show i => Show (ShR n i) where
  showsPrec :: Int -> ShR n i -> ShowS
showsPrec Int
_ (ShR ListR n i
l) = (i -> ShowS) -> ListR n i -> ShowS
forall (n :: Natural) i. (i -> ShowS) -> ListR n i -> ShowS
listrShow i -> ShowS
forall a. Show a => a -> ShowS
shows ListR n i
l
#endif

instance NFData i => NFData (ShR sh i)

-- | This checks only whether the ranks are equal, not whether the actual
-- values are.
shrEqRank :: ShR n i -> ShR n' i -> Maybe (n :~: n')
shrEqRank :: forall (n :: Natural) i (n' :: Natural).
ShR n i -> ShR n' i -> Maybe (n :~: n')
shrEqRank (ShR ListR n i
sh) (ShR ListR n' i
sh') = ListR n i -> ListR n' i -> Maybe (n :~: n')
forall (n :: Natural) i (n' :: Natural).
ListR n i -> ListR n' i -> Maybe (n :~: n')
listrEqRank ListR n i
sh ListR n' i
sh'

-- | This compares the shapes for value equality.
shrEqual :: Eq i => ShR n i -> ShR n' i -> Maybe (n :~: n')
shrEqual :: forall i (n :: Natural) (n' :: Natural).
Eq i =>
ShR n i -> ShR n' i -> Maybe (n :~: n')
shrEqual (ShR ListR n i
sh) (ShR ListR n' i
sh') = ListR n i -> ListR n' i -> Maybe (n :~: n')
forall i (n :: Natural) (n' :: Natural).
Eq i =>
ListR n i -> ListR n' i -> Maybe (n :~: n')
listrEqual ListR n i
sh ListR n' i
sh'

shrLength :: ShR sh i -> Int
shrLength :: forall (n :: Natural) a. ShR n a -> Int
shrLength (ShR ListR sh i
l) = ListR sh i -> Int
forall (n :: Natural) a. ListR n a -> Int
listrLength ListR sh i
l

-- | This function can also be used to conjure up a 'KnownNat' dictionary;
-- pattern matching on the returned 'SNat' with the 'pattern SNat' pattern
-- synonym yields 'KnownNat' evidence.
shrRank :: ShR n i -> SNat n
shrRank :: forall (n :: Natural) i. ShR n i -> SNat n
shrRank (ShR ListR n i
sh) = ListR n i -> SNat n
forall (n :: Natural) i. ListR n i -> SNat n
listrRank ListR n i
sh

-- | The number of elements in an array described by this shape.
shrSize :: IShR n -> Int
shrSize :: forall (n :: Natural). IShR n -> Int
shrSize ShR n Int
ZSR = Int
1
shrSize (Int
n :$: ShR n Int
sh) = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
* ShR n Int -> Int
forall (n :: Natural). IShR n -> Int
shrSize ShR n Int
sh

shrHead :: ShR (n + 1) i -> i
shrHead :: forall (n :: Natural) i. ShR (n + 1) i -> i
shrHead (ShR ListR (n + 1) i
list) = ListR (n + 1) i -> i
forall (n :: Natural) i. ListR (n + 1) i -> i
listrHead ListR (n + 1) i
list

shrTail :: ShR (n + 1) i -> ShR n i
shrTail :: forall (n :: Natural) i. ShR (n + 1) i -> ShR n i
shrTail (ShR ListR (n + 1) i
list) = ListR n i -> ShR n i
forall (n :: Natural) i. ListR n i -> ShR n i
ShR (ListR (n + 1) i -> ListR n i
forall (n :: Natural) i. ListR (n + 1) i -> ListR n i
listrTail ListR (n + 1) i
list)

shrInit :: ShR (n + 1) i -> ShR n i
shrInit :: forall (n :: Natural) i. ShR (n + 1) i -> ShR n i
shrInit (ShR ListR (n + 1) i
list) = ListR n i -> ShR n i
forall (n :: Natural) i. ListR n i -> ShR n i
ShR (ListR (n + 1) i -> ListR n i
forall (n :: Natural) i. ListR (n + 1) i -> ListR n i
listrInit ListR (n + 1) i
list)

shrLast :: ShR (n + 1) i -> i
shrLast :: forall (n :: Natural) i. ShR (n + 1) i -> i
shrLast (ShR ListR (n + 1) i
list) = ListR (n + 1) i -> i
forall (n :: Natural) i. ListR (n + 1) i -> i
listrLast ListR (n + 1) i
list

-- | Performs a runtime check that the lengths are identical.
shrCast :: SNat n' -> ShR n i -> ShR n' i
shrCast :: forall (n' :: Natural) (n :: Natural) i.
SNat n' -> ShR n i -> ShR n' i
shrCast SNat n'
n (ShR ListR n i
sh) = ListR n' i -> ShR n' i
forall (n :: Natural) i. ListR n i -> ShR n i
ShR (String -> SNat n' -> ListR n i -> ListR n' i
forall (n' :: Natural) (n :: Natural) i.
String -> SNat n' -> ListR n i -> ListR n' i
listrCastWithName String
"shrCast" SNat n'
n ListR n i
sh)

shrAppend :: forall n m i. ShR n i -> ShR m i -> ShR (n + m) i
shrAppend :: forall (n :: Natural) (m :: Natural) i.
ShR n i -> ShR m i -> ShR (n + m) i
shrAppend = (ListR n i -> ListR m i -> ListR (n + m) i)
-> ShR n i -> ShR m i -> ShR (n + m) i
forall a b. Coercible a b => a -> b
coerce (forall (n :: Natural) i (m :: Natural).
ListR n i -> ListR m i -> ListR (n + m) i
listrAppend @_ @i)

shrZip :: ShR n i -> ShR n j -> ShR n (i, j)
shrZip :: forall (n :: Natural) i j. ShR n i -> ShR n j -> ShR n (i, j)
shrZip (ShR ListR n i
l1) (ShR ListR n j
l2) = ListR n (i, j) -> ShR n (i, j)
forall (n :: Natural) i. ListR n i -> ShR n i
ShR (ListR n (i, j) -> ShR n (i, j)) -> ListR n (i, j) -> ShR n (i, j)
forall a b. (a -> b) -> a -> b
$ ListR n i -> ListR n j -> ListR n (i, j)
forall (n :: Natural) i j. ListR n i -> ListR n j -> ListR n (i, j)
listrZip ListR n i
l1 ListR n j
l2

shrZipWith :: (i -> j -> k) -> ShR n i -> ShR n j -> ShR n k
shrZipWith :: forall i j k (n :: Natural).
(i -> j -> k) -> ShR n i -> ShR n j -> ShR n k
shrZipWith i -> j -> k
f (ShR ListR n i
l1) (ShR ListR n j
l2) = ListR n k -> ShR n k
forall (n :: Natural) i. ListR n i -> ShR n i
ShR (ListR n k -> ShR n k) -> ListR n k -> ShR n k
forall a b. (a -> b) -> a -> b
$ (i -> j -> k) -> ListR n i -> ListR n j -> ListR n k
forall i j k (n :: Natural).
(i -> j -> k) -> ListR n i -> ListR n j -> ListR n k
listrZipWith i -> j -> k
f ListR n i
l1 ListR n j
l2

shrPermutePrefix :: forall n i. [Int] -> ShR n i -> ShR n i
shrPermutePrefix :: forall (n :: Natural) i. [Int] -> ShR n i -> ShR n i
shrPermutePrefix = ([Int] -> ListR n i -> ListR n i) -> [Int] -> ShR n i -> ShR n i
forall a b. Coercible a b => a -> b
coerce (forall i (n :: Natural). [Int] -> ListR n i -> ListR n i
listrPermutePrefix @i)


-- | Untyped: length is checked at runtime.
instance KnownNat n => IsList (ListR n i) where
  type Item (ListR n i) = i
  fromList :: [Item (ListR n i)] -> ListR n i
fromList [Item (ListR n i)]
topl = SNat n -> [i] -> ListR n i
forall (n' :: Natural). SNat n' -> [i] -> ListR n' i
go (forall (n :: Natural). KnownNat n => SNat n
SNat @n) [i]
[Item (ListR n i)]
topl
    where
      go :: SNat n' -> [i] -> ListR n' i
      go :: forall (n' :: Natural). SNat n' -> [i] -> ListR n' i
go SNat n'
SZ [] = ListR n' i
ListR 0 i
forall i. ListR 0 i
ZR
      go (SS SNat n
n) (i
i : [i]
is) = i
i i -> ListR n i -> ListR (n + 1) i
forall (n :: Natural) {i}. i -> ListR n i -> ListR (n + 1) i
::: SNat n -> [i] -> ListR n i
forall (n' :: Natural). SNat n' -> [i] -> ListR n' i
go SNat n
n [i]
is
      go SNat n'
_ [i]
_ = String -> ListR n' i
forall a. HasCallStack => String -> a
error (String -> ListR n' i) -> String -> ListR n' i
forall a b. (a -> b) -> a -> b
$ String
"IsList(ListR): Mismatched list length (type says "
                         String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (SNat n -> Integer
forall (n :: Natural). SNat n -> Integer
fromSNat (forall (n :: Natural). KnownNat n => SNat n
SNat @n)) 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 (ListR n i)]
topl) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
  toList :: ListR n i -> [Item (ListR n i)]
toList = ListR n i -> [i]
ListR n i -> [Item (ListR n i)]
forall a. ListR n a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
Foldable.toList

-- | Untyped: length is checked at runtime.
instance KnownNat n => IsList (IxR n i) where
  type Item (IxR n i) = i
  fromList :: [Item (IxR n i)] -> IxR n i
fromList = ListR n i -> IxR n i
forall (n :: Natural) i. ListR n i -> IxR n i
IxR (ListR n i -> IxR n i) -> ([i] -> ListR n i) -> [i] -> IxR n i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [i] -> ListR n i
[Item (ListR n i)] -> ListR n i
forall l. IsList l => [Item l] -> l
IsList.fromList
  toList :: IxR n i -> [Item (IxR n i)]
toList = IxR n i -> [i]
IxR n i -> [Item (IxR n i)]
forall a. IxR n a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
Foldable.toList

-- | Untyped: length is checked at runtime.
instance KnownNat n => IsList (ShR n i) where
  type Item (ShR n i) = i
  fromList :: [Item (ShR n i)] -> ShR n i
fromList = ListR n i -> ShR n i
forall (n :: Natural) i. ListR n i -> ShR n i
ShR (ListR n i -> ShR n i) -> ([i] -> ListR n i) -> [i] -> ShR n i
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [i] -> ListR n i
[Item (ListR n i)] -> ListR n i
forall l. IsList l => [Item l] -> l
IsList.fromList
  toList :: ShR n i -> [Item (ShR n i)]
toList = ShR n i -> [i]
ShR n i -> [Item (ShR n i)]
forall a. ShR n a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
Foldable.toList


-- * Internal helper functions

listrCastWithName :: String -> SNat n' -> ListR n i -> ListR n' i
listrCastWithName :: forall (n' :: Natural) (n :: Natural) i.
String -> SNat n' -> ListR n i -> ListR n' i
listrCastWithName String
_ SNat n'
SZ ListR n i
ZR = ListR n' i
ListR 0 i
forall i. ListR 0 i
ZR
listrCastWithName String
name (SS SNat n
n) (i
i ::: ListR n i
idx) = i
i i -> ListR n i -> ListR (n + 1) i
forall (n :: Natural) {i}. i -> ListR n i -> ListR (n + 1) i
::: String -> SNat n -> ListR n i -> ListR n i
forall (n' :: Natural) (n :: Natural) i.
String -> SNat n' -> ListR n i -> ListR n' i
listrCastWithName String
name SNat n
n ListR n i
idx
listrCastWithName String
name SNat n'
_ ListR n i
_ = String -> ListR n' i
forall a. HasCallStack => String -> a
error (String -> ListR n' i) -> String -> ListR n' i
forall a b. (a -> b) -> a -> b
$ String
name String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": ranks don't match"