module UVMHS.Core.Chunky where

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

import qualified Prelude as HS

import qualified Data.Char as HS


------------
-- Chunks --
------------

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

toBitsℤ64 ∷ ℤ64 → ℕ64
toBitsℤ64 :: ℤ64 -> ℕ64
toBitsℤ64 = ℤ64 -> ℕ64
forall a b. a -> b
coerce_UNSAFE

frBitsℤ64 ∷ ℕ64 → ℤ64
frBitsℤ64 :: ℕ64 -> ℤ64
frBitsℤ64 = ℕ64 -> ℤ64
forall a b. a -> b
coerce_UNSAFE

toBits𝔻 ∷ 𝔻 → ℕ64
toBits𝔻 :: 𝔻 -> ℕ64
toBits𝔻 = 𝔻 -> ℕ64
forall a b. a -> b
coerce_UNSAFE

frBits𝔻 ∷ ℕ64 → 𝔻
frBits𝔻 :: ℕ64 -> 𝔻
frBits𝔻 = ℕ64 -> 𝔻
forall a b. a -> b
coerce_UNSAFE

skipChunk ∷ (Monad m) ⇒ m ℕ8 → ℕ64 → m ()
skipChunk :: forall (m :: * -> *). Monad m => m ℕ8 -> ℕ64 -> m ()
skipChunk m ℕ8
g ℕ64
n₀ = ℕ64 -> m ()
loop (ℕ -> ℕ64
𝕟64 ℕ
0)
  where
    loop :: ℕ64 -> m ()
loop ℕ64
n
      | ℕ64
n ℕ64 -> ℕ64 -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ ℕ64
n₀ = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return ()
      | 𝔹
otherwise = do
          ℕ8
_ ← m ℕ8
g
          ℕ64 -> m ()
loop (ℕ64 -> m ()) -> ℕ64 -> m ()
forall a b. (a -> b) -> a -> b
$ ℕ64 -> ℕ64
forall a. (One a, Plus a) => a -> a
succ ℕ64
n

emptyChunk ∷ ℕ64 → 𝐼 ℕ8
emptyChunk :: ℕ64 -> 𝐼 ℕ8
emptyChunk ℕ64
n = ℕ -> ℕ8 -> 𝐼 ℕ8
forall n a. (Eq n, Zero n, One n, Plus n) => n -> a -> 𝐼 a
replicate (ℕ64 -> ℕ
forall a. ToNat a => a -> ℕ
nat ℕ64
n) (ℕ -> ℕ8
𝕟8 ℕ
0)

joinBytes ∷ (ℕ8,ℕ8,ℕ8,ℕ8,ℕ8,ℕ8,ℕ8,ℕ8) → ℕ64
joinBytes :: (ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8) -> ℕ64
joinBytes (ℕ8
b₁,ℕ8
b₂,ℕ8
b₃,ℕ8
b₄,ℕ8
b₅,ℕ8
b₆,ℕ8
b₇,ℕ8
b₈) =
    ℕ8 -> ℕ64
forall a. ToNat64 a => a -> ℕ64
nat64 ℕ8
b₁ ℕ64 -> ℕ64 -> ℕ64
forall a. BitShiftL a => a -> ℕ64 -> a
⋘ ℕ -> ℕ64
𝕟64  ℕ
0 
  ℕ64 -> ℕ64 -> ℕ64
forall a. BitOr a => a -> a -> a
⟇ ℕ8 -> ℕ64
forall a. ToNat64 a => a -> ℕ64
nat64 ℕ8
b₂ ℕ64 -> ℕ64 -> ℕ64
forall a. BitShiftL a => a -> ℕ64 -> a
⋘ ℕ -> ℕ64
𝕟64  ℕ
8 
  ℕ64 -> ℕ64 -> ℕ64
forall a. BitOr a => a -> a -> a
⟇ ℕ8 -> ℕ64
forall a. ToNat64 a => a -> ℕ64
nat64 ℕ8
b₃ ℕ64 -> ℕ64 -> ℕ64
forall a. BitShiftL a => a -> ℕ64 -> a
⋘ ℕ -> ℕ64
𝕟64 ℕ
16 
  ℕ64 -> ℕ64 -> ℕ64
forall a. BitOr a => a -> a -> a
⟇ ℕ8 -> ℕ64
forall a. ToNat64 a => a -> ℕ64
nat64 ℕ8
b₄ ℕ64 -> ℕ64 -> ℕ64
forall a. BitShiftL a => a -> ℕ64 -> a
⋘ ℕ -> ℕ64
𝕟64 ℕ
24
  ℕ64 -> ℕ64 -> ℕ64
forall a. BitOr a => a -> a -> a
⟇ ℕ8 -> ℕ64
forall a. ToNat64 a => a -> ℕ64
nat64 ℕ8
b₅ ℕ64 -> ℕ64 -> ℕ64
forall a. BitShiftL a => a -> ℕ64 -> a
⋘ ℕ -> ℕ64
𝕟64 ℕ
32 
  ℕ64 -> ℕ64 -> ℕ64
forall a. BitOr a => a -> a -> a
⟇ ℕ8 -> ℕ64
forall a. ToNat64 a => a -> ℕ64
nat64 ℕ8
b₆ ℕ64 -> ℕ64 -> ℕ64
forall a. BitShiftL a => a -> ℕ64 -> a
⋘ ℕ -> ℕ64
𝕟64 ℕ
40 
  ℕ64 -> ℕ64 -> ℕ64
forall a. BitOr a => a -> a -> a
⟇ ℕ8 -> ℕ64
forall a. ToNat64 a => a -> ℕ64
nat64 ℕ8
b₇ ℕ64 -> ℕ64 -> ℕ64
forall a. BitShiftL a => a -> ℕ64 -> a
⋘ ℕ -> ℕ64
𝕟64 ℕ
48 
  ℕ64 -> ℕ64 -> ℕ64
forall a. BitOr a => a -> a -> a
⟇ ℕ8 -> ℕ64
forall a. ToNat64 a => a -> ℕ64
nat64 ℕ8
b₈ ℕ64 -> ℕ64 -> ℕ64
forall a. BitShiftL a => a -> ℕ64 -> a
⋘ ℕ -> ℕ64
𝕟64 ℕ
56

splitBytes ∷ ℕ64 → (ℕ8,ℕ8,ℕ8,ℕ8,ℕ8,ℕ8,ℕ8,ℕ8)
splitBytes :: ℕ64 -> (ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8)
splitBytes ℕ64
n =
  ( ℕ64 -> ℕ8
trℕ8 (ℕ64 -> ℕ8) -> ℕ64 -> ℕ8
forall a b. (a -> b) -> a -> b
$ ℕ64
n ℕ64 -> ℕ64 -> ℕ64
forall a. BitShiftR a => a -> ℕ64 -> a
⋙ ℕ -> ℕ64
𝕟64  ℕ
0
  , ℕ64 -> ℕ8
trℕ8 (ℕ64 -> ℕ8) -> ℕ64 -> ℕ8
forall a b. (a -> b) -> a -> b
$ ℕ64
n ℕ64 -> ℕ64 -> ℕ64
forall a. BitShiftR a => a -> ℕ64 -> a
⋙ ℕ -> ℕ64
𝕟64  ℕ
8
  , ℕ64 -> ℕ8
trℕ8 (ℕ64 -> ℕ8) -> ℕ64 -> ℕ8
forall a b. (a -> b) -> a -> b
$ ℕ64
n ℕ64 -> ℕ64 -> ℕ64
forall a. BitShiftR a => a -> ℕ64 -> a
⋙ ℕ -> ℕ64
𝕟64 ℕ
16
  , ℕ64 -> ℕ8
trℕ8 (ℕ64 -> ℕ8) -> ℕ64 -> ℕ8
forall a b. (a -> b) -> a -> b
$ ℕ64
n ℕ64 -> ℕ64 -> ℕ64
forall a. BitShiftR a => a -> ℕ64 -> a
⋙ ℕ -> ℕ64
𝕟64 ℕ
24
  , ℕ64 -> ℕ8
trℕ8 (ℕ64 -> ℕ8) -> ℕ64 -> ℕ8
forall a b. (a -> b) -> a -> b
$ ℕ64
n ℕ64 -> ℕ64 -> ℕ64
forall a. BitShiftR a => a -> ℕ64 -> a
⋙ ℕ -> ℕ64
𝕟64 ℕ
32
  , ℕ64 -> ℕ8
trℕ8 (ℕ64 -> ℕ8) -> ℕ64 -> ℕ8
forall a b. (a -> b) -> a -> b
$ ℕ64
n ℕ64 -> ℕ64 -> ℕ64
forall a. BitShiftR a => a -> ℕ64 -> a
⋙ ℕ -> ℕ64
𝕟64 ℕ
40
  , ℕ64 -> ℕ8
trℕ8 (ℕ64 -> ℕ8) -> ℕ64 -> ℕ8
forall a b. (a -> b) -> a -> b
$ ℕ64
n ℕ64 -> ℕ64 -> ℕ64
forall a. BitShiftR a => a -> ℕ64 -> a
⋙ ℕ -> ℕ64
𝕟64 ℕ
48
  , ℕ64 -> ℕ8
trℕ8 (ℕ64 -> ℕ8) -> ℕ64 -> ℕ8
forall a b. (a -> b) -> a -> b
$ ℕ64
n ℕ64 -> ℕ64 -> ℕ64
forall a. BitShiftR a => a -> ℕ64 -> a
⋙ ℕ -> ℕ64
𝕟64 ℕ
56
  )

class Chunky a where
  chunkSize ∷ P a → ℕ64
  fromChunk ∷ ∀ m. (Monad m) ⇒ m ℕ8 → m a
  toChunk ∷ a → 𝐼 ℕ8

instance {-# OVERLAPPABLE #-} (Chunky b,a ⇄ b) ⇒ Chunky a where
  chunkSize :: P a -> ℕ64
chunkSize P a
P = forall a. Chunky a => P a -> ℕ64
chunkSize @b P b
forall k (a :: k). P a
P
  fromChunk :: forall (m :: * -> *). Monad m => m ℕ8 -> m a
fromChunk = (b -> a) -> m b -> m a
forall a b. (a -> b) -> m a -> m b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map b -> a
forall a b. (a ⇄ b) => b -> a
isofr (m b -> m a) -> (m ℕ8 -> m b) -> m ℕ8 -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ m ℕ8 -> m b
forall a (m :: * -> *). (Chunky a, Monad m) => m ℕ8 -> m a
forall (m :: * -> *). Monad m => m ℕ8 -> m b
fromChunk
  toChunk :: a -> 𝐼 ℕ8
toChunk = b -> 𝐼 ℕ8
forall a. Chunky a => a -> 𝐼 ℕ8
toChunk (b -> 𝐼 ℕ8) -> (a -> b) -> a -> 𝐼 ℕ8
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> b
forall a b. (a ⇄ b) => a -> b
isoto

instance Chunky () where
  chunkSize :: P () -> ℕ64
chunkSize P ()
P = ℕ -> ℕ64
𝕟64 ℕ
0
  fromChunk :: forall (m :: * -> *). Monad m => m ℕ8 -> m ()
fromChunk m ℕ8
_ = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return ()
  toChunk :: () -> 𝐼 ℕ8
toChunk ()  = 𝐼 ℕ8
forall a. 𝐼 a
empty𝐼

instance Chunky ℕ8 where
  chunkSize :: P ℕ8 -> ℕ64
chunkSize P ℕ8
P = ℕ -> ℕ64
𝕟64 ℕ
1
  fromChunk :: forall (m :: * -> *). Monad m => m ℕ8 -> m ℕ8
fromChunk   = m ℕ8 -> m ℕ8
forall a. a -> a
id
  toChunk :: ℕ8 -> 𝐼 ℕ8
toChunk     = ℕ8 -> 𝐼 ℕ8
forall a t. Single a t => a -> t
single

instance Chunky 𝔹 where
  chunkSize :: P 𝔹 -> ℕ64
chunkSize P 𝔹
P = ℕ -> ℕ64
𝕟64 ℕ
1
  fromChunk :: forall (m :: * -> *). Monad m => m ℕ8 -> m 𝔹
fromChunk m ℕ8
g = do
    ℕ8
b ← m ℕ8
g
    𝔹 -> m 𝔹
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return (𝔹 -> m 𝔹) -> 𝔹 -> m 𝔹
forall a b. (a -> b) -> a -> b
$ case ℕ8
b ℕ8 -> ℕ8 -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ ℕ -> ℕ8
𝕟8 ℕ
0 of
      𝔹
True → 𝔹
False 
      𝔹
False → 𝔹
True
  toChunk :: 𝔹 -> 𝐼 ℕ8
toChunk 𝔹
b = ℕ8 -> 𝐼 ℕ8
forall a. Chunky a => a -> 𝐼 ℕ8
toChunk (ℕ8 -> 𝐼 ℕ8) -> ℕ8 -> 𝐼 ℕ8
forall a b. (a -> b) -> a -> b
$ case 𝔹
b of
    𝔹
False → ℕ -> ℕ8
𝕟8 ℕ
0
    𝔹
True → ℕ -> ℕ8
𝕟8 ℕ
1

instance Chunky ℂ where
  chunkSize :: P ℂ -> ℕ64
chunkSize P ℂ
P = ℕ -> ℕ64
𝕟64 ℕ
4
  fromChunk :: forall (m :: * -> *). Monad m => m ℕ8 -> m ℂ
fromChunk m ℕ8
g = do
    ℕ8
b₁ ← m ℕ8
g ; ℕ8
b₂ ← m ℕ8
g ; ℕ8
b₃ ← m ℕ8
g ; ℕ8
b₄ ← m ℕ8
g
    ℂ -> m ℂ
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return (ℂ -> m ℂ) -> ℂ -> m ℂ
forall a b. (a -> b) -> a -> b
$ Int -> ℂ
HS.chr (Int -> ℂ) -> Int -> ℂ
forall a b. (a -> b) -> a -> b
$ ℤ64 -> Int
forall a b. CHS a b => a -> b
tohs (ℤ64 -> Int) -> ℤ64 -> Int
forall a b. (a -> b) -> a -> b
$ ℕ64 -> ℤ64
frBitsℤ64 (ℕ64 -> ℤ64) -> ℕ64 -> ℤ64
forall a b. (a -> b) -> a -> b
$ (ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8) -> ℕ64
joinBytes (ℕ8
b₁,ℕ8
b₂,ℕ8
b₃,ℕ8
b₄,ℕ -> ℕ8
𝕟8 ℕ
0,ℕ -> ℕ8
𝕟8 ℕ
0,ℕ -> ℕ8
𝕟8 ℕ
0,ℕ -> ℕ8
𝕟8 ℕ
0)
  toChunk :: ℂ -> 𝐼 ℕ8
toChunk ℂ
c = (forall b. (ℕ8 -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
-> 𝐼 ℕ8
forall a.
(forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
𝐼 ((forall b. (ℕ8 -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
 -> 𝐼 ℕ8)
-> (forall b. (ℕ8 -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
-> 𝐼 ℕ8
forall a b. (a -> b) -> a -> b
HS.$ \ (ℕ8 -> b -> (b -> b) -> b
f ∷ ℕ8 → b → (b → b) → b) b
i b -> b
𝓀 →
    let (ℕ8
b₁,ℕ8
b₂,ℕ8
b₃,ℕ8
b₄,ℕ8
_,ℕ8
_,ℕ8
_,ℕ8
_) = ℕ64 -> (ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8)
splitBytes (ℕ64 -> (ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8))
-> ℕ64 -> (ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8)
forall a b. (a -> b) -> a -> b
$ ℤ64 -> ℕ64
toBitsℤ64 (ℤ64 -> ℕ64) -> ℤ64 -> ℕ64
forall a b. (a -> b) -> a -> b
$ Int -> ℤ64
forall a b. CHS a b => b -> a
frhs (Int -> ℤ64) -> Int -> ℤ64
forall a b. (a -> b) -> a -> b
$ ℂ -> Int
HS.ord ℂ
c
    in 
      ℕ8 -> b -> (b -> b) -> b
f ℕ8
b₁ b
i ((b -> b) -> b) -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b
i' →
      ℕ8 -> b -> (b -> b) -> b
f ℕ8
b₂ b
i' ((b -> b) -> b) -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b
i'' → 
      ℕ8 -> b -> (b -> b) -> b
f ℕ8
b₃ b
i'' ((b -> b) -> b) -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b
i''' → 
      ℕ8 -> b -> (b -> b) -> b
f ℕ8
b₄ b
i''' b -> b
𝓀

instance Chunky ℕ64 where
  chunkSize :: P ℕ64 -> ℕ64
chunkSize P ℕ64
P = ℕ -> ℕ64
𝕟64 ℕ
8
  fromChunk :: forall (m :: * -> *). Monad m => m ℕ8 -> m ℕ64
fromChunk m ℕ8
g = do
    ℕ8
b₁ ← m ℕ8
g ; ℕ8
b₂ ← m ℕ8
g ; ℕ8
b₃ ← m ℕ8
g ; ℕ8
b₄ ← m ℕ8
g
    ℕ8
b₅ ← m ℕ8
g ; ℕ8
b₆ ← m ℕ8
g ; ℕ8
b₇ ← m ℕ8
g ; ℕ8
b₈ ← m ℕ8
g
    ℕ64 -> m ℕ64
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return (ℕ64 -> m ℕ64) -> ℕ64 -> m ℕ64
forall a b. (a -> b) -> a -> b
$ (ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8) -> ℕ64
joinBytes (ℕ8
b₁,ℕ8
b₂,ℕ8
b₃,ℕ8
b₄,ℕ8
b₅,ℕ8
b₆,ℕ8
b₇,ℕ8
b₈)
  toChunk :: ℕ64 -> 𝐼 ℕ8
toChunk ℕ64
n = (forall b. (ℕ8 -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
-> 𝐼 ℕ8
forall a.
(forall b. (a -> b -> (b -> b) -> b) -> b -> (b -> b) -> b) -> 𝐼 a
𝐼 ((forall b. (ℕ8 -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
 -> 𝐼 ℕ8)
-> (forall b. (ℕ8 -> b -> (b -> b) -> b) -> b -> (b -> b) -> b)
-> 𝐼 ℕ8
forall a b. (a -> b) -> a -> b
HS.$ \ (ℕ8 -> b -> (b -> b) -> b
f ∷ ℕ8 → b → (b → b) → b) b
i b -> b
𝓀 →
    let (ℕ8
b₁,ℕ8
b₂,ℕ8
b₃,ℕ8
b₄,ℕ8
b₅,ℕ8
b₆,ℕ8
b₇,ℕ8
b₈) = ℕ64 -> (ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8, ℕ8)
splitBytes ℕ64
n
    in 
      ℕ8 -> b -> (b -> b) -> b
f ℕ8
b₁ b
i ((b -> b) -> b) -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b
i' →
      ℕ8 -> b -> (b -> b) -> b
f ℕ8
b₂ b
i' ((b -> b) -> b) -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b
i'' →
      ℕ8 -> b -> (b -> b) -> b
f ℕ8
b₃ b
i'' ((b -> b) -> b) -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b
i''' →
      ℕ8 -> b -> (b -> b) -> b
f ℕ8
b₄ b
i''' ((b -> b) -> b) -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b
i'''' →
      ℕ8 -> b -> (b -> b) -> b
f ℕ8
b₅ b
i'''' ((b -> b) -> b) -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b
i''''' →
      ℕ8 -> b -> (b -> b) -> b
f ℕ8
b₆ b
i''''' ((b -> b) -> b) -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b
i'''''' →
      ℕ8 -> b -> (b -> b) -> b
f ℕ8
b₇ b
i'''''' ((b -> b) -> b) -> (b -> b) -> b
forall a b. (a -> b) -> a -> b
$ \ b
i''''''' →
      ℕ8 -> b -> (b -> b) -> b
f ℕ8
b₈ b
i''''''' b -> b
𝓀

instance Chunky ℤ64 where
  chunkSize :: P ℤ64 -> ℕ64
chunkSize P ℤ64
P = ℕ -> ℕ64
𝕟64 ℕ
8
  fromChunk :: forall (m :: * -> *). Monad m => m ℕ8 -> m ℤ64
fromChunk = (ℕ64 -> ℤ64) -> m ℕ64 -> m ℤ64
forall a b. (a -> b) -> m a -> m b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (forall a b. a -> b
coerce_UNSAFE @ℕ64 @ℤ64) (m ℕ64 -> m ℤ64) -> (m ℕ8 -> m ℕ64) -> m ℕ8 -> m ℤ64
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ m ℕ8 -> m ℕ64
forall a (m :: * -> *). (Chunky a, Monad m) => m ℕ8 -> m a
forall (m :: * -> *). Monad m => m ℕ8 -> m ℕ64
fromChunk
  toChunk :: ℤ64 -> 𝐼 ℕ8
toChunk = ℕ64 -> 𝐼 ℕ8
forall a. Chunky a => a -> 𝐼 ℕ8
toChunk (ℕ64 -> 𝐼 ℕ8) -> (ℤ64 -> ℕ64) -> ℤ64 -> 𝐼 ℕ8
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (forall a b. a -> b
coerce_UNSAFE @ℤ64 @ℕ64)

instance Chunky 𝔻 where
  chunkSize :: P 𝔻 -> ℕ64
chunkSize P 𝔻
P = ℕ -> ℕ64
𝕟64 ℕ
8
  fromChunk :: forall (m :: * -> *). Monad m => m ℕ8 -> m 𝔻
fromChunk = (ℕ64 -> 𝔻) -> m ℕ64 -> m 𝔻
forall a b. (a -> b) -> m a -> m b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (forall a b. a -> b
coerce_UNSAFE @ℕ64 @𝔻) (m ℕ64 -> m 𝔻) -> (m ℕ8 -> m ℕ64) -> m ℕ8 -> m 𝔻
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ m ℕ8 -> m ℕ64
forall a (m :: * -> *). (Chunky a, Monad m) => m ℕ8 -> m a
forall (m :: * -> *). Monad m => m ℕ8 -> m ℕ64
fromChunk
  toChunk :: 𝔻 -> 𝐼 ℕ8
toChunk = ℕ64 -> 𝐼 ℕ8
forall a. Chunky a => a -> 𝐼 ℕ8
toChunk (ℕ64 -> 𝐼 ℕ8) -> (𝔻 -> ℕ64) -> 𝔻 -> 𝐼 ℕ8
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ (forall a b. a -> b
coerce_UNSAFE @𝔻 @ℕ64)

instance (Chunky a,Chunky b) ⇒ Chunky (a ∧ b) where
  chunkSize :: P (a ∧ b) -> ℕ64
chunkSize P (a ∧ b)
P = forall a. Chunky a => P a -> ℕ64
chunkSize @a P a
forall k (a :: k). P a
P ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ forall a. Chunky a => P a -> ℕ64
chunkSize @b P b
forall k (a :: k). P a
P
  fromChunk :: forall (m :: * -> *). Monad m => m ℕ8 -> m (a ∧ b)
fromChunk m ℕ8
g = do
    a
x ← m ℕ8 -> m a
forall a (m :: * -> *). (Chunky a, Monad m) => m ℕ8 -> m a
forall (m :: * -> *). Monad m => m ℕ8 -> m a
fromChunk m ℕ8
g
    b
y ← m ℕ8 -> m b
forall a (m :: * -> *). (Chunky a, Monad m) => m ℕ8 -> m a
forall (m :: * -> *). Monad m => m ℕ8 -> m b
fromChunk m ℕ8
g
    (a ∧ b) -> m (a ∧ b)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return ((a ∧ b) -> m (a ∧ b)) -> (a ∧ b) -> m (a ∧ b)
forall a b. (a -> b) -> a -> b
$ a
x a -> b -> a ∧ b
forall a b. a -> b -> a ∧ b
:* b
y
  toChunk :: (a ∧ b) -> 𝐼 ℕ8
toChunk (a
x :* b
y) = a -> 𝐼 ℕ8
forall a. Chunky a => a -> 𝐼 ℕ8
toChunk a
x 𝐼 ℕ8 -> 𝐼 ℕ8 -> 𝐼 ℕ8
forall a. Append a => a -> a -> a
⧺ b -> 𝐼 ℕ8
forall a. Chunky a => a -> 𝐼 ℕ8
toChunk b
y

instance (Chunky a,Chunky b) ⇒ Chunky (a ∨ b) where
  chunkSize :: P (a ∨ b) -> ℕ64
chunkSize P (a ∨ b)
P = ℕ -> ℕ64
𝕟64 ℕ
1 ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ (forall a. Chunky a => P a -> ℕ64
chunkSize @a P a
forall k (a :: k). P a
P ℕ64 -> ℕ64 -> ℕ64
forall a. Ord a => a -> a -> a
⩏ forall a. Chunky a => P a -> ℕ64
chunkSize @b P b
forall k (a :: k). P a
P)
  fromChunk :: forall (m :: * -> *). Monad m => m ℕ8 -> m (a ∨ b)
fromChunk m ℕ8
g = do
    ℕ8
b ← m ℕ8
g
    case ℕ8
b ℕ8 -> ℕ8 -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ ℕ -> ℕ8
𝕟8 ℕ
0 of
      𝔹
True → do
        a
x ← m ℕ8 -> m a
forall a (m :: * -> *). (Chunky a, Monad m) => m ℕ8 -> m a
forall (m :: * -> *). Monad m => m ℕ8 -> m a
fromChunk m ℕ8
g
        m ℕ8 -> ℕ64 -> m ()
forall (m :: * -> *). Monad m => m ℕ8 -> ℕ64 -> m ()
skipChunk m ℕ8
g (ℕ64 -> m ()) -> ℕ64 -> m ()
forall a b. (a -> b) -> a -> b
$ (forall a. Chunky a => P a -> ℕ64
chunkSize @a P a
forall k (a :: k). P a
P ℕ64 -> ℕ64 -> ℕ64
forall a. Ord a => a -> a -> a
⩏ forall a. Chunky a => P a -> ℕ64
chunkSize @b P b
forall k (a :: k). P a
P) ℕ64 -> ℕ64 -> ℕ64
forall a. Minus a => a -> a -> a
- forall a. Chunky a => P a -> ℕ64
chunkSize @a P a
forall k (a :: k). P a
P
        (a ∨ b) -> m (a ∨ b)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return ((a ∨ b) -> m (a ∨ b)) -> (a ∨ b) -> m (a ∨ b)
forall a b. (a -> b) -> a -> b
$ a -> a ∨ b
forall a b. a -> a ∨ b
Inl a
x
      𝔹
False → do
        b
y ← m ℕ8 -> m b
forall a (m :: * -> *). (Chunky a, Monad m) => m ℕ8 -> m a
forall (m :: * -> *). Monad m => m ℕ8 -> m b
fromChunk m ℕ8
g
        m ℕ8 -> ℕ64 -> m ()
forall (m :: * -> *). Monad m => m ℕ8 -> ℕ64 -> m ()
skipChunk m ℕ8
g (ℕ64 -> m ()) -> ℕ64 -> m ()
forall a b. (a -> b) -> a -> b
$ (forall a. Chunky a => P a -> ℕ64
chunkSize @a P a
forall k (a :: k). P a
P ℕ64 -> ℕ64 -> ℕ64
forall a. Ord a => a -> a -> a
⩏ forall a. Chunky a => P a -> ℕ64
chunkSize @b P b
forall k (a :: k). P a
P) ℕ64 -> ℕ64 -> ℕ64
forall a. Minus a => a -> a -> a
- forall a. Chunky a => P a -> ℕ64
chunkSize @b P b
forall k (a :: k). P a
P
        (a ∨ b) -> m (a ∨ b)
forall a. a -> m a
forall (m :: * -> *) a. Return m => a -> m a
return ((a ∨ b) -> m (a ∨ b)) -> (a ∨ b) -> m (a ∨ b)
forall a b. (a -> b) -> a -> b
$ b -> a ∨ b
forall a b. b -> a ∨ b
Inr b
y
  toChunk :: (a ∨ b) -> 𝐼 ℕ8
toChunk = \case
    Inl a
x → ℕ8 -> 𝐼 ℕ8
forall a t. Single a t => a -> t
single (ℕ -> ℕ8
𝕟8 ℕ
0) 𝐼 ℕ8 -> 𝐼 ℕ8 -> 𝐼 ℕ8
forall a. Append a => a -> a -> a
⧺ a -> 𝐼 ℕ8
forall a. Chunky a => a -> 𝐼 ℕ8
toChunk a
x 𝐼 ℕ8 -> 𝐼 ℕ8 -> 𝐼 ℕ8
forall a. Append a => a -> a -> a
⧺ ℕ64 -> 𝐼 ℕ8
emptyChunk ((forall a. Chunky a => P a -> ℕ64
chunkSize @a P a
forall k (a :: k). P a
P ℕ64 -> ℕ64 -> ℕ64
forall a. Ord a => a -> a -> a
⩏ forall a. Chunky a => P a -> ℕ64
chunkSize @b P b
forall k (a :: k). P a
P) ℕ64 -> ℕ64 -> ℕ64
forall a. Minus a => a -> a -> a
- forall a. Chunky a => P a -> ℕ64
chunkSize @a P a
forall k (a :: k). P a
P)
    Inr b
y → ℕ8 -> 𝐼 ℕ8
forall a t. Single a t => a -> t
single (ℕ -> ℕ8
𝕟8 ℕ
1) 𝐼 ℕ8 -> 𝐼 ℕ8 -> 𝐼 ℕ8
forall a. Append a => a -> a -> a
⧺ b -> 𝐼 ℕ8
forall a. Chunky a => a -> 𝐼 ℕ8
toChunk b
y 𝐼 ℕ8 -> 𝐼 ℕ8 -> 𝐼 ℕ8
forall a. Append a => a -> a -> a
⧺ ℕ64 -> 𝐼 ℕ8
emptyChunk ((forall a. Chunky a => P a -> ℕ64
chunkSize @a P a
forall k (a :: k). P a
P ℕ64 -> ℕ64 -> ℕ64
forall a. Ord a => a -> a -> a
⩏ forall a. Chunky a => P a -> ℕ64
chunkSize @b P b
forall k (a :: k). P a
P) ℕ64 -> ℕ64 -> ℕ64
forall a. Minus a => a -> a -> a
- forall a. Chunky a => P a -> ℕ64
chunkSize @b P b
forall k (a :: k). P a
P)

-- chunkIOBytes ∷ UArr.UArray ℕ64 ℕ8 → State ℕ64 ℕ8
-- chunkIOBytes a = do
--   i ← next
--   return $ a UArr.! i