module UVMHS.Core.Sized where

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

import UVMHS.Core.LensDeriving

instance CSized 𝕊 where csize :: 𝕊 -> ℕ64
csize = ℕ -> ℕ64
forall a. (ToNatO64 a, STACK) => a -> ℕ64
natΩ64 (ℕ -> ℕ64) -> (𝕊 -> ℕ) -> 𝕊 -> ℕ64
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝕊 -> ℕ
length𝕊

---------
-- 𝐼A --
---------

data 𝐼A a = 𝐼A
  { forall a. 𝐼A a -> ℕ64
𝑖aSize ∷ ℕ64
  , forall a. 𝐼A a -> 𝐼 a
𝑖aIter ∷ 𝐼 a
  } deriving (Int -> 𝐼A a -> ShowS
[𝐼A a] -> ShowS
𝐼A a -> String
(Int -> 𝐼A a -> ShowS)
-> (𝐼A a -> String) -> ([𝐼A a] -> ShowS) -> Show (𝐼A a)
forall a. Show a => Int -> 𝐼A a -> ShowS
forall a. Show a => [𝐼A a] -> ShowS
forall a. Show a => 𝐼A a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> 𝐼A a -> ShowS
showsPrec :: Int -> 𝐼A a -> ShowS
$cshow :: forall a. Show a => 𝐼A a -> String
show :: 𝐼A a -> String
$cshowList :: forall a. Show a => [𝐼A a] -> ShowS
showList :: [𝐼A a] -> ShowS
Show)
makeLenses ''𝐼A

class ToIterA a t | t → a where iterA ∷ t → 𝐼A a
instance ToIterA a (𝐼A a) where iterA :: 𝐼A a -> 𝐼A a
iterA = 𝐼A a -> 𝐼A a
forall a. a -> a
id

instance Null   (𝐼A a) where null :: 𝐼A a
null                  = ℕ64 -> 𝐼 a -> 𝐼A a
forall a. ℕ64 -> 𝐼 a -> 𝐼A a
𝐼A ℕ64
forall a. Zero a => a
zero 𝐼 a
forall a. Null a => a
null
instance Append (𝐼A a) where 𝐼A ℕ64
a₁ 𝐼 a
xs₁ ⧺ :: 𝐼A a -> 𝐼A a -> 𝐼A a
⧺ 𝐼A ℕ64
a₂ 𝐼 a
xs₂ = ℕ64 -> 𝐼 a -> 𝐼A a
forall a. ℕ64 -> 𝐼 a -> 𝐼A a
𝐼A (ℕ64
a₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
a₂) (𝐼 a -> 𝐼A a) -> 𝐼 a -> 𝐼A a
forall a b. (a -> b) -> a -> b
$ 𝐼 a
xs₁ 𝐼 a -> 𝐼 a -> 𝐼 a
forall a. Append a => a -> a -> a
⧺ 𝐼 a
xs₂
instance Monoid (𝐼A a)

instance              ToIter a (𝐼A a) where iter :: 𝐼A a -> 𝐼 a
iter     = 𝐼A a -> 𝐼 a
forall a. 𝐼A a -> 𝐼 a
𝑖aIter
instance (ASized a) ⇒ Single a (𝐼A a) where single :: a -> 𝐼A a
single a
s = ℕ64 -> 𝐼 a -> 𝐼A a
forall a. ℕ64 -> 𝐼 a -> 𝐼A a
𝐼A (a -> ℕ64
forall a. ASized a => a -> ℕ64
asize a
s) (𝐼 a -> 𝐼A a) -> 𝐼 a -> 𝐼A a
forall a b. (a -> b) -> a -> b
$ a -> 𝐼 a
forall a t. Single a t => a -> t
single a
s
instance              ASized   (𝐼A a) where asize :: 𝐼A a -> ℕ64
asize    = 𝐼A a -> ℕ64
forall a. 𝐼A a -> ℕ64
𝑖aSize

instance FunctorM 𝐼C where mapM :: forall (m :: * -> *) a b. Monad m => (a -> m b) -> 𝐼C a -> m (𝐼C b)
mapM a -> m b
f (𝐼C ℕ64
n 𝐼 a
xs) = ℕ64 -> 𝐼 b -> 𝐼C b
forall a. ℕ64 -> 𝐼 a -> 𝐼C a
𝐼C ℕ64
n (𝐼 b -> 𝐼C b) -> m (𝐼 b) -> m (𝐼C b)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ (a -> m b) -> 𝐼 a -> m (𝐼 b)
forall (t :: * -> *) (m :: * -> *) a b.
(FunctorM t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> 𝐼 a -> m (𝐼 b)
mapM a -> m b
f 𝐼 a
xs

iterAI ∷ (ToIter a t,ASized a) ⇒ t → 𝐼A a
iterAI :: forall a t. (ToIter a t, ASized a) => t -> 𝐼A a
iterAI t
xs = ℕ64 -> 𝐼 a -> 𝐼A a
forall a. ℕ64 -> 𝐼 a -> 𝐼A a
𝐼A (𝐼 ℕ64 -> ℕ64
forall a t. (ToIter a t, Additive a) => t -> a
sum (𝐼 ℕ64 -> ℕ64) -> 𝐼 ℕ64 -> ℕ64
forall a b. (a -> b) -> a -> b
$ (a -> ℕ64) -> 𝐼 a -> 𝐼 ℕ64
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> ℕ64
forall a. ASized a => a -> ℕ64
asize (𝐼 a -> 𝐼 ℕ64) -> 𝐼 a -> 𝐼 ℕ64
forall a b. (a -> b) -> a -> b
$ t -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter t
xs) (𝐼 a -> 𝐼A a) -> 𝐼 a -> 𝐼A a
forall a b. (a -> b) -> a -> b
$ t -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter t
xs

--------
-- 𝐼C --
--------

data 𝐼C a = 𝐼C
  { forall a. 𝐼C a -> ℕ64
𝑖cSize ∷ ℕ64
  , forall a. 𝐼C a -> 𝐼 a
𝑖cIter ∷ 𝐼 a
  } deriving (Int -> 𝐼C a -> ShowS
[𝐼C a] -> ShowS
𝐼C a -> String
(Int -> 𝐼C a -> ShowS)
-> (𝐼C a -> String) -> ([𝐼C a] -> ShowS) -> Show (𝐼C a)
forall a. Show a => Int -> 𝐼C a -> ShowS
forall a. Show a => [𝐼C a] -> ShowS
forall a. Show a => 𝐼C a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> 𝐼C a -> ShowS
showsPrec :: Int -> 𝐼C a -> ShowS
$cshow :: forall a. Show a => 𝐼C a -> String
show :: 𝐼C a -> String
$cshowList :: forall a. Show a => [𝐼C a] -> ShowS
showList :: [𝐼C a] -> ShowS
Show)
makeLenses ''𝐼C

class ToIterC a t | t → a where iterC ∷ t → 𝐼C a
instance ToIterC a (𝐼C a) where iterC :: 𝐼C a -> 𝐼C a
iterC = 𝐼C a -> 𝐼C a
forall a. a -> a
id

instance Null   (𝐼C a) where null :: 𝐼C a
null                  = ℕ64 -> 𝐼 a -> 𝐼C a
forall a. ℕ64 -> 𝐼 a -> 𝐼C a
𝐼C ℕ64
forall a. Zero a => a
zero 𝐼 a
forall a. Null a => a
null
instance Append (𝐼C a) where 𝐼C ℕ64
c₁ 𝐼 a
xs₁ ⧺ :: 𝐼C a -> 𝐼C a -> 𝐼C a
⧺ 𝐼C ℕ64
c₂ 𝐼 a
xs₂ = ℕ64 -> 𝐼 a -> 𝐼C a
forall a. ℕ64 -> 𝐼 a -> 𝐼C a
𝐼C (ℕ64
c₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
c₂) (𝐼 a
xs₁ 𝐼 a -> 𝐼 a -> 𝐼 a
forall a. Append a => a -> a -> a
⧺ 𝐼 a
xs₂)
instance Monoid (𝐼C a)

instance ToIter a (𝐼C a) where iter :: 𝐼C a -> 𝐼 a
iter   = 𝐼C a -> 𝐼 a
forall a. 𝐼C a -> 𝐼 a
𝑖cIter
instance Single a (𝐼C a) where single :: a -> 𝐼C a
single = ℕ64 -> 𝐼 a -> 𝐼C a
forall a. ℕ64 -> 𝐼 a -> 𝐼C a
𝐼C ℕ64
forall a. One a => a
one (𝐼 a -> 𝐼C a) -> (a -> 𝐼 a) -> a -> 𝐼C a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> 𝐼 a
forall a t. Single a t => a -> t
single
instance CSized   (𝐼C a) where csize :: 𝐼C a -> ℕ64
csize  = 𝐼C a -> ℕ64
forall a. 𝐼C a -> ℕ64
𝑖cSize

instance Functor 𝐼C where map :: forall a b. (a -> b) -> 𝐼C a -> 𝐼C b
map a -> b
f (𝐼C ℕ64
c 𝐼 a
xs) = ℕ64 -> 𝐼 b -> 𝐼C b
forall a. ℕ64 -> 𝐼 a -> 𝐼C a
𝐼C ℕ64
c (𝐼 b -> 𝐼C b) -> 𝐼 b -> 𝐼C b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> 𝐼 a -> 𝐼 b
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> b
f 𝐼 a
xs

iterCI ∷ (ToIter a t) ⇒ t → 𝐼C a
iterCI :: forall a t. ToIter a t => t -> 𝐼C a
iterCI t
xs = ℕ64 -> 𝐼 a -> 𝐼C a
forall a. ℕ64 -> 𝐼 a -> 𝐼C a
𝐼C (t -> ℕ64
forall n t a. (Zero n, One n, Plus n, ToIter a t) => t -> n
count t
xs) (𝐼 a -> 𝐼C a) -> 𝐼 a -> 𝐼C a
forall a b. (a -> b) -> a -> b
$ t -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter t
xs

---------
-- 𝐼AC --
---------

data 𝐼AC a = 𝐼AC
  { forall a. 𝐼AC a -> ℕ64
𝑖acSize ∷ ℕ64
  , forall a. 𝐼AC a -> ℕ64
𝑖acCSize ∷ ℕ64
  , forall a. 𝐼AC a -> 𝐼 a
𝑖acIter ∷ 𝐼 a
  } deriving (Int -> 𝐼AC a -> ShowS
[𝐼AC a] -> ShowS
𝐼AC a -> String
(Int -> 𝐼AC a -> ShowS)
-> (𝐼AC a -> String) -> ([𝐼AC a] -> ShowS) -> Show (𝐼AC a)
forall a. Show a => Int -> 𝐼AC a -> ShowS
forall a. Show a => [𝐼AC a] -> ShowS
forall a. Show a => 𝐼AC a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> 𝐼AC a -> ShowS
showsPrec :: Int -> 𝐼AC a -> ShowS
$cshow :: forall a. Show a => 𝐼AC a -> String
show :: 𝐼AC a -> String
$cshowList :: forall a. Show a => [𝐼AC a] -> ShowS
showList :: [𝐼AC a] -> ShowS
Show)
makeLenses ''𝐼AC

class ToIterAC a t | t → a where iterAC ∷ t → 𝐼AC a
instance ToIterAC a (𝐼AC a) where iterAC :: 𝐼AC a -> 𝐼AC a
iterAC = 𝐼AC a -> 𝐼AC a
forall a. a -> a
id

instance Null   (𝐼AC a) where null :: 𝐼AC a
null                          = ℕ64 -> ℕ64 -> 𝐼 a -> 𝐼AC a
forall a. ℕ64 -> ℕ64 -> 𝐼 a -> 𝐼AC a
𝐼AC ℕ64
forall a. Zero a => a
zero ℕ64
forall a. Zero a => a
zero 𝐼 a
forall a. Null a => a
null
instance Append (𝐼AC a) where 𝐼AC ℕ64
c₁ ℕ64
a₁ 𝐼 a
xs₁ ⧺ :: 𝐼AC a -> 𝐼AC a -> 𝐼AC a
⧺ 𝐼AC ℕ64
c₂ ℕ64
a₂ 𝐼 a
xs₂ = ℕ64 -> ℕ64 -> 𝐼 a -> 𝐼AC a
forall a. ℕ64 -> ℕ64 -> 𝐼 a -> 𝐼AC a
𝐼AC (ℕ64
c₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
c₂) (ℕ64
a₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
a₂) (𝐼 a
xs₁ 𝐼 a -> 𝐼 a -> 𝐼 a
forall a. Append a => a -> a -> a
⧺ 𝐼 a
xs₂)
instance Monoid (𝐼AC a)

instance              ToIter a (𝐼AC a) where iter :: 𝐼AC a -> 𝐼 a
iter     = 𝐼AC a -> 𝐼 a
forall a. 𝐼AC a -> 𝐼 a
𝑖acIter
instance (ASized a) ⇒ Single a (𝐼AC a) where single :: a -> 𝐼AC a
single a
s = ℕ64 -> ℕ64 -> 𝐼 a -> 𝐼AC a
forall a. ℕ64 -> ℕ64 -> 𝐼 a -> 𝐼AC a
𝐼AC ℕ64
forall a. One a => a
one (a -> ℕ64
forall a. ASized a => a -> ℕ64
asize a
s) (𝐼 a -> 𝐼AC a) -> 𝐼 a -> 𝐼AC a
forall a b. (a -> b) -> a -> b
$ a -> 𝐼 a
forall a t. Single a t => a -> t
single a
s
instance              ASized   (𝐼AC a) where asize :: 𝐼AC a -> ℕ64
asize    = 𝐼AC a -> ℕ64
forall a. 𝐼AC a -> ℕ64
𝑖acSize
instance              CSized   (𝐼AC a) where csize :: 𝐼AC a -> ℕ64
csize    = 𝐼AC a -> ℕ64
forall a. 𝐼AC a -> ℕ64
𝑖acCSize

iterACI ∷ (ToIter a t,ASized a) ⇒ t → 𝐼AC a
iterACI :: forall a t. (ToIter a t, ASized a) => t -> 𝐼AC a
iterACI t
xs = ℕ64 -> ℕ64 -> 𝐼 a -> 𝐼AC a
forall a. ℕ64 -> ℕ64 -> 𝐼 a -> 𝐼AC a
𝐼AC (t -> ℕ64
forall n t a. (Zero n, One n, Plus n, ToIter a t) => t -> n
count t
xs) (𝐼 ℕ64 -> ℕ64
forall a t. (ToIter a t, Additive a) => t -> a
sum (𝐼 ℕ64 -> ℕ64) -> 𝐼 ℕ64 -> ℕ64
forall a b. (a -> b) -> a -> b
$ (a -> ℕ64) -> 𝐼 a -> 𝐼 ℕ64
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> ℕ64
forall a. ASized a => a -> ℕ64
asize (𝐼 a -> 𝐼 ℕ64) -> 𝐼 a -> 𝐼 ℕ64
forall a b. (a -> b) -> a -> b
$ t -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter t
xs) (𝐼 a -> 𝐼AC a) -> 𝐼 a -> 𝐼AC a
forall a b. (a -> b) -> a -> b
$ t -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter t
xs

---------------
-- Instances --
---------------

instance                       ASized 𝕊       where asize :: 𝕊 -> ℕ64
asize           = 𝕊 -> ℕ64
length64𝕊
instance (ASized a,ASized b) ⇒ ASized (a ∨ b) where asize :: (a ∨ b) -> ℕ64
asize           = (a -> ℕ64) -> (b -> ℕ64) -> (a ∨ b) -> ℕ64
forall a c b. (a -> c) -> (b -> c) -> (a ∨ b) -> c
elimChoice a -> ℕ64
forall a. ASized a => a -> ℕ64
asize b -> ℕ64
forall a. ASized a => a -> ℕ64
asize
instance (ASized a,ASized b) ⇒ ASized (a ∧ b) where asize :: (a ∧ b) -> ℕ64
asize (a
x :* b
y)  = a -> ℕ64
forall a. ASized a => a -> ℕ64
asize a
x ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ b -> ℕ64
forall a. ASized a => a -> ℕ64
asize b
y

---------------
-- Utilities --
---------------

buildC ∷ ℕ64 → a → (a → a) → 𝐼C a
buildC :: forall a. ℕ64 -> a -> (a -> a) -> 𝐼C a
buildC ℕ64
n a
x a -> a
g = ℕ64 -> 𝐼 a -> 𝐼C a
forall a. ℕ64 -> 𝐼 a -> 𝐼C a
𝐼C ℕ64
n (𝐼 a -> 𝐼C a) -> 𝐼 a -> 𝐼C a
forall a b. (a -> b) -> a -> b
$ ℕ64 -> a -> (a -> a) -> 𝐼 a
forall n a.
(Eq n, Zero n, One n, Plus n) =>
n -> a -> (a -> a) -> 𝐼 a
build ℕ64
n a
x a -> a
g

uptoC ∷ ℕ64 → 𝐼C ℕ64
uptoC :: ℕ64 -> 𝐼C ℕ64
uptoC ℕ64
n = ℕ64 -> ℕ64 -> (ℕ64 -> ℕ64) -> 𝐼C ℕ64
forall a. ℕ64 -> a -> (a -> a) -> 𝐼C a
buildC ℕ64
n ℕ64
forall a. Zero a => a
zero ℕ64 -> ℕ64
forall a. (One a, Plus a) => a -> a
succ

stringCS ∷ (ToIter ℂ t,CSized t) ⇒ t → 𝕊
stringCS :: forall t. (ToIter ℂ t, CSized t) => t -> 𝕊
stringCS t
ss = ℕ64 -> t -> 𝕊
forall t. ToIter ℂ t => ℕ64 -> t -> 𝕊
build𝕊CN (t -> ℕ64
forall a. CSized a => a -> ℕ64
csize t
ss) t
ss

stringSS ∷ (ToIter 𝕊 t,ASized t) ⇒ t → 𝕊
stringSS :: forall t. (ToIter 𝕊 t, ASized t) => t -> 𝕊
stringSS t
ss = ℕ64 -> t -> 𝕊
forall t. ToIter 𝕊 t => ℕ64 -> t -> 𝕊
build𝕊SN (t -> ℕ64
forall a. ASized a => a -> ℕ64
asize t
ss) t
ss

reiterC ∷ (ToIterC a t) ⇒ s → (a → s → (s ∧ b)) → t → 𝐼C b
reiterC :: forall a t s b. ToIterC a t => s -> (a -> s -> s ∧ b) -> t -> 𝐼C b
reiterC s
s a -> s -> s ∧ b
f (t -> 𝐼C a
forall a t. ToIterC a t => t -> 𝐼C a
iterC → 𝐼C ℕ64
n 𝐼 a
xs) = ℕ64 -> 𝐼 b -> 𝐼C b
forall a. ℕ64 -> 𝐼 a -> 𝐼C a
𝐼C ℕ64
n (𝐼 b -> 𝐼C b) -> 𝐼 b -> 𝐼C b
forall a b. (a -> b) -> a -> b
$ s -> (a -> s -> s ∧ b) -> 𝐼 a -> 𝐼 b
forall a t s b. ToIter a t => s -> (a -> s -> s ∧ b) -> t -> 𝐼 b
reiter s
s a -> s -> s ∧ b
f 𝐼 a
xs

withIndexC ∷ ∀ t a. (ToIterC a t) ⇒ t → 𝐼C (ℕ64 ∧ a)
withIndexC :: forall t a. ToIterC a t => t -> 𝐼C (ℕ64 ∧ a)
withIndexC = ℕ64 -> (a -> ℕ64 -> ℕ64 ∧ (ℕ64 ∧ a)) -> t -> 𝐼C (ℕ64 ∧ a)
forall a t s b. ToIterC a t => s -> (a -> s -> s ∧ b) -> t -> 𝐼C b
reiterC ℕ64
forall a. Zero a => a
zero ((a -> ℕ64 -> ℕ64 ∧ (ℕ64 ∧ a)) -> t -> 𝐼C (ℕ64 ∧ a))
-> (a -> ℕ64 -> ℕ64 ∧ (ℕ64 ∧ a)) -> t -> 𝐼C (ℕ64 ∧ a)
forall a b. (a -> b) -> a -> b
$ \ a
x ℕ64
i → (ℕ64
i ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ ℕ64
forall a. One a => a
one) ℕ64 -> (ℕ64 ∧ a) -> ℕ64 ∧ (ℕ64 ∧ a)
forall a b. a -> b -> a ∧ b
:* (ℕ64
i ℕ64 -> a -> ℕ64 ∧ a
forall a b. a -> b -> a ∧ b
:* a
x)

zipWithC ∷ (ToIterC a t₁,ToIterC b t₂) ⇒ (a → b → c) → t₁ → t₂ → 𝐼C c
zipWithC :: forall a t₁ b t₂ c.
(ToIterC a t₁, ToIterC b t₂) =>
(a -> b -> c) -> t₁ -> t₂ -> 𝐼C c
zipWithC a -> b -> c
f (t₁ -> 𝐼C a
forall a t. ToIterC a t => t -> 𝐼C a
iterC → 𝐼C ℕ64
n₁ 𝐼 a
xs) (t₂ -> 𝐼C b
forall a t. ToIterC a t => t -> 𝐼C a
iterC → 𝐼C ℕ64
n₂ 𝐼 b
ys) = ℕ64 -> 𝐼 c -> 𝐼C c
forall a. ℕ64 -> 𝐼 a -> 𝐼C a
𝐼C (ℕ64
n₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Meet a => a -> a -> a
⊓ ℕ64
n₂) (𝐼 c -> 𝐼C c) -> 𝐼 c -> 𝐼C c
forall a b. (a -> b) -> a -> b
$ (a -> b -> c) -> 𝐼 a -> 𝐼 b -> 𝐼 c
forall a t₁ b t₂ c.
(ToIter a t₁, ToIter b t₂) =>
(a -> b -> c) -> t₁ -> t₂ -> 𝐼 c
zipWith a -> b -> c
f 𝐼 a
xs 𝐼 b
ys

zipC ∷ (ToIterC a t₁,ToIterC b t₂) ⇒ t₁ → t₂ → 𝐼C (a ∧ b)
zipC :: forall a t₁ b t₂.
(ToIterC a t₁, ToIterC b t₂) =>
t₁ -> t₂ -> 𝐼C (a ∧ b)
zipC = (a -> b -> a ∧ b) -> t₁ -> t₂ -> 𝐼C (a ∧ b)
forall a t₁ b t₂ c.
(ToIterC a t₁, ToIterC b t₂) =>
(a -> b -> c) -> t₁ -> t₂ -> 𝐼C c
zipWithC a -> b -> a ∧ b
forall a b. a -> b -> a ∧ b
(:*)

prodWith𝐼C ∷ (a → b → c) → 𝐼C a → 𝐼C b → 𝐼C c
prodWith𝐼C :: forall a b c. (a -> b -> c) -> 𝐼C a -> 𝐼C b -> 𝐼C c
prodWith𝐼C a -> b -> c
f (𝐼C ℕ64
n₁ 𝐼 a
xs) (𝐼C ℕ64
n₂ 𝐼 b
ys) = ℕ64 -> 𝐼 c -> 𝐼C c
forall a. ℕ64 -> 𝐼 a -> 𝐼C a
𝐼C (ℕ64
n₁ ℕ64 -> ℕ64 -> ℕ64
forall a. Times a => a -> a -> a
× ℕ64
n₂) (𝐼 c -> 𝐼C c) -> 𝐼 c -> 𝐼C c
forall a b. (a -> b) -> a -> b
$ do
  a
x ← 𝐼 a
xs
  b
y ← 𝐼 b
ys
  c -> 𝐼 c
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return (c -> 𝐼 c) -> c -> 𝐼 c
forall a b. (a -> b) -> a -> b
$ a -> b -> c
f a
x b
y