module UVMHS.Lib.Sep where

import UVMHS.Core

data Sep i a = 
    SepE a
  | SepN a i (𝐼C (a ∧ i)) a

sepI ∷ (Null a) ⇒ i → Sep i a
sepI :: forall a i. Null a => i -> Sep i a
sepI i
i = a -> i -> 𝐼C (a ∧ i) -> a -> Sep i a
forall i a. a -> i -> 𝐼C (a ∧ i) -> a -> Sep i a
SepN a
forall a. Null a => a
null i
i 𝐼C (a ∧ i)
forall a. Null a => a
null a
forall a. Null a => a
null

instance (Null a) ⇒ Null (Sep i a) where null :: Sep i a
null = a -> Sep i a
forall i a. a -> Sep i a
SepE a
forall a. Null a => a
null
instance (Append a) ⇒ Append (Sep i a) where
  SepE a
x₁ ⧺ :: Sep i a -> Sep i a -> Sep i a
⧺ SepE a
x₂ = a -> Sep i a
forall i a. a -> Sep i a
SepE (a -> Sep i a) -> a -> Sep i a
forall a b. (a -> b) -> a -> b
$ a
x₁ a -> a -> a
forall a. Append a => a -> a -> a
⧺ a
x₂
  SepE a
x₁ ⧺ SepN a
x₂₁ i
i₂ 𝐼C (a ∧ i)
xis₂ a
x₂₂ = a -> i -> 𝐼C (a ∧ i) -> a -> Sep i a
forall i a. a -> i -> 𝐼C (a ∧ i) -> a -> Sep i a
SepN (a
x₁ a -> a -> a
forall a. Append a => a -> a -> a
⧺ a
x₂₁) i
i₂ 𝐼C (a ∧ i)
xis₂ a
x₂₂
  SepN a
x₁₁ i
i₁ 𝐼C (a ∧ i)
xis₁ a
x₁₂ ⧺ SepE a
x₂ = a -> i -> 𝐼C (a ∧ i) -> a -> Sep i a
forall i a. a -> i -> 𝐼C (a ∧ i) -> a -> Sep i a
SepN a
x₁₁ i
i₁ 𝐼C (a ∧ i)
xis₁ (a -> Sep i a) -> a -> Sep i a
forall a b. (a -> b) -> a -> b
$ a
x₁₂ a -> a -> a
forall a. Append a => a -> a -> a
⧺ a
x₂
  SepN a
x₁₁ i
i₁ 𝐼C (a ∧ i)
xis₁ a
x₁₂ ⧺ SepN a
x₂₁ i
i₂ 𝐼C (a ∧ i)
xis₂ a
x₂₂ = 
    let xis' :: 𝐼C (a ∧ i)
xis' = 𝐼C (a ∧ i)
xis₁ 𝐼C (a ∧ i) -> 𝐼C (a ∧ i) -> 𝐼C (a ∧ i)
forall a. Append a => a -> a -> a
⧺ (a ∧ i) -> 𝐼C (a ∧ i)
forall a t. Single a t => a -> t
single ((a
x₁₂ a -> a -> a
forall a. Append a => a -> a -> a
⧺ a
x₂₁) a -> i -> a ∧ i
forall a b. a -> b -> a ∧ b
:* i
i₂) 𝐼C (a ∧ i) -> 𝐼C (a ∧ i) -> 𝐼C (a ∧ i)
forall a. Append a => a -> a -> a
⧺ 𝐼C (a ∧ i)
xis₂
    in a -> i -> 𝐼C (a ∧ i) -> a -> Sep i a
forall i a. a -> i -> 𝐼C (a ∧ i) -> a -> Sep i a
SepN a
x₁₁ i
i₁ 𝐼C (a ∧ i)
xis' a
x₂₂
instance (Monoid a) ⇒ Monoid (Sep i a)

instance ToIter a (Sep a a) where
  iter :: Sep a a -> 𝐼 a
iter = \case
    SepE a
x → a -> 𝐼 a
forall a t. Single a t => a -> t
single a
x
    SepN a
x₁ a
i 𝐼C (a ∧ a)
xis a
x₂ → [𝐼 a] -> 𝐼 a
forall a t. (Monoid a, ToIter a t) => t -> a
concat
      [ a -> 𝐼 a
forall a t. Single a t => a -> t
single a
x₁
      , a -> 𝐼 a
forall a t. Single a t => a -> t
single a
i
      , do a
x' :* a
i' ← 𝐼C (a ∧ a) -> 𝐼 (a ∧ a)
forall a t. ToIter a t => t -> 𝐼 a
iter 𝐼C (a ∧ a)
xis  
           [a] -> 𝐼 a
forall a t. ToIter a t => t -> 𝐼 a
iter [a
x',a
i']
      , a -> 𝐼 a
forall a t. Single a t => a -> t
single a
x₂
      ]

instance Functor (Sep i) where map :: forall a b. (a -> b) -> Sep i a -> Sep i b
map = (i -> i) -> (a -> b) -> Sep i a -> Sep i b
forall i j a b. (i -> j) -> (a -> b) -> Sep i a -> Sep j b
mapSep i -> i
forall a. a -> a
id

instance CSized (Sep i a) where
  csize :: Sep i a -> ℕ64
csize = \case
    SepE a
_ → ℕ64
forall a. Zero a => a
zero
    SepN a
_ i
_ 𝐼C (a ∧ i)
xis a
_ → ℕ64
forall a. One a => a
one ℕ64 -> ℕ64 -> ℕ64
forall a. Plus a => a -> a -> a
+ 𝐼C (a ∧ i) -> ℕ64
forall a. CSized a => a -> ℕ64
csize 𝐼C (a ∧ i)
xis

mapSep ∷ (i → j) → (a → b) → Sep i a → Sep j b
mapSep :: forall i j a b. (i -> j) -> (a -> b) -> Sep i a -> Sep j b
mapSep i -> j
f a -> b
g = \case
  SepE a
x → b -> Sep j b
forall i a. a -> Sep i a
SepE (b -> Sep j b) -> b -> Sep j b
forall a b. (a -> b) -> a -> b
$ a -> b
g a
x
  SepN a
x₁ i
i 𝐼C (a ∧ i)
xis a
x₂ → b -> j -> 𝐼C (b ∧ j) -> b -> Sep j b
forall i a. a -> i -> 𝐼C (a ∧ i) -> a -> Sep i a
SepN (a -> b
g a
x₁) (i -> j
f i
i) (((a ∧ i) -> b ∧ j) -> 𝐼C (a ∧ i) -> 𝐼C (b ∧ j)
forall a b. (a -> b) -> 𝐼C a -> 𝐼C b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((a -> b) -> (i -> j) -> (a ∧ i) -> b ∧ j
forall a₁ a₂ b₁ b₂.
(a₁ -> a₂) -> (b₁ -> b₂) -> (a₁ ∧ b₁) -> a₂ ∧ b₂
mapPair a -> b
g i -> j
f) 𝐼C (a ∧ i)
xis) (b -> Sep j b) -> b -> Sep j b
forall a b. (a -> b) -> a -> b
$ a -> b
g a
x₂
  
mapSepI ∷ (i → j) → Sep i a → Sep j a
mapSepI :: forall i j a. (i -> j) -> Sep i a -> Sep j a
mapSepI i -> j
f = (i -> j) -> (a -> a) -> Sep i a -> Sep j a
forall i j a b. (i -> j) -> (a -> b) -> Sep i a -> Sep j b
mapSep i -> j
f a -> a
forall a. a -> a
id