open import Cubical.Foundations.Prelude

module SignatureAlgebra.Signature (ℓi : Level) where

open import Cubical.Foundations.Structure

open import DCPO ℓi

open import SignatureAlgebra.Monomial ℓi

private
  variable
    ℓd ℓt ℓc ℓmb ℓmc ℓmct ℓv : Level

record PreSignature (ℓc ℓmb ℓmc ℓmct : Level)
    : Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) (ℓ-suc ℓc)) (ℓ-suc ℓmb)) (ℓ-suc ℓmc)) (ℓ-suc ℓmct)) where
  constructor presignature
  field
    constructorNames : Type ℓc
    constructors     : constructorNames → Monomial ℓmb ℓmc ℓmct
open PreSignature public

data Term (Σ : PreSignature ℓc ℓmb ℓmc ℓmct) (V : Type ℓv)
    : Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓc) (ℓ-suc ℓmb)) (ℓ-suc ℓmc)) (ℓ-suc ℓmct)) ℓv) where
  var    : (x : V) → Term Σ V
  constr : (c : constructorNames Σ)
         → (Monomial.B (constructors Σ c) → Term Σ V)
         → ⟨ Monomial.C (constructors Σ c) ⟩
         → Term Σ V

⟦_⟧ₜ : {Σ : PreSignature ℓc ℓmb ℓmc ℓmct} {V : Type ℓv}
     → Term Σ V
     → (D : DCPO ℓd ℓt)
     → ((c : constructorNames Σ) → ⟨ ⟦ constructors Σ c ⟧ₘ D ⟩ → ⟨ D ⟩)
     → (V → ⟨ D ⟩) → ⟨ D ⟩
⟦ var x ⟧ₜ D interpretation ρ = ρ x
⟦ constr cName f c ⟧ₜ D interpretation ρ =
  interpretation cName ((λ b → ⟦ f b ⟧ₜ D interpretation ρ) , c)

record Inequality (Σ : PreSignature ℓc ℓmb ℓmc ℓmct) (ℓv : Level)
    : Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) ℓc) (ℓ-suc ℓmb)) (ℓ-suc ℓmc)) (ℓ-suc ℓmct)) (ℓ-suc ℓv)) where
  constructor inequality
  field
    V : Type ℓv
    lhs : Term Σ V
    rhs : Term Σ V
open Inequality public

record Signature (ℓc ℓmb ℓmc ℓmct ℓe ℓv : Level)
    : Type (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-max (ℓ-suc ℓi) (ℓ-suc ℓc)) (ℓ-suc ℓmb)) (ℓ-suc ℓmc)) (ℓ-suc ℓmct)) (ℓ-suc ℓe)) (ℓ-suc ℓv)) where
  constructor signature
  field
    preSignature    : PreSignature ℓc ℓmb ℓmc ℓmct
    inequalityNames : Type ℓe
    inequalities    : inequalityNames → Inequality preSignature ℓv
  open PreSignature preSignature public
open Signature public