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

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

open import Algebra.Bundles using (Monoid)

module Algebra.Solver.Monoid.Normal {c ℓ} (M : Monoid c ℓ) where

open import Data.Fin.Base using (Fin)
import Data.Fin.Properties as Fin
open import Data.List.Base using (List; [] ; _∷_; _++_)
import Data.List.Relation.Binary.Equality.DecPropositional as ≋
open import Data.Nat.Base using (ℕ)
open import Data.Vec.Base using (lookup)
open import Function.Base using (_∘_; _$_)
open import Relation.Binary.Definitions using (DecidableEquality)
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
import Relation.Nullary.Decidable as Dec using (map; map′)

open Monoid M
open ≈-Reasoning setoid

private
  variable
    n : ℕ


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

open import Algebra.Solver.Monoid.Expression rawMonoid public

------------------------------------------------------------------------
-- Normal forms

-- A normal form is a list of variables.

Normal : ℕ → Set _
Normal n = List (Fin n)

-- The semantics of a normal form.

⟦_⟧⇓ : Normal n → Env n → Carrier
⟦ []     ⟧⇓ ρ = ε
⟦ x ∷ nf ⟧⇓ ρ = lookup ρ x ∙ ⟦ nf ⟧⇓ ρ

-- We can decide if two normal forms are /syntactically/ equal.

infix  _≟_

_≟_ : DecidableEquality (Normal n)
nf₁ ≟ nf₂ = Dec.map′ ≋⇒≡ ≡⇒≋ (nf₁ ≋? nf₂)
  where open ≋ Fin._≟_ using (_≋?_; ≋⇒≡; ≡⇒≋)

-- A normaliser.

normalise : Expr n → Normal n
normalise (var x)   = x ∷ []
normalise id        = []
normalise (e₁ ⊕ e₂) = normalise e₁ ++ normalise e₂

-- The normaliser is homomorphic with respect to _++_/_∙_.

comp-correct : ∀ nf₁ nf₂ (ρ : Env n) →
              ⟦ nf₁ ++ nf₂ ⟧⇓ ρ ≈ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ)
comp-correct [] nf₂ ρ = begin
  ⟦ nf₂ ⟧⇓ ρ      ≈⟨ identityˡ _ ⟨
  ε ∙ ⟦ nf₂ ⟧⇓ ρ  ∎
comp-correct (x ∷ nf₁) nf₂ ρ = begin
  lookup ρ x ∙ ⟦ nf₁ ++ nf₂ ⟧⇓ ρ          ≈⟨ ∙-congˡ (comp-correct nf₁ nf₂ ρ) ⟩
  lookup ρ x ∙ (⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ)  ≈⟨ assoc _ _ _ ⟨
  lookup ρ x ∙ ⟦ nf₁ ⟧⇓ ρ ∙ ⟦ nf₂ ⟧⇓ ρ    ∎

-- The normaliser preserves the semantics of the expression.

correct : ∀ e ρ → ⟦ normalise {n = n} e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ
correct (var x) ρ = begin
  lookup ρ x ∙ ε  ≈⟨ identityʳ _ ⟩
  lookup ρ x      ∎
correct id ρ = begin
  ε  ∎
correct (e₁ ⊕ e₂) ρ = begin
  ⟦ normalise e₁ ++ normalise e₂ ⟧⇓ ρ        ≈⟨ comp-correct (normalise e₁) (normalise e₂) ρ ⟩
  ⟦ normalise e₁ ⟧⇓ ρ ∙ ⟦ normalise e₂ ⟧⇓ ρ  ≈⟨ ∙-cong (correct e₁ ρ) (correct e₂ ρ) ⟩
  ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ                        ∎