------------------------------------------------------------------------
-- The Agda standard library
--
-- A solver for equations over monoids
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Algebra.Bundles.Raw using (RawMonoid)

module Algebra.Solver.Monoid.Expression {c } (M : RawMonoid c ) where

open import Data.Fin.Base using (Fin)
open import Data.Nat.Base using ()
open import Data.Vec.Base using (Vec; lookup)
open import Level using (suc; _⊔_)
open import Relation.Binary.Definitions using (DecidableEquality)

open RawMonoid M

private
  variable
    n : 

------------------------------------------------------------------------
-- Monoid expressions

-- There is one constructor for every operation, plus one for
-- variables; there may be at most n variables.

infixr 5 _⊕_

data Expr (n : ) : Set where
  var : Fin n  Expr n
  id  : Expr n
  _⊕_ : Expr n  Expr n  Expr n

-- An environment contains one value for every variable.

Env :   Set _
Env n = Vec Carrier n

-- The semantics of an expression is a function from an environment to
-- a value.

⟦_⟧ : Expr n  Env n  Carrier
 var x    ρ = lookup ρ x
 id       ρ = ε
 e₁  e₂  ρ =  e₁  ρ   e₂  ρ

------------------------------------------------------------------------
-- API for normal expressions

record NormalAPI a : Set (suc a  c  ) where
  infix 5 _≟_

  field

-- The type of normal forms.
    Normal    :   Set a
-- We can decide if two normal forms are /syntactically/ equal.
    _≟_       : DecidableEquality (Normal n)
-- A normaliser.
    normalise : Expr n  Normal n
-- The semantics of a normal form.
    ⟦_⟧⇓      : Normal n  Env n  Carrier
-- The normaliser preserves the semantics of the expression.
    correct   :  e ρ   normalise {n = n} e ⟧⇓ ρ   e  ρ