module FP.Prelude.Core
  ( module FP.Prelude.Core
  , module Control.Exception
  , module Data.Char
  , module Data.Coerce
  , module Data.List
  , module Language.Haskell.TH
  , module Numeric.Natural
  , module Prelude
  , module System.IO.Unsafe
  ) where

import Control.Exception (assert)
import Data.Char (isSpace,isAlphaNum,isLetter,isDigit,isSpace)
import Data.Coerce (Coercible,coerce)
import Data.List (sort,sortBy)
import Language.Haskell.TH (Q)
import Prelude 
  ( Int,Integer,Double,Char
  , Eq(..),Ord(..),Ordering(..)
  , Show(..),Read(..),read
  , Bool(..),otherwise
  , Maybe(..)
  , Either(..)
  , ($),seq
  , IO
  )
import Numeric.Natural (Natural)
import System.Exit
import System.IO.Unsafe (unsafePerformIO)

import qualified Data.Map               as Map
import qualified Data.Set               as Set
import qualified Data.Sequence          as Sequence
import qualified Data.Text              as Text
import qualified Data.Text.Lazy.Builder as TextLazyBuilder
import qualified Data.Text.Lazy         as TextLazy
import qualified Data.Text.IO           as Text
import qualified Prelude                as Prelude

-- 0: low/right associativity application
{- infixr 0 $ -}   -- ($) ∷ (a → b) → a → b
infixr 0 ♯$        -- / strict application
                   -- \ (♯$) ∷ (a → b) → a → b
infixr 0 ^$        -- / alias for `map`
                   -- \ (^$) ∷ (Functor t) ⇒ (a → b) → t a → t b
infixr 0 *$        -- / alias for `extend`
                   -- \ (*$) ∷ (Monad m) ⇒ (a → m b) → m a → m b
infixr 0 ^*$       -- / alias for `mapM`
                   -- \ (^*$) ∷ (FunctorM t,Monad m) ⇒ (a → m b) → t a → m (t b)

-- 1: semicolons
infixr 1 ≫=        -- (≫=) ∷ (Monad m) ⇒ m a → (a → m b) → m b
infixr 1 ≫         -- (≫) ∷ (Monad m) ⇒ m a → m b → m b
infixr 1 ≫=*       -- (≫=*) ∷ 𝒫 a → (a → 𝒫 b) → 𝒫 b
infixr 1 >>=       -- alias for (≫=)
infixr 1 >>        -- alias for (≫)

-- 3: arrows
infixr 3 ⇰         -- ★ → ★ → ★
infixr 3 ↦         -- (↦) ∷ (Ord k) ⇒ k → v → k ⇰ v

-- 4: sums
infixr 4 ⨄         -- ★ → ★
infixr 4 ∨         -- (∨) ∷ 𝔹 → 𝔹 → 𝔹
infixr 4 ⧺         -- (⧺) ∷ (Monoid a) ⇒ a → a → a
infixr 4 +         -- (+) ∷ (Additive a) ⇒ a → a → a
infix  4 -         -- (-) ∷ (Subtractive a) ⇒ a → a → a

-- 5: products
infixr 5 ∧         -- (∧) ∷ 𝔹 → 𝔹 → 𝔹
infixr 5 ×         -- (×) ∷ (Multiplicative a) ⇒ a → a → a
infix  5 /         -- (/) ∷ (Divisible a) ⇒ a → a → a
infix  5 ⌿         -- (⌿) ∷ (TruncateDivisible a) ⇒ a → a → a
infixr 5 <×>       -- (<×>) ∷ (Monad m) ⇒ m a → m b → m (a,b)

-- 6: relations
infix 6 ≟          -- / alias for `(==)`
                   -- \ (≟) ∷ (Eq a) ⇒ a → a → 𝔹
infix 6 ⋚          -- / alias for `compare`
                   -- \ (⋚) ∷ (Ord a) ⇒ a → a → Ordering
infix 6 ≤          -- (≤) ∷ (Ord a) ⇒ a → a → 𝔹
infix 6 ≥          -- (≥) ∷ (Ord a) ⇒ a → a → 𝔹
infix 6 ∈          -- (∈) ∷ a → 𝒫 a → 𝔹

-- 7: composition
infixr 7 ∘         -- (∘) ∷ (b → c) → (a → b) → a → c
infixr 7 ∘∘        -- (∘∘) ∷ (c → c) → (a → b → c) → a → b → d
infixr 7 ^∘        -- (^∘) ∷ (Functor t) ⇒ (b → c) → (a → t b) → a → t c
infixr 7 *∘        -- (*∘) ∷ (Monad m) ⇒ (b → m c) → (a → m b) → a → m c
infixr 7 ^*∘       -- (^*∘) ∷ (FunctorM t,Monad m) ⇒ (b → m c) → (a → m b) → t a → m (t c) 

-- 8: indexing structures and exponentials
infixl 8 #         -- (#) ∷ k ⇰ v → k → Maybe v
infixl 8 #!        -- (#!) ∷ k ⇰ v → k → v
infixl 8 ^         -- (^) ∷ (Exponential a) ⇒ a → a → a

-- 9: application
infixl 9 ♯⋅        -- (♯⋅) ∷ (a → b) → a → b
infixl 9 ^⋅        -- (^⋅) ∷ (Functor t) ⇒ (a → b) → t a → t b 
infixl 9 *⋅        -- (*⋅) ∷ (Monad m) ⇒ (a → m b) → (m a → m b)
infixl 9 ^*⋅       -- (^*⋅) ∷ (FunctorM t,Monad m) ⇒ (a → m b) → t a → m (t b) 
infixl 9 <⋅>       -- (<×>) ∷ (Monad m) ⇒ m (a → b) → m a → m b

--------------
-- Universe --
--------------

type ℤ = Integer
data ℤᵀ = ZNegInfinity | ZPosInfinity | ZFinite ℤ
type ℕ = Natural
data ℕᵀ = NInfinity | NFinite ℕ
type 𝕀 = Int
type 𝔻 = Double
type ℂ = Char
type 𝕊 = Text.Text
type 𝕊ᵇ = TextLazyBuilder.Builder
-- - ()
type 𝔹 = Bool
type (⨄) = Either
-- - (,)
-- - (→)
newtype Fold a = Fold { runFold ∷ ∀ b. (a → b → b) → b → b }
data Stream a where Stream ∷ ∀ s a. s → (s → Maybe (a,s)) → Stream a

-- - []

type 𝒮 = Sequence.Seq

data 𝒫 a where 
  EmptySet ∷ 𝒫 a
  InhabitedSet ∷ (Ord a) ⇒ Set.Set a → 𝒫 a

data k ⇰ v where
  EmptyDict ∷ k ⇰ v
  InhabitedDict ∷ (Ord k) ⇒ Map.Map k v → k ⇰ v

newtype k ⇰♭⧺ v = LazyDictAppend { runLazyDictAppend ∷ Fold (k,v) }
newtype k ⇰♭⊔ v = LazyDictJoin { runLazyDictJoin ∷ Fold (k,v) }
newtype 𝒫ᵇ a = LazySet { runLazySet ∷ Fold a }

-------------
-- Classes --
-------------

-- # Equality and Order

(≟) ∷ (Eq a) ⇒ a → a → 𝔹
(≟) = (==)

(⋚) ∷ (Ord a) ⇒ a → a → Ordering
(⋚) = compare

(≤) ∷ (Ord a) ⇒ a → a → 𝔹
x ≤ y = case x ⋚ y of {LT → True;EQ → True;GT → False}

(≥) ∷ (Ord a) ⇒ a → a → 𝔹
x ≥ y = case x ⋚ y of {LT → False;EQ → True;GT → True}

minBy ∷ (Ord b) ⇒ (a → b) → a → a → a
minBy f x y = if f x ≤ f y then x else y

maxBy ∷ (Ord b) ⇒ (a → b) → a → a → a
maxBy f x y = if f x ≥ f y then x else y

-- Arithmatic

class Peano a where {suc ∷ a → a;zero ∷ a}
class (Peano a) ⇒ Additive a where (+) ∷ a → a → a
class (Additive a) ⇒ Subtractive a where (-) ∷ a → a → a
class (Additive a) ⇒ Multiplicative a where {one ∷ a;(×) ∷ a → a → a}
class (Multiplicative a) ⇒ Divisible a where (/) ∷ a → a → a
class (Multiplicative a) ⇒ TruncateDivisible a where (⌿) ∷ a → a → a
class (Multiplicative a) ⇒ Exponential a where (^) ∷ a → a → a

negate ∷ (Subtractive a) ⇒ a → a 
negate x = zero - x

inverse ∷ (Divisible a) ⇒ a → a 
inverse x = one / x

-- # Monoid

class Monoid a where {null ∷ a;(⧺) ∷ a → a → a}

-- # Functor

class Functor (t ∷ ★ → ★) where map ∷ (a → b) → (t a → t b)

mapOn ∷ (Functor t) ⇒ t a → (a → b) → t b 
mapOn = flip map

(^⋅) ∷ (Functor t) ⇒ (a → b) → t a → t b 
(^⋅) = map

(^$) ∷ (Functor t) ⇒ (a → b) → t a → t b 
(^$) = map

(^∘) ∷ (Functor t) ⇒ (b → c) → (a → t b) → a → t c 
g ^∘ f = map g ∘ f

-- # Monad

class (Functor m) ⇒ Monad (m ∷ ★ → ★) where {return ∷ a → m a;(≫=) ∷ m a → (a → m b) → m b}

(*⋅) ∷ (Monad m) ⇒ (a → m b) → (m a → m b)
(*⋅) = extend

(*$) ∷ (Monad m) ⇒ (a → m b) → (m a → m b)
(*$) = extend

(*∘) ∷ (Monad m) ⇒ (b → m c) → (a → m b) → (a → m c)
(g *∘ f) x = g *$ f x

kreturn ∷ (Monad m) ⇒ (a → b) → (a → m b)
kreturn = (∘) return

extend ∷ (Monad m) ⇒ (a → m b) → (m a → m b)
extend = flip (≫=)

(≫) ∷ (Monad m) ⇒ m a → m b → m b
aM ≫ bM = aM ≫= const bM

void ∷ (Monad m) ⇒ m a → m ()
void = mmap (const ())

mjoin ∷ (Monad m) ⇒ m (m a) → m a
mjoin = extend id

mmap ∷ (Monad m) ⇒ (a → b) → m a → m b
mmap f aM = return ∘ f *$ aM

(<×>) ∷ (Monad m) ⇒ m a → m b → m (a,b)
aM <×> bM = do
  a ← aM
  b ← bM
  return (a,b)

(<⋅>) ∷ (Monad m) ⇒ m (a → b) → m a → m b
fM <⋅> aM = do {f ← fM;a ← aM;return $ f a}

when ∷ (Monad m) ⇒ 𝔹 → m () → m ()
when True = id
when False = const $ return ()

whenM ∷ (Monad m) ⇒ m 𝔹 → m () → m ()
whenM bM aM = do
  b ← bM
  when b aM

whenMaybe ∷ (Monad m) ⇒ Maybe a → (a → m ()) → m ()
whenMaybe Nothing _ = return ()
whenMaybe (Just x) f = f x

whenMaybeM ∷ (Monad m) ⇒ m (Maybe a) → (a → m ()) → m ()
whenMaybeM xMM f = do
  xM ← xMM
  whenMaybe xM f

returnMaybe ∷ (Monad m) ⇒ m a → Maybe a → m a
returnMaybe xM Nothing = xM
returnMaybe _ (Just x) = return x

-- # FunctorM

class FunctorM (t ∷ ★ → ★) where mapM ∷ (Monad m) ⇒ (a → m b) → t a → m (t b)

mapMOn ∷ (FunctorM t,Monad m) ⇒ t a → (a → m b) → m (t b) 
mapMOn = flip mapM

sequence ∷ (FunctorM t,Monad m) ⇒ t (m a) → m (t a) 
sequence = mapM id

(^*⋅) ∷ (FunctorM t,Monad m) ⇒ (a → m b) → t a → m (t b) 
(^*⋅) = mapM

(^*$) ∷ (FunctorM t,Monad m) ⇒ (a → m b) → t a → m (t b) 
(^*$) = mapM

(^*∘) ∷ (FunctorM t,Monad m) ⇒ (b → m c) → (a → m b) → t a → m (t c) 
(g ^*∘ f) aT = mapM g *$ f ^*$ aT

-- # Conversion

class ToFold a t | t → a where fold ∷ t → Fold a
class ToStream a t | t → a where stream ∷ t → Stream a
class Singleton a t | t → a where single ∷ a → t

class ToInteger a where 𝕫 ∷ a → ℤ
class ToNatural a where 𝕟 ∷ a → ℕ
class ToInt a where 𝕚 ∷ a → 𝕀
class ToDouble a where 𝕕 ∷ a → 𝔻
class ToString a where 𝕤 ∷ a → 𝕊

𝕟ᵀ ∷ (ToNatural a) ⇒ a → ℕᵀ
𝕟ᵀ = NFinite ∘ 𝕟

-- # Lookup

class Lookup k v t | t → k,t → v where lookup ∷ k → t → Maybe v

(#) ∷ (Lookup k v t) ⇒ t → k → Maybe v
(#) = flip lookup

(#!) ∷ (Lookup k v t) ⇒ t → k → v
m #! k = ifNothing (error "unsafe (#!)") $ m # k

-----------
-- Types --
-----------

-- # Integer (ℤ)

instance Peano ℤ where {zero = 0;suc = Prelude.succ}
instance Additive ℤ where (+) = (Prelude.+)
instance Subtractive ℤ where (-) = (Prelude.-)
instance Multiplicative ℤ where {one = 1;(×) = (Prelude.*)}
instance TruncateDivisible ℤ where (⌿) = Prelude.div

instance ToInteger ℤ where 𝕫 = id
instance ToNatural ℤ where 𝕟 = Prelude.fromIntegral
instance ToInt ℤ where 𝕚 = Prelude.fromIntegral
instance ToDouble ℤ where 𝕕 = Prelude.fromIntegral

-- # Natural (ℕ)

instance Peano ℕ where {zero = 𝕟 0;suc = Prelude.succ}
instance Additive ℕ where (+) = (Prelude.+)
instance Subtractive ℕ where (-) = (Prelude.-)
instance Multiplicative ℕ where {one = 𝕟 1;(×) = (Prelude.*)}
instance TruncateDivisible ℕ where (⌿) = Prelude.div

instance ToInteger ℕ where 𝕫 = Prelude.fromIntegral
instance ToNatural ℕ where 𝕟 = id
instance ToInt ℕ where 𝕚 = Prelude.fromIntegral
instance ToDouble ℕ where 𝕕 = Prelude.fromIntegral

-- # NaturalTop (ℕᵀ)

instance Peano ℕᵀ where 
  zero = 𝕟ᵀ 0
  suc NInfinity = NInfinity
  suc (NFinite n) = NFinite $ suc n
instance Additive ℕᵀ where 
  NInfinity + _ = NInfinity
  _ + NInfinity = NInfinity
  NFinite n₁ + NFinite n₂ = NFinite $ n₁ + n₂

instance ToDouble ℕᵀ where 
  𝕕 NInfinity = 𝕤read "NInfinity"
  𝕕 (NFinite n) = 𝕕 n

-- # Int (𝕀)

instance Peano 𝕀 where {zero = 𝕚 0;suc = Prelude.succ}
instance Additive 𝕀 where (+) = (Prelude.+)
instance Subtractive 𝕀 where (-) = (Prelude.-)
instance Multiplicative 𝕀 where {one = 𝕚 1;(×) = (Prelude.*)}
instance TruncateDivisible 𝕀 where (⌿) = Prelude.div

instance ToInteger 𝕀 where 𝕫 = Prelude.fromIntegral
instance ToNatural 𝕀 where 𝕟 = Prelude.fromIntegral
instance ToInt 𝕀 where 𝕚 = id
instance ToDouble 𝕀 where 𝕕 = Prelude.fromIntegral

-- # Double (𝔻)

instance Peano 𝔻 where {zero = 𝕕 0;suc = Prelude.succ}
instance Additive 𝔻 where (+) = (Prelude.+)
instance Subtractive 𝔻 where (-) = (Prelude.-)
instance Multiplicative 𝔻 where {one = 𝕕 1;(×) = (Prelude.*)}
instance Divisible 𝔻 where (/) = (Prelude./)

instance ToDouble 𝔻 where 𝕕 = id

-- # Char (ℂ)

instance ToString ℂ where 𝕤 = single
instance ToString [ℂ] where 𝕤 = Text.pack
instance ToString (Fold ℂ) where 𝕤 = 𝕤 ∘ list
instance ToString (Stream ℂ) where 𝕤 = 𝕤 ∘ list

-- # String (𝕊)

instance Monoid 𝕊 where {null = Text.empty;(⧺) = Text.append}

instance ToFold ℂ 𝕊 where fold = fold ∘ stream
instance ToStream ℂ 𝕊 where stream = stream ∘ Text.unpack
instance Singleton ℂ 𝕊 where single = Text.singleton
instance ToString 𝕊 where 𝕤 = id

chars ∷ 𝕊 → [ℂ]
chars = Text.unpack

𝕤show ∷ (Show a) ⇒ a → 𝕊
𝕤show = 𝕤 ∘ show

𝕤read ∷ (Read a) ⇒ 𝕊 → a
𝕤read = read ∘ chars

-- # Lazy String (𝕊ᵇ)

instance ToString 𝕊ᵇ where 𝕤 = TextLazy.toStrict ∘ TextLazyBuilder.toLazyText

instance Monoid 𝕊ᵇ where {null = Prelude.mempty;(⧺) = Prelude.mappend}

𝕤ᵇ ∷ (ToString a) ⇒ a → 𝕊ᵇ
𝕤ᵇ = TextLazyBuilder.fromText ∘ 𝕤

-- # Unit ()

-- # Bool (𝔹)

not ∷ 𝔹 → 𝔹
not True  = False
not False = True

(∧) ∷ 𝔹 → 𝔹 → 𝔹
True  ∧ x = x
False ∧ _ = False

(∨) ∷ 𝔹 → 𝔹 → 𝔹
True  ∨ _ = True
False ∨ x = x

fif ∷ 𝔹 → a → a → a
fif True x _ = x
fif False _ y = y

-- # Sum

-- no Monoid
instance Functor ((⨄) a) where map = mmap
instance Monad ((⨄) a) where {return = Right;abM ≫= k = elimSum Left k abM}
instance FunctorM ((⨄) a) where 
  mapM _ (Left x) = return $ Left x
  mapM f (Right y) = Right ^$ f y

elimSum ∷ (a → c) → (b → c) → a ⨄ b → c
elimSum f g aorb = case aorb of
  Left x → f x
  Right y → g y

mapSum ∷ (a → a') → (b → b') → a ⨄ b → a' ⨄ b'
mapSum f _ (Left x) = Left $ f x
mapSum _ g (Right y) = Right $ g y

mapLeft ∷ (a → c) → a ⨄ b → c ⨄ b
mapLeft f = mapSum f id

mapRight ∷ (b → c) → a ⨄ b → a ⨄ c
mapRight g = mapSum id g

swapSum ∷ a ⨄ b → b ⨄ a
swapSum (Left x) = Right x
swapSum (Right y) = Left y

-- # Product

instance (Monoid a,Monoid b) ⇒ Monoid (a,b) where{null = (null,null);(a₁,b₁) ⧺ (a₂,b₂) = (a₁ ⧺ a₂,b₁ ⧺ b₂)}
instance Functor ((,) a) where map f (x,y) = (x,f y)
instance (Monoid a) ⇒ Monad ((,) a) where {return = (null,); (x,y) ≫= k = let (x',z) = k y in (x ⧺ x',z)}
instance FunctorM ((,) a) where mapM f (x,y) = (x,) ^$ f y

fst ∷ (a,b) → a
fst (x,_) = x

snd ∷ (a,b) → b
snd (_,y) = y

swap ∷ (a,b) → (b,a)
swap (x,y) = (y,x)

mapPair ∷ (a → a') → (b → b') → (a,b) → (a',b')
mapPair f g (a,b) = (f a,g b)

mapFst ∷ (a → a') → (a,b) → (a',b)
mapFst f = mapPair f id

mapSnd ∷ (b → b') → (a,b) → (a,b')
mapSnd f = mapPair id f

-- # Function

instance (Monoid b) ⇒ Monoid (a → b) where {null = const null;(f ⧺ g) x = f x ⧺ g x}
instance Functor ((→) a) where map = (∘)
instance Monad ((→) a) where {return = const;(f ≫= k) x = k (f x) x }
-- no FunctorM

id ∷ a → a
id x = x

(♯$) ∷ (a → b) → a → b
f ♯$ x = x `seq` f x

(♯⋅) ∷ (a → b) → a → b
f ♯⋅ x = x `seq` f x

(∘) ∷ (b → c) → (a → b) → (a → c)
(g ∘ f) x = g (f x)

(∘∘) ∷ (c → d) → (a → b → c) → (a → b → d)
(∘∘) = (∘) ∘ (∘)

const ∷ b → (a → b)
const x = \ _ → x

flip ∷ (a → b → c) → (b → a → c)
flip f y x = f x y

curry ∷ ((a,b) → c) → a → b → c
curry f x y = f (x,y)

uncurry ∷ (a → b → c) → (a,b) → c
uncurry f (x,y) = f x y

rotateR ∷ (a → b → c → d) → (c → a → b → d)
rotateR f c a b = f a b c

rotateL ∷ (a → b → c → d) → (b → c → a → d)
rotateL f b c a = f a b c

mirror ∷ (a → b → c → d) → (c → b → a → d)
mirror f c b a = f a b c

on ∷ (b → b → c) → (a → b) → (a → a → c)
on p f x y = p (f x) (f y)

-- # Maybe

-- no Monoid
instance Functor Maybe where map = mmap
instance Monad Maybe where
  return = Just
  Nothing ≫= _ = Nothing
  Just x ≫= k = k x
instance FunctorM Maybe where 
  mapM _ Nothing = return Nothing
  mapM f (Just x) = Just ^$ f x

elimMaybe ∷ b → (a → b) → Maybe a → b
elimMaybe y f aM = case aM of
  Nothing → y
  Just a → f a

elimMaybeOn ∷ Maybe a → b → (a → b) → b
elimMaybeOn = rotateR elimMaybe

ifNothing ∷ a → Maybe a → a
ifNothing x = elimMaybe x id

-- # Fold

instance (Eq a) ⇒ Eq (Fold a) where (==) = (≟) `on` list
instance (Ord a) ⇒ Ord (Fold a) where compare = compare `on` list
instance (Show a) ⇒ Show (Fold a) where show = chars ∘ (⧺) "fold " ∘ 𝕤show ∘ list

instance Monoid (Fold a) where
  null = emptyFold
  Fold g₁ ⧺ Fold g₂ = Fold $ \ f → g₁ f ∘ g₂ f
instance Functor Fold where
  map g (Fold h) = Fold $ \ f → h $ f ∘ g
instance Monad Fold where
  return = singleFold
  xs ≫= f = concat $ map f xs

instance ToFold a (Fold a) where fold = id
instance Singleton a (Fold a) where single = singleFold

-- Operations

emptyFold ∷ Fold a
emptyFold = Fold $ \ _ i → i

singleFold ∷ a → Fold a
singleFold x = Fold $ \ f i → f x i

consFold ∷ a → Fold a → Fold a
consFold x (Fold g) = Fold $ \ f i → g f (f x i)

-- Reducers

foldlk ∷ (ToFold a t) ⇒ (b → a → (b → b) → b) → b → t → b
foldlk f i₀ (fold → Fold g) = g (\ x k i → f i x k) id i₀

foldlkOn ∷ (ToFold a t) ⇒ t → b → (b → a → (b → b) → b) → b
foldlkOn = mirror foldlk

foldl ∷ (ToFold a t) ⇒ (b → a → b) → b → t → b
foldl f = foldlk $ \ i x k → k ♯$ f i x

foldlOn ∷ (ToFold a t) ⇒ t → b → (b → a → b) → b
foldlOn = mirror foldl

iter ∷ (ToFold a t) ⇒ (a → b → b) → b → t → b
iter = foldl ∘ flip

iterOn ∷ (ToFold a t) ⇒ t → b → (a → b → b) → b
iterOn = mirror iter

foldr ∷ (ToFold a t) ⇒ (a → b → b) → b → t → b
foldr f = foldlk $ \ i x k → f x $ k i

foldrOn ∷ (ToFold a t) ⇒ t → b → (a → b → b) → b
foldrOn = mirror foldr

sum ∷ (ToFold a t,Additive a) ⇒ t → a
sum = iter (+) zero

product ∷ (ToFold a t,Multiplicative a) ⇒ t → a
product = iter (×) one

concat ∷ (ToFold a t,Monoid a) ⇒ t → a
concat = foldr (⧺) null

mfoldl ∷ (Monad m,ToFold a t) ⇒ (b → a → m b) → b → t → m b
mfoldl f = foldl (\ bM a → bM ≫= \ b → f b a) ∘ return

miter ∷ (Monad m,ToFold a t) ⇒ (a → b → m b) → b → t → m b
miter f = iter (\ a bM → bM ≫= f a) ∘ return

mfoldr ∷ (Monad m,ToFold a t) ⇒ (a → b → m b) → b → t → m b
mfoldr f = foldr (extend ∘ f) ∘ return

foreach ∷ (Monad m,ToFold a t) ⇒ (a → m ()) → t → m ()
foreach f = foldl (\ m a → m ≫ f a) $ return ()

foreachOn ∷ (Monad m,ToFold a t) ⇒ t → (a → m ()) → m () 
foreachOn = flip foreach

exec ∷ (Monad m,ToFold (m ()) t) ⇒ t → m () 
exec = foreach id

-- Conversion

list ∷ (ToFold a t) ⇒ t → [a]
list = foldr (:) []

set ∷ (ToFold a t,Ord a) ⇒ t → 𝒫 a
set = iter insert emptySet

lazySet ∷ (ToFold a t) ⇒ t → 𝒫ᵇ a
lazySet = LazySet ∘ fold

dict ∷ (ToFold (k,v) t,Ord k) ⇒ t → k ⇰ v
dict = foldr (uncurry insertDict) emptyDict

dictAppend ∷ (ToFold (k,v) t,Ord k,Monoid v) ⇒ t → k ⇰ v
dictAppend = foldr ((⧺) ∘ single) null

lazyDictAppend ∷ (ToFold (k,v) t) ⇒ t → k ⇰♭⧺ v
lazyDictAppend = LazyDictAppend ∘ fold

-- # Stream

instance (Eq a) ⇒ Eq (Stream a) where (==) = (≟) `on` list
instance (Ord a) ⇒ Ord (Stream a) where compare = compare `on` list
instance (Show a) ⇒ Show (Stream a) where show = chars ∘ (⧺) "stream " ∘ 𝕤show ∘ list

instance Monoid (Stream a) where
  null = emptyStream
  Stream s₁₀ f₁ ⧺ Stream s₂₀ f₂ = Stream (Left s₁₀) $ \ s →
    let doRight s₂ = case f₂ s₂ of
          Nothing → Nothing
          Just (x,s₂') → Just (x,Right s₂')
    in case s of
      Left s₁ → case f₁ s₁ of
        Nothing → doRight s₂₀
        Just (x,s₁') → Just (x,Left s₁')
      Right s₂ → doRight s₂
instance Functor Stream where map g (Stream s₀ f) = Stream s₀ $ map (mapFst g) ∘ f
instance Monad Stream where {return = singleStream;xs ≫= k = concat $ map k xs}
instance FunctorM Stream where mapM f = stream ^∘ mapM f ∘ list

instance ToFold a (Stream a) where 
  fold (Stream s₀ g) = Fold $ \ f i₀ →
    let loop s i = case g s of
          Nothing → i
          Just (x,s') → f x $ loop s' i
    in loop s₀ i₀
instance ToStream a (Stream a) where stream = id
instance Singleton a (Stream a) where single = singleStream

emptyStream ∷ Stream a
emptyStream = Stream () $ \ () → Nothing

singleStream ∷ a → Stream a
singleStream x = Stream (Just x) $ map (,Nothing)

unconsStream ∷ Stream a → Maybe (a,Stream a)
unconsStream (Stream s f) = case f s of
  Nothing → Nothing
  Just (x,s') → Just (x,Stream s' f)

isEmpty ∷ (ToStream a t) ⇒ t → 𝔹
isEmpty (stream → xs) = case unconsStream xs of
  Nothing → True
  Just _ → False

-- # List

instance Monoid [a] where
  null = []
  [] ⧺ ys = ys
  x:xs ⧺ ys = x:(xs ⧺ ys)
instance Functor [] where
  map _ [] = []
  map f (x:xs) = f x:map f xs
instance Monad [] where
  return = (:[])
  [] ≫= _ = []
  x:xs ≫= k = k x ⧺ (xs ≫= k)
instance FunctorM [] where
  mapM _ [] = return []
  mapM f (x:xs) = do
    y ← f x
    ys ← mapM f xs
    return $ y:ys

instance ToFold a [a] where fold = fold ∘ stream
instance ToStream a [a] where stream xs = Stream xs uncons
instance Singleton a [a] where single = singleList

singleList ∷ a → [a]
singleList = (:[])

cons ∷ a → [a] → [a]
cons = (:)

uncons ∷ [a] → Maybe (a,[a])
uncons [] = Nothing
uncons (x:xs) = Just (x,xs)

zip ∷ [a] → [b] → Maybe [(a,b)]
zip [] [] = Just []
zip (x:xs) (y:ys) = do
  xys ← zip xs ys
  return $ (x,y):xys
zip _ _ = Nothing

zipAssumeSameLength ∷ [a] → [b] → [(a,b)]
zipAssumeSameLength [] [] = []
zipAssumeSameLength (x:xs) (y:ys) = (x,y) : zipAssumeSameLength xs ys
zipAssumeSameLength _ _ = error "zipAssumeSameLength: not same length"

unzip ∷ [(a,b)] → ([a],[b])
unzip xys = (map fst xys,map snd xys)

partition ∷ [a ⨄ b] → ([a],[b])
partition [] = ([],[])
partition (Left x:xys) = let (xs,ys) = partition xys in (x:xs,ys)
partition (Right y:xys) = let (xs,ys) = partition xys in (xs,y:ys)

reverse ∷ [a] → [a]
reverse = foldl (flip (:)) []

-- # Set

instance Eq (𝒫 a) where (==) = elimPrim21Set True (Set.null) (≟)
instance Ord (𝒫 a) where compare = elimPrim22Set EQ (\ s → compare Set.empty s) (\ s → compare s Set.empty) compare
instance (Show a) ⇒ Show (𝒫 a) where show = chars ∘ (⧺) "set " ∘ 𝕤show ∘ list
instance Monoid (𝒫 a) where {null = emptySet;(⧺) = unionSet}
instance ToFold a (𝒫 a) where fold = fold ∘ stream
instance ToStream a (𝒫 a) where stream = elimPrimConcreteSet null $ stream ∘ Set.toList
instance (Ord a) ⇒ Singleton a (𝒫 a) where single = singleSet

elimPrimConcreteSet ∷ b → ((Ord a) ⇒ Set.Set a → b) → 𝒫 a → b
elimPrimConcreteSet i f = \case
  EmptySet → i
  InhabitedSet x → f x

elimPrimOnSet ∷ 𝒫 a → b → ((Ord a) ⇒ Set.Set a → b) → b
elimPrimOnSet s i f = elimPrimConcreteSet i f s

elimPrim22Set ∷
     c
  → ((Ord b) ⇒ Set.Set b → c)
  → ((Ord a) ⇒ Set.Set a → c)
  → ((Ord a,Ord b) ⇒ Set.Set a → Set.Set b → c)
  → 𝒫 a → 𝒫 b → c
elimPrim22Set i f1 f2 ff s1 s2 =
  elimPrimOnSet s1 (elimPrimOnSet s2 i f1) $ \ p1 →
    elimPrimOnSet s2 (f2 p1) $ \ p2 →
      ff p1 p2

elimPrim21Set ∷
     b
  → ((Ord a) ⇒ Set.Set a → b)
  → ((Ord a) ⇒ Set.Set a → Set.Set a → b)
  → 𝒫 a → 𝒫 a → b
elimPrim21Set i f = elimPrim22Set i f f

toPrimSet ∷ 𝒫 a → Set.Set a
toPrimSet = elimPrimConcreteSet Set.empty id

learnSet ∷ 𝒫 a → b → ((Ord a) ⇒ b) → b
learnSet s i f = elimPrimOnSet s i $ const f

learn22Set ∷ 𝒫 a → 𝒫 b → c → ((Ord b) ⇒ c) → ((Ord a) ⇒ c) → ((Ord a,Ord b) ⇒ c) → c
learn22Set xs ys i fNoXs fNoYs f = 
  learnSet xs (learnSet ys i fNoXs) $
  learnSet ys fNoYs f

emptySet ∷ 𝒫 a
emptySet = EmptySet

singleSet ∷ (Ord a) ⇒ a → 𝒫 a
singleSet x = insert x null

insert ∷ (Ord a) ⇒ a → 𝒫 a → 𝒫 a
insert x = elimPrimConcreteSet (InhabitedSet $ Set.singleton x) $ InhabitedSet ∘ Set.insert x

unionSet ∷ 𝒫 a → 𝒫 a → 𝒫 a
unionSet = elimPrim21Set EmptySet InhabitedSet $ InhabitedSet ∘∘ Set.union

intersectionSet ∷ 𝒫 a → 𝒫 a → 𝒫 a
intersectionSet = elimPrim21Set EmptySet (const EmptySet) $ InhabitedSet ∘∘ Set.intersection

differenceSet ∷ 𝒫 a → 𝒫 a → 𝒫 a
differenceSet = elimPrim22Set EmptySet (const EmptySet) InhabitedSet $ InhabitedSet ∘∘ (Set.\\)

isSubsetOf ∷ 𝒫 a → 𝒫 a → 𝔹
isSubsetOf = elimPrim22Set True (const True) (const False) $ Set.isSubsetOf

(∈) ∷ a → 𝒫 a → 𝔹
(∈) x = elimPrimConcreteSet False $ Set.member x

elem ∷ a → 𝒫 a → Bool
elem = (∈)

elemOf ∷ 𝒫 a → a → 𝔹
elemOf = flip elem

removeMin ∷ 𝒫 a → Maybe (a,𝒫 a)
removeMin = elimPrimConcreteSet Nothing $ map (mapSnd InhabitedSet) ∘ Set.minView

removeMax ∷ 𝒫 a → Maybe (a,𝒫 a)
removeMax = elimPrimConcreteSet Nothing $ map (mapSnd InhabitedSet) ∘ Set.maxView

mapSet ∷ (Ord b) ⇒ (a → b) → 𝒫 a → 𝒫 b
mapSet f = elimPrimConcreteSet EmptySet $ InhabitedSet ∘ Set.map f

mapSetOn ∷ (Ord b) ⇒ 𝒫 a → (a → b) → 𝒫 b
mapSetOn = flip mapSet

extendSet ∷ (a → 𝒫 b) → 𝒫 a → 𝒫 b
extendSet f = iter unionSet emptySet ∘ map f ∘ stream

(≫=*) ∷ 𝒫 a → (a → 𝒫 b) → 𝒫 b
(≫=*) = flip extendSet

-- # Dict

instance (Eq v) ⇒ Eq (k ⇰ v) where (==) = elimPrim21Dict True (Map.null) (≟)
instance (Ord v) ⇒ Ord (k ⇰ v) where compare = elimPrim22Dict EQ (\ m → Map.empty ⋚ m) (\ m → m ⋚ Map.empty) (⋚)
instance (Show k,Show v) ⇒ Show (k ⇰ v) where show = chars ∘ (⧺) "dict " ∘ 𝕤show ∘ list
instance (Monoid v) ⇒ Monoid (k ⇰ v) where {null = EmptyDict;(⧺) = unionWithDict (⧺)}
instance Functor ((⇰) k) where map f = elimPrimDict EmptyDict $ InhabitedDict ∘ Map.map f
instance ToFold (k,v) (k ⇰ v) where fold = fold ∘ stream
instance ToStream (k,v) (k ⇰ v) where stream = elimPrimDict null $ stream ∘ Map.toList
instance (Ord k) ⇒ Singleton (k,v) (k ⇰ v) where single (k,v) = InhabitedDict $ Map.singleton k v

instance Lookup k v (k ⇰ v) where lookup k = elimPrimDict Nothing $ Map.lookup k

elimPrimDict ∷ b → ((Ord k) ⇒ Map.Map k v → b) → k ⇰ v → b
elimPrimDict i f = \case {EmptyDict → i;InhabitedDict p → f p}

elimPrimOnDict ∷ k ⇰ v → b → ((Ord k) ⇒ Map.Map k v → b) → b
elimPrimOnDict m i f = elimPrimDict i f m

elimPrim22Dict ∷
     b
  → ((Ord k) ⇒ Map.Map k v → b)
  → ((Ord k) ⇒ Map.Map k v → b)
  → ((Ord k) ⇒ Map.Map k v → Map.Map k v → b)
  → k ⇰ v → k ⇰ v → b
elimPrim22Dict i f1 f2 ff s1 s2 =
  elimPrimOnDict s1 (elimPrimOnDict s2 i f1) $ \ p1 →
    elimPrimOnDict s2 (f2 p1) $ \ p2 →
      ff p1 p2

elimPrim21Dict ∷
     b
  → ((Ord k) ⇒ Map.Map k v → b)
  → ((Ord k) ⇒ Map.Map k v → Map.Map k v → b)
  → k ⇰ v
  → k ⇰ v
  → b
elimPrim21Dict i f = elimPrim22Dict i f f

toPrimDict ∷ k ⇰ v → Map.Map k v
toPrimDict = elimPrimDict Map.empty id

learnDict ∷ k ⇰ v → b → ((Ord k) ⇒ b) → b
learnDict m i f = elimPrimOnDict m i $ const f

emptyDict ∷ k ⇰ v
emptyDict = EmptyDict

keys ∷ k ⇰ v → 𝒫 k
keys = elimPrimDict emptySet $ InhabitedSet ∘ Map.keysSet

values ∷ k ⇰ v → [v]
values = elimPrimDict null $ Map.elems

type Old a = a
type New a = a

insertWithDict ∷ (Ord k) ⇒ (Old v → New v → v) → k → v → k ⇰ v → k ⇰ v
insertWithDict f k v = elimPrimDict (InhabitedDict $ Map.singleton k v) $ 
  InhabitedDict ∘ Map.insertWith (flip f) k v

insertDict ∷ (Ord k) ⇒ k → v → k ⇰ v → k ⇰ v
insertDict = insertWithDict $ const id

(↦) ∷ (Ord k) ⇒ k → v → (k,v)
(↦) = (,)

removeMinDict ∷ k ⇰ v → Maybe ((k,v),k ⇰ v)
removeMinDict = elimPrimDict Nothing $ map (mapSnd InhabitedDict) ∘ Map.minViewWithKey

removeMaxDict ∷ k ⇰ v → Maybe ((k,v),k ⇰ v)
removeMaxDict = elimPrimDict Nothing $ map (mapSnd InhabitedDict) ∘ Map.maxViewWithKey

unionWithDict ∷ (Old v → New v → v) → k ⇰ v → k ⇰ v → k ⇰ v
unionWithDict f = elimPrim21Dict EmptyDict InhabitedDict $ InhabitedDict ∘∘ Map.unionWith (flip f)

unionWithDictOn ∷ k ⇰ v → k ⇰ v → (Old v → New v → v) → k ⇰ v
unionWithDictOn d₁ d₂ f = unionWithDict f d₁ d₂

isSubdictOfBy ∷ (v → v → 𝔹) → k ⇰ v → k ⇰ v → 𝔹
isSubdictOfBy lte = elimPrim22Dict True (const True) (const False) $ Map.isSubmapOfBy lte

intersectionWithDict ∷ (Old v → New v → v) → k ⇰ v → k ⇰ v → k ⇰ v
intersectionWithDict f = elimPrim21Dict EmptyDict (const EmptyDict) $ 
  InhabitedDict ∘∘ Map.intersectionWith (flip f)

differenceWithDict ∷ (v → v → v) → k ⇰ v → k ⇰ v → k ⇰ v
differenceWithDict f = elimPrim22Dict EmptyDict (const EmptyDict) InhabitedDict $ 
  InhabitedDict ∘∘ Map.differenceWith (Just ∘∘ f)

modifyDict ∷ (v → v) → k → k ⇰ v → k ⇰ v
modifyDict f k m = learnDict m EmptyDict $ case lookup k m of
  Nothing → m
  Just x → insertDict k (f x) m

modifyDictOn ∷ k → (v → v) → k ⇰ v → k ⇰ v
modifyDictOn = flip modifyDict

onlyKeys ∷ (Ord k) ⇒ 𝒫 k → k ⇰ v → k ⇰ v
onlyKeys s m = iterOn s EmptyDict $ \ k → elimMaybe id (insertDict k) $ lookup k m

filterDict ∷ (v → 𝔹) → k ⇰ v → k ⇰ v
filterDict f = elimPrimDict EmptyDict $ InhabitedDict ∘ Map.filter f

-- # Lazy Set and Dict

instance (Ord a) ⇒ Eq (𝒫ᵇ a) where (==) = (==) `on` concretizeSet
instance (Ord a) ⇒ Ord (𝒫ᵇ a) where compare = compare `on` concretizeSet
instance (Ord a,Show a) ⇒ Show (𝒫ᵇ a) where show = chars ∘ (⧺) "setᵇ " ∘ 𝕤show ∘ list ∘ concretizeSet
instance ToFold a (𝒫ᵇ a) where fold = runLazySet
instance Singleton a (𝒫ᵇ a) where single = lazySet ∘ singleFold

instance Functor 𝒫ᵇ where
  map f = LazySet ∘ map f ∘ runLazySet

concretizeSet ∷ (Ord a) ⇒ 𝒫ᵇ a → 𝒫 a
concretizeSet (LazySet xs) = set xs

instance (Ord k,Eq v,Monoid v) ⇒ Eq (k ⇰♭⧺ v) where (==) = (==) `on` concretizeDictAppend
instance (Ord k,Ord v,Monoid v) ⇒ Ord (k ⇰♭⧺ v) where compare = compare `on` concretizeDictAppend
instance (Ord k,Show k,Show v,Monoid v) ⇒ Show (k ⇰♭⧺ v) where show = chars ∘ (⧺) "dictᵇ " ∘ 𝕤show ∘ list ∘ concretizeDictAppend
instance ToFold (k,v) (k ⇰♭⧺ v) where fold = runLazyDictAppend
instance Singleton (k,v) (k ⇰♭⧺ v) where single = lazyDictAppend ∘ singleFold

instance Monoid (k ⇰♭⧺ v) where
  null = LazyDictAppend null
  LazyDictAppend xs ⧺ LazyDictAppend ys = LazyDictAppend $ xs ⧺ ys

concretizeDictAppend ∷ (Ord k,Monoid v) ⇒ k ⇰♭⧺ v → k ⇰ v
concretizeDictAppend (LazyDictAppend kvs) = dictAppend kvs

mapKeyLazyDictAppend ∷ (k → k') → k ⇰♭⧺ v → k' ⇰♭⧺ v
mapKeyLazyDictAppend f = LazyDictAppend ∘ map (mapFst f) ∘ runLazyDictAppend

-- # Errors

error ∷ 𝕊 → a
error msg = Prelude.error (chars msg)

undefined ∷ a
undefined = error "undefined"

-- # IO

class MonadIO (m ∷ ★ → ★) where io ∷ IO a → m a
instance MonadIO IO where io = id

instance Functor IO where map = mmap
instance Monad IO where {return=Prelude.return;(≫=) = (Prelude.>>=)}

print ∷ (MonadIO m) ⇒ 𝕊 → m ()
print = io ∘ Text.putStr

printLn ∷ (MonadIO m) ⇒ 𝕊 → m ()
printLn = io ∘ Text.putStrLn

failIO ∷ (MonadIO m) ⇒ 𝕊 → m a
failIO = io ∘ Prelude.fail ∘ chars

abortIO ∷ (MonadIO m) ⇒ m a
abortIO = io $ exitWith $ ExitFailure $ 𝕚 1

readFile ∷ (MonadIO m) ⇒ 𝕊 → m 𝕊
readFile = io ∘ Text.readFile ∘ chars

readInput ∷ IO 𝕊
readInput = Text.getContents

writeFile ∷ (MonadIO m) ⇒ 𝕊 → 𝕊 → m ()
writeFile fn = io ∘ Text.writeFile (chars fn)

trace ∷ 𝕊 → a → a
trace s x = unsafePerformIO $ do
  printLn s
  return x

traceM ∷ (Monad m) ⇒ 𝕊 → m ()
traceM msg = trace msg $ return ()

ioFailure ∷ (Monad m,MonadIO m) ⇒ Maybe a → m a
ioFailure Nothing = abortIO
ioFailure (Just x) = return x


-- # Rebindable Syntax

ifThenElse ∷ 𝔹 → a → a → a
ifThenElse = fif

fromInteger ∷ ℤ → ℤ
fromInteger = id

fromString ∷ [ℂ] → 𝕊
fromString = 𝕤

fail ∷ [ℂ] → m a
fail = Prelude.error

(>>=) ∷ (Monad m) ⇒ m a → (a → m b) → m b
(>>=) = (≫=)

(>>) ∷ (Monad m) ⇒ m a → m b → m b
(>>) = (≫)