{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
module Data.Array.Nested.Ranked (
  Ranked(Ranked),
  rquotArray, rremArray, ratan2Array,
  rshape, rrank,
  module Data.Array.Nested.Ranked,
  liftRanked1, liftRanked2,
) where

import Prelude hiding (mappend, mconcat)

import Data.Array.RankedS qualified as S
import Data.Bifunctor (first)
import Data.Coerce (coerce)
import Data.List.NonEmpty (NonEmpty)
import Data.Proxy
import Data.Type.Equality
import Data.Vector.Storable qualified as VS
import Foreign.Storable (Storable)
import GHC.TypeLits
import GHC.TypeNats qualified as TN

import Data.Array.Nested.Convert
import Data.Array.Nested.Lemmas
import Data.Array.Nested.Mixed
import Data.Array.Nested.Mixed.Shape
import Data.Array.Nested.Permutation
import Data.Array.Nested.Ranked.Base
import Data.Array.Nested.Ranked.Shape
import Data.Array.Nested.Types
import Data.Array.Strided.Arith
import Data.Array.XArray (XArray(..))
import Data.Array.XArray qualified as X


remptyArray :: KnownElt a => Ranked 1 a
remptyArray :: forall a. KnownElt a => Ranked 1 a
remptyArray = Mixed '[ 'Just 0] a -> Ranked (Rank '[ 'Just 0]) a
forall (sh :: [Maybe Nat]) a.
Elt a =>
Mixed sh a -> Ranked (Rank sh) a
mtoRanked (IShX '[] -> Mixed '[ 'Just 0] a
forall a (sh :: [Maybe Nat]).
KnownElt a =>
IShX sh -> Mixed ('Just 0 : sh) a
memptyArray IShX '[]
forall (sh :: [Maybe Nat]) i. (sh ~ '[]) => ShX sh i
ZSX)

-- | The total number of elements in the array.
rsize :: Elt a => Ranked n a -> Int
rsize :: forall a (n :: Nat). Elt a => Ranked n a -> Int
rsize = IShR n -> Int
forall (n :: Nat). IShR n -> Int
shrSize (IShR n -> Int) -> (Ranked n a -> IShR n) -> Ranked n a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ranked n a -> IShR n
forall a (n :: Nat). Elt a => Ranked n a -> IShR n
rshape

rindex :: Elt a => Ranked n a -> IIxR n -> a
rindex :: forall a (n :: Nat). Elt a => Ranked n a -> IIxR n -> a
rindex (Ranked Mixed (Replicate n 'Nothing) a
arr) IIxR n
idx = Mixed (Replicate n 'Nothing) a -> IIxX (Replicate n 'Nothing) -> a
forall (sh :: [Maybe Nat]). Mixed sh a -> IIxX sh -> a
forall a (sh :: [Maybe Nat]). Elt a => Mixed sh a -> IIxX sh -> a
mindex Mixed (Replicate n 'Nothing) a
arr (IIxR n -> IIxX (Replicate n 'Nothing)
forall (n :: Nat) i. IxR n i -> IxX (Replicate n 'Nothing) i
ixxFromIxR IIxR n
idx)

rindexPartial :: forall n m a. Elt a => Ranked (n + m) a -> IIxR n -> Ranked m a
rindexPartial :: forall (n :: Nat) (m :: Nat) a.
Elt a =>
Ranked (n + m) a -> IIxR n -> Ranked m a
rindexPartial (Ranked Mixed (Replicate (n + m) 'Nothing) a
arr) IIxR n
idx =
  Mixed (Replicate m 'Nothing) a -> Ranked m a
forall (n :: Nat) a. Mixed (Replicate n 'Nothing) a -> Ranked n a
Ranked (forall a (sh :: [Maybe Nat]) (sh' :: [Maybe Nat]).
Elt a =>
Mixed (sh ++ sh') a -> IIxX sh -> Mixed sh' a
mindexPartial @a @(Replicate n Nothing) @(Replicate m Nothing)
            ((Mixed (Replicate (n + m) 'Nothing) a
 :~: Mixed (Replicate n 'Nothing ++ Replicate m 'Nothing) a)
-> Mixed (Replicate (n + m) 'Nothing) a
-> Mixed (Replicate n 'Nothing ++ Replicate m 'Nothing) a
forall a b. (a :~: b) -> a -> b
castWith ((Replicate (n + m) 'Nothing
 :~: (Replicate n 'Nothing ++ Replicate m 'Nothing))
-> Mixed (Replicate (n + m) 'Nothing) a
   :~: Mixed (Replicate n 'Nothing ++ Replicate m 'Nothing) a
forall {k1} {k2} {k3} (f :: k1 -> k2 -> k3) (c :: k2) (a :: k1)
       (b :: k1).
(a :~: b) -> f a c :~: f b c
subst2 (SNat n
-> Proxy m
-> Proxy 'Nothing
-> Replicate (n + m) 'Nothing
   :~: (Replicate n 'Nothing ++ Replicate m 'Nothing)
forall {a1} (n :: Nat) (m :: Nat) (a2 :: a1).
SNat n
-> Proxy m
-> Proxy a2
-> Replicate (n + m) a2 :~: (Replicate n a2 ++ Replicate m a2)
lemReplicatePlusApp (IIxR n -> SNat n
forall (n :: Nat) i. IxR n i -> SNat n
ixrRank IIxR n
idx) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @m) (forall (t :: Maybe Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @Nothing))) Mixed (Replicate (n + m) 'Nothing) a
arr)
            (IIxR n -> IxX (Replicate n 'Nothing) Int
forall (n :: Nat) i. IxR n i -> IxX (Replicate n 'Nothing) i
ixxFromIxR IIxR n
idx))

-- | __WARNING__: All values returned from the function must have equal shape.
-- See the documentation of 'mgenerate' for more details.
rgenerate :: forall n a. KnownElt a => IShR n -> (IIxR n -> a) -> Ranked n a
rgenerate :: forall (n :: Nat) a.
KnownElt a =>
IShR n -> (IIxR n -> a) -> Ranked n a
rgenerate IShR n
sh IIxR n -> a
f
  | sn :: SNat n
sn@SNat n
SNat <- IShR n -> SNat n
forall (n :: Nat) i. ShR n i -> SNat n
shrRank IShR n
sh
  , Dict KnownShX (Replicate n 'Nothing)
Dict <- SNat n -> Dict KnownShX (Replicate n 'Nothing)
forall (n :: Nat). SNat n -> Dict KnownShX (Replicate n 'Nothing)
lemKnownReplicate SNat n
sn
  , Rank (Replicate n 'Nothing) :~: n
Refl <- SNat n -> Rank (Replicate n 'Nothing) :~: n
forall (proxy :: Nat -> *) (n :: Nat).
proxy n -> Rank (Replicate n 'Nothing) :~: n
lemRankReplicate SNat n
sn
  = Mixed (Replicate n 'Nothing) a -> Ranked n a
forall (n :: Nat) a. Mixed (Replicate n 'Nothing) a -> Ranked n a
Ranked (IShX (Replicate n 'Nothing)
-> (IIxX (Replicate n 'Nothing) -> a)
-> Mixed (Replicate n 'Nothing) a
forall (sh :: [Maybe Nat]) a.
KnownElt a =>
IShX sh -> (IIxX sh -> a) -> Mixed sh a
mgenerate (IShR n -> IShX (Replicate n 'Nothing)
forall (n :: Nat) i. ShR n i -> ShX (Replicate n 'Nothing) i
shxFromShR IShR n
sh) (IIxR n -> a
f (IIxR n -> a)
-> (IIxX (Replicate n 'Nothing) -> IIxR n)
-> IIxX (Replicate n 'Nothing)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IIxX (Replicate n 'Nothing) -> IIxR n
IIxX (Replicate n 'Nothing)
-> IxR (Rank (Replicate n 'Nothing)) Int
forall (sh :: [Maybe Nat]) i. IxX sh i -> IxR (Rank sh) i
ixrFromIxX))

-- | See the documentation of 'mlift'.
rlift :: forall n1 n2 a. Elt a
      => SNat n2
      -> (forall sh' b. Storable b => StaticShX sh' -> XArray (Replicate n1 Nothing ++ sh') b -> XArray (Replicate n2 Nothing ++ sh') b)
      -> Ranked n1 a -> Ranked n2 a
rlift :: forall (n1 :: Nat) (n2 :: Nat) a.
Elt a =>
SNat n2
-> (forall (sh' :: [Maybe Nat]) b.
    Storable b =>
    StaticShX sh'
    -> XArray (Replicate n1 'Nothing ++ sh') b
    -> XArray (Replicate n2 'Nothing ++ sh') b)
-> Ranked n1 a
-> Ranked n2 a
rlift SNat n2
sn2 forall (sh' :: [Maybe Nat]) b.
Storable b =>
StaticShX sh'
-> XArray (Replicate n1 'Nothing ++ sh') b
-> XArray (Replicate n2 'Nothing ++ sh') b
f (Ranked Mixed (Replicate n1 'Nothing) a
arr) = Mixed (Replicate n2 'Nothing) a -> Ranked n2 a
forall (n :: Nat) a. Mixed (Replicate n 'Nothing) a -> Ranked n a
Ranked (StaticShX (Replicate n2 'Nothing)
-> (forall (sh' :: [Maybe Nat]) b.
    Storable b =>
    StaticShX sh'
    -> XArray (Replicate n1 'Nothing ++ sh') b
    -> XArray (Replicate n2 'Nothing ++ sh') b)
-> Mixed (Replicate n1 'Nothing) a
-> Mixed (Replicate n2 'Nothing) a
forall (sh1 :: [Maybe Nat]) (sh2 :: [Maybe Nat]).
StaticShX sh2
-> (forall (sh' :: [Maybe Nat]) b.
    Storable b =>
    StaticShX sh' -> XArray (sh1 ++ sh') b -> XArray (sh2 ++ sh') b)
-> Mixed sh1 a
-> Mixed sh2 a
forall a (sh1 :: [Maybe Nat]) (sh2 :: [Maybe Nat]).
Elt a =>
StaticShX sh2
-> (forall (sh' :: [Maybe Nat]) b.
    Storable b =>
    StaticShX sh' -> XArray (sh1 ++ sh') b -> XArray (sh2 ++ sh') b)
-> Mixed sh1 a
-> Mixed sh2 a
mlift (SNat n2 -> StaticShX (Replicate n2 'Nothing)
forall (n :: Nat). SNat n -> StaticShX (Replicate n 'Nothing)
ssxFromSNat SNat n2
sn2) StaticShX sh'
-> XArray (Replicate n1 'Nothing ++ sh') b
-> XArray (Replicate n2 'Nothing ++ sh') b
forall (sh' :: [Maybe Nat]) b.
Storable b =>
StaticShX sh'
-> XArray (Replicate n1 'Nothing ++ sh') b
-> XArray (Replicate n2 'Nothing ++ sh') b
f Mixed (Replicate n1 'Nothing) a
arr)

-- | See the documentation of 'mlift2'.
rlift2 :: forall n1 n2 n3 a. Elt a
       => SNat n3
       -> (forall sh' b. Storable b => StaticShX sh' -> XArray (Replicate n1 Nothing ++ sh') b -> XArray (Replicate n2 Nothing ++ sh') b -> XArray (Replicate n3 Nothing ++ sh') b)
       -> Ranked n1 a -> Ranked n2 a -> Ranked n3 a
rlift2 :: forall (n1 :: Nat) (n2 :: Nat) (n3 :: Nat) a.
Elt a =>
SNat n3
-> (forall (sh' :: [Maybe Nat]) b.
    Storable b =>
    StaticShX sh'
    -> XArray (Replicate n1 'Nothing ++ sh') b
    -> XArray (Replicate n2 'Nothing ++ sh') b
    -> XArray (Replicate n3 'Nothing ++ sh') b)
-> Ranked n1 a
-> Ranked n2 a
-> Ranked n3 a
rlift2 SNat n3
sn3 forall (sh' :: [Maybe Nat]) b.
Storable b =>
StaticShX sh'
-> XArray (Replicate n1 'Nothing ++ sh') b
-> XArray (Replicate n2 'Nothing ++ sh') b
-> XArray (Replicate n3 'Nothing ++ sh') b
f (Ranked Mixed (Replicate n1 'Nothing) a
arr1) (Ranked Mixed (Replicate n2 'Nothing) a
arr2) = Mixed (Replicate n3 'Nothing) a -> Ranked n3 a
forall (n :: Nat) a. Mixed (Replicate n 'Nothing) a -> Ranked n a
Ranked (StaticShX (Replicate n3 'Nothing)
-> (forall (sh' :: [Maybe Nat]) b.
    Storable b =>
    StaticShX sh'
    -> XArray (Replicate n1 'Nothing ++ sh') b
    -> XArray (Replicate n2 'Nothing ++ sh') b
    -> XArray (Replicate n3 'Nothing ++ sh') b)
-> Mixed (Replicate n1 'Nothing) a
-> Mixed (Replicate n2 'Nothing) a
-> Mixed (Replicate n3 'Nothing) a
forall (sh1 :: [Maybe Nat]) (sh2 :: [Maybe Nat])
       (sh3 :: [Maybe Nat]).
StaticShX sh3
-> (forall (sh' :: [Maybe Nat]) b.
    Storable b =>
    StaticShX sh'
    -> XArray (sh1 ++ sh') b
    -> XArray (sh2 ++ sh') b
    -> XArray (sh3 ++ sh') b)
-> Mixed sh1 a
-> Mixed sh2 a
-> Mixed sh3 a
forall a (sh1 :: [Maybe Nat]) (sh2 :: [Maybe Nat])
       (sh3 :: [Maybe Nat]).
Elt a =>
StaticShX sh3
-> (forall (sh' :: [Maybe Nat]) b.
    Storable b =>
    StaticShX sh'
    -> XArray (sh1 ++ sh') b
    -> XArray (sh2 ++ sh') b
    -> XArray (sh3 ++ sh') b)
-> Mixed sh1 a
-> Mixed sh2 a
-> Mixed sh3 a
mlift2 (SNat n3 -> StaticShX (Replicate n3 'Nothing)
forall (n :: Nat). SNat n -> StaticShX (Replicate n 'Nothing)
ssxFromSNat SNat n3
sn3) StaticShX sh'
-> XArray (Replicate n1 'Nothing ++ sh') b
-> XArray (Replicate n2 'Nothing ++ sh') b
-> XArray (Replicate n3 'Nothing ++ sh') b
forall (sh' :: [Maybe Nat]) b.
Storable b =>
StaticShX sh'
-> XArray (Replicate n1 'Nothing ++ sh') b
-> XArray (Replicate n2 'Nothing ++ sh') b
-> XArray (Replicate n3 'Nothing ++ sh') b
f Mixed (Replicate n1 'Nothing) a
arr1 Mixed (Replicate n2 'Nothing) a
arr2)

rsumOuter1P :: forall n a.
               (Storable a, NumElt a)
            => Ranked (n + 1) (Primitive a) -> Ranked n (Primitive a)
rsumOuter1P :: forall (n :: Nat) a.
(Storable a, NumElt a) =>
Ranked (n + 1) (Primitive a) -> Ranked n (Primitive a)
rsumOuter1P (Ranked Mixed (Replicate (n + 1) 'Nothing) (Primitive a)
arr)
  | ('Nothing : Replicate n 'Nothing) :~: Replicate (n + 1) 'Nothing
Refl <- forall (a2 :: Maybe Nat) (n :: Nat).
(a2 : Replicate n a2) :~: Replicate (n + 1) a2
forall {a1} (a2 :: a1) (n :: Nat).
(a2 : Replicate n a2) :~: Replicate (n + 1) a2
lemReplicateSucc @(Nothing @Nat) @n
  = Mixed (Replicate n 'Nothing) (Primitive a)
-> Ranked n (Primitive a)
forall (n :: Nat) a. Mixed (Replicate n 'Nothing) a -> Ranked n a
Ranked (Mixed ('Nothing : Replicate n 'Nothing) (Primitive a)
-> Mixed (Replicate n 'Nothing) (Primitive a)
forall (sh :: [Maybe Nat]) (n :: Maybe Nat) a.
(Storable a, NumElt a) =>
Mixed (n : sh) (Primitive a) -> Mixed sh (Primitive a)
msumOuter1P Mixed ('Nothing : Replicate n 'Nothing) (Primitive a)
Mixed (Replicate (n + 1) 'Nothing) (Primitive a)
arr)

rsumOuter1 :: forall n a. (NumElt a, PrimElt a)
           => Ranked (n + 1) a -> Ranked n a
rsumOuter1 :: forall (n :: Nat) a.
(NumElt a, PrimElt a) =>
Ranked (n + 1) a -> Ranked n a
rsumOuter1 = Ranked n (Primitive a) -> Ranked n a
forall a (n :: Nat).
PrimElt a =>
Ranked n (Primitive a) -> Ranked n a
rfromPrimitive (Ranked n (Primitive a) -> Ranked n a)
-> (Ranked (n + 1) a -> Ranked n (Primitive a))
-> Ranked (n + 1) a
-> Ranked n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ranked (n + 1) (Primitive a) -> Ranked n (Primitive a)
forall (n :: Nat) a.
(Storable a, NumElt a) =>
Ranked (n + 1) (Primitive a) -> Ranked n (Primitive a)
rsumOuter1P (Ranked (n + 1) (Primitive a) -> Ranked n (Primitive a))
-> (Ranked (n + 1) a -> Ranked (n + 1) (Primitive a))
-> Ranked (n + 1) a
-> Ranked n (Primitive a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ranked (n + 1) a -> Ranked (n + 1) (Primitive a)
forall a (n :: Nat).
PrimElt a =>
Ranked n a -> Ranked n (Primitive a)
rtoPrimitive

rsumAllPrim :: (PrimElt a, NumElt a) => Ranked n a -> a
rsumAllPrim :: forall a (n :: Nat). (PrimElt a, NumElt a) => Ranked n a -> a
rsumAllPrim (Ranked Mixed (Replicate n 'Nothing) a
arr) = Mixed (Replicate n 'Nothing) a -> a
forall a (sh :: [Maybe Nat]).
(PrimElt a, NumElt a) =>
Mixed sh a -> a
msumAllPrim Mixed (Replicate n 'Nothing) a
arr

rtranspose :: forall n a. Elt a => PermR -> Ranked n a -> Ranked n a
rtranspose :: forall (n :: Nat) a. Elt a => PermR -> Ranked n a -> Ranked n a
rtranspose PermR
perm Ranked n a
arr
  | sn :: SNat n
sn@SNat n
SNat <- Ranked n a -> SNat n
forall a (n :: Nat). Elt a => Ranked n a -> SNat n
rrank Ranked n a
arr
  , Dict KnownShX (Replicate n 'Nothing)
Dict <- SNat n -> Dict KnownShX (Replicate n 'Nothing)
forall (n :: Nat). SNat n -> Dict KnownShX (Replicate n 'Nothing)
lemKnownReplicate SNat n
sn
  , PermR -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length PermR
perm Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Proxy n -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
natVal (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n))
  = SNat n
-> (forall (sh' :: [Maybe Nat]) b.
    Storable b =>
    StaticShX sh'
    -> XArray (Replicate n 'Nothing ++ sh') b
    -> XArray (Replicate n 'Nothing ++ sh') b)
-> Ranked n a
-> Ranked n a
forall (n1 :: Nat) (n2 :: Nat) a.
Elt a =>
SNat n2
-> (forall (sh' :: [Maybe Nat]) b.
    Storable b =>
    StaticShX sh'
    -> XArray (Replicate n1 'Nothing ++ sh') b
    -> XArray (Replicate n2 'Nothing ++ sh') b)
-> Ranked n1 a
-> Ranked n2 a
rlift SNat n
sn
          (\StaticShX sh'
ssh' -> SNat n
-> StaticShX sh'
-> PermR
-> XArray (Replicate n 'Nothing ++ sh') b
-> XArray (Replicate n 'Nothing ++ sh') b
forall (n :: Nat) (sh :: [Maybe Nat]) a.
SNat n
-> StaticShX sh
-> PermR
-> XArray (Replicate n 'Nothing ++ sh) a
-> XArray (Replicate n 'Nothing ++ sh) a
X.transposeUntyped (forall (n :: Nat). KnownNat n => SNat n
natSing @n) StaticShX sh'
ssh' PermR
perm)
          Ranked n a
arr
  | Bool
otherwise
  = [Char] -> Ranked n a
forall a. HasCallStack => [Char] -> a
error [Char]
"Data.Array.Nested.rtranspose: Permutation longer than rank of array"

rconcat :: forall n a. Elt a => NonEmpty (Ranked (n + 1) a) -> Ranked (n + 1) a
rconcat :: forall (n :: Nat) a.
Elt a =>
NonEmpty (Ranked (n + 1) a) -> Ranked (n + 1) a
rconcat
  | ('Nothing : Replicate n 'Nothing) :~: Replicate (n + 1) 'Nothing
Refl <- forall (a2 :: Maybe Nat) (n :: Nat).
(a2 : Replicate n a2) :~: Replicate (n + 1) a2
forall {a1} (a2 :: a1) (n :: Nat).
(a2 : Replicate n a2) :~: Replicate (n + 1) a2
lemReplicateSucc @(Nothing @Nat) @n
  = (NonEmpty (Mixed ('Nothing : Replicate n 'Nothing) a)
 -> Mixed ('Nothing : Replicate n 'Nothing) a)
-> NonEmpty (Ranked (n + 1) a) -> Ranked (n + 1) a
forall a b. Coercible a b => a -> b
coerce NonEmpty (Mixed ('Nothing : Replicate n 'Nothing) a)
-> Mixed ('Nothing : Replicate n 'Nothing) a
forall (sh :: [Maybe Nat]).
NonEmpty (Mixed ('Nothing : sh) a) -> Mixed ('Nothing : sh) a
forall a (sh :: [Maybe Nat]).
Elt a =>
NonEmpty (Mixed ('Nothing : sh) a) -> Mixed ('Nothing : sh) a
mconcat

rappend :: forall n a. Elt a
        => Ranked (n + 1) a -> Ranked (n + 1) a -> Ranked (n + 1) a
rappend :: forall (n :: Nat) a.
Elt a =>
Ranked (n + 1) a -> Ranked (n + 1) a -> Ranked (n + 1) a
rappend Ranked (n + 1) a
arr1 Ranked (n + 1) a
arr2
  | sn :: SNat (n + 1)
sn@SNat (n + 1)
SNat <- Ranked (n + 1) a -> SNat (n + 1)
forall a (n :: Nat). Elt a => Ranked n a -> SNat n
rrank Ranked (n + 1) a
arr1
  , Dict KnownShX (Replicate (n + 1) 'Nothing)
Dict <- SNat (n + 1) -> Dict KnownShX (Replicate (n + 1) 'Nothing)
forall (n :: Nat). SNat n -> Dict KnownShX (Replicate n 'Nothing)
lemKnownReplicate SNat (n + 1)
sn
  , ('Nothing : Replicate n 'Nothing) :~: Replicate (n + 1) 'Nothing
Refl <- forall (a2 :: Maybe Nat) (n :: Nat).
(a2 : Replicate n a2) :~: Replicate (n + 1) a2
forall {a1} (a2 :: a1) (n :: Nat).
(a2 : Replicate n a2) :~: Replicate (n + 1) a2
lemReplicateSucc @(Nothing @Nat) @n
  = (Mixed ('Nothing : Replicate n 'Nothing) a
 -> Mixed ('Nothing : Replicate n 'Nothing) a
 -> Mixed ('Nothing : Replicate n 'Nothing) a)
-> Ranked (n + 1) a -> Ranked (n + 1) a -> Ranked (n + 1) a
forall a b. Coercible a b => a -> b
coerce (forall (n :: Maybe Nat) (m :: Maybe Nat) (sh :: [Maybe Nat]) a.
Elt a =>
Mixed (n : sh) a -> Mixed (m : sh) a -> Mixed (AddMaybe n m : sh) a
mappend @Nothing @Nothing @(Replicate n Nothing))
      Ranked (n + 1) a
arr1 Ranked (n + 1) a
arr2

rscalar :: Elt a => a -> Ranked 0 a
rscalar :: forall a. Elt a => a -> Ranked 0 a
rscalar a
x = Mixed (Replicate 0 'Nothing) a -> Ranked 0 a
forall (n :: Nat) a. Mixed (Replicate n 'Nothing) a -> Ranked n a
Ranked (a -> Mixed '[] a
forall a. Elt a => a -> Mixed '[] a
mscalar a
x)

rfromVectorP :: forall n a. Storable a => IShR n -> VS.Vector a -> Ranked n (Primitive a)
rfromVectorP :: forall (n :: Nat) a.
Storable a =>
IShR n -> Vector a -> Ranked n (Primitive a)
rfromVectorP IShR n
sh Vector a
v
  | Dict KnownShX (Replicate n 'Nothing)
Dict <- SNat n -> Dict KnownShX (Replicate n 'Nothing)
forall (n :: Nat). SNat n -> Dict KnownShX (Replicate n 'Nothing)
lemKnownReplicate (IShR n -> SNat n
forall (n :: Nat) i. ShR n i -> SNat n
shrRank IShR n
sh)
  = Mixed (Replicate n 'Nothing) (Primitive a)
-> Ranked n (Primitive a)
forall (n :: Nat) a. Mixed (Replicate n 'Nothing) a -> Ranked n a
Ranked (IShX (Replicate n 'Nothing)
-> Vector a -> Mixed (Replicate n 'Nothing) (Primitive a)
forall (sh :: [Maybe Nat]) a.
Storable a =>
IShX sh -> Vector a -> Mixed sh (Primitive a)
mfromVectorP (IShR n -> IShX (Replicate n 'Nothing)
forall (n :: Nat) i. ShR n i -> ShX (Replicate n 'Nothing) i
shxFromShR IShR n
sh) Vector a
v)

rfromVector :: forall n a. PrimElt a => IShR n -> VS.Vector a -> Ranked n a
rfromVector :: forall (n :: Nat) a. PrimElt a => IShR n -> Vector a -> Ranked n a
rfromVector IShR n
sh Vector a
v = Ranked n (Primitive a) -> Ranked n a
forall a (n :: Nat).
PrimElt a =>
Ranked n (Primitive a) -> Ranked n a
rfromPrimitive (IShR n -> Vector a -> Ranked n (Primitive a)
forall (n :: Nat) a.
Storable a =>
IShR n -> Vector a -> Ranked n (Primitive a)
rfromVectorP IShR n
sh Vector a
v)

rtoVectorP :: Storable a => Ranked n (Primitive a) -> VS.Vector a
rtoVectorP :: forall a (n :: Nat).
Storable a =>
Ranked n (Primitive a) -> Vector a
rtoVectorP = (Mixed (Replicate n 'Nothing) (Primitive a) -> Vector a)
-> Ranked n (Primitive a) -> Vector a
forall a b. Coercible a b => a -> b
coerce Mixed (Replicate n 'Nothing) (Primitive a) -> Vector a
forall a (sh :: [Maybe Nat]).
Storable a =>
Mixed sh (Primitive a) -> Vector a
mtoVectorP

rtoVector :: PrimElt a => Ranked n a -> VS.Vector a
rtoVector :: forall a (n :: Nat). PrimElt a => Ranked n a -> Vector a
rtoVector = (Mixed (Replicate n 'Nothing) a -> Vector a)
-> Ranked n a -> Vector a
forall a b. Coercible a b => a -> b
coerce Mixed (Replicate n 'Nothing) a -> Vector a
forall a (sh :: [Maybe Nat]). PrimElt a => Mixed sh a -> Vector a
mtoVector

rfromList1 :: Elt a => NonEmpty a -> Ranked 1 a
rfromList1 :: forall a. Elt a => NonEmpty a -> Ranked 1 a
rfromList1 NonEmpty a
l = Mixed (Replicate 1 'Nothing) a -> Ranked 1 a
forall (n :: Nat) a. Mixed (Replicate n 'Nothing) a -> Ranked n a
Ranked (NonEmpty a -> Mixed '[ 'Nothing] a
forall a. Elt a => NonEmpty a -> Mixed '[ 'Nothing] a
mfromList1 NonEmpty a
l)

rfromListOuter :: forall n a. Elt a => NonEmpty (Ranked n a) -> Ranked (n + 1) a
rfromListOuter :: forall (n :: Nat) a.
Elt a =>
NonEmpty (Ranked n a) -> Ranked (n + 1) a
rfromListOuter NonEmpty (Ranked n a)
l
  | ('Nothing : Replicate n 'Nothing) :~: Replicate (n + 1) 'Nothing
Refl <- forall (a2 :: Maybe Nat) (n :: Nat).
(a2 : Replicate n a2) :~: Replicate (n + 1) a2
forall {a1} (a2 :: a1) (n :: Nat).
(a2 : Replicate n a2) :~: Replicate (n + 1) a2
lemReplicateSucc @(Nothing @Nat) @n
  = Mixed (Replicate (n + 1) 'Nothing) a -> Ranked (n + 1) a
forall (n :: Nat) a. Mixed (Replicate n 'Nothing) a -> Ranked n a
Ranked (NonEmpty (Mixed (Replicate n 'Nothing) a)
-> Mixed ('Nothing : Replicate n 'Nothing) a
forall (sh :: [Maybe Nat]).
NonEmpty (Mixed sh a) -> Mixed ('Nothing : sh) a
forall a (sh :: [Maybe Nat]).
Elt a =>
NonEmpty (Mixed sh a) -> Mixed ('Nothing : sh) a
mfromListOuter (NonEmpty (Ranked n a) -> NonEmpty (Mixed (Replicate n 'Nothing) a)
forall a b. Coercible a b => a -> b
coerce NonEmpty (Ranked n a)
l :: NonEmpty (Mixed (Replicate n Nothing) a)))

rfromListLinear :: forall n a. Elt a => IShR n -> NonEmpty a -> Ranked n a
rfromListLinear :: forall (n :: Nat) a. Elt a => IShR n -> NonEmpty a -> Ranked n a
rfromListLinear IShR n
sh NonEmpty a
l = IShR n -> Ranked 1 a -> Ranked n a
forall (n :: Nat) (n' :: Nat) a.
Elt a =>
IShR n' -> Ranked n a -> Ranked n' a
rreshape IShR n
sh (NonEmpty a -> Ranked 1 a
forall a. Elt a => NonEmpty a -> Ranked 1 a
rfromList1 NonEmpty a
l)

rfromListPrim :: PrimElt a => [a] -> Ranked 1 a
rfromListPrim :: forall a. PrimElt a => [a] -> Ranked 1 a
rfromListPrim [a]
l = Mixed (Replicate 1 'Nothing) a -> Ranked 1 a
forall (n :: Nat) a. Mixed (Replicate n 'Nothing) a -> Ranked n a
Ranked ([a] -> Mixed '[ 'Nothing] a
forall a. PrimElt a => [a] -> Mixed '[ 'Nothing] a
mfromListPrim [a]
l)

rfromListPrimLinear :: PrimElt a => IShR n -> [a] -> Ranked n a
rfromListPrimLinear :: forall a (n :: Nat). PrimElt a => IShR n -> [a] -> Ranked n a
rfromListPrimLinear IShR n
sh [a]
l =
  let M_Primitive IShX '[ 'Nothing]
_ XArray '[ 'Nothing] a
xarr = Mixed '[ 'Nothing] a -> Mixed '[ 'Nothing] (Primitive a)
forall (sh :: [Maybe Nat]). Mixed sh a -> Mixed sh (Primitive a)
forall a (sh :: [Maybe Nat]).
PrimElt a =>
Mixed sh a -> Mixed sh (Primitive a)
toPrimitive ([a] -> Mixed '[ 'Nothing] a
forall a. PrimElt a => [a] -> Mixed '[ 'Nothing] a
mfromListPrim [a]
l)
  in Mixed (Replicate n 'Nothing) a -> Ranked n a
forall (n :: Nat) a. Mixed (Replicate n 'Nothing) a -> Ranked n a
Ranked (Mixed (Replicate n 'Nothing) a -> Ranked n a)
-> Mixed (Replicate n 'Nothing) a -> Ranked n a
forall a b. (a -> b) -> a -> b
$ Mixed (Replicate n 'Nothing) (Primitive a)
-> Mixed (Replicate n 'Nothing) a
forall (sh :: [Maybe Nat]). Mixed sh (Primitive a) -> Mixed sh a
forall a (sh :: [Maybe Nat]).
PrimElt a =>
Mixed sh (Primitive a) -> Mixed sh a
fromPrimitive (Mixed (Replicate n 'Nothing) (Primitive a)
 -> Mixed (Replicate n 'Nothing) a)
-> Mixed (Replicate n 'Nothing) (Primitive a)
-> Mixed (Replicate n 'Nothing) a
forall a b. (a -> b) -> a -> b
$ IShX (Replicate n 'Nothing)
-> XArray (Replicate n 'Nothing) a
-> Mixed (Replicate n 'Nothing) (Primitive a)
forall (sh :: [Maybe Nat]) a.
IShX sh -> XArray sh a -> Mixed sh (Primitive a)
M_Primitive (IShR n -> IShX (Replicate n 'Nothing)
forall (n :: Nat) i. ShR n i -> ShX (Replicate n 'Nothing) i
shxFromShR IShR n
sh) (StaticShX '[ 'Nothing]
-> IShX (Replicate n 'Nothing)
-> XArray '[ 'Nothing] a
-> XArray (Replicate n 'Nothing) a
forall (sh1 :: [Maybe Nat]) (sh2 :: [Maybe Nat]) a.
Storable a =>
StaticShX sh1 -> IShX sh2 -> XArray sh1 a -> XArray sh2 a
X.reshape (() -> SMayNat () SNat 'Nothing
forall {k} i (f :: k -> *). i -> SMayNat i f 'Nothing
SUnknown () SMayNat () SNat 'Nothing -> StaticShX '[] -> StaticShX '[ 'Nothing]
forall {sh1 :: [Maybe Nat]} (n :: Maybe Nat) (sh :: [Maybe Nat]).
((n : sh) ~ sh1) =>
SMayNat () SNat n -> StaticShX sh -> StaticShX sh1
:!% StaticShX '[]
forall (sh :: [Maybe Nat]). (sh ~ '[]) => StaticShX sh
ZKX) (IShR n -> IShX (Replicate n 'Nothing)
forall (n :: Nat) i. ShR n i -> ShX (Replicate n 'Nothing) i
shxFromShR IShR n
sh) XArray '[ 'Nothing] a
xarr)

rtoList :: Elt a => Ranked 1 a -> [a]
rtoList :: forall a. Elt a => Ranked 1 a -> [a]
rtoList = (Ranked 0 a -> a) -> [Ranked 0 a] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map Ranked 0 a -> a
forall a. Elt a => Ranked 0 a -> a
runScalar ([Ranked 0 a] -> [a])
-> (Ranked 1 a -> [Ranked 0 a]) -> Ranked 1 a -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ranked 1 a -> [Ranked 0 a]
Ranked (0 + 1) a -> [Ranked 0 a]
forall (n :: Nat) a. Elt a => Ranked (n + 1) a -> [Ranked n a]
rtoListOuter

rtoListOuter :: forall n a. Elt a => Ranked (n + 1) a -> [Ranked n a]
rtoListOuter :: forall (n :: Nat) a. Elt a => Ranked (n + 1) a -> [Ranked n a]
rtoListOuter (Ranked Mixed (Replicate (n + 1) 'Nothing) a
arr)
  | ('Nothing : Replicate n 'Nothing) :~: Replicate (n + 1) 'Nothing
Refl <- forall (a2 :: Maybe Nat) (n :: Nat).
(a2 : Replicate n a2) :~: Replicate (n + 1) a2
forall {a1} (a2 :: a1) (n :: Nat).
(a2 : Replicate n a2) :~: Replicate (n + 1) a2
lemReplicateSucc @(Nothing @Nat) @n
  = [Mixed (Replicate n 'Nothing) a] -> [Ranked n a]
forall a b. Coercible a b => a -> b
coerce (forall a (n :: Maybe Nat) (sh :: [Maybe Nat]).
Elt a =>
Mixed (n : sh) a -> [Mixed sh a]
mtoListOuter @a @Nothing @(Replicate n Nothing) Mixed ('Nothing : Replicate n 'Nothing) a
Mixed (Replicate (n + 1) 'Nothing) a
arr)

rtoListLinear :: Elt a => Ranked n a -> [a]
rtoListLinear :: forall a (n :: Nat). Elt a => Ranked n a -> [a]
rtoListLinear (Ranked Mixed (Replicate n 'Nothing) a
arr) = Mixed (Replicate n 'Nothing) a -> [a]
forall a (sh :: [Maybe Nat]). Elt a => Mixed sh a -> [a]
mtoListLinear Mixed (Replicate n 'Nothing) a
arr

rfromOrthotope :: PrimElt a => SNat n -> S.Array n a -> Ranked n a
rfromOrthotope :: forall a (n :: Nat). PrimElt a => SNat n -> Array n a -> Ranked n a
rfromOrthotope SNat n
sn Array n a
arr
  | Rank (Replicate n 'Nothing) :~: n
Refl <- SNat n -> Rank (Replicate n 'Nothing) :~: n
forall (proxy :: Nat -> *) (n :: Nat).
proxy n -> Rank (Replicate n 'Nothing) :~: n
lemRankReplicate SNat n
sn
  = let xarr :: XArray (Replicate n 'Nothing) a
xarr = Array (Rank (Replicate n 'Nothing)) a
-> XArray (Replicate n 'Nothing) a
forall (sh :: [Maybe Nat]) a. Array (Rank sh) a -> XArray sh a
XArray Array n a
Array (Rank (Replicate n 'Nothing)) a
arr
    in Mixed (Replicate n 'Nothing) a -> Ranked n a
forall (n :: Nat) a. Mixed (Replicate n 'Nothing) a -> Ranked n a
Ranked (Mixed (Replicate n 'Nothing) (Primitive a)
-> Mixed (Replicate n 'Nothing) a
forall (sh :: [Maybe Nat]). Mixed sh (Primitive a) -> Mixed sh a
forall a (sh :: [Maybe Nat]).
PrimElt a =>
Mixed sh (Primitive a) -> Mixed sh a
fromPrimitive (IShX (Replicate n 'Nothing)
-> XArray (Replicate n 'Nothing) a
-> Mixed (Replicate n 'Nothing) (Primitive a)
forall (sh :: [Maybe Nat]) a.
IShX sh -> XArray sh a -> Mixed sh (Primitive a)
M_Primitive (StaticShX (Replicate n 'Nothing)
-> XArray (Replicate n 'Nothing) a -> IShX (Replicate n 'Nothing)
forall (sh :: [Maybe Nat]) a.
StaticShX sh -> XArray sh a -> IShX sh
X.shape (SNat n -> StaticShX (Replicate n 'Nothing)
forall (n :: Nat). SNat n -> StaticShX (Replicate n 'Nothing)
ssxFromSNat SNat n
sn) XArray (Replicate n 'Nothing) a
xarr) XArray (Replicate n 'Nothing) a
xarr))

rtoOrthotope :: PrimElt a => Ranked n a -> S.Array n a
rtoOrthotope :: forall a (n :: Nat). PrimElt a => Ranked n a -> Array n a
rtoOrthotope (Ranked n a -> Ranked n (Primitive a)
forall a (n :: Nat).
PrimElt a =>
Ranked n a -> Ranked n (Primitive a)
rtoPrimitive -> Ranked (M_Primitive IShX (Replicate n 'Nothing)
sh (XArray Array (Rank (Replicate n 'Nothing)) a
arr)))
  | Rank (Replicate n 'Nothing) :~: n
Refl <- SNat n -> Rank (Replicate n 'Nothing) :~: n
forall (proxy :: Nat -> *) (n :: Nat).
proxy n -> Rank (Replicate n 'Nothing) :~: n
lemRankReplicate (ShR n Int -> SNat n
forall (n :: Nat) i. ShR n i -> SNat n
shrRank (ShR n Int -> SNat n) -> ShR n Int -> SNat n
forall a b. (a -> b) -> a -> b
$ IShX (Replicate n 'Nothing) -> ShR n Int
forall (n :: Nat). IShX (Replicate n 'Nothing) -> IShR n
shrFromShX2 IShX (Replicate n 'Nothing)
sh)
  = Array n a
Array (Rank (Replicate n 'Nothing)) a
arr

runScalar :: Elt a => Ranked 0 a -> a
runScalar :: forall a. Elt a => Ranked 0 a -> a
runScalar Ranked 0 a
arr = Ranked 0 a -> IIxR 0 -> a
forall a (n :: Nat). Elt a => Ranked n a -> IIxR n -> a
rindex Ranked 0 a
arr IIxR 0
forall (n :: Nat) i. (n ~ 0) => IxR n i
ZIR

rnest :: forall n m a. Elt a => SNat n -> Ranked (n + m) a -> Ranked n (Ranked m a)
rnest :: forall (n :: Nat) (m :: Nat) a.
Elt a =>
SNat n -> Ranked (n + m) a -> Ranked n (Ranked m a)
rnest SNat n
n Ranked (n + m) a
arr
  | Replicate (n + m) 'Nothing
:~: (Replicate n 'Nothing ++ Replicate m 'Nothing)
Refl <- SNat n
-> Proxy m
-> Proxy 'Nothing
-> Replicate (n + m) 'Nothing
   :~: (Replicate n 'Nothing ++ Replicate m 'Nothing)
forall {a1} (n :: Nat) (m :: Nat) (a2 :: a1).
SNat n
-> Proxy m
-> Proxy a2
-> Replicate (n + m) a2 :~: (Replicate n a2 ++ Replicate m a2)
lemReplicatePlusApp SNat n
n (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @m) (forall (t :: Maybe Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Nothing @Nat))
  = Mixed (Replicate n 'Nothing) (Mixed (Replicate m 'Nothing) a)
-> Ranked n (Ranked m a)
forall a b. Coercible a b => a -> b
coerce (StaticShX (Replicate n 'Nothing)
-> Mixed (Replicate n 'Nothing ++ Replicate m 'Nothing) a
-> Mixed (Replicate n 'Nothing) (Mixed (Replicate m 'Nothing) a)
forall (sh :: [Maybe Nat]) (sh' :: [Maybe Nat]) a.
Elt a =>
StaticShX sh -> Mixed (sh ++ sh') a -> Mixed sh (Mixed sh' a)
mnest (SNat n -> StaticShX (Replicate n 'Nothing)
forall (n :: Nat). SNat n -> StaticShX (Replicate n 'Nothing)
ssxFromSNat SNat n
n) (Ranked (n + m) a -> Mixed (Replicate (n + m) 'Nothing) a
forall a b. Coercible a b => a -> b
coerce Ranked (n + m) a
arr))

runNest :: forall n m a. Elt a => Ranked n (Ranked m a) -> Ranked (n + m) a
runNest :: forall (n :: Nat) (m :: Nat) a.
Elt a =>
Ranked n (Ranked m a) -> Ranked (n + m) a
runNest rarr :: Ranked n (Ranked m a)
rarr@(Ranked (M_Ranked (M_Nest IShX (Replicate n 'Nothing)
_ Mixed (Replicate n 'Nothing ++ Replicate m 'Nothing) a
arr)))
  | Replicate (n + m) 'Nothing
:~: (Replicate n 'Nothing ++ Replicate m 'Nothing)
Refl <- SNat n
-> Proxy m
-> Proxy 'Nothing
-> Replicate (n + m) 'Nothing
   :~: (Replicate n 'Nothing ++ Replicate m 'Nothing)
forall {a1} (n :: Nat) (m :: Nat) (a2 :: a1).
SNat n
-> Proxy m
-> Proxy a2
-> Replicate (n + m) a2 :~: (Replicate n a2 ++ Replicate m a2)
lemReplicatePlusApp (Ranked n (Ranked m a) -> SNat n
forall a (n :: Nat). Elt a => Ranked n a -> SNat n
rrank Ranked n (Ranked m a)
rarr) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @m) (forall (t :: Maybe Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Nothing @Nat))
  = Mixed (Replicate (n + m) 'Nothing) a -> Ranked (n + m) a
forall (n :: Nat) a. Mixed (Replicate n 'Nothing) a -> Ranked n a
Ranked Mixed (Replicate (n + m) 'Nothing) a
Mixed (Replicate n 'Nothing ++ Replicate m 'Nothing) a
arr

rzip :: (Elt a, Elt b) => Ranked n a -> Ranked n b -> Ranked n (a, b)
rzip :: forall a b (n :: Nat).
(Elt a, Elt b) =>
Ranked n a -> Ranked n b -> Ranked n (a, b)
rzip = (Mixed (Replicate n 'Nothing) a
 -> Mixed (Replicate n 'Nothing) b
 -> Mixed (Replicate n 'Nothing) (a, b))
-> Ranked n a -> Ranked n b -> Ranked n (a, b)
forall a b. Coercible a b => a -> b
coerce Mixed (Replicate n 'Nothing) a
-> Mixed (Replicate n 'Nothing) b
-> Mixed (Replicate n 'Nothing) (a, b)
forall a b (sh :: [Maybe Nat]).
(Elt a, Elt b) =>
Mixed sh a -> Mixed sh b -> Mixed sh (a, b)
mzip

runzip :: Ranked n (a, b) -> (Ranked n a, Ranked n b)
runzip :: forall (n :: Nat) a b. Ranked n (a, b) -> (Ranked n a, Ranked n b)
runzip = (Mixed (Replicate n 'Nothing) (a, b)
 -> (Mixed (Replicate n 'Nothing) a,
     Mixed (Replicate n 'Nothing) b))
-> Ranked n (a, b) -> (Ranked n a, Ranked n b)
forall a b. Coercible a b => a -> b
coerce Mixed (Replicate n 'Nothing) (a, b)
-> (Mixed (Replicate n 'Nothing) a, Mixed (Replicate n 'Nothing) b)
forall (sh :: [Maybe Nat]) a b.
Mixed sh (a, b) -> (Mixed sh a, Mixed sh b)
munzip

rrerankP :: forall n1 n2 n a b. (Storable a, Storable b)
         => SNat n -> IShR n2
         -> (Ranked n1 (Primitive a) -> Ranked n2 (Primitive b))
         -> Ranked (n + n1) (Primitive a) -> Ranked (n + n2) (Primitive b)
rrerankP :: forall (n1 :: Nat) (n2 :: Nat) (n :: Nat) a b.
(Storable a, Storable b) =>
SNat n
-> IShR n2
-> (Ranked n1 (Primitive a) -> Ranked n2 (Primitive b))
-> Ranked (n + n1) (Primitive a)
-> Ranked (n + n2) (Primitive b)
rrerankP SNat n
sn IShR n2
sh2 Ranked n1 (Primitive a) -> Ranked n2 (Primitive b)
f (Ranked Mixed (Replicate (n + n1) 'Nothing) (Primitive a)
arr)
  | Replicate (n + n1) 'Nothing
:~: (Replicate n 'Nothing ++ Replicate n1 'Nothing)
Refl <- SNat n
-> Proxy n1
-> Proxy 'Nothing
-> Replicate (n + n1) 'Nothing
   :~: (Replicate n 'Nothing ++ Replicate n1 'Nothing)
forall {a1} (n :: Nat) (m :: Nat) (a2 :: a1).
SNat n
-> Proxy m
-> Proxy a2
-> Replicate (n + m) a2 :~: (Replicate n a2 ++ Replicate m a2)
lemReplicatePlusApp SNat n
sn (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n1) (forall (t :: Maybe Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Nothing @Nat))
  , Replicate (n + n2) 'Nothing
:~: (Replicate n 'Nothing ++ Replicate n2 'Nothing)
Refl <- SNat n
-> Proxy n2
-> Proxy 'Nothing
-> Replicate (n + n2) 'Nothing
   :~: (Replicate n 'Nothing ++ Replicate n2 'Nothing)
forall {a1} (n :: Nat) (m :: Nat) (a2 :: a1).
SNat n
-> Proxy m
-> Proxy a2
-> Replicate (n + m) a2 :~: (Replicate n a2 ++ Replicate m a2)
lemReplicatePlusApp SNat n
sn (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @n2) (forall (t :: Maybe Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Nothing @Nat))
  = Mixed (Replicate (n + n2) 'Nothing) (Primitive b)
-> Ranked (n + n2) (Primitive b)
forall (n :: Nat) a. Mixed (Replicate n 'Nothing) a -> Ranked n a
Ranked (StaticShX (Replicate n 'Nothing)
-> IShX (Replicate n2 'Nothing)
-> (Mixed (Replicate n1 'Nothing) (Primitive a)
    -> Mixed (Replicate n2 'Nothing) (Primitive b))
-> Mixed
     (Replicate n 'Nothing ++ Replicate n1 'Nothing) (Primitive a)
-> Mixed
     (Replicate n 'Nothing ++ Replicate n2 'Nothing) (Primitive b)
forall (sh1 :: [Maybe Nat]) (sh2 :: [Maybe Nat])
       (sh :: [Maybe Nat]) a b.
(Storable a, Storable b) =>
StaticShX sh
-> IShX sh2
-> (Mixed sh1 (Primitive a) -> Mixed sh2 (Primitive b))
-> Mixed (sh ++ sh1) (Primitive a)
-> Mixed (sh ++ sh2) (Primitive b)
mrerankP (SNat n -> StaticShX (Replicate n 'Nothing)
forall (n :: Nat). SNat n -> StaticShX (Replicate n 'Nothing)
ssxFromSNat SNat n
sn) (IShR n2 -> IShX (Replicate n2 'Nothing)
forall (n :: Nat) i. ShR n i -> ShX (Replicate n 'Nothing) i
shxFromShR IShR n2
sh2)
                     (\Mixed (Replicate n1 'Nothing) (Primitive a)
a -> let Ranked Mixed (Replicate n2 'Nothing) (Primitive b)
r = Ranked n1 (Primitive a) -> Ranked n2 (Primitive b)
f (Mixed (Replicate n1 'Nothing) (Primitive a)
-> Ranked n1 (Primitive a)
forall (n :: Nat) a. Mixed (Replicate n 'Nothing) a -> Ranked n a
Ranked Mixed (Replicate n1 'Nothing) (Primitive a)
a) in Mixed (Replicate n2 'Nothing) (Primitive b)
r)
                     Mixed (Replicate (n + n1) 'Nothing) (Primitive a)
Mixed (Replicate n 'Nothing ++ Replicate n1 'Nothing) (Primitive a)
arr)

-- | If there is a zero-sized dimension in the @n@-prefix of the shape of the
-- input array, then there is no way to deduce the full shape of the output
-- array (more precisely, the @n2@ part): that could only come from calling
-- @f@, and there are no subarrays to call @f@ on. @orthotope@ errors out in
-- this case; we choose to fill the @n2@ part of the output shape with zeros.
--
-- For example, if:
--
-- @
-- arr :: Ranked 5 Int   -- of shape [3, 0, 4, 2, 21]
-- f :: Ranked 2 Int -> Ranked 3 Float
-- @
--
-- then:
--
-- @
-- rrerank _ _ _ f arr :: Ranked 5 Float
-- @
--
-- and this result will have shape @[3, 0, 4, 0, 0, 0]@. Note that the
-- "reranked" part (the last 3 entries) are zero; we don't know if @f@ intended
-- to return an array with shape all-0 here (it probably didn't), but there is
-- no better number to put here absent a subarray of the input to pass to @f@.
rrerank :: forall n1 n2 n a b. (PrimElt a, PrimElt b)
        => SNat n -> IShR n2
        -> (Ranked n1 a -> Ranked n2 b)
        -> Ranked (n + n1) a -> Ranked (n + n2) b
rrerank :: forall (n1 :: Nat) (n2 :: Nat) (n :: Nat) a b.
(PrimElt a, PrimElt b) =>
SNat n
-> IShR n2
-> (Ranked n1 a -> Ranked n2 b)
-> Ranked (n + n1) a
-> Ranked (n + n2) b
rrerank SNat n
sn IShR n2
sh2 Ranked n1 a -> Ranked n2 b
f (Ranked (n + n1) a -> Ranked (n + n1) (Primitive a)
forall a (n :: Nat).
PrimElt a =>
Ranked n a -> Ranked n (Primitive a)
rtoPrimitive -> Ranked (n + n1) (Primitive a)
arr) =
  Ranked (n + n2) (Primitive b) -> Ranked (n + n2) b
forall a (n :: Nat).
PrimElt a =>
Ranked n (Primitive a) -> Ranked n a
rfromPrimitive (Ranked (n + n2) (Primitive b) -> Ranked (n + n2) b)
-> Ranked (n + n2) (Primitive b) -> Ranked (n + n2) b
forall a b. (a -> b) -> a -> b
$ SNat n
-> IShR n2
-> (Ranked n1 (Primitive a) -> Ranked n2 (Primitive b))
-> Ranked (n + n1) (Primitive a)
-> Ranked (n + n2) (Primitive b)
forall (n1 :: Nat) (n2 :: Nat) (n :: Nat) a b.
(Storable a, Storable b) =>
SNat n
-> IShR n2
-> (Ranked n1 (Primitive a) -> Ranked n2 (Primitive b))
-> Ranked (n + n1) (Primitive a)
-> Ranked (n + n2) (Primitive b)
rrerankP SNat n
sn IShR n2
sh2 (Ranked n2 b -> Ranked n2 (Primitive b)
forall a (n :: Nat).
PrimElt a =>
Ranked n a -> Ranked n (Primitive a)
rtoPrimitive (Ranked n2 b -> Ranked n2 (Primitive b))
-> (Ranked n1 (Primitive a) -> Ranked n2 b)
-> Ranked n1 (Primitive a)
-> Ranked n2 (Primitive b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ranked n1 a -> Ranked n2 b
f (Ranked n1 a -> Ranked n2 b)
-> (Ranked n1 (Primitive a) -> Ranked n1 a)
-> Ranked n1 (Primitive a)
-> Ranked n2 b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ranked n1 (Primitive a) -> Ranked n1 a
forall a (n :: Nat).
PrimElt a =>
Ranked n (Primitive a) -> Ranked n a
rfromPrimitive) Ranked (n + n1) (Primitive a)
arr

rreplicate :: forall n m a. Elt a
           => IShR n -> Ranked m a -> Ranked (n + m) a
rreplicate :: forall (n :: Nat) (m :: Nat) a.
Elt a =>
IShR n -> Ranked m a -> Ranked (n + m) a
rreplicate IShR n
sh (Ranked Mixed (Replicate m 'Nothing) a
arr)
  | Replicate (n + m) 'Nothing
:~: (Replicate n 'Nothing ++ Replicate m 'Nothing)
Refl <- SNat n
-> Proxy m
-> Proxy 'Nothing
-> Replicate (n + m) 'Nothing
   :~: (Replicate n 'Nothing ++ Replicate m 'Nothing)
forall {a1} (n :: Nat) (m :: Nat) (a2 :: a1).
SNat n
-> Proxy m
-> Proxy a2
-> Replicate (n + m) a2 :~: (Replicate n a2 ++ Replicate m a2)
lemReplicatePlusApp (IShR n -> SNat n
forall (n :: Nat) i. ShR n i -> SNat n
shrRank IShR n
sh) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @m) (forall (t :: Maybe Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Nothing @Nat))
  = Mixed (Replicate (n + m) 'Nothing) a -> Ranked (n + m) a
forall (n :: Nat) a. Mixed (Replicate n 'Nothing) a -> Ranked n a
Ranked (IShX (Replicate n 'Nothing)
-> Mixed (Replicate m 'Nothing) a
-> Mixed (Replicate n 'Nothing ++ Replicate m 'Nothing) a
forall (sh :: [Maybe Nat]) (sh' :: [Maybe Nat]) a.
Elt a =>
IShX sh -> Mixed sh' a -> Mixed (sh ++ sh') a
mreplicate (IShR n -> IShX (Replicate n 'Nothing)
forall (n :: Nat) i. ShR n i -> ShX (Replicate n 'Nothing) i
shxFromShR IShR n
sh) Mixed (Replicate m 'Nothing) a
arr)

rreplicateScalP :: forall n a. Storable a => IShR n -> a -> Ranked n (Primitive a)
rreplicateScalP :: forall (n :: Nat) a.
Storable a =>
IShR n -> a -> Ranked n (Primitive a)
rreplicateScalP IShR n
sh a
x
  | Dict KnownShX (Replicate n 'Nothing)
Dict <- SNat n -> Dict KnownShX (Replicate n 'Nothing)
forall (n :: Nat). SNat n -> Dict KnownShX (Replicate n 'Nothing)
lemKnownReplicate (IShR n -> SNat n
forall (n :: Nat) i. ShR n i -> SNat n
shrRank IShR n
sh)
  = Mixed (Replicate n 'Nothing) (Primitive a)
-> Ranked n (Primitive a)
forall (n :: Nat) a. Mixed (Replicate n 'Nothing) a -> Ranked n a
Ranked (IShX (Replicate n 'Nothing)
-> a -> Mixed (Replicate n 'Nothing) (Primitive a)
forall (sh :: [Maybe Nat]) a.
Storable a =>
IShX sh -> a -> Mixed sh (Primitive a)
mreplicateScalP (IShR n -> IShX (Replicate n 'Nothing)
forall (n :: Nat) i. ShR n i -> ShX (Replicate n 'Nothing) i
shxFromShR IShR n
sh) a
x)

rreplicateScal :: forall n a. PrimElt a
               => IShR n -> a -> Ranked n a
rreplicateScal :: forall (n :: Nat) a. PrimElt a => IShR n -> a -> Ranked n a
rreplicateScal IShR n
sh a
x = Ranked n (Primitive a) -> Ranked n a
forall a (n :: Nat).
PrimElt a =>
Ranked n (Primitive a) -> Ranked n a
rfromPrimitive (IShR n -> a -> Ranked n (Primitive a)
forall (n :: Nat) a.
Storable a =>
IShR n -> a -> Ranked n (Primitive a)
rreplicateScalP IShR n
sh a
x)

rslice :: forall n a. Elt a => Int -> Int -> Ranked (n + 1) a -> Ranked (n + 1) a
rslice :: forall (n :: Nat) a.
Elt a =>
Int -> Int -> Ranked (n + 1) a -> Ranked (n + 1) a
rslice Int
i Int
n Ranked (n + 1) a
arr
  | ('Nothing : Replicate n 'Nothing) :~: Replicate (n + 1) 'Nothing
Refl <- forall (a2 :: Maybe Nat) (n :: Nat).
(a2 : Replicate n a2) :~: Replicate (n + 1) a2
forall {a1} (a2 :: a1) (n :: Nat).
(a2 : Replicate n a2) :~: Replicate (n + 1) a2
lemReplicateSucc @(Nothing @Nat) @n
  = SNat (n + 1)
-> (forall (sh' :: [Maybe Nat]) b.
    Storable b =>
    StaticShX sh'
    -> XArray (Replicate (n + 1) 'Nothing ++ sh') b
    -> XArray (Replicate (n + 1) 'Nothing ++ sh') b)
-> Ranked (n + 1) a
-> Ranked (n + 1) a
forall (n1 :: Nat) (n2 :: Nat) a.
Elt a =>
SNat n2
-> (forall (sh' :: [Maybe Nat]) b.
    Storable b =>
    StaticShX sh'
    -> XArray (Replicate n1 'Nothing ++ sh') b
    -> XArray (Replicate n2 'Nothing ++ sh') b)
-> Ranked n1 a
-> Ranked n2 a
rlift (Ranked (n + 1) a -> SNat (n + 1)
forall a (n :: Nat). Elt a => Ranked n a -> SNat n
rrank Ranked (n + 1) a
arr)
          (\StaticShX sh'
_ -> Int
-> Int
-> XArray ('Nothing : (Replicate n 'Nothing ++ sh')) b
-> XArray ('Nothing : (Replicate n 'Nothing ++ sh')) b
forall (sh :: [Maybe Nat]) a.
Int -> Int -> XArray ('Nothing : sh) a -> XArray ('Nothing : sh) a
X.sliceU Int
i Int
n)
          Ranked (n + 1) a
arr

rrev1 :: forall n a. Elt a => Ranked (n + 1) a -> Ranked (n + 1) a
rrev1 :: forall (n :: Nat) a. Elt a => Ranked (n + 1) a -> Ranked (n + 1) a
rrev1 Ranked (n + 1) a
arr =
  SNat (n + 1)
-> (forall (sh' :: [Maybe Nat]) b.
    Storable b =>
    StaticShX sh'
    -> XArray (Replicate (n + 1) 'Nothing ++ sh') b
    -> XArray (Replicate (n + 1) 'Nothing ++ sh') b)
-> Ranked (n + 1) a
-> Ranked (n + 1) a
forall (n1 :: Nat) (n2 :: Nat) a.
Elt a =>
SNat n2
-> (forall (sh' :: [Maybe Nat]) b.
    Storable b =>
    StaticShX sh'
    -> XArray (Replicate n1 'Nothing ++ sh') b
    -> XArray (Replicate n2 'Nothing ++ sh') b)
-> Ranked n1 a
-> Ranked n2 a
rlift (Ranked (n + 1) a -> SNat (n + 1)
forall a (n :: Nat). Elt a => Ranked n a -> SNat n
rrank Ranked (n + 1) a
arr)
        (\(StaticShX sh'
_ :: StaticShX sh') ->
          case forall (a2 :: Maybe Nat) (n :: Nat).
(a2 : Replicate n a2) :~: Replicate (n + 1) a2
forall {a1} (a2 :: a1) (n :: Nat).
(a2 : Replicate n a2) :~: Replicate (n + 1) a2
lemReplicateSucc @(Nothing @Nat) @n of
            ('Nothing : Replicate n 'Nothing) :~: Replicate (n + 1) 'Nothing
Refl -> forall (n :: Maybe Nat) (sh :: [Maybe Nat]) a.
XArray (n : sh) a -> XArray (n : sh) a
X.rev1 @Nothing @(Replicate n Nothing ++ sh'))
        Ranked (n + 1) a
arr

rreshape :: forall n n' a. Elt a
         => IShR n' -> Ranked n a -> Ranked n' a
rreshape :: forall (n :: Nat) (n' :: Nat) a.
Elt a =>
IShR n' -> Ranked n a -> Ranked n' a
rreshape IShR n'
sh' rarr :: Ranked n a
rarr@(Ranked Mixed (Replicate n 'Nothing) a
arr)
  | Dict KnownShX (Replicate n 'Nothing)
Dict <- SNat n -> Dict KnownShX (Replicate n 'Nothing)
forall (n :: Nat). SNat n -> Dict KnownShX (Replicate n 'Nothing)
lemKnownReplicate (Ranked n a -> SNat n
forall a (n :: Nat). Elt a => Ranked n a -> SNat n
rrank Ranked n a
rarr)
  , Dict KnownShX (Replicate n' 'Nothing)
Dict <- SNat n' -> Dict KnownShX (Replicate n' 'Nothing)
forall (n :: Nat). SNat n -> Dict KnownShX (Replicate n 'Nothing)
lemKnownReplicate (IShR n' -> SNat n'
forall (n :: Nat) i. ShR n i -> SNat n
shrRank IShR n'
sh')
  = Mixed (Replicate n' 'Nothing) a -> Ranked n' a
forall (n :: Nat) a. Mixed (Replicate n 'Nothing) a -> Ranked n a
Ranked (IShX (Replicate n' 'Nothing)
-> Mixed (Replicate n 'Nothing) a
-> Mixed (Replicate n' 'Nothing) a
forall (sh :: [Maybe Nat]) (sh' :: [Maybe Nat]) a.
Elt a =>
IShX sh' -> Mixed sh a -> Mixed sh' a
mreshape (IShR n' -> IShX (Replicate n' 'Nothing)
forall (n :: Nat) i. ShR n i -> ShX (Replicate n 'Nothing) i
shxFromShR IShR n'
sh') Mixed (Replicate n 'Nothing) a
arr)

rflatten :: Elt a => Ranked n a -> Ranked 1 a
rflatten :: forall a (n :: Nat). Elt a => Ranked n a -> Ranked 1 a
rflatten (Ranked Mixed (Replicate n 'Nothing) a
arr) = Mixed '[Flatten' 1 (Replicate n 'Nothing)] a
-> Ranked (Rank '[Flatten' 1 (Replicate n 'Nothing)]) a
forall (sh :: [Maybe Nat]) a.
Elt a =>
Mixed sh a -> Ranked (Rank sh) a
mtoRanked (Mixed (Replicate n 'Nothing) a
-> Mixed '[Flatten' 1 (Replicate n 'Nothing)] a
forall a (sh :: [Maybe Nat]).
Elt a =>
Mixed sh a -> Mixed '[Flatten sh] a
mflatten Mixed (Replicate n 'Nothing) a
arr)

riota :: (Enum a, PrimElt a) => Int -> Ranked 1 a
riota :: forall a. (Enum a, PrimElt a) => Int -> Ranked 1 a
riota Int
n = Nat -> (forall {n :: Nat}. SNat n -> Ranked 1 a) -> Ranked 1 a
forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
TN.withSomeSNat (Int -> Nat
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n) ((forall {n :: Nat}. SNat n -> Ranked 1 a) -> Ranked 1 a)
-> (forall {n :: Nat}. SNat n -> Ranked 1 a) -> Ranked 1 a
forall a b. (a -> b) -> a -> b
$ Mixed '[ 'Just n] a -> Ranked 1 a
Mixed '[ 'Just n] a -> Ranked (Rank '[ 'Just n]) a
forall (sh :: [Maybe Nat]) a.
Elt a =>
Mixed sh a -> Ranked (Rank sh) a
mtoRanked (Mixed '[ 'Just n] a -> Ranked 1 a)
-> (SNat n -> Mixed '[ 'Just n] a) -> SNat n -> Ranked 1 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SNat n -> Mixed '[ 'Just n] a
forall a (n :: Nat).
(Enum a, PrimElt a) =>
SNat n -> Mixed '[ 'Just n] a
miota

-- | Throws if the array is empty.
rminIndexPrim :: (PrimElt a, NumElt a) => Ranked n a -> IIxR n
rminIndexPrim :: forall a (n :: Nat). (PrimElt a, NumElt a) => Ranked n a -> IIxR n
rminIndexPrim rarr :: Ranked n a
rarr@(Ranked Mixed (Replicate n 'Nothing) a
arr)
  | Rank (Replicate n 'Nothing) :~: n
Refl <- SNat n -> Rank (Replicate n 'Nothing) :~: n
forall (proxy :: Nat -> *) (n :: Nat).
proxy n -> Rank (Replicate n 'Nothing) :~: n
lemRankReplicate (Ranked n (Primitive a) -> SNat n
forall a (n :: Nat). Elt a => Ranked n a -> SNat n
rrank (Ranked n a -> Ranked n (Primitive a)
forall a (n :: Nat).
PrimElt a =>
Ranked n a -> Ranked n (Primitive a)
rtoPrimitive Ranked n a
rarr))
  = IxX (Replicate n 'Nothing) Int
-> IxR (Rank (Replicate n 'Nothing)) Int
forall (sh :: [Maybe Nat]) i. IxX sh i -> IxR (Rank sh) i
ixrFromIxX (Mixed (Replicate n 'Nothing) a -> IxX (Replicate n 'Nothing) Int
forall a (sh :: [Maybe Nat]).
(PrimElt a, NumElt a) =>
Mixed sh a -> IIxX sh
mminIndexPrim Mixed (Replicate n 'Nothing) a
arr)

-- | Throws if the array is empty.
rmaxIndexPrim :: (PrimElt a, NumElt a) => Ranked n a -> IIxR n
rmaxIndexPrim :: forall a (n :: Nat). (PrimElt a, NumElt a) => Ranked n a -> IIxR n
rmaxIndexPrim rarr :: Ranked n a
rarr@(Ranked Mixed (Replicate n 'Nothing) a
arr)
  | Rank (Replicate n 'Nothing) :~: n
Refl <- SNat n -> Rank (Replicate n 'Nothing) :~: n
forall (proxy :: Nat -> *) (n :: Nat).
proxy n -> Rank (Replicate n 'Nothing) :~: n
lemRankReplicate (Ranked n (Primitive a) -> SNat n
forall a (n :: Nat). Elt a => Ranked n a -> SNat n
rrank (Ranked n a -> Ranked n (Primitive a)
forall a (n :: Nat).
PrimElt a =>
Ranked n a -> Ranked n (Primitive a)
rtoPrimitive Ranked n a
rarr))
  = IxX (Replicate n 'Nothing) Int
-> IxR (Rank (Replicate n 'Nothing)) Int
forall (sh :: [Maybe Nat]) i. IxX sh i -> IxR (Rank sh) i
ixrFromIxX (Mixed (Replicate n 'Nothing) a -> IxX (Replicate n 'Nothing) Int
forall a (sh :: [Maybe Nat]).
(PrimElt a, NumElt a) =>
Mixed sh a -> IIxX sh
mmaxIndexPrim Mixed (Replicate n 'Nothing) a
arr)

rdot1Inner :: forall n a. (PrimElt a, NumElt a) => Ranked (n + 1) a -> Ranked (n + 1) a -> Ranked n a
rdot1Inner :: forall (n :: Nat) a.
(PrimElt a, NumElt a) =>
Ranked (n + 1) a -> Ranked (n + 1) a -> Ranked n a
rdot1Inner Ranked (n + 1) a
arr1 Ranked (n + 1) a
arr2
  | SNat (n + 1)
SNat <- Ranked (n + 1) a -> SNat (n + 1)
forall a (n :: Nat). Elt a => Ranked n a -> SNat n
rrank Ranked (n + 1) a
arr1
  , Replicate (n + 1) 'Nothing
:~: (Replicate n 'Nothing ++ Replicate 1 'Nothing)
Refl <- SNat n
-> Proxy 1
-> Proxy 'Nothing
-> Replicate (n + 1) 'Nothing
   :~: (Replicate n 'Nothing ++ Replicate 1 'Nothing)
forall {a1} (n :: Nat) (m :: Nat) (a2 :: a1).
SNat n
-> Proxy m
-> Proxy a2
-> Replicate (n + m) a2 :~: (Replicate n a2 ++ Replicate m a2)
lemReplicatePlusApp (forall (n :: Nat). KnownNat n => SNat n
SNat @n) (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @1) (forall (t :: Maybe Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Nothing @Nat))
  = (Mixed (Replicate n 'Nothing ++ '[ 'Nothing]) a
 -> Mixed (Replicate n 'Nothing ++ '[ 'Nothing]) a
 -> Mixed (Replicate n 'Nothing) a)
-> Ranked (n + 1) a -> Ranked (n + 1) a -> Ranked n a
forall a b. Coercible a b => a -> b
coerce (Proxy 'Nothing
-> Mixed (Replicate n 'Nothing ++ '[ 'Nothing]) a
-> Mixed (Replicate n 'Nothing ++ '[ 'Nothing]) a
-> Mixed (Replicate n 'Nothing) a
forall (sh :: [Maybe Nat]) (n :: Maybe Nat) a.
(PrimElt a, NumElt a) =>
Proxy n
-> Mixed (sh ++ '[n]) a -> Mixed (sh ++ '[n]) a -> Mixed sh a
mdot1Inner (forall (t :: Maybe Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Nothing @Nat))) Ranked (n + 1) a
arr1 Ranked (n + 1) a
arr2

-- | This has a temporary, suboptimal implementation in terms of 'mflatten'.
-- Prefer 'rdot1Inner' if applicable.
rdot :: (PrimElt a, NumElt a) => Ranked n a -> Ranked n a -> a
rdot :: forall a (n :: Nat).
(PrimElt a, NumElt a) =>
Ranked n a -> Ranked n a -> a
rdot = (Mixed (Replicate n 'Nothing) a
 -> Mixed (Replicate n 'Nothing) a -> a)
-> Ranked n a -> Ranked n a -> a
forall a b. Coercible a b => a -> b
coerce Mixed (Replicate n 'Nothing) a
-> Mixed (Replicate n 'Nothing) a -> a
forall a (sh :: [Maybe Nat]).
(PrimElt a, NumElt a) =>
Mixed sh a -> Mixed sh a -> a
mdot

rtoXArrayPrimP :: Ranked n (Primitive a) -> (IShR n, XArray (Replicate n Nothing) a)
rtoXArrayPrimP :: forall (n :: Nat) a.
Ranked n (Primitive a) -> (IShR n, XArray (Replicate n 'Nothing) a)
rtoXArrayPrimP (Ranked Mixed (Replicate n 'Nothing) (Primitive a)
arr) = (IShX (Replicate n 'Nothing) -> IShR n)
-> (IShX (Replicate n 'Nothing), XArray (Replicate n 'Nothing) a)
-> (IShR n, XArray (Replicate n 'Nothing) a)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first IShX (Replicate n 'Nothing) -> IShR n
forall (n :: Nat). IShX (Replicate n 'Nothing) -> IShR n
shrFromShX2 (Mixed (Replicate n 'Nothing) (Primitive a)
-> (IShX (Replicate n 'Nothing), XArray (Replicate n 'Nothing) a)
forall (sh :: [Maybe Nat]) a.
Mixed sh (Primitive a) -> (IShX sh, XArray sh a)
mtoXArrayPrimP Mixed (Replicate n 'Nothing) (Primitive a)
arr)

rtoXArrayPrim :: PrimElt a => Ranked n a -> (IShR n, XArray (Replicate n Nothing) a)
rtoXArrayPrim :: forall a (n :: Nat).
PrimElt a =>
Ranked n a -> (IShR n, XArray (Replicate n 'Nothing) a)
rtoXArrayPrim (Ranked Mixed (Replicate n 'Nothing) a
arr) = (IShX (Replicate n 'Nothing) -> IShR n)
-> (IShX (Replicate n 'Nothing), XArray (Replicate n 'Nothing) a)
-> (IShR n, XArray (Replicate n 'Nothing) a)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first IShX (Replicate n 'Nothing) -> IShR n
forall (n :: Nat). IShX (Replicate n 'Nothing) -> IShR n
shrFromShX2 (Mixed (Replicate n 'Nothing) a
-> (IShX (Replicate n 'Nothing), XArray (Replicate n 'Nothing) a)
forall a (sh :: [Maybe Nat]).
PrimElt a =>
Mixed sh a -> (IShX sh, XArray sh a)
mtoXArrayPrim Mixed (Replicate n 'Nothing) a
arr)

rfromXArrayPrimP :: SNat n -> XArray (Replicate n Nothing) a -> Ranked n (Primitive a)
rfromXArrayPrimP :: forall (n :: Nat) a.
SNat n -> XArray (Replicate n 'Nothing) a -> Ranked n (Primitive a)
rfromXArrayPrimP SNat n
sn XArray (Replicate n 'Nothing) a
arr = Mixed (Replicate n 'Nothing) (Primitive a)
-> Ranked n (Primitive a)
forall (n :: Nat) a. Mixed (Replicate n 'Nothing) a -> Ranked n a
Ranked (StaticShX (Replicate n 'Nothing)
-> XArray (Replicate n 'Nothing) a
-> Mixed (Replicate n 'Nothing) (Primitive a)
forall (sh :: [Maybe Nat]) a.
StaticShX sh -> XArray sh a -> Mixed sh (Primitive a)
mfromXArrayPrimP (ShX (Replicate n 'Nothing) Int -> StaticShX (Replicate n 'Nothing)
forall (sh :: [Maybe Nat]) i. ShX sh i -> StaticShX sh
ssxFromShX (StaticShX (Replicate n 'Nothing)
-> XArray (Replicate n 'Nothing) a
-> ShX (Replicate n 'Nothing) Int
forall (sh :: [Maybe Nat]) a.
StaticShX sh -> XArray sh a -> IShX sh
X.shape (SNat n -> StaticShX (Replicate n 'Nothing)
forall (n :: Nat). SNat n -> StaticShX (Replicate n 'Nothing)
ssxFromSNat SNat n
sn) XArray (Replicate n 'Nothing) a
arr)) XArray (Replicate n 'Nothing) a
arr)

rfromXArrayPrim :: PrimElt a => SNat n -> XArray (Replicate n Nothing) a -> Ranked n a
rfromXArrayPrim :: forall a (n :: Nat).
PrimElt a =>
SNat n -> XArray (Replicate n 'Nothing) a -> Ranked n a
rfromXArrayPrim SNat n
sn XArray (Replicate n 'Nothing) a
arr = Mixed (Replicate n 'Nothing) a -> Ranked n a
forall (n :: Nat) a. Mixed (Replicate n 'Nothing) a -> Ranked n a
Ranked (StaticShX (Replicate n 'Nothing)
-> XArray (Replicate n 'Nothing) a
-> Mixed (Replicate n 'Nothing) a
forall a (sh :: [Maybe Nat]).
PrimElt a =>
StaticShX sh -> XArray sh a -> Mixed sh a
mfromXArrayPrim (ShX (Replicate n 'Nothing) Int -> StaticShX (Replicate n 'Nothing)
forall (sh :: [Maybe Nat]) i. ShX sh i -> StaticShX sh
ssxFromShX (StaticShX (Replicate n 'Nothing)
-> XArray (Replicate n 'Nothing) a
-> ShX (Replicate n 'Nothing) Int
forall (sh :: [Maybe Nat]) a.
StaticShX sh -> XArray sh a -> IShX sh
X.shape (SNat n -> StaticShX (Replicate n 'Nothing)
forall (n :: Nat). SNat n -> StaticShX (Replicate n 'Nothing)
ssxFromSNat SNat n
sn) XArray (Replicate n 'Nothing) a
arr)) XArray (Replicate n 'Nothing) a
arr)

rfromPrimitive :: PrimElt a => Ranked n (Primitive a) -> Ranked n a
rfromPrimitive :: forall a (n :: Nat).
PrimElt a =>
Ranked n (Primitive a) -> Ranked n a
rfromPrimitive (Ranked Mixed (Replicate n 'Nothing) (Primitive a)
arr) = Mixed (Replicate n 'Nothing) a -> Ranked n a
forall (n :: Nat) a. Mixed (Replicate n 'Nothing) a -> Ranked n a
Ranked (Mixed (Replicate n 'Nothing) (Primitive a)
-> Mixed (Replicate n 'Nothing) a
forall (sh :: [Maybe Nat]). Mixed sh (Primitive a) -> Mixed sh a
forall a (sh :: [Maybe Nat]).
PrimElt a =>
Mixed sh (Primitive a) -> Mixed sh a
fromPrimitive Mixed (Replicate n 'Nothing) (Primitive a)
arr)

rtoPrimitive :: PrimElt a => Ranked n a -> Ranked n (Primitive a)
rtoPrimitive :: forall a (n :: Nat).
PrimElt a =>
Ranked n a -> Ranked n (Primitive a)
rtoPrimitive (Ranked Mixed (Replicate n 'Nothing) a
arr) = Mixed (Replicate n 'Nothing) (Primitive a)
-> Ranked n (Primitive a)
forall (n :: Nat) a. Mixed (Replicate n 'Nothing) a -> Ranked n a
Ranked (Mixed (Replicate n 'Nothing) a
-> Mixed (Replicate n 'Nothing) (Primitive a)
forall (sh :: [Maybe Nat]). Mixed sh a -> Mixed sh (Primitive a)
forall a (sh :: [Maybe Nat]).
PrimElt a =>
Mixed sh a -> Mixed sh (Primitive a)
toPrimitive Mixed (Replicate n 'Nothing) a
arr)