\begin{code}
{-# OPTIONS --safe #-}

open import Prelude
open import Data.Vec
open import Signatures
open import FinitenessConditions

--------------------------------------------------------------------------------
-- Equations and theories for computations
--------------------------------------------------------------------------------

module FreeMonad.Theory where

open import FreeMonad.Syntax
private variable 𝔽 : Signature

--------------------------------------------------------------------------------
-- An equation
--------------------------------------------------------------------------------


infix 4 _≐_
record Equation (𝔽 : Signature) (Ξ½ : Type a) : Type a
\end{code}
%<*equation>
\begin{code}
record Equation 𝔽 Ξ½ where
  constructor _≐_
  field lhs rhs : Syntax 𝔽 Ξ½
\end{code}
%</equation>
\begin{code}
open Equation public

βˆ€βΏ : βˆ€ {n} β†’ (βˆ€ {A : Type} β†’ Curryⁿ n (Syntax 𝔽 A) (const (Equation 𝔽 A))) 
   β†’ Equation 𝔽 (Fin n)
βˆ€βΏ {n = n} f = uncurryⁿ {A = Syntax _ (Fin n)} f var

--------------------------------------------------------------------------------
-- A law (equation with the type params as existentials)
--------------------------------------------------------------------------------

record Law (𝔽 : Signature) (β„“ : Level) : Type (β„“suc β„“)
record Law 𝔽 β„“ where
  field  Ξ“  : Type β„“
         Ξ½  : Ξ“ β†’ Type β„“
         eqn : (Ξ³ : Ξ“) β†’ Equation 𝔽 (Ξ½ Ξ³)

--------------------------------------------------------------------------------
-- A theory
--------------------------------------------------------------------------------

record Theory (𝔽 : Signature) (β„“ : Level) : Type (β„“suc β„“)
record Theory 𝔽 β„“ where
  field  Laws  : Type
         Eqns  : Laws β†’ Law 𝔽 β„“

open Theory

_◁≑_ : {β„“ : Level} β†’ (L : Type) β†’ (L β†’ Law 𝔽 β„“) β†’ Theory 𝔽 β„“
(laws ◁≑ eqns) .Laws = laws
(laws ◁≑ eqns) .Eqns = eqns

open Law public

-----------------------------------------------------------------------------------
-- Algebras can "respect" an equation or a full theory
--------------------------------------------------------------------------------

module _ {𝔽 : Signature} {π’ž : Type a} {Ξ½ : Type b} where
  private module RespectsExt where
    infix 3 _Respects_
    _Respects_ : 𝔽 -Alg[ π’ž ] β†’ Equation 𝔽 Ξ½ β†’ Type _
    Ο• Respects lhs ≐ rhs = flip (interp 𝔽 Ο•) lhs ≑ flip (interp 𝔽 Ο•) rhs

  infix 3 _Respects_
  _Respects_ : 𝔽 -Alg[ π’ž ] β†’ Equation 𝔽 Ξ½ β†’ Type _
\end{code}
%<*respects>
\begin{code}
  Ο• Respects (lhs ≐ rhs) = βˆ€ (ρ : Ξ½ β†’ π’ž) β†’ interp 𝔽 Ο• ρ lhs ≑ interp 𝔽 Ο• ρ rhs
\end{code}
%</respects>
\begin{code}
infix 4 _Models_
_Models_ : 𝔽 -Alg[ A ] β†’ Theory 𝔽 b β†’ Type _
\end{code}
%<*in-theory>
\begin{code}
Ο• Models 𝒯 = βˆ€ i Ξ³ β†’ Ο• Respects 𝒯 .Eqns i .eqn Ξ³
\end{code}
%</in-theory>
\begin{code}

module _ {𝔽 : Signature} where
  _-Model[_] : Theory 𝔽 a β†’ Type b β†’ Type _
\end{code}
%<*t-model>
\begin{code}
  𝒯 -Model[ π’ž ] = Ξ£[ Ο• ⦂ 𝔽 -Alg[ π’ž ] ] Γ— Ο• Models 𝒯
\end{code}
%</t-model>
\begin{code}

--------------------------------------------------------------------------------
-- A theory needs to have finitely many variables
--------------------------------------------------------------------------------

FiniteVars : Theory 𝔽 a β†’ _
FiniteVars 𝒯 =
  βˆ€ i β†’
  let law = 𝒯 .Eqns i in
  (Ξ³ : Ξ“ law) β†’
  SplitQuotientedChoiceω (ν law γ)

--------------------------------------------------------------------------------
-- In some cases we need variables to have decidable equality
--------------------------------------------------------------------------------
DiscreteVars : Theory 𝔽 a β†’ _
DiscreteVars 𝒯 =
  βˆ€ i β†’
  let law = 𝒯 .Eqns i in
  (Ξ³ : Ξ“ law) β†’
  Discrete (Ξ½ law Ξ³)
\end{code}