```------------------------------------------------------------------------
-- The Agda standard library
--
-- Reflection-based solver for monoid equalities
------------------------------------------------------------------------
--
-- This solver automates the construction of proofs of equivalences
-- between monoid expressions.
-- When called like so:
--
--   proof : ∀ x y z → (x ∙ y) ∙ z ≈ x ∙ (y ∙ z) ∙ ε
--   proof x y z = solve mon
--
-- The following diagram describes what happens under the hood:
--
--            ┌▸x ∙ (y ∙ (z ∙ ε)) ════ x ∙ (y ∙ (z ∙ ε))◂┐
--            │         ║                      ║         │
--            │         ║                      ║         │
--          [_⇓]        ║                      ║        [_⇓]
--          ╱           ║                      ║          ╲
--         ╱            ║                      ║           ╲
-- (x ∙′ y) ∙′ z      homo                   homo    x ∙′ (y ∙′ z) ∙′ ε′
--   ▴     ╲            ║                      ║           ╱       ▴
--   │      ╲           ║                      ║          ╱        │
--   │       [_↓]       ║                      ║        [_↓]       │
--   │        │         ║                      ║         │         │
--   │        │         ║                      ║         │         │
--   │        └───▸(x ∙ y) ∙ z          x ∙ (y ∙ z) ∙ ε◂─┘         │
--   │                  │                      │                   │
--   │                  │                      │                   │
--   └────reflection────┘                      └───reflection──────┘
--
-- The actual output—the proof constructed by the solver—is represented
-- by the double-lined path (══).
--
-- We start at the bottom, with our two expressions.
-- Through reflection, we convert these two expressions to their AST
-- representations, in the Expr type.
-- We then can evaluate the AST in two ways: one simply gives us back
-- the two expressions we put in ([_↓]), and the other normalises
-- ([_⇓]).
-- We use the homo function to prove equivalence between these two
-- forms: joining up these two proofs gives us the desired overall
-- proof.

-- Note: What's going on with the Monoid parameter?
--
-- This module is not parameterised over a monoid, which is contrary
-- to what you might expect. Instead, we take the monoid record as an
-- argument to the solve macro, and then pass it around as an
-- argument wherever we need it.
--
-- We need to get the monoid record at the call site, not the import
-- site, to ensure that it's consistent with the rest of the context.
-- For instance, if we wanted to produce `x ∙ y` using the monoid record
-- as imported, we would run into problems:
-- * If we tried to just reflect on the expression itself
--   (quoteTerm (x ∙ y)) we would likely get some de Bruijn indices
--   wrong (in x and y), and ∙ might not even be in scope where the
--   user wants us to solve! If they're solving an expression like
--   x + (y + z), they can pass in the +-0-monoid, but don't have to
--   open it themselves.
-- * If instead we tried to construct a term which accesses the _∙_
--   field on the reflection of the record, we'd run into similar
--   problems again. While the record is a parameter for us, it might
--   not be for the user.
-- Basically, we need the Monoid we're looking at to be exactly the
-- same as the one the user is looking at, and in order to do that we
-- quote it at the call site.

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

module Tactic.MonoidSolver where

open import Algebra
open import Function

open import Data.Bool    as Bool    using (Bool; _∨_; if_then_else_)
open import Data.Maybe   as Maybe   using (Maybe; just; nothing; maybe)
open import Data.List    as List    using (List; _∷_; [])
open import Data.Nat     as ℕ       using (ℕ; suc; zero)
open import Data.Product as Product using (_×_; _,_)

open import Reflection.AST
open import Reflection.AST.Term
open import Reflection.AST.Argument
import Reflection.AST.Name as Name
open import Reflection.TCM
open import Reflection.TCM.Syntax

import Relation.Binary.Reasoning.Setoid as SetoidReasoning

----------------------------------------------------------------------
-- The Expr type with homomorphism proofs
----------------------------------------------------------------------

infixl 7 _∙′_
data Expr {a} (A : Set a) : Set a where
_∙′_  : Expr A → Expr A → Expr A
ε′    : Expr A
[_↑]  : A → Expr A

module _ {m₁ m₂} (monoid : Monoid m₁ m₂) where

open Monoid monoid
open SetoidReasoning setoid

-- Convert the AST to an expression (i.e. evaluate it) without
-- normalising.
[_↓] : Expr Carrier → Carrier
[ x ∙′ y  ↓] = [ x ↓] ∙ [ y ↓]
[ ε′      ↓] = ε
[ [ x ↑]  ↓] = x

-- Convert an AST to an expression (i.e. evaluate it) while
-- normalising.
--
-- This first function actually converts an AST to the Cayley
-- representation of the underlying monoid.
-- This obeys the monoid laws up to beta-eta equality, which is the
-- property which gives us the "normalising" behaviour we want.
[_⇓]′ : Expr Carrier → Carrier → Carrier
[ x ∙′ y  ⇓]′ z = [ x ⇓]′ ([ y ⇓]′ z)
[ ε′      ⇓]′ y = y
[ [ x ↑]  ⇓]′ y = x ∙ y

[_⇓] : Expr Carrier → Carrier
[ x ⇓] = [ x ⇓]′ ε

homo′ : ∀ x y → [ x ⇓] ∙ y ≈ [ x ⇓]′ y
homo′ ε′ y       = identityˡ y
homo′ [ x ↑] y   = ∙-congʳ (identityʳ x)
homo′ (x ∙′ y) z = begin
[ x ∙′ y ⇓] ∙ z       ≡⟨⟩
[ x ⇓]′ [ y ⇓] ∙ z    ≈˘⟨ ∙-congʳ (homo′ x [ y ⇓]) ⟩
([ x ⇓] ∙ [ y ⇓]) ∙ z ≈⟨ assoc [ x ⇓] [ y ⇓] z ⟩
[ x ⇓] ∙ ([ y ⇓] ∙ z) ≈⟨ ∙-congˡ (homo′ y z) ⟩
[ x ⇓] ∙ ([ y ⇓]′ z)  ≈⟨ homo′ x ([ y ⇓]′ z) ⟩
[ x ⇓]′ ([ y ⇓]′ z)   ∎

homo : ∀ x → [ x ⇓] ≈ [ x ↓]
homo ε′       = refl
homo [ x ↑]   = identityʳ x
homo (x ∙′ y) = begin
[ x ∙′ y ⇓]     ≡⟨⟩
[ x ⇓]′ [ y ⇓]  ≈˘⟨ homo′ x [ y ⇓] ⟩
[ x ⇓] ∙ [ y ⇓] ≈⟨ ∙-cong (homo x) (homo y) ⟩
[ x ↓] ∙ [ y ↓] ∎

----------------------------------------------------------------------
-- Helpers for reflection
----------------------------------------------------------------------

getArgs : Term → Maybe (Term × Term)
getArgs (def _ xs) = go xs
where
go : List (Arg Term) → Maybe (Term × Term)
go (vArg x ∷ vArg y ∷ []) = just (x , y)
go (x ∷ xs)               = go xs
go _                      = nothing
getArgs _ = nothing

----------------------------------------------------------------------
-- Getting monoid names
----------------------------------------------------------------------

-- We try to be flexible here, by matching two kinds of names.
-- The first is the field accessor for the monoid record itself.
-- However, users will likely want to use the solver with
-- expressions like:
--
--   xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
--
-- So we also evaluate the field accessor to find functions like ++.

record MonoidNames : Set where
field
is-∙ : Name → Bool
is-ε : Name → Bool

buildMatcher : Name → Maybe Name → Name → Bool
buildMatcher n nothing  x = n Name.≡ᵇ x
buildMatcher n (just m) x = n Name.≡ᵇ x ∨ m Name.≡ᵇ x

findMonoidNames : Term → TC MonoidNames
findMonoidNames mon = do
∙-altName ← normalise (def (quote Monoid._∙_) (2 ⋯⟅∷⟆ mon ⟨∷⟩ []))
ε-altName ← normalise (def (quote Monoid.ε)   (2 ⋯⟅∷⟆ mon ⟨∷⟩ []))
pure record
{ is-∙ = buildMatcher (quote Monoid._∙_) (getName ∙-altName)
; is-ε = buildMatcher (quote Monoid.ε)   (getName ε-altName)
}

----------------------------------------------------------------------
-- Building Expr
----------------------------------------------------------------------

-- We now define a function that takes an AST representing the LHS
-- or RHS of the equation to solve and converts it into an AST
-- respresenting the corresponding Expr.

″ε″ : Term
″ε″ = quote ε′ ⟨ con ⟩ []

[_↑]′ : Term → Term
[ t ↑]′ = quote [_↑] ⟨ con ⟩ (t ⟨∷⟩ [])

module _ (names : MonoidNames) where

open MonoidNames names

mutual
″∙″ : List (Arg Term) → Term
″∙″ (x ⟨∷⟩ y ⟨∷⟩ []) = quote _∙′_ ⟨ con ⟩ buildExpr x ⟨∷⟩ buildExpr y ⟨∷⟩ []
″∙″ (x ∷ xs)         = ″∙″ xs
″∙″ _                = unknown

buildExpr : Term → Term
buildExpr t@(def n xs) =
if is-∙ n
then ″∙″ xs
else if is-ε n
then ″ε″
else
[ t ↑]′
buildExpr t@(con n xs) =
if is-∙ n
then ″∙″ xs
else if is-ε n
then ″ε″
else [ t ↑]′
buildExpr t = quote [_↑] ⟨ con ⟩ (t ⟨∷⟩ [])

----------------------------------------------------------------------
-- Constructing the solution
----------------------------------------------------------------------

-- This function joins up the two homomorphism proofs. It constructs
-- a proof of the following form:
--
--   trans (sym (homo x)) (homo y)
--
-- where x and y are the Expr representations of each side of the
-- goal equation.

constructSoln : Term → MonoidNames → Term → Term → Term
constructSoln mon names lhs rhs =
quote Monoid.trans ⟨ def ⟩ 2 ⋯⟅∷⟆ mon ⟨∷⟩
(quote Monoid.sym ⟨ def ⟩ 2 ⋯⟅∷⟆ mon ⟨∷⟩
(quote homo ⟨ def ⟩ 2 ⋯⟅∷⟆ mon ⟨∷⟩ buildExpr names lhs ⟨∷⟩ []) ⟨∷⟩ [])
⟨∷⟩
(quote homo ⟨ def ⟩ 2 ⋯⟅∷⟆ mon ⟨∷⟩ buildExpr names rhs ⟨∷⟩ []) ⟨∷⟩
[]

----------------------------------------------------------------------
-- Macro
----------------------------------------------------------------------

solve-macro : Term → Term → TC _
solve-macro mon hole = do
hole′ ← inferType hole >>= normalise
names ← findMonoidNames mon
just (lhs , rhs) ← pure (getArgs hole′)
where nothing → typeError (termErr hole′ ∷ [])
let soln = constructSoln mon names lhs rhs
unify hole soln

macro
solve : Term → Term → TC _
solve = solve-macro
```