{-# OPTIONS --cubical --safe --exact-split #-}

module Cubical.Structures.Set.CMon.CList where

open import Cubical.Foundations.Everything
open import Cubical.Data.Sigma
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.Empty as ⊥
import Cubical.Data.List as L

import Cubical.Structures.Set.Mon.Desc as M
import Cubical.Structures.Set.CMon.Desc as M
import Cubical.Structures.Free as F
open import Cubical.Structures.Sig
open import Cubical.Structures.Str public
open import Cubical.Structures.Tree
open import Cubical.Structures.Eq
open import Cubical.Structures.Arity

infixr  _∷_

data CList {a} (A : Type a) : Type a where
  [] : CList A
  _∷_ : (a : A) -> (as : CList A) -> CList A
  comm : (a b : A)
      -> {as bs : CList A} (cs : CList A)
      -> (p : as ≡ b ∷ cs) (q : bs ≡ a ∷ cs)
      -> a ∷ as ≡ b ∷ bs
  isSetCList : isSet (CList A)

pattern [_] a = a ∷ []

module elimCListSet {ℓ p : Level} {A : Type ℓ} (P : CList A -> Type p)
                   ([]* : P [])
                   (_∷*_ : (x : A) {xs : CList A} -> P xs -> P (x ∷ xs))
                   (comm* : (a b : A)
                            -> {as bs : CList A} {cs : CList A}
                            -> {as* : P as}
                            -> {bs* : P bs}
                            -> (cs* : P cs)
                            -> {p : as ≡ b ∷ cs} {q : bs ≡ a ∷ cs}
                            -> (bp : PathP (λ i -> P (p i)) as* (b ∷* cs*))
                            -> (bq : PathP (λ i -> P (q i)) bs* (a ∷* cs*))
                            -> PathP (λ i -> P (comm a b cs p q i)) (a ∷* as*) (b ∷* bs*)
                   )
                   (isSetCList* : {xs : CList A} -> isSet (P xs))
                   where
  f : (xs : CList A) -> P xs
  f [] = []*
  f (a ∷ as) = a ∷* f as
  f (comm a b {as} {bs} cs p q i) =
    comm* a b (f cs) (cong f p) (cong f q) i
  f (isSetCList xs ys p q i j) =
    isOfHLevel→isOfHLevelDep  (λ xs -> isSetCList* {xs = xs}) (f xs) (f ys) (cong f p) (cong f q) (isSetCList xs ys p q) i j

module elimCListProp {ℓ p : Level} {A : Type ℓ} (P : CList A -> Type p)
                   ([]* : P [])
                   (_∷*_ : (x : A) {xs : CList A} -> P xs -> P (x ∷ xs))
                   (isSetCList* : {xs : CList A} -> isProp (P xs))
                   where
  f : (xs : CList A) -> P xs
  f = elimCListSet.f P []* _∷*_
    (λ a b {as} {bs} {cs} {as*} {bs*} cs* bp bq -> toPathP (isSetCList* _ (b ∷* bs*)))
    (isProp→isSet isSetCList*)

private
  variable
    ℓ : Level
    A : Type ℓ

_++_ : CList A -> CList A -> CList A
[] ++ bs = bs
(a ∷ as) ++ bs = a ∷ (as ++ bs)
comm a b cs p q i ++ bs = comm a b (cs ++ bs) (cong (_++ bs) p) (cong (_++ bs) q) i
isSetCList a b p q i j ++ bs = isSetCList (a ++ bs) (b ++ bs) (cong (_++ bs) p) (cong (_++ bs) q) i j

++-unitl : (as : CList A) -> [] ++ as ≡ as
++-unitl as = refl

++-unitr : (as : CList A) -> as ++ [] ≡ as
++-unitr = elimCListProp.f _ refl (λ a p -> cong (a ∷_) p) (isSetCList _ _)

++-assocr : (as bs cs : CList A) -> (as ++ bs) ++ cs ≡ as ++ (bs ++ cs)
++-assocr = elimCListProp.f _
  (λ _ _ -> refl)
  (λ x p bs cs -> cong (x ∷_) (p bs cs))
  (isPropΠ λ _ -> isPropΠ λ _ -> isSetCList _ _)

swap : (a b : A) (cs : CList A) -> a ∷ b ∷ cs ≡ b ∷ a ∷ cs
swap a b cs = comm a b cs refl refl

++-∷ : (a : A) (as : CList A) -> a ∷ as ≡ as ++ [ a ]
++-∷ a = elimCListProp.f (λ as -> a ∷ as ≡ as ++ [ a ])
  refl
  (λ b {as} p -> swap a b as ∙ cong (b ∷_) p)
  (isSetCList _ _) 

++-comm : (as bs : CList A) -> as ++ bs ≡ bs ++ as
++-comm = elimCListProp.f _
  (sym ∘ ++-unitr)
  (λ a {as} p bs -> cong (a ∷_) (p bs) ∙ cong (_++ as) (++-∷ a bs) ∙ ++-assocr bs [ a ] as)
  (isPropΠ λ _ -> isSetCList _ _)

clist-α : ∀ {n : Level} {X : Type n} -> sig M.MonSig (CList X) -> CList X
clist-α (M.`e , i) = []
clist-α (M.`⊕ , i) = i fzero ++ i fone

module Free {x y : Level} {A : Type x} {𝔜 : struct y M.MonSig} (isSet𝔜 : isSet (𝔜 .car)) (𝔜-cmon : 𝔜 ⊨ M.CMonSEq) where
  module 𝔜 = M.CMonSEq 𝔜 𝔜-cmon

  𝔛 : M.CMonStruct
  𝔛 = < CList A , clist-α >

  module _ (f : A -> 𝔜 .car) where
    _♯ : CList A -> 𝔜 .car
    _♯ = elimCListSet.f _
      𝔜.e
      (λ a p -> f a 𝔜.⊕ p)
      (λ a b {ab} {bs} {cs} {as*} {bs*} cs* bp bq ->
        f a 𝔜.⊕ as* ≡⟨ cong (f a 𝔜.⊕_) bp ⟩
        f a 𝔜.⊕ f b 𝔜.⊕ cs* ≡⟨ sym (𝔜.assocr _ _ _) ⟩
        (f a 𝔜.⊕ f b) 𝔜.⊕ cs* ≡⟨ cong (𝔜._⊕ cs*) (𝔜.comm _ _) ⟩
        (f b 𝔜.⊕ f a) 𝔜.⊕ cs* ≡⟨ 𝔜.assocr _ _ _ ⟩
        f b 𝔜.⊕ (f a 𝔜.⊕ cs*) ≡⟨ cong (f b 𝔜.⊕_) (sym bq) ⟩
        f b 𝔜.⊕ bs* ∎
      )
      isSet𝔜

    private
      ♯-++ : ∀ xs ys -> (xs ++ ys) ♯ ≡ (xs ♯) 𝔜.⊕ (ys ♯)
      ♯-++ = elimCListProp.f _
        (λ ys -> sym (𝔜.unitl (ys ♯)))
        (λ a {xs} p ys ->
          f a 𝔜.⊕ ((xs ++ ys) ♯) ≡⟨ cong (f a 𝔜.⊕_) (p ys) ⟩
          f a 𝔜.⊕ ((xs ♯) 𝔜.⊕ (ys ♯)) ≡⟨ sym (𝔜.assocr (f a) (xs ♯) (ys ♯)) ⟩
          _ ∎
        )
        (isPropΠ λ _ -> isSet𝔜 _ _)

    ♯-isMonHom : structHom 𝔛 𝔜
    fst ♯-isMonHom = _♯
    snd ♯-isMonHom M.`e i = 𝔜.e-eta
    snd ♯-isMonHom M.`⊕ i = 𝔜.⊕-eta i _♯ ∙ sym (♯-++ (i fzero) (i fone))

  private
    clistEquivLemma : (g : structHom 𝔛 𝔜) -> (x : CList A) -> g .fst x ≡ ((g .fst ∘ [_]) ♯) x
    clistEquivLemma (g , homMonWit) = elimCListProp.f _
      (sym (homMonWit M.`e (lookup L.[])) ∙ 𝔜.e-eta)
      (λ x {xs} p ->
        g (x ∷ xs) ≡⟨ sym (homMonWit M.`⊕ (lookup ([ x ] L.∷ xs L.∷ L.[]))) ⟩
        _ ≡⟨ 𝔜.⊕-eta (lookup ([ x ] L.∷ xs L.∷ L.[])) g ⟩
        _ ≡⟨ cong (g [ x ] 𝔜.⊕_) p ⟩
        _ ∎
      )
      (isSet𝔜 _ _)

    clistEquivLemma-β : (g : structHom 𝔛 𝔜) -> g ≡ ♯-isMonHom (g .fst ∘ [_])
    clistEquivLemma-β g = structHom≡ 𝔛 𝔜 g (♯-isMonHom (g .fst ∘ [_])) isSet𝔜 (funExt (clistEquivLemma g))

  clistMonEquiv : structHom 𝔛 𝔜 ≃ (A -> 𝔜 .car)
  clistMonEquiv =
    isoToEquiv (iso (λ g -> g .fst ∘ [_]) ♯-isMonHom (λ g -> funExt (𝔜.unitr ∘ g)) (sym ∘ clistEquivLemma-β))

module CListDef = F.Definition M.MonSig M.CMonEqSig M.CMonSEq

clist-sat : ∀ {n} {X : Type n} -> < CList X , clist-α > ⊨ M.CMonSEq
clist-sat (M.`mon M.`unitl) ρ = ++-unitl (ρ fzero)
clist-sat (M.`mon M.`unitr) ρ = ++-unitr (ρ fzero)
clist-sat (M.`mon M.`assocr) ρ = ++-assocr (ρ fzero) (ρ fone) (ρ ftwo)
clist-sat M.`comm ρ = ++-comm (ρ fzero) (ρ fone)

clistDef : ∀ {ℓ ℓ'} -> CListDef.Free ℓ ℓ' 
F.Definition.Free.F clistDef = CList
F.Definition.Free.η clistDef = [_]
F.Definition.Free.α clistDef = clist-α
F.Definition.Free.sat clistDef = clist-sat
F.Definition.Free.isFree clistDef isSet𝔜 satMon = (Free.clistMonEquiv isSet𝔜 satMon) .snd