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

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

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

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

-- Ideas adapted from "Internalizing Representation Independence with Univalence" to a phased setting.

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

data Batch (E : Type) : Type where
  inj : List E × List E → Batch E
  tilt : ◯ (∀ e l₁ l₂ → inj (l₁ ++ [ e ] , l₂) ≡ inj (l₁ , l₂ ++ [ e ]))
  trunc : (b b' : Batch E) (α β : b ≡ b') → α ≡ β

multitilt : (l₁ l₂ l₃ : List E) → ◯ (inj (l₁ ++ rev l₃ , l₂) ≡ inj (l₁ , l₂ ++ l₃))
multitilt l₁ l₂ [] abs = cong inj (cong₂ _,_ (++-unit-r l₁) (sym (++-unit-r l₂)))
multitilt l₁ l₂ (e ∷ l₃) abs =
  cong (λ ws → inj (ws , l₂)) (sym (++-assoc l₁ (rev l₃) (e ∷ [])))
  ∙ tilt abs e (l₁ ++ rev l₃) l₂
  ∙ multitilt l₁ (l₂ ++ [ e ]) l₃ abs
  ∙ cong (λ l → inj (l₁ , l)) (++-assoc l₂ [ e ] l₃)

batchedPreQueue : PreQueue
batchedPreQueue .X = Batch E
batchedPreQueue .empty = inj ([] , [])
batchedPreQueue .enqueue = b-enqueue
  where
    b-enqueue : E → Batch E → Batch E
    b-enqueue e (inj (l₁ , l₂)) = inj (e ∷ l₁ , l₂)
    b-enqueue e (tilt abs e' l₁ l₂ i) = tilt abs e' (e ∷ l₁) l₂ i
    b-enqueue e (trunc b b' α β i j) = trunc _ _ (cong (b-enqueue e) α) (cong (b-enqueue e) β) i j

batchedPreQueue .dequeue = b-dequeue
  where
    dequeueFlush : List E → E × Batch E
    dequeueFlush [] = e₀ , inj ([] , [])
    dequeueFlush (e ∷ es) = e , inj ([] , es)

    b-dequeue : Batch E → E × Batch E
    b-dequeue (inj (l₁ , [])) = dequeueFlush (rev l₁)
    b-dequeue (inj (l₁ , e ∷ l₂)) = e , inj (l₁ , l₂)
    b-dequeue (tilt abs e l₁ [] i) = dequeueP i
      where
        dequeueP : dequeueFlush (rev (l₁ ++ [ e ])) ≡ (e , inj (l₁ , []))
        dequeueP =
          cong dequeueFlush (rev-++ l₁ [ e ])
          ∙ cong₂ {B = λ _ → Batch E} {x = e} _,_ refl (sym (multitilt [] [] (rev l₁) abs))
          ∙ cong (λ l → (e , inj (l , []))) (rev-rev l₁)
    b-dequeue (tilt abs e' l₁ (e ∷ l₂) i) = e , tilt abs e' l₁ l₂ i
    b-dequeue (trunc b b' α β i j) =
      isSetΣ ESet (λ _ → trunc)
      (b-dequeue b) (b-dequeue b') (cong b-dequeue α) (cong b-dequeue β)
      i j

quot : List E → Batch E
quot l = inj ([] , l)

eval : Batch E → List E
eval (inj (l₁ , l₂)) = revAppend (l₁ , l₂)
eval (tilt abs e l₁ l₂ i) =
  (cong₂ _++_ refl (rev-++ l₁ [ e ])
  ∙ sym (++-assoc l₂ [ e ] (rev l₁)))
  i
eval (trunc b b' α β i j) = isOfHLevelList  ESet (eval b) (eval b') (cong eval α) (cong eval β) i j

eval-quot : (l : List E) → ◯ (eval (quot l) ≡ l)
eval-quot l _ = ++-unit-r l

quot-eval : (b : Batch E) → ◯ (quot (eval b) ≡ b)
quot-eval (inj (l₁ , l₂)) abs =
  sym (multitilt [] l₂ (rev l₁) abs)
  ∙ cong inj (cong₂ {B = λ _ → List E} _,_ (rev-rev l₁) {u = l₂} refl)
quot-eval (tilt abs e l₁ l₂ i) abs' =
  isOfHLevelPathP'
  {A = λ i → quot (eval (tilt abs e l₁ l₂ i)) ≡ tilt abs e l₁ l₂ i}
  
  (trunc _ _)
      (sym (multitilt [] l₂ (rev (l₁ ++ [ e ])) abs')
      ∙ cong inj (cong₂ {B = λ _ → List E} _,_ (rev-rev (l₁ ++ [ e ])) {u = l₂} refl))
      (sym (multitilt [] (l₂ ++ [ e ]) (rev l₁) abs')
      ∙ cong inj (cong₂ {B = λ _ → List E} _,_ (rev-rev l₁) {u = l₂ ++ [ e ]} refl))
    .fst i
quot-eval (trunc b b' α β i j) abs =
  isOfHLevelPathP'
  {A = λ i →
    PathP (λ j → quot (eval (trunc b b' α β i j)) ≡ trunc b b' α β i j)
      (quot-eval b abs) (quot-eval b' abs)}
  
  (isOfHLevelPathP'  (isOfHLevelSuc  trunc _ _) _ _)
  (cong (λ b → quot-eval b abs) α) (cong (λ b → quot-eval b abs) β)
  .fst i j

quot-empty : ◯ (quot (listPreQueue .empty) ≡ batchedPreQueue .empty)
quot-empty abs = refl

quot-enqueue : ◯ ((e : E) (l : List E) → quot (listPreQueue .enqueue e l) ≡ batchedPreQueue .enqueue e (quot l))
quot-enqueue abs e l = sym (multitilt [] l [ e ] abs)

quot-dequeue : ◯ ((l : List E) →
    (listPreQueue .dequeue l .fst ≡ batchedPreQueue .dequeue (quot l) .fst)
  × (quot (listPreQueue .dequeue l .snd) ≡ batchedPreQueue .dequeue (quot l) .snd))
quot-dequeue abs [] = refl , refl
quot-dequeue abs (x ∷ l) = refl , refl

batchedEquiv : ◯ (Batch E ≃ List E)
batchedEquiv abs = isoToEquiv (iso eval quot (λ l → eval-quot l abs) (λ b → quot-eval b abs))

batchedQueue : Queue
batchedQueue .fst = batchedPreQueue
batchedQueue .snd abs = sym $
  prequeue-path
    (invEquiv (batchedEquiv abs))
    (quot-empty abs)
    (quot-enqueue abs)
    (fst ∘ quot-dequeue abs)
    (snd ∘ quot-dequeue abs)