module AlgebraicSignature where

open import InitialAlgebra public
open import Prelude public
open import Size

----------------------------------------------------------------------
-- Algebraic signatures
----------------------------------------------------------------------
record Sig : Set₁ where
  constructor mkSig
  field
    Op : Set
    Ar : Op → Set

open Sig public

-- Associated W-type
data 𝕎 (Σ : Sig) : Set where
  sup : (a : Op Σ) → (Ar Σ a → 𝕎 Σ) → 𝕎 Σ

-- Sum of signatures
infixr  _⊕_
_⊕_ : Sig → Sig → Sig
Op (Σ ⊕ Σ')         = Op Σ ⊎ Op Σ'
Ar (Σ ⊕ Σ') (ι₁ a)  = Ar Σ a
Ar (Σ ⊕ Σ') (ι₂ a') = Ar Σ' a'

⨁ : (A : Set)(B : A → Sig) → Sig
Op (⨁ A Σ)         = ∑ x ∶ A , Op (Σ x)
Ar (⨁ A Σ) (x , a) = Ar (Σ x) a

syntax ⨁ A (λ x → Σ) = ⨁ x ∶ A , Σ

-- Empty signature
emp : Sig
Op emp = 𝟘
Ar emp ()

-- Signature with a constant and a  binary operation
bin : Sig
Op bin       = 𝔹
Ar bin false = 𝟘
Ar bin true  = 𝔹

----------------------------------------------------------------------
-- Σ-filtered sizes
----------------------------------------------------------------------
record Filtered
  (Σ : Sig)
  (κ : Set)
  {{_ : Size κ}}
  : -------------
  Set₁
  where
  field
    ⨆ˢ  : (a : Op Σ)(f : Ar Σ a → κ) → κ
    <⨆ˢ :
      {a : Op Σ}
      (f : Ar Σ a → κ)
      (x : Ar Σ a)
      → --------------
      f x < ⨆ˢ a f

  <ᵇ⨆ˢ :
    {a : Op Σ}
    (f : Ar Σ a → κ)
    (x : Ar Σ a)
    → --------------
    f x <ᵇ ⨆ˢ a f
  <ᵇ⨆ˢ f x = <inst (<⨆ˢ f x)

open Filtered{{...}} public

-- Filteredness for an indexed sum of signatures implies filteredness
-- for each signature
Filtered⨁ :
  (κ : Set)
  {{_ : Size κ}}
  (A : Set)
  (Σ : A → Sig)
  {{_ : Filtered (⨁ A Σ) κ}}
  (x : A)
  → ------------------------
  Filtered (Σ x) κ
⨆ˢ {{Filtered⨁ _ _ _ x}} a = ⨆ˢ (x , a)
<⨆ˢ{{Filtered⨁ _ _ _ _}}   = <⨆ˢ

-- Filteredness for a binary sum of signatures implies filteredness
-- for each signature
Filtered⊕l :
  (κ : Set)
  {{_ : Size κ}}
  (Σ Σ' : Sig)
  {{_ : Filtered (Σ ⊕ Σ') κ}}
  → -------------------------
  Filtered Σ κ
⨆ˢ   {{Filtered⊕l _ _ _}} a = ⨆ˢ (ι₁ a)
<⨆ˢ  {{Filtered⊕l _ _ _}}   = <⨆ˢ

Filtered⊕r :
  (κ : Set)
  {{_ : Size κ}}
  (Σ Σ' : Sig)
  {{_ : Filtered (Σ ⊕ Σ') κ}}
  → -------------------------
  Filtered Σ' κ
⨆ˢ  {{Filtered⊕r _ _ _}} a = ⨆ˢ (ι₂ a)
<⨆ˢ {{Filtered⊕r _ _ _}}   = <⨆ˢ

----------------------------------------------------------------------
-- Plump order
----------------------------------------------------------------------
module _ {Σ : Sig} where
  infix  _≼_ _≺_
  mutual
    data _≼_ : 𝕎 Σ → 𝕎 Σ → Prop where
      sup≼ :
        {a   : Op Σ}
        {f   : Ar Σ a → 𝕎 Σ}
        {i   : 𝕎 Σ}
        (f<i : ∀ x → f x ≺ i)
        → ------------------
        sup a f ≼ i
    data _≺_ : 𝕎 Σ → 𝕎 Σ → Prop where
      ≺sup :
        {a    : Op Σ}
        {f    : Ar Σ a → 𝕎 Σ}
        (x    : Ar Σ a)
        {i    : 𝕎 Σ}
        (i≼fx : i ≼ f x)
        → -------------------
        i ≺ sup a f

    -- ≼ is reflexive
    ≼refl : ∀ i → i ≼ i
    ≼refl (sup _ f) = sup≼ λ x → ≺sup x (≼refl (f x))

  -- Transitivity
  mutual
    ≼≼ : ∀{i j k} → j ≼ k → i ≼ j → i ≼ k
    ≼≼ j≼k (sup≼ f≺i) = sup≼ λ x → ≼≺ j≼k (f≺i x)

    ≼≺  : ∀{i j k} → j ≼ k → i ≺ j → i ≺ k
    ≼≺ (sup≼ f≺i) (≺sup x i≼fx) = ≺≼ (f≺i x) i≼fx

    ≺≼ : ∀{i j k } → j ≺ k → i ≼ j → i ≺ k
    ≺≼ (≺sup x i≼fx) i≼j = ≺sup x (≼≼ i≼fx i≼j)

  ≺→≼ : ∀{i j} → i ≺ j → i ≼ j
  ≺→≼ (≺sup x (sup≼ f≺i)) = sup≼ (λ y → ≺sup x (≺→≼ (f≺i y)))

  ≺≺ : ∀{i j k} → j ≺ k → i ≺ j → i ≺ k
  ≺≺ (≺sup x i≼fx) i≺j = ≺sup x (≺→≼ (≼≺ i≼fx i≺j))

  -- Well-foundedness of ≺
  ≺iswf : wf.iswf _≺_
  ≺iswf i = wf.acc λ j j≺i → α i j (≺→≼ j≺i)
    where
    α : ∀ i j → j ≼ i → wf.Acc _≺_ j
    α (sup _ f) j j≼i = wf.acc α'
      where
      α' : ∀ k → k ≺ j → wf.Acc _≺_ k
      α' k k≺j with ≼≺ j≼i k≺j
      ... | ≺sup x k≼fx = α (f x) k k≼fx

plump : Sig → Set
plump Σ = 𝕎 (bin ⊕ Σ)

instance
  SizePlump : {Σ : Sig} → Size (plump Σ)
  _<_   {{thin{{SizePlump{Σ}}}}} = _≺_
  <<    {{thin{{SizePlump{Σ}}}}} = ≺≺
  Oˢ    {{SizePlump{Σ}}}         = sup (ι₁ false) λ()
  _⊔ˢ_  {{SizePlump{Σ}}} i j     = sup (ι₁ true) λ{true → i ; false → j}
  <⊔ˢl  {{SizePlump{Σ}}}         = ≺sup true (≼refl _)
  <⊔ˢr  {{SizePlump {Σ}}}        = ≺sup false (≼refl _)
  <iswf {{SizePlump {Σ}}}        = ≺iswf

  FilteredPlump : {Σ : Sig} → Filtered Σ (plump Σ)
  ⨆ˢ  {{FilteredPlump}} a f = sup (ι₂ a) f
  <⨆ˢ {{FilteredPlump}} f x = ≺sup x (≼refl (f x))