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