module UVMHS.Core.VectorStatic
  ( module UVMHS.Core.VectorStatic
  , module Foreign.Storable
  ) where

import UVMHS.Core.Init

import UVMHS.Core.Classes
import UVMHS.Core.Data

import UVMHS.Core.Static

import UVMHS.Core.Vector

import Foreign.Storable (Storable(..))

import qualified Prelude as HS
import qualified Data.Vector as VB
import qualified Data.Vector.Storable  as VU

infixl 6 ⋅,✖

newtype 𝕍SV n a = 𝕍SV { forall (n :: 𝐍) a. 𝕍SV n a -> 𝕀64 n -> a
un𝕍SV ∷ 𝕀64 n → a }

instance Functor (𝕍SV n) where map :: forall a b. (a -> b) -> 𝕍SV n a -> 𝕍SV n b
map a -> b
f 𝕍SV n a
xs = (𝕀64 n -> b) -> 𝕍SV n b
forall (n :: 𝐍) a. (𝕀64 n -> a) -> 𝕍SV n a
𝕍SV ((𝕀64 n -> b) -> 𝕍SV n b) -> (𝕀64 n -> b) -> 𝕍SV n b
forall a b. (a -> b) -> a -> b
$ a -> b
f (a -> b) -> (𝕀64 n -> a) -> 𝕀64 n -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝕍SV n a -> 𝕀64 n -> a
forall (n :: 𝐍) a. 𝕍SV n a -> 𝕀64 n -> a
un𝕍SV 𝕍SV n a
xs
instance Access (𝕀64 n) a (𝕍SV n a) where ⋕ :: 𝕍SV n a -> 𝕀64 n -> a
(⋕) = 𝕍SV n a -> 𝕀64 n -> a
forall (n :: 𝐍) a. 𝕍SV n a -> 𝕀64 n -> a
un𝕍SV

--------
-- 𝕍S --
--------

newtype 𝕍S n a = 𝕍S_UNSAFE { forall {k} (n :: k) a. 𝕍S n a -> Vector a
un𝕍S ∷ VB.Vector a }
  deriving (𝕍S n a -> 𝕍S n a -> Bool
(𝕍S n a -> 𝕍S n a -> Bool)
-> (𝕍S n a -> 𝕍S n a -> Bool) -> Eq (𝕍S n a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (n :: k) a. Eq a => 𝕍S n a -> 𝕍S n a -> Bool
$c== :: forall k (n :: k) a. Eq a => 𝕍S n a -> 𝕍S n a -> Bool
== :: 𝕍S n a -> 𝕍S n a -> Bool
$c/= :: forall k (n :: k) a. Eq a => 𝕍S n a -> 𝕍S n a -> Bool
/= :: 𝕍S n a -> 𝕍S n a -> Bool
Eq,Eq (𝕍S n a)
Eq (𝕍S n a) =>
(𝕍S n a -> 𝕍S n a -> Ordering)
-> (𝕍S n a -> 𝕍S n a -> Bool)
-> (𝕍S n a -> 𝕍S n a -> Bool)
-> (𝕍S n a -> 𝕍S n a -> Bool)
-> (𝕍S n a -> 𝕍S n a -> Bool)
-> (𝕍S n a -> 𝕍S n a -> 𝕍S n a)
-> (𝕍S n a -> 𝕍S n a -> 𝕍S n a)
-> Ord (𝕍S n a)
𝕍S n a -> 𝕍S n a -> Bool
𝕍S n a -> 𝕍S n a -> Ordering
𝕍S n a -> 𝕍S n a -> 𝕍S n a
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
forall k (n :: k) a. Ord a => Eq (𝕍S n a)
forall k (n :: k) a. Ord a => 𝕍S n a -> 𝕍S n a -> Bool
forall k (n :: k) a. Ord a => 𝕍S n a -> 𝕍S n a -> Ordering
forall k (n :: k) a. Ord a => 𝕍S n a -> 𝕍S n a -> 𝕍S n a
$ccompare :: forall k (n :: k) a. Ord a => 𝕍S n a -> 𝕍S n a -> Ordering
compare :: 𝕍S n a -> 𝕍S n a -> Ordering
$c< :: forall k (n :: k) a. Ord a => 𝕍S n a -> 𝕍S n a -> Bool
< :: 𝕍S n a -> 𝕍S n a -> Bool
$c<= :: forall k (n :: k) a. Ord a => 𝕍S n a -> 𝕍S n a -> Bool
<= :: 𝕍S n a -> 𝕍S n a -> Bool
$c> :: forall k (n :: k) a. Ord a => 𝕍S n a -> 𝕍S n a -> Bool
> :: 𝕍S n a -> 𝕍S n a -> Bool
$c>= :: forall k (n :: k) a. Ord a => 𝕍S n a -> 𝕍S n a -> Bool
>= :: 𝕍S n a -> 𝕍S n a -> Bool
$cmax :: forall k (n :: k) a. Ord a => 𝕍S n a -> 𝕍S n a -> 𝕍S n a
max :: 𝕍S n a -> 𝕍S n a -> 𝕍S n a
$cmin :: forall k (n :: k) a. Ord a => 𝕍S n a -> 𝕍S n a -> 𝕍S n a
min :: 𝕍S n a -> 𝕍S n a -> 𝕍S n a
Ord)

instance ToIter a (𝕍S n a)             where iter :: 𝕍S n a -> 𝐼 a
iter   = 𝕍S n a -> 𝐼 a
forall {k} (n :: k) a. 𝕍S n a -> 𝐼 a
iter𝕍S
instance (Show a) ⇒ Show (𝕍S n a)      where show :: 𝕍S n a -> String
show   = 𝕊 -> String
tohsChars (𝕊 -> String) -> (𝕍S n a -> 𝕊) -> 𝕍S n a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝕍S n a -> 𝕊
forall {k} a (n :: k). Show a => 𝕍S n a -> 𝕊
show𝕍S
instance Access (𝕀64 n) a (𝕍S n a)     where ⋕ :: 𝕍S n a -> 𝕀64 n -> a
(⋕)    = (𝕀64 n -> 𝕍S n a -> a) -> 𝕍S n a -> 𝕀64 n -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip 𝕀64 n -> 𝕍S n a -> a
forall (n :: 𝐍) a. 𝕀64 n -> 𝕍S n a -> a
idx𝕍S
instance Lookup ℕ64 a (𝕍S n a)         where ⋕? :: 𝕍S n a -> ℕ64 -> 𝑂 a
(⋕?)   = (ℕ64 -> 𝕍S n a -> 𝑂 a) -> 𝕍S n a -> ℕ64 -> 𝑂 a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ℕ64 -> 𝕍S n a -> 𝑂 a
forall {k} (n :: k) a. ℕ64 -> 𝕍S n a -> 𝑂 a
idxChecked𝕍S
instance (𝒩 n,Null a) ⇒ Null (𝕍S n a)  where null :: 𝕍S n a
null   = ℕ64S n -> 𝕍S n a
forall (n :: 𝐍) a. (𝒩 n, Null a) => ℕ64S n -> 𝕍S n a
null𝕍S ℕ64S n
forall (n :: 𝐍). 𝒩64 n => ℕ64S n
𝕟64s
instance (𝒩 n) ⇒ Functor (𝕍S n)        where map :: forall a b. (a -> b) -> 𝕍S n a -> 𝕍S n b
map    = (a -> b) -> 𝕍S n a -> 𝕍S n b
forall (n :: 𝐍) a b. 𝒩 n => (a -> b) -> 𝕍S n a -> 𝕍S n b
map𝕍S

instance (𝒩 n,Zero a)  ⇒ Zero  (𝕍S n a) where zero :: 𝕍S n a
zero     = ℕ64S n -> a -> 𝕍S n a
forall (n :: 𝐍) a. 𝒩 n => ℕ64S n -> a -> 𝕍S n a
const𝕍S ℕ64S n
forall (n :: 𝐍). 𝒩64 n => ℕ64S n
𝕟64s a
forall a. Zero a => a
zero
instance (𝒩 n,One a)   ⇒ One   (𝕍S n a) where one :: 𝕍S n a
one      = ℕ64S n -> a -> 𝕍S n a
forall (n :: 𝐍) a. 𝒩 n => ℕ64S n -> a -> 𝕍S n a
const𝕍S ℕ64S n
forall (n :: 𝐍). 𝒩64 n => ℕ64S n
𝕟64s a
forall a. One a => a
one
instance (𝒩 n,Plus a)  ⇒ Plus  (𝕍S n a) where 𝕍S n a
xs + :: 𝕍S n a -> 𝕍S n a -> 𝕍S n a
+ 𝕍S n a
ys  = ℕ64S n -> (𝕀64 n -> a) -> 𝕍S n a
forall (n :: 𝐍) a. 𝒩 n => ℕ64S n -> (𝕀64 n -> a) -> 𝕍S n a
svecF ℕ64S n
forall (n :: 𝐍). 𝒩64 n => ℕ64S n
𝕟64s ((𝕀64 n -> a) -> 𝕍S n a) -> (𝕀64 n -> a) -> 𝕍S n a
forall a b. (a -> b) -> a -> b
$ \ 𝕀64 n
i → 𝕍S n a
xs 𝕍S n a -> 𝕀64 n -> a
forall k v t. Access k v t => t -> k -> v
⋕ 𝕀64 n
i a -> a -> a
forall a. Plus a => a -> a -> a
+ 𝕍S n a
ys 𝕍S n a -> 𝕀64 n -> a
forall k v t. Access k v t => t -> k -> v
⋕ 𝕀64 n
i
instance (𝒩 n,Times a) ⇒ Times (𝕍S n a) where 𝕍S n a
xs × :: 𝕍S n a -> 𝕍S n a -> 𝕍S n a
× 𝕍S n a
ys  = ℕ64S n -> (𝕀64 n -> a) -> 𝕍S n a
forall (n :: 𝐍) a. 𝒩 n => ℕ64S n -> (𝕀64 n -> a) -> 𝕍S n a
svecF ℕ64S n
forall (n :: 𝐍). 𝒩64 n => ℕ64S n
𝕟64s ((𝕀64 n -> a) -> 𝕍S n a) -> (𝕀64 n -> a) -> 𝕍S n a
forall a b. (a -> b) -> a -> b
$ \ 𝕀64 n
i → 𝕍S n a
xs 𝕍S n a -> 𝕀64 n -> a
forall k v t. Access k v t => t -> k -> v
⋕ 𝕀64 n
i a -> a -> a
forall a. Times a => a -> a -> a
× 𝕍S n a
ys 𝕍S n a -> 𝕀64 n -> a
forall k v t. Access k v t => t -> k -> v
⋕ 𝕀64 n
i

-- instance DotProduct U 𝕍S where

svec ∷ ∀ n a. (𝒩 n) ⇒ 𝐼S n a → 𝕍S n a
svec :: forall (n :: 𝐍) a. 𝒩 n => 𝐼S n a -> 𝕍S n a
svec 𝐼S n a
xs = Vector a -> 𝕍S n a
forall {k} (n :: k) a. Vector a -> 𝕍S n a
𝕍S_UNSAFE (Vector a -> 𝕍S n a) -> Vector a -> 𝕍S n a
forall a b. (a -> b) -> a -> b
$ Int -> [a] -> Vector a
forall a. Int -> [a] -> Vector a
VB.fromListN (ℤ64 -> Int
forall a b. CHS a b => a -> b
tohs (ℤ64 -> Int) -> ℤ64 -> Int
forall a b. (a -> b) -> a -> b
$ ℕ64 -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64 (ℕ64 -> ℤ64) -> ℕ64 -> ℤ64
forall a b. (a -> b) -> a -> b
$ ℕ64S n -> ℕ64
forall (n :: 𝐍). ℕ64S n -> ℕ64
unℕ64S (ℕ64S n -> ℕ64) -> ℕ64S n -> ℕ64
forall a b. (a -> b) -> a -> b
$ forall (n :: 𝐍). 𝒩64 n => ℕ64S n
𝕟64s @n) ([a] -> Vector a) -> [a] -> Vector a
forall a b. (a -> b) -> a -> b
$ 𝐼 a -> [a]
forall a t. ToIter a t => t -> [a]
lazyList (𝐼 a -> [a]) -> 𝐼 a -> [a]
forall a b. (a -> b) -> a -> b
$ 𝐼S n a -> 𝐼 a
forall (n :: 𝐍) a. 𝐼S n a -> 𝐼 a
un𝐼S 𝐼S n a
xs

svecF ∷ ∀ n a. (𝒩 n) ⇒ ℕ64S n → (𝕀64 n → a) → 𝕍S n a
svecF :: forall (n :: 𝐍) a. 𝒩 n => ℕ64S n -> (𝕀64 n -> a) -> 𝕍S n a
svecF ℕ64S n
n 𝕀64 n -> a
f = 𝐼S n a -> 𝕍S n a
forall (n :: 𝐍) a. 𝒩 n => 𝐼S n a -> 𝕍S n a
svec (𝐼S n a -> 𝕍S n a) -> 𝐼S n a -> 𝕍S n a
forall a b. (a -> b) -> a -> b
$ (𝕀64 n -> a) -> 𝐼S n (𝕀64 n) -> 𝐼S n a
forall a b. (a -> b) -> 𝐼S n a -> 𝐼S n b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map 𝕀64 n -> a
f (𝐼S n (𝕀64 n) -> 𝐼S n a) -> 𝐼S n (𝕀64 n) -> 𝐼S n a
forall a b. (a -> b) -> a -> b
$ ℕ64S n -> 𝐼S n (𝕀64 n)
forall (n :: 𝐍). 𝒩64 n => ℕ64S n -> 𝐼S n (𝕀64 n)
upto𝕀64 ℕ64S n
n

idx𝕍S ∷ 𝕀64 n → 𝕍S n a → a
idx𝕍S :: forall (n :: 𝐍) a. 𝕀64 n -> 𝕍S n a -> a
idx𝕍S 𝕀64 n
i 𝕍S n a
xs = Vector a -> Int -> a
forall a. Vector a -> Int -> a
VB.unsafeIndex (𝕍S n a -> Vector a
forall {k} (n :: k) a. 𝕍S n a -> Vector a
un𝕍S 𝕍S n a
xs) (Int -> a) -> Int -> a
forall a b. (a -> b) -> a -> b
$ ℤ64 -> Int
forall a b. CHS a b => a -> b
tohs (ℤ64 -> Int) -> ℤ64 -> Int
forall a b. (a -> b) -> a -> b
$ ℕ64 -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64 (ℕ64 -> ℤ64) -> ℕ64 -> ℤ64
forall a b. (a -> b) -> a -> b
$ 𝕀64 n -> ℕ64
forall (n :: 𝐍). 𝕀64 n -> ℕ64
un𝕀64 𝕀64 n
i

idxChecked𝕍S ∷ ℕ64 → 𝕍S n a → 𝑂 a
idxChecked𝕍S :: forall {k} (n :: k) a. ℕ64 -> 𝕍S n a -> 𝑂 a
idxChecked𝕍S ℕ64
i 𝕍S n a
xs = Maybe a -> 𝑂 a
forall a b. CHS a b => b -> a
frhs (Maybe a -> 𝑂 a) -> Maybe a -> 𝑂 a
forall a b. (a -> b) -> a -> b
$ 𝕍S n a -> Vector a
forall {k} (n :: k) a. 𝕍S n a -> Vector a
un𝕍S 𝕍S n a
xs Vector a -> Int -> Maybe a
forall a. Vector a -> Int -> Maybe a
VB.!? ℤ64 -> Int
forall a b. CHS a b => a -> b
tohs (ℕ64 -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64 ℕ64
i)

iter𝕍SS ∷ 𝕍S n a → 𝐼S n a
iter𝕍SS :: forall (n :: 𝐍) a. 𝕍S n a -> 𝐼S n a
iter𝕍SS 𝕍S n a
xs = 𝐼 a -> 𝐼S n a
forall (n :: 𝐍) a. 𝐼 a -> 𝐼S n a
𝐼S_UNSAFE (𝐼 a -> 𝐼S n a) -> 𝐼 a -> 𝐼S n a
forall a b. (a -> b) -> a -> b
$ 𝕍S n a -> 𝐼 a
forall {k} (n :: k) a. 𝕍S n a -> 𝐼 a
iter𝕍S 𝕍S n a
xs

iter𝕍S ∷ 𝕍S n a → 𝐼 a
iter𝕍S :: forall {k} (n :: k) a. 𝕍S n a -> 𝐼 a
iter𝕍S 𝕍S n a
xs = [a] -> 𝐼 a
forall a. [a] -> 𝐼 a
iterLL ([a] -> 𝐼 a) -> [a] -> 𝐼 a
forall a b. (a -> b) -> a -> b
$ Vector a -> [a]
forall a. Vector a -> [a]
VB.toList (Vector a -> [a]) -> Vector a -> [a]
forall a b. (a -> b) -> a -> b
$ 𝕍S n a -> Vector a
forall {k} (n :: k) a. 𝕍S n a -> Vector a
un𝕍S 𝕍S n a
xs

show𝕍S ∷ (Show a) ⇒ 𝕍S n a → 𝕊
show𝕍S :: forall {k} a (n :: k). Show a => 𝕍S n a -> 𝕊
show𝕍S = 𝕊 -> 𝕊 -> 𝕊 -> (a -> 𝕊) -> 𝐼 a -> 𝕊
forall a t. ToIter a t => 𝕊 -> 𝕊 -> 𝕊 -> (a -> 𝕊) -> t -> 𝕊
showCollection 𝕊
"𝕍S[" 𝕊
"]" 𝕊
"," a -> 𝕊
forall a. Show a => a -> 𝕊
show𝕊 (𝐼 a -> 𝕊) -> (𝕍S n a -> 𝐼 a) -> 𝕍S n a -> 𝕊
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝕍S n a -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter

null𝕍S ∷ (𝒩 n,Null a) ⇒ ℕ64S n → 𝕍S n a
null𝕍S :: forall (n :: 𝐍) a. (𝒩 n, Null a) => ℕ64S n -> 𝕍S n a
null𝕍S ℕ64S n
n = ℕ64S n -> (𝕀64 n -> a) -> 𝕍S n a
forall (n :: 𝐍) a. 𝒩 n => ℕ64S n -> (𝕀64 n -> a) -> 𝕍S n a
svecF ℕ64S n
n ((𝕀64 n -> a) -> 𝕍S n a) -> (𝕀64 n -> a) -> 𝕍S n a
forall a b. (a -> b) -> a -> b
$ a -> 𝕀64 n -> a
forall a b. a -> b -> a
const a
forall a. Null a => a
null

map𝕍S ∷ (𝒩 n) ⇒ (a → b) → 𝕍S n a → 𝕍S n b
map𝕍S :: forall (n :: 𝐍) a b. 𝒩 n => (a -> b) -> 𝕍S n a -> 𝕍S n b
map𝕍S a -> b
f = 𝐼S n b -> 𝕍S n b
forall (n :: 𝐍) a. 𝒩 n => 𝐼S n a -> 𝕍S n a
svec (𝐼S n b -> 𝕍S n b) -> (𝐼S n a -> 𝐼S n b) -> 𝐼S n a -> 𝕍S n b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (a -> b) -> 𝐼S n a -> 𝐼S n b
forall a b. (a -> b) -> 𝐼S n a -> 𝐼S n b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> b
f (𝐼S n a -> 𝕍S n b) -> (𝕍S n a -> 𝐼S n a) -> 𝕍S n a -> 𝕍S n b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝕍S n a -> 𝐼S n a
forall (n :: 𝐍) a. 𝕍S n a -> 𝐼S n a
iter𝕍SS

const𝕍S ∷ (𝒩 n) ⇒ ℕ64S n → a → 𝕍S n a
const𝕍S :: forall (n :: 𝐍) a. 𝒩 n => ℕ64S n -> a -> 𝕍S n a
const𝕍S ℕ64S n
n a
x = ℕ64S n -> (𝕀64 n -> a) -> 𝕍S n a
forall (n :: 𝐍) a. 𝒩 n => ℕ64S n -> (𝕀64 n -> a) -> 𝕍S n a
svecF ℕ64S n
n ((𝕀64 n -> a) -> 𝕍S n a) -> (𝕀64 n -> a) -> 𝕍S n a
forall a b. (a -> b) -> a -> b
$ a -> 𝕀64 n -> a
forall a b. a -> b -> a
const a
x

svirt ∷ (𝒩 n) ⇒ 𝕍S n a → 𝕍SV n a
svirt :: forall (n :: 𝐍) a. 𝒩 n => 𝕍S n a -> 𝕍SV n a
svirt 𝕍S n a
xs = (𝕀64 n -> a) -> 𝕍SV n a
forall (n :: 𝐍) a. (𝕀64 n -> a) -> 𝕍SV n a
𝕍SV ((𝕀64 n -> a) -> 𝕍SV n a) -> (𝕀64 n -> a) -> 𝕍SV n a
forall a b. (a -> b) -> a -> b
$ \ 𝕀64 n
i → 𝕍S n a
xs 𝕍S n a -> 𝕀64 n -> a
forall k v t. Access k v t => t -> k -> v
⋕ 𝕀64 n
i

svirt2 ∷ (𝒩 m,𝒩 n) ⇒ 𝕍S m (𝕍S n a) → 𝕍SV m (𝕍SV n a)
svirt2 :: forall (m :: 𝐍) (n :: 𝐍) a.
(𝒩 m, 𝒩 n) =>
𝕍S m (𝕍S n a) -> 𝕍SV m (𝕍SV n a)
svirt2 = (𝕍S n a -> 𝕍SV n a) -> 𝕍SV m (𝕍S n a) -> 𝕍SV m (𝕍SV n a)
forall a b. (a -> b) -> 𝕍SV m a -> 𝕍SV m b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map 𝕍S n a -> 𝕍SV n a
forall (n :: 𝐍) a. 𝒩 n => 𝕍S n a -> 𝕍SV n a
svirt (𝕍SV m (𝕍S n a) -> 𝕍SV m (𝕍SV n a))
-> (𝕍S m (𝕍S n a) -> 𝕍SV m (𝕍S n a))
-> 𝕍S m (𝕍S n a)
-> 𝕍SV m (𝕍SV n a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝕍S m (𝕍S n a) -> 𝕍SV m (𝕍S n a)
forall (n :: 𝐍) a. 𝒩 n => 𝕍S n a -> 𝕍SV n a
svirt

sconc ∷ (𝒩 n) ⇒ ℕ64S n → 𝕍SV n a → 𝕍S n a
sconc :: forall (n :: 𝐍) a. 𝒩 n => ℕ64S n -> 𝕍SV n a -> 𝕍S n a
sconc ℕ64S n
n 𝕍SV n a
xs = ℕ64S n -> (𝕀64 n -> a) -> 𝕍S n a
forall (n :: 𝐍) a. 𝒩 n => ℕ64S n -> (𝕀64 n -> a) -> 𝕍S n a
svecF ℕ64S n
n ((𝕀64 n -> a) -> 𝕍S n a) -> (𝕀64 n -> a) -> 𝕍S n a
forall a b. (a -> b) -> a -> b
$ 𝕍SV n a -> 𝕀64 n -> a
forall (n :: 𝐍) a. 𝕍SV n a -> 𝕀64 n -> a
un𝕍SV 𝕍SV n a
xs

sconc2 ∷ (𝒩 m,𝒩 n) ⇒ ℕ64S m → ℕ64S n → 𝕍SV m (𝕍SV n a) → 𝕍S m (𝕍S n a)
sconc2 :: forall (m :: 𝐍) (n :: 𝐍) a.
(𝒩 m, 𝒩 n) =>
ℕ64S m -> ℕ64S n -> 𝕍SV m (𝕍SV n a) -> 𝕍S m (𝕍S n a)
sconc2 ℕ64S m
m ℕ64S n
n = ℕ64S m -> 𝕍SV m (𝕍S n a) -> 𝕍S m (𝕍S n a)
forall (n :: 𝐍) a. 𝒩 n => ℕ64S n -> 𝕍SV n a -> 𝕍S n a
sconc ℕ64S m
m (𝕍SV m (𝕍S n a) -> 𝕍S m (𝕍S n a))
-> (𝕍SV m (𝕍SV n a) -> 𝕍SV m (𝕍S n a))
-> 𝕍SV m (𝕍SV n a)
-> 𝕍S m (𝕍S n a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (𝕍SV n a -> 𝕍S n a) -> 𝕍SV m (𝕍SV n a) -> 𝕍SV m (𝕍S n a)
forall a b. (a -> b) -> 𝕍SV m a -> 𝕍SV m b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (ℕ64S n -> 𝕍SV n a -> 𝕍S n a
forall (n :: 𝐍) a. 𝒩 n => ℕ64S n -> 𝕍SV n a -> 𝕍S n a
sconc ℕ64S n
n)

𝐭 ∷ (𝒩 m,𝒩 n) ⇒ 𝕍S m (𝕍S n a) → 𝕍S n (𝕍S m a)
𝐭 :: forall (m :: 𝐍) (n :: 𝐍) a.
(𝒩 m, 𝒩 n) =>
𝕍S m (𝕍S n a) -> 𝕍S n (𝕍S m a)
𝐭 𝕍S m (𝕍S n a)
xs = ℕ64S n -> (𝕀64 n -> 𝕍S m a) -> 𝕍S n (𝕍S m a)
forall (n :: 𝐍) a. 𝒩 n => ℕ64S n -> (𝕀64 n -> a) -> 𝕍S n a
svecF ℕ64S n
forall (n :: 𝐍). 𝒩64 n => ℕ64S n
𝕟64s ((𝕀64 n -> 𝕍S m a) -> 𝕍S n (𝕍S m a))
-> (𝕀64 n -> 𝕍S m a) -> 𝕍S n (𝕍S m a)
forall a b. (a -> b) -> a -> b
$ \ 𝕀64 n
j → ℕ64S m -> (𝕀64 m -> a) -> 𝕍S m a
forall (n :: 𝐍) a. 𝒩 n => ℕ64S n -> (𝕀64 n -> a) -> 𝕍S n a
svecF ℕ64S m
forall (n :: 𝐍). 𝒩64 n => ℕ64S n
𝕟64s ((𝕀64 m -> a) -> 𝕍S m a) -> (𝕀64 m -> a) -> 𝕍S m a
forall a b. (a -> b) -> a -> b
$ \ 𝕀64 m
i → 𝕍S m (𝕍S n a)
xs 𝕍S m (𝕍S n a) -> 𝕀64 m -> 𝕍S n a
forall k v t. Access k v t => t -> k -> v
⋕ 𝕀64 m
i 𝕍S n a -> 𝕀64 n -> a
forall k v t. Access k v t => t -> k -> v
⋕ 𝕀64 n
j

(⋅) ∷ (𝒩 n,Additive a,Times a) ⇒ 𝕍S n a → 𝕍S n a → a
𝕍S n a
xs ⋅ :: forall (n :: 𝐍) a.
(𝒩 n, Additive a, Times a) =>
𝕍S n a -> 𝕍S n a -> a
⋅ 𝕍S n a
ys = 𝐼S n a -> a
forall a t. (ToIter a t, Additive a) => t -> a
sum (𝐼S n a -> a) -> 𝐼S n a -> a
forall a b. (a -> b) -> a -> b
$ (𝕀64 n -> a) -> 𝐼S n (𝕀64 n) -> 𝐼S n a
forall a b. (a -> b) -> 𝐼S n a -> 𝐼S n b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (\ 𝕀64 n
i → 𝕍S n a
xs 𝕍S n a -> 𝕀64 n -> a
forall k v t. Access k v t => t -> k -> v
⋕ 𝕀64 n
i a -> a -> a
forall a. Times a => a -> a -> a
× 𝕍S n a
ys 𝕍S n a -> 𝕀64 n -> a
forall k v t. Access k v t => t -> k -> v
⋕ 𝕀64 n
i) (𝐼S n (𝕀64 n) -> 𝐼S n a) -> 𝐼S n (𝕀64 n) -> 𝐼S n a
forall a b. (a -> b) -> a -> b
$ ℕ64S n -> 𝐼S n (𝕀64 n)
forall (n :: 𝐍). 𝒩64 n => ℕ64S n -> 𝐼S n (𝕀64 n)
upto𝕀64 (ℕ64S n -> 𝐼S n (𝕀64 n)) -> ℕ64S n -> 𝐼S n (𝕀64 n)
forall a b. (a -> b) -> a -> b
$ ℕ64S n
forall (n :: 𝐍). 𝒩64 n => ℕ64S n
𝕟64s

(✖) ∷ (𝒩 m,𝒩 n,𝒩 o,Additive a,Times a) ⇒ 𝕍S m (𝕍S o a) → 𝕍S n (𝕍S o a) → 𝕍S m (𝕍S n a)
𝕍S m (𝕍S o a)
xs ✖ :: forall (m :: 𝐍) (n :: 𝐍) (o :: 𝐍) a.
(𝒩 m, 𝒩 n, 𝒩 o, Additive a, Times a) =>
𝕍S m (𝕍S o a) -> 𝕍S n (𝕍S o a) -> 𝕍S m (𝕍S n a)
✖ 𝕍S n (𝕍S o a)
ys = ℕ64S m -> (𝕀64 m -> 𝕍S n a) -> 𝕍S m (𝕍S n a)
forall (n :: 𝐍) a. 𝒩 n => ℕ64S n -> (𝕀64 n -> a) -> 𝕍S n a
svecF ℕ64S m
forall (n :: 𝐍). 𝒩64 n => ℕ64S n
𝕟64s ((𝕀64 m -> 𝕍S n a) -> 𝕍S m (𝕍S n a))
-> (𝕀64 m -> 𝕍S n a) -> 𝕍S m (𝕍S n a)
forall a b. (a -> b) -> a -> b
$ \ 𝕀64 m
i → ℕ64S n -> (𝕀64 n -> a) -> 𝕍S n a
forall (n :: 𝐍) a. 𝒩 n => ℕ64S n -> (𝕀64 n -> a) -> 𝕍S n a
svecF ℕ64S n
forall (n :: 𝐍). 𝒩64 n => ℕ64S n
𝕟64s ((𝕀64 n -> a) -> 𝕍S n a) -> (𝕀64 n -> a) -> 𝕍S n a
forall a b. (a -> b) -> a -> b
$ \ 𝕀64 n
j → 𝕍S m (𝕍S o a)
xs 𝕍S m (𝕍S o a) -> 𝕀64 m -> 𝕍S o a
forall k v t. Access k v t => t -> k -> v
⋕ 𝕀64 m
i 𝕍S o a -> 𝕍S o a -> a
forall (n :: 𝐍) a.
(𝒩 n, Additive a, Times a) =>
𝕍S n a -> 𝕍S n a -> a
⋅ 𝕍S n (𝕍S o a)
ys 𝕍S n (𝕍S o a) -> 𝕀64 n -> 𝕍S o a
forall k v t. Access k v t => t -> k -> v
⋕ 𝕀64 n
j

d𝕍 ∷ 𝕍 a → (∀ n. (𝒩64 n) ⇒ 𝕍S n a → b) → b
d𝕍 :: forall a b. 𝕍 a -> (forall (n :: 𝐍). 𝒩64 n => 𝕍S n a -> b) -> b
d𝕍 𝕍 a
xs forall (n :: 𝐍). 𝒩64 n => 𝕍S n a -> b
f = ℕ64 -> (forall {n :: 𝐍}. 𝒩64 n => ℕ64S n -> b) -> b
forall a. ℕ64 -> (forall (n :: 𝐍). 𝒩64 n => ℕ64S n -> a) -> a
𝕟64d (ℤ64 -> ℕ64
forall a. (ToNatO64 a, STACK) => a -> ℕ64
natΩ64 (ℤ64 -> ℕ64) -> ℤ64 -> ℕ64
forall a b. (a -> b) -> a -> b
$ Int -> ℤ64
forall a b. CHS a b => b -> a
frhs (Int -> ℤ64) -> Int -> ℤ64
forall a b. (a -> b) -> a -> b
$ Vector a -> Int
forall a. Vector a -> Int
VB.length (Vector a -> Int) -> Vector a -> Int
forall a b. (a -> b) -> a -> b
$ 𝕍 a -> Vector a
forall a. 𝕍 a -> Vector a
un𝕍 𝕍 a
xs) ((forall {n :: 𝐍}. 𝒩64 n => ℕ64S n -> b) -> b)
-> (forall {n :: 𝐍}. 𝒩64 n => ℕ64S n -> b) -> b
forall a b. (a -> b) -> a -> b
HS.$ \ (ℕ64S n
_ ∷ ℕ64S n) → forall (n :: 𝐍). 𝒩64 n => 𝕍S n a -> b
f @n (𝕍S n a -> b) -> 𝕍S n a -> b
forall a b. (a -> b) -> a -> b
$ Vector a -> 𝕍S n a
forall {k} (n :: k) a. Vector a -> 𝕍S n a
𝕍S_UNSAFE (Vector a -> 𝕍S n a) -> Vector a -> 𝕍S n a
forall a b. (a -> b) -> a -> b
$ 𝕍 a -> Vector a
forall a. 𝕍 a -> Vector a
un𝕍 𝕍 a
xs

--------
-- 𝕌S --
--------

newtype 𝕌S n a = 𝕌S_UNSAFE { forall {k} (n :: k) a. 𝕌S n a -> Vector a
un𝕌S ∷ VU.Vector a }
  deriving (𝕌S n a -> 𝕌S n a -> Bool
(𝕌S n a -> 𝕌S n a -> Bool)
-> (𝕌S n a -> 𝕌S n a -> Bool) -> Eq (𝕌S n a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (n :: k) a. (Storable a, Eq a) => 𝕌S n a -> 𝕌S n a -> Bool
$c== :: forall k (n :: k) a. (Storable a, Eq a) => 𝕌S n a -> 𝕌S n a -> Bool
== :: 𝕌S n a -> 𝕌S n a -> Bool
$c/= :: forall k (n :: k) a. (Storable a, Eq a) => 𝕌S n a -> 𝕌S n a -> Bool
/= :: 𝕌S n a -> 𝕌S n a -> Bool
Eq,Eq (𝕌S n a)
Eq (𝕌S n a) =>
(𝕌S n a -> 𝕌S n a -> Ordering)
-> (𝕌S n a -> 𝕌S n a -> Bool)
-> (𝕌S n a -> 𝕌S n a -> Bool)
-> (𝕌S n a -> 𝕌S n a -> Bool)
-> (𝕌S n a -> 𝕌S n a -> Bool)
-> (𝕌S n a -> 𝕌S n a -> 𝕌S n a)
-> (𝕌S n a -> 𝕌S n a -> 𝕌S n a)
-> Ord (𝕌S n a)
𝕌S n a -> 𝕌S n a -> Bool
𝕌S n a -> 𝕌S n a -> Ordering
𝕌S n a -> 𝕌S n a -> 𝕌S n a
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
forall k (n :: k) a. (Storable a, Ord a) => Eq (𝕌S n a)
forall k (n :: k) a.
(Storable a, Ord a) =>
𝕌S n a -> 𝕌S n a -> Bool
forall k (n :: k) a.
(Storable a, Ord a) =>
𝕌S n a -> 𝕌S n a -> Ordering
forall k (n :: k) a.
(Storable a, Ord a) =>
𝕌S n a -> 𝕌S n a -> 𝕌S n a
$ccompare :: forall k (n :: k) a.
(Storable a, Ord a) =>
𝕌S n a -> 𝕌S n a -> Ordering
compare :: 𝕌S n a -> 𝕌S n a -> Ordering
$c< :: forall k (n :: k) a.
(Storable a, Ord a) =>
𝕌S n a -> 𝕌S n a -> Bool
< :: 𝕌S n a -> 𝕌S n a -> Bool
$c<= :: forall k (n :: k) a.
(Storable a, Ord a) =>
𝕌S n a -> 𝕌S n a -> Bool
<= :: 𝕌S n a -> 𝕌S n a -> Bool
$c> :: forall k (n :: k) a.
(Storable a, Ord a) =>
𝕌S n a -> 𝕌S n a -> Bool
> :: 𝕌S n a -> 𝕌S n a -> Bool
$c>= :: forall k (n :: k) a.
(Storable a, Ord a) =>
𝕌S n a -> 𝕌S n a -> Bool
>= :: 𝕌S n a -> 𝕌S n a -> Bool
$cmax :: forall k (n :: k) a.
(Storable a, Ord a) =>
𝕌S n a -> 𝕌S n a -> 𝕌S n a
max :: 𝕌S n a -> 𝕌S n a -> 𝕌S n a
$cmin :: forall k (n :: k) a.
(Storable a, Ord a) =>
𝕌S n a -> 𝕌S n a -> 𝕌S n a
min :: 𝕌S n a -> 𝕌S n a -> 𝕌S n a
Ord)

instance (Storable a) ⇒ ToIter a (𝕌S n a)         where iter :: 𝕌S n a -> 𝐼 a
iter   = 𝕌S n a -> 𝐼 a
forall k a (n :: k). Storable a => 𝕌S n a -> 𝐼 a
iter𝕌S
instance (Storable a,Show a) ⇒ Show (𝕌S n a)      where show :: 𝕌S n a -> String
show   = 𝕊 -> String
tohsChars (𝕊 -> String) -> (𝕌S n a -> 𝕊) -> 𝕌S n a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝕌S n a -> 𝕊
forall {k} a (n :: k). (Storable a, Show a) => 𝕌S n a -> 𝕊
show𝕌S
instance (Storable a) ⇒ Access (𝕀64 n) a (𝕌S n a) where ⋕ :: 𝕌S n a -> 𝕀64 n -> a
(⋕)    = (𝕀64 n -> 𝕌S n a -> a) -> 𝕌S n a -> 𝕀64 n -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip 𝕀64 n -> 𝕌S n a -> a
forall a (n :: 𝐍). Storable a => 𝕀64 n -> 𝕌S n a -> a
idx𝕌S
instance (Storable a) ⇒ Lookup ℕ64 a (𝕌S n a)     where ⋕? :: 𝕌S n a -> ℕ64 -> 𝑂 a
(⋕?)   = (ℕ64 -> 𝕌S n a -> 𝑂 a) -> 𝕌S n a -> ℕ64 -> 𝑂 a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ℕ64 -> 𝕌S n a -> 𝑂 a
forall {k} a (n :: k). Storable a => ℕ64 -> 𝕌S n a -> 𝑂 a
idxChecked𝕌S
instance (𝒩 n,Storable a,Null a) ⇒ Null (𝕌S n a)  where null :: 𝕌S n a
null   = ℕ64S n -> 𝕌S n a
forall (n :: 𝐍) a. (𝒩 n, Storable a, Null a) => ℕ64S n -> 𝕌S n a
null𝕌S ℕ64S n
forall (n :: 𝐍). 𝒩64 n => ℕ64S n
𝕟64s

suvec ∷ ∀ n a. (𝒩 n,Storable a) ⇒ 𝐼S n a → 𝕌S n a
suvec :: forall (n :: 𝐍) a. (𝒩 n, Storable a) => 𝐼S n a -> 𝕌S n a
suvec 𝐼S n a
xs = Vector a -> 𝕌S n a
forall {k} (n :: k) a. Vector a -> 𝕌S n a
𝕌S_UNSAFE (Vector a -> 𝕌S n a) -> Vector a -> 𝕌S n a
forall a b. (a -> b) -> a -> b
$ Int -> [a] -> Vector a
forall a. Storable a => Int -> [a] -> Vector a
VU.fromListN (ℤ64 -> Int
forall a b. CHS a b => a -> b
tohs (ℤ64 -> Int) -> ℤ64 -> Int
forall a b. (a -> b) -> a -> b
$ ℕ64 -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64 (ℕ64 -> ℤ64) -> ℕ64 -> ℤ64
forall a b. (a -> b) -> a -> b
$ ℕ64S n -> ℕ64
forall (n :: 𝐍). ℕ64S n -> ℕ64
unℕ64S (ℕ64S n -> ℕ64) -> ℕ64S n -> ℕ64
forall a b. (a -> b) -> a -> b
$ forall (n :: 𝐍). 𝒩64 n => ℕ64S n
𝕟64s @n) ([a] -> Vector a) -> [a] -> Vector a
forall a b. (a -> b) -> a -> b
$ 𝐼 a -> [a]
forall a t. ToIter a t => t -> [a]
lazyList (𝐼 a -> [a]) -> 𝐼 a -> [a]
forall a b. (a -> b) -> a -> b
$ 𝐼S n a -> 𝐼 a
forall (n :: 𝐍) a. 𝐼S n a -> 𝐼 a
un𝐼S 𝐼S n a
xs

suvecF ∷ ∀ n a. (𝒩 n,Storable a) ⇒ ℕ64S n → (𝕀64 n → a) → 𝕌S n a
suvecF :: forall (n :: 𝐍) a.
(𝒩 n, Storable a) =>
ℕ64S n -> (𝕀64 n -> a) -> 𝕌S n a
suvecF ℕ64S n
n 𝕀64 n -> a
f = 𝐼S n a -> 𝕌S n a
forall (n :: 𝐍) a. (𝒩 n, Storable a) => 𝐼S n a -> 𝕌S n a
suvec (𝐼S n a -> 𝕌S n a) -> 𝐼S n a -> 𝕌S n a
forall a b. (a -> b) -> a -> b
$ (𝕀64 n -> a) -> 𝐼S n (𝕀64 n) -> 𝐼S n a
forall a b. (a -> b) -> 𝐼S n a -> 𝐼S n b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map 𝕀64 n -> a
f (𝐼S n (𝕀64 n) -> 𝐼S n a) -> 𝐼S n (𝕀64 n) -> 𝐼S n a
forall a b. (a -> b) -> a -> b
$ ℕ64S n -> 𝐼S n (𝕀64 n)
forall (n :: 𝐍). 𝒩64 n => ℕ64S n -> 𝐼S n (𝕀64 n)
upto𝕀64 ℕ64S n
n

idx𝕌S ∷ (Storable a) ⇒ 𝕀64 n → 𝕌S n a → a
idx𝕌S :: forall a (n :: 𝐍). Storable a => 𝕀64 n -> 𝕌S n a -> a
idx𝕌S 𝕀64 n
i 𝕌S n a
xs = Vector a -> Int -> a
forall a. Storable a => Vector a -> Int -> a
VU.unsafeIndex (𝕌S n a -> Vector a
forall {k} (n :: k) a. 𝕌S n a -> Vector a
un𝕌S 𝕌S n a
xs) (Int -> a) -> Int -> a
forall a b. (a -> b) -> a -> b
$ ℤ64 -> Int
forall a b. CHS a b => a -> b
tohs (ℤ64 -> Int) -> ℤ64 -> Int
forall a b. (a -> b) -> a -> b
$ ℕ64 -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64 (ℕ64 -> ℤ64) -> ℕ64 -> ℤ64
forall a b. (a -> b) -> a -> b
$ 𝕀64 n -> ℕ64
forall (n :: 𝐍). 𝕀64 n -> ℕ64
un𝕀64 𝕀64 n
i

idxChecked𝕌S ∷ (Storable a) ⇒ ℕ64 → 𝕌S n a → 𝑂 a
idxChecked𝕌S :: forall {k} a (n :: k). Storable a => ℕ64 -> 𝕌S n a -> 𝑂 a
idxChecked𝕌S ℕ64
i 𝕌S n a
xs = Maybe a -> 𝑂 a
forall a b. CHS a b => b -> a
frhs (Maybe a -> 𝑂 a) -> Maybe a -> 𝑂 a
forall a b. (a -> b) -> a -> b
$ 𝕌S n a -> Vector a
forall {k} (n :: k) a. 𝕌S n a -> Vector a
un𝕌S 𝕌S n a
xs Vector a -> Int -> Maybe a
forall a. Storable a => Vector a -> Int -> Maybe a
VU.!? ℤ64 -> Int
forall a b. CHS a b => a -> b
tohs (ℕ64 -> ℤ64
forall a. (ToIntO64 a, STACK) => a -> ℤ64
intΩ64 ℕ64
i)

iter𝕌SS ∷ (Storable a) ⇒ 𝕌S n a → 𝐼S n a
iter𝕌SS :: forall a (n :: 𝐍). Storable a => 𝕌S n a -> 𝐼S n a
iter𝕌SS 𝕌S n a
xs = 𝐼 a -> 𝐼S n a
forall (n :: 𝐍) a. 𝐼 a -> 𝐼S n a
𝐼S_UNSAFE (𝐼 a -> 𝐼S n a) -> 𝐼 a -> 𝐼S n a
forall a b. (a -> b) -> a -> b
$ 𝐼 a -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter (𝐼 a -> 𝐼 a) -> 𝐼 a -> 𝐼 a
forall a b. (a -> b) -> a -> b
$ 𝕌S n a -> 𝐼 a
forall k a (n :: k). Storable a => 𝕌S n a -> 𝐼 a
iter𝕌S 𝕌S n a
xs

iter𝕌S ∷ (Storable a) ⇒ 𝕌S n a → 𝐼 a
iter𝕌S :: forall k a (n :: k). Storable a => 𝕌S n a -> 𝐼 a
iter𝕌S 𝕌S n a
xs = [a] -> 𝐼 a
forall a. [a] -> 𝐼 a
iterLL ([a] -> 𝐼 a) -> [a] -> 𝐼 a
forall a b. (a -> b) -> a -> b
$ Vector a -> [a]
forall a. Storable a => Vector a -> [a]
VU.toList (Vector a -> [a]) -> Vector a -> [a]
forall a b. (a -> b) -> a -> b
$ 𝕌S n a -> Vector a
forall {k} (n :: k) a. 𝕌S n a -> Vector a
un𝕌S 𝕌S n a
xs

show𝕌S ∷ (Storable a,Show a) ⇒ 𝕌S n a → 𝕊
show𝕌S :: forall {k} a (n :: k). (Storable a, Show a) => 𝕌S n a -> 𝕊
show𝕌S = 𝕊 -> 𝕊 -> 𝕊 -> (a -> 𝕊) -> 𝐼 a -> 𝕊
forall a t. ToIter a t => 𝕊 -> 𝕊 -> 𝕊 -> (a -> 𝕊) -> t -> 𝕊
showCollection 𝕊
"𝕌S[" 𝕊
"]" 𝕊
"," a -> 𝕊
forall a. Show a => a -> 𝕊
show𝕊 (𝐼 a -> 𝕊) -> (𝕌S n a -> 𝐼 a) -> 𝕌S n a -> 𝕊
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝕌S n a -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter

null𝕌S ∷ (𝒩 n,Storable a,Null a) ⇒ ℕ64S n → 𝕌S n a
null𝕌S :: forall (n :: 𝐍) a. (𝒩 n, Storable a, Null a) => ℕ64S n -> 𝕌S n a
null𝕌S ℕ64S n
n = ℕ64S n -> (𝕀64 n -> a) -> 𝕌S n a
forall (n :: 𝐍) a.
(𝒩 n, Storable a) =>
ℕ64S n -> (𝕀64 n -> a) -> 𝕌S n a
suvecF ℕ64S n
n ((𝕀64 n -> a) -> 𝕌S n a) -> (𝕀64 n -> a) -> 𝕌S n a
forall a b. (a -> b) -> a -> b
$ a -> 𝕀64 n -> a
forall a b. a -> b -> a
const a
forall a. Null a => a
null

map𝕌S ∷ (𝒩 n,Storable a,Storable b) ⇒ (a → b) → 𝕌S n a → 𝕌S n b
map𝕌S :: forall (n :: 𝐍) a b.
(𝒩 n, Storable a, Storable b) =>
(a -> b) -> 𝕌S n a -> 𝕌S n b
map𝕌S a -> b
f = 𝐼S n b -> 𝕌S n b
forall (n :: 𝐍) a. (𝒩 n, Storable a) => 𝐼S n a -> 𝕌S n a
suvec (𝐼S n b -> 𝕌S n b) -> (𝐼S n a -> 𝐼S n b) -> 𝐼S n a -> 𝕌S n b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (a -> b) -> 𝐼S n a -> 𝐼S n b
forall a b. (a -> b) -> 𝐼S n a -> 𝐼S n b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> b
f (𝐼S n a -> 𝕌S n b) -> (𝕌S n a -> 𝐼S n a) -> 𝕌S n a -> 𝕌S n b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝕌S n a -> 𝐼S n a
forall a (n :: 𝐍). Storable a => 𝕌S n a -> 𝐼S n a
iter𝕌SS

d𝕌 ∷ (Storable a) ⇒ 𝕌 a → (∀ n. (𝒩64 n) ⇒ 𝕌S n a → b) → b
d𝕌 :: forall a b.
Storable a =>
𝕌 a -> (forall (n :: 𝐍). 𝒩64 n => 𝕌S n a -> b) -> b
d𝕌 𝕌 a
xs forall (n :: 𝐍). 𝒩64 n => 𝕌S n a -> b
f = ℕ64 -> (forall {n :: 𝐍}. 𝒩64 n => ℕ64S n -> b) -> b
forall a. ℕ64 -> (forall (n :: 𝐍). 𝒩64 n => ℕ64S n -> a) -> a
𝕟64d (ℤ64 -> ℕ64
forall a. (ToNatO64 a, STACK) => a -> ℕ64
natΩ64 (ℤ64 -> ℕ64) -> ℤ64 -> ℕ64
forall a b. (a -> b) -> a -> b
$ Int -> ℤ64
forall a b. CHS a b => b -> a
frhs (Int -> ℤ64) -> Int -> ℤ64
forall a b. (a -> b) -> a -> b
$ Vector a -> Int
forall a. Storable a => Vector a -> Int
VU.length (Vector a -> Int) -> Vector a -> Int
forall a b. (a -> b) -> a -> b
$ 𝕌 a -> Vector a
forall a. 𝕌 a -> Vector a
un𝕌 𝕌 a
xs) ((forall {n :: 𝐍}. 𝒩64 n => ℕ64S n -> b) -> b)
-> (forall {n :: 𝐍}. 𝒩64 n => ℕ64S n -> b) -> b
forall a b. (a -> b) -> a -> b
HS.$ \ (ℕ64S n
_ ∷ ℕ64S n) → forall (n :: 𝐍). 𝒩64 n => 𝕌S n a -> b
f @n (𝕌S n a -> b) -> 𝕌S n a -> b
forall a b. (a -> b) -> a -> b
$ Vector a -> 𝕌S n a
forall {k} (n :: k) a. Vector a -> 𝕌S n a
𝕌S_UNSAFE (Vector a -> 𝕌S n a) -> Vector a -> 𝕌S n a
forall a b. (a -> b) -> a -> b
$ 𝕌 a -> Vector a
forall a. 𝕌 a -> Vector a
un𝕌 𝕌 a
xs

--------
-- 𝕄S --
--------

data 𝕄S (ns ∷ [𝐍]) a where
  Nil𝕄S ∷ a → 𝕄S '[] a
  Cons𝕄S ∷ 𝕍S n (𝕄S ns a) → 𝕄S (n ': ns) a

zero𝕄S ∷ (AllC 𝒩 ns,Zero a) ⇒ Spine ns → 𝕄S ns a
zero𝕄S :: forall (ns :: [𝐍]) a. (AllC 𝒩 ns, Zero a) => Spine ns -> 𝕄S ns a
zero𝕄S = \case
  Spine ns
NilSpine → 𝕄S ns a
forall a. Zero a => a
zero
  ConsSpine Spine xs
sp → 𝕍S x (𝕄S xs a) -> 𝕄S (x : xs) a
forall (n :: 𝐍) (ns :: [𝐍]) a. 𝕍S n (𝕄S ns a) -> 𝕄S (n : ns) a
Cons𝕄S (𝕍S x (𝕄S xs a) -> 𝕄S (x : xs) a)
-> 𝕍S x (𝕄S xs a) -> 𝕄S (x : xs) a
forall a b. (a -> b) -> a -> b
$ ℕ64S x -> 𝕄S xs a -> 𝕍S x (𝕄S xs a)
forall (n :: 𝐍) a. 𝒩 n => ℕ64S n -> a -> 𝕍S n a
const𝕍S ℕ64S x
forall (n :: 𝐍). 𝒩64 n => ℕ64S n
𝕟64s (𝕄S xs a -> 𝕍S x (𝕄S xs a)) -> 𝕄S xs a -> 𝕍S x (𝕄S xs a)
forall a b. (a -> b) -> a -> b
$ Spine xs -> 𝕄S xs a
forall (ns :: [𝐍]) a. (AllC 𝒩 ns, Zero a) => Spine ns -> 𝕄S ns a
zero𝕄S Spine xs
sp

instance (HasSpine ns,AllC 𝒩 ns,Zero a) ⇒ Zero (𝕄S ns a) where
  zero :: 𝕄S ns a
zero = Spine ns -> 𝕄S ns a
forall (ns :: [𝐍]) a. (AllC 𝒩 ns, Zero a) => Spine ns -> 𝕄S ns a
zero𝕄S Spine ns
forall {a} (xs :: [a]). HasSpine xs => Spine xs
spine

instance (AllC 𝒩 ns,Plus a) ⇒ Plus (𝕄S ns a) where
  Nil𝕄S a
x + :: 𝕄S ns a -> 𝕄S ns a -> 𝕄S ns a
+ Nil𝕄S a
y = a -> 𝕄S '[] a
forall a. a -> 𝕄S '[] a
Nil𝕄S (a -> 𝕄S '[] a) -> a -> 𝕄S '[] a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Plus a => a -> a -> a
+ a
y
  Cons𝕄S 𝕍S n (𝕄S ns a)
xs + Cons𝕄S 𝕍S n (𝕄S ns a)
ys = 𝕍S n (𝕄S ns a) -> 𝕄S (n : ns) a
forall (n :: 𝐍) (ns :: [𝐍]) a. 𝕍S n (𝕄S ns a) -> 𝕄S (n : ns) a
Cons𝕄S (𝕍S n (𝕄S ns a) -> 𝕄S (n : ns) a)
-> 𝕍S n (𝕄S ns a) -> 𝕄S (n : ns) a
forall a b. (a -> b) -> a -> b
$ 𝕍S n (𝕄S ns a)
xs 𝕍S n (𝕄S ns a) -> 𝕍S n (𝕄S ns a) -> 𝕍S n (𝕄S ns a)
forall a. Plus a => a -> a -> a
+ 𝕍S n (𝕄S ns a)
𝕍S n (𝕄S ns a)
ys

instance (AllC 𝒩 ns,Times a) ⇒ Times (𝕄S ns a) where
  Nil𝕄S a
x × :: 𝕄S ns a -> 𝕄S ns a -> 𝕄S ns a
× Nil𝕄S a
y = a -> 𝕄S '[] a
forall a. a -> 𝕄S '[] a
Nil𝕄S (a -> 𝕄S '[] a) -> a -> 𝕄S '[] a
forall a b. (a -> b) -> a -> b
$ a
x a -> a -> a
forall a. Times a => a -> a -> a
× a
y
  Cons𝕄S 𝕍S n (𝕄S ns a)
xs × Cons𝕄S 𝕍S n (𝕄S ns a)
ys = 𝕍S n (𝕄S ns a) -> 𝕄S (n : ns) a
forall (n :: 𝐍) (ns :: [𝐍]) a. 𝕍S n (𝕄S ns a) -> 𝕄S (n : ns) a
Cons𝕄S (𝕍S n (𝕄S ns a) -> 𝕄S (n : ns) a)
-> 𝕍S n (𝕄S ns a) -> 𝕄S (n : ns) a
forall a b. (a -> b) -> a -> b
$ 𝕍S n (𝕄S ns a)
xs 𝕍S n (𝕄S ns a) -> 𝕍S n (𝕄S ns a) -> 𝕍S n (𝕄S ns a)
forall a. Times a => a -> a -> a
× 𝕍S n (𝕄S ns a)
𝕍S n (𝕄S ns a)
ys

mapUnder𝕄S ∷ (AllC 𝒩 ns) ⇒ Spine ns → (𝕄S ms₁ a → 𝕄S ms₂ b) → 𝕄S (ns ⧺ ms₁) a → 𝕄S (ns ⧺ ms₂) b
mapUnder𝕄S :: forall (ns :: [𝐍]) (ms₁ :: [𝐍]) a (ms₂ :: [𝐍]) b.
AllC 𝒩 ns =>
Spine ns
-> (𝕄S ms₁ a -> 𝕄S ms₂ b) -> 𝕄S (ns ⧺ ms₁) a -> 𝕄S (ns ⧺ ms₂) b
mapUnder𝕄S Spine ns
sp 𝕄S ms₁ a -> 𝕄S ms₂ b
f 𝕄S (ns ⧺ ms₁) a
xs = case Spine ns
sp of
  Spine ns
NilSpine → 𝕄S ms₁ a -> 𝕄S ms₂ b
f 𝕄S ms₁ a
𝕄S (ns ⧺ ms₁) a
xs
  ConsSpine Spine xs
sp' → case 𝕄S (ns ⧺ ms₁) a
xs of
    Cons𝕄S (𝕍S n (𝕄S ns a)
xs' ∷ 𝕍S n (𝕄S ns a)) → 𝕍S n (𝕄S (xs ⧺ ms₂) b) -> 𝕄S (n : (xs ⧺ ms₂)) b
forall (n :: 𝐍) (ns :: [𝐍]) a. 𝕍S n (𝕄S ns a) -> 𝕄S (n : ns) a
Cons𝕄S (𝕍S n (𝕄S (xs ⧺ ms₂) b) -> 𝕄S (n : (xs ⧺ ms₂)) b)
-> 𝕍S n (𝕄S (xs ⧺ ms₂) b) -> 𝕄S (n : (xs ⧺ ms₂)) b
forall a b. (a -> b) -> a -> b
$ (𝕄S (xs ⧺ ms₁) a -> 𝕄S (xs ⧺ ms₂) b)
-> 𝕍S n (𝕄S (xs ⧺ ms₁) a) -> 𝕍S n (𝕄S (xs ⧺ ms₂) b)
forall a b. (a -> b) -> 𝕍S n a -> 𝕍S n b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (Spine xs
-> (𝕄S ms₁ a -> 𝕄S ms₂ b) -> 𝕄S (xs ⧺ ms₁) a -> 𝕄S (xs ⧺ ms₂) b
forall (ns :: [𝐍]) (ms₁ :: [𝐍]) a (ms₂ :: [𝐍]) b.
AllC 𝒩 ns =>
Spine ns
-> (𝕄S ms₁ a -> 𝕄S ms₂ b) -> 𝕄S (ns ⧺ ms₁) a -> 𝕄S (ns ⧺ ms₂) b
mapUnder𝕄S Spine xs
sp' 𝕄S ms₁ a -> 𝕄S ms₂ b
f) 𝕍S n (𝕄S ns a)
𝕍S n (𝕄S (xs ⧺ ms₁) a)
xs'