module UVMHS.Core.Init
  ( module UVMHS.Core.Init
  , module Control.Exception
  , module Data.Coerce
  , module GHC.Exts
  , module GHC.Stack
  , module Prelude
  , module Data.String
  ) where

import Prelude
  ( undefined,otherwise
  , Bool(..),Eq((==)),Ord(compare),Show(show),Ordering(..),IO
  , fromInteger
  )
import Data.Coerce 
  ( coerce
  , Coercible
  )
import GHC.Exts 
  ( type Constraint
  )
import GHC.Stack 
  ( type CallStack,callStack,withFrozenCallStack
  )

import Control.Exception
  ( assert
  )

import Data.String
  ( fromString
  )

import qualified Prelude as HS
import qualified GHC.Types as HS
import qualified GHC.Stack as HS

import qualified Data.Int as HS
import qualified Data.Ratio as HS
import qualified Data.Word as HS
import qualified Numeric.Natural as HS
import qualified Unsafe.Coerce as HS

import qualified Data.Text as Text

import qualified Data.Set as Set
import qualified Data.Map.Strict as Map
import qualified Data.Sequence as Sequence

import qualified Language.Haskell.TH.Syntax as TH

infixr 0 $

infixr 1 ⇰
infixl 2 ⩔
infixl 3 ⩓
infixl 5 ∨
infixl 6 ∧
infixl 7 ∘
infixl 8 :*
infixr 8 :&

------------------------------------
-- Numeric and Boolean Base Types --
------------------------------------

type ℕ   = HS.Natural
type ℕ64 = HS.Word64
type ℕ32 = HS.Word32
type ℕ16 = HS.Word16
type ℕ8  = HS.Word8
type ℤ   = HS.Integer
type ℤ64 = HS.Int64
type ℤ32 = HS.Int32
type ℤ16 = HS.Int16
type ℤ8  = HS.Int8
type ℚ   = HS.Rational
type ℚᴾ  = HS.Ratio ℕ
type 𝔻   = HS.Double

-- non-negative double
newtype 𝔻ᴾ = 𝔻ᴾ { 𝔻ᴾ -> 𝔻
un𝔻ᴾ ∷ 𝔻 }
  deriving (𝔻ᴾ -> 𝔻ᴾ -> Bool
(𝔻ᴾ -> 𝔻ᴾ -> Bool) -> (𝔻ᴾ -> 𝔻ᴾ -> Bool) -> Eq 𝔻ᴾ
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: 𝔻ᴾ -> 𝔻ᴾ -> Bool
== :: 𝔻ᴾ -> 𝔻ᴾ -> Bool
$c/= :: 𝔻ᴾ -> 𝔻ᴾ -> Bool
/= :: 𝔻ᴾ -> 𝔻ᴾ -> Bool
Eq,Eq 𝔻ᴾ
Eq 𝔻ᴾ =>
(𝔻ᴾ -> 𝔻ᴾ -> Ordering)
-> (𝔻ᴾ -> 𝔻ᴾ -> Bool)
-> (𝔻ᴾ -> 𝔻ᴾ -> Bool)
-> (𝔻ᴾ -> 𝔻ᴾ -> Bool)
-> (𝔻ᴾ -> 𝔻ᴾ -> Bool)
-> (𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ)
-> Ord 𝔻ᴾ
𝔻ᴾ -> 𝔻ᴾ -> Bool
𝔻ᴾ -> 𝔻ᴾ -> Ordering
𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: 𝔻ᴾ -> 𝔻ᴾ -> Ordering
compare :: 𝔻ᴾ -> 𝔻ᴾ -> Ordering
$c< :: 𝔻ᴾ -> 𝔻ᴾ -> Bool
< :: 𝔻ᴾ -> 𝔻ᴾ -> Bool
$c<= :: 𝔻ᴾ -> 𝔻ᴾ -> Bool
<= :: 𝔻ᴾ -> 𝔻ᴾ -> Bool
$c> :: 𝔻ᴾ -> 𝔻ᴾ -> Bool
> :: 𝔻ᴾ -> 𝔻ᴾ -> Bool
$c>= :: 𝔻ᴾ -> 𝔻ᴾ -> Bool
>= :: 𝔻ᴾ -> 𝔻ᴾ -> Bool
$cmax :: 𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ
max :: 𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ
$cmin :: 𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ
min :: 𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ
Ord,Int -> 𝔻ᴾ -> ShowS
[𝔻ᴾ] -> ShowS
𝔻ᴾ -> String
(Int -> 𝔻ᴾ -> ShowS)
-> (𝔻ᴾ -> String) -> ([𝔻ᴾ] -> ShowS) -> Show 𝔻ᴾ
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> 𝔻ᴾ -> ShowS
showsPrec :: Int -> 𝔻ᴾ -> ShowS
$cshow :: 𝔻ᴾ -> String
show :: 𝔻ᴾ -> String
$cshowList :: [𝔻ᴾ] -> ShowS
showList :: [𝔻ᴾ] -> ShowS
Show,ℤ -> 𝔻ᴾ
𝔻ᴾ -> 𝔻ᴾ
𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ
(𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ)
-> (ℤ -> 𝔻ᴾ)
-> Num 𝔻ᴾ
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (ℤ -> a)
-> Num a
$c+ :: 𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ
+ :: 𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ
$c- :: 𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ
- :: 𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ
$c* :: 𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ
* :: 𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ
$cnegate :: 𝔻ᴾ -> 𝔻ᴾ
negate :: 𝔻ᴾ -> 𝔻ᴾ
$cabs :: 𝔻ᴾ -> 𝔻ᴾ
abs :: 𝔻ᴾ -> 𝔻ᴾ
$csignum :: 𝔻ᴾ -> 𝔻ᴾ
signum :: 𝔻ᴾ -> 𝔻ᴾ
$cfromInteger :: ℤ -> 𝔻ᴾ
fromInteger :: ℤ -> 𝔻ᴾ
HS.Num,Num 𝔻ᴾ
Num 𝔻ᴾ =>
(𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ) -> (𝔻ᴾ -> 𝔻ᴾ) -> (ℚ -> 𝔻ᴾ) -> Fractional 𝔻ᴾ
ℚ -> 𝔻ᴾ
𝔻ᴾ -> 𝔻ᴾ
𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ
forall a.
Num a =>
(a -> a -> a) -> (a -> a) -> (ℚ -> a) -> Fractional a
$c/ :: 𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ
/ :: 𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ
$crecip :: 𝔻ᴾ -> 𝔻ᴾ
recip :: 𝔻ᴾ -> 𝔻ᴾ
$cfromRational :: ℚ -> 𝔻ᴾ
fromRational :: ℚ -> 𝔻ᴾ
HS.Fractional,Fractional 𝔻ᴾ
𝔻ᴾ
Fractional 𝔻ᴾ =>
𝔻ᴾ
-> (𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ)
-> (𝔻ᴾ -> 𝔻ᴾ)
-> Floating 𝔻ᴾ
𝔻ᴾ -> 𝔻ᴾ
𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ
forall a.
Fractional a =>
a
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> Floating a
$cpi :: 𝔻ᴾ
pi :: 𝔻ᴾ
$cexp :: 𝔻ᴾ -> 𝔻ᴾ
exp :: 𝔻ᴾ -> 𝔻ᴾ
$clog :: 𝔻ᴾ -> 𝔻ᴾ
log :: 𝔻ᴾ -> 𝔻ᴾ
$csqrt :: 𝔻ᴾ -> 𝔻ᴾ
sqrt :: 𝔻ᴾ -> 𝔻ᴾ
$c** :: 𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ
** :: 𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ
$clogBase :: 𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ
logBase :: 𝔻ᴾ -> 𝔻ᴾ -> 𝔻ᴾ
$csin :: 𝔻ᴾ -> 𝔻ᴾ
sin :: 𝔻ᴾ -> 𝔻ᴾ
$ccos :: 𝔻ᴾ -> 𝔻ᴾ
cos :: 𝔻ᴾ -> 𝔻ᴾ
$ctan :: 𝔻ᴾ -> 𝔻ᴾ
tan :: 𝔻ᴾ -> 𝔻ᴾ
$casin :: 𝔻ᴾ -> 𝔻ᴾ
asin :: 𝔻ᴾ -> 𝔻ᴾ
$cacos :: 𝔻ᴾ -> 𝔻ᴾ
acos :: 𝔻ᴾ -> 𝔻ᴾ
$catan :: 𝔻ᴾ -> 𝔻ᴾ
atan :: 𝔻ᴾ -> 𝔻ᴾ
$csinh :: 𝔻ᴾ -> 𝔻ᴾ
sinh :: 𝔻ᴾ -> 𝔻ᴾ
$ccosh :: 𝔻ᴾ -> 𝔻ᴾ
cosh :: 𝔻ᴾ -> 𝔻ᴾ
$ctanh :: 𝔻ᴾ -> 𝔻ᴾ
tanh :: 𝔻ᴾ -> 𝔻ᴾ
$casinh :: 𝔻ᴾ -> 𝔻ᴾ
asinh :: 𝔻ᴾ -> 𝔻ᴾ
$cacosh :: 𝔻ᴾ -> 𝔻ᴾ
acosh :: 𝔻ᴾ -> 𝔻ᴾ
$catanh :: 𝔻ᴾ -> 𝔻ᴾ
atanh :: 𝔻ᴾ -> 𝔻ᴾ
$clog1p :: 𝔻ᴾ -> 𝔻ᴾ
log1p :: 𝔻ᴾ -> 𝔻ᴾ
$cexpm1 :: 𝔻ᴾ -> 𝔻ᴾ
expm1 :: 𝔻ᴾ -> 𝔻ᴾ
$clog1pexp :: 𝔻ᴾ -> 𝔻ᴾ
log1pexp :: 𝔻ᴾ -> 𝔻ᴾ
$clog1mexp :: 𝔻ᴾ -> 𝔻ᴾ
log1mexp :: 𝔻ᴾ -> 𝔻ᴾ
HS.Floating,Num 𝔻ᴾ
Ord 𝔻ᴾ
(Num 𝔻ᴾ, Ord 𝔻ᴾ) => (𝔻ᴾ -> ℚ) -> Real 𝔻ᴾ
𝔻ᴾ -> ℚ
forall a. (Num a, Ord a) => (a -> ℚ) -> Real a
$ctoRational :: 𝔻ᴾ -> ℚ
toRational :: 𝔻ᴾ -> ℚ
HS.Real)

-- union of integer, rational and double
data ℝ = Integer ℤ | Rational ℚ | Double 𝔻
  deriving (ℝ -> ℝ -> Bool
(ℝ -> ℝ -> Bool) -> (ℝ -> ℝ -> Bool) -> Eq ℝ
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ℝ -> ℝ -> Bool
== :: ℝ -> ℝ -> Bool
$c/= :: ℝ -> ℝ -> Bool
/= :: ℝ -> ℝ -> Bool
Eq,Eq ℝ
Eq ℝ =>
(ℝ -> ℝ -> Ordering)
-> (ℝ -> ℝ -> Bool)
-> (ℝ -> ℝ -> Bool)
-> (ℝ -> ℝ -> Bool)
-> (ℝ -> ℝ -> Bool)
-> (ℝ -> ℝ -> ℝ)
-> (ℝ -> ℝ -> ℝ)
-> Ord ℝ
ℝ -> ℝ -> Bool
ℝ -> ℝ -> Ordering
ℝ -> ℝ -> ℝ
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ℝ -> ℝ -> Ordering
compare :: ℝ -> ℝ -> Ordering
$c< :: ℝ -> ℝ -> Bool
< :: ℝ -> ℝ -> Bool
$c<= :: ℝ -> ℝ -> Bool
<= :: ℝ -> ℝ -> Bool
$c> :: ℝ -> ℝ -> Bool
> :: ℝ -> ℝ -> Bool
$c>= :: ℝ -> ℝ -> Bool
>= :: ℝ -> ℝ -> Bool
$cmax :: ℝ -> ℝ -> ℝ
max :: ℝ -> ℝ -> ℝ
$cmin :: ℝ -> ℝ -> ℝ
min :: ℝ -> ℝ -> ℝ
Ord,Int -> ℝ -> ShowS
[ℝ] -> ShowS
ℝ -> String
(Int -> ℝ -> ShowS) -> (ℝ -> String) -> ([ℝ] -> ShowS) -> Show ℝ
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ℝ -> ShowS
showsPrec :: Int -> ℝ -> ShowS
$cshow :: ℝ -> String
show :: ℝ -> String
$cshowList :: [ℝ] -> ShowS
showList :: [ℝ] -> ShowS
Show)

-- non-negative variant of ^^
data ℝᴾ = Natural ℕ | Rationalᴾ ℚᴾ | Doubleᴾ 𝔻ᴾ
  deriving (ℝᴾ -> ℝᴾ -> Bool
(ℝᴾ -> ℝᴾ -> Bool) -> (ℝᴾ -> ℝᴾ -> Bool) -> Eq ℝᴾ
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ℝᴾ -> ℝᴾ -> Bool
== :: ℝᴾ -> ℝᴾ -> Bool
$c/= :: ℝᴾ -> ℝᴾ -> Bool
/= :: ℝᴾ -> ℝᴾ -> Bool
Eq,Eq ℝᴾ
Eq ℝᴾ =>
(ℝᴾ -> ℝᴾ -> Ordering)
-> (ℝᴾ -> ℝᴾ -> Bool)
-> (ℝᴾ -> ℝᴾ -> Bool)
-> (ℝᴾ -> ℝᴾ -> Bool)
-> (ℝᴾ -> ℝᴾ -> Bool)
-> (ℝᴾ -> ℝᴾ -> ℝᴾ)
-> (ℝᴾ -> ℝᴾ -> ℝᴾ)
-> Ord ℝᴾ
ℝᴾ -> ℝᴾ -> Bool
ℝᴾ -> ℝᴾ -> Ordering
ℝᴾ -> ℝᴾ -> ℝᴾ
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ℝᴾ -> ℝᴾ -> Ordering
compare :: ℝᴾ -> ℝᴾ -> Ordering
$c< :: ℝᴾ -> ℝᴾ -> Bool
< :: ℝᴾ -> ℝᴾ -> Bool
$c<= :: ℝᴾ -> ℝᴾ -> Bool
<= :: ℝᴾ -> ℝᴾ -> Bool
$c> :: ℝᴾ -> ℝᴾ -> Bool
> :: ℝᴾ -> ℝᴾ -> Bool
$c>= :: ℝᴾ -> ℝᴾ -> Bool
>= :: ℝᴾ -> ℝᴾ -> Bool
$cmax :: ℝᴾ -> ℝᴾ -> ℝᴾ
max :: ℝᴾ -> ℝᴾ -> ℝᴾ
$cmin :: ℝᴾ -> ℝᴾ -> ℝᴾ
min :: ℝᴾ -> ℝᴾ -> ℝᴾ
Ord,Int -> ℝᴾ -> ShowS
[ℝᴾ] -> ShowS
ℝᴾ -> String
(Int -> ℝᴾ -> ShowS)
-> (ℝᴾ -> String) -> ([ℝᴾ] -> ShowS) -> Show ℝᴾ
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ℝᴾ -> ShowS
showsPrec :: Int -> ℝᴾ -> ShowS
$cshow :: ℝᴾ -> String
show :: ℝᴾ -> String
$cshowList :: [ℝᴾ] -> ShowS
showList :: [ℝᴾ] -> ShowS
Show)

-- bools
type 𝔹 = HS.Bool

not ∷ 𝔹 → 𝔹
not :: Bool -> Bool
not Bool
True = Bool
False
not Bool
False = Bool
True

(⩔) ∷ 𝔹 → 𝔹 → 𝔹
Bool
b₁ ⩔ :: Bool -> Bool -> Bool
⩔ ~Bool
b₂ = if Bool
b₁ then Bool
True else Bool
b₂

(⩓) ∷ 𝔹 → 𝔹 → 𝔹
Bool
b₁ ⩓ :: Bool -> Bool -> Bool
⩓ ~Bool
b₂ = if Bool
b₁ then Bool
b₂ else Bool
False

cond ∷ 𝔹 → a → a → a
cond :: forall a. Bool -> a -> a -> a
cond Bool
b ~a
x ~a
y = case Bool
b of { Bool
True → a
x ; Bool
False → a
y }

---------------------------
-- Char and String Types --
---------------------------

type ℂ = HS.Char
type 𝕊 = Text.Text

-----------------------
-- "Algebraic" Types --
-----------------------

data Void

exfalso ∷ Void → a
exfalso :: forall a. Void -> a
exfalso = Void -> a
\case

data a ∨ b = Inl a | Inr b
  deriving ((a ∨ b) -> (a ∨ b) -> Bool
((a ∨ b) -> (a ∨ b) -> Bool)
-> ((a ∨ b) -> (a ∨ b) -> Bool) -> Eq (a ∨ b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b. (Eq a, Eq b) => (a ∨ b) -> (a ∨ b) -> Bool
$c== :: forall a b. (Eq a, Eq b) => (a ∨ b) -> (a ∨ b) -> Bool
== :: (a ∨ b) -> (a ∨ b) -> Bool
$c/= :: forall a b. (Eq a, Eq b) => (a ∨ b) -> (a ∨ b) -> Bool
/= :: (a ∨ b) -> (a ∨ b) -> Bool
Eq,Eq (a ∨ b)
Eq (a ∨ b) =>
((a ∨ b) -> (a ∨ b) -> Ordering)
-> ((a ∨ b) -> (a ∨ b) -> Bool)
-> ((a ∨ b) -> (a ∨ b) -> Bool)
-> ((a ∨ b) -> (a ∨ b) -> Bool)
-> ((a ∨ b) -> (a ∨ b) -> Bool)
-> ((a ∨ b) -> (a ∨ b) -> a ∨ b)
-> ((a ∨ b) -> (a ∨ b) -> a ∨ b)
-> Ord (a ∨ b)
(a ∨ b) -> (a ∨ b) -> Bool
(a ∨ b) -> (a ∨ b) -> Ordering
(a ∨ b) -> (a ∨ b) -> a ∨ b
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a b. (Ord a, Ord b) => Eq (a ∨ b)
forall a b. (Ord a, Ord b) => (a ∨ b) -> (a ∨ b) -> Bool
forall a b. (Ord a, Ord b) => (a ∨ b) -> (a ∨ b) -> Ordering
forall a b. (Ord a, Ord b) => (a ∨ b) -> (a ∨ b) -> a ∨ b
$ccompare :: forall a b. (Ord a, Ord b) => (a ∨ b) -> (a ∨ b) -> Ordering
compare :: (a ∨ b) -> (a ∨ b) -> Ordering
$c< :: forall a b. (Ord a, Ord b) => (a ∨ b) -> (a ∨ b) -> Bool
< :: (a ∨ b) -> (a ∨ b) -> Bool
$c<= :: forall a b. (Ord a, Ord b) => (a ∨ b) -> (a ∨ b) -> Bool
<= :: (a ∨ b) -> (a ∨ b) -> Bool
$c> :: forall a b. (Ord a, Ord b) => (a ∨ b) -> (a ∨ b) -> Bool
> :: (a ∨ b) -> (a ∨ b) -> Bool
$c>= :: forall a b. (Ord a, Ord b) => (a ∨ b) -> (a ∨ b) -> Bool
>= :: (a ∨ b) -> (a ∨ b) -> Bool
$cmax :: forall a b. (Ord a, Ord b) => (a ∨ b) -> (a ∨ b) -> a ∨ b
max :: (a ∨ b) -> (a ∨ b) -> a ∨ b
$cmin :: forall a b. (Ord a, Ord b) => (a ∨ b) -> (a ∨ b) -> a ∨ b
min :: (a ∨ b) -> (a ∨ b) -> a ∨ b
Ord,Int -> (a ∨ b) -> ShowS
[a ∨ b] -> ShowS
(a ∨ b) -> String
(Int -> (a ∨ b) -> ShowS)
-> ((a ∨ b) -> String) -> ([a ∨ b] -> ShowS) -> Show (a ∨ b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> (a ∨ b) -> ShowS
forall a b. (Show a, Show b) => [a ∨ b] -> ShowS
forall a b. (Show a, Show b) => (a ∨ b) -> String
$cshowsPrec :: forall a b. (Show a, Show b) => Int -> (a ∨ b) -> ShowS
showsPrec :: Int -> (a ∨ b) -> ShowS
$cshow :: forall a b. (Show a, Show b) => (a ∨ b) -> String
show :: (a ∨ b) -> String
$cshowList :: forall a b. (Show a, Show b) => [a ∨ b] -> ShowS
showList :: [a ∨ b] -> ShowS
Show)
data a ∧ b = a :* b
  deriving ((a ∧ b) -> (a ∧ b) -> Bool
((a ∧ b) -> (a ∧ b) -> Bool)
-> ((a ∧ b) -> (a ∧ b) -> Bool) -> Eq (a ∧ b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b. (Eq a, Eq b) => (a ∧ b) -> (a ∧ b) -> Bool
$c== :: forall a b. (Eq a, Eq b) => (a ∧ b) -> (a ∧ b) -> Bool
== :: (a ∧ b) -> (a ∧ b) -> Bool
$c/= :: forall a b. (Eq a, Eq b) => (a ∧ b) -> (a ∧ b) -> Bool
/= :: (a ∧ b) -> (a ∧ b) -> Bool
Eq,Eq (a ∧ b)
Eq (a ∧ b) =>
((a ∧ b) -> (a ∧ b) -> Ordering)
-> ((a ∧ b) -> (a ∧ b) -> Bool)
-> ((a ∧ b) -> (a ∧ b) -> Bool)
-> ((a ∧ b) -> (a ∧ b) -> Bool)
-> ((a ∧ b) -> (a ∧ b) -> Bool)
-> ((a ∧ b) -> (a ∧ b) -> a ∧ b)
-> ((a ∧ b) -> (a ∧ b) -> a ∧ b)
-> Ord (a ∧ b)
(a ∧ b) -> (a ∧ b) -> Bool
(a ∧ b) -> (a ∧ b) -> Ordering
(a ∧ b) -> (a ∧ b) -> a ∧ b
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a b. (Ord a, Ord b) => Eq (a ∧ b)
forall a b. (Ord a, Ord b) => (a ∧ b) -> (a ∧ b) -> Bool
forall a b. (Ord a, Ord b) => (a ∧ b) -> (a ∧ b) -> Ordering
forall a b. (Ord a, Ord b) => (a ∧ b) -> (a ∧ b) -> a ∧ b
$ccompare :: forall a b. (Ord a, Ord b) => (a ∧ b) -> (a ∧ b) -> Ordering
compare :: (a ∧ b) -> (a ∧ b) -> Ordering
$c< :: forall a b. (Ord a, Ord b) => (a ∧ b) -> (a ∧ b) -> Bool
< :: (a ∧ b) -> (a ∧ b) -> Bool
$c<= :: forall a b. (Ord a, Ord b) => (a ∧ b) -> (a ∧ b) -> Bool
<= :: (a ∧ b) -> (a ∧ b) -> Bool
$c> :: forall a b. (Ord a, Ord b) => (a ∧ b) -> (a ∧ b) -> Bool
> :: (a ∧ b) -> (a ∧ b) -> Bool
$c>= :: forall a b. (Ord a, Ord b) => (a ∧ b) -> (a ∧ b) -> Bool
>= :: (a ∧ b) -> (a ∧ b) -> Bool
$cmax :: forall a b. (Ord a, Ord b) => (a ∧ b) -> (a ∧ b) -> a ∧ b
max :: (a ∧ b) -> (a ∧ b) -> a ∧ b
$cmin :: forall a b. (Ord a, Ord b) => (a ∧ b) -> (a ∧ b) -> a ∧ b
min :: (a ∧ b) -> (a ∧ b) -> a ∧ b
Ord,Int -> (a ∧ b) -> ShowS
[a ∧ b] -> ShowS
(a ∧ b) -> String
(Int -> (a ∧ b) -> ShowS)
-> ((a ∧ b) -> String) -> ([a ∧ b] -> ShowS) -> Show (a ∧ b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> (a ∧ b) -> ShowS
forall a b. (Show a, Show b) => [a ∧ b] -> ShowS
forall a b. (Show a, Show b) => (a ∧ b) -> String
$cshowsPrec :: forall a b. (Show a, Show b) => Int -> (a ∧ b) -> ShowS
showsPrec :: Int -> (a ∧ b) -> ShowS
$cshow :: forall a b. (Show a, Show b) => (a ∧ b) -> String
show :: (a ∧ b) -> String
$cshowList :: forall a b. (Show a, Show b) => [a ∧ b] -> ShowS
showList :: [a ∧ b] -> ShowS
Show)

----------------------
-- Collection Types --
----------------------

data 𝑂 a = None | Some a
  deriving (𝑂 a -> 𝑂 a -> Bool
(𝑂 a -> 𝑂 a -> Bool) -> (𝑂 a -> 𝑂 a -> Bool) -> Eq (𝑂 a)
forall a. Eq a => 𝑂 a -> 𝑂 a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => 𝑂 a -> 𝑂 a -> Bool
== :: 𝑂 a -> 𝑂 a -> Bool
$c/= :: forall a. Eq a => 𝑂 a -> 𝑂 a -> Bool
/= :: 𝑂 a -> 𝑂 a -> Bool
Eq,Eq (𝑂 a)
Eq (𝑂 a) =>
(𝑂 a -> 𝑂 a -> Ordering)
-> (𝑂 a -> 𝑂 a -> Bool)
-> (𝑂 a -> 𝑂 a -> Bool)
-> (𝑂 a -> 𝑂 a -> Bool)
-> (𝑂 a -> 𝑂 a -> Bool)
-> (𝑂 a -> 𝑂 a -> 𝑂 a)
-> (𝑂 a -> 𝑂 a -> 𝑂 a)
-> Ord (𝑂 a)
𝑂 a -> 𝑂 a -> Bool
𝑂 a -> 𝑂 a -> Ordering
𝑂 a -> 𝑂 a -> 𝑂 a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (𝑂 a)
forall a. Ord a => 𝑂 a -> 𝑂 a -> Bool
forall a. Ord a => 𝑂 a -> 𝑂 a -> Ordering
forall a. Ord a => 𝑂 a -> 𝑂 a -> 𝑂 a
$ccompare :: forall a. Ord a => 𝑂 a -> 𝑂 a -> Ordering
compare :: 𝑂 a -> 𝑂 a -> Ordering
$c< :: forall a. Ord a => 𝑂 a -> 𝑂 a -> Bool
< :: 𝑂 a -> 𝑂 a -> Bool
$c<= :: forall a. Ord a => 𝑂 a -> 𝑂 a -> Bool
<= :: 𝑂 a -> 𝑂 a -> Bool
$c> :: forall a. Ord a => 𝑂 a -> 𝑂 a -> Bool
> :: 𝑂 a -> 𝑂 a -> Bool
$c>= :: forall a. Ord a => 𝑂 a -> 𝑂 a -> Bool
>= :: 𝑂 a -> 𝑂 a -> Bool
$cmax :: forall a. Ord a => 𝑂 a -> 𝑂 a -> 𝑂 a
max :: 𝑂 a -> 𝑂 a -> 𝑂 a
$cmin :: forall a. Ord a => 𝑂 a -> 𝑂 a -> 𝑂 a
min :: 𝑂 a -> 𝑂 a -> 𝑂 a
Ord,Int -> 𝑂 a -> ShowS
[𝑂 a] -> ShowS
𝑂 a -> String
(Int -> 𝑂 a -> ShowS)
-> (𝑂 a -> String) -> ([𝑂 a] -> ShowS) -> Show (𝑂 a)
forall a. Show a => Int -> 𝑂 a -> ShowS
forall a. Show a => [𝑂 a] -> ShowS
forall a. Show a => 𝑂 a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> 𝑂 a -> ShowS
showsPrec :: Int -> 𝑂 a -> ShowS
$cshow :: forall a. Show a => 𝑂 a -> String
show :: 𝑂 a -> String
$cshowList :: forall a. Show a => [𝑂 a] -> ShowS
showList :: [𝑂 a] -> ShowS
Show)
data 𝐿 a = Nil | a :& 𝐿 a
  deriving (𝐿 a -> 𝐿 a -> Bool
(𝐿 a -> 𝐿 a -> Bool) -> (𝐿 a -> 𝐿 a -> Bool) -> Eq (𝐿 a)
forall a. Eq a => 𝐿 a -> 𝐿 a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => 𝐿 a -> 𝐿 a -> Bool
== :: 𝐿 a -> 𝐿 a -> Bool
$c/= :: forall a. Eq a => 𝐿 a -> 𝐿 a -> Bool
/= :: 𝐿 a -> 𝐿 a -> Bool
Eq,Eq (𝐿 a)
Eq (𝐿 a) =>
(𝐿 a -> 𝐿 a -> Ordering)
-> (𝐿 a -> 𝐿 a -> Bool)
-> (𝐿 a -> 𝐿 a -> Bool)
-> (𝐿 a -> 𝐿 a -> Bool)
-> (𝐿 a -> 𝐿 a -> Bool)
-> (𝐿 a -> 𝐿 a -> 𝐿 a)
-> (𝐿 a -> 𝐿 a -> 𝐿 a)
-> Ord (𝐿 a)
𝐿 a -> 𝐿 a -> Bool
𝐿 a -> 𝐿 a -> Ordering
𝐿 a -> 𝐿 a -> 𝐿 a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (𝐿 a)
forall a. Ord a => 𝐿 a -> 𝐿 a -> Bool
forall a. Ord a => 𝐿 a -> 𝐿 a -> Ordering
forall a. Ord a => 𝐿 a -> 𝐿 a -> 𝐿 a
$ccompare :: forall a. Ord a => 𝐿 a -> 𝐿 a -> Ordering
compare :: 𝐿 a -> 𝐿 a -> Ordering
$c< :: forall a. Ord a => 𝐿 a -> 𝐿 a -> Bool
< :: 𝐿 a -> 𝐿 a -> Bool
$c<= :: forall a. Ord a => 𝐿 a -> 𝐿 a -> Bool
<= :: 𝐿 a -> 𝐿 a -> Bool
$c> :: forall a. Ord a => 𝐿 a -> 𝐿 a -> Bool
> :: 𝐿 a -> 𝐿 a -> Bool
$c>= :: forall a. Ord a => 𝐿 a -> 𝐿 a -> Bool
>= :: 𝐿 a -> 𝐿 a -> Bool
$cmax :: forall a. Ord a => 𝐿 a -> 𝐿 a -> 𝐿 a
max :: 𝐿 a -> 𝐿 a -> 𝐿 a
$cmin :: forall a. Ord a => 𝐿 a -> 𝐿 a -> 𝐿 a
min :: 𝐿 a -> 𝐿 a -> 𝐿 a
Ord,(forall (m :: * -> *). Quote m => 𝐿 a -> m Exp)
-> (forall (m :: * -> *). Quote m => 𝐿 a -> Code m (𝐿 a))
-> Lift (𝐿 a)
forall a (m :: * -> *). (Lift a, Quote m) => 𝐿 a -> m Exp
forall a (m :: * -> *). (Lift a, Quote m) => 𝐿 a -> Code m (𝐿 a)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => 𝐿 a -> m Exp
forall (m :: * -> *). Quote m => 𝐿 a -> Code m (𝐿 a)
$clift :: forall a (m :: * -> *). (Lift a, Quote m) => 𝐿 a -> m Exp
lift :: forall (m :: * -> *). Quote m => 𝐿 a -> m Exp
$cliftTyped :: forall a (m :: * -> *). (Lift a, Quote m) => 𝐿 a -> Code m (𝐿 a)
liftTyped :: forall (m :: * -> *). Quote m => 𝐿 a -> Code m (𝐿 a)
TH.Lift)

-- iterator type             
--                           fold function               continuation
--                           ↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓       ↓↓↓↓↓↓↓
newtype 𝐼 a = 𝐼 { forall a.
𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
un𝐼 ∷ ∀ b. (a → b → (b → b) → b) → b → (b → b) → b }
--                                ↑   ↑↑↑↑↑↑↑        ↑
--                      accumulator   continuation   accumulator


run𝐼 ∷ (b → b) → b → (a → b → (b → b) → b) → 𝐼 a → b
run𝐼 :: forall b a. (b -> b) -> b -> (a -> b -> (b -> b) -> b) -> 𝐼 a -> b
run𝐼 b -> b
𝓀 b
i a -> b -> (b -> b) -> b
f 𝐼 a
xs = 𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
forall a.
𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
un𝐼 𝐼 a
xs a -> b -> (b -> b) -> b
f b
i b -> b
𝓀

run𝐼On ∷ 𝐼 a → (b → b) → b → (a → b → (b → b) → b) → b
run𝐼On :: forall a b. 𝐼 a -> (b -> b) -> b -> (a -> b -> (b -> b) -> b) -> b
run𝐼On 𝐼 a
xs b -> b
𝓀 b
i a -> b -> (b -> b) -> b
f = 𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
forall a.
𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
un𝐼 𝐼 a
xs a -> b -> (b -> b) -> b
f b
i b -> b
𝓀

foldk𝐼 ∷ b → (a → b → (b → b) → b) → 𝐼 a → b
foldk𝐼 :: forall b a. b -> (a -> b -> (b -> b) -> b) -> 𝐼 a -> b
foldk𝐼 = (b -> b) -> b -> (a -> b -> (b -> b) -> b) -> 𝐼 a -> b
forall b a. (b -> b) -> b -> (a -> b -> (b -> b) -> b) -> 𝐼 a -> b
run𝐼 b -> b
forall a. a -> a
id

-- accumulate values in natural order
-- (i.e., from "left to right")
-- constant space overhead
fold𝐼 ∷ b → (a → b → b) → 𝐼 a → b
fold𝐼 :: forall b a. b -> (a -> b -> b) -> 𝐼 a -> b
fold𝐼 b
i₀ a -> b -> b
f = (b -> b) -> b -> (a -> b -> (b -> b) -> b) -> 𝐼 a -> b
forall b a. (b -> b) -> b -> (a -> b -> (b -> b) -> b) -> 𝐼 a -> b
run𝐼 b -> b
forall a. a -> a
id b
i₀ ((a -> b -> (b -> b) -> b) -> 𝐼 a -> b)
-> (a -> b -> (b -> b) -> b) -> 𝐼 a -> b
forall a b. (a -> b) -> a -> b
$ \ a
x b
i b -> b
𝓀 → b -> b
𝓀 (b -> b) -> b -> b
forall a b. (a -> b) -> a -> b
$ a -> b -> b
f a
x b
i

-- accumulate values in reverse order
-- (i.e., from "right to left")
-- linear space overhead
foldr𝐼 ∷ b → (a → b → b) → 𝐼 a → b
foldr𝐼 :: forall b a. b -> (a -> b -> b) -> 𝐼 a -> b
foldr𝐼 b
i₀ a -> b -> b
f = (b -> b) -> b -> (a -> b -> (b -> b) -> b) -> 𝐼 a -> b
forall b a. (b -> b) -> b -> (a -> b -> (b -> b) -> b) -> 𝐼 a -> b
run𝐼 b -> b
forall a. a -> a
id b
i₀ ((a -> b -> (b -> b) -> b) -> 𝐼 a -> b)
-> (a -> b -> (b -> b) -> b) -> 𝐼 a -> b
forall a b. (a -> b) -> a -> b
$ \ a
x b
i b -> b
𝓀 → a -> b -> b
f a
x (b -> b) -> b -> b
forall a b. (a -> b) -> a -> b
$ b -> b
𝓀 b
i

map𝐼 ∷ (a → b) → 𝐼 a → 𝐼 b
map𝐼 :: forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
map𝐼 a -> b
f 𝐼 a
xs = (forall b. (b -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 b
forall a.
(forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
𝐼 ((forall b. (b -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
 -> 𝐼 b)
-> (forall b. (b -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
-> 𝐼 b
forall a b. (a -> b) -> a -> b
HS.$ \ b -> b -> (b -> b) -> b
g → 𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
forall a.
𝐼 a -> forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
un𝐼 𝐼 a
xs ((a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
-> (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ b -> b -> (b -> b) -> b
g (b -> b -> (b -> b) -> b) -> (a -> b) -> a -> b -> (b -> b) -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> b
f

null𝐼 ∷ 𝐼 a
null𝐼 :: forall a. 𝐼 a
null𝐼 = (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.$ (b -> (b -> b) -> b)
-> (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b
forall a b. a -> b -> a
const ((b -> (b -> b) -> b)
 -> (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
-> (b -> (b -> b) -> b)
-> (a -> b -> (b -> b) -> b)
-> b
-> (b -> b)
-> b
forall a b. (a -> b) -> a -> b
$ \ b
i b -> b
𝓀 → b -> b
𝓀 b
i

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

list𝐼 ∷ 𝐼 a → 𝐿 a
list𝐼 :: forall a. 𝐼 a -> 𝐿 a
list𝐼 = 𝐿 a -> (a -> 𝐿 a -> 𝐿 a) -> 𝐼 a -> 𝐿 a
forall b a. b -> (a -> b -> b) -> 𝐼 a -> b
foldr𝐼 𝐿 a
forall a. 𝐿 a
Nil a -> 𝐿 a -> 𝐿 a
forall a. a -> 𝐿 a -> 𝐿 a
(:&)

iter𝐿 ∷ 𝐿 a → 𝐼 a
iter𝐿 :: forall a. 𝐿 a -> 𝐼 a
iter𝐿 𝐿 a
xs₀ = (forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
forall a.
(forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
𝐼 ((forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
 -> 𝐼 a)
-> (forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
-> 𝐼 a
forall a b. (a -> b) -> a -> b
HS.$ \ a -> b -> (b -> b) -> b
f → ((b -> b) -> b -> b) -> b -> (b -> b) -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((b -> b) -> b -> b) -> b -> (b -> b) -> b)
-> ((b -> b) -> b -> b) -> b -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b -> b
𝓀 →
  let loop :: 𝐿 a -> b -> b
loop 𝐿 a
xs b
i = case 𝐿 a
xs of
        𝐿 a
Nil → b -> b
𝓀 b
i
        a
x :& 𝐿 a
xs' →
          a -> b -> (b -> b) -> b
f a
x b
i ((b -> b) -> b) -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b
i' →
          𝐿 a -> b -> b
loop 𝐿 a
xs' b
i'
  in 𝐿 a -> b -> b
loop 𝐿 a
xs₀

lazyList𝐼 ∷ 𝐼 a → [a]
lazyList𝐼 :: forall a. 𝐼 a -> [a]
lazyList𝐼 = [a] -> (a -> [a] -> [a]) -> 𝐼 a -> [a]
forall b a. b -> (a -> b -> b) -> 𝐼 a -> b
foldr𝐼 [] (:)

iterLL ∷ [a] → 𝐼 a
iterLL :: forall a. [a] -> 𝐼 a
iterLL [a]
xs₀ = (forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
forall a.
(forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
𝐼 ((forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
 -> 𝐼 a)
-> (forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
-> 𝐼 a
forall a b. (a -> b) -> a -> b
HS.$ \ a -> b -> (b -> b) -> b
f → ((b -> b) -> b -> b) -> b -> (b -> b) -> b
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((b -> b) -> b -> b) -> b -> (b -> b) -> b)
-> ((b -> b) -> b -> b) -> b -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b -> b
𝓀 →
  let loop :: [a] -> b -> b
loop [a]
xs b
i = case [a]
xs of
        [] → b -> b
𝓀 b
i
        a
x:[a]
xs' → 
          a -> b -> (b -> b) -> b
f a
x b
i ((b -> b) -> b) -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b
i' →
          [a] -> b -> b
loop [a]
xs' b
i'
  in [a] -> b -> b
loop [a]
xs₀

-- stream
newtype 𝑆 a = 𝑆 { forall a. 𝑆 a -> () -> 𝑂 (a ∧ 𝑆 a)
un𝑆 ∷ () → 𝑂 (a ∧ 𝑆 a) }
-- sequence (finger trees)
newtype 𝑄 a = 𝑄 { forall a. 𝑄 a -> Seq a
un𝑄 ∷ Sequence.Seq a }
  deriving (𝑄 a -> 𝑄 a -> Bool
(𝑄 a -> 𝑄 a -> Bool) -> (𝑄 a -> 𝑄 a -> Bool) -> Eq (𝑄 a)
forall a. Eq a => 𝑄 a -> 𝑄 a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => 𝑄 a -> 𝑄 a -> Bool
== :: 𝑄 a -> 𝑄 a -> Bool
$c/= :: forall a. Eq a => 𝑄 a -> 𝑄 a -> Bool
/= :: 𝑄 a -> 𝑄 a -> Bool
Eq,Eq (𝑄 a)
Eq (𝑄 a) =>
(𝑄 a -> 𝑄 a -> Ordering)
-> (𝑄 a -> 𝑄 a -> Bool)
-> (𝑄 a -> 𝑄 a -> Bool)
-> (𝑄 a -> 𝑄 a -> Bool)
-> (𝑄 a -> 𝑄 a -> Bool)
-> (𝑄 a -> 𝑄 a -> 𝑄 a)
-> (𝑄 a -> 𝑄 a -> 𝑄 a)
-> Ord (𝑄 a)
𝑄 a -> 𝑄 a -> Bool
𝑄 a -> 𝑄 a -> Ordering
𝑄 a -> 𝑄 a -> 𝑄 a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (𝑄 a)
forall a. Ord a => 𝑄 a -> 𝑄 a -> Bool
forall a. Ord a => 𝑄 a -> 𝑄 a -> Ordering
forall a. Ord a => 𝑄 a -> 𝑄 a -> 𝑄 a
$ccompare :: forall a. Ord a => 𝑄 a -> 𝑄 a -> Ordering
compare :: 𝑄 a -> 𝑄 a -> Ordering
$c< :: forall a. Ord a => 𝑄 a -> 𝑄 a -> Bool
< :: 𝑄 a -> 𝑄 a -> Bool
$c<= :: forall a. Ord a => 𝑄 a -> 𝑄 a -> Bool
<= :: 𝑄 a -> 𝑄 a -> Bool
$c> :: forall a. Ord a => 𝑄 a -> 𝑄 a -> Bool
> :: 𝑄 a -> 𝑄 a -> Bool
$c>= :: forall a. Ord a => 𝑄 a -> 𝑄 a -> Bool
>= :: 𝑄 a -> 𝑄 a -> Bool
$cmax :: forall a. Ord a => 𝑄 a -> 𝑄 a -> 𝑄 a
max :: 𝑄 a -> 𝑄 a -> 𝑄 a
$cmin :: forall a. Ord a => 𝑄 a -> 𝑄 a -> 𝑄 a
min :: 𝑄 a -> 𝑄 a -> 𝑄 a
Ord)
-- set (BB-ω trees)
newtype 𝑃 a = 𝑃 { forall a. 𝑃 a -> Set a
un𝑃 ∷ Set.Set a }
  deriving (𝑃 a -> 𝑃 a -> Bool
(𝑃 a -> 𝑃 a -> Bool) -> (𝑃 a -> 𝑃 a -> Bool) -> Eq (𝑃 a)
forall a. Eq a => 𝑃 a -> 𝑃 a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => 𝑃 a -> 𝑃 a -> Bool
== :: 𝑃 a -> 𝑃 a -> Bool
$c/= :: forall a. Eq a => 𝑃 a -> 𝑃 a -> Bool
/= :: 𝑃 a -> 𝑃 a -> Bool
Eq,Eq (𝑃 a)
Eq (𝑃 a) =>
(𝑃 a -> 𝑃 a -> Ordering)
-> (𝑃 a -> 𝑃 a -> Bool)
-> (𝑃 a -> 𝑃 a -> Bool)
-> (𝑃 a -> 𝑃 a -> Bool)
-> (𝑃 a -> 𝑃 a -> Bool)
-> (𝑃 a -> 𝑃 a -> 𝑃 a)
-> (𝑃 a -> 𝑃 a -> 𝑃 a)
-> Ord (𝑃 a)
𝑃 a -> 𝑃 a -> Bool
𝑃 a -> 𝑃 a -> Ordering
𝑃 a -> 𝑃 a -> 𝑃 a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (𝑃 a)
forall a. Ord a => 𝑃 a -> 𝑃 a -> Bool
forall a. Ord a => 𝑃 a -> 𝑃 a -> Ordering
forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
$ccompare :: forall a. Ord a => 𝑃 a -> 𝑃 a -> Ordering
compare :: 𝑃 a -> 𝑃 a -> Ordering
$c< :: forall a. Ord a => 𝑃 a -> 𝑃 a -> Bool
< :: 𝑃 a -> 𝑃 a -> Bool
$c<= :: forall a. Ord a => 𝑃 a -> 𝑃 a -> Bool
<= :: 𝑃 a -> 𝑃 a -> Bool
$c> :: forall a. Ord a => 𝑃 a -> 𝑃 a -> Bool
> :: 𝑃 a -> 𝑃 a -> Bool
$c>= :: forall a. Ord a => 𝑃 a -> 𝑃 a -> Bool
>= :: 𝑃 a -> 𝑃 a -> Bool
$cmax :: forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
max :: 𝑃 a -> 𝑃 a -> 𝑃 a
$cmin :: forall a. Ord a => 𝑃 a -> 𝑃 a -> 𝑃 a
min :: 𝑃 a -> 𝑃 a -> 𝑃 a
Ord)
-- dictionary (BB-ω trees)
newtype k ⇰ v = 𝐷 { forall k v. (k ⇰ v) -> Map k v
un𝐷 ∷ Map.Map k v }
  deriving ((k ⇰ v) -> (k ⇰ v) -> Bool
((k ⇰ v) -> (k ⇰ v) -> Bool)
-> ((k ⇰ v) -> (k ⇰ v) -> Bool) -> Eq (k ⇰ v)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k v. (Eq k, Eq v) => (k ⇰ v) -> (k ⇰ v) -> Bool
$c== :: forall k v. (Eq k, Eq v) => (k ⇰ v) -> (k ⇰ v) -> Bool
== :: (k ⇰ v) -> (k ⇰ v) -> Bool
$c/= :: forall k v. (Eq k, Eq v) => (k ⇰ v) -> (k ⇰ v) -> Bool
/= :: (k ⇰ v) -> (k ⇰ v) -> Bool
Eq,Eq (k ⇰ v)
Eq (k ⇰ v) =>
((k ⇰ v) -> (k ⇰ v) -> Ordering)
-> ((k ⇰ v) -> (k ⇰ v) -> Bool)
-> ((k ⇰ v) -> (k ⇰ v) -> Bool)
-> ((k ⇰ v) -> (k ⇰ v) -> Bool)
-> ((k ⇰ v) -> (k ⇰ v) -> Bool)
-> ((k ⇰ v) -> (k ⇰ v) -> k ⇰ v)
-> ((k ⇰ v) -> (k ⇰ v) -> k ⇰ v)
-> Ord (k ⇰ v)
(k ⇰ v) -> (k ⇰ v) -> Bool
(k ⇰ v) -> (k ⇰ v) -> Ordering
(k ⇰ v) -> (k ⇰ v) -> k ⇰ v
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k v. (Ord k, Ord v) => Eq (k ⇰ v)
forall k v. (Ord k, Ord v) => (k ⇰ v) -> (k ⇰ v) -> Bool
forall k v. (Ord k, Ord v) => (k ⇰ v) -> (k ⇰ v) -> Ordering
forall k v. (Ord k, Ord v) => (k ⇰ v) -> (k ⇰ v) -> k ⇰ v
$ccompare :: forall k v. (Ord k, Ord v) => (k ⇰ v) -> (k ⇰ v) -> Ordering
compare :: (k ⇰ v) -> (k ⇰ v) -> Ordering
$c< :: forall k v. (Ord k, Ord v) => (k ⇰ v) -> (k ⇰ v) -> Bool
< :: (k ⇰ v) -> (k ⇰ v) -> Bool
$c<= :: forall k v. (Ord k, Ord v) => (k ⇰ v) -> (k ⇰ v) -> Bool
<= :: (k ⇰ v) -> (k ⇰ v) -> Bool
$c> :: forall k v. (Ord k, Ord v) => (k ⇰ v) -> (k ⇰ v) -> Bool
> :: (k ⇰ v) -> (k ⇰ v) -> Bool
$c>= :: forall k v. (Ord k, Ord v) => (k ⇰ v) -> (k ⇰ v) -> Bool
>= :: (k ⇰ v) -> (k ⇰ v) -> Bool
$cmax :: forall k v. (Ord k, Ord v) => (k ⇰ v) -> (k ⇰ v) -> k ⇰ v
max :: (k ⇰ v) -> (k ⇰ v) -> k ⇰ v
$cmin :: forall k v. (Ord k, Ord v) => (k ⇰ v) -> (k ⇰ v) -> k ⇰ v
min :: (k ⇰ v) -> (k ⇰ v) -> k ⇰ v
Ord)

------------------------
-- Other Useful Types --
------------------------

data Lazy a = Lazy { forall a. Lazy a -> a
unLazy ∷ ~a }

data Nat = Z | S Nat
  deriving (Nat -> Nat -> Bool
(Nat -> Nat -> Bool) -> (Nat -> Nat -> Bool) -> Eq Nat
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Nat -> Nat -> Bool
== :: Nat -> Nat -> Bool
$c/= :: Nat -> Nat -> Bool
/= :: Nat -> Nat -> Bool
Eq,Eq Nat
Eq Nat =>
(Nat -> Nat -> Ordering)
-> (Nat -> Nat -> Bool)
-> (Nat -> Nat -> Bool)
-> (Nat -> Nat -> Bool)
-> (Nat -> Nat -> Bool)
-> (Nat -> Nat -> Nat)
-> (Nat -> Nat -> Nat)
-> Ord Nat
Nat -> Nat -> Bool
Nat -> Nat -> Ordering
Nat -> Nat -> Nat
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Nat -> Nat -> Ordering
compare :: Nat -> Nat -> Ordering
$c< :: Nat -> Nat -> Bool
< :: Nat -> Nat -> Bool
$c<= :: Nat -> Nat -> Bool
<= :: Nat -> Nat -> Bool
$c> :: Nat -> Nat -> Bool
> :: Nat -> Nat -> Bool
$c>= :: Nat -> Nat -> Bool
>= :: Nat -> Nat -> Bool
$cmax :: Nat -> Nat -> Nat
max :: Nat -> Nat -> Nat
$cmin :: Nat -> Nat -> Nat
min :: Nat -> Nat -> Nat
Ord,Int -> Nat -> ShowS
[Nat] -> ShowS
Nat -> String
(Int -> Nat -> ShowS)
-> (Nat -> String) -> ([Nat] -> ShowS) -> Show Nat
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Nat -> ShowS
showsPrec :: Int -> Nat -> ShowS
$cshow :: Nat -> String
show :: Nat -> String
$cshowList :: [Nat] -> ShowS
showList :: [Nat] -> ShowS
Show)

data (≟) (a ∷ k) (b ∷ k) ∷ ★ where
  Refl ∷ ∀ (k ∷ ★) (a ∷ k). a ≟ a

data P (a ∷ k) = P
  deriving (P a -> P a -> Bool
(P a -> P a -> Bool) -> (P a -> P a -> Bool) -> Eq (P a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (a :: k). P a -> P a -> Bool
$c== :: forall k (a :: k). P a -> P a -> Bool
== :: P a -> P a -> Bool
$c/= :: forall k (a :: k). P a -> P a -> Bool
/= :: P a -> P a -> Bool
Eq,Eq (P a)
Eq (P a) =>
(P a -> P a -> Ordering)
-> (P a -> P a -> Bool)
-> (P a -> P a -> Bool)
-> (P a -> P a -> Bool)
-> (P a -> P a -> Bool)
-> (P a -> P a -> P a)
-> (P a -> P a -> P a)
-> Ord (P a)
P a -> P a -> Bool
P a -> P a -> Ordering
P a -> P a -> P a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall k (a :: k). Eq (P a)
forall k (a :: k). P a -> P a -> Bool
forall k (a :: k). P a -> P a -> Ordering
forall k (a :: k). P a -> P a -> P a
$ccompare :: forall k (a :: k). P a -> P a -> Ordering
compare :: P a -> P a -> Ordering
$c< :: forall k (a :: k). P a -> P a -> Bool
< :: P a -> P a -> Bool
$c<= :: forall k (a :: k). P a -> P a -> Bool
<= :: P a -> P a -> Bool
$c> :: forall k (a :: k). P a -> P a -> Bool
> :: P a -> P a -> Bool
$c>= :: forall k (a :: k). P a -> P a -> Bool
>= :: P a -> P a -> Bool
$cmax :: forall k (a :: k). P a -> P a -> P a
max :: P a -> P a -> P a
$cmin :: forall k (a :: k). P a -> P a -> P a
min :: P a -> P a -> P a
Ord,Int -> P a -> ShowS
[P a] -> ShowS
P a -> String
(Int -> P a -> ShowS)
-> (P a -> String) -> ([P a] -> ShowS) -> Show (P a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (a :: k). Int -> P a -> ShowS
forall k (a :: k). [P a] -> ShowS
forall k (a :: k). P a -> String
$cshowsPrec :: forall k (a :: k). Int -> P a -> ShowS
showsPrec :: Int -> P a -> ShowS
$cshow :: forall k (a :: k). P a -> String
show :: P a -> String
$cshowList :: forall k (a :: k). [P a] -> ShowS
showList :: [P a] -> ShowS
Show)

-- Wrap a constraint in a value
data W (c ∷ Constraint) where W ∷ (c) ⇒ W c

coerce_UNSAFE ∷ a → b
coerce_UNSAFE :: forall a b. a -> b
coerce_UNSAFE = a -> b
forall a b. a -> b
HS.unsafeCoerce

weq_UNSAFE ∷ P a → P b → W (a ~ b)
weq_UNSAFE :: forall {k} (a :: k) (b :: k). P a -> P b -> W (a ~ b)
weq_UNSAFE P a
P P b
P = W (() ~ ()) -> W (a ~ b)
forall a b. a -> b
coerce_UNSAFE (W (() ~ ()) -> W (a ~ b)) -> W (() ~ ()) -> W (a ~ b)
forall a b. (a -> b) -> a -> b
$ forall (c :: Constraint). c => W c
W @(() ~ ())

void_UNSAFE ∷ Void
void_UNSAFE :: Void
void_UNSAFE = () -> Void
forall a b. a -> b
coerce_UNSAFE ()

deriving instance Eq (W c)
deriving instance Ord (W c)
deriving instance Show (W c)

with ∷ W c → ((c) ⇒ a) → a
with :: forall (c :: Constraint) a. W c -> (c => a) -> a
with W c
W c => a
x = a
c => a
x

-- Existentially quantified type
data Ex (t ∷ k → ★) ∷ ★ where
  Ex ∷ ∀ (k ∷ ★) (t ∷ k → ★) (a ∷ k). t a → Ex t

deriving instance (∀ a. Show (t a)) ⇒ Show (Ex t)

unpack ∷ ∀ (k ∷ ★) (t ∷ k → ★) (b ∷ ★). Ex t → (∀ (a ∷ k). t a → b) → b
unpack :: forall k (t :: k -> *) b. Ex t -> (forall (a :: k). t a -> b) -> b
unpack (Ex t a
x) forall (a :: k). t a -> b
f = t a -> b
forall (a :: k). t a -> b
f t a
x

-- Constrained existentially quantified type with
data Ex_C (c ∷ k → Constraint) (t ∷ k → ★) ∷ ★ where
  Ex_C ∷ ∀ (k ∷ ★) (c ∷ k → Constraint) (t ∷ k → ★) (a ∷ k). (c a) ⇒ t a → Ex_C c t

deriving instance (∀ a. c a ⇒ Show (t a)) ⇒ Show (Ex_C c t)

unpack_C ∷ ∀ (k ∷ ★) (c ∷ k → Constraint) (t ∷ k → ★) (b ∷ ★). Ex_C c t → (∀ (a ∷ k). (c a) ⇒ t a → b) → b
unpack_C :: forall k (c :: k -> Constraint) (t :: k -> *) b.
Ex_C c t -> (forall (a :: k). c a => t a -> b) -> b
unpack_C (Ex_C t a
x) forall (a :: k). c a => t a -> b
f = t a -> b
forall (a :: k). c a => t a -> b
f t a
x

--------------------
-- Haskell Syntax --
--------------------

-- fromString ∷ [ℂ] → 𝕊
-- fromString = Text.pack

-- fromInteger ∷ ℤ → ℕ
-- fromInteger = HS.fromIntegral

negate ∷ ℕ → ℤ
negate :: ℕ -> ℤ
negate ℕ
n = ℤ -> ℤ
forall a. Num a => a -> a
HS.negate (ℕ -> ℤ
forall a b. (Integral a, Num b) => a -> b
HS.fromIntegral ℕ
n)

fromRational ∷ HS.Rational → 𝔻
fromRational :: ℚ -> 𝔻
fromRational = ℚ -> 𝔻
forall a. Fractional a => ℚ -> a
HS.fromRational

fail ∷ ∀ (r ∷ HS.RuntimeRep) (a ∷ HS.TYPE r) m. (STACK) ⇒ [ℂ] → m a
fail :: forall a (m :: * -> *). STACK => String -> m a
fail = String -> m a
forall a. STACK => String -> a
HS.error

ifThenElse ∷ 𝔹 → a → a → a
ifThenElse :: forall a. Bool -> a -> a -> a
ifThenElse = Bool -> a -> a -> a
forall a. Bool -> a -> a -> a
cond

-----------------------
-- Basic Conversions --
-----------------------

𝕤 ∷ [ℂ] → 𝕊
𝕤 :: String -> 𝕊
𝕤 = String -> 𝕊
Text.pack

𝕟 ∷ ℕ → ℕ
𝕟 :: ℕ -> ℕ
𝕟 = ℕ -> ℕ
forall a. a -> a
id

𝕟64 ∷ ℕ → ℕ64
𝕟64 :: ℕ -> ℕ64
𝕟64 = ℕ -> ℕ64
forall a b. (Integral a, Num b) => a -> b
HS.fromIntegral

𝕟32 ∷ ℕ → ℕ32
𝕟32 :: ℕ -> ℕ32
𝕟32 = ℕ -> ℕ32
forall a b. (Integral a, Num b) => a -> b
HS.fromIntegral

𝕟16 ∷ ℕ → ℕ16
𝕟16 :: ℕ -> ℕ16
𝕟16 = ℕ -> ℕ16
forall a b. (Integral a, Num b) => a -> b
HS.fromIntegral

𝕟8 ∷ ℕ → ℕ8
𝕟8 :: ℕ -> ℕ8
𝕟8 = ℕ -> ℕ8
forall a b. (Integral a, Num b) => a -> b
HS.fromIntegral

𝕫 ∷ ℕ → ℤ
𝕫 :: ℕ -> ℤ
𝕫 = ℕ -> ℤ
forall a b. (Integral a, Num b) => a -> b
HS.fromIntegral

𝕫64 ∷ ℕ → ℤ64
𝕫64 :: ℕ -> ℤ64
𝕫64 = ℕ -> ℤ64
forall a b. (Integral a, Num b) => a -> b
HS.fromIntegral

𝕫32 ∷ ℕ → ℤ32
𝕫32 :: ℕ -> ℤ32
𝕫32 = ℕ -> ℤ32
forall a b. (Integral a, Num b) => a -> b
HS.fromIntegral

𝕫16 ∷ ℕ → ℤ16
𝕫16 :: ℕ -> ℤ16
𝕫16 = ℕ -> ℤ16
forall a b. (Integral a, Num b) => a -> b
HS.fromIntegral

𝕫8 ∷ ℕ → ℤ8
𝕫8 :: ℕ -> ℤ8
𝕫8 = ℕ -> ℤ8
forall a b. (Integral a, Num b) => a -> b
HS.fromIntegral

𝕢 ∷ ℕ → ℚ
𝕢 :: ℕ -> ℚ
𝕢 = ℕ -> ℚ
forall a b. (Integral a, Num b) => a -> b
HS.fromIntegral

𝕢ᴾ ∷ ℕ → ℚᴾ
𝕢ᴾ :: ℕ -> ℚᴾ
𝕢ᴾ = ℕ -> ℚᴾ
forall a b. (Integral a, Num b) => a -> b
HS.fromIntegral

𝕕ᴾ ∷ 𝔻 → 𝔻ᴾ
𝕕ᴾ :: 𝔻 -> 𝔻ᴾ
𝕕ᴾ = 𝔻 -> 𝔻ᴾ
𝔻ᴾ

tohsChars ∷ 𝕊 → [ℂ]
tohsChars :: 𝕊 -> String
tohsChars = 𝕊 -> String
Text.unpack

frhsChars ∷ [ℂ] → 𝕊
frhsChars :: String -> 𝕊
frhsChars = String -> 𝕊
Text.pack

---------------------
-- Call Stack Type --
---------------------

type STACK = HS.HasCallStack

error ∷ ∀ (r ∷ HS.RuntimeRep) (a ∷ HS.TYPE r). (STACK) ⇒ 𝕊 → a
error :: forall a. STACK => 𝕊 -> a
error 𝕊
s = String -> a
forall a. STACK => String -> a
HS.error (𝕊 -> String
tohsChars 𝕊
s)

------------------------------
-- Basic Function Functions --
------------------------------

($) ∷ ∀ r a (b ∷ HS.TYPE r). (a → b) → a → b
a -> b
f $ :: forall a b. (a -> b) -> a -> b
$ a
x = a -> b
f a
x

id ∷ a → a
id :: forall a. a -> a
id = \ a
x → a
x

appto ∷ a → (a → b) → b
appto :: forall a b. a -> (a -> b) -> b
appto = \ a
x a -> b
f → a -> b
f a
x

const ∷ a → b → a
const :: forall a b. a -> b -> a
const a
x = \ b
_ → a
x

(∘) ∷ (b → c) → (a → b) → a → c
b -> c
g ∘ :: forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> b
f = \ a
x → b -> c
g (a -> b
f a
x)

(∘∘) ∷ (c → d) → (a → b → c) → (a → b → d)
∘∘ :: forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
(∘∘) = ((b -> c) -> b -> d) -> (a -> b -> c) -> a -> b -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
(∘) (((b -> c) -> b -> d) -> (a -> b -> c) -> a -> b -> d)
-> ((c -> d) -> (b -> c) -> b -> d)
-> (c -> d)
-> (a -> b -> c)
-> a
-> b
-> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (c -> d) -> (b -> c) -> b -> d
forall b c a. (b -> c) -> (a -> b) -> a -> c
(∘)

(∘∘∘) ∷ (d → e) → (a → b → c → d) → a → b → c → e
∘∘∘ :: forall d e a b c.
(d -> e) -> (a -> b -> c -> d) -> a -> b -> c -> e
(∘∘∘) = ((c -> d) -> c -> e) -> (a -> b -> c -> d) -> a -> b -> c -> e
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
(∘∘) (((c -> d) -> c -> e) -> (a -> b -> c -> d) -> a -> b -> c -> e)
-> ((d -> e) -> (c -> d) -> c -> e)
-> (d -> e)
-> (a -> b -> c -> d)
-> a
-> b
-> c
-> e
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (d -> e) -> (c -> d) -> c -> e
forall b c a. (b -> c) -> (a -> b) -> a -> c
(∘)

flip ∷ (a → b → c) → (b → a → c)
flip :: forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> b -> c
f = \ b
y a
x → a -> b -> c
f a
x b
y

rotateR ∷ (a → b → c → d) → (c → a → b → d)
rotateR :: forall a b c d. (a -> b -> c -> d) -> c -> a -> b -> d
rotateR a -> b -> c -> d
f = \ c
c a
a b
b → a -> b -> c -> d
f a
a b
b c
c

rotateL ∷ (a → b → c → d) → (b → c → a → d)
rotateL :: forall a b c d. (a -> b -> c -> d) -> b -> c -> a -> d
rotateL a -> b -> c -> d
f = \ b
b c
c a
a → a -> b -> c -> d
f a
a b
b c
c

mirror ∷ (a → b → c → d) → (c → b → a → d)
mirror :: forall a b c d. (a -> b -> c -> d) -> c -> b -> a -> d
mirror a -> b -> c -> d
f = \ c
c b
b a
a → a -> b -> c -> d
f a
a b
b c
c

on ∷ (b → b → c) → (a → b) → (a → a → c)
on :: forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on b -> b -> c
p a -> b
f = \ a
x a
y → b -> b -> c
p (a -> b
f a
x) (a -> b
f a
y)

curry ∷ (a → b → c) → a ∧ b → c
curry :: forall a b c. (a -> b -> c) -> (a ∧ b) -> c
curry a -> b -> c
f (a
x :* b
y) = a -> b -> c
f a
x b
y

uncurry ∷ (a ∧ b → c) → a → b → c
uncurry :: forall a b c. ((a ∧ b) -> c) -> a -> b -> c
uncurry (a ∧ b) -> c
f a
x b
y = (a ∧ b) -> c
f (a
x a -> b -> a ∧ b
forall a b. a -> b -> a ∧ b
:* b
y)


-----------------------------------
-- Conversion to Vanilla Haskell --
-----------------------------------

tohs𝑂F ∷ (a → b) → 𝑂 a → HS.Maybe b
tohs𝑂F :: forall a b. (a -> b) -> 𝑂 a -> Maybe b
tohs𝑂F a -> b
f = \case
  𝑂 a
None → Maybe b
forall a. Maybe a
HS.Nothing
  Some a
x → b -> Maybe b
forall a. a -> Maybe a
HS.Just (b -> Maybe b) -> b -> Maybe b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
x

tohs𝑂 ∷ 𝑂 a → HS.Maybe a
tohs𝑂 :: forall a. 𝑂 a -> Maybe a
tohs𝑂 = (a -> a) -> 𝑂 a -> Maybe a
forall a b. (a -> b) -> 𝑂 a -> Maybe b
tohs𝑂F a -> a
forall a. a -> a
id

frhs𝑂F ∷ (a → b) → HS.Maybe a → 𝑂 b
frhs𝑂F :: forall a b. (a -> b) -> Maybe a -> 𝑂 b
frhs𝑂F a -> b
f = \case
  Maybe a
HS.Nothing → 𝑂 b
forall a. 𝑂 a
None
  HS.Just a
x → b -> 𝑂 b
forall a. a -> 𝑂 a
Some (b -> 𝑂 b) -> b -> 𝑂 b
forall a b. (a -> b) -> a -> b
$ a -> b
f a
x

frhs𝑂 ∷ HS.Maybe a → 𝑂 a
frhs𝑂 :: forall a. Maybe a -> 𝑂 a
frhs𝑂 = (a -> a) -> Maybe a -> 𝑂 a
forall a b. (a -> b) -> Maybe a -> 𝑂 b
frhs𝑂F a -> a
forall a. a -> a
id

class CHS a b | b → a where
  tohs ∷ a → b
  frhs ∷ b → a

instance {-# OVERLAPPABLE #-} (a ~ b) ⇒ CHS a b where 
  tohs :: a -> b
tohs = a -> a
a -> b
forall a. a -> a
id
  frhs :: b -> a
frhs = b -> a
b -> b
forall a. a -> a
id
instance {-# OVERLAPPING #-} CHS ℤ64 HS.Int where
  tohs :: ℤ64 -> Int
tohs = ℤ64 -> Int
forall a b. (Integral a, Num b) => a -> b
HS.fromIntegral
  frhs :: Int -> ℤ64
frhs = Int -> ℤ64
forall a b. (Integral a, Num b) => a -> b
HS.fromIntegral
instance {-# OVERLAPPING #-} (CHS a b) ⇒ CHS (𝐿 a) [b] where
  tohs :: 𝐿 a -> [b]
tohs = 𝐼 b -> [b]
forall a. 𝐼 a -> [a]
lazyList𝐼 (𝐼 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
map𝐼 a -> b
forall a b. CHS a b => a -> b
tohs (𝐼 a -> [b]) -> (𝐿 a -> 𝐼 a) -> 𝐿 a -> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐿 a -> 𝐼 a
forall a. 𝐿 a -> 𝐼 a
iter𝐿
  frhs :: [b] -> 𝐿 a
frhs = 𝐼 a -> 𝐿 a
forall a. 𝐼 a -> 𝐿 a
list𝐼 (𝐼 a -> 𝐿 a) -> (𝐼 b -> 𝐼 a) -> 𝐼 b -> 𝐿 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (b -> a) -> 𝐼 b -> 𝐼 a
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
map𝐼 b -> a
forall a b. CHS a b => b -> a
frhs (𝐼 b -> 𝐿 a) -> ([b] -> 𝐼 b) -> [b] -> 𝐿 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ [b] -> 𝐼 b
forall a. [a] -> 𝐼 a
iterLL
instance {-# OVERLAPPING #-} (CHS a₁ b₁,CHS a₂ b₂) ⇒ CHS (a₁ ∧ a₂) (b₁,b₂) where
  tohs :: (a₁ ∧ a₂) -> (b₁, b₂)
tohs (a₁
x :* a₂
y) = (a₁ -> b₁
forall a b. CHS a b => a -> b
tohs a₁
x,a₂ -> b₂
forall a b. CHS a b => a -> b
tohs a₂
y)
  frhs :: (b₁, b₂) -> a₁ ∧ a₂
frhs (b₁
x,b₂
y) = b₁ -> a₁
forall a b. CHS a b => b -> a
frhs b₁
x a₁ -> a₂ -> a₁ ∧ a₂
forall a b. a -> b -> a ∧ b
:* b₂ -> a₂
forall a b. CHS a b => b -> a
frhs b₂
y
instance {-# OVERLAPPING #-} (CHS a₁ b₁,CHS a₂ b₂,CHS a₃ b₃) ⇒ CHS (a₁ ∧ a₂ ∧ a₃) (b₁,b₂,b₃) where
  tohs :: ((a₁ ∧ a₂) ∧ a₃) -> (b₁, b₂, b₃)
tohs (a₁
x :* a₂
y :* a₃
z) = (a₁ -> b₁
forall a b. CHS a b => a -> b
tohs a₁
x,a₂ -> b₂
forall a b. CHS a b => a -> b
tohs a₂
y,a₃ -> b₃
forall a b. CHS a b => a -> b
tohs a₃
z)
  frhs :: (b₁, b₂, b₃) -> (a₁ ∧ a₂) ∧ a₃
frhs (b₁
x,b₂
y,b₃
z) = b₁ -> a₁
forall a b. CHS a b => b -> a
frhs b₁
x a₁ -> a₂ -> a₁ ∧ a₂
forall a b. a -> b -> a ∧ b
:* b₂ -> a₂
forall a b. CHS a b => b -> a
frhs b₂
y (a₁ ∧ a₂) -> a₃ -> (a₁ ∧ a₂) ∧ a₃
forall a b. a -> b -> a ∧ b
:* b₃ -> a₃
forall a b. CHS a b => b -> a
frhs b₃
z
instance {-# OVERLAPPING #-} (CHS a₁ b₁,CHS a₂ b₂,CHS a₃ b₃,CHS a₄ b₄) ⇒ CHS (a₁ ∧ a₂ ∧ a₃ ∧ a₄) (b₁,b₂,b₃,b₄) where
  tohs :: (((a₁ ∧ a₂) ∧ a₃) ∧ a₄) -> (b₁, b₂, b₃, b₄)
tohs (a₁
w :* a₂
x :* a₃
y :* a₄
z) = (a₁ -> b₁
forall a b. CHS a b => a -> b
tohs a₁
w,a₂ -> b₂
forall a b. CHS a b => a -> b
tohs a₂
x,a₃ -> b₃
forall a b. CHS a b => a -> b
tohs a₃
y,a₄ -> b₄
forall a b. CHS a b => a -> b
tohs a₄
z)
  frhs :: (b₁, b₂, b₃, b₄) -> ((a₁ ∧ a₂) ∧ a₃) ∧ a₄
frhs (b₁
w,b₂
x,b₃
y,b₄
z) = b₁ -> a₁
forall a b. CHS a b => b -> a
frhs b₁
w a₁ -> a₂ -> a₁ ∧ a₂
forall a b. a -> b -> a ∧ b
:* b₂ -> a₂
forall a b. CHS a b => b -> a
frhs b₂
x (a₁ ∧ a₂) -> a₃ -> (a₁ ∧ a₂) ∧ a₃
forall a b. a -> b -> a ∧ b
:* b₃ -> a₃
forall a b. CHS a b => b -> a
frhs b₃
y ((a₁ ∧ a₂) ∧ a₃) -> a₄ -> ((a₁ ∧ a₂) ∧ a₃) ∧ a₄
forall a b. a -> b -> a ∧ b
:* b₄ -> a₄
forall a b. CHS a b => b -> a
frhs b₄
z
instance {-# OVERLAPPING #-} (CHS a₁ b₁,CHS a₂ b₂) ⇒ CHS (a₁ ∨ a₂) (HS.Either b₁ b₂) where
  tohs :: (a₁ ∨ a₂) -> Either b₁ b₂
tohs = \case
    Inl a₁
x → b₁ -> Either b₁ b₂
forall a b. a -> Either a b
HS.Left (b₁ -> Either b₁ b₂) -> b₁ -> Either b₁ b₂
forall a b. (a -> b) -> a -> b
$ a₁ -> b₁
forall a b. CHS a b => a -> b
tohs a₁
x
    Inr a₂
y → b₂ -> Either b₁ b₂
forall a b. b -> Either a b
HS.Right (b₂ -> Either b₁ b₂) -> b₂ -> Either b₁ b₂
forall a b. (a -> b) -> a -> b
$ a₂ -> b₂
forall a b. CHS a b => a -> b
tohs a₂
y
  frhs :: Either b₁ b₂ -> a₁ ∨ a₂
frhs = \case
    HS.Left b₁
x → a₁ -> a₁ ∨ a₂
forall a b. a -> a ∨ b
Inl (a₁ -> a₁ ∨ a₂) -> a₁ -> a₁ ∨ a₂
forall a b. (a -> b) -> a -> b
$ b₁ -> a₁
forall a b. CHS a b => b -> a
frhs b₁
x
    HS.Right b₂
y → a₂ -> a₁ ∨ a₂
forall a b. b -> a ∨ b
Inr (a₂ -> a₁ ∨ a₂) -> a₂ -> a₁ ∨ a₂
forall a b. (a -> b) -> a -> b
$ b₂ -> a₂
forall a b. CHS a b => b -> a
frhs b₂
y
instance {-# OVERLAPPING #-} (CHS a b) ⇒ CHS (𝑂 a) (HS.Maybe b) where
  tohs :: 𝑂 a -> Maybe b
tohs = (a -> b) -> 𝑂 a -> Maybe b
forall a b. (a -> b) -> 𝑂 a -> Maybe b
tohs𝑂F a -> b
forall a b. CHS a b => a -> b
tohs
  frhs :: Maybe b -> 𝑂 a
frhs = (b -> a) -> Maybe b -> 𝑂 a
forall a b. (a -> b) -> Maybe a -> 𝑂 b
frhs𝑂F b -> a
forall a b. CHS a b => b -> a
frhs