{-# OPTIONS --cubical #-}
open import Agda.Primitive
open import Cubical.Foundations.Everything
open import Cubical.Relation.Binary
open import Cubical.Relation.Binary.Order.Toset
open import Cubical.Data.Sum.Base
open import Cubical.HITs.PropositionalTruncation
open import Cubical.Relation.Nullary.Base using (Discrete)
module DistrLaw
  {ℓ : _} {A : Type ℓ} (R@(_≤_ , Rprop) : PropRel A A ℓ)
  (≤-Toset : IsToset _≤_)
  (total≤ : (a b : A) → (a ≤ b) ⊎ (b ≤ a))
  where

private
  _≤h_ : A → A → hProp ℓ
  a ≤h b = (a ≤ b , Rprop a b)

open import Cubical.HITs.FiniteMultiset as M
open import FMSetAll
open import Cubical.Data.List.Base hiding (_++_ ; length)
open import Cubical.Data.Unit.Base
open import Cubical.Data.Sigma.Base
open import Cubical.Relation.Binary.Order

open import OnLengthOrder
open import FMSetUniv
open import Cubical.Induction.WellFounded
open import Agda.Builtin.Nat
open import Cubical.Data.Nat.Properties

data L {l} {A : Type l} (r : FMSet A → Type l) : FMSet A → Type l where
  []   : L r []
  _∷_  : {g : FMSet A} (x : A) → (r g) → L r (x ∷ g)

open import Cubical.Data.Maybe


private
  variable
    l : Level
    B : Type l
-- if A has a total order
-- head : FMSet A -> Maybe A
-- head [] = nothing
-- head (x ∷ xs) = {!   !}

-- open import Cubical.Data.Nat

-- test : L (\xs -> Unit*) (1 M.∷ 2 M.∷ 3 M.∷ [])
-- test = 1 ∷ tt*

{-
L' : ∀ {l} {A : Type l} (r : FMSet A → Type l) → FMSet A → Type l
L' r [] = Unit*
L' r (x ∷ xs) = (r xs)
 -}

data EIList {l} {A : Type l} : FMSet A → Type l where
  []  : EIList []
  _∷_ : {g : FMSet A} (x : A) → (EIList g) → EIList (x ∷ g)

-- test : EIList (1 M.∷ 2 M.∷ 3 M.∷ [])
-- test = 1 ∷ (2 ∷ (3 ∷ []))

-- EIList' : ∀ {l} {A : Type l} → FMSet A → Type l
-- EIList' [] = Unit*
-- EIList' (x ∷ xs) = (EIList' xs)

cataL : {r : FMSet B → Type l} → ({g₂ : FMSet B} → L r g₂ → r g₂) →
  {g : FMSet B} → EIList g → r g
cataL alg [] = alg []
cataL alg (x ∷ xs) = alg (x ∷ cataL alg xs)

〖_〗L : {r : FMSet B → Type l} → ({g₂ : FMSet B} → r g₂ → L r g₂) →
  {g : FMSet B} → r g → EIList g
〖_〗L grow {g} seed with grow seed
〖_〗L grow .{[]}    seed | [] = []
〖_〗L grow .{x ∷ g′} seed | _∷_ {g = g′} x seed′ = x ∷ 〖_〗L grow {g′} seed′

module _ {l : Level} {B : Type l} where
  open Length {A = B}
  private
    module WFI<l = WFI (<l-wellfounded {A = B})
    
  〖_〗L′ : {r : FMSet B → Type l} → ({g₂ : FMSet B} → r g₂ → L r g₂) →
    {g : FMSet B} → r g → EIList g
  〖_〗L′ {r = r} grow {g} = WFI<l.induction step g where
    step : ∀ x → (∀ y → y <l x → (r y → EIList y)) → (r x → EIList x)
    step gs IH seed with grow {g₂ = gs} seed
    ...| [] = []
    ...| _∷_ {g = g′} x seed′ = x ∷ IH g′ ( , sym length-∷) seed′

-- Util

infixr -2 _€_
_€_ : {ℓ = ℓ₁ : Level} {ℓ' : Level} {A = A₁ : Type ℓ₁} {B : A₁ → Type ℓ'} →
 (a : A₁) → ((a : A₁) → B a) → B a
_€_ = flip _$_

open IsToset ≤-Toset

≤-to-# : {a b : A} {xs : FMSet A} → a ≤ b →
  All (b ≤h_) xs → All (a ≤h_) xs
≤-to-# {a = a} {b = b} a≤b = mapAll _ _ (is-trans a b _ a≤b)

-- end Util

-- Para

_⌜_ : ∀ {ℓ ℓ′ ℓ′′} {A : Type ℓ} → (L : A → Type ℓ′) → (R : A → Type ℓ′′) → (i : A) → Type (ℓ-max ℓ′ ℓ′′)
_⌜_ l r i = l i × r i

paraL : {l : Level} → {A : Type l} → {r : FMSet A → Type l} → {g : FMSet A} →
  ({g₂ : FMSet A} → L (EIList ⌜ r) g₂ → r g₂) → EIList g → r g
paraL alg [] = alg []
paraL alg (x ∷ l) = alg (x ∷ (l , paraL alg l))

-- end Para

inL : {l : Level} {A : Type l} {g : FMSet A} → (L EIList) g → EIList g
inL [] = []
inL (x ∷ xs) = x ∷ xs

mapL : {l : _} → {A : Type l} → {r r′ : FMSet A → Type l} → {g : FMSet A} →
  ({g₂ : FMSet A} → r g₂ → r′ g₂) → L r g → L r′ g
mapL f [] = []
mapL f (x ∷ rg) = (x ∷ f rg)

infixr  _⋊_
data O (r : FMSet A → Type ℓ) : FMSet A → Type ℓ where
  []   : O r []
  _⋊_ :  {g : FMSet A} (x : A) → (rg : r g) → All (x ≤h_) g → O r (x ∷ g)

data OEIList : FMSet A → Type ℓ where
  []   : OEIList []
  _⋊_ :  {g : FMSet A} (x : A) → (rg : OEIList g) → All (x ≤h_) g → OEIList (x ∷ g)

outO : {g : FMSet A} → OEIList g → (O OEIList) g
outO [] = []
outO ((x ⋊ xs) prf) = (x ⋊ xs) prf

mapO : {r r′ : FMSet A → Type ℓ} → {g : FMSet A} →
  ({g₂ : FMSet A} → r g₂ → r′ g₂) → O r g → O r′ g
mapO f [] = []
mapO f ((x ⋊ rg) prf) = (x ⋊ f rg) prf

anaO : {r : FMSet A → Type ℓ} → ({g₂ : FMSet A} → r g₂ → O r g₂) → {g : FMSet A} → r g → OEIList g
anaO grow {g} seed with grow seed
anaO grow .{[]} seed | [] = []
anaO grow .{x ∷ _} seed | (x ⋊ seed′) prf = (x ⋊ anaO grow {_} seed′) prf

_⊞_ : ∀ {ℓ ℓ′ ℓ′′} {A : Type ℓ} → (L : A → Type ℓ′) → (R : A → Type ℓ′′) → (i : A) → Type (ℓ-max ℓ′ ℓ′′)
_⊞_ l r i = l i ⊎ r i

apoO : {r : FMSet A → Type ℓ} → {g : FMSet A} → ({g₂ : FMSet A} → r g₂ → O (OEIList ⊞ r) g₂) → r g → OEIList g
apoO grow seed with grow seed
... | [] = []
... | ((x ⋊ inl list ) prf) = (x ⋊ list) prf
... | ((x ⋊ inr seed′) prf) = (x ⋊ apoO grow seed′) prf

σ : {g : FMSet A} {r : FMSet A → Type ℓ} → L (O r) g → O (L r) g
σ [] = []
σ (x ∷ []) = (x ⋊ []) []-A
σ (x ∷ (x₁ ⋊ rg) x₂) with total≤ x x₁
...| inl x≤x₁ = (x ⋊ (x₁ ∷ rg)) $ x≤x₁ ∷-A ≤-to-# x≤x₁ x₂
...| inr x₁≤x = (x₁ ⋊ (x ∷ rg)) $ x₁≤x ∷-A x₂ € subst (O (L _)) (comm _ _ _)

-- --

infixl  _₊
infixl  _ₓ

_₊ : ∀ {ℓ ℓ′} {A : Type ℓ} → ((A → Type ℓ′) → (A → Type ℓ′)) → (A → Type ℓ′) → (A → Type ℓ′)
_₊ F p = p ⊞ F p

_ₓ : ∀ {ℓ ℓ′} {A : Type ℓ} → ((A → Type ℓ′) → (A → Type ℓ′)) → (A → Type ℓ′) → (A → Type ℓ′)
_ₓ F p = p ⌜ F p

swop : {g : FMSet A} {r : FMSet A → Type ℓ} → L ((O ₓ) r) g → O ((L ₊) r) g
swop [] = []
swop (x ∷ (fst₁ , [])) = (x ⋊ inl fst₁) []-A
swop (x ∷ (fst₁ , (x₁ ⋊ rg) x₂)) with total≤ x x₁
...| inl x≤x₁ = (x ⋊ inl fst₁) $ x≤x₁ ∷-A ≤-to-# x≤x₁ x₂
...| inr x₁≤x = (x₁ ⋊ inr (x ∷ rg)) $ x₁≤x ∷-A x₂ € subst (O ((L ₊) _)) (comm _ _ _)

insSort bubblesort : {g : FMSet A} → EIList g → OEIList g
insSort     = cataL (anaO (σ ∘ mapL outO))
bubblesort  = anaO (cataL (mapO inL ∘ σ))

-- Ordered Trees

data S (r : FMSet A → Type ℓ) : FMSet A → Type ℓ where
  leaf : S r []
  _┌_┐_ :  {g₁ g₂ : FMSet A} (lt : r g₁) → (x : A) → (rt : r g₂) →
               All (_≤h x) g₁ → All (x ≤h_) g₂ → S r (x ∷ g₁ ++ g₂)

pattern _^_┌_┐_^_ lt g₁ x rt g₂ p1 p2 = _┌_┐_ {g₁ = g₁} {g₂ = g₂} lt x rt p1 p2

data Stree : FMSet A → Type ℓ where
  leaf : Stree []
  _┌_┐_ :  {g₁ g₂ : FMSet A} (lt : Stree g₁) → (x : A) → (rt : Stree g₂) →
               All (_≤h x) g₁ → All (x ≤h_) g₂ → Stree (x ∷ g₁ ++ g₂)

module _ {r : FMSet A → Type ℓ} where
  open Length {A = A}
  private
    module WFI<l = WFI (<l-wellfounded {A = A})

    shuffle1 : ∀ {g₁ g₂ x} → length g₁ + suc (length g₂) ≡ length (x ∷ g₁ ++ g₂)
    shuffle1 {g₁} {g₂} {x} =
      length g₁ + suc (length g₂) ≡⟨ +-suc _ _ ⟩
      suc (length g₁ + length g₂) ≡⟨ cong suc (sym length-++) ⟩
      suc (length (g₁ ++ g₂)) ≡⟨ sym length-∷ ⟩
      length (x ∷ g₁ ++ g₂) ∎

    sub1 : ∀ g₁ → ∀ {g₂ x} → Σ[ d ∈ Nat ] d + suc (length g₂) ≡ length (x ∷ g₁ ++ g₂)
    sub1 g₁ = (length g₁ , shuffle1)

    shuffle2 : ∀ {g₁ g₂ x} → length g₂ + suc (length g₁) ≡ length (x ∷ g₁ ++ g₂)
    shuffle2 {g₁} {g₂} {x} = shuffle1 ∙ cong (length ∘ (x ∷_)) (comm-++ g₂ g₁)

    sub2 : ∀ g₂ → ∀ {g₁ x} → Σ[ d ∈ Nat ] d + suc (length g₁) ≡ length (x ∷ g₁ ++ g₂)
    sub2 g₂ = (length g₂ , shuffle2)

  anaS : (grow : {gₓ : FMSet A} → r gₓ → S r gₓ) → {g : FMSet A} → r g → Stree g
  anaS grow {g = g} = WFI<l.induction step g where
    step : ∀ x → (∀ y → y <l x → (r y → Stree y)) → (r x → Stree x)
    step gs IH seed with grow {gₓ = gs} seed
    ...| leaf                            = leaf
    ...| (lt ^ g₁ ┌ x₁ ┐ rt ^ g₂) p₁ p₂  = (IH g₁ (sub2 g₂) lt ┌ x₁ ┐ IH g₂ (sub1 g₁) rt) p₁ p₂

  apoS : (grow : {gₓ : FMSet A} → r gₓ → S (Stree ⊞ r) gₓ) → {g : FMSet A} → r g → Stree g
  apoS grow {g = g} = WFI<l.induction step g where
    step : ∀ x → (∀ y → y <l x → (r y → Stree y)) → (r x → Stree x)
    step gs IH seed with grow {gₓ = gs} seed
    ...| leaf                                    = leaf
    ...| (inl lt ┌ x₁ ┐ inl rt) p₁ p₂            = (lt ┌ x₁ ┐ rt) p₁ p₂
    ...| (inr ls ^ g₁ ┌ x₁ ┐ inl rt ^ g₂) p₁ p₂  = (IH g₁ (sub2 g₂) ls ┌ x₁ ┐ rt) p₁ p₂
    ...| (inl lt ^ g₁ ┌ x₁ ┐ inr rs ^ g₂) p₁ p₂  = (lt ┌ x₁ ┐ IH g₂ (sub1 g₁) rs) p₁ p₂
    ...| (inr ls ^ g₁ ┌ x₁ ┐ inr rs ^ g₂) p₁ p₂  = (IH g₁ (sub2 g₂) ls ┌ x₁ ┐ IH g₂ (sub1 g₁) rs) p₁ p₂

-- apoS grow seed with grow seed
-- ... | leaf = leaf
-- ... | (inl lt ┌ x₁ ┐ inl rt) prf₁ prf₂ = (lt ┌ x₁ ┐ rt) prf₁ prf₂
-- ... | (inr ls ┌ x₁ ┐ inl rt) prf₁ prf₂ = (apoS grow ls ┌ x₁ ┐ rt) prf₁ prf₂
-- ... | (inl lt ┌ x₁ ┐ inr rs) prf₁ prf₂ = (lt ┌ x₁ ┐ apoS grow rs) prf₁ prf₂
-- ... | (inr ls ┌ x₁ ┐ inr rs) prf₁ prf₂ = (apoS grow ls ┌ x₁ ┐ apoS grow rs) prf₁ prf₂

-- anaS⇂ : {r : FMSet A → Type ℓ} → ({gₓ : FMSet A} → r gₓ → S r gₓ) → {g : FMSet A} → r g → Stree g
-- anaS⇂ grow {gs} seed with grow seed
-- anaS⇂ grow .{[]} seed | leaf = leaf
-- anaS⇂ grow .{x₁ ∷ g₁ ++ g₂} seed | (ls ^ g₁ ┌ x₁ ┐ rs ^ g₂) prf₁ prf₂ =
--   (anaS⇂ grow {g₁} ls ┌ x₁ ┐ anaS⇂ grow {g₂} rs) prf₁ prf₂

private
  rearrange : (x x₁ : A) → (g₁ g₂ : FMSet A) →
    x₁ ∷ g₁ ++ (x ∷ g₂) ≡ x ∷ x₁ ∷ g₁ ++ g₂
  rearrange x x₁ g₁ g₂ =
    x₁ ∷ g₁ ++ (x ∷ g₂) ≡⟨ cong (x₁ ∷_) (comm-++ g₁ (x ∷ g₂))⟩
    x₁ ∷ x ∷ g₂ ++ g₁   ≡⟨ cong (λ o → x₁ ∷ x ∷ o) (comm-++ g₂ g₁)⟩
    x₁ ∷ x ∷ (g₁ ++ g₂) ≡⟨ comm _ _ _ ⟩
    x ∷ x₁ ∷ g₁ ++ g₂ ∎

sprout : {g : FMSet A} {r : FMSet A → Type ℓ} → L ((S ₓ) r) g → S ((L ₊) r) g
sprout []                                  = leaf
sprout (x ∷ (fst₁ , leaf))                 = (inl fst₁ ┌ x ┐ inl fst₁) []-A []-A
sprout (x ∷ (fst₁ , (lt ┌ x₁ ┐ rt) x₂ x₃)) with total≤ x x₁
...| inl x≤x₁ = (inr (x ∷ lt) ┌ x₁ ┐ inl rt) (x≤x₁ ∷-A x₂) x₃ €
       subst (S ((L ₊) _)) (comm _ _ _)
sprout (x ∷ (fst₁ , (lt ^ g₁ ┌ x₁ ┐ rt ^ _) x₂ x₃)) |
     inr x₁≤x = (inl lt ┌ x₁ ┐ inr (x ∷ rt)) x₂ (x₁≤x ∷-A x₃) €
       subst (S ((L ₊) _)) $ rearrange _ _ g₁ _

wither : {g : FMSet A} {r : FMSet A → Type ℓ} → S ((O ₓ) r) g → O ((S ₊) r) g
wither leaf = []
wither (((fst₁ , []) ┌ x ┐ (fst₂ , snd₂)) x₁ x₂) = (x ⋊ inl fst₂) x₂
wither (((fst₁ , (x₃ ⋊ rg) x₄) ┌ x ┐ (fst₂ , snd₂)) x₁ x₂) with uncons-A x₁
... | (x₃≤x , All-x≤-g) = (x₃ ⋊ inr ((rg ┌ x ┐ fst₂) All-x≤-g x₂))
  (x₃≤x ∷-A x₄ ++-A ≤-to-# x₃≤x x₂) €
  subst (O ((S ₊) _)) (comm _ _ _)

-- heapsort

data H (r : FMSet A → Type ℓ) : FMSet A → Type ℓ where
  leaf : H r []
  _┌_┐_ :  {g₁ g₂ : FMSet A} (lt : r g₁) → (x : A) → (rt : r g₂) →
               All (x ≤h_) g₁ → All (x ≤h_) g₂ → H r (x ∷ g₁ ++ g₂)

pattern _^_┌_┐_^_ lt g₁ x rt g₂ p1 p2 = _┌_┐_ {g₁ = g₁} {g₂ = g₂} lt x rt p1 p2

pile : {g : FMSet A} {r : FMSet A → Type ℓ} → L ((H ₓ) r) g → H ((L ₊) r) g
pile []                                  = leaf
pile (x ∷ (fst₁ , leaf))                 = (inl fst₁ ┌ x ┐ inl fst₁) []-A []-A
pile (x ∷ (fst₁ , (lt ┌ x₁ ┐ rt) x₂ x₃)) with total≤ x x₁
pile (x ∷ (fst₁ , (lt ^ _ ┌ x₁ ┐ rt ^ g₂) x₂ x₃))
  | inl x≤x₁ = (inr (x₁ ∷ rt) ┌ x ┐ inl lt) (≤-to-# x≤x₁ (is-refl _ ∷-A x₃)) (≤-to-# x≤x₁ x₂) €
       subst (H ((L ₊) _)) (cong (λ o → x ∷ x₁ ∷ o) (comm-++ g₂ _))
pile (x ∷ (fst₁ , (lt ^ _ ┌ x₁ ┐ rt ^ g₂) x₂ x₃))
  | inr x₁≤x = (inr (x ∷ rt) ┌ x₁ ┐ inl lt) (x₁≤x ∷-A x₃) x₂ €
       subst (H ((L ₊) _)) ((comm _ _ _) ∙ cong (λ o → x ∷ x₁ ∷ o) (comm-++ g₂ _))

sift : {g : FMSet A} {r : FMSet A → Type ℓ} → H ((O ₓ) r) g → O ((H ₊) r) g
sift leaf = []
sift (((fst₁ , []) ┌ x ┐ (fst₂ , snd₂)) x₁ x₂) = (x ⋊ inl fst₂) x₂
sift (((fst₁ , (x₃ ⋊ rg) x₄) ┌ x ┐ (fst₂ , [])) x₁ x₂) = (x ⋊ inl fst₁) x₁ € subst (O ((H ₊) _)) $ sym $ unitr-++ (x ∷ x₃ ∷ _)
sift (((l , (b ⋊ l') b#l') ┌ a ┐ (r , (c ⋊ r') c#r')) a#l a#r) with total≤ b c | uncons-A a#l
...| inl b≤c | (a≤b , _) = (a ⋊  inr ((l' ┌ b ┐ r) b#l' (b≤c ∷-A ≤-to-# b≤c c#r'))) (a#l ++-A a#r)
sift (((l , (b ⋊ l') b#l') ^ (_ ∷ g₁) ┌ a ┐ (r , (c ⋊ r') c#r') ^ _) a#l a#r)
  | inr c≤b | (a≤b , _) = (a ⋊ inr ((l ┌ c ┐ r') (≤-to-# c≤b $ is-refl _ ∷-A b#l') c#r' €
    subst (H _) (sym (rearrange _ _ g₁ _))))
    (a≤b ∷-A (≤-to-# a≤b b#l') ++-A a#r)