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

module Cubical.Structures.Set.CMon.Desc where

open import Cubical.Foundations.Everything
open import Cubical.Data.Nat
open import Cubical.Data.Nat.Order
open import Cubical.Data.List
open import Cubical.Data.Sigma
open import Cubical.Data.Empty as 
open import Cubical.Functions.Logic as L
open import Cubical.Structures.Arity as F public

open import Cubical.Structures.Sig
open import Cubical.Structures.Str public
open import Cubical.Structures.Tree
open import Cubical.Structures.Eq

import Cubical.Structures.Set.Mon.Desc as M

open M.MonSym

CMonSym = M.MonSym
CMonAr = M.MonAr
CMonFinSig = M.MonFinSig
CMonSig = M.MonSig

CMonStruct :  {n} -> Type (ℓ-suc n)
CMonStruct {n} = struct n CMonSig

CMon→Mon :  {} -> CMonStruct {} -> M.MonStruct {}
car (CMon→Mon 𝔛) = 𝔛 .car
alg (CMon→Mon 𝔛) = 𝔛 .alg

module CMonStruct {} (𝔛 : CMonStruct {}) where
  open M.MonStruct (CMon→Mon 𝔛) public

data CMonEq : Type where
  `mon : M.MonEq -> CMonEq
  `comm : CMonEq

CMonEqFree : CMonEq -> 
CMonEqFree (`mon eqn) = M.MonEqFree eqn
CMonEqFree `comm = 2

CMonEqSig : EqSig ℓ-zero ℓ-zero
CMonEqSig = finEqSig (CMonEq , CMonEqFree)

cmonEqLhs : (eq : CMonEq) -> FinTree CMonFinSig (CMonEqFree eq)
cmonEqLhs (`mon eqn) = M.monEqLhs eqn
cmonEqLhs `comm = node (`⊕ , lookup (leaf fzero  leaf fone  []))

cmonEqRhs : (eq : CMonEq) -> FinTree CMonFinSig (CMonEqFree eq)
cmonEqRhs (`mon eqn) = M.monEqRhs eqn
cmonEqRhs `comm = node (`⊕ , lookup (leaf fone  leaf fzero  []))

CMonSEq : sysEq CMonSig CMonEqSig
CMonSEq n = cmonEqLhs n , cmonEqRhs n

cmonSatMon :  {s} {str : struct s CMonSig} -> str  CMonSEq -> str  M.MonSEq
cmonSatMon {_} {str} cmonSat eqn ρ = cmonSat (`mon eqn) ρ

module CMonSEq {} (𝔛 : CMonStruct {}) (ϕ : 𝔛  CMonSEq) where
  open M.MonSEq (CMon→Mon 𝔛) (cmonSatMon ϕ) public

  comm :  m n -> m  n  n  m
  comm m n =
      m  n
    ≡⟨⟩
      𝔛 .alg (`⊕ , lookup (m  n  []))
    ≡⟨ cong  z -> 𝔛 .alg (`⊕ , z)) (funExt lemma1) 
      𝔛 .alg (`⊕ ,  x -> sharp CMonSig 𝔛 (lookup (m  n  [])) (lookup (leaf fzero  leaf fone  []) x)))
    ≡⟨ ϕ `comm (lookup (m  n  [])) 
      𝔛 .alg (`⊕ ,  x -> sharp CMonSig 𝔛 (lookup (m  n  [])) (lookup (leaf fone  leaf fzero  []) x)))
    ≡⟨ cong  z -> 𝔛 .alg (`⊕ , z)) (sym (funExt lemma2)) 
      𝔛 .alg (`⊕ , lookup (n  m  []))
    ≡⟨⟩
      n  m 
    where
      lemma1 : (w : CMonSig .arity `⊕) -> lookup (m  n  []) w  sharp CMonSig 𝔛 (lookup (m  n  [])) (lookup (leaf fzero  leaf fone  []) w)
      lemma1 (zero , p) = refl
      lemma1 (suc zero , p) = refl
      lemma1 (suc (suc n) , p) = ⊥.rec (¬m+n<m {m = 2} p)

      lemma2 : (w : CMonSig .arity `⊕) -> lookup (n  m  []) w  sharp CMonSig 𝔛 (lookup (m  n  [])) (lookup (leaf fone  leaf fzero  []) w)
      lemma2 (zero , p) = refl
      lemma2 (suc zero , p) = refl
      lemma2 (suc (suc n) , p) = ⊥.rec (¬m+n<m {m = 2} p)

ℕ-CMonStr : CMonStruct
ℕ-CMonStr = M.ℕ-MonStr

ℕ-CMonStr-MonSEq : ℕ-CMonStr  CMonSEq
ℕ-CMonStr-MonSEq (`mon eqn) ρ = M.ℕ-MonStr-MonSEq eqn ρ
ℕ-CMonStr-MonSEq `comm ρ = +-comm (ρ fzero) (ρ fone)

⊔-MonStr-CMonSEq : ( : Level) -> M.⊔-MonStr   CMonSEq
⊔-MonStr-CMonSEq  (`mon eqn) ρ = M.⊔-MonStr-MonSEq  eqn ρ
⊔-MonStr-CMonSEq  `comm ρ = ⊔-comm (ρ fzero) (ρ fone)

⊓-MonStr-CMonSEq : ( : Level) -> M.⊓-MonStr   CMonSEq
⊓-MonStr-CMonSEq  (`mon eqn) ρ = M.⊓-MonStr-MonSEq  eqn ρ
⊓-MonStr-CMonSEq  `comm ρ = ⊓-comm (ρ fzero) (ρ fone)