module UVMHS.Core.Data.Iter where

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

import UVMHS.Core.Data.Arithmetic ()
import UVMHS.Core.Data.List ()
import UVMHS.Core.Data.String
import UVMHS.Core.Data.Pair
import UVMHS.Core.Data.Stream

import qualified Prelude as HS
import qualified Data.List as HS


instance Null (𝐼 a) where null :: 𝐼 a
null = 𝐼 a
forall a. 𝐼 a
empty𝐼
instance Append (𝐼 a) where ⧺ :: 𝐼 a -> 𝐼 a -> 𝐼 a
(⧺) = 𝐼 a -> 𝐼 a -> 𝐼 a
forall a. 𝐼 a -> 𝐼 a -> 𝐼 a
append𝐼
instance Monoid (𝐼 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 Return 𝐼 where return :: forall a. a -> 𝐼 a
return = a -> 𝐼 a
forall a. a -> 𝐼 a
single𝐼
instance Bind 𝐼 where ≫= :: forall a b. 𝐼 a -> (a -> 𝐼 b) -> 𝐼 b
(≫=) = 𝐼 a -> (a -> 𝐼 b) -> 𝐼 b
forall a b. 𝐼 a -> (a -> 𝐼 b) -> 𝐼 b
bind𝐼
instance Monad 𝐼
instance FunctorM 𝐼 where mapM :: forall (m :: * -> *) a b. Monad m => (a -> m b) -> 𝐼 a -> m (𝐼 b)
mapM = (a -> m b) -> 𝐼 a -> m (𝐼 b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> 𝐼 a -> m (𝐼 b)
mapM𝐼
instance Single a (𝐼 a) where single :: a -> 𝐼 a
single = a -> 𝐼 a
forall a. a -> 𝐼 a
single𝐼
instance ToIter a (𝐼 a) where iter :: 𝐼 a -> 𝐼 a
iter = 𝐼 a -> 𝐼 a
forall a. a -> a
id

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
∘ 𝕊 -> 𝕊 -> 𝕊 -> (a -> 𝕊) -> 𝑆 a -> 𝕊
forall a t. ToIter a t => 𝕊 -> 𝕊 -> 𝕊 -> (a -> 𝕊) -> t -> 𝕊
showCollection 𝕊
"𝑆[" 𝕊
"]" 𝕊
"," a -> 𝕊
forall a. Show a => a -> 𝕊
show𝕊
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
∘ 𝕊 -> 𝕊 -> 𝕊 -> (a -> 𝕊) -> 𝐼 a -> 𝕊
forall a t. ToIter a t => 𝕊 -> 𝕊 -> 𝕊 -> (a -> 𝕊) -> t -> 𝕊
showCollection 𝕊
"𝐼[" 𝕊
"]" 𝕊
"," a -> 𝕊
forall a. Show a => a -> 𝕊
show𝕊
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
∘ 𝕊 -> 𝕊 -> 𝕊 -> (a -> 𝕊) -> 𝐿 a -> 𝕊
forall a t. ToIter a t => 𝕊 -> 𝕊 -> 𝕊 -> (a -> 𝕊) -> t -> 𝕊
showCollection 𝕊
"[" 𝕊
"]" 𝕊
"," a -> 𝕊
forall a. Show a => a -> 𝕊
show𝕊

instance 𝕊 ⇄ 𝐼 ℂ where
  isoto :: 𝕊 -> 𝐼 ℂ
isoto = String -> 𝐼 ℂ
forall a t. ToIter a t => t -> 𝐼 a
iter (String -> 𝐼 ℂ) -> (𝕊 -> String) -> 𝕊 -> 𝐼 ℂ
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝕊 -> String
tohsChars
  isofr :: 𝐼 ℂ -> 𝕊
isofr = 𝐼 ℂ -> 𝕊
forall t. ToIter ℂ t => t -> 𝕊
string

empty𝐼 ∷ 𝐼 a
empty𝐼 :: forall a. 𝐼 a
empty𝐼 = 𝐼 a
forall a. 𝐼 a
null𝐼

cons𝐼 ∷ a → 𝐼 a → 𝐼 a
cons𝐼 :: forall a. a -> 𝐼 a -> 𝐼 a
cons𝐼 a
x 𝐼 a
xs = (forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
forall a.
(forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
𝐼 ((forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
 -> 𝐼 a)
-> (forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
-> 𝐼 a
forall a b. (a -> b) -> a -> b
HS.$ \ a -> b -> (b -> b) -> b
f b
i b -> b
𝓀 → 
  a -> b -> (b -> b) -> b
f a
x b
i ((b -> b) -> b) -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b
i' →
  𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
forall a.
𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
un𝐼 𝐼 a
xs a -> b -> (b -> b) -> b
f b
i' b -> b
𝓀

stream ∷ (ToIter a t) ⇒ t → 𝑆 a
stream :: forall a t. ToIter a t => t -> 𝑆 a
stream = 𝐼 a -> 𝑆 a
forall a. 𝐼 a -> 𝑆 a
stream𝐼 (𝐼 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

zipWith ∷ (ToIter a t₁,ToIter b t₂) ⇒ (a → b → c) → t₁ → t₂ → 𝐼 c
zipWith :: forall a t₁ b t₂ c.
(ToIter a t₁, ToIter b t₂) =>
(a -> b -> c) -> t₁ -> t₂ -> 𝐼 c
zipWith a -> b -> c
f t₁
xs t₂
ys = 𝑆 c -> 𝐼 c
forall a t. ToIter a t => t -> 𝐼 a
iter (𝑆 c -> 𝐼 c) -> 𝑆 c -> 𝐼 c
forall a b. (a -> b) -> a -> b
$ (a -> b -> c) -> 𝑆 a -> 𝑆 b -> 𝑆 c
forall a b c. (a -> b -> c) -> 𝑆 a -> 𝑆 b -> 𝑆 c
zipWith𝑆 a -> b -> c
f (t₁ -> 𝑆 a
forall a t. ToIter a t => t -> 𝑆 a
stream t₁
xs) (𝑆 b -> 𝑆 c) -> 𝑆 b -> 𝑆 c
forall a b. (a -> b) -> a -> b
$ t₂ -> 𝑆 b
forall a t. ToIter a t => t -> 𝑆 a
stream t₂
ys

zip ∷ (ToIter a t₁,ToIter b t₂) ⇒ t₁ → t₂ → 𝐼 (a ∧ b)
zip :: forall a t₁ b t₂.
(ToIter a t₁, ToIter b t₂) =>
t₁ -> t₂ -> 𝐼 (a ∧ b)
zip = (a -> b -> a ∧ b) -> t₁ -> t₂ -> 𝐼 (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
(:*)

snoc𝐼 ∷ 𝐼 a → a → 𝐼 a
snoc𝐼 :: forall a. 𝐼 a -> a -> 𝐼 a
snoc𝐼 𝐼 a
xs a
x = (forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
forall a.
(forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
𝐼 ((forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
 -> 𝐼 a)
-> (forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
-> 𝐼 a
forall a b. (a -> b) -> a -> b
HS.$ \ a -> b -> (b -> b) -> b
f b
i b -> b
𝓀 → 
  𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
forall a.
𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
un𝐼 𝐼 a
xs a -> b -> (b -> b) -> b
f b
i ((b -> b) -> b) -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b
i' →
  a -> b -> (b -> b) -> b
f a
x b
i' b -> b
𝓀

isEmpty ∷ (ToIter a t) ⇒ t → 𝔹
isEmpty :: forall a t. ToIter a t => t -> 𝔹
isEmpty t
xs = 𝐼 a -> (𝔹 -> 𝔹) -> 𝔹 -> (a -> 𝔹 -> (𝔹 -> 𝔹) -> 𝔹) -> 𝔹
forall a b. 𝐼 a -> (b -> b) -> b -> (a -> b -> (b -> b) -> b) -> b
run𝐼On (t -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter t
xs) 𝔹 -> 𝔹
forall a. a -> a
id 𝔹
True ((a -> 𝔹 -> (𝔹 -> 𝔹) -> 𝔹) -> 𝔹) -> (a -> 𝔹 -> (𝔹 -> 𝔹) -> 𝔹) -> 𝔹
forall a b. (a -> b) -> a -> b
$ \ a
_ 𝔹
_ 𝔹 -> 𝔹
_ → 𝔹
False

firstElem ∷ (ToIter a t) ⇒ t → 𝑂 a
firstElem :: forall a t. ToIter a t => t -> 𝑂 a
firstElem t
xs = 𝐼 a
-> (𝑂 a -> 𝑂 a) -> 𝑂 a -> (a -> 𝑂 a -> (𝑂 a -> 𝑂 a) -> 𝑂 a) -> 𝑂 a
forall a b. 𝐼 a -> (b -> b) -> b -> (a -> b -> (b -> b) -> b) -> b
run𝐼On (t -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter t
xs) 𝑂 a -> 𝑂 a
forall a. a -> a
id 𝑂 a
forall a. 𝑂 a
None ((a -> 𝑂 a -> (𝑂 a -> 𝑂 a) -> 𝑂 a) -> 𝑂 a)
-> (a -> 𝑂 a -> (𝑂 a -> 𝑂 a) -> 𝑂 a) -> 𝑂 a
forall a b. (a -> b) -> a -> b
$ \ a
x 𝑂 a
_ 𝑂 a -> 𝑂 a
_ → a -> 𝑂 a
forall a. a -> 𝑂 a
Some a
x

append𝐼 ∷ 𝐼 a → 𝐼 a → 𝐼 a
append𝐼 :: forall a. 𝐼 a -> 𝐼 a -> 𝐼 a
append𝐼 𝐼 a
xs 𝐼 a
ys = (forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
forall a.
(forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
𝐼 ((forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
 -> 𝐼 a)
-> (forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
-> 𝐼 a
forall a b. (a -> b) -> a -> b
HS.$ \ a -> b -> (b -> b) -> b
f b
i b -> b
𝓀 →
  𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
forall a.
𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
un𝐼 𝐼 a
xs a -> b -> (b -> b) -> b
f b
i ((b -> b) -> b) -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b
i' →
  𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
forall a.
𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
un𝐼 𝐼 a
ys a -> b -> (b -> b) -> b
f b
i' b -> b
𝓀

bind𝐼 ∷ ∀ a b. 𝐼 a → (a → 𝐼 b) → 𝐼 b
bind𝐼 :: forall a b. 𝐼 a -> (a -> 𝐼 b) -> 𝐼 b
bind𝐼 𝐼 a
xs a -> 𝐼 b
f =
  (forall b. (b -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 b
forall a.
(forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
𝐼 (
    \ (b -> b -> (b -> b) -> b
g ∷ b → c → (c → c) → c) (b
i₀ ∷ c) (b -> b
k₀ ∷ c → c) →
        𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
forall a.
𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
un𝐼 𝐼 a
xs (\ (a
x ∷ a) (b
i ∷ c) (b -> b
k ∷ c → c) →
          𝐼 b -> forall b. (b -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
forall a.
𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
un𝐼 (a -> 𝐼 b
f a
x) b -> b -> (b -> b) -> b
g b
i b -> b
k)
        b
i₀ b -> b
k₀
  )

mjoin𝐼 ∷ ∀ a. 𝐼 (𝐼 a) → 𝐼 a
mjoin𝐼 :: forall a. 𝐼 (𝐼 a) -> 𝐼 a
mjoin𝐼 𝐼 (𝐼 a)
xss = 𝐼 (𝐼 a) -> (𝐼 a -> 𝐼 a) -> 𝐼 a
forall a b. 𝐼 a -> (a -> 𝐼 b) -> 𝐼 b
bind𝐼 𝐼 (𝐼 a)
xss 𝐼 a -> 𝐼 a
forall a. a -> a
id

mapM𝐼 ∷ (Monad m) ⇒ (a → m b) → 𝐼 a → m (𝐼 b)
mapM𝐼 :: forall (m :: * -> *) a b. Monad m => (a -> m b) -> 𝐼 a -> m (𝐼 b)
mapM𝐼 a -> m b
f = m (𝐼 b) -> (a -> m (𝐼 b) -> m (𝐼 b)) -> 𝐼 a -> m (𝐼 b)
forall b a. b -> (a -> b -> b) -> 𝐼 a -> b
fold𝐼 (𝐼 b -> m (𝐼 b)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return 𝐼 b
forall a. 𝐼 a
empty𝐼) ((a -> m (𝐼 b) -> m (𝐼 b)) -> 𝐼 a -> m (𝐼 b))
-> (a -> m (𝐼 b) -> m (𝐼 b)) -> 𝐼 a -> m (𝐼 b)
forall a b. (a -> b) -> a -> b
$ \ a
x m (𝐼 b)
ysM → do
  𝐼 b
ys ← m (𝐼 b)
ysM
  b
y ← a -> m b
f a
x
  𝐼 b -> m (𝐼 b)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return (𝐼 b -> m (𝐼 b)) -> 𝐼 b -> m (𝐼 b)
forall a b. (a -> b) -> a -> b
$ 𝐼 b -> b -> 𝐼 b
forall a. 𝐼 a -> a -> 𝐼 a
snoc𝐼 𝐼 b
ys b
y

fold ∷ (ToIter a t) ⇒ b → (a → b → b) → t → b
fold :: forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
fold b
i a -> b -> b
f = b -> (a -> b -> b) -> 𝐼 a -> b
forall b a. b -> (a -> b -> b) -> 𝐼 a -> b
fold𝐼 b
i a -> b -> b
f (𝐼 a -> b) -> (t -> 𝐼 a) -> t -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ t -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter

foldFromWith ∷ (ToIter a t) ⇒ b → (a → b → b) → t → b
foldFromWith :: forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
foldFromWith = b -> (a -> b -> b) -> t -> b
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
fold

foldFromOn ∷ (ToIter a t) ⇒ b → t → (a → b → b) → b
foldFromOn :: forall a t b. ToIter a t => b -> t -> (a -> b -> b) -> b
foldFromOn = ((a -> b -> b) -> t -> b) -> t -> (a -> b -> b) -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((a -> b -> b) -> t -> b) -> t -> (a -> b -> b) -> b)
-> (b -> (a -> b -> b) -> t -> b) -> b -> t -> (a -> b -> b) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ b -> (a -> b -> b) -> t -> b
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
fold

foldOnFrom ∷ (ToIter a t) ⇒ t → b → (a → b → b) → b
foldOnFrom :: forall a t b. ToIter a t => t -> b -> (a -> b -> b) -> b
foldOnFrom = (b -> (a -> b -> b) -> t -> b) -> t -> b -> (a -> b -> b) -> b
forall a b c d. (a -> b -> c -> d) -> c -> a -> b -> d
rotateR b -> (a -> b -> b) -> t -> b
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
fold

foldOnWith ∷ (ToIter a t) ⇒ t → (a → b → b) → b → b
foldOnWith :: forall a t b. ToIter a t => t -> (a -> b -> b) -> b -> b
foldOnWith = (b -> (a -> b -> b) -> t -> b) -> t -> (a -> b -> b) -> b -> b
forall a b c d. (a -> b -> c -> d) -> c -> b -> a -> d
mirror b -> (a -> b -> b) -> t -> b
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
fold

foldWithOn ∷ (ToIter a t) ⇒ (a → b → b) → t → b → b
foldWithOn :: forall a t b. ToIter a t => (a -> b -> b) -> t -> b -> b
foldWithOn = (b -> (a -> b -> b) -> t -> b) -> (a -> b -> b) -> t -> b -> b
forall a b c d. (a -> b -> c -> d) -> b -> c -> a -> d
rotateL b -> (a -> b -> b) -> t -> b
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
fold

foldWithFrom ∷ (ToIter a t) ⇒ (a → b → b) → b → t → b
foldWithFrom :: forall a t b. ToIter a t => (a -> b -> b) -> b -> t -> b
foldWithFrom = (b -> (a -> b -> b) -> t -> b) -> (a -> b -> b) -> b -> t -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip b -> (a -> b -> b) -> t -> b
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
fold

foldk ∷ (ToIter a t) ⇒ b → (a → b → (b → b) → b) → t → b
foldk :: forall a t b.
ToIter a t =>
b -> (a -> b -> (b -> b) -> b) -> t -> b
foldk b
i a -> b -> (b -> b) -> b
f = b -> (a -> b -> (b -> b) -> b) -> 𝐼 a -> b
forall b a. b -> (a -> b -> (b -> b) -> b) -> 𝐼 a -> b
foldk𝐼 b
i a -> b -> (b -> b) -> b
f (𝐼 a -> b) -> (t -> 𝐼 a) -> t -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ t -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter

foldkFromWith ∷ (ToIter a t) ⇒ b → (a → b → (b → b) → b) → t → b
foldkFromWith :: forall a t b.
ToIter a t =>
b -> (a -> b -> (b -> b) -> b) -> t -> b
foldkFromWith = b -> (a -> b -> (b -> b) -> b) -> t -> b
forall a t b.
ToIter a t =>
b -> (a -> b -> (b -> b) -> b) -> t -> b
foldk

foldkFromOn ∷ (ToIter a t) ⇒ b → t → (a → b → (b → b) → b) → b
foldkFromOn :: forall a t b.
ToIter a t =>
b -> t -> (a -> b -> (b -> b) -> b) -> b
foldkFromOn = ((a -> b -> (b -> b) -> b) -> t -> b)
-> t -> (a -> b -> (b -> b) -> b) -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((a -> b -> (b -> b) -> b) -> t -> b)
 -> t -> (a -> b -> (b -> b) -> b) -> b)
-> (b -> (a -> b -> (b -> b) -> b) -> t -> b)
-> b
-> t
-> (a -> b -> (b -> b) -> b)
-> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ b -> (a -> b -> (b -> b) -> b) -> t -> b
forall a t b.
ToIter a t =>
b -> (a -> b -> (b -> b) -> b) -> t -> b
foldk

foldkOnFrom ∷ (ToIter a t) ⇒ t → b → (a → b → (b → b) → b) → b
foldkOnFrom :: forall a t b.
ToIter a t =>
t -> b -> (a -> b -> (b -> b) -> b) -> b
foldkOnFrom = (b -> (a -> b -> (b -> b) -> b) -> t -> b)
-> t -> b -> (a -> b -> (b -> b) -> b) -> b
forall a b c d. (a -> b -> c -> d) -> c -> a -> b -> d
rotateR b -> (a -> b -> (b -> b) -> b) -> t -> b
forall a t b.
ToIter a t =>
b -> (a -> b -> (b -> b) -> b) -> t -> b
foldk

foldkOnWith ∷ (ToIter a t) ⇒ t → (a → b → (b → b) → b) → b → b
foldkOnWith :: forall a t b.
ToIter a t =>
t -> (a -> b -> (b -> b) -> b) -> b -> b
foldkOnWith = (b -> (a -> b -> (b -> b) -> b) -> t -> b)
-> t -> (a -> b -> (b -> b) -> b) -> b -> b
forall a b c d. (a -> b -> c -> d) -> c -> b -> a -> d
mirror b -> (a -> b -> (b -> b) -> b) -> t -> b
forall a t b.
ToIter a t =>
b -> (a -> b -> (b -> b) -> b) -> t -> b
foldk

foldkWithOn ∷ (ToIter a t) ⇒ (a → b → (b → b) → b) → t → b → b
foldkWithOn :: forall a t b.
ToIter a t =>
(a -> b -> (b -> b) -> b) -> t -> b -> b
foldkWithOn = (b -> (a -> b -> (b -> b) -> b) -> t -> b)
-> (a -> b -> (b -> b) -> b) -> t -> b -> b
forall a b c d. (a -> b -> c -> d) -> b -> c -> a -> d
rotateL b -> (a -> b -> (b -> b) -> b) -> t -> b
forall a t b.
ToIter a t =>
b -> (a -> b -> (b -> b) -> b) -> t -> b
foldk

foldkWithFrom ∷ (ToIter a t) ⇒ (a → b → (b → b) → b) → b → t → b
foldkWithFrom :: forall a t b.
ToIter a t =>
(a -> b -> (b -> b) -> b) -> b -> t -> b
foldkWithFrom = (b -> (a -> b -> (b -> b) -> b) -> t -> b)
-> (a -> b -> (b -> b) -> b) -> b -> t -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip b -> (a -> b -> (b -> b) -> b) -> t -> b
forall a t b.
ToIter a t =>
b -> (a -> b -> (b -> b) -> b) -> t -> b
foldk

foldr ∷ (ToIter a t) ⇒ b → (a → b → b) → t → b
foldr :: forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
foldr b
i a -> b -> b
f = b -> (a -> b -> b) -> 𝐼 a -> b
forall b a. b -> (a -> b -> b) -> 𝐼 a -> b
foldr𝐼 b
i a -> b -> b
f (𝐼 a -> b) -> (t -> 𝐼 a) -> t -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ t -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter

foldrFromWith ∷ (ToIter a t) ⇒ b → (a → b → b) → t → b
foldrFromWith :: forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
foldrFromWith = b -> (a -> b -> b) -> t -> b
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
foldr

foldrFromOn ∷ (ToIter a t) ⇒ b → t → (a → b → b) → b
foldrFromOn :: forall a t b. ToIter a t => b -> t -> (a -> b -> b) -> b
foldrFromOn = ((a -> b -> b) -> t -> b) -> t -> (a -> b -> b) -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((a -> b -> b) -> t -> b) -> t -> (a -> b -> b) -> b)
-> (b -> (a -> b -> b) -> t -> b) -> b -> t -> (a -> b -> b) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ b -> (a -> b -> b) -> t -> b
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
foldr

foldrOnFrom ∷ (ToIter a t) ⇒ t → b → (a → b → b) → b
foldrOnFrom :: forall a t b. ToIter a t => t -> b -> (a -> b -> b) -> b
foldrOnFrom = (b -> (a -> b -> b) -> t -> b) -> t -> b -> (a -> b -> b) -> b
forall a b c d. (a -> b -> c -> d) -> c -> a -> b -> d
rotateR b -> (a -> b -> b) -> t -> b
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
foldr

foldrOnWith ∷ (ToIter a t) ⇒ t → (a → b → b) → b → b
foldrOnWith :: forall a t b. ToIter a t => t -> (a -> b -> b) -> b -> b
foldrOnWith = (b -> (a -> b -> b) -> t -> b) -> t -> (a -> b -> b) -> b -> b
forall a b c d. (a -> b -> c -> d) -> c -> b -> a -> d
mirror b -> (a -> b -> b) -> t -> b
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
foldr

foldrWithOn ∷ (ToIter a t) ⇒ (a → b → b) → t → b → b
foldrWithOn :: forall a t b. ToIter a t => (a -> b -> b) -> t -> b -> b
foldrWithOn = (b -> (a -> b -> b) -> t -> b) -> (a -> b -> b) -> t -> b -> b
forall a b c d. (a -> b -> c -> d) -> b -> c -> a -> d
rotateL b -> (a -> b -> b) -> t -> b
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
foldr

foldrWithFrom ∷ (ToIter a t) ⇒ (a → b → b) → b → t → b
foldrWithFrom :: forall a t b. ToIter a t => (a -> b -> b) -> b -> t -> b
foldrWithFrom = (b -> (a -> b -> b) -> t -> b) -> (a -> b -> b) -> b -> t -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip b -> (a -> b -> b) -> t -> b
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
foldr

mfold ∷ (Monad m,ToIter a t) ⇒ b → (a → b → m b) → t → m b
mfold :: forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> m b) -> t -> m b
mfold b
i₀ a -> b -> m b
f = m b -> (a -> m b -> (m b -> m b) -> m b) -> t -> m b
forall a t b.
ToIter a t =>
b -> (a -> b -> (b -> b) -> b) -> t -> b
foldkFromWith (b -> m b
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return b
i₀) ((a -> m b -> (m b -> m b) -> m b) -> t -> m b)
-> (a -> m b -> (m b -> m b) -> m b) -> t -> m b
forall a b. (a -> b) -> a -> b
$ \ a
x m b
iM m b -> m b
𝓀 → do b
i ← m b
iM ; m b -> m b
𝓀 (m b -> m b) -> m b -> m b
forall a b. (a -> b) -> a -> b
$ a -> b -> m b
f a
x b
i

mfoldFromWith ∷ (Monad m,ToIter a t) ⇒ b → (a → b → m b) → t → m b
mfoldFromWith :: forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> m b) -> t -> m b
mfoldFromWith = b -> (a -> b -> m b) -> t -> m b
forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> m b) -> t -> m b
mfold

mfoldFromOn ∷ (Monad m,ToIter a t) ⇒ b → t → (a → b → m b) → m b
mfoldFromOn :: forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> t -> (a -> b -> m b) -> m b
mfoldFromOn = ((a -> b -> m b) -> t -> m b) -> t -> (a -> b -> m b) -> m b
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((a -> b -> m b) -> t -> m b) -> t -> (a -> b -> m b) -> m b)
-> (b -> (a -> b -> m b) -> t -> m b)
-> b
-> t
-> (a -> b -> m b)
-> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ b -> (a -> b -> m b) -> t -> m b
forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> m b) -> t -> m b
mfold

mfoldOnFrom ∷ (Monad m,ToIter a t) ⇒ t → b → (a → b → m b) → m b
mfoldOnFrom :: forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
t -> b -> (a -> b -> m b) -> m b
mfoldOnFrom = (b -> (a -> b -> m b) -> t -> m b)
-> t -> b -> (a -> b -> m b) -> m b
forall a b c d. (a -> b -> c -> d) -> c -> a -> b -> d
rotateR b -> (a -> b -> m b) -> t -> m b
forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> m b) -> t -> m b
mfold

mfoldOnWith ∷ (Monad m,ToIter a t) ⇒ t → (a → b → m b) → b → m b
mfoldOnWith :: forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
t -> (a -> b -> m b) -> b -> m b
mfoldOnWith = (b -> (a -> b -> m b) -> t -> m b)
-> t -> (a -> b -> m b) -> b -> m b
forall a b c d. (a -> b -> c -> d) -> c -> b -> a -> d
mirror b -> (a -> b -> m b) -> t -> m b
forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> m b) -> t -> m b
mfold

mfoldWithOn ∷ (Monad m,ToIter a t) ⇒ (a → b → m b) → t → b → m b
mfoldWithOn :: forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
(a -> b -> m b) -> t -> b -> m b
mfoldWithOn = (b -> (a -> b -> m b) -> t -> m b)
-> (a -> b -> m b) -> t -> b -> m b
forall a b c d. (a -> b -> c -> d) -> b -> c -> a -> d
rotateL b -> (a -> b -> m b) -> t -> m b
forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> m b) -> t -> m b
mfold

mfoldWithFrom ∷ (Monad m,ToIter a t) ⇒ (a → b → m b) → b → t → m b
mfoldWithFrom :: forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
(a -> b -> m b) -> b -> t -> m b
mfoldWithFrom = (b -> (a -> b -> m b) -> t -> m b)
-> (a -> b -> m b) -> b -> t -> m b
forall a b c. (a -> b -> c) -> b -> a -> c
flip b -> (a -> b -> m b) -> t -> m b
forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> m b) -> t -> m b
mfold

mfoldk ∷ (Monad m,ToIter a t) ⇒ b → (a → b → (m b → m b) → m b) → t → m b
mfoldk :: forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> (m b -> m b) -> m b) -> t -> m b
mfoldk b
i₀ a -> b -> (m b -> m b) -> m b
f = m b -> (a -> m b -> (m b -> m b) -> m b) -> t -> m b
forall a t b.
ToIter a t =>
b -> (a -> b -> (b -> b) -> b) -> t -> b
foldkFromWith (b -> m b
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return b
i₀) ((a -> m b -> (m b -> m b) -> m b) -> t -> m b)
-> (a -> m b -> (m b -> m b) -> m b) -> t -> m b
forall a b. (a -> b) -> a -> b
$ \ a
x m b
iM m b -> m b
𝓀 → do b
i ← m b
iM ; a -> b -> (m b -> m b) -> m b
f a
x b
i m b -> m b
𝓀

mfoldkFromWith ∷ (Monad m,ToIter a t) ⇒ b → (a → b → (m b → m b) → m b) → t → m b
mfoldkFromWith :: forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> (m b -> m b) -> m b) -> t -> m b
mfoldkFromWith = b -> (a -> b -> (m b -> m b) -> m b) -> t -> m b
forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> (m b -> m b) -> m b) -> t -> m b
mfoldk

mfoldkFromOn ∷ (Monad m,ToIter a t) ⇒ b → t → (a → b → (m b → m b) → m b) → m b
mfoldkFromOn :: forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> t -> (a -> b -> (m b -> m b) -> m b) -> m b
mfoldkFromOn = ((a -> b -> (m b -> m b) -> m b) -> t -> m b)
-> t -> (a -> b -> (m b -> m b) -> m b) -> m b
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((a -> b -> (m b -> m b) -> m b) -> t -> m b)
 -> t -> (a -> b -> (m b -> m b) -> m b) -> m b)
-> (b -> (a -> b -> (m b -> m b) -> m b) -> t -> m b)
-> b
-> t
-> (a -> b -> (m b -> m b) -> m b)
-> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ b -> (a -> b -> (m b -> m b) -> m b) -> t -> m b
forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> (m b -> m b) -> m b) -> t -> m b
mfoldk

mfoldkOnFrom ∷ (Monad m,ToIter a t) ⇒ t → b → (a → b → (m b → m b) → m b) → m b
mfoldkOnFrom :: forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
t -> b -> (a -> b -> (m b -> m b) -> m b) -> m b
mfoldkOnFrom = (b -> (a -> b -> (m b -> m b) -> m b) -> t -> m b)
-> t -> b -> (a -> b -> (m b -> m b) -> m b) -> m b
forall a b c d. (a -> b -> c -> d) -> c -> a -> b -> d
rotateR b -> (a -> b -> (m b -> m b) -> m b) -> t -> m b
forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> (m b -> m b) -> m b) -> t -> m b
mfoldk

mfoldkOnWith ∷ (Monad m,ToIter a t) ⇒ t → (a → b → (m b → m b) → m b) → b → m b
mfoldkOnWith :: forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
t -> (a -> b -> (m b -> m b) -> m b) -> b -> m b
mfoldkOnWith = (b -> (a -> b -> (m b -> m b) -> m b) -> t -> m b)
-> t -> (a -> b -> (m b -> m b) -> m b) -> b -> m b
forall a b c d. (a -> b -> c -> d) -> c -> b -> a -> d
mirror b -> (a -> b -> (m b -> m b) -> m b) -> t -> m b
forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> (m b -> m b) -> m b) -> t -> m b
mfoldk

mfoldkWithOn ∷ (Monad m,ToIter a t) ⇒ (a → b → (m b → m b) → m b) → t → b → m b
mfoldkWithOn :: forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
(a -> b -> (m b -> m b) -> m b) -> t -> b -> m b
mfoldkWithOn = (b -> (a -> b -> (m b -> m b) -> m b) -> t -> m b)
-> (a -> b -> (m b -> m b) -> m b) -> t -> b -> m b
forall a b c d. (a -> b -> c -> d) -> b -> c -> a -> d
rotateL b -> (a -> b -> (m b -> m b) -> m b) -> t -> m b
forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> (m b -> m b) -> m b) -> t -> m b
mfoldk

mfoldkWithFrom ∷ (Monad m,ToIter a t) ⇒ (a → b → (m b → m b) → m b) → b → t → m b
mfoldkWithFrom :: forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
(a -> b -> (m b -> m b) -> m b) -> b -> t -> m b
mfoldkWithFrom = (b -> (a -> b -> (m b -> m b) -> m b) -> t -> m b)
-> (a -> b -> (m b -> m b) -> m b) -> b -> t -> m b
forall a b c. (a -> b -> c) -> b -> a -> c
flip b -> (a -> b -> (m b -> m b) -> m b) -> t -> m b
forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> (m b -> m b) -> m b) -> t -> m b
mfoldk

mfoldr ∷ (Monad m,ToIter a t) ⇒ b → (a → b → m b) → t → m b
mfoldr :: forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> m b) -> t -> m b
mfoldr b
i₀ a -> b -> m b
f = m b -> (a -> m b -> (m b -> m b) -> m b) -> t -> m b
forall a t b.
ToIter a t =>
b -> (a -> b -> (b -> b) -> b) -> t -> b
foldkFromWith (b -> m b
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return b
i₀) ((a -> m b -> (m b -> m b) -> m b) -> t -> m b)
-> (a -> m b -> (m b -> m b) -> m b) -> t -> m b
forall a b. (a -> b) -> a -> b
$ \ a
x m b
iM m b -> m b
𝓀 → do b
i ← m b -> m b
𝓀 m b
iM ; a -> b -> m b
f a
x b
i

mfoldrFromWith ∷ (Monad m,ToIter a t) ⇒ b → (a → b → m b) → t → m b
mfoldrFromWith :: forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> m b) -> t -> m b
mfoldrFromWith = b -> (a -> b -> m b) -> t -> m b
forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> m b) -> t -> m b
mfoldr

mfoldrFromOn ∷ (Monad m,ToIter a t) ⇒ b → t → (a → b → m b) → m b
mfoldrFromOn :: forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> t -> (a -> b -> m b) -> m b
mfoldrFromOn = ((a -> b -> m b) -> t -> m b) -> t -> (a -> b -> m b) -> m b
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((a -> b -> m b) -> t -> m b) -> t -> (a -> b -> m b) -> m b)
-> (b -> (a -> b -> m b) -> t -> m b)
-> b
-> t
-> (a -> b -> m b)
-> m b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ b -> (a -> b -> m b) -> t -> m b
forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> m b) -> t -> m b
mfoldr

mfoldrOnFrom ∷ (Monad m,ToIter a t) ⇒ t → b → (a → b → m b) → m b
mfoldrOnFrom :: forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
t -> b -> (a -> b -> m b) -> m b
mfoldrOnFrom = (b -> (a -> b -> m b) -> t -> m b)
-> t -> b -> (a -> b -> m b) -> m b
forall a b c d. (a -> b -> c -> d) -> c -> a -> b -> d
rotateR b -> (a -> b -> m b) -> t -> m b
forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> m b) -> t -> m b
mfoldr

mfoldrOnWith ∷ (Monad m,ToIter a t) ⇒ t → (a → b → m b) → b → m b
mfoldrOnWith :: forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
t -> (a -> b -> m b) -> b -> m b
mfoldrOnWith = (b -> (a -> b -> m b) -> t -> m b)
-> t -> (a -> b -> m b) -> b -> m b
forall a b c d. (a -> b -> c -> d) -> c -> b -> a -> d
mirror b -> (a -> b -> m b) -> t -> m b
forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> m b) -> t -> m b
mfoldr

mfoldrWithOn ∷ (Monad m,ToIter a t) ⇒ (a → b → m b) → t → b → m b
mfoldrWithOn :: forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
(a -> b -> m b) -> t -> b -> m b
mfoldrWithOn = (b -> (a -> b -> m b) -> t -> m b)
-> (a -> b -> m b) -> t -> b -> m b
forall a b c d. (a -> b -> c -> d) -> b -> c -> a -> d
rotateL b -> (a -> b -> m b) -> t -> m b
forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> m b) -> t -> m b
mfoldr

mfoldrWithFrom ∷ (Monad m,ToIter a t) ⇒ (a → b → m b) → b → t → m b
mfoldrWithFrom :: forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
(a -> b -> m b) -> b -> t -> m b
mfoldrWithFrom = (b -> (a -> b -> m b) -> t -> m b)
-> (a -> b -> m b) -> b -> t -> m b
forall a b c. (a -> b -> c) -> b -> a -> c
flip b -> (a -> b -> m b) -> t -> m b
forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> m b) -> t -> m b
mfoldr

eachWith ∷ (Monad m,ToIter a t) ⇒ (a → m ()) → t → m ()
eachWith :: forall (m :: * -> *) a t.
(Monad m, ToIter a t) =>
(a -> m ()) -> t -> m ()
eachWith a -> m ()
f = () -> (a -> () -> m ()) -> t -> m ()
forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> m b) -> t -> m b
mfoldFromWith () ((a -> () -> m ()) -> t -> m ()) -> (a -> () -> m ()) -> t -> m ()
forall a b. (a -> b) -> a -> b
$ m () -> () -> m ()
forall a b. a -> b -> a
const (m () -> () -> m ()) -> (a -> m ()) -> a -> () -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> m ()
f

eachOn ∷ (Monad m,ToIter a t) ⇒ t → (a → m ()) → m () 
eachOn :: forall (m :: * -> *) a t.
(Monad m, ToIter a t) =>
t -> (a -> m ()) -> m ()
eachOn = ((a -> m ()) -> t -> m ()) -> t -> (a -> m ()) -> m ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> m ()) -> t -> m ()
forall (m :: * -> *) a t.
(Monad m, ToIter a t) =>
(a -> m ()) -> t -> m ()
eachWith

eachkWith ∷ (Monad m,ToIter a t) ⇒ (a → (m () → m ()) → m ()) → t → m ()
eachkWith :: forall (m :: * -> *) a t.
(Monad m, ToIter a t) =>
(a -> (m () -> m ()) -> m ()) -> t -> m ()
eachkWith a -> (m () -> m ()) -> m ()
f = () -> (a -> () -> (m () -> m ()) -> m ()) -> t -> m ()
forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> (m b -> m b) -> m b) -> t -> m b
mfoldkFromWith () ((a -> () -> (m () -> m ()) -> m ()) -> t -> m ())
-> (a -> () -> (m () -> m ()) -> m ()) -> t -> m ()
forall a b. (a -> b) -> a -> b
$ ((m () -> m ()) -> m ()) -> () -> (m () -> m ()) -> m ()
forall a b. a -> b -> a
const (((m () -> m ()) -> m ()) -> () -> (m () -> m ()) -> m ())
-> (a -> (m () -> m ()) -> m ())
-> a
-> ()
-> (m () -> m ())
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> (m () -> m ()) -> m ()
f

eachkOn ∷ (Monad m,ToIter a t) ⇒ t → (a → (m () → m ()) → m ()) → m () 
eachkOn :: forall (m :: * -> *) a t.
(Monad m, ToIter a t) =>
t -> (a -> (m () -> m ()) -> m ()) -> m ()
eachkOn = ((a -> (m () -> m ()) -> m ()) -> t -> m ())
-> t -> (a -> (m () -> m ()) -> m ()) -> m ()
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> (m () -> m ()) -> m ()) -> t -> m ()
forall (m :: * -> *) a t.
(Monad m, ToIter a t) =>
(a -> (m () -> m ()) -> m ()) -> t -> m ()
eachkWith

exec ∷ (Monad m,ToIter (m ()) t) ⇒ t → m () 
exec :: forall (m :: * -> *) t. (Monad m, ToIter (m ()) t) => t -> m ()
exec = (m () -> m ()) -> t -> m ()
forall (m :: * -> *) a t.
(Monad m, ToIter a t) =>
(a -> m ()) -> t -> m ()
eachWith m () -> m ()
forall a. a -> a
id

sum ∷ (ToIter a t,Additive a) ⇒ t → a
sum :: forall a t. (ToIter a t, Additive a) => t -> a
sum = a -> (a -> a -> a) -> t -> a
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
fold a
forall a. Zero a => a
zero a -> a -> a
forall a. Plus a => a -> a -> a
(+)

product ∷ (ToIter a t,Multiplicative a) ⇒ t → a
product :: forall a t. (ToIter a t, Multiplicative a) => t -> a
product = a -> (a -> a -> a) -> t -> a
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
fold a
forall a. One a => a
one a -> a -> a
forall a. Times a => a -> a -> a
(×)

concat ∷ (Monoid a,ToIter a t) ⇒ t → a
concat :: forall a t. (Monoid a, ToIter a t) => t -> a
concat = a -> (a -> a -> a) -> t -> a
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
foldr a
forall a. Null a => a
null a -> a -> a
forall a. Append a => a -> a -> a
(⧺)

sequence ∷ (Seqoid a,ToIter a t) ⇒ t → a
sequence :: forall a t. (Seqoid a, ToIter a t) => t -> a
sequence = a -> (a -> a -> a) -> t -> a
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
foldr a
forall a. Eps a => a
eps a -> a -> a
forall a. Seq a => a -> a -> a
(▷)

compose ∷ (ToIter (a → a) t) ⇒ t → a → a
compose :: forall a t. ToIter (a -> a) t => t -> a -> a
compose = (a -> a) -> ((a -> a) -> (a -> a) -> a -> a) -> t -> a -> a
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
foldr a -> a
forall a. a -> a
id (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
(∘)

mcompose ∷ (Monad m) ⇒ (ToIter (a → m a) t) ⇒ t → a → m a
mcompose :: forall (m :: * -> *) a t.
(Monad m, ToIter (a -> m a) t) =>
t -> a -> m a
mcompose = (a -> m a)
-> ((a -> m a) -> (a -> m a) -> a -> m a) -> t -> a -> m a
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
foldr a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return (a -> m a) -> (a -> m a) -> a -> m a
forall (m :: * -> *) b c a.
Bind m =>
(b -> m c) -> (a -> m b) -> a -> m c
(*∘)

wcompose ∷ (Comonad w) ⇒ (ToIter (w a → a) t) ⇒ t → w a → a
wcompose :: forall (w :: * -> *) a t.
(Comonad w, ToIter (w a -> a) t) =>
t -> w a -> a
wcompose = (w a -> a)
-> ((w a -> a) -> (w a -> a) -> w a -> a) -> t -> w a -> a
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
foldr w a -> a
forall a. w a -> a
forall (w :: * -> *) a. Extract w => w a -> a
extract (w a -> a) -> (w a -> a) -> w a -> a
forall (w :: * -> *) b c a.
Cobind w =>
(w b -> c) -> (w a -> b) -> w a -> c
(%∘)

minsFrom ∷ (ToIter a t,Ord a) ⇒ a → t → a
minsFrom :: forall a t. (ToIter a t, Ord a) => a -> t -> a
minsFrom = (a -> a -> a) -> a -> t -> a
forall a t b. ToIter a t => (a -> b -> b) -> b -> t -> b
foldWithFrom a -> a -> a
forall a. Ord a => a -> a -> a
(⩎)

maxsFrom ∷ (ToIter a t,Ord a) ⇒ a → t → a
maxsFrom :: forall a t. (ToIter a t, Ord a) => a -> t -> a
maxsFrom = (a -> a -> a) -> a -> t -> a
forall a t b. ToIter a t => (a -> b -> b) -> b -> t -> b
foldWithFrom a -> a -> a
forall a. Ord a => a -> a -> a
(⩏)

joinsFrom ∷ (ToIter a t,Join a) ⇒ a → t → a
joinsFrom :: forall a t. (ToIter a t, Join a) => a -> t -> a
joinsFrom = (a -> a -> a) -> a -> t -> a
forall a t b. ToIter a t => (a -> b -> b) -> b -> t -> b
foldWithFrom a -> a -> a
forall a. Join a => a -> a -> a
(⊔)

joins ∷ (JoinLattice a,ToIter a t) ⇒ t → a
joins :: forall a t. (JoinLattice a, ToIter a t) => t -> a
joins = a -> t -> a
forall a t. (ToIter a t, Join a) => a -> t -> a
joinsFrom a
forall a. Bot a => a
bot

meetsFrom ∷ (ToIter a t,Meet a) ⇒ a → t → a
meetsFrom :: forall a t. (ToIter a t, Meet a) => a -> t -> a
meetsFrom = (a -> a -> a) -> a -> t -> a
forall a t b. ToIter a t => (a -> b -> b) -> b -> t -> b
foldWithFrom a -> a -> a
forall a. Meet a => a -> a -> a
(⊓)

meets ∷ (MeetLattice a,ToIter a t) ⇒ t → a
meets :: forall a t. (MeetLattice a, ToIter a t) => t -> a
meets = a -> t -> a
forall a t. (ToIter a t, Meet a) => a -> t -> a
meetsFrom a
forall a. Top a => a
top

or ∷ (ToIter 𝔹 t) ⇒ t → 𝔹
or :: forall t. ToIter 𝔹 t => t -> 𝔹
or = 𝔹 -> (𝔹 -> 𝔹 -> (𝔹 -> 𝔹) -> 𝔹) -> t -> 𝔹
forall a t b.
ToIter a t =>
b -> (a -> b -> (b -> b) -> b) -> t -> b
foldk 𝔹
False ((𝔹 -> 𝔹 -> (𝔹 -> 𝔹) -> 𝔹) -> t -> 𝔹)
-> (𝔹 -> 𝔹 -> (𝔹 -> 𝔹) -> 𝔹) -> t -> 𝔹
forall a b. (a -> b) -> a -> b
$ \ 𝔹
b₁ 𝔹
b₂ 𝔹 -> 𝔹
𝓀 → if 𝔹
b₁ then 𝔹
True else 𝔹 -> 𝔹
𝓀 𝔹
b₂

orf ∷ (ToIter (a → 𝔹) t) ⇒ t → a → 𝔹
orf :: forall a t. ToIter (a -> 𝔹) t => t -> a -> 𝔹
orf t
fs a
x = 𝐼 𝔹 -> 𝔹
forall t. ToIter 𝔹 t => t -> 𝔹
or (𝐼 𝔹 -> 𝔹) -> 𝐼 𝔹 -> 𝔹
forall a b. (a -> b) -> a -> b
$ ((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. a -> (a -> b) -> b
appto a
x) (𝐼 (a -> 𝔹) -> 𝐼 𝔹) -> 𝐼 (a -> 𝔹) -> 𝐼 𝔹
forall a b. (a -> b) -> a -> b
$ t -> 𝐼 (a -> 𝔹)
forall a t. ToIter a t => t -> 𝐼 a
iter t
fs

andf ∷ (ToIter (a → 𝔹) t) ⇒ t → a → 𝔹
andf :: forall a t. ToIter (a -> 𝔹) t => t -> a -> 𝔹
andf t
fs a
x = 𝐼 𝔹 -> 𝔹
forall t. ToIter 𝔹 t => t -> 𝔹
and (𝐼 𝔹 -> 𝔹) -> 𝐼 𝔹 -> 𝔹
forall a b. (a -> b) -> a -> b
$ ((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. a -> (a -> b) -> b
appto a
x) (𝐼 (a -> 𝔹) -> 𝐼 𝔹) -> 𝐼 (a -> 𝔹) -> 𝐼 𝔹
forall a b. (a -> b) -> a -> b
$ t -> 𝐼 (a -> 𝔹)
forall a t. ToIter a t => t -> 𝐼 a
iter t
fs

and ∷ (ToIter 𝔹 t) ⇒ t → 𝔹
and :: forall t. ToIter 𝔹 t => t -> 𝔹
and = 𝔹 -> (𝔹 -> 𝔹 -> (𝔹 -> 𝔹) -> 𝔹) -> t -> 𝔹
forall a t b.
ToIter a t =>
b -> (a -> b -> (b -> b) -> b) -> t -> b
foldk 𝔹
True ((𝔹 -> 𝔹 -> (𝔹 -> 𝔹) -> 𝔹) -> t -> 𝔹)
-> (𝔹 -> 𝔹 -> (𝔹 -> 𝔹) -> 𝔹) -> t -> 𝔹
forall a b. (a -> b) -> a -> b
$ \ 𝔹
b₁ 𝔹
b₂ 𝔹 -> 𝔹
𝓀 → if 𝔹
b₁ then 𝔹 -> 𝔹
𝓀 𝔹
b₂ else 𝔹
False

count ∷ ∀ n t a. (Zero n,One n,Plus n,ToIter a t) ⇒ t → n
count :: forall n t a. (Zero n, One n, Plus n, ToIter a t) => t -> n
count = n -> (a -> n -> n) -> t -> n
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
fold n
forall a. Zero a => a
zero ((a -> n -> n) -> t -> n) -> (a -> n -> n) -> t -> n
forall a b. (a -> b) -> a -> b
$ (n -> n) -> a -> n -> n
forall a b. a -> b -> a
const n -> n
forall a. (One a, Plus a) => a -> a
succ

countWith ∷ ∀ n t a. (Zero n,One n,Plus n,ToIter a t) ⇒ (a → 𝔹) → t → n
countWith :: forall n t a.
(Zero n, One n, Plus n, ToIter a t) =>
(a -> 𝔹) -> t -> n
countWith a -> 𝔹
f = n -> (a -> n -> n) -> t -> n
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
fold n
forall a. Zero a => a
zero ((a -> n -> n) -> t -> n) -> (a -> n -> n) -> t -> n
forall a b. (a -> b) -> a -> b
$ \ a
x → case a -> 𝔹
f a
x of
  𝔹
True → n -> n
forall a. (One a, Plus a) => a -> a
succ
  𝔹
False → n -> n
forall a. a -> a
id

reverse ∷ (ToIter a t) ⇒ t → 𝐼 a
reverse :: forall a t. ToIter a t => t -> 𝐼 a
reverse t
xs = (forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
forall a.
(forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
𝐼 ((forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
 -> 𝐼 a)
-> (forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
-> 𝐼 a
forall a b. (a -> b) -> a -> b
HS.$ \ a -> b -> (b -> b) -> b
f b
i₀ b -> b
𝓀₀ → 𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
forall a.
𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
un𝐼 (t -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter t
xs) (\ a
x b -> b
𝓀 (b -> b) -> b -> b
m𝓀 → (b -> b) -> b -> b
m𝓀 ((b -> b) -> b -> b) -> (b -> b) -> b -> b
forall a b. (a -> b) -> a -> b
$ \ b
i → a -> b -> (b -> b) -> b
f a
x b
i b -> b
𝓀) b -> b
𝓀₀ (b -> b) -> b -> b
forall a. a -> a
id b
i₀

replicateI ∷ ∀ n a. (Eq n,Zero n,One n,Plus n) ⇒ n → (n → a) → 𝐼 a
replicateI :: forall n a. (Eq n, Zero n, One n, Plus n) => n -> (n -> a) -> 𝐼 a
replicateI n
n₀ n -> a
g = (forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
forall a.
(forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
𝐼 ((forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
 -> 𝐼 a)
-> (forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
-> 𝐼 a
forall a b. (a -> b) -> a -> b
HS.$ \ a -> b -> (b -> b) -> b
f → ((b -> b) -> b -> b) -> b -> (b -> b) -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((b -> b) -> b -> b) -> b -> (b -> b) -> b)
-> ((b -> b) -> b -> b) -> b -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b -> b
𝓀 → 
  let loop :: n -> b -> b
loop n
n b
i
        | n
n n -> n -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ n
n₀ = b -> b
𝓀 b
i
        | 𝔹
otherwise = 
            a -> b -> (b -> b) -> b
f (n -> a
g n
n) b
i ((b -> b) -> b) -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b
i' →
            n -> b -> b
loop (n -> n
forall a. (One a, Plus a) => a -> a
succ n
n) b
i'
  in n -> b -> b
loop n
forall a. Zero a => a
zero

replicate ∷ ∀ n a. (Eq n,Zero n,One n,Plus n) ⇒ n → a → 𝐼 a
replicate :: forall n a. (Eq n, Zero n, One n, Plus n) => n -> a -> 𝐼 a
replicate n
n = n -> (n -> a) -> 𝐼 a
forall n a. (Eq n, Zero n, One n, Plus n) => n -> (n -> a) -> 𝐼 a
replicateI n
n ((n -> a) -> 𝐼 a) -> (a -> n -> a) -> a -> 𝐼 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> n -> a
forall a b. a -> b -> a
const

build ∷ ∀ n a. (Eq n,Zero n,One n,Plus n) ⇒ n → a → (a → a) → 𝐼 a
build :: forall n a.
(Eq n, Zero n, One n, Plus n) =>
n -> a -> (a -> a) -> 𝐼 a
build n
n₀ a
x₀ a -> a
g = (forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
forall a.
(forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
𝐼 ((forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
 -> 𝐼 a)
-> (forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
-> 𝐼 a
forall a b. (a -> b) -> a -> b
HS.$ \ a -> b -> (b -> b) -> b
f → ((b -> b) -> b -> b) -> b -> (b -> b) -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((b -> b) -> b -> b) -> b -> (b -> b) -> b)
-> ((b -> b) -> b -> b) -> b -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b -> b
𝓀 → 
  let loop :: n -> a -> b -> b
loop n
n a
x b
i
        | n
n n -> n -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ n
n₀ = b -> b
𝓀 b
i
        | 𝔹
otherwise = 
            a -> b -> (b -> b) -> b
f a
x b
i ((b -> b) -> b) -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b
i' →
            n -> a -> b -> b
loop (n -> n
forall a. (One a, Plus a) => a -> a
succ n
n) (a -> a
g a
x) b
i'
  in n -> a -> b -> b
loop n
forall a. Zero a => a
zero a
x₀

range ∷ (Eq n,Zero n,One n,Plus n,Minus n) ⇒ n → n → 𝐼 n
range :: forall n. (Eq n, Zero n, One n, Plus n, Minus n) => n -> n -> 𝐼 n
range n
lb n
ub = n -> n -> (n -> n) -> 𝐼 n
forall n a.
(Eq n, Zero n, One n, Plus n) =>
n -> a -> (a -> a) -> 𝐼 a
build (n
ub n -> n -> n
forall a. Minus a => a -> a -> a
- n
lb) n
lb n -> n
forall a. (One a, Plus a) => a -> a
succ

upto ∷ (Eq n,Zero n,One n,Plus n) ⇒ n → 𝐼 n
upto :: forall n. (Eq n, Zero n, One n, Plus n) => n -> 𝐼 n
upto n
n = n -> n -> (n -> n) -> 𝐼 n
forall n a.
(Eq n, Zero n, One n, Plus n) =>
n -> a -> (a -> a) -> 𝐼 a
build n
n n
forall a. Zero a => a
zero n -> n
forall a. (One a, Plus a) => a -> a
succ

reiter ∷ (ToIter a t) ⇒ s → (a → s → (s ∧ b)) → t → 𝐼 b
reiter :: forall a t s b. ToIter a t => s -> (a -> s -> s ∧ b) -> t -> 𝐼 b
reiter s
s₀ a -> s -> s ∧ b
f t
xs = 
  (forall b. (b -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 b
forall a.
(forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
𝐼 ((forall b. (b -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
 -> 𝐼 b)
-> (forall b. (b -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
-> 𝐼 b
forall a b. (a -> b) -> a -> b
HS.$ \ b -> b -> (b -> b) -> b
g b
i₀ b -> b
𝓀₀ → 
    (s ∧ b) -> b
forall a b. (a ∧ b) -> b
snd ((s ∧ b) -> b) -> (s ∧ b) -> b
forall a b. (a -> b) -> a -> b
$ 𝐼 a
-> ((s ∧ b) -> s ∧ b)
-> (s ∧ b)
-> (a -> (s ∧ b) -> ((s ∧ b) -> s ∧ b) -> s ∧ b)
-> s ∧ b
forall a b. 𝐼 a -> (b -> b) -> b -> (a -> b -> (b -> b) -> b) -> b
run𝐼On (t -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter t
xs) (\ (s
s :* b
i) → s
s s -> b -> s ∧ b
forall a b. a -> b -> a ∧ b
:* b -> b
𝓀₀ b
i) (s
s₀ s -> b -> s ∧ b
forall a b. a -> b -> a ∧ b
:* b
i₀) ((a -> (s ∧ b) -> ((s ∧ b) -> s ∧ b) -> s ∧ b) -> s ∧ b)
-> (a -> (s ∧ b) -> ((s ∧ b) -> s ∧ b) -> s ∧ b) -> s ∧ b
forall a b. (a -> b) -> a -> b
$ \ a
x (s
s :* b
i) (s ∧ b) -> s ∧ b
𝓀 → 
        let s
s' :* b
y = a -> s -> s ∧ b
f a
x s
s
        in (s
s' s -> b -> s ∧ b
forall a b. a -> b -> a ∧ b
:*) (b -> s ∧ b) -> b -> s ∧ b
forall a b. (a -> b) -> a -> b
$ b -> b -> (b -> b) -> b
g b
y b
i ((b -> b) -> b) -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b
i' → 
          (s ∧ b) -> b
forall a b. (a ∧ b) -> b
snd ((s ∧ b) -> b) -> (s ∧ b) -> b
forall a b. (a -> b) -> a -> b
$ (s ∧ b) -> s ∧ b
𝓀 ((s ∧ b) -> s ∧ b) -> (s ∧ b) -> s ∧ b
forall a b. (a -> b) -> a -> b
$ s
s' s -> b -> s ∧ b
forall a b. a -> b -> a ∧ b
:* b
i'

withIndex ∷ ∀ n t a. (Zero n,One n,Plus n,ToIter a t) ⇒ t → 𝐼 (n ∧ a)
withIndex :: forall n t a. (Zero n, One n, Plus n, ToIter a t) => t -> 𝐼 (n ∧ a)
withIndex = n -> (a -> n -> n ∧ (n ∧ a)) -> t -> 𝐼 (n ∧ a)
forall a t s b. ToIter a t => s -> (a -> s -> s ∧ b) -> t -> 𝐼 b
reiter n
forall a. Zero a => a
zero ((a -> n -> n ∧ (n ∧ a)) -> t -> 𝐼 (n ∧ a))
-> (a -> n -> n ∧ (n ∧ a)) -> t -> 𝐼 (n ∧ a)
forall a b. (a -> b) -> a -> b
$ \ a
x n
i → (n
i n -> n -> n
forall a. Plus a => a -> a -> a
+ n
forall a. One a => a
one) n -> (n ∧ a) -> n ∧ (n ∧ a)
forall a b. a -> b -> a ∧ b
:* (n
i n -> a -> n ∧ a
forall a b. a -> b -> a ∧ b
:* a
x)

withFirst ∷ (ToIter a t) ⇒ t → 𝐼 (𝔹 ∧ a)
withFirst :: forall a t. ToIter a t => t -> 𝐼 (𝔹 ∧ a)
withFirst = 𝔹 -> (a -> 𝔹 -> 𝔹 ∧ (𝔹 ∧ a)) -> t -> 𝐼 (𝔹 ∧ a)
forall a t s b. ToIter a t => s -> (a -> s -> s ∧ b) -> t -> 𝐼 b
reiter 𝔹
True ((a -> 𝔹 -> 𝔹 ∧ (𝔹 ∧ a)) -> t -> 𝐼 (𝔹 ∧ a))
-> (a -> 𝔹 -> 𝔹 ∧ (𝔹 ∧ a)) -> t -> 𝐼 (𝔹 ∧ a)
forall a b. (a -> b) -> a -> b
$ \ a
x 𝔹
b → 𝔹
False 𝔹 -> (𝔹 ∧ a) -> 𝔹 ∧ (𝔹 ∧ a)
forall a b. a -> b -> a ∧ b
:* (𝔹
b 𝔹 -> a -> 𝔹 ∧ a
forall a b. a -> b -> a ∧ b
:* a
x)

mapFirst ∷ (ToIter a t) ⇒ (a → a) → t → 𝐼 a
mapFirst :: forall a t. ToIter a t => (a -> a) -> t -> 𝐼 a
mapFirst a -> a
f = 𝔹 -> (a -> 𝔹 -> 𝔹 ∧ a) -> t -> 𝐼 a
forall a t s b. ToIter a t => s -> (a -> s -> s ∧ b) -> t -> 𝐼 b
reiter 𝔹
True ((a -> 𝔹 -> 𝔹 ∧ a) -> t -> 𝐼 a) -> (a -> 𝔹 -> 𝔹 ∧ a) -> t -> 𝐼 a
forall a b. (a -> b) -> a -> b
$ \ a
x 𝔹
b → 
  let x' :: a
x' = if 𝔹
b then a -> a
f a
x else a
x 
  in 𝔹
False 𝔹 -> a -> 𝔹 ∧ a
forall a b. a -> b -> a ∧ b
:* a
x'

mapAfterFirst ∷ (ToIter a t) ⇒ (a → a) → t → 𝐼 a
mapAfterFirst :: forall a t. ToIter a t => (a -> a) -> t -> 𝐼 a
mapAfterFirst a -> a
f = 𝔹 -> (a -> 𝔹 -> 𝔹 ∧ a) -> t -> 𝐼 a
forall a t s b. ToIter a t => s -> (a -> s -> s ∧ b) -> t -> 𝐼 b
reiter 𝔹
True ((a -> 𝔹 -> 𝔹 ∧ a) -> t -> 𝐼 a) -> (a -> 𝔹 -> 𝔹 ∧ a) -> t -> 𝐼 a
forall a b. (a -> b) -> a -> b
$ \ a
x 𝔹
b → 
  let x' :: a
x' = if 𝔹
b then a
x else a -> a
f a
x 
  in 𝔹
False 𝔹 -> a -> 𝔹 ∧ a
forall a b. a -> b -> a ∧ b
:* a
x'

keepN ∷ (ToIter a t,Eq n,Zero n,One n,Plus n) ⇒ n → t → 𝐼 a
keepN :: forall a t n.
(ToIter a t, Eq n, Zero n, One n, Plus n) =>
n -> t -> 𝐼 a
keepN n
n₀ t
xs = (forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
forall a.
(forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
𝐼 ((forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
 -> 𝐼 a)
-> (forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
-> 𝐼 a
forall a b. (a -> b) -> a -> b
HS.$ \ a -> b -> (b -> b) -> b
f b
i₀ b -> b
𝓀₀ → 
  let g :: a -> (n ∧ b) -> ((n ∧ b) -> n ∧ b) -> n ∧ b
g a
x (n
n :* b
i) (n ∧ b) -> n ∧ b
𝓀 = (n -> n
forall a. (One a, Plus a) => a -> a
succ n
n n -> b -> n ∧ b
forall a b. a -> b -> a ∧ b
:*) (b -> n ∧ b) -> b -> n ∧ b
forall a b. (a -> b) -> a -> b
$
        if n
n n -> n -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ n
n₀
        then b -> b
𝓀₀ b
i
        else a -> b -> (b -> b) -> b
f a
x b
i ((b -> b) -> b) -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ (n ∧ b) -> b
forall a b. (a ∧ b) -> b
snd ((n ∧ b) -> b) -> ((n ∧ b) -> n ∧ b) -> (n ∧ b) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (n ∧ b) -> n ∧ b
𝓀 ((n ∧ b) -> b) -> (b -> n ∧ b) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (n -> n
forall a. (One a, Plus a) => a -> a
succ n
n n -> b -> n ∧ b
forall a b. a -> b -> a ∧ b
:*)
  in (n ∧ b) -> b
forall a b. (a ∧ b) -> b
snd ((n ∧ b) -> b) -> (n ∧ b) -> b
forall a b. (a -> b) -> a -> b
$ 𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
forall a.
𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
un𝐼 (t -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter t
xs) a -> (n ∧ b) -> ((n ∧ b) -> n ∧ b) -> n ∧ b
g (n
forall a. Zero a => a
zero n -> b -> n ∧ b
forall a b. a -> b -> a ∧ b
:* b
i₀) (((n ∧ b) -> n ∧ b) -> n ∧ b) -> ((n ∧ b) -> n ∧ b) -> n ∧ b
forall a b. (a -> b) -> a -> b
$ (b -> b) -> (n ∧ b) -> n ∧ b
forall b₁ b₂ a. (b₁ -> b₂) -> (a ∧ b₁) -> a ∧ b₂
mapSnd b -> b
𝓀₀

withLast ∷ (ToIter a t) ⇒ t → 𝐼 (𝔹 ∧ a)
withLast :: forall a t. ToIter a t => t -> 𝐼 (𝔹 ∧ a)
withLast = 𝐼 (𝔹 ∧ a) -> 𝐼 (𝔹 ∧ a)
forall a t. ToIter a t => t -> 𝐼 a
reverse (𝐼 (𝔹 ∧ 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)
withFirst (𝐼 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
reverse

mapLast ∷ (ToIter a t) ⇒ (a → a) → t → 𝐼 a
mapLast :: forall a t. ToIter a t => (a -> a) -> t -> 𝐼 a
mapLast a -> a
f = ((𝔹 ∧ a) -> a) -> 𝐼 (𝔹 ∧ a) -> 𝐼 a
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (\ (𝔹
b :* a
x) → case 𝔹
b of {𝔹
True → a -> a
f a
x;𝔹
False → a
x}) (𝐼 (𝔹 ∧ 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)
withLast

mapLastOn ∷ (ToIter a t) ⇒ t → (a → a) → 𝐼 a
mapLastOn :: forall a t. ToIter a t => t -> (a -> a) -> 𝐼 a
mapLastOn = ((a -> a) -> t -> 𝐼 a) -> t -> (a -> a) -> 𝐼 a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> a) -> t -> 𝐼 a
forall a t. ToIter a t => (a -> a) -> t -> 𝐼 a
mapLast

mapBeforeLast ∷ (ToIter a t) ⇒ (a → a) → t → 𝐼 a
mapBeforeLast :: forall a t. ToIter a t => (a -> a) -> t -> 𝐼 a
mapBeforeLast a -> a
f = ((𝔹 ∧ a) -> a) -> 𝐼 (𝔹 ∧ a) -> 𝐼 a
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (\ (𝔹
b :* a
x) → case 𝔹
b of {𝔹
True → a
x;𝔹
False → a -> a
f a
x}) (𝐼 (𝔹 ∧ 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)
withLast

filterMap ∷ (ToIter a t) ⇒ (a → 𝑂 b) → t → 𝐼 b
filterMap :: forall a t b. ToIter a t => (a -> 𝑂 b) -> t -> 𝐼 b
filterMap a -> 𝑂 b
f t
xs = (forall b. (b -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 b
forall a.
(forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
𝐼 ((forall b. (b -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
 -> 𝐼 b)
-> (forall b. (b -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
-> 𝐼 b
forall a b. (a -> b) -> a -> b
HS.$ \ b -> b -> (b -> b) -> b
g →
  𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
forall a.
𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
un𝐼 (t -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter t
xs) ((a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
-> (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ a
x b
i b -> b
𝓀 → 
    case a -> 𝑂 b
f a
x of
      𝑂 b
None → b -> b
𝓀 b
i
      Some b
y → b -> b -> (b -> b) -> b
g b
y b
i b -> b
𝓀

filterMapOn ∷ (ToIter a t) ⇒ t → (a → 𝑂 b) → 𝐼 b
filterMapOn :: forall a t b. ToIter a t => t -> (a -> 𝑂 b) -> 𝐼 b
filterMapOn = ((a -> 𝑂 b) -> t -> 𝐼 b) -> t -> (a -> 𝑂 b) -> 𝐼 b
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> 𝑂 b) -> t -> 𝐼 b
forall a t b. ToIter a t => (a -> 𝑂 b) -> t -> 𝐼 b
filterMap

filter ∷ (ToIter a t) ⇒ (a → 𝔹) → t → 𝐼 a
filter :: forall a t. ToIter a t => (a -> 𝔹) -> t -> 𝐼 a
filter a -> 𝔹
f = (a -> 𝑂 a) -> t -> 𝐼 a
forall a t b. ToIter a t => (a -> 𝑂 b) -> t -> 𝐼 b
filterMap ((a -> 𝑂 a) -> t -> 𝐼 a) -> (a -> 𝑂 a) -> t -> 𝐼 a
forall a b. (a -> b) -> a -> b
$ \ a
x → case a -> 𝔹
f a
x of {𝔹
True → a -> 𝑂 a
forall a. a -> 𝑂 a
Some a
x;𝔹
False → 𝑂 a
forall a. 𝑂 a
None}

filterOn ∷ (ToIter a t) ⇒ t → (a → 𝔹) → 𝐼 a
filterOn :: forall a t. ToIter a t => t -> (a -> 𝔹) -> 𝐼 a
filterOn = ((a -> 𝔹) -> t -> 𝐼 a) -> t -> (a -> 𝔹) -> 𝐼 a
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> 𝔹) -> t -> 𝐼 a
forall a t. ToIter a t => (a -> 𝔹) -> t -> 𝐼 a
filter

inbetween ∷ (ToIter a t) ⇒ a → t → 𝐼 a
inbetween :: forall a t. ToIter a t => a -> t -> 𝐼 a
inbetween a
xⁱ t
xs = (forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
forall a.
(forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
𝐼 ((forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
 -> 𝐼 a)
-> (forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
-> 𝐼 a
forall a b. (a -> b) -> a -> b
HS.$ \ a -> b -> (b -> b) -> b
f →
  𝐼 (𝔹 ∧ a)
-> forall b. ((𝔹 ∧ a) -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
forall a.
𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
un𝐼 (𝐼 a -> 𝐼 (𝔹 ∧ a)
forall a t. ToIter a t => t -> 𝐼 (𝔹 ∧ a)
withFirst (𝐼 a -> 𝐼 (𝔹 ∧ a)) -> 𝐼 a -> 𝐼 (𝔹 ∧ a)
forall a b. (a -> b) -> a -> b
$ t -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter t
xs) (((𝔹 ∧ a) -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
-> ((𝔹 ∧ a) -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ (𝔹
b :* a
x) b
i b -> b
𝓀 →
    if 𝔹
b 
    then a -> b -> (b -> b) -> b
f a
x b
i b -> b
𝓀
    else 
      a -> b -> (b -> b) -> b
f a
xⁱ b
i ((b -> b) -> b) -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b
i' →
      a -> b -> (b -> b) -> b
f a
x b
i' b -> b
𝓀

alignLeftFill ∷ ℂ → ℕ → 𝕊 → 𝕊
alignLeftFill :: ℂ -> ℕ -> 𝕊 -> 𝕊
alignLeftFill ℂ
c ℕ
n 𝕊
s = 𝐼 𝕊 -> 𝕊
forall t. ToIter 𝕊 t => t -> 𝕊
build𝕊S (𝐼 𝕊 -> 𝕊) -> 𝐼 𝕊 -> 𝕊
forall a b. (a -> b) -> a -> b
$ [𝐼 𝕊] -> 𝐼 𝕊
forall a t. (Monoid a, ToIter a t) => t -> a
concat
  [ 𝕊 -> 𝐼 𝕊
forall a. a -> 𝐼 a
single𝐼 𝕊
s
  , 𝕊 -> 𝐼 𝕊
forall a. a -> 𝐼 a
single𝐼 (𝕊 -> 𝐼 𝕊) -> 𝕊 -> 𝐼 𝕊
forall a b. (a -> b) -> a -> b
$ 𝐼 ℂ -> 𝕊
forall t. ToIter ℂ t => t -> 𝕊
string (𝐼 ℂ -> 𝕊) -> 𝐼 ℂ -> 𝕊
forall a b. (a -> b) -> a -> b
$ ℕ -> ℂ -> 𝐼 ℂ
forall n a. (Eq n, Zero n, One n, Plus n) => n -> a -> 𝐼 a
replicate (ℕ
n ℕ -> ℕ -> ℕ
forall a. Minus a => a -> a -> a
- 𝕊 -> ℕ
length𝕊 𝕊
s ℕ -> ℕ -> ℕ
forall a. Meet a => a -> a -> a
⊓ ℕ
n) ℂ
c
  ]

alignLeft ∷ ℕ → 𝕊 → 𝕊
alignLeft :: ℕ -> 𝕊 -> 𝕊
alignLeft = ℂ -> ℕ -> 𝕊 -> 𝕊
alignLeftFill ℂ
' '

alignRightFill ∷ ℂ → ℕ → 𝕊 → 𝕊
alignRightFill :: ℂ -> ℕ -> 𝕊 -> 𝕊
alignRightFill ℂ
c ℕ
n 𝕊
s = 𝐼 𝕊 -> 𝕊
forall t. ToIter 𝕊 t => t -> 𝕊
build𝕊S (𝐼 𝕊 -> 𝕊) -> 𝐼 𝕊 -> 𝕊
forall a b. (a -> b) -> a -> b
$ [𝐼 𝕊] -> 𝐼 𝕊
forall a t. (Monoid a, ToIter a t) => t -> a
concat
  [ 𝕊 -> 𝐼 𝕊
forall a. a -> 𝐼 a
single𝐼 (𝕊 -> 𝐼 𝕊) -> 𝕊 -> 𝐼 𝕊
forall a b. (a -> b) -> a -> b
$ 𝐼 ℂ -> 𝕊
forall t. ToIter ℂ t => t -> 𝕊
string (𝐼 ℂ -> 𝕊) -> 𝐼 ℂ -> 𝕊
forall a b. (a -> b) -> a -> b
$ ℕ -> ℂ -> 𝐼 ℂ
forall n a. (Eq n, Zero n, One n, Plus n) => n -> a -> 𝐼 a
replicate (ℕ
n ℕ -> ℕ -> ℕ
forall a. Minus a => a -> a -> a
- 𝕊 -> ℕ
length𝕊 𝕊
s ℕ -> ℕ -> ℕ
forall a. Meet a => a -> a -> a
⊓ ℕ
n) ℂ
c
  , 𝕊 -> 𝐼 𝕊
forall a. a -> 𝐼 a
single𝐼 𝕊
s
  ]

alignRight ∷ ℕ → 𝕊 → 𝕊
alignRight :: ℕ -> 𝕊 -> 𝕊
alignRight = ℂ -> ℕ -> 𝕊 -> 𝕊
alignRightFill ℂ
' '

list ∷ (ToIter a t) ⇒ t → 𝐿 a
list :: forall a t. ToIter a t => t -> 𝐿 a
list = 𝐼 a -> 𝐿 a
forall a. 𝐼 a -> 𝐿 a
list𝐼 (𝐼 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

lazyList ∷ (ToIter a t) ⇒ t → [a]
lazyList :: forall a t. ToIter a t => t -> [a]
lazyList = 𝐼 a -> [a]
forall a. 𝐼 a -> [a]
lazyList𝐼 (𝐼 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

string ∷ (ToIter ℂ t) ⇒ t → 𝕊
string :: forall t. ToIter ℂ t => t -> 𝕊
string = t -> 𝕊
forall t. ToIter ℂ t => t -> 𝕊
build𝕊C

stringS ∷ (ToIter 𝕊 t) ⇒ t → 𝕊
stringS :: forall t. ToIter 𝕊 t => t -> 𝕊
stringS = t -> 𝕊
forall t. ToIter 𝕊 t => t -> 𝕊
build𝕊S

truncate𝕊 ∷ ℕ64 → 𝕊 → 𝕊 → 𝕊
truncate𝕊 :: ℕ64 -> 𝕊 -> 𝕊 -> 𝕊
truncate𝕊 ℕ64
n 𝕊
t 𝕊
s =
  if ℕ -> ℕ64
forall a. (ToNatO64 a, STACK) => a -> ℕ64
natΩ64 (𝕊 -> ℕ
length𝕊 𝕊
s) ℕ64 -> ℕ64 -> 𝔹
forall a. Ord a => a -> a -> 𝔹
≤ ℕ64
n
  then 𝕊
s
  else 𝐼 ℂ -> 𝕊
forall t. ToIter ℂ t => t -> 𝕊
string (𝐼 ℂ -> 𝕊) -> 𝐼 ℂ -> 𝕊
forall a b. (a -> b) -> a -> b
$ ℕ64 -> 𝕊 -> 𝐼 ℂ
forall a t n.
(ToIter a t, Eq n, Zero n, One n, Plus n) =>
n -> t -> 𝐼 a
keepN ℕ64
n 𝕊
s 𝐼 ℂ -> 𝐼 ℂ -> 𝐼 ℂ
forall a. Append a => a -> a -> a
⧺ 𝕊 -> 𝐼 ℂ
forall a t. ToIter a t => t -> 𝐼 a
iter 𝕊
t

showCollection ∷ (ToIter a t) ⇒ 𝕊 → 𝕊 → 𝕊 → (a → 𝕊) → t → 𝕊
showCollection :: forall a t. ToIter a t => 𝕊 -> 𝕊 -> 𝕊 -> (a -> 𝕊) -> t -> 𝕊
showCollection 𝕊
l 𝕊
r 𝕊
i a -> 𝕊
showA t
xs = [𝕊] -> 𝕊
forall a t. (Monoid a, ToIter a t) => t -> a
concat
  [ 𝕊
l
  , 𝐼 𝕊 -> 𝕊
forall a t. (Monoid a, ToIter a t) => t -> a
concat (𝐼 𝕊 -> 𝕊) -> 𝐼 𝕊 -> 𝕊
forall a b. (a -> b) -> a -> b
$ 𝕊 -> 𝐼 𝕊 -> 𝐼 𝕊
forall a t. ToIter a t => a -> t -> 𝐼 a
inbetween 𝕊
i (𝐼 𝕊 -> 𝐼 𝕊) -> 𝐼 𝕊 -> 𝐼 𝕊
forall a b. (a -> b) -> a -> b
$ (a -> 𝕊) -> 𝐼 a -> 𝐼 𝕊
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> 𝕊
showA (𝐼 a -> 𝐼 𝕊) -> 𝐼 a -> 𝐼 𝕊
forall a b. (a -> b) -> a -> b
$ t -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter t
xs
  , 𝕊
r
  ]

showWith𝐼 ∷ (a → 𝕊) → 𝐼 a → 𝕊
showWith𝐼 :: forall a. (a -> 𝕊) -> 𝐼 a -> 𝕊
showWith𝐼 = 𝕊 -> 𝕊 -> 𝕊 -> (a -> 𝕊) -> 𝐼 a -> 𝕊
forall a t. ToIter a t => 𝕊 -> 𝕊 -> 𝕊 -> (a -> 𝕊) -> t -> 𝕊
showCollection 𝕊
"𝐼[" 𝕊
"]" 𝕊
","

firstMaxByLT ∷ (ToIter a t) ⇒ (a → a → 𝔹) → t → 𝑂 a
firstMaxByLT :: forall a t. ToIter a t => (a -> a -> 𝔹) -> t -> 𝑂 a
firstMaxByLT a -> a -> 𝔹
f = 𝑂 a -> (a -> 𝑂 a -> 𝑂 a) -> t -> 𝑂 a
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
fold 𝑂 a
forall a. 𝑂 a
None ((a -> 𝑂 a -> 𝑂 a) -> t -> 𝑂 a) -> (a -> 𝑂 a -> 𝑂 a) -> t -> 𝑂 a
forall a b. (a -> b) -> a -> b
$ \ a
x 𝑂 a
xM →
  case 𝑂 a
xM of
    𝑂 a
None → a -> 𝑂 a
forall a. a -> 𝑂 a
Some a
x
    Some a
x' → case a -> a -> 𝔹
f a
x' a
x of
      𝔹
True → a -> 𝑂 a
forall a. a -> 𝑂 a
Some a
x
      𝔹
False → a -> 𝑂 a
forall a. a -> 𝑂 a
Some a
x'

sortWith ∷ (ToIter a t) ⇒ (a → a → Ordering) → t → 𝐿 a
sortWith :: forall a t. ToIter a t => (a -> a -> Ordering) -> t -> 𝐿 a
sortWith a -> a -> Ordering
f = [a] -> 𝐿 a
forall a t. ToIter a t => t -> 𝐿 a
list ([a] -> 𝐿 a) -> ([a] -> [a]) -> [a] -> 𝐿 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (a -> a -> Ordering) -> [a] -> [a]
forall a. (a -> a -> Ordering) -> [a] -> [a]
HS.sortBy a -> a -> Ordering
f ([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]
lazyList

sortOn ∷ (ToIter a t,Ord b) ⇒ (a → b) → t → 𝐿 a
sortOn :: forall a t b. (ToIter a t, Ord b) => (a -> b) -> t -> 𝐿 a
sortOn a -> b
f = (a -> a -> Ordering) -> t -> 𝐿 a
forall a t. ToIter a t => (a -> a -> Ordering) -> t -> 𝐿 a
sortWith ((a -> a -> Ordering) -> t -> 𝐿 a)
-> (a -> a -> Ordering) -> t -> 𝐿 a
forall a b. (a -> b) -> a -> b
$ b -> b -> Ordering
forall a. Ord a => a -> a -> Ordering
(⋚) (b -> b -> Ordering) -> (a -> b) -> a -> a -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` a -> b
f

sort ∷ (ToIter a t,Ord a) ⇒ t → 𝐿 a
sort :: forall a t. (ToIter a t, Ord a) => t -> 𝐿 a
sort = (a -> a -> Ordering) -> t -> 𝐿 a
forall a t. ToIter a t => (a -> a -> Ordering) -> t -> 𝐿 a
sortWith a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
(⋚)

materialize ∷ (ToIter a t) ⇒ t → 𝐼 a
materialize :: forall a t. ToIter a t => t -> 𝐼 a
materialize = 𝐿 a -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter (𝐿 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
list

mapWhile ∷ (a → a) → (a → 𝔹) → 𝐼 a → 𝐼 a
mapWhile :: forall a. (a -> a) -> (a -> 𝔹) -> 𝐼 a -> 𝐼 a
mapWhile a -> a
f a -> 𝔹
p = 𝔹 -> (a -> 𝔹 -> 𝔹 ∧ a) -> 𝐼 a -> 𝐼 a
forall a t s b. ToIter a t => s -> (a -> s -> s ∧ b) -> t -> 𝐼 b
reiter 𝔹
True ((a -> 𝔹 -> 𝔹 ∧ a) -> 𝐼 a -> 𝐼 a)
-> (a -> 𝔹 -> 𝔹 ∧ a) -> 𝐼 a -> 𝐼 a
forall a b. (a -> b) -> a -> b
$ \ a
x 𝔹
b → do
  if 𝔹
b 𝔹 -> 𝔹 -> 𝔹
⩓ a -> 𝔹
p a
x
  then 𝔹
True 𝔹 -> a -> 𝔹 ∧ a
forall a b. a -> b -> a ∧ b
:* a -> a
f a
x
  else 𝔹
False 𝔹 -> a -> 𝔹 ∧ a
forall a b. a -> b -> a ∧ b
:* a
x

dropWhile ∷ (a → 𝔹) → 𝐼 a → 𝐼 a
dropWhile :: forall a. (a -> 𝔹) -> 𝐼 a -> 𝐼 a
dropWhile a -> 𝔹
p 𝐼 a
xs₀ =
  let loop :: 𝑂 (a ∧ 𝑆 a) -> 𝐼 a
loop = \case
        𝑂 (a ∧ 𝑆 a)
None → 𝐼 a
forall a. Null a => a
null
        Some (a
x :* 𝑆 a
xs')
          | a -> 𝔹
p a
x → 𝑂 (a ∧ 𝑆 a) -> 𝐼 a
loop (𝑂 (a ∧ 𝑆 a) -> 𝐼 a) -> 𝑂 (a ∧ 𝑆 a) -> 𝐼 a
forall a b. (a -> b) -> a -> b
$ 𝑆 a -> () -> 𝑂 (a ∧ 𝑆 a)
forall a. 𝑆 a -> () -> 𝑂 (a ∧ 𝑆 a)
un𝑆 𝑆 a
xs' ()
          | 𝔹
otherwise → 𝑆 a -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter (𝑆 a -> 𝐼 a) -> 𝑆 a -> 𝐼 a
forall a b. (a -> b) -> a -> b
$ (() -> 𝑂 (a ∧ 𝑆 a)) -> 𝑆 a
forall a. (() -> 𝑂 (a ∧ 𝑆 a)) -> 𝑆 a
𝑆 ((() -> 𝑂 (a ∧ 𝑆 a)) -> 𝑆 a) -> (() -> 𝑂 (a ∧ 𝑆 a)) -> 𝑆 a
forall a b. (a -> b) -> a -> b
$ \ () → (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
x a -> 𝑆 a -> a ∧ 𝑆 a
forall a b. a -> b -> a ∧ b
:* 𝑆 a
xs'
  in 𝑂 (a ∧ 𝑆 a) -> 𝐼 a
loop (𝑂 (a ∧ 𝑆 a) -> 𝐼 a) -> 𝑂 (a ∧ 𝑆 a) -> 𝐼 a
forall a b. (a -> b) -> a -> b
$ 𝑆 a -> () -> 𝑂 (a ∧ 𝑆 a)
forall a. 𝑆 a -> () -> 𝑂 (a ∧ 𝑆 a)
un𝑆 (𝐼 a -> 𝑆 a
forall a t. ToIter a t => t -> 𝑆 a
stream 𝐼 a
xs₀) ()

---------
-- All --
---------

instance All () where
  all :: 𝐼 ()
all = () -> 𝐼 ()
forall a t. Single a t => a -> t
single ()

instance All 𝔹 where 
  all :: 𝐼 𝔹
all = [𝔹] -> 𝐼 𝔹
forall a t. ToIter a t => t -> 𝐼 a
iter [𝔹
True,𝔹
False]

instance (All a) ⇒ All (𝑂 a) where
  all :: 𝐼 (𝑂 a)
all = 𝑂 a -> 𝐼 (𝑂 a)
forall a t. Single a t => a -> t
single 𝑂 a
forall a. 𝑂 a
None 𝐼 (𝑂 a) -> 𝐼 (𝑂 a) -> 𝐼 (𝑂 a)
forall a. Append a => a -> a -> a
⧺ (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. a -> 𝑂 a
Some 𝐼 a
forall a. All a => 𝐼 a
all

instance (All a,All b) ⇒ All (a ∨ b) where
  all :: 𝐼 (a ∨ b)
all = (a -> a ∨ b) -> 𝐼 a -> 𝐼 (a ∨ b)
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> a ∨ b
forall a b. a -> a ∨ b
Inl 𝐼 a
forall a. All a => 𝐼 a
all 𝐼 (a ∨ b) -> 𝐼 (a ∨ b) -> 𝐼 (a ∨ b)
forall a. Append a => a -> a -> a
⧺ (b -> a ∨ b) -> 𝐼 b -> 𝐼 (a ∨ b)
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map b -> a ∨ b
forall a b. b -> a ∨ b
Inr 𝐼 b
forall a. All a => 𝐼 a
all

instance (All a,All b) ⇒ All (a ∧ b) where 
  all :: 𝐼 (a ∧ b)
all = do a
x ← 𝐼 a
forall a. All a => 𝐼 a
all ; b
y ← 𝐼 b
forall a. All a => 𝐼 a
all ; (a ∧ b) -> 𝐼 (a ∧ b)
forall a. a -> 𝐼 a
forall (m :: * -> *) a. Return m => a -> m a
return ((a ∧ b) -> 𝐼 (a ∧ b)) -> (a ∧ b) -> 𝐼 (a ∧ b)
forall a b. (a -> b) -> a -> b
$ a
x a -> b -> a ∧ b
forall a b. a -> b -> a ∧ b
:* b
y


----