    ------------------------------------------------------------------------
    -- 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.Base using (_⟨_⟩_)

    open import Data.Bool.Base    as Bool    using (Bool; _∨_; if_then_else_)
    open import Data.Maybe.Base   as Maybe   using (Maybe; just; nothing; maybe)
    open import Data.List.Base    as List    using (List; _∷_; [])
    open import Data.Nat.Base     as ℕ       using (ℕ; suc; zero)
    open import Data.Product.Base 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 ≈-Reasoning

    ------------------------------------------------------------------------
    -- 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 ≈-Reasoning 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