module UVMHS.Core.Data.Iter where

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

import UVMHS.Core.Data.Arithmetic
import UVMHS.Core.Data.Choice
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 (Eq a) ⇒ Eq (𝐼 a) where == :: 𝐼 a -> 𝐼 a -> Bool
(==) = 𝑆 a -> 𝑆 a -> Bool
forall a. Eq a => a -> a -> Bool
(≡) (𝑆 a -> 𝑆 a -> Bool) -> (𝐼 a -> 𝑆 a) -> 𝐼 a -> 𝐼 a -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` 𝐼 a -> 𝑆 a
forall a t. ToIter a t => t -> 𝑆 a
stream
instance (Ord a) ⇒ Ord (𝐼 a) where compare :: 𝐼 a -> 𝐼 a -> Ordering
compare = 𝑆 a -> 𝑆 a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (𝑆 a -> 𝑆 a -> Ordering) -> (𝐼 a -> 𝑆 a) -> 𝐼 a -> 𝐼 a -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` 𝐼 a -> 𝑆 a
forall a t. ToIter a t => t -> 𝑆 a
stream

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 Lookup ℕ64  a (𝐼 a) where ⋕? :: 𝐼 a -> ℕ64 -> 𝑂 a
(⋕?) = (ℕ64 -> 𝐼 a -> 𝑂 a) -> 𝐼 a -> ℕ64 -> 𝑂 a
forall a b c. (a -> b -> c) -> b -> a -> c
flip ℕ64 -> 𝐼 a -> 𝑂 a
forall a. ℕ64 -> 𝐼 a -> 𝑂 a
lookup𝐼

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
yield b
i b -> b
done →
  a -> b -> (b -> b) -> b
yield 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
yield b
i' b -> b
done

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
yield b
i b -> b
done →
  𝐼 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
yield b
i ((b -> b) -> b) -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b
i' →
  a -> b -> (b -> b) -> b
yield a
x b
i' b -> b
done

isEmpty ∷ (ToIter a t) ⇒ t → 𝔹
isEmpty :: forall a t. ToIter a t => t -> Bool
isEmpty t
xs = 𝐼 a
-> (Bool -> Bool)
-> Bool
-> (a -> Bool -> (Bool -> Bool) -> Bool)
-> Bool
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) Bool -> Bool
forall a. a -> a
id Bool
True ((a -> Bool -> (Bool -> Bool) -> Bool) -> Bool)
-> (a -> Bool -> (Bool -> Bool) -> Bool) -> Bool
forall a b. (a -> b) -> a -> b
$ \ a
_ Bool
_ Bool -> Bool
_ → Bool
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
yield b
i b -> b
done →
  𝐼 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
yield 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
yield b
i' b -> b
done

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
𝐼 ((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
yield ∷ b → c → (c → c) → c) (b
i₀ ∷ c) (b -> b
done ∷ c → c) →
  let yield' ∷ a → c → (c → c) → c
      yield' :: a -> b -> (b -> b) -> b
yield' a
x b
i b -> b
continue = 𝐼 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
yield b
i b -> b
continue
  in 
  𝐼 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
yield' b
i₀ b -> b
done

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 = 𝐼 b -> (a -> 𝐼 b -> m (𝐼 b)) -> 𝐼 a -> m (𝐼 b)
forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> m b) -> t -> m b
mfoldFromWith 𝐼 b
forall a. Null a => a
null ((a -> 𝐼 b -> m (𝐼 b)) -> 𝐼 a -> m (𝐼 b))
-> (a -> 𝐼 b -> m (𝐼 b)) -> 𝐼 a -> m (𝐼 b)
forall a b. (a -> b) -> a -> b
$ \ a
x 𝐼 b
ys → do
  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
k → do b
i ← m b
iM ; m b -> m b
k (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
k → do b
i ← m b
iM ; a -> b -> (m b -> m b) -> m b
f a
x b
i m b -> m b
k

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
k → do b
i ← m b -> m b
k 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 Bool t => t -> Bool
or = Bool -> (Bool -> Bool -> (Bool -> Bool) -> Bool) -> t -> Bool
forall a t b.
ToIter a t =>
b -> (a -> b -> (b -> b) -> b) -> t -> b
foldk Bool
False ((Bool -> Bool -> (Bool -> Bool) -> Bool) -> t -> Bool)
-> (Bool -> Bool -> (Bool -> Bool) -> Bool) -> t -> Bool
forall a b. (a -> b) -> a -> b
$ \ Bool
b₁ Bool
b₂ Bool -> Bool
k → if Bool
b₁ then Bool
True else Bool -> Bool
k Bool
b₂

orf ∷ (ToIter (a → 𝔹) t) ⇒ t → a → 𝔹
orf :: forall a t. ToIter (a -> Bool) t => t -> a -> Bool
orf t
fs a
x = 𝐼 Bool -> Bool
forall t. ToIter Bool t => t -> Bool
or (𝐼 Bool -> Bool) -> 𝐼 Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ((a -> Bool) -> Bool) -> 𝐼 (a -> Bool) -> 𝐼 Bool
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (a -> (a -> Bool) -> Bool
forall a b. a -> (a -> b) -> b
appto a
x) (𝐼 (a -> Bool) -> 𝐼 Bool) -> 𝐼 (a -> Bool) -> 𝐼 Bool
forall a b. (a -> b) -> a -> b
$ t -> 𝐼 (a -> Bool)
forall a t. ToIter a t => t -> 𝐼 a
iter t
fs

andf ∷ (ToIter (a → 𝔹) t) ⇒ t → a → 𝔹
andf :: forall a t. ToIter (a -> Bool) t => t -> a -> Bool
andf t
fs a
x = 𝐼 Bool -> Bool
forall t. ToIter Bool t => t -> Bool
and (𝐼 Bool -> Bool) -> 𝐼 Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ((a -> Bool) -> Bool) -> 𝐼 (a -> Bool) -> 𝐼 Bool
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (a -> (a -> Bool) -> Bool
forall a b. a -> (a -> b) -> b
appto a
x) (𝐼 (a -> Bool) -> 𝐼 Bool) -> 𝐼 (a -> Bool) -> 𝐼 Bool
forall a b. (a -> b) -> a -> b
$ t -> 𝐼 (a -> Bool)
forall a t. ToIter a t => t -> 𝐼 a
iter t
fs

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

eqs ∷ (Eq a,ToIter a t) ⇒ t → 𝔹
eqs :: forall a t. (Eq a, ToIter a t) => t -> Bool
eqs t
xs = case 𝑆 a -> () -> 𝑂 (a ∧ 𝑆 a)
forall a. 𝑆 a -> () -> 𝑂 (a ∧ 𝑆 a)
un𝑆 (t -> 𝑆 a
forall a t. ToIter a t => t -> 𝑆 a
stream t
xs) () of
  𝑂 (a ∧ 𝑆 a)
None → Bool
True
  Some (a
x :* 𝑆 a
xs') → 𝑆 Bool -> Bool
forall t. ToIter Bool t => t -> Bool
and (𝑆 Bool -> Bool) -> 𝑆 Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (a -> Bool) -> 𝑆 a -> 𝑆 Bool
forall a b. (a -> b) -> 𝑆 a -> 𝑆 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(≡) a
x) 𝑆 a
xs'

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 -> Bool) -> t -> n
countWith a -> Bool
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 -> Bool
f a
x of
  Bool
True → n -> n
forall a. (One a, Plus a) => a -> a
succ
  Bool
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
yield b
i₀ b -> b
done → 𝐼 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
k (b -> b) -> b -> b
k' → (b -> b) -> b -> b
k' ((b -> b) -> b -> b) -> (b -> b) -> b -> b
forall a b. (a -> b) -> a -> b
$ \ b
i → a -> b -> (b -> b) -> b
yield a
x b
i b -> b
k) b -> b
done (b -> b) -> b -> b
forall a. a -> a
id b
i₀
-- NOTE: this definition would be equivalent to the identify function
-- fancyIterID xs = 𝐼 HS.$ \ yield i₀ done → un𝐼 (iter xs) (\ x k k' → \ i → yield x i $ k' k) done id 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
gen = (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
yield b
i₀ b -> b
done →
  let loop :: n -> b -> b
loop n
n b
i
        | n
n n -> n -> Bool
forall a. Eq a => a -> a -> Bool
≡ n
n₀ = b -> b
done b
i
        | Bool
otherwise =
            a -> b -> (b -> b) -> b
yield (n -> a
gen 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 b
i₀

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
gen = (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
yield b
i₀ b -> b
done →
  let loop :: n -> a -> b -> b
loop n
n a
x b
i
        | n
n n -> n -> Bool
forall a. Eq a => a -> a -> Bool
≡ n
n₀ = b -> b
done b
i
        | Bool
otherwise =
            a -> b -> (b -> b) -> b
yield 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
gen a
x) b
i'
  in n -> a -> b -> b
loop n
forall a. Zero a => a
zero a
x₀ b
i₀

range ∷ (Eq n,Additive n,One n,Minus n) ⇒ n → n → 𝐼 n
range :: forall n. (Eq n, Additive n, One 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,Additive n,One n) ⇒ n → 𝐼 n
upto :: forall n. (Eq n, Additive n, One 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

uptoStep ∷ ℕ64 → ℕ64 → 𝐼 ℕ64
uptoStep :: ℕ64 -> ℕ64 -> 𝐼 ℕ64
uptoStep ℕ64
n ℕ64
step = (ℕ64 -> ℕ64) -> 𝐼 ℕ64 -> 𝐼 ℕ64
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (ℕ64 -> ℕ64 -> ℕ64
forall a. Times a => a -> a -> a
(×) ℕ64
step) (𝐼 ℕ64 -> 𝐼 ℕ64) -> 𝐼 ℕ64 -> 𝐼 ℕ64
forall a b. (a -> b) -> a -> b
$ ℕ64 -> 𝐼 ℕ64
forall n. (Eq n, Additive n, One n) => n -> 𝐼 n
upto (ℕ64 -> 𝐼 ℕ64) -> ℕ64 -> 𝐼 ℕ64
forall a b. (a -> b) -> a -> b
$ ℤ -> ℕ64
forall a. (ToNatO64 a, STACK) => a -> ℕ64
natΩ64 (ℤ -> ℕ64) -> ℤ -> ℕ64
forall a b. (a -> b) -> a -> b
$ 𝔻 -> ℤ
ceiling (𝔻 -> ℤ) -> 𝔻 -> ℤ
forall a b. (a -> b) -> a -> b
$ ℕ64 -> 𝔻
forall a. ToDouble a => a -> 𝔻
dbl ℕ64
n 𝔻 -> 𝔻 -> 𝔻
forall a. Divide a => a -> a -> a
/ ℕ64 -> 𝔻
forall a. ToDouble a => a -> 𝔻
dbl ℕ64
step

mapState𝐼 ∷ ∀ t a b s. (ToIter a t) ⇒ s → (a → s → (s ∧ b)) → t → 𝐼 b
mapState𝐼 :: forall t a b s. ToIter a t => s -> (a -> s -> s ∧ b) -> t -> 𝐼 b
mapState𝐼 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
yield ∷ b → i → (i → i) → i) (b
i₀ ∷ i) (b -> b
done ∷ i → i) →
  let 
      yield' ∷ a → s ∧ i → (s ∧ i → s ∧ i) → s ∧ i
      yield' :: a -> (s ∧ b) -> ((s ∧ b) -> s ∧ b) -> s ∧ b
yield' a
x (s
s :* b
i) (s ∧ b) -> s ∧ b
continue =
        let s
s' :* b
y = a -> s -> s ∧ b
f a
x s
s
            i'' :: b
i'' = b -> b -> (b -> b) -> b
yield 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
continue ((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'
        in 
        s
s' s -> b -> s ∧ b
forall a b. a -> b -> a ∧ b
:* b
i''
      i₀' :: s ∧ b
i₀' = s
s₀ s -> b -> s ∧ b
forall a b. a -> b -> a ∧ b
:* b
i₀
      done' ∷ s ∧ i → s ∧ i
      done' :: (s ∧ b) -> s ∧ b
done' (s
s :* b
i) = s
s s -> b -> s ∧ b
forall a b. a -> b -> a ∧ b
:* b -> b
done b
i
  in
  (s ∧ b) -> b
forall a b. (a ∧ b) -> b
snd ((s ∧ b) -> b) -> (s ∧ 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 -> (s ∧ b) -> ((s ∧ b) -> s ∧ b) -> s ∧ b
yield' s ∧ b
i₀' (s ∧ b) -> s ∧ b
done' 

mapStateOnFrom𝐼 ∷ ∀ t a b s. (ToIter a t) ⇒ t → s → (a → s → (s ∧ b)) → 𝐼 b
mapStateOnFrom𝐼 :: forall t a b s. ToIter a t => t -> s -> (a -> s -> s ∧ b) -> 𝐼 b
mapStateOnFrom𝐼 = (s -> (a -> s -> s ∧ b) -> t -> 𝐼 b)
-> t -> s -> (a -> s -> s ∧ b) -> 𝐼 b
forall a b c d. (a -> b -> c -> d) -> c -> a -> b -> d
rotateR s -> (a -> s -> s ∧ b) -> t -> 𝐼 b
forall t a b s. ToIter a t => s -> (a -> s -> s ∧ b) -> t -> 𝐼 b
mapState𝐼

mapCont𝐼 ∷ ∀ t a b. (ToIter a t) ⇒ (∀ i. a → i → (b → i → (i → i) → i) → (i → i) → (i → i) → i) → t → 𝐼 b
mapCont𝐼 :: forall t a b.
ToIter a t =>
(forall i.
 a -> i -> (b -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> t -> 𝐼 b
mapCont𝐼 forall i.
a -> i -> (b -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i
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
yield ∷ b → i → (i → i) → i) (b
i₀ ∷ i) (b -> b
done ∷ i → i) →
  let yield' ∷ a → i → (i → i) → i
      yield' :: a -> b -> (b -> b) -> b
yield' a
x b
i b -> b
continue =
        a -> b -> (b -> b -> (b -> b) -> b) -> (b -> b) -> (b -> b) -> b
forall i.
a -> i -> (b -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i
f a
x b
i b -> b -> (b -> b) -> b
yield b -> b
continue b -> b
done
  in
  𝐼 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
yield' b
i₀ b -> b
done

mapContOn𝐼 ∷ ∀ t a b. (ToIter a t) ⇒ t → (∀ i. a → i → (b → i → (i → i) → i) → (i → i) → (i → i) → i) → 𝐼 b
mapContOn𝐼 :: forall t a b.
ToIter a t =>
t
-> (forall i.
    a -> i -> (b -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> 𝐼 b
mapContOn𝐼 = ((forall i.
  a -> i -> (b -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
 -> t -> 𝐼 b)
-> t
-> (forall i.
    a -> i -> (b -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> 𝐼 b
forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall i.
 a -> i -> (b -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> t -> 𝐼 b
forall t a b.
ToIter a t =>
(forall i.
 a -> i -> (b -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> t -> 𝐼 b
mapCont𝐼

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 t a b s. ToIter a t => s -> (a -> s -> s ∧ b) -> t -> 𝐼 b
mapState𝐼 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 -> n
forall a. (One a, Plus a) => a -> a
succ n
i 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 -> 𝐼 (Bool ∧ a)
withFirst = Bool -> (a -> Bool -> Bool ∧ (Bool ∧ a)) -> t -> 𝐼 (Bool ∧ a)
forall t a b s. ToIter a t => s -> (a -> s -> s ∧ b) -> t -> 𝐼 b
mapState𝐼 Bool
True ((a -> Bool -> Bool ∧ (Bool ∧ a)) -> t -> 𝐼 (Bool ∧ a))
-> (a -> Bool -> Bool ∧ (Bool ∧ a)) -> t -> 𝐼 (Bool ∧ a)
forall a b. (a -> b) -> a -> b
$ \ a
x Bool
b → Bool
False Bool -> (Bool ∧ a) -> Bool ∧ (Bool ∧ a)
forall a b. a -> b -> a ∧ b
:* (Bool
b Bool -> a -> Bool ∧ 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 = Bool -> (a -> Bool -> Bool ∧ a) -> t -> 𝐼 a
forall t a b s. ToIter a t => s -> (a -> s -> s ∧ b) -> t -> 𝐼 b
mapState𝐼 Bool
True ((a -> Bool -> Bool ∧ a) -> t -> 𝐼 a)
-> (a -> Bool -> Bool ∧ a) -> t -> 𝐼 a
forall a b. (a -> b) -> a -> b
$ \ a
x Bool
b →
  let x' :: a
x' = if Bool
b then a -> a
f a
x else a
x
  in Bool
False Bool -> a -> Bool ∧ 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 = Bool -> (a -> Bool -> Bool ∧ a) -> t -> 𝐼 a
forall t a b s. ToIter a t => s -> (a -> s -> s ∧ b) -> t -> 𝐼 b
mapState𝐼 Bool
True ((a -> Bool -> Bool ∧ a) -> t -> 𝐼 a)
-> (a -> Bool -> Bool ∧ a) -> t -> 𝐼 a
forall a b. (a -> b) -> a -> b
$ \ a
x Bool
b →
  let x' :: a
x' = if Bool
b then a
x else a -> a
f a
x
  in Bool
False Bool -> a -> Bool ∧ a
forall a b. a -> b -> a ∧ b
:* a
x'

keepN ∷ (ToIter a t,Ord n,Zero n,One n,Plus n) ⇒ n → t → 𝐼 a
keepN :: forall a t n.
(ToIter a t, Ord n, Zero n, One n, Plus n) =>
n -> t -> 𝐼 a
keepN n
n₀ t
xs =
  𝐼 (n ∧ a)
-> (forall {i}.
    (n ∧ a)
    -> i -> (a -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> 𝐼 a
forall t a b.
ToIter a t =>
t
-> (forall i.
    a -> i -> (b -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> 𝐼 b
mapContOn𝐼 (t -> 𝐼 (n ∧ a)
forall n t a. (Zero n, One n, Plus n, ToIter a t) => t -> 𝐼 (n ∧ a)
withIndex t
xs) ((forall {i}.
  (n ∧ a)
  -> i -> (a -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
 -> 𝐼 a)
-> (forall {i}.
    (n ∧ a)
    -> i -> (a -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> 𝐼 a
forall a b. (a -> b) -> a -> b
$ \ (n
n :* a
x) i
i a -> i -> (i -> i) -> i
yield i -> i
continue i -> i
done →
    if n
n n -> n -> Bool
forall a. Ord a => a -> a -> Bool
< n
n₀ 
    then a -> i -> (i -> i) -> i
yield a
x i
i i -> i
continue
    else i -> i
done i
i 

dropN ∷ (ToIter a t,Ord n,Zero n,One n,Plus n) ⇒ n → t → 𝐼 a
dropN :: forall a t n.
(ToIter a t, Ord n, Zero n, One n, Plus n) =>
n -> t -> 𝐼 a
dropN n
n₀ t
xs =
  𝐼 (n ∧ a)
-> (forall {i}.
    (n ∧ a)
    -> i -> (a -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> 𝐼 a
forall t a b.
ToIter a t =>
t
-> (forall i.
    a -> i -> (b -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> 𝐼 b
mapContOn𝐼 (t -> 𝐼 (n ∧ a)
forall n t a. (Zero n, One n, Plus n, ToIter a t) => t -> 𝐼 (n ∧ a)
withIndex t
xs) ((forall {i}.
  (n ∧ a)
  -> i -> (a -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
 -> 𝐼 a)
-> (forall {i}.
    (n ∧ a)
    -> i -> (a -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> 𝐼 a
forall a b. (a -> b) -> a -> b
$ \ (n
n :* a
x) i
i a -> i -> (i -> i) -> i
yield i -> i
continue i -> i
_done →
    if n
n n -> n -> Bool
forall a. Ord a => a -> a -> Bool
< n
n₀
    then i -> i
continue i
i
    else a -> i -> (i -> i) -> i
yield a
x i
i i -> i
continue

withLast ∷ (ToIter a t) ⇒ t → 𝐼 (𝔹 ∧ a)
withLast :: forall a t. ToIter a t => t -> 𝐼 (Bool ∧ a)
withLast = 𝐼 (Bool ∧ a) -> 𝐼 (Bool ∧ a)
forall a t. ToIter a t => t -> 𝐼 a
reverse (𝐼 (Bool ∧ a) -> 𝐼 (Bool ∧ a))
-> (𝐼 a -> 𝐼 (Bool ∧ a)) -> 𝐼 a -> 𝐼 (Bool ∧ a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐼 a -> 𝐼 (Bool ∧ a)
forall a t. ToIter a t => t -> 𝐼 (Bool ∧ a)
withFirst (𝐼 a -> 𝐼 (Bool ∧ a)) -> (t -> 𝐼 a) -> t -> 𝐼 (Bool ∧ 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 = ((Bool ∧ a) -> a) -> 𝐼 (Bool ∧ a) -> 𝐼 a
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (\ (Bool
b :* a
x) → if Bool
b then a -> a
f a
x else a
x) (𝐼 (Bool ∧ a) -> 𝐼 a) -> (t -> 𝐼 (Bool ∧ a)) -> t -> 𝐼 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ t -> 𝐼 (Bool ∧ a)
forall a t. ToIter a t => t -> 𝐼 (Bool ∧ 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 = ((Bool ∧ a) -> a) -> 𝐼 (Bool ∧ a) -> 𝐼 a
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (\ (Bool
b :* a
x) → if Bool
b then a
x else a -> a
f a
x) (𝐼 (Bool ∧ a) -> 𝐼 a) -> (t -> 𝐼 (Bool ∧ a)) -> t -> 𝐼 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ t -> 𝐼 (Bool ∧ a)
forall a t. ToIter a t => t -> 𝐼 (Bool ∧ a)
withLast

filter ∷ (ToIter a t) ⇒ (a → 𝔹) → t → 𝐼 a
filter :: forall a t. ToIter a t => (a -> Bool) -> t -> 𝐼 a
filter a -> Bool
p = (forall i.
 a -> i -> (a -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> t -> 𝐼 a
forall t a b.
ToIter a t =>
(forall i.
 a -> i -> (b -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> t -> 𝐼 b
mapCont𝐼 ((forall i.
  a -> i -> (a -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
 -> t -> 𝐼 a)
-> (forall i.
    a -> i -> (a -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> t
-> 𝐼 a
forall a b. (a -> b) -> a -> b
$ \ a
x i
i a -> i -> (i -> i) -> i
yield i -> i
continue i -> i
_done →
  if a -> Bool
p a
x
  then a -> i -> (i -> i) -> i
yield a
x i
i i -> i
continue
  else i -> i
continue i
i

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

filterO ∷ (ToIter (𝑂 a) t) ⇒ t → 𝐼 a
filterO :: forall a t. ToIter (𝑂 a) t => t -> 𝐼 a
filterO = (forall i.
 𝑂 a -> i -> (a -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> t -> 𝐼 a
forall t a b.
ToIter a t =>
(forall i.
 a -> i -> (b -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> t -> 𝐼 b
mapCont𝐼 ((forall i.
  𝑂 a -> i -> (a -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
 -> t -> 𝐼 a)
-> (forall i.
    𝑂 a -> i -> (a -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> t
-> 𝐼 a
forall a b. (a -> b) -> a -> b
$ \ 𝑂 a
xO i
i a -> i -> (i -> i) -> i
yield i -> i
continue i -> i
_done → case 𝑂 a
xO of
  𝑂 a
None → i -> i
continue i
i
  Some a
x → a -> i -> (i -> i) -> i
yield a
x i
i i -> i
continue

filterMap ∷ (ToIter a t) ⇒ (a → 𝑂 b) → t → 𝐼 b
filterMap :: forall a t b. ToIter a t => (a -> 𝑂 b) -> t -> 𝐼 b
filterMap a -> 𝑂 b
f = 𝐼 (𝑂 b) -> 𝐼 b
forall a t. ToIter (𝑂 a) t => t -> 𝐼 a
filterO (𝐼 (𝑂 b) -> 𝐼 b) -> (𝐼 a -> 𝐼 (𝑂 b)) -> 𝐼 a -> 𝐼 b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (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 -> 𝐼 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

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

filterM ∷ (ToIter a t,Monad m) ⇒ (a → m 𝔹) → t → m (𝐼 a)
filterM :: forall a t (m :: * -> *).
(ToIter a t, Monad m) =>
(a -> m Bool) -> t -> m (𝐼 a)
filterM a -> m Bool
p = 𝐼 a -> (a -> 𝐼 a -> m (𝐼 a)) -> t -> m (𝐼 a)
forall (m :: * -> *) a t b.
(Monad m, ToIter a t) =>
b -> (a -> b -> m b) -> t -> m b
mfoldFromWith 𝐼 a
forall a. Null a => a
null ((a -> 𝐼 a -> m (𝐼 a)) -> t -> m (𝐼 a))
-> (a -> 𝐼 a -> m (𝐼 a)) -> t -> m (𝐼 a)
forall a b. (a -> b) -> a -> b
$ \ a
x 𝐼 a
xs → do
  Bool
b ← a -> m Bool
p a
x
  𝐼 a -> m (𝐼 a)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return (𝐼 a -> m (𝐼 a)) -> 𝐼 a -> m (𝐼 a)
forall a b. (a -> b) -> a -> b
$ if Bool
b then 𝐼 a -> a -> 𝐼 a
forall a. 𝐼 a -> a -> 𝐼 a
snoc𝐼 𝐼 a
xs a
x else 𝐼 a
xs

filterMOn ∷ (ToIter a t,Monad m) ⇒ t → (a → m 𝔹) → m (𝐼 a)
filterMOn :: forall a t (m :: * -> *).
(ToIter a t, Monad m) =>
t -> (a -> m Bool) -> m (𝐼 a)
filterMOn = ((a -> m Bool) -> t -> m (𝐼 a)) -> t -> (a -> m Bool) -> m (𝐼 a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> m Bool) -> t -> m (𝐼 a)
forall a t (m :: * -> *).
(ToIter a t, Monad m) =>
(a -> m Bool) -> t -> m (𝐼 a)
filterM

filterMapM ∷ (ToIter a t,Monad m) ⇒ (a → m (𝑂 b)) → t → m (𝐼 b)
filterMapM :: forall a t (m :: * -> *) b.
(ToIter a t, Monad m) =>
(a -> m (𝑂 b)) -> t -> m (𝐼 b)
filterMapM a -> m (𝑂 b)
f = 𝐼 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
mfoldFromWith 𝐼 b
forall a. Null a => a
null ((a -> 𝐼 b -> m (𝐼 b)) -> t -> m (𝐼 b))
-> (a -> 𝐼 b -> m (𝐼 b)) -> t -> m (𝐼 b)
forall a b. (a -> b) -> a -> b
$ \ a
x 𝐼 b
ys → do
  𝑂 b
yO ← 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
$ case 𝑂 b
yO of
    𝑂 b
None → 𝐼 b
ys
    Some b
y → 𝐼 b -> b -> 𝐼 b
forall a. 𝐼 a -> a -> 𝐼 a
snoc𝐼 𝐼 b
ys b
y

filterMapMOn ∷ (ToIter a t,Monad m) ⇒ t → (a → m (𝑂 b)) → m (𝐼 b)
filterMapMOn :: forall a t (m :: * -> *) b.
(ToIter a t, Monad m) =>
t -> (a -> m (𝑂 b)) -> m (𝐼 b)
filterMapMOn = ((a -> m (𝑂 b)) -> t -> m (𝐼 b)) -> t -> (a -> m (𝑂 b)) -> m (𝐼 b)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> m (𝑂 b)) -> t -> m (𝐼 b)
forall a t (m :: * -> *) b.
(ToIter a t, Monad m) =>
(a -> m (𝑂 b)) -> t -> m (𝐼 b)
filterMapM

inbetween ∷ (ToIter a t) ⇒ a → t → 𝐼 a
inbetween :: forall a t. ToIter a t => a -> t -> 𝐼 a
inbetween a
sep t
xs = 𝐼 (Bool ∧ a)
-> (forall {i}.
    (Bool ∧ a)
    -> i -> (a -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> 𝐼 a
forall t a b.
ToIter a t =>
t
-> (forall i.
    a -> i -> (b -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> 𝐼 b
mapContOn𝐼 (t -> 𝐼 (Bool ∧ a)
forall a t. ToIter a t => t -> 𝐼 (Bool ∧ a)
withFirst t
xs) ((forall {i}.
  (Bool ∧ a)
  -> i -> (a -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
 -> 𝐼 a)
-> (forall {i}.
    (Bool ∧ a)
    -> i -> (a -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> 𝐼 a
forall a b. (a -> b) -> a -> b
$ \ (Bool
b :* a
x) i
i a -> i -> (i -> i) -> i
yield i -> i
continue i -> i
_done →
  if Bool
b
  then 
    a -> i -> (i -> i) -> i
yield a
x i
i i -> i
continue
  else
    a -> i -> (i -> i) -> i
yield a
sep i
i ((i -> i) -> i) -> (i -> i) -> i
forall a b. (a -> b) -> a -> b
$ \ i
i' →
    a -> i -> (i -> i) -> i
yield a
x i
i' i -> i
continue

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 -> Bool
forall a. Ord a => a -> a -> Bool
≤ ℕ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, Ord 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 -> Bool) -> t -> 𝑂 a
firstMaxByLT a -> a -> Bool
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 -> Bool
f a
x' a
x of
      Bool
True → a -> 𝑂 a
forall a. a -> 𝑂 a
Some a
x
      Bool
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 -> Bool) -> 𝐼 a -> 𝐼 a
mapWhile a -> a
f a -> Bool
p = Bool -> (a -> Bool -> Bool ∧ a) -> 𝐼 a -> 𝐼 a
forall t a b s. ToIter a t => s -> (a -> s -> s ∧ b) -> t -> 𝐼 b
mapState𝐼 Bool
True ((a -> Bool -> Bool ∧ a) -> 𝐼 a -> 𝐼 a)
-> (a -> Bool -> Bool ∧ a) -> 𝐼 a -> 𝐼 a
forall a b. (a -> b) -> a -> b
$ \ a
x Bool
b → do
  if Bool
b Bool -> Bool -> Bool
⩓ a -> Bool
p a
x
  then Bool
True Bool -> a -> Bool ∧ a
forall a b. a -> b -> a ∧ b
:* a -> a
f a
x
  else Bool
False Bool -> a -> Bool ∧ a
forall a b. a -> b -> a ∧ b
:* a
x

dropWhile ∷ ∀ a. (a → 𝔹) → 𝐼 a → 𝐼 a
dropWhile :: forall a. (a -> Bool) -> 𝐼 a -> 𝐼 a
dropWhile a -> Bool
p 𝐼 a
xs =
  let xs' :: 𝐼 (Bool ∧ a)
xs' = 𝐼 a -> Bool -> (a -> Bool -> Bool ∧ (Bool ∧ a)) -> 𝐼 (Bool ∧ a)
forall t a b s. ToIter a t => t -> s -> (a -> s -> s ∧ b) -> 𝐼 b
mapStateOnFrom𝐼 𝐼 a
xs Bool
True ((a -> Bool -> Bool ∧ (Bool ∧ a)) -> 𝐼 (Bool ∧ a))
-> (a -> Bool -> Bool ∧ (Bool ∧ a)) -> 𝐼 (Bool ∧ a)
forall a b. (a -> b) -> a -> b
$ \ a
x Bool
b → 
        let b' :: Bool
b' = Bool
b Bool -> Bool -> Bool
⩓ a -> Bool
p a
x 
        in 
        Bool
b' Bool -> (Bool ∧ a) -> Bool ∧ (Bool ∧ a)
forall a b. a -> b -> a ∧ b
:* (Bool
b' Bool -> a -> Bool ∧ a
forall a b. a -> b -> a ∧ b
:* a
x)
  in 
  𝐼 (Bool ∧ a)
-> (forall {i}.
    (Bool ∧ a)
    -> i -> (a -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> 𝐼 a
forall t a b.
ToIter a t =>
t
-> (forall i.
    a -> i -> (b -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> 𝐼 b
mapContOn𝐼 𝐼 (Bool ∧ a)
xs' ((forall {i}.
  (Bool ∧ a)
  -> i -> (a -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
 -> 𝐼 a)
-> (forall {i}.
    (Bool ∧ a)
    -> i -> (a -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> 𝐼 a
forall a b. (a -> b) -> a -> b
$ \ (Bool
b :* a
x) i
i a -> i -> (i -> i) -> i
yield i -> i
continue i -> i
_done → 
    if Bool
b then i -> i
continue i
i else a -> i -> (i -> i) -> i
yield a
x i
i i -> i
continue

takeWhile ∷ ∀ a. (a → 𝔹) → 𝐼 a → 𝐼 a
takeWhile :: forall a. (a -> Bool) -> 𝐼 a -> 𝐼 a
takeWhile a -> Bool
p = (forall i.
 a -> i -> (a -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> 𝐼 a -> 𝐼 a
forall t a b.
ToIter a t =>
(forall i.
 a -> i -> (b -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> t -> 𝐼 b
mapCont𝐼 ((forall i.
  a -> i -> (a -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
 -> 𝐼 a -> 𝐼 a)
-> (forall i.
    a -> i -> (a -> i -> (i -> i) -> i) -> (i -> i) -> (i -> i) -> i)
-> 𝐼 a
-> 𝐼 a
forall a b. (a -> b) -> a -> b
$ \ a
x i
i a -> i -> (i -> i) -> i
yield i -> i
continue i -> i
done →
  if a -> Bool
p a
x then a -> i -> (i -> i) -> i
yield a
x i
i i -> i
continue else i -> i
done i
i

lookup𝐼 ∷ ℕ64 → 𝐼 a → 𝑂 a
lookup𝐼 :: forall a. ℕ64 -> 𝐼 a -> 𝑂 a
lookup𝐼 ℕ64
n 𝐼 a
xs = 𝐼 a -> 𝑂 a
forall a t. ToIter a t => t -> 𝑂 a
firstElem (𝐼 a -> 𝑂 a) -> 𝐼 a -> 𝑂 a
forall a b. (a -> b) -> a -> b
$ ℕ64 -> 𝐼 a -> 𝐼 a
forall a t n.
(ToIter a t, Ord n, Zero n, One n, Plus n) =>
n -> t -> 𝐼 a
dropN ℕ64
n 𝐼 a
xs

partition ∷ (a → b ∨ c) → 𝐿 a → 𝐿 b ∧ 𝐿 c
partition :: forall a b c. (a -> b ∨ c) -> 𝐿 a -> 𝐿 b ∧ 𝐿 c
partition a -> b ∨ c
decide = (𝐿 b ∧ 𝐿 c) -> (a -> (𝐿 b ∧ 𝐿 c) -> 𝐿 b ∧ 𝐿 c) -> 𝐿 a -> 𝐿 b ∧ 𝐿 c
forall a t b. ToIter a t => b -> (a -> b -> b) -> t -> b
foldrFromWith (𝐿 b
forall a. 𝐿 a
Nil 𝐿 b -> 𝐿 c -> 𝐿 b ∧ 𝐿 c
forall a b. a -> b -> a ∧ b
:* 𝐿 c
forall a. 𝐿 a
Nil) ((a -> (𝐿 b ∧ 𝐿 c) -> 𝐿 b ∧ 𝐿 c) -> 𝐿 a -> 𝐿 b ∧ 𝐿 c)
-> (a -> (𝐿 b ∧ 𝐿 c) -> 𝐿 b ∧ 𝐿 c) -> 𝐿 a -> 𝐿 b ∧ 𝐿 c
forall a b. (a -> b) -> a -> b
$
  (b -> (𝐿 b ∧ 𝐿 c) -> 𝐿 b ∧ 𝐿 c)
-> (c -> (𝐿 b ∧ 𝐿 c) -> 𝐿 b ∧ 𝐿 c)
-> (b ∨ c)
-> (𝐿 b ∧ 𝐿 c)
-> 𝐿 b ∧ 𝐿 c
forall a c b. (a -> c) -> (b -> c) -> (a ∨ b) -> c
elimChoice ((𝐿 b -> 𝐿 b) -> (𝐿 b ∧ 𝐿 c) -> 𝐿 b ∧ 𝐿 c
forall a₁ a₂ b. (a₁ -> a₂) -> (a₁ ∧ b) -> a₂ ∧ b
mapFst ((𝐿 b -> 𝐿 b) -> (𝐿 b ∧ 𝐿 c) -> 𝐿 b ∧ 𝐿 c)
-> (b -> 𝐿 b -> 𝐿 b) -> b -> (𝐿 b ∧ 𝐿 c) -> 𝐿 b ∧ 𝐿 c
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ b -> 𝐿 b -> 𝐿 b
forall a. a -> 𝐿 a -> 𝐿 a
(:&)) ((𝐿 c -> 𝐿 c) -> (𝐿 b ∧ 𝐿 c) -> 𝐿 b ∧ 𝐿 c
forall b₁ b₂ a. (b₁ -> b₂) -> (a ∧ b₁) -> a ∧ b₂
mapSnd ((𝐿 c -> 𝐿 c) -> (𝐿 b ∧ 𝐿 c) -> 𝐿 b ∧ 𝐿 c)
-> (c -> 𝐿 c -> 𝐿 c) -> c -> (𝐿 b ∧ 𝐿 c) -> 𝐿 b ∧ 𝐿 c
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ c -> 𝐿 c -> 𝐿 c
forall a. a -> 𝐿 a -> 𝐿 a
(:&)) ((b ∨ c) -> (𝐿 b ∧ 𝐿 c) -> 𝐿 b ∧ 𝐿 c)
-> (a -> b ∨ c) -> a -> (𝐿 b ∧ 𝐿 c) -> 𝐿 b ∧ 𝐿 c
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> b ∨ c
decide

partition𝔹 ∷ (a → 𝔹) → 𝐿 a → 𝐿 a ∧ 𝐿 a
partition𝔹 :: forall a. (a -> Bool) -> 𝐿 a -> 𝐿 a ∧ 𝐿 a
partition𝔹 a -> Bool
decide = (a -> a ∨ a) -> 𝐿 a -> 𝐿 a ∧ 𝐿 a
forall a b c. (a -> b ∨ c) -> 𝐿 a -> 𝐿 b ∧ 𝐿 c
partition (\ a
a → (a ∨ a) -> (a ∨ a) -> Bool -> a ∨ a
forall a. a -> a -> Bool -> a
elim𝔹 (a -> a ∨ a
forall a b. a -> a ∨ b
Inl a
a) (a -> a ∨ a
forall a b. b -> a ∨ b
Inr a
a) (a -> Bool
decide a
a))

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

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

instance All 𝔹 where
  all :: 𝐼 Bool
all = [Bool] -> 𝐼 Bool
forall a t. ToIter a t => t -> 𝐼 a
iter [Bool
True,Bool
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