{-# OPTIONS --cubical --exact-split #-}
module FMSetUniv where
open import Cubical.Foundations.Everything
import Cubical.Data.Empty as ⊥
import Cubical.Functions.Logic as L
open import Cubical.HITs.FiniteMultiset
open import Cubical.Data.Unit.Base
open import Cubical.Data.Nat
open import Cubical.Data.FinSet
open import Cubical.Relation.Nullary
open import Cubical.HITs.PropositionalTruncation as P
open import Cubical.Data.Sum as S
open import Cubical.Data.Unit as ⊤
open import Cubical.Data.Sigma

postulate
  TODO : ∀ {ℓ} {A : Type ℓ} → A

module _ {n : Level} where
  -- level n versions
  ⊥* : hProp n
  ⊥* = ⊥.⊥* , \{ () }
  ⊔-identityˡ* : (P : hProp n) → ⊥* L.⊔ P ≡ P
  ⊔-identityˡ* P = L.⇒∶ (L.⊔-elim ⊥* P (λ _ → P) (λ ()) (λ x → x))
                     ⇐∶ L.inr

module _ {n : Level} {A : Type n} {isDiscA : Discrete A} where

    decElim : ∀ {ℓ ℓ'} {P : Type ℓ} {A : Dec P → Type ℓ'} → ((p : P) → A (yes p)) → ((q : ¬ P) → A (no q)) → (p : Dec P) → A p
    decElim ifyes ifno (yes p) = ifyes p
    decElim ifyes ifno (no ¬p) = ifno ¬p

    isDiscA-β-yes : (a x : A) (p : a ≡ x) -> isDiscA a x ≡ yes p
    isDiscA-β-yes a x p =
      decElim {A = \d -> d ≡ yes p}
        (\q -> congS yes (Discrete→isSet isDiscA a x q p))
        (\q -> ⊥.rec (q p))
        (isDiscA a x)

    isDiscA-β-refl : (x : A) -> isDiscA x x ≡ yes refl
    isDiscA-β-refl x = isDiscA-β-yes x x refl

    isDiscA-β-no : (a x : A) (p : ¬ (a ≡ x)) -> isDiscA a x ≡ no p
    isDiscA-β-no a x p =
      decElim {A = \d -> d ≡ no p}
        (\q -> ⊥.rec (p q))
        (\q -> congS no (isProp→ ⊥.isProp⊥ q p))
        (isDiscA a x)

module Mem {n : Level} {A : Type n} {isSetA : isSet A} (x : A) where
  private
    よ : A → hProp n
    よ a = (a ≡ x) , isSetA a x
    module mem = FMSetUniversal isSetHProp ⊥* L._⊔_ L.⊔-comm L.⊔-assoc ⊔-identityˡ* よ
  opaque
    _∈_ : FMSet A → hProp n
    _∈_ = mem.f-extend

module Length {n : Level} {A : Type n} where
  private
    module 1♯ = FMSetUniversal {A = A} isSetℕ  _+_ +-comm +-assoc (\_ -> refl) (\_ -> )

  opaque
    length : FMSet A -> ℕ
    length = 1♯.f-extend

    length-[] : length [] ≡ 
    length-[] = 1♯.f-extend-nil

    length-∷ : ∀ {x xs} -> length (x ∷ xs) ≡  + length xs
    length-∷ {x = x} {xs = xs} = 1♯.f-extend-cons x xs

    length-++ : ∀ {xs ys} -> length (xs ++ ys) ≡ length xs + length ys
    length-++ {xs = xs} {ys = ys} = 1♯.f-extend-++ xs ys

    length-0 : ∀ {xs} -> length xs ≡  -> xs ≡ []
    length-0 {xs = xs} =
      ElimProp.f {B = \xs -> length xs ≡  -> xs ≡ []}
        (isProp→ (trunc _ _)) (\_ -> refl) (\x {xs} f p -> ⊥.rec (snotz (sym (length-∷ {x = x} {xs = xs}) ∙ p))) xs

module Count {n : Level} {A : Type n} {isDiscA : Discrete A} (x : A) where
  private
    Χ : A → ℕ
    Χ a = decRec (\_ -> ) (\_ -> ) (isDiscA a x)

    Χ-β : Χ x ≡ 
    Χ-β = congS (decRec _ _) (isDiscA-β-refl {isDiscA = isDiscA} x)

    module count = FMSetUniversal isSetℕ  _+_ +-comm +-assoc (\_ -> refl) Χ

  opaque
    _∈ᵐ_ : FMSet A → ℕ
    _∈ᵐ_ = count.f-extend

    ∈ᵐ-[] : (_∈ᵐ_ []) ≡ 
    ∈ᵐ-[] = count.f-extend-nil

    ∈ᵐ-∷ : ∀ {xs} -> (_∈ᵐ_ (x ∷ xs)) ≡  + _∈ᵐ_ xs
    ∈ᵐ-∷ {xs = xs} = let q = count.f-extend-cons x xs in q ∙ congS (_+ _∈ᵐ_ xs) Χ-β

    ∈ᵐ-++ : ∀ {xs ys} -> (_∈ᵐ_ (xs ++ ys)) ≡ (_∈ᵐ_ xs) + (_∈ᵐ_ ys)
    ∈ᵐ-++ {xs = xs} {ys = ys} = let q = count.f-extend-++ xs ys in q

module Remove {n : Level} {A : Type n} {isDiscA : Discrete A} (x : A) where
  private
    r : A -> FMSet A
    r a = decRec (\_ -> []) (\_ -> [ a ]) (isDiscA a x)
    module rem = FMSetUniversal {A = A} trunc [] _++_ comm-++ assoc-++ unitl-++ r

  rem : FMSet A → FMSet A
  rem = rem.f-extend

_ : Remove.rem {isDiscA = discreteℕ}  ( ∷  ∷  ∷  ∷ []) ≡ ( ∷  ∷ [])
_ = refl

module _ {n : Level} (A : Type n) where
  supp : (A -> ℕ) -> Type n
  supp f = Σ[ a ∈ A ] ¬ (f a ≡ )

  FMultiSet : Type n
  FMultiSet = Σ[ f ∈ (A -> ℕ) ] isFinSet (supp f)

-- module FM {n : Level} (A : Type n) {isDiscA : Discrete A} where

--   isSetFMultiSet : isSet (FMultiSet A)
--   isSetFMultiSet = isSetΣSndProp (isSet→ isSetℕ) (\_ -> isPropIsFinSet)

--   null : FMultiSet A
--   null = (\_ -> 0) , 0 , ∣ isoToEquiv (iso (\{ (a , ϕ) -> ϕ refl }) ⊥.rec ⊥.elim \{ (a , ϕ) -> ⊥.rec (ϕ refl) }) ∣₁

--   singleton : A -> FMultiSet A
--   singleton x = (\a -> decRec (\_ -> 1) (\_ -> 0) (isDiscA a x)) , 1 ,
--     ∣ isoToEquiv (iso (\{ (a , ϕ) -> inl tt }) (S.rec (\_ -> x , (\q -> snotz (congS (decRec _ _) (sym (isDiscA-β-refl {isDiscA = isDiscA} x)) ∙ q))) ⊥.elim)
--                  (S.elim (\a -> congS inl (isContrUnit .snd a)) ⊥.elim) \{ (a , ϕ) -> Σ≡Prop (\_ -> isProp→ ⊥.isProp⊥) (decRec sym (\ψ -> ⊥.rec (ϕ (congS (decRec _ _) (isDiscA-β-no a x ψ)))) (isDiscA a x)) }) ∣₁

--   _∪_ : FMultiSet A -> FMultiSet A -> FMultiSet A
--   (f , m , ϕ) ∪ (g , n , ψ) =
--     (\a -> f a + g a) , m + n ,
--       P.map2
--         (\e1 e2 -> TODO)
--         ϕ ψ

-- module _ {n : Level} {A : Type n} where
--   module fm = FM A
--   module fmset = FMSetUniversal fm.isSetFMultiSet fm.null fm._∪_ TODO TODO TODO fm.singleton

--   FMSet→FMultiset : FMSet A -> FMultiSet A
--   FMSet→FMultiset = fmset.f-extend