module UVMHS.Core.Static where

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

import qualified Prelude as HS
import qualified Data.Proxy as HS
import qualified Data.Type.Equality as HS

import qualified GHC.TypeLits as HS

infix 4 ≍,≺,≼,≻,<,≤

-- type literals: nat and string --

type family (a ∷ k) ≡ (b ∷ k) where
  a ≡ a = 'True
  _ ≡ _ = 'False

type family (x ∷ 𝔹) ⩔ (y ∷ 𝔹) where
  'False ⩔ x = x
  x ⩔ 'False = x
  'True ⩔ 'True = 'True

type family (x ∷ 𝔹) ⩓ (y ∷ 𝔹) where
  'True ⩓ x = x
  x ⩓ 'True = x
  'False ⩓ 'False = 'False

type 𝐍 = HS.Nat
type 𝐒 = HS.Symbol

type (m ∷ 𝐍) + (n ∷ 𝐍) = m HS.+ n
type (m ∷ 𝐍) × (n ∷ 𝐍) = m HS.* n
type (m ∷ 𝐍) ^ (n ∷ 𝐍) = m HS.^ n
type (m ∷ 𝐍) - (n ∷ 𝐍) = m HS.- n
type (m ∷ 𝐍) / (n ∷ 𝐍) = m `HS.Div` n
type (m ∷ 𝐍) % (n ∷ 𝐍) = m `HS.Mod` n
type Log2 (n ∷ 𝐍) = HS.Log2 n

type (m ∷ 𝐍) ⋚ (n ∷ 𝐍) = HS.CmpNat m n

type (m ∷ 𝐍) ≺  (n ∷ 𝐍) = (m ⋚ n) ≡ 'LT ~ 'True
type (m ∷ 𝐍) ≍  (n ∷ 𝐍) = (m ⋚ n) ≡ 'EQ ~ 'True
type (m ∷ 𝐍) ≻  (n ∷ 𝐍) = (m ⋚ n) ≡ 'GT ~ 'True

type (m ∷ 𝐍) ≼ (n ∷ 𝐍) = ((m ⋚ n) ≡ 'LT) ⩔ ((m ⋚ n ≡ 'EQ)) ~ 'True

wnlt_UNSAFE ∷ ∀ m n. P m → P n → W (m ≺ n)
wnlt_UNSAFE :: forall (m :: 𝐍) (n :: 𝐍). P m -> P n -> W (m ≺ n)
wnlt_UNSAFE P m
_ P n
_ = forall (a :: Bool) (b :: Bool). P a -> P b -> W (a ~ b)
forall {k} (a :: k) (b :: k). P a -> P b -> W (a ~ b)
weq_UNSAFE @(m ⋚ n ≡ 'LT) @'True P ((m ⋚ n) ≡ 'LT)
forall k (a :: k). P a
P P 'True
forall k (a :: k). P a
P

wneq_UNSAFE ∷ ∀ m n. P m → P n → W (m ≍ n)
wneq_UNSAFE :: forall (m :: 𝐍) (n :: 𝐍). P m -> P n -> W (m ≍ n)
wneq_UNSAFE P m
_ P n
_ = forall (a :: Bool) (b :: Bool). P a -> P b -> W (a ~ b)
forall {k} (a :: k) (b :: k). P a -> P b -> W (a ~ b)
weq_UNSAFE @(m ⋚ n ≡ 'EQ) @'True P ((m ⋚ n) ≡ 'EQ)
forall k (a :: k). P a
P P 'True
forall k (a :: k). P a
P

wngt_UNSAFE ∷ ∀ m n. P m → P n → W (m ≻ n)
wngt_UNSAFE :: forall (m :: 𝐍) (n :: 𝐍). P m -> P n -> W (m ≻ n)
wngt_UNSAFE P m
_ P n
_ = forall (a :: Bool) (b :: Bool). P a -> P b -> W (a ~ b)
forall {k} (a :: k) (b :: k). P a -> P b -> W (a ~ b)
weq_UNSAFE @(m ⋚ n ≡ 'GT) @'True P ((m ⋚ n) ≡ 'GT)
forall k (a :: k). P a
P P 'True
forall k (a :: k). P a
P

wnlte_UNSAFE ∷ ∀ m n. P m → P n → W (m ≼ n)
wnlte_UNSAFE :: forall (m :: 𝐍) (n :: 𝐍). P m -> P n -> W (m ≼ n)
wnlte_UNSAFE P m
_ P n
_ = forall (a :: Bool) (b :: Bool). P a -> P b -> W (a ~ b)
forall {k} (a :: k) (b :: k). P a -> P b -> W (a ~ b)
weq_UNSAFE @((m ⋚ n ≡ 'LT) ⩔ (m ⋚ n ≡ 'EQ)) @'True P (((m ⋚ n) ≡ 'LT) ⩔ ((m ⋚ n) ≡ 'EQ))
forall k (a :: k). P a
P P 'True
forall k (a :: k). P a
P 

data (m ∷ 𝐍) < (n ∷ 𝐍) where
  W_LT ∷ (m ≺ n) ⇒ m < n

withLT ∷ m < n → ((m ≺ n) ⇒ a) → a
withLT :: forall (m :: 𝐍) (n :: 𝐍) a. (m < n) -> ((m ≺ n) => a) -> a
withLT m < n
W_LT (m ≺ n) => a
x = a
(m ≺ n) => a
x

nlt_UNSAFE ∷ ∀ m n. P m → P n → m < n
nlt_UNSAFE :: forall (m :: 𝐍) (n :: 𝐍). P m -> P n -> m < n
nlt_UNSAFE P m
_ P n
_ = W (m ≺ n) -> ((m ≺ n) => m < n) -> m < n
forall (c :: Constraint) a. W c -> (c => a) -> a
with (forall (m :: 𝐍) (n :: 𝐍). P m -> P n -> W (m ≺ n)
wnlt_UNSAFE @m @n P m
forall k (a :: k). P a
P P n
forall k (a :: k). P a
P) m < n
(m ≺ n) => m < n
forall (m :: 𝐍) (n :: 𝐍). (m ≺ n) => m < n
W_LT

instance Transitive (<) where
  b < c
_ ⊚ :: forall (b :: 𝐍) (c :: 𝐍) (a :: 𝐍). (b < c) -> (a < b) -> a < c
⊚ a < b
_ = P a -> P c -> a < c
forall (m :: 𝐍) (n :: 𝐍). P m -> P n -> m < n
nlt_UNSAFE P a
forall k (a :: k). P a
P P c
forall k (a :: k). P a
P

data (m ∷ 𝐍) ≤ (n ∷ 𝐍) where
  W_LTE ∷ (m ≼ n) ⇒ m ≤ n

withLTE ∷ m ≤ n → ((m ≼ n) ⇒ a) → a
withLTE :: forall (m :: 𝐍) (n :: 𝐍) a. (m ≤ n) -> ((m ≼ n) => a) -> a
withLTE m ≤ n
W_LTE (m ≼ n) => a
x = a
(m ≼ n) => a
x

nlte_UNSAFE ∷ ∀ m n. P m → P n → m ≤ n
nlte_UNSAFE :: forall (m :: 𝐍) (n :: 𝐍). P m -> P n -> m ≤ n
nlte_UNSAFE P m
_ P n
_ = W (m ≼ n) -> ((m ≼ n) => m ≤ n) -> m ≤ n
forall (c :: Constraint) a. W c -> (c => a) -> a
with (forall (m :: 𝐍) (n :: 𝐍). P m -> P n -> W (m ≼ n)
wnlte_UNSAFE @m @n P m
forall k (a :: k). P a
P P n
forall k (a :: k). P a
P) m ≤ n
(m ≼ n) => m ≤ n
forall (m :: 𝐍) (n :: 𝐍). (m ≼ n) => m ≤ n
W_LTE

instance Reflexive (≤) where
  refl :: forall (a :: 𝐍). a ≤ a
refl = a ≤ a
forall (m :: 𝐍) (n :: 𝐍). (m ≼ n) => m ≤ n
W_LTE
instance Transitive (≤) where
  b ≤ c
_ ⊚ :: forall (b :: 𝐍) (c :: 𝐍) (a :: 𝐍). (b ≤ c) -> (a ≤ b) -> a ≤ c
⊚ a ≤ b
_ = P a -> P c -> a ≤ c
forall (m :: 𝐍) (n :: 𝐍). P m -> P n -> m ≤ n
nlte_UNSAFE P a
forall k (a :: k). P a
P P c
forall k (a :: k). P a
P
instance Category (≤)

irreflLT ∷ n < n → Void
irreflLT :: forall (n :: 𝐍). (n < n) -> Void
irreflLT n < n
_ = Void
void_UNSAFE

weakenLT ∷ n₁ < n₂ → n₁ ≤ n₂
weakenLT :: forall (n₁ :: 𝐍) (n₂ :: 𝐍). (n₁ < n₂) -> n₁ ≤ n₂
weakenLT n₁ < n₂
_ = P n₁ -> P n₂ -> n₁ ≤ n₂
forall (m :: 𝐍) (n :: 𝐍). P m -> P n -> m ≤ n
nlte_UNSAFE P n₁
forall k (a :: k). P a
P P n₂
forall k (a :: k). P a
P

succLT ∷ n₁ < n₂ → n₁+1 ≤ n₂
succLT :: forall (n₁ :: 𝐍) (n₂ :: 𝐍). (n₁ < n₂) -> (n₁ + 1) ≤ n₂
succLT n₁ < n₂
_ = P (n₁ + 1) -> P n₂ -> (n₁ + 1) ≤ n₂
forall (m :: 𝐍) (n :: 𝐍). P m -> P n -> m ≤ n
nlte_UNSAFE P (n₁ + 1)
forall k (a :: k). P a
P P n₂
forall k (a :: k). P a
P

succLTE ∷ n₁ ≤ n₂ → n₁ < n₂+1
succLTE :: forall (n₁ :: 𝐍) (n₂ :: 𝐍). (n₁ ≤ n₂) -> n₁ < (n₂ + 1)
succLTE n₁ ≤ n₂
_ = P n₁ -> P (n₂ + 1) -> n₁ < (n₂ + 1)
forall (m :: 𝐍) (n :: 𝐍). P m -> P n -> m < n
nlt_UNSAFE P n₁
forall k (a :: k). P a
P P (n₂ + 1)
forall k (a :: k). P a
P

(⊚♯) ∷ n₁ ≤ n₂ → n₂ < n₃ → n₁ < n₃
n₁ ≤ n₂
_ ⊚♯ :: forall (n₁ :: 𝐍) (n₂ :: 𝐍) (n₃ :: 𝐍).
(n₁ ≤ n₂) -> (n₂ < n₃) -> n₁ < n₃
⊚♯ n₂ < n₃
_ = P n₁ -> P n₃ -> n₁ < n₃
forall (m :: 𝐍) (n :: 𝐍). P m -> P n -> m < n
nlt_UNSAFE P n₁
forall k (a :: k). P a
P P n₃
forall k (a :: k). P a
P

(♯⊚) ∷ n₁ < n₂ → n₂ ≤ n₃ → n₁ < n₃
n₁ < n₂
_ ♯⊚ :: forall (n₁ :: 𝐍) (n₂ :: 𝐍) (n₃ :: 𝐍).
(n₁ < n₂) -> (n₂ ≤ n₃) -> n₁ < n₃
♯⊚ n₂ ≤ n₃
_ = P n₁ -> P n₃ -> n₁ < n₃
forall (m :: 𝐍) (n :: 𝐍). P m -> P n -> m < n
nlt_UNSAFE P n₁
forall k (a :: k). P a
P P n₃
forall k (a :: k). P a
P

-- singleton literals: nat, nat64 and string --

newtype ℕS   (n ∷ 𝐍) = ℕS_UNSAFE   { forall (n :: 𝐍). ℕS n -> 𝐍
unℕS   ∷ ℕ   }
newtype ℕ64S (n ∷ 𝐍) = ℕ64S_UNSAFE { forall (n :: 𝐍). ℕ64S n -> ℕ64
unℕ64S ∷ ℕ64 }
newtype 𝕊S   (s ∷ 𝐒) = 𝕊S_UNSAFE   { forall (s :: 𝐒). 𝕊S s -> 𝕊
un𝕊S   ∷ 𝕊   }

class (HS.KnownNat n)    ⇒ 𝒩   (n ∷ 𝐍) where reifyℕ   ∷ P n → ℕ
class (HS.KnownNat n)    ⇒ 𝒩64 (n ∷ 𝐍) where reifyℕ64 ∷ P n → ℕ64
class (HS.KnownSymbol s) ⇒ 𝒮   (s ∷ 𝐒) where reify𝕊   ∷ P s → 𝕊

instance (HS.KnownNat n)    ⇒ 𝒩   (n ∷ 𝐍) where reifyℕ :: P n -> 𝐍
reifyℕ   P n
_ = Integer -> 𝐍
forall a. (ToNatO a, STACK) => a -> 𝐍
natΩ   (Integer -> 𝐍) -> Integer -> 𝐍
forall a b. (a -> b) -> a -> b
$ forall (n :: 𝐍) (proxy :: 𝐍 -> *). KnownNat n => proxy n -> Integer
HS.natVal    @n P n
forall k (a :: k). P a
P
instance (HS.KnownNat n)    ⇒ 𝒩64 (n ∷ 𝐍) where reifyℕ64 :: P n -> ℕ64
reifyℕ64 P n
_ = Integer -> ℕ64
forall a. (ToNatO64 a, STACK) => a -> ℕ64
natΩ64 (Integer -> ℕ64) -> Integer -> ℕ64
forall a b. (a -> b) -> a -> b
$ forall (n :: 𝐍) (proxy :: 𝐍 -> *). KnownNat n => proxy n -> Integer
HS.natVal    @n P n
forall k (a :: k). P a
P
instance (HS.KnownSymbol s) ⇒ 𝒮   (s ∷ 𝐒) where reify𝕊 :: P s -> 𝕊
reify𝕊   P s
_ = String -> 𝕊
forall t. ToIter ℂ t => t -> 𝕊
string (String -> 𝕊) -> String -> 𝕊
forall a b. (a -> b) -> a -> b
$ forall (n :: 𝐒) (proxy :: 𝐒 -> *).
KnownSymbol n =>
proxy n -> String
HS.symbolVal @s P s
forall k (a :: k). P a
P

compare𝐍 ∷ ∀ (a ∷ 𝐍) (b ∷ 𝐍). (𝒩 a,𝒩 b) ⇒ 𝑂 (a ≟ b)
compare𝐍 :: forall (a :: 𝐍) (b :: 𝐍). (𝒩 a, 𝒩 b) => 𝑂 (a ≟ b)
compare𝐍 = case Proxy a -> Proxy b -> Maybe (a :~: b)
forall (a :: 𝐍) (b :: 𝐍) (proxy1 :: 𝐍 -> *) (proxy2 :: 𝐍 -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> Maybe (a :~: b)
HS.sameNat (forall (t :: 𝐍). Proxy t
forall {k} (t :: k). Proxy t
HS.Proxy @a) (forall (t :: 𝐍). Proxy t
forall {k} (t :: k). Proxy t
HS.Proxy @b) of
  Maybe (a :~: b)
HS.Nothing → 𝑂 (a ≟ b)
forall a. 𝑂 a
None
  HS.Just a :~: b
HS.Refl → (a ≟ b) -> 𝑂 (a ≟ b)
forall a. a -> 𝑂 a
Some a ≟ a
a ≟ b
forall k (a :: k). a ≟ a
Refl

𝕟s ∷ ∀ n. (𝒩 n) ⇒ ℕS n
𝕟s :: forall (n :: 𝐍). 𝒩 n => ℕS n
𝕟s = 𝐍 -> ℕS n
forall (n :: 𝐍). 𝐍 -> ℕS n
ℕS_UNSAFE (𝐍 -> ℕS n) -> 𝐍 -> ℕS n
forall a b. (a -> b) -> a -> b
$ forall (n :: 𝐍). 𝒩 n => P n -> 𝐍
reifyℕ @n P n
forall k (a :: k). P a
P

𝕟d ∷ ℕ → (∀ n. (𝒩 n) ⇒ ℕS n → a) → a
𝕟d :: forall a. 𝐍 -> (forall (n :: 𝐍). 𝒩 n => ℕS n -> a) -> a
𝕟d 𝐍
n forall (n :: 𝐍). 𝒩 n => ℕS n -> a
f = case Integer -> Maybe SomeNat
HS.someNatVal (Integer -> Maybe SomeNat) -> Integer -> Maybe SomeNat
forall a b. (a -> b) -> a -> b
$ 𝐍 -> Integer
forall a. ToInt a => a -> Integer
int 𝐍
n of
  Maybe SomeNat
HS.Nothing → 𝕊 -> a
forall a. STACK => 𝕊 -> a
error 𝕊
"impossible"
  HS.Just (HS.SomeNat (Proxy n
HS.Proxy ∷ HS.Proxy n)) → forall (n :: 𝐍). 𝒩 n => ℕS n -> a
f @n (ℕS n -> a) -> ℕS n -> a
forall a b. (a -> b) -> a -> b
$ 𝐍 -> ℕS n
forall (n :: 𝐍). 𝐍 -> ℕS n
ℕS_UNSAFE 𝐍
n

𝕟64s ∷ ∀ n. (𝒩64 n) ⇒ ℕ64S n
𝕟64s :: forall (n :: 𝐍). 𝒩64 n => ℕ64S n
𝕟64s = ℕ64 -> ℕ64S n
forall (n :: 𝐍). ℕ64 -> ℕ64S n
ℕ64S_UNSAFE (ℕ64 -> ℕ64S n) -> ℕ64 -> ℕ64S n
forall a b. (a -> b) -> a -> b
$ forall (n :: 𝐍). 𝒩64 n => P n -> ℕ64
reifyℕ64 @n P n
forall k (a :: k). P a
P

𝕟64d ∷ ℕ64 → (∀ n. (𝒩64 n) ⇒ ℕ64S n → a) → a
𝕟64d :: forall a. ℕ64 -> (forall (n :: 𝐍). 𝒩64 n => ℕ64S n -> a) -> a
𝕟64d ℕ64
n forall (n :: 𝐍). 𝒩64 n => ℕ64S n -> a
f = case Integer -> Maybe SomeNat
HS.someNatVal (Integer -> Maybe SomeNat) -> Integer -> Maybe SomeNat
forall a b. (a -> b) -> a -> b
$ ℕ64 -> Integer
forall a. ToInt a => a -> Integer
int ℕ64
n of
  Maybe SomeNat
HS.Nothing → 𝕊 -> a
forall a. STACK => 𝕊 -> a
error 𝕊
"impossible"
  HS.Just (HS.SomeNat (Proxy n
HS.Proxy ∷ HS.Proxy n)) → forall (n :: 𝐍). 𝒩64 n => ℕ64S n -> a
f @n (ℕ64S n -> a) -> ℕ64S n -> a
forall a b. (a -> b) -> a -> b
$ ℕ64 -> ℕ64S n
forall (n :: 𝐍). ℕ64 -> ℕ64S n
ℕ64S_UNSAFE ℕ64
n

𝕤s ∷ ∀ s. (HS.KnownSymbol s) ⇒ 𝕊S s
𝕤s :: forall (s :: 𝐒). KnownSymbol s => 𝕊S s
𝕤s = 𝕊 -> 𝕊S s
forall (s :: 𝐒). 𝕊 -> 𝕊S s
𝕊S_UNSAFE (𝕊 -> 𝕊S s) -> 𝕊 -> 𝕊S s
forall a b. (a -> b) -> a -> b
$ forall (s :: 𝐒). 𝒮 s => P s -> 𝕊
reify𝕊 @s P s
forall k (a :: k). P a
P

𝕤sd ∷ 𝕊 → (∀ s. (𝒮 s) ⇒ 𝕊S s → a) → a
𝕤sd :: forall a. 𝕊 -> (forall (s :: 𝐒). 𝒮 s => 𝕊S s -> a) -> a
𝕤sd 𝕊
s forall (s :: 𝐒). 𝒮 s => 𝕊S s -> a
f = case String -> SomeSymbol
HS.someSymbolVal (String -> SomeSymbol) -> String -> SomeSymbol
forall a b. (a -> b) -> a -> b
$ 𝕊 -> String
tohsChars 𝕊
s of
  HS.SomeSymbol (Proxy n
HS.Proxy ∷ HS.Proxy s) → 𝕊S n -> a
forall (s :: 𝐒). 𝒮 s => 𝕊S s -> a
f (𝕊S n -> a) -> 𝕊S n -> a
forall a b. (a -> b) -> a -> b
$ forall (s :: 𝐒). 𝕊 -> 𝕊S s
𝕊S_UNSAFE @s 𝕊
s

-- heterogeneous lists --

-- infixr 8 :&&

type family (xs ∷ [a]) ⧺ (ys ∷ [a]) ∷ [a] where
  '[] ⧺ ys = ys
  (x ': xs) ⧺ ys = x ': (xs ⧺ ys)

type family Sum (ns ∷ [𝐍]) where
  Sum '[] = 0
  Sum (n ': ns) = n + Sum ns

type family Prod (ns ∷ [𝐍]) where
  Prod '[] = 1
  Prod (n ': ns) = n × Prod ns

-- data 𝐿S (is ∷ [i]) (c ∷ i → Constraint) (a ∷ i → ★) ∷ ★ where
--   NilS ∷ 𝐿S '[] c a
--   (:&&) ∷ (c x) ⇒ a x → 𝐿S xs c a → 𝐿S (x ': xs) c a
-- 
-- map𝐿S ∷ ∀ i (xs ∷ [i]) (c ∷ i → Constraint) (a ∷ i → ★) (b ∷ i → ★) . (∀ (x ∷ i). a x → b x) → 𝐿S xs c a → 𝐿S xs c b
-- map𝐿S f = \case
--   NilS → NilS
--   x :&& xs → f x :&& map𝐿S f xs
-- 
-- append𝐿S ∷ 𝐿S xs c a → 𝐿S ys c a → 𝐿S (xs ⧺ ys) c a
-- append𝐿S xs ys = case xs of
--   NilS → ys
--   x :&& xs' → x :&& append𝐿S xs' ys
-- 
-- iter𝐿S ∷ ∀ i (xs ∷ [i]) (c ∷ i → Constraint) (a ∷ i → ★) (b ∷ ★). (∀ (x ∷ i). (c x) ⇒ a x → b) → 𝐿S xs c a → 𝐼 b
-- iter𝐿S f = \case
--   NilS → null
--   x :&& xs → single (f x) ⧺ iter𝐿S f xs

type family AllC (c ∷ a → Constraint) (xs ∷ [a]) ∷ Constraint where
  AllC _ '[] = ()
  AllC c (x ': xs) = (c x,AllC c xs)

-- class (AllC c xs) ⇒ AllCC c xs
-- instance (AllC c xs) ⇒ AllCC c xs

-- instance (∀ x. (c x) ⇒ Plus (a x)) ⇒ Plus (𝐿S xs c a) where
--   NilS + NilS = NilS
--   x :&& xs + y :&& ys = (x + y) :&& (xs + ys)
-- 
-- instance (∀ x. (c x) ⇒ Times (a x)) ⇒ Times (𝐿S xs c a) where
--   NilS × NilS = NilS
--   x :&& xs × y :&& ys = (x × y) :&& (xs × ys)

data Spine ∷ [a] → ★ where
  NilSpine ∷ Spine '[]
  ConsSpine ∷ Spine xs → Spine (x ': xs)

class HasSpine xs where spine ∷ Spine xs

instance HasSpine '[] where spine :: Spine '[]
spine = Spine '[]
forall a. Spine '[]
NilSpine
instance (HasSpine xs) ⇒ HasSpine (x ': xs) where spine :: Spine (x : xs)
spine = Spine xs -> Spine (x : xs)
forall {a} (xs :: [a]) (x :: a). Spine xs -> Spine (x : xs)
ConsSpine Spine xs
forall {a} (xs :: [a]). HasSpine xs => Spine xs
spine

-- zero𝐿S ∷ (AllC c xs,∀ x. (c x) ⇒ Zero (a x)) ⇒ Spine xs → 𝐿S xs c a
-- zero𝐿S = \case
--   NilSpine → NilS
--   ConsSpine sp → zero :&& zero𝐿S sp
-- 
-- instance (HasSpine xs,AllC c xs,∀ x. (c x) ⇒ Zero (a x)) ⇒ Zero (𝐿S xs c a) where
--   zero = zero𝐿S spine
-- 
-- type family PrependMany (xs ∷ [a]) (xxs ∷ [[a]]) ∷ [[a]] where
--   PrependMany _ '[] = '[]
--   PrependMany xs (xs' ': xss) = (xs ⧺ xs') ': PrependMany xs xss

-- indices --

newtype 𝕀64 (n ∷ 𝐍) = 𝕀64_UNSAFE { forall (n :: 𝐍). 𝕀64 n -> ℕ64
un𝕀64 ∷ ℕ64 }

𝕚64 ∷ ∀ m n. (m ≺ n) ⇒ ℕ64S m → 𝕀64 n
𝕚64 :: forall (m :: 𝐍) (n :: 𝐍). (m ≺ n) => ℕ64S m -> 𝕀64 n
𝕚64 ℕ64S m
m = ℕ64 -> 𝕀64 n
forall (n :: 𝐍). ℕ64 -> 𝕀64 n
𝕀64_UNSAFE (ℕ64 -> 𝕀64 n) -> ℕ64 -> 𝕀64 n
forall a b. (a -> b) -> a -> b
$ ℕ64S m -> ℕ64
forall (n :: 𝐍). ℕ64S n -> ℕ64
unℕ64S ℕ64S m
m

𝕚64d ∷ ∀ n. (𝒩64 n) ⇒ ℕ64 → 𝑂 (𝕀64 n)
𝕚64d :: forall (n :: 𝐍). 𝒩64 n => ℕ64 -> 𝑂 (𝕀64 n)
𝕚64d ℕ64
m = 
  if ℕ64
m ℕ64 -> ℕ64 -> Bool
forall a. Ord a => a -> a -> Bool
< ℕ64S n -> ℕ64
forall (n :: 𝐍). ℕ64S n -> ℕ64
unℕ64S (forall (n :: 𝐍). 𝒩64 n => ℕ64S n
𝕟64s @n)
  then 𝕀64 n -> 𝑂 (𝕀64 n)
forall a. a -> 𝑂 a
Some (𝕀64 n -> 𝑂 (𝕀64 n)) -> 𝕀64 n -> 𝑂 (𝕀64 n)
forall a b. (a -> b) -> a -> b
$ ℕ64 -> 𝕀64 n
forall (n :: 𝐍). ℕ64 -> 𝕀64 n
𝕀64_UNSAFE ℕ64
m
  else 𝑂 (𝕀64 n)
forall a. 𝑂 a
None

𝕟64di ∷ ∀ n a. 𝕀64 n → (∀ m. (m ≺ n) ⇒ ℕ64S m → a) → a
𝕟64di :: forall (n :: 𝐍) a.
𝕀64 n -> (forall (m :: 𝐍). (m ≺ n) => ℕ64S m -> a) -> a
𝕟64di 𝕀64 n
i forall (m :: 𝐍). (m ≺ n) => ℕ64S m -> a
f = ℕ64 -> (forall {n :: 𝐍}. 𝒩64 n => ℕ64S n -> a) -> a
forall a. ℕ64 -> (forall (n :: 𝐍). 𝒩64 n => ℕ64S n -> a) -> a
𝕟64d (𝕀64 n -> ℕ64
forall (n :: 𝐍). 𝕀64 n -> ℕ64
un𝕀64 𝕀64 n
i) ((forall {n :: 𝐍}. 𝒩64 n => ℕ64S n -> a) -> a)
-> (forall {n :: 𝐍}. 𝒩64 n => ℕ64S n -> a) -> a
forall a b. (a -> b) -> a -> b
HS.$ \ (ℕ64S n
m ∷ ℕ64S m) → W (n ≺ n) -> ((n ≺ n) => a) -> a
forall (c :: Constraint) a. W c -> (c => a) -> a
with (forall (m :: 𝐍) (n :: 𝐍). P m -> P n -> W (m ≺ n)
wnlt_UNSAFE @m @n P n
forall k (a :: k). P a
P P n
forall k (a :: k). P a
P) (((n ≺ n) => a) -> a) -> ((n ≺ n) => a) -> a
forall a b. (a -> b) -> a -> b
HS.$ ℕ64S n -> a
forall (m :: 𝐍). (m ≺ n) => ℕ64S m -> a
f ℕ64S n
m

upto𝕀64 ∷ ∀ n. (𝒩64 n) ⇒ ℕ64S n → 𝐼S n (𝕀64 n)
upto𝕀64 :: forall (n :: 𝐍). 𝒩64 n => ℕ64S n -> 𝐼S n (𝕀64 n)
upto𝕀64 ℕ64S n
n = 𝐼 (𝕀64 n) -> 𝐼S n (𝕀64 n)
forall (n :: 𝐍) a. 𝐼 a -> 𝐼S n a
𝐼S_UNSAFE (𝐼 (𝕀64 n) -> 𝐼S n (𝕀64 n)) -> 𝐼 (𝕀64 n) -> 𝐼S n (𝕀64 n)
forall a b. (a -> b) -> a -> b
$ (ℕ64 -> 𝕀64 n) -> 𝐼 ℕ64 -> 𝐼 (𝕀64 n)
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ℕ64 -> 𝕀64 n
forall (n :: 𝐍). ℕ64 -> 𝕀64 n
𝕀64_UNSAFE (𝐼 ℕ64 -> 𝐼 (𝕀64 n)) -> 𝐼 ℕ64 -> 𝐼 (𝕀64 n)
forall a b. (a -> b) -> a -> b
$ ℕ64 -> 𝐼 ℕ64
forall n. (Eq n, Zero n, One n, Plus n) => n -> 𝐼 n
upto (ℕ64 -> 𝐼 ℕ64) -> ℕ64 -> 𝐼 ℕ64
forall a b. (a -> b) -> a -> b
$ ℕ64S n -> ℕ64
forall (n :: 𝐍). ℕ64S n -> ℕ64
unℕ64S ℕ64S n
n

wk𝕀64 ∷ (m ≼ n) ⇒ 𝕀64 m → 𝕀64 n
wk𝕀64 :: forall (m :: 𝐍) (n :: 𝐍). (m ≼ n) => 𝕀64 m -> 𝕀64 n
wk𝕀64 𝕀64 m
i = ℕ64 -> 𝕀64 n
forall (n :: 𝐍). ℕ64 -> 𝕀64 n
𝕀64_UNSAFE (ℕ64 -> 𝕀64 n) -> ℕ64 -> 𝕀64 n
forall a b. (a -> b) -> a -> b
$ 𝕀64 m -> ℕ64
forall (n :: 𝐍). 𝕀64 n -> ℕ64
un𝕀64 𝕀64 m
i

-- static iterators --

newtype 𝐼S (n ∷ 𝐍) a = 𝐼S_UNSAFE
  { forall (n :: 𝐍) a. 𝐼S n a -> 𝐼 a
un𝐼S ∷ 𝐼 a
  } deriving (Int -> 𝐼S n a -> ShowS
[𝐼S n a] -> ShowS
𝐼S n a -> String
(Int -> 𝐼S n a -> ShowS)
-> (𝐼S n a -> String) -> ([𝐼S n a] -> ShowS) -> Show (𝐼S n a)
forall (n :: 𝐍) a. Show a => Int -> 𝐼S n a -> ShowS
forall (n :: 𝐍) a. Show a => [𝐼S n a] -> ShowS
forall (n :: 𝐍) a. Show a => 𝐼S n a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (n :: 𝐍) a. Show a => Int -> 𝐼S n a -> ShowS
showsPrec :: Int -> 𝐼S n a -> ShowS
$cshow :: forall (n :: 𝐍) a. Show a => 𝐼S n a -> String
show :: 𝐼S n a -> String
$cshowList :: forall (n :: 𝐍) a. Show a => [𝐼S n a] -> ShowS
showList :: [𝐼S n a] -> ShowS
Show)

instance Functor (𝐼S n) where map :: forall a b. (a -> b) -> 𝐼S n a -> 𝐼S n b
map a -> b
f 𝐼S n a
xs = 𝐼 b -> 𝐼S n b
forall (n :: 𝐍) a. 𝐼 a -> 𝐼S n a
𝐼S_UNSAFE (𝐼 b -> 𝐼S n b) -> 𝐼 b -> 𝐼S n b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> 𝐼 a -> 𝐼 b
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> b
f (𝐼 a -> 𝐼 b) -> 𝐼 a -> 𝐼 b
forall a b. (a -> b) -> a -> b
$ 𝐼S n a -> 𝐼 a
forall (n :: 𝐍) a. 𝐼S n a -> 𝐼 a
un𝐼S 𝐼S n a
xs
instance ToIter a (𝐼S n a) where iter :: 𝐼S n a -> 𝐼 a
iter = 𝐼S n a -> 𝐼 a
forall (n :: 𝐍) a. 𝐼S n a -> 𝐼 a
un𝐼S

-- class ToIterS n a t | t → n,t → a where iterS ∷ t → 𝐼S n a

-- classes --

-- infixl 5 +♮
-- infixl 6 ×♮
-- 
-- class ZeroS  t where zeroS ∷ t 0
-- class OneS   t where oneS  ∷ t 1
-- class PlusS  t where (+♮)  ∷ t m → t n → t (m + n)
-- class TimesS t where (×♮)  ∷ t m → t n → t (m × n)
-- 
-- instance ZeroS  ℕ64S where zeroS  = 𝕟64s @0
-- instance OneS   ℕ64S where oneS   = 𝕟64s @1
-- instance PlusS  ℕ64S where m +♮ n = ℕ64S_UNSAFE $ unℕ64S m + unℕ64S n
-- instance TimesS ℕ64S where m ×♮ n = ℕ64S_UNSAFE $ unℕ64S m × unℕ64S n

class NullS t where 
  nullS ∷ t 0 a
class SingleS t where
  𝔢 ∷ a → t 1 a
class AppendS t where 
  (⧺♮) ∷ t n₁ a → t n₂ a → t (n₁ + n₂) a
-- class AppendSL t where
--   (⧺♭) ∷ t ns₁ a → t ns₂ a → t (ns₁ ⧺ ns₂) a

instance NullS 𝐼S where nullS :: forall a. 𝐼S 0 a
nullS = 𝐼 a -> 𝐼S 0 a
forall (n :: 𝐍) a. 𝐼 a -> 𝐼S n a
𝐼S_UNSAFE 𝐼 a
forall a. Null a => a
null
instance SingleS 𝐼S where 𝔢 :: forall a. a -> 𝐼S 1 a
𝔢 = 𝐼 a -> 𝐼S 1 a
forall (n :: 𝐍) a. 𝐼 a -> 𝐼S n a
𝐼S_UNSAFE (𝐼 a -> 𝐼S 1 a) -> (a -> 𝐼 a) -> a -> 𝐼S 1 a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> 𝐼 a
forall a t. Single a t => a -> t
single
instance AppendS 𝐼S where 𝐼S n₁ a
xs ⧺♮ :: forall (n₁ :: 𝐍) a (n₂ :: 𝐍). 𝐼S n₁ a -> 𝐼S n₂ a -> 𝐼S (n₁ + n₂) a
⧺♮ 𝐼S n₂ a
ys = 𝐼 a -> 𝐼S (n₁ + n₂) a
forall (n :: 𝐍) a. 𝐼 a -> 𝐼S n a
𝐼S_UNSAFE (𝐼 a -> 𝐼S (n₁ + n₂) a) -> 𝐼 a -> 𝐼S (n₁ + n₂) a
forall a b. (a -> b) -> a -> b
$ 𝐼S n₁ a -> 𝐼 a
forall (n :: 𝐍) a. 𝐼S n a -> 𝐼 a
un𝐼S 𝐼S n₁ a
xs 𝐼 a -> 𝐼 a -> 𝐼 a
forall a. Append a => a -> a -> a
⧺ 𝐼S n₂ a -> 𝐼 a
forall (n :: 𝐍) a. 𝐼S n a -> 𝐼 a
un𝐼S 𝐼S n₂ a
ys
-- instance AppendSL (𝐿S c) where (⧺♭) = append𝐿S