module UVMHS.Core.VectorSparse where

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

import qualified Data.IntMap.Strict as IntMap
import qualified Data.IntSet as IntSet

import qualified Prelude as HS

data 𝑉 a = 𝑉 { forall a. 𝑉 a -> IntMap a
un𝑉 ∷ IntMap.IntMap a }
  deriving (𝑉 a -> 𝑉 a -> Bool
(𝑉 a -> 𝑉 a -> Bool) -> (𝑉 a -> 𝑉 a -> Bool) -> Eq (𝑉 a)
forall a. Eq a => 𝑉 a -> 𝑉 a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => 𝑉 a -> 𝑉 a -> Bool
== :: 𝑉 a -> 𝑉 a -> Bool
$c/= :: forall a. Eq a => 𝑉 a -> 𝑉 a -> Bool
/= :: 𝑉 a -> 𝑉 a -> Bool
Eq,Eq (𝑉 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)
𝑉 a -> 𝑉 a -> Bool
𝑉 a -> 𝑉 a -> Ordering
𝑉 a -> 𝑉 a -> 𝑉 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 a. Ord a => Eq (𝑉 a)
forall a. Ord a => 𝑉 a -> 𝑉 a -> Bool
forall a. Ord a => 𝑉 a -> 𝑉 a -> Ordering
forall a. Ord a => 𝑉 a -> 𝑉 a -> 𝑉 a
$ccompare :: forall a. Ord a => 𝑉 a -> 𝑉 a -> Ordering
compare :: 𝑉 a -> 𝑉 a -> Ordering
$c< :: forall a. Ord a => 𝑉 a -> 𝑉 a -> Bool
< :: 𝑉 a -> 𝑉 a -> Bool
$c<= :: forall a. Ord a => 𝑉 a -> 𝑉 a -> Bool
<= :: 𝑉 a -> 𝑉 a -> Bool
$c> :: forall a. Ord a => 𝑉 a -> 𝑉 a -> Bool
> :: 𝑉 a -> 𝑉 a -> Bool
$c>= :: forall a. Ord a => 𝑉 a -> 𝑉 a -> Bool
>= :: 𝑉 a -> 𝑉 a -> Bool
$cmax :: forall a. Ord a => 𝑉 a -> 𝑉 a -> 𝑉 a
max :: 𝑉 a -> 𝑉 a -> 𝑉 a
$cmin :: forall a. Ord a => 𝑉 a -> 𝑉 a -> 𝑉 a
min :: 𝑉 a -> 𝑉 a -> 𝑉 a
Ord)

instance Lookup ℤ64 a (𝑉 a) where ⋕? :: 𝑉 a -> ℤ64 -> 𝑂 a
(⋕?) = 𝑉 a -> ℤ64 -> 𝑂 a
forall a. 𝑉 a -> ℤ64 -> 𝑂 a
lookup𝑉
instance Single (ℤ64 ∧ a) (𝑉 a) where single :: (ℤ64 ∧ a) -> 𝑉 a
single = (ℤ64 ∧ a) -> 𝑉 a
forall a. (ℤ64 ∧ a) -> 𝑉 a
single𝑉

instance (POrd a) ⇒ POrd (𝑉 a) where ⊑ :: 𝑉 a -> 𝑉 a -> Bool
(⊑) = (a -> a -> Bool) -> 𝑉 a -> 𝑉 a -> Bool
forall a. (a -> a -> Bool) -> 𝑉 a -> 𝑉 a -> Bool
subDictBy𝑉 a -> a -> Bool
forall a. POrd a => a -> a -> Bool
(⊑)

instance Null (𝑉 a) where null :: 𝑉 a
null = 𝑉 a
forall a. 𝑉 a
wø
instance (Append a) ⇒ Append (𝑉 a) where ⧺ :: 𝑉 a -> 𝑉 a -> 𝑉 a
(⧺) = (a -> a -> a) -> 𝑉 a -> 𝑉 a -> 𝑉 a
forall a. (a -> a -> a) -> 𝑉 a -> 𝑉 a -> 𝑉 a
unionWith𝑉 a -> a -> a
forall a. Append a => a -> a -> a
(⧺)
instance (Append a) ⇒ Monoid (𝑉 a) 

instance (Null a) ⇒ Unit (𝑉 a) where unit :: 𝑉 a
unit = ℤ64
forall a. Null a => a
null ℤ64 -> a -> 𝑉 a
forall a. ℤ64 -> a -> 𝑉 a
↦♮ a
forall a. Null a => a
null
instance (Append a,Cross a) ⇒ Cross (𝑉 a) where
  𝑉 a
ixs₁ ⨳ :: 𝑉 a -> 𝑉 a -> 𝑉 a
⨳ 𝑉 a
ixs₂ = 𝑉 a -> (𝑉 a -> 𝑉 a -> 𝑉 a) -> 𝐼 (𝑉 a) -> 𝑉 a
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
foldr 𝑉 a
forall a. 𝑉 a
wø ((a -> a -> a) -> 𝑉 a -> 𝑉 a -> 𝑉 a
forall a. (a -> a -> a) -> 𝑉 a -> 𝑉 a -> 𝑉 a
unionWith𝑉 a -> a -> a
forall a. Append a => a -> a -> a
(⧺)) (𝐼 (𝑉 a) -> 𝑉 a) -> 𝐼 (𝑉 a) -> 𝑉 a
forall a b. (a -> b) -> a -> b
$ do
    (ℤ64
i₁ :* a
x₁) ← 𝑉 a -> 𝐼 (ℤ64 ∧ a)
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑉 a
ixs₁
    (ℤ64
i₂ :* a
x₂) ← 𝑉 a -> 𝐼 (ℤ64 ∧ a)
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑉 a
ixs₂
    𝑉 a -> 𝐼 (𝑉 a)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (𝑉 a -> 𝐼 (𝑉 a)) -> 𝑉 a -> 𝐼 (𝑉 a)
forall a b. (a -> b) -> a -> b
$ (ℤ64
i₁ ℤ64 -> ℤ64 -> ℤ64
forall a. Append a => a -> a -> a
⧺ ℤ64
i₂) ℤ64 -> a -> 𝑉 a
forall a. ℤ64 -> a -> 𝑉 a
↦♮ (a
x₁ a -> a -> a
forall a. Cross a => a -> a -> a
⨳ a
x₂)
instance (Prodoid a) ⇒ Prodoid (𝑉 a)

instance Zero (𝑉 a) where zero :: 𝑉 a
zero = 𝑉 a
forall a. 𝑉 a
wø
instance (Plus a) ⇒ Plus (𝑉 a) where + :: 𝑉 a -> 𝑉 a -> 𝑉 a
(+) = (a -> a -> a) -> 𝑉 a -> 𝑉 a -> 𝑉 a
forall a. (a -> a -> a) -> 𝑉 a -> 𝑉 a -> 𝑉 a
unionWith𝑉 a -> a -> a
forall a. Plus a => a -> a -> a
(+)
instance (Plus a) ⇒ Additive (𝑉 a)

instance (Zero a) ⇒ One (𝑉 a) where one :: 𝑉 a
one = ℤ64
forall a. Zero a => a
zero ℤ64 -> a -> 𝑉 a
forall a. ℤ64 -> a -> 𝑉 a
↦♮ a
forall a. Zero a => a
zero
instance (Plus a,Times a) ⇒ Times (𝑉 a) where
  𝑉 a
ixs₁ × :: 𝑉 a -> 𝑉 a -> 𝑉 a
× 𝑉 a
ixs₂ = 𝑉 a -> (𝑉 a -> 𝑉 a -> 𝑉 a) -> 𝐼 (𝑉 a) -> 𝑉 a
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
fold 𝑉 a
forall a. 𝑉 a
wø ((a -> a -> a) -> 𝑉 a -> 𝑉 a -> 𝑉 a
forall a. (a -> a -> a) -> 𝑉 a -> 𝑉 a -> 𝑉 a
unionWith𝑉 a -> a -> a
forall a. Plus a => a -> a -> a
(+)) (𝐼 (𝑉 a) -> 𝑉 a) -> 𝐼 (𝑉 a) -> 𝑉 a
forall a b. (a -> b) -> a -> b
$ do
    (ℤ64
i₁ :* a
x₁) ← 𝑉 a -> 𝐼 (ℤ64 ∧ a)
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑉 a
ixs₁
    (ℤ64
i₂ :* a
x₂) ← 𝑉 a -> 𝐼 (ℤ64 ∧ a)
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑉 a
ixs₂
    𝑉 a -> 𝐼 (𝑉 a)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (𝑉 a -> 𝐼 (𝑉 a)) -> 𝑉 a -> 𝐼 (𝑉 a)
forall a b. (a -> b) -> a -> b
$ (ℤ64
i₁ ℤ64 -> ℤ64 -> ℤ64
forall a. Plus a => a -> a -> a
+ ℤ64
i₂) ℤ64 -> a -> 𝑉 a
forall a. ℤ64 -> a -> 𝑉 a
↦♮ (a
x₁ a -> a -> a
forall a. Times a => a -> a -> a
× a
x₂)
instance (Multiplicative a) ⇒ Multiplicative (𝑉 a)

instance Bot (𝑉 a) where bot :: 𝑉 a
bot = 𝑉 a
forall a. 𝑉 a
wø
instance (Join a) ⇒ Join (𝑉 a) where ⊔ :: 𝑉 a -> 𝑉 a -> 𝑉 a
(⊔) = (a -> a -> a) -> 𝑉 a -> 𝑉 a -> 𝑉 a
forall a. (a -> a -> a) -> 𝑉 a -> 𝑉 a -> 𝑉 a
unionWith𝑉 a -> a -> a
forall a. Join a => a -> a -> a
(⊔)
instance (Join a) ⇒ JoinLattice (𝑉 a)

instance Top (𝑉 a) where top :: 𝑉 a
top = 𝑉 a
forall a. 𝑉 a
wø
instance (Meet a) ⇒ Meet (𝑉 a) where ⊓ :: 𝑉 a -> 𝑉 a -> 𝑉 a
(⊓) = (a -> a -> a) -> 𝑉 a -> 𝑉 a -> 𝑉 a
forall a. (a -> a -> a) -> 𝑉 a -> 𝑉 a -> 𝑉 a
unionWith𝑉 a -> a -> a
forall a. Meet a => a -> a -> a
(⊓)
instance (Meet a) ⇒ MeetLattice (𝑉 a)

instance Functor 𝑉 where map :: forall a b. (a -> b) -> 𝑉 a -> 𝑉 b
map = (a -> b) -> 𝑉 a -> 𝑉 b
forall a b. (a -> b) -> 𝑉 a -> 𝑉 b
map𝑉

instance ToIter (ℤ64 ∧ a) (𝑉 a) where iter :: 𝑉 a -> 𝐼 (ℤ64 ∧ a)
iter = 𝑉 a -> 𝐼 (ℤ64 ∧ a)
forall a. 𝑉 a -> 𝐼 (ℤ64 ∧ a)
iter𝑉

instance (Show a) ⇒ Show (𝑉 a) where 
  show :: 𝑉 a -> String
show = 𝕊 -> String
tohsChars (𝕊 -> String) -> (𝑉 a -> 𝕊) -> 𝑉 a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝕊 -> 𝕊 -> 𝕊 -> ((ℤ64 ∧ a) -> 𝕊) -> 𝑉 a -> 𝕊
forall a t. ToIter a t => 𝕊 -> 𝕊 -> 𝕊 -> (a -> 𝕊) -> t -> 𝕊
showCollection 𝕊
"{" 𝕊
"}" 𝕊
"," (\ (ℤ64
i :* a
x) → ℤ64 -> 𝕊
forall a. Show a => a -> 𝕊
show𝕊 ℤ64
i 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
⧺ 𝕊
"⇒" 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
⧺ a -> 𝕊
forall a. Show a => a -> 𝕊
show𝕊 a
x)

lookup𝑉 ∷ 𝑉 a → ℤ64 → 𝑂 a
lookup𝑉 :: forall a. 𝑉 a -> ℤ64 -> 𝑂 a
lookup𝑉 𝑉 a
ixs ℤ64
i = 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
$ 𝑉 a -> IntMap a
forall a. 𝑉 a -> IntMap a
un𝑉 𝑉 a
ixs IntMap a -> Int -> Maybe a
forall a. IntMap a -> Int -> Maybe a
IntMap.!? ℤ64 -> Int
forall a b. CHS a b => a -> b
tohs ℤ64
i

single𝑉 ∷ ℤ64 ∧ a → 𝑉 a
single𝑉 :: forall a. (ℤ64 ∧ a) -> 𝑉 a
single𝑉 (ℤ64
i :* a
x) = IntMap a -> 𝑉 a
forall a. IntMap a -> 𝑉 a
𝑉 (IntMap a -> 𝑉 a) -> IntMap a -> 𝑉 a
forall a b. (a -> b) -> a -> b
$ Int -> a -> IntMap a
forall a. Int -> a -> IntMap a
IntMap.singleton (ℤ64 -> Int
forall a b. CHS a b => a -> b
tohs ℤ64
i) a
x

subDictBy𝑉 ∷ (a → a → 𝔹) → 𝑉 a → 𝑉 a → 𝔹
subDictBy𝑉 :: forall a. (a -> a -> Bool) -> 𝑉 a -> 𝑉 a -> Bool
subDictBy𝑉 a -> a -> Bool
f 𝑉 a
ixs₁ 𝑉 a
ixs₂ = (a -> a -> Bool) -> IntMap a -> IntMap a -> Bool
forall a b. (a -> b -> Bool) -> IntMap a -> IntMap b -> Bool
IntMap.isSubmapOfBy a -> a -> Bool
f (𝑉 a -> IntMap a
forall a. 𝑉 a -> IntMap a
un𝑉 𝑉 a
ixs₁) (𝑉 a -> IntMap a
forall a. 𝑉 a -> IntMap a
un𝑉 𝑉 a
ixs₂)

wø ∷ 𝑉 a
wø :: forall a. 𝑉 a
wø = IntMap a -> 𝑉 a
forall a. IntMap a -> 𝑉 a
𝑉 IntMap a
forall a. IntMap a
IntMap.empty

unionWith𝑉 ∷ (a → a → a) → 𝑉 a → 𝑉 a → 𝑉 a
unionWith𝑉 :: forall a. (a -> a -> a) -> 𝑉 a -> 𝑉 a -> 𝑉 a
unionWith𝑉 a -> a -> a
f 𝑉 a
ixs₁ 𝑉 a
ixs₂ = IntMap a -> 𝑉 a
forall a. IntMap a -> 𝑉 a
𝑉 (IntMap a -> 𝑉 a) -> IntMap a -> 𝑉 a
forall a b. (a -> b) -> a -> b
$ (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
forall a. (a -> a -> a) -> IntMap a -> IntMap a -> IntMap a
IntMap.unionWith a -> a -> a
f (𝑉 a -> IntMap a
forall a. 𝑉 a -> IntMap a
un𝑉 𝑉 a
ixs₁) (𝑉 a -> IntMap a
forall a. 𝑉 a -> IntMap a
un𝑉 𝑉 a
ixs₂)
  
(↦♮) ∷ ℤ64 → a → 𝑉 a
ℤ64
i ↦♮ :: forall a. ℤ64 -> a -> 𝑉 a
↦♮ a
x = IntMap a -> 𝑉 a
forall a. IntMap a -> 𝑉 a
𝑉 (IntMap a -> 𝑉 a) -> IntMap a -> 𝑉 a
forall a b. (a -> b) -> a -> b
$ Int -> a -> IntMap a
forall a. Int -> a -> IntMap a
IntMap.singleton (ℤ64 -> Int
forall a b. CHS a b => a -> b
tohs ℤ64
i) a
x

(⋵♮) ∷ ℤ64 → 𝑉 a → 𝔹
ℤ64
i ⋵♮ :: forall a. ℤ64 -> 𝑉 a -> Bool
⋵♮ 𝑉 a
ixs = ℤ64 -> Int
forall a b. CHS a b => a -> b
tohs ℤ64
i Int -> IntMap a -> Bool
forall a. Int -> IntMap a -> Bool
`IntMap.member` 𝑉 a -> IntMap a
forall a. 𝑉 a -> IntMap a
un𝑉 𝑉 a
ixs

(⩌♮) ∷ 𝑉 a → 𝑉 a → 𝑉 a
𝑉 a
ixs₁ ⩌♮ :: forall a. 𝑉 a -> 𝑉 a -> 𝑉 a
⩌♮ 𝑉 a
ixs₂ = IntMap a -> 𝑉 a
forall a. IntMap a -> 𝑉 a
𝑉 (IntMap a -> 𝑉 a) -> IntMap a -> 𝑉 a
forall a b. (a -> b) -> a -> b
$ 𝑉 a -> IntMap a
forall a. 𝑉 a -> IntMap a
un𝑉 𝑉 a
ixs₁ IntMap a -> IntMap a -> IntMap a
forall a. IntMap a -> IntMap a -> IntMap a
`IntMap.union` 𝑉 a -> IntMap a
forall a. 𝑉 a -> IntMap a
un𝑉 𝑉 a
ixs₂

(⩍♮) ∷ 𝑉 a → 𝑉 a → 𝑉 a
𝑉 a
ixs₁ ⩍♮ :: forall a. 𝑉 a -> 𝑉 a -> 𝑉 a
⩍♮ 𝑉 a
ixs₂ = IntMap a -> 𝑉 a
forall a. IntMap a -> 𝑉 a
𝑉 (IntMap a -> 𝑉 a) -> IntMap a -> 𝑉 a
forall a b. (a -> b) -> a -> b
$ 𝑉 a -> IntMap a
forall a. 𝑉 a -> IntMap a
un𝑉 𝑉 a
ixs₁ IntMap a -> IntMap a -> IntMap a
forall a b. IntMap a -> IntMap b -> IntMap a
`IntMap.intersection` 𝑉 a -> IntMap a
forall a. 𝑉 a -> IntMap a
un𝑉 𝑉 a
ixs₂
 
-- (∸♮) ∷ 𝑉 a → 𝑉 a → 𝑉 a
-- ixs₁ ∸♮ ixs₂ = 𝑉 $ un𝑉 ixs₁ `IntMap.difference` un𝑉 ixs₂

delete𝑉 ∷ ℤ64 → 𝑉 a → 𝑉 a
delete𝑉 :: forall a. ℤ64 -> 𝑉 a -> 𝑉 a
delete𝑉 ℤ64
i 𝑉 a
ixs = IntMap a -> 𝑉 a
forall a. IntMap a -> 𝑉 a
𝑉 (IntMap a -> 𝑉 a) -> IntMap a -> 𝑉 a
forall a b. (a -> b) -> a -> b
$ Int -> IntMap a -> IntMap a
forall a. Int -> IntMap a -> IntMap a
IntMap.delete (ℤ64 -> Int
forall a b. CHS a b => a -> b
tohs ℤ64
i) (IntMap a -> IntMap a) -> IntMap a -> IntMap a
forall a b. (a -> b) -> a -> b
$ 𝑉 a -> IntMap a
forall a. 𝑉 a -> IntMap a
un𝑉 𝑉 a
ixs

size𝑉 ∷ 𝑉 a → ℕ
size𝑉 :: forall a. 𝑉 a -> ℕ
size𝑉 = Int -> ℕ
forall a b. (Integral a, Num b) => a -> b
HS.fromIntegral (Int -> ℕ) -> (IntMap a -> Int) -> IntMap a -> ℕ
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ IntMap a -> Int
forall a. IntMap a -> Int
IntMap.size (IntMap a -> ℕ) -> (𝑉 a -> IntMap a) -> 𝑉 a -> ℕ
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝑉 a -> IntMap a
forall a. 𝑉 a -> IntMap a
un𝑉

(⊎♮) ∷ (Additive a) ⇒ 𝑉 a → 𝑉 a → 𝑉 a
⊎♮ :: forall a. Additive a => 𝑉 a -> 𝑉 a -> 𝑉 a
(⊎♮) = (a -> a -> a) -> 𝑉 a -> 𝑉 a -> 𝑉 a
forall a. (a -> a -> a) -> 𝑉 a -> 𝑉 a -> 𝑉 a
unionWith𝑉 a -> a -> a
forall a. Plus a => a -> a -> a
(+)

unionsWith𝑉 ∷ (ToIter (𝑉 a) t) ⇒ (a → a → a) → t → 𝑉 a
unionsWith𝑉 :: forall a t. ToIter (𝑉 a) t => (a -> a -> a) -> t -> 𝑉 a
unionsWith𝑉 = 𝑉 a -> (𝑉 a -> 𝑉 a -> 𝑉 a) -> t -> 𝑉 a
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
fold 𝑉 a
forall a. 𝑉 a
wø ((𝑉 a -> 𝑉 a -> 𝑉 a) -> t -> 𝑉 a)
-> ((a -> a -> a) -> 𝑉 a -> 𝑉 a -> 𝑉 a)
-> (a -> a -> a)
-> t
-> 𝑉 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (a -> a -> a) -> 𝑉 a -> 𝑉 a -> 𝑉 a
forall a. (a -> a -> a) -> 𝑉 a -> 𝑉 a -> 𝑉 a
unionWith𝑉
 
interWith𝑉 ∷ (a → b → c) → 𝑉 a → 𝑉 b → 𝑉 c
interWith𝑉 :: forall a b c. (a -> b -> c) -> 𝑉 a -> 𝑉 b -> 𝑉 c
interWith𝑉 a -> b -> c
f 𝑉 a
ixs₁ 𝑉 b
ixs₂ = IntMap c -> 𝑉 c
forall a. IntMap a -> 𝑉 a
𝑉 (IntMap c -> 𝑉 c) -> IntMap c -> 𝑉 c
forall a b. (a -> b) -> a -> b
$ (a -> b -> c) -> IntMap a -> IntMap b -> IntMap c
forall a b c. (a -> b -> c) -> IntMap a -> IntMap b -> IntMap c
IntMap.intersectionWith a -> b -> c
f (𝑉 a -> IntMap a
forall a. 𝑉 a -> IntMap a
un𝑉 𝑉 a
ixs₁) (𝑉 b -> IntMap b
forall a. 𝑉 a -> IntMap a
un𝑉 𝑉 b
ixs₂)

-- -- diffWith ∷ (v → v → v) → 𝑉 a → 𝑉 a → 𝑉 a
-- -- diffWith f ixs₁ ixs₂ = 𝑉 $ IntMap.differenceWith (\ x y → HS.Just (f x y)) (un𝑉 ixs₁) (un𝑉 ixs₂)

minView𝑉 ∷ 𝑉 a → 𝑂 (ℤ64 ∧ a ∧ (𝑉 a))
minView𝑉 :: forall a. 𝑉 a -> 𝑂 ((ℤ64 ∧ a) ∧ 𝑉 a)
minView𝑉 = (((ℤ64 ∧ a) ∧ IntMap a) -> (ℤ64 ∧ a) ∧ 𝑉 a)
-> 𝑂 ((ℤ64 ∧ a) ∧ IntMap a) -> 𝑂 ((ℤ64 ∧ a) ∧ 𝑉 a)
forall a b. (a -> b) -> 𝑂 a -> 𝑂 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((IntMap a -> 𝑉 a) -> ((ℤ64 ∧ a) ∧ IntMap a) -> (ℤ64 ∧ a) ∧ 𝑉 a
forall b₁ b₂ a. (b₁ -> b₂) -> (a ∧ b₁) -> a ∧ b₂
mapSnd IntMap a -> 𝑉 a
forall a. IntMap a -> 𝑉 a
𝑉) (𝑂 ((ℤ64 ∧ a) ∧ IntMap a) -> 𝑂 ((ℤ64 ∧ a) ∧ 𝑉 a))
-> (Maybe ((Int, a), IntMap a) -> 𝑂 ((ℤ64 ∧ a) ∧ IntMap a))
-> Maybe ((Int, a), IntMap a)
-> 𝑂 ((ℤ64 ∧ a) ∧ 𝑉 a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Maybe ((Int, a), IntMap a) -> 𝑂 ((ℤ64 ∧ a) ∧ IntMap a)
forall a b. CHS a b => b -> a
frhs (Maybe ((Int, a), IntMap a) -> 𝑂 ((ℤ64 ∧ a) ∧ 𝑉 a))
-> (IntMap a -> Maybe ((Int, a), IntMap a))
-> IntMap a
-> 𝑂 ((ℤ64 ∧ a) ∧ 𝑉 a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ IntMap a -> Maybe ((Int, a), IntMap a)
forall a. IntMap a -> Maybe ((Int, a), IntMap a)
IntMap.minViewWithKey (IntMap a -> 𝑂 ((ℤ64 ∧ a) ∧ 𝑉 a))
-> (𝑉 a -> IntMap a) -> 𝑉 a -> 𝑂 ((ℤ64 ∧ a) ∧ 𝑉 a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝑉 a -> IntMap a
forall a. 𝑉 a -> IntMap a
un𝑉

maxView𝑉 ∷ 𝑉 a → 𝑂 (ℤ64 ∧ a ∧ (𝑉 a))
maxView𝑉 :: forall a. 𝑉 a -> 𝑂 ((ℤ64 ∧ a) ∧ 𝑉 a)
maxView𝑉 = (((ℤ64 ∧ a) ∧ IntMap a) -> (ℤ64 ∧ a) ∧ 𝑉 a)
-> 𝑂 ((ℤ64 ∧ a) ∧ IntMap a) -> 𝑂 ((ℤ64 ∧ a) ∧ 𝑉 a)
forall a b. (a -> b) -> 𝑂 a -> 𝑂 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((IntMap a -> 𝑉 a) -> ((ℤ64 ∧ a) ∧ IntMap a) -> (ℤ64 ∧ a) ∧ 𝑉 a
forall b₁ b₂ a. (b₁ -> b₂) -> (a ∧ b₁) -> a ∧ b₂
mapSnd IntMap a -> 𝑉 a
forall a. IntMap a -> 𝑉 a
𝑉) (𝑂 ((ℤ64 ∧ a) ∧ IntMap a) -> 𝑂 ((ℤ64 ∧ a) ∧ 𝑉 a))
-> (Maybe ((Int, a), IntMap a) -> 𝑂 ((ℤ64 ∧ a) ∧ IntMap a))
-> Maybe ((Int, a), IntMap a)
-> 𝑂 ((ℤ64 ∧ a) ∧ 𝑉 a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Maybe ((Int, a), IntMap a) -> 𝑂 ((ℤ64 ∧ a) ∧ IntMap a)
forall a b. CHS a b => b -> a
frhs (Maybe ((Int, a), IntMap a) -> 𝑂 ((ℤ64 ∧ a) ∧ 𝑉 a))
-> (IntMap a -> Maybe ((Int, a), IntMap a))
-> IntMap a
-> 𝑂 ((ℤ64 ∧ a) ∧ 𝑉 a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ IntMap a -> Maybe ((Int, a), IntMap a)
forall a. IntMap a -> Maybe ((Int, a), IntMap a)
IntMap.maxViewWithKey (IntMap a -> 𝑂 ((ℤ64 ∧ a) ∧ 𝑉 a))
-> (𝑉 a -> IntMap a) -> 𝑉 a -> 𝑂 ((ℤ64 ∧ a) ∧ 𝑉 a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝑉 a -> IntMap a
forall a. 𝑉 a -> IntMap a
un𝑉

minKey𝑉 ∷ 𝑉 a → 𝑂 ℤ64
minKey𝑉 :: forall a. 𝑉 a -> 𝑂 ℤ64
minKey𝑉 𝑉 a
ixs = (ℤ64 ∧ a) -> ℤ64
forall a b. (a ∧ b) -> a
fst ((ℤ64 ∧ a) -> ℤ64)
-> (((ℤ64 ∧ a) ∧ 𝑉 a) -> ℤ64 ∧ a) -> ((ℤ64 ∧ a) ∧ 𝑉 a) -> ℤ64
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((ℤ64 ∧ a) ∧ 𝑉 a) -> ℤ64 ∧ a
forall a b. (a ∧ b) -> a
fst (((ℤ64 ∧ a) ∧ 𝑉 a) -> ℤ64) -> 𝑂 ((ℤ64 ∧ a) ∧ 𝑉 a) -> 𝑂 ℤ64
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ 𝑉 a -> 𝑂 ((ℤ64 ∧ a) ∧ 𝑉 a)
forall a. 𝑉 a -> 𝑂 ((ℤ64 ∧ a) ∧ 𝑉 a)
minView𝑉 𝑉 a
ixs

maxKey𝑉 ∷ 𝑉 a → 𝑂 ℤ64
maxKey𝑉 :: forall a. 𝑉 a -> 𝑂 ℤ64
maxKey𝑉 𝑉 a
ixs = (ℤ64 ∧ a) -> ℤ64
forall a b. (a ∧ b) -> a
fst ((ℤ64 ∧ a) -> ℤ64)
-> (((ℤ64 ∧ a) ∧ 𝑉 a) -> ℤ64 ∧ a) -> ((ℤ64 ∧ a) ∧ 𝑉 a) -> ℤ64
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((ℤ64 ∧ a) ∧ 𝑉 a) -> ℤ64 ∧ a
forall a b. (a ∧ b) -> a
fst (((ℤ64 ∧ a) ∧ 𝑉 a) -> ℤ64) -> 𝑂 ((ℤ64 ∧ a) ∧ 𝑉 a) -> 𝑂 ℤ64
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ 𝑉 a -> 𝑂 ((ℤ64 ∧ a) ∧ 𝑉 a)
forall a. 𝑉 a -> 𝑂 ((ℤ64 ∧ a) ∧ 𝑉 a)
maxView𝑉 𝑉 a
ixs

view𝑉 ∷ ℤ64 → 𝑉 a → 𝑂 (a ∧ (𝑉 a))
view𝑉 :: forall a. ℤ64 -> 𝑉 a -> 𝑂 (a ∧ 𝑉 a)
view𝑉 ℤ64
i 𝑉 a
ixs
  | ℤ64
i ℤ64 -> 𝑉 a -> Bool
forall a. ℤ64 -> 𝑉 a -> Bool
⋵♮ 𝑉 a
ixs = (a ∧ 𝑉 a) -> 𝑂 (a ∧ 𝑉 a)
forall a. a -> 𝑂 a
Some ((a ∧ 𝑉 a) -> 𝑂 (a ∧ 𝑉 a)) -> (a ∧ 𝑉 a) -> 𝑂 (a ∧ 𝑉 a)
forall a b. (a -> b) -> a -> b
$ (𝑉 a
ixs 𝑉 a -> ℤ64 -> a
forall k v t. (Lookup k v t, STACK) => t -> k -> v
⋕! ℤ64
i) a -> 𝑉 a -> a ∧ 𝑉 a
forall a b. a -> b -> a ∧ b
:* ℤ64 -> 𝑉 a -> 𝑉 a
forall a. ℤ64 -> 𝑉 a -> 𝑉 a
delete𝑉 ℤ64
i 𝑉 a
ixs
  | Bool
otherwise = 𝑂 (a ∧ 𝑉 a)
forall a. 𝑂 a
None

without𝑉 ∷ 𝑃 ℤ64 → 𝑉 a → 𝑉 a
without𝑉 :: forall a. 𝑃 ℤ64 -> 𝑉 a -> 𝑉 a
without𝑉 𝑃 ℤ64
is 𝑉 a
ixs = IntMap a -> 𝑉 a
forall a. IntMap a -> 𝑉 a
𝑉 (IntMap a -> 𝑉 a) -> IntMap a -> 𝑉 a
forall a b. (a -> b) -> a -> b
$ IntMap a -> IntSet -> IntMap a
forall a. IntMap a -> IntSet -> IntMap a
IntMap.withoutKeys (𝑉 a -> IntMap a
forall a. 𝑉 a -> IntMap a
un𝑉 𝑉 a
ixs) (IntSet -> IntMap a) -> IntSet -> IntMap a
forall a b. (a -> b) -> a -> b
$ [Int] -> IntSet
IntSet.fromList ([Int] -> IntSet) -> [Int] -> IntSet
forall a b. (a -> b) -> a -> b
$ 𝐼 Int -> [Int]
forall a t. ToIter a t => t -> [a]
lazyList (𝐼 Int -> [Int]) -> 𝐼 Int -> [Int]
forall a b. (a -> b) -> a -> b
$ (ℤ64 -> Int) -> 𝐼 ℤ64 -> 𝐼 Int
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ℤ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 t. ToIter a t => t -> 𝐼 a
iter 𝑃 ℤ64
is

restrict𝑉 ∷ 𝑃 ℤ64 → 𝑉 a → 𝑉 a
restrict𝑉 :: forall a. 𝑃 ℤ64 -> 𝑉 a -> 𝑉 a
restrict𝑉 𝑃 ℤ64
is 𝑉 a
ixs = IntMap a -> 𝑉 a
forall a. IntMap a -> 𝑉 a
𝑉 (IntMap a -> 𝑉 a) -> IntMap a -> 𝑉 a
forall a b. (a -> b) -> a -> b
$ IntMap a -> IntSet -> IntMap a
forall a. IntMap a -> IntSet -> IntMap a
IntMap.restrictKeys (𝑉 a -> IntMap a
forall a. 𝑉 a -> IntMap a
un𝑉 𝑉 a
ixs) (IntSet -> IntMap a) -> IntSet -> IntMap a
forall a b. (a -> b) -> a -> b
$ [Int] -> IntSet
IntSet.fromList ([Int] -> IntSet) -> [Int] -> IntSet
forall a b. (a -> b) -> a -> b
$ 𝐼 Int -> [Int]
forall a t. ToIter a t => t -> [a]
lazyList (𝐼 Int -> [Int]) -> 𝐼 Int -> [Int]
forall a b. (a -> b) -> a -> b
$ (ℤ64 -> Int) -> 𝐼 ℤ64 -> 𝐼 Int
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ℤ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 t. ToIter a t => t -> 𝐼 a
iter 𝑃 ℤ64
is

keys𝑉 ∷ 𝑉 a → 𝐼 ℤ64
keys𝑉 :: forall a. 𝑉 a -> 𝐼 ℤ64
keys𝑉 = (Int -> ℤ64) -> 𝐼 Int -> 𝐼 ℤ64
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map Int -> ℤ64
forall a b. CHS a b => b -> a
frhs (𝐼 Int -> 𝐼 ℤ64) -> ([Int] -> 𝐼 Int) -> [Int] -> 𝐼 ℤ64
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ [Int] -> 𝐼 Int
forall a t. ToIter a t => t -> 𝐼 a
iter ([Int] -> 𝐼 ℤ64) -> (IntMap a -> [Int]) -> IntMap a -> 𝐼 ℤ64
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ IntMap a -> [Int]
forall a. IntMap a -> [Int]
IntMap.keys (IntMap a -> 𝐼 ℤ64) -> (𝑉 a -> IntMap a) -> 𝑉 a -> 𝐼 ℤ64
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝑉 a -> IntMap a
forall a. 𝑉 a -> IntMap a
un𝑉

values𝑉 ∷ 𝑉 a → 𝐼 a
values𝑉 :: forall a. 𝑉 a -> 𝐼 a
values𝑉 = (a -> a) -> 𝐼 a -> 𝐼 a
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> a
forall a b. CHS a b => b -> a
frhs (𝐼 a -> 𝐼 a) -> ([a] -> 𝐼 a) -> [a] -> 𝐼 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ [a] -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter ([a] -> 𝐼 a) -> (IntMap a -> [a]) -> IntMap a -> 𝐼 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ IntMap a -> [a]
forall a. IntMap a -> [a]
IntMap.elems (IntMap a -> 𝐼 a) -> (𝑉 a -> IntMap a) -> 𝑉 a -> 𝐼 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝑉 a -> IntMap a
forall a. 𝑉 a -> IntMap a
un𝑉

map𝑉 ∷ (a → b) → 𝑉 a → 𝑉 b
map𝑉 :: forall a b. (a -> b) -> 𝑉 a -> 𝑉 b
map𝑉 a -> b
f = IntMap b -> 𝑉 b
forall a. IntMap a -> 𝑉 a
𝑉 (IntMap b -> 𝑉 b) -> (IntMap a -> IntMap b) -> IntMap a -> 𝑉 b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (a -> b) -> IntMap a -> IntMap b
forall a b. (a -> b) -> IntMap a -> IntMap b
IntMap.map a -> b
f (IntMap a -> 𝑉 b) -> (𝑉 a -> IntMap a) -> 𝑉 a -> 𝑉 b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝑉 a -> IntMap a
forall a. 𝑉 a -> IntMap a
un𝑉

mapK𝑉 ∷ (ℤ64 → a → b) → 𝑉 a → 𝑉 b
mapK𝑉 :: forall a b. (ℤ64 -> a -> b) -> 𝑉 a -> 𝑉 b
mapK𝑉 ℤ64 -> a -> b
f 𝑉 a
ixs = 𝐼 (𝑉 b) -> 𝑉 b
forall a t. ToIter (𝑉 a) t => t -> 𝑉 a
spvec (𝐼 (𝑉 b) -> 𝑉 b) -> 𝐼 (𝑉 b) -> 𝑉 b
forall a b. (a -> b) -> a -> b
$ 𝐼 (ℤ64 ∧ a) -> ((ℤ64 ∧ a) -> 𝑉 b) -> 𝐼 (𝑉 b)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (𝑉 a -> 𝐼 (ℤ64 ∧ a)
forall a t. ToIter a t => t -> 𝐼 a
iter 𝑉 a
ixs) (((ℤ64 ∧ a) -> 𝑉 b) -> 𝐼 (𝑉 b)) -> ((ℤ64 ∧ a) -> 𝑉 b) -> 𝐼 (𝑉 b)
forall a b. (a -> b) -> a -> b
$ \ (ℤ64
i :* a
x) → ℤ64
i ℤ64 -> b -> 𝑉 b
forall a. ℤ64 -> a -> 𝑉 a
↦♮ ℤ64 -> a -> b
f ℤ64
i a
x

iter𝑉 ∷ 𝑉 a → 𝐼 (ℤ64 ∧ a)
iter𝑉 :: forall a. 𝑉 a -> 𝐼 (ℤ64 ∧ a)
iter𝑉 = ((Int, a) -> ℤ64 ∧ a) -> 𝐼 (Int, a) -> 𝐼 (ℤ64 ∧ a)
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (Int, a) -> ℤ64 ∧ a
forall a b. CHS a b => b -> a
frhs (𝐼 (Int, a) -> 𝐼 (ℤ64 ∧ a))
-> ([(Int, a)] -> 𝐼 (Int, a)) -> [(Int, a)] -> 𝐼 (ℤ64 ∧ a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ [(Int, a)] -> 𝐼 (Int, a)
forall a. [a] -> 𝐼 a
iterLL ([(Int, a)] -> 𝐼 (ℤ64 ∧ a))
-> (IntMap a -> [(Int, a)]) -> IntMap a -> 𝐼 (ℤ64 ∧ a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ IntMap a -> [(Int, a)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList (IntMap a -> 𝐼 (ℤ64 ∧ a))
-> (𝑉 a -> IntMap a) -> 𝑉 a -> 𝐼 (ℤ64 ∧ a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝑉 a -> IntMap a
forall a. 𝑉 a -> IntMap a
un𝑉

spvec𝐼 ∷ 𝐼 (ℤ64 ∧ a) → 𝑉 a
spvec𝐼 :: forall a. 𝐼 (ℤ64 ∧ a) -> 𝑉 a
spvec𝐼 = IntMap a -> 𝑉 a
forall a. IntMap a -> 𝑉 a
𝑉 (IntMap a -> 𝑉 a) -> ([(Int, a)] -> IntMap a) -> [(Int, a)] -> 𝑉 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ [(Int, a)] -> IntMap a
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, a)] -> 𝑉 a)
-> (𝐼 (Int, a) -> [(Int, a)]) -> 𝐼 (Int, a) -> 𝑉 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐼 (Int, a) -> [(Int, a)]
forall a t. ToIter a t => t -> [a]
lazyList (𝐼 (Int, a) -> 𝑉 a)
-> (𝐼 (ℤ64 ∧ a) -> 𝐼 (Int, a)) -> 𝐼 (ℤ64 ∧ a) -> 𝑉 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((ℤ64 ∧ a) -> (Int, a)) -> 𝐼 (ℤ64 ∧ a) -> 𝐼 (Int, a)
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (ℤ64 ∧ a) -> (Int, a)
forall a b. CHS a b => a -> b
tohs

spvec ∷ (ToIter (𝑉 a) t) ⇒ t → 𝑉 a
spvec :: forall a t. ToIter (𝑉 a) t => t -> 𝑉 a
spvec = 𝑉 a -> (𝑉 a -> 𝑉 a -> 𝑉 a) -> 𝐼 (𝑉 a) -> 𝑉 a
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
foldr 𝑉 a
forall a. 𝑉 a
wø 𝑉 a -> 𝑉 a -> 𝑉 a
forall a. 𝑉 a -> 𝑉 a -> 𝑉 a
(⩌♮) (𝐼 (𝑉 a) -> 𝑉 a) -> (t -> 𝐼 (𝑉 a)) -> t -> 𝑉 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ t -> 𝐼 (𝑉 a)
forall a t. ToIter a t => t -> 𝐼 a
iter
 
assoc𝑉 ∷ (ToIter (ℤ64 ∧ a) t) ⇒ t → 𝑉 a
assoc𝑉 :: forall a t. ToIter (ℤ64 ∧ a) t => t -> 𝑉 a
assoc𝑉 = 𝐼 (𝑉 a) -> 𝑉 a
forall a t. ToIter (𝑉 a) t => t -> 𝑉 a
spvec (𝐼 (𝑉 a) -> 𝑉 a) -> (𝐼 (ℤ64 ∧ a) -> 𝐼 (𝑉 a)) -> 𝐼 (ℤ64 ∧ a) -> 𝑉 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ ((ℤ64 ∧ a) -> 𝑉 a) -> 𝐼 (ℤ64 ∧ a) -> 𝐼 (𝑉 a)
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (ℤ64 ∧ a) -> 𝑉 a
forall a t. Single a t => a -> t
single (𝐼 (ℤ64 ∧ a) -> 𝑉 a) -> (t -> 𝐼 (ℤ64 ∧ a)) -> t -> 𝑉 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ t -> 𝐼 (ℤ64 ∧ a)
forall a t. ToIter a t => t -> 𝐼 a
iter

join𝑉 ∷ (Ord a,Ord b) ⇒ 𝑉 (𝑃 a) → 𝑉 (𝑃 b) → 𝑉 (𝑃 (a ∧ b))
join𝑉 :: forall a b. (Ord a, Ord b) => 𝑉 (𝑃 a) -> 𝑉 (𝑃 b) -> 𝑉 (𝑃 (a ∧ b))
join𝑉 = (𝑃 a -> 𝑃 b -> 𝑃 (a ∧ b)) -> 𝑉 (𝑃 a) -> 𝑉 (𝑃 b) -> 𝑉 (𝑃 (a ∧ b))
forall a b c. (a -> b -> c) -> 𝑉 a -> 𝑉 b -> 𝑉 c
interWith𝑉 ((𝑃 a -> 𝑃 b -> 𝑃 (a ∧ b)) -> 𝑉 (𝑃 a) -> 𝑉 (𝑃 b) -> 𝑉 (𝑃 (a ∧ b)))
-> (𝑃 a -> 𝑃 b -> 𝑃 (a ∧ b)) -> 𝑉 (𝑃 a) -> 𝑉 (𝑃 b) -> 𝑉 (𝑃 (a ∧ b))
forall a b. (a -> b) -> a -> b
$ \ 𝑃 a
vs₁ 𝑃 b
vs₂ → 𝐼 (a ∧ b) -> 𝑃 (a ∧ b)
forall a. Ord a => 𝐼 a -> 𝑃 a
pow𝐼𝑃 (𝐼 (a ∧ b) -> 𝑃 (a ∧ b)) -> 𝐼 (a ∧ b) -> 𝑃 (a ∧ b)
forall a b. (a -> b) -> a -> b
$ 𝐼 (a ∧ b) -> 𝐼 (a ∧ b)
forall a t. ToIter a t => t -> 𝐼 a
iter (𝐼 (a ∧ b) -> 𝐼 (a ∧ b)) -> 𝐼 (a ∧ b) -> 𝐼 (a ∧ b)
forall a b. (a -> b) -> a -> b
$ (a -> b -> a ∧ b) -> 𝑃 a -> 𝑃 b -> 𝐼 (a ∧ b)
forall a t₁ b t₂ c.
(ToIter a t₁, ToIter b t₂) =>
(a -> b -> c) -> t₁ -> t₂ -> 𝐼 c
zipWith a -> b -> a ∧ b
forall a b. a -> b -> a ∧ b
(:*) 𝑃 a
vs₁ 𝑃 b
vs₂