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

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

open import Algebra.Bundles using (Monoid)
import Algebra.Solver.Monoid.Expression as Expression

module Algebra.Solver.Monoid.Solver {a c ℓ} (M : Monoid c ℓ)
  (open Monoid M using (rawMonoid; setoid; _≈_))
  (open Expression rawMonoid using (Expr; Env; var; ⟦_⟧; NormalAPI))
  (N : NormalAPI a) where

open import Data.Maybe.Base as Maybe
  using (Maybe; From-just; from-just)
open import Data.Nat.Base using (ℕ)
open import Function.Base using (_∘_; _$_)
open import Relation.Binary.Consequences using (dec⇒weaklyDec)
open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
import Relation.Binary.Reflection as Reflection

open NormalAPI N

private
  variable
    n : ℕ
  module
    R = Reflection setoid var ⟦_⟧ (⟦_⟧⇓ ∘ normalise) correct


------------------------------------------------------------------------
-- Proof procedures

-- Re-export the existing solver machinery from `Reflection`

open R public
  using (solve; _⊜_)

-- We can also give a sound, but not necessarily complete, procedure
-- for determining if two expressions have the same semantics.

prove′ : ∀ e₁ e₂ → Maybe ((ρ : Env n) → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ)
prove′ e₁ e₂ = Maybe.map lemma $ dec⇒weaklyDec _≟_ (normalise e₁) (normalise e₂)
  where
  open import Relation.Binary.Reasoning.Setoid setoid
  lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
  lemma eq ρ = R.prove ρ e₁ e₂ $ begin
    ⟦ normalise e₁ ⟧⇓ ρ  ≡⟨ cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩
    ⟦ normalise e₂ ⟧⇓ ρ  ∎

-- This procedure can then be combined with from-just.

prove : ∀ n (e₁ e₂ : Expr n) → From-just (prove′ e₁ e₂)
prove _ e₁ e₂ = from-just $ prove′ e₁ e₂