------------------------------------------------------------------------
-- The Agda standard library
--
-- An implementation of the ring solver that requires you to manually
-- pass the equation you wish to solve.
------------------------------------------------------------------------

-- You'll probably want to use `Tactic.RingSolver` instead which uses
-- reflection to automatically extract the equation.

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

open import Tactic.RingSolver.Core.AlmostCommutativeRing

module Tactic.RingSolver.NonReflective
  {ℓ₁ ℓ₂} (ring : AlmostCommutativeRing ℓ₁ ℓ₂)
  (let open AlmostCommutativeRing ring)
  where

open import Algebra.Morphism
open import Function.Base using (id; _⟨_⟩_)
open import Data.Bool.Base using (Bool; true; false; T; if_then_else_)
open import Data.Maybe.Base
open import Data.Empty using (⊥-elim)
open import Data.Nat.Base using ()
open import Data.Product.Base using (_×_; proj₁; proj₂; _,_)
open import Data.Vec.Base using (Vec)
open import Data.Vec.N-ary

open import Tactic.RingSolver.Core.Polynomial.Parameters
open import Tactic.RingSolver.Core.Expression public
open import Algebra.Properties.Semiring.Exp.TCOptimised semiring

module Ops where
  zero-homo :  x  T (is-just (0≟ x))  0#  x
  zero-homo x _ with 0≟ x
  zero-homo x _  | just p = p
  zero-homo x () | nothing

  homo : Homomorphism ℓ₁ ℓ₂ ℓ₁ ℓ₂
  homo = record
    { from = record
      { rawRing = AlmostCommutativeRing.rawRing ring
      ; isZero  = λ x  is-just (0≟ x)
      }
    ; to = record
      { isAlmostCommutativeRing = record
          { isCommutativeSemiring = isCommutativeSemiring
          ; -‿cong       = -‿cong
          ; -‿*-distribˡ = -‿*-distribˡ
          ; -‿+-comm     = -‿+-comm
          }
      }
    ; morphism      = -raw-almostCommutative⟶ ring
    ; Zero-C⟶Zero-R = zero-homo
    }
  open Eval rawRing id public

  open import Tactic.RingSolver.Core.Polynomial.Base (Homomorphism.from homo)

  norm :  {n}  Expr Carrier n  Poly n
  norm (Κ x)   = κ x
  norm (Ι x)   = ι x
  norm (x  y) = norm x  norm y
  norm (x  y) = norm x  norm y
  norm ( x)   =  norm x
  norm (x  i) = norm x  i

  ⟦_⇓⟧ :  {n}  Expr Carrier n  Vec Carrier n  Carrier
   expr ⇓⟧ =  norm expr ⟧ₚ where

    open import Tactic.RingSolver.Core.Polynomial.Semantics homo
      renaming (⟦_⟧ to ⟦_⟧ₚ)

  correct :  {n} (expr : Expr Carrier n) ρ   expr ⇓⟧ ρ   expr  ρ
  correct {n = n} = go
    where
    open import Tactic.RingSolver.Core.Polynomial.Homomorphism homo

    go :  (expr : Expr Carrier n) ρ   expr ⇓⟧ ρ   expr  ρ
    go (Κ x)   ρ = κ-hom x ρ
    go (Ι x)   ρ = ι-hom x ρ
    go (x  y) ρ = ⊞-hom (norm x) (norm y) ρ  trans  (go x ρ  +-cong  go y ρ)
    go (x  y) ρ = ⊠-hom (norm x) (norm y) ρ  trans  (go x ρ  *-cong  go y ρ)
    go ( x)   ρ = ⊟-hom (norm x) ρ    trans  -‿cong (go x ρ)
    go (x  i) ρ = ⊡-hom (norm x) i ρ  trans  ^-congˡ i (go x ρ)

  open import Relation.Binary.Reflection setoid Ι ⟦_⟧ ⟦_⇓⟧ correct public

solve :  (n : ) 
        (f : N-ary n (Expr Carrier n) (Expr Carrier n × Expr Carrier n)) 
        Eqʰ n _≈_ (curryⁿ (Ops.⟦_⇓⟧ (proj₁ (Ops.close n f)))) (curryⁿ (Ops.⟦_⇓⟧ (proj₂ (Ops.close n f)))) 
        Eq  n _≈_ (curryⁿ (Ops.⟦_⟧  (proj₁ (Ops.close n f)))) (curryⁿ (Ops.⟦_⟧  (proj₂ (Ops.close n f))))
solve = Ops.solve
{-# INLINE solve #-}

infixl 6 _⊜_
_⊜_ :  {n : } 
      Expr Carrier n 
      Expr Carrier n 
      Expr Carrier n × Expr Carrier n
_⊜_ = _,_
{-# INLINE _⊜_ #-}