open import Cubical.Foundations.Prelude hiding (empty)
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Function
open import Cubical.Foundations.Univalence hiding (Glue; glue)

open import Cubical.Data.List
open import Cubical.Data.Sigma hiding (empty)

module Queue.Glued
  (ABS : Type) (ABS-isProp : isProp ABS)
  (E : Type) (e₀ : E) (ESet : isSet E) where

open import Modality.Glue ABS ABS-isProp
open import Queue.Base ABS ABS-isProp E e₀ ESet

private
  revAppend : List E × List E → List E
  revAppend (l₁ , l₂) = l₂ ++ rev l₁


batchedPreQueue : PreQueue
batchedPreQueue .X = Glue' revAppend

batchedPreQueue .empty = triangle empty-⊤ empty-abs empty-correct
  where
    empty-⊤ : List E × List E
    empty-⊤ = [] , []

    empty-abs : List E
    empty-abs = listPreQueue .empty

    empty-correct : revAppend empty-⊤ ≡ empty-abs
    empty-correct = refl

batchedPreQueue .enqueue e =
  square (enqueue-⊤ e) (enqueue-abs e) enqueue-correct
  where
    enqueue-⊤ : E → List E × List E → List E × List E
    enqueue-⊤ e (l₁ , l₂) = e ∷ l₁ , l₂

    enqueue-abs : E → List E → List E
    enqueue-abs = listPreQueue .enqueue

    enqueue-correct : revAppend ∘ enqueue-⊤ e ≡ enqueue-abs e ∘ revAppend
    enqueue-correct = funExt λ { (l₁ , l₂) → sym (++-assoc l₂ (rev l₁) (e ∷ [])) }

batchedPreQueue .dequeue x =
  glue (square (fst ∘ dequeue-⊤) (fst ∘ dequeue-abs) fst-dequeue-correct x) ,
  square (snd ∘ dequeue-⊤) (snd ∘ dequeue-abs) snd-dequeue-correct x
  where
    dequeue-⊤ : List E × List E → E × (List E × List E)
    dequeue-⊤ (l₁ , []) with rev l₁
    ... | [] = e₀ , [] , []
    ... | e ∷ l₂ = e , [] , l₂
    dequeue-⊤ (l₁ , e ∷ l₂) = e , l₁ , l₂

    dequeue-abs : List E → E × List E
    dequeue-abs = listPreQueue .dequeue

    fst-dequeue-correct : fst ∘ dequeue-⊤ ≡ (fst ∘ dequeue-abs) ∘ revAppend
    fst-dequeue-correct = funExt lemma
      where
        lemma : (x : List E × List E) → fst (dequeue-⊤ x) ≡ fst (dequeue-abs (revAppend x))
        lemma (l₁ , []) with rev l₁
        ... | [] = refl
        ... | e ∷ l₂ = refl
        lemma (l₁ , e ∷ l₂) = refl

    snd-dequeue-correct : revAppend ∘ (snd ∘ dequeue-⊤) ≡ (snd ∘ dequeue-abs) ∘ revAppend
    snd-dequeue-correct = funExt lemma
      where
        lemma : (x : List E × List E) → revAppend (snd (dequeue-⊤ x)) ≡ snd (dequeue-abs (revAppend x))
        lemma (l₁ , []) with rev l₁
        ... | [] = refl
        ... | e ∷ l₂ = ++-unit-r l₂
        lemma (l₁ , e ∷ l₂) = refl


batchedQueue : Queue
batchedQueue .fst = batchedPreQueue
batchedQueue .snd abs =
  prequeue-path
    (◯Glue' revAppend abs)
    refl
    (λ e q →
        equivFun (◯Glue' revAppend abs) (batchedPreQueue .enqueue e q)
      ≡⟨ refl ⟩
        transport refl (q .snd .fst (transport refl abs) ++ [ e ])
      ≡⟨ transportRefl _ ⟩
        q .snd .fst (transport refl abs) ++ [ e ]
      ≡⟨ sym (cong (_++ [ e ]) (transportRefl _)) ⟩
        transport refl (q .snd .fst (transport refl abs)) ++ [ e ]
      ≡⟨ refl ⟩
        listPreQueue .enqueue e (◯Glue' revAppend abs .fst q)
      ∎
    )
    (λ q →
        glue (square _ (fst ∘ listPreQueue .dequeue) _ q)
      ≡⟨ ◯glue (square _ (fst ∘ listPreQueue .dequeue) _ q) abs ⟩
        fst (listPreQueue .dequeue (q .snd .fst abs))
      ≡⟨ cong (λ x → fst (listPreQueue .dequeue (q .snd .fst x))) (sym (transportRefl abs)) ⟩
        fst (listPreQueue .dequeue (q .snd .fst (transport refl abs)))
      ≡⟨ cong (fst ∘ listPreQueue .dequeue) (sym (transportRefl (q .snd .fst (transport refl abs)))) ⟩
        fst (listPreQueue .dequeue (transport refl (q .snd .fst (transport refl abs))))
      ≡⟨ refl ⟩
        fst (listPreQueue .dequeue (◯Glue' revAppend abs .fst q))
      ∎
    )
    (λ q →
        equivFun (◯Glue' revAppend abs) (snd (batchedPreQueue .dequeue q))
      ≡⟨ refl ⟩
        transport refl (snd (listPreQueue .dequeue (q .snd .fst (transport refl abs))))
      ≡⟨ transportRefl _ ⟩
        snd (listPreQueue .dequeue (q .snd .fst (transport refl abs)))
      ≡⟨ sym (cong {y = q .snd .fst _} (λ x → snd (listPreQueue .dequeue x)) (transportRefl _)) ⟩
        snd (listPreQueue .dequeue (transport refl (q .snd .fst (transport refl abs))))
      ≡⟨ refl ⟩
        snd (listPreQueue .dequeue (◯Glue' revAppend abs .fst q))
      ∎
    )