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

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

module Queue.Examples
  (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 public

module Demo where
  demo : Queue → E → E
  demo q e = q .fst .dequeue (q .fst .enqueue e (q .fst .empty)) .fst

  theorem : ∀ q e → ◯ (demo q e ≡ e)
  theorem q e abs = modularity queue-isConcrete (λ q → demo q e) q listQueue abs

module QueueReverse where
  open import Cubical.Data.Nat

  fromList : (q : Queue) → List E → q .fst .X
  fromList q [] = q .fst .empty
  fromList q (e ∷ es) = q .fst .enqueue e (fromList q es)

  toList : (q : Queue) → ℕ → q .fst .X → List E
  toList q zero x = []
  toList q (suc k) x =
    let e , x' = q .fst .dequeue x in
    e ∷ toList q k x'

  qreverse : Queue → List E → List E
  qreverse q l = toList q (length l) (fromList q l)

  reverse = rev

  length-reverse : (l : List E) → length (reverse l) ≡ length l
  length-reverse [] = refl
  length-reverse (x ∷ l) =
    length++ (reverse l) [ x ] ∙
    +-suc (length (rev l))  ∙
    cong suc (+-zero (length (rev l))) ∙
    cong suc (length-reverse l)

  theorem : (q : Queue) → ◯ (qreverse q ≡ reverse)
  theorem q abs = funExt λ l →
      qreverse q l
    ≡⟨ modularity queue-isConcrete (λ q → qreverse q l) q listQueue abs ⟩
      qreverse listQueue l
    ≡⟨ refl ⟩
      toList listQueue (length l) (fromList listQueue l)
    ≡⟨ cong (toList listQueue (length l)) (fromList-lemma l) ⟩
      toList listQueue (length l) (reverse l)
    ≡⟨ cong (λ k → toList listQueue k (reverse l)) (sym (length-reverse l)) ⟩
      toList listQueue (length (reverse l)) (reverse l)
    ≡⟨ toList-lemma (reverse l) ⟩
      reverse l
    ∎
    where
      fromList-lemma : ∀ l → fromList listQueue l ≡ reverse l
      fromList-lemma [] = refl
      fromList-lemma (e ∷ l) = cong (_++ [ e ]) (fromList-lemma l)

      toList-lemma : ∀ l → toList listQueue (length l) l ≡ l
      toList-lemma [] = refl
      toList-lemma (e ∷ l) = cong (e ∷_) (toList-lemma l)