------------------------------------------------------------------------
-- The Agda standard library
--
-- A type for expressions over a raw ring.
------------------------------------------------------------------------

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

module Tactic.RingSolver.Core.Expression where

open import Data.Nat.Base using (ℕ)
open import Data.Fin.Base using (Fin)
open import Data.Vec.Base as Vec using (Vec)

open import Algebra

infixl 6 _⊕_
infixl 7 _⊗_
infixr 8 _⊛_
infix 8 ⊝_

data Expr {a} (A : Set a) (n : ℕ) : Set a where
  Κ   : A → Expr A n                   -- Constant
  Ι   : Fin n → Expr A n               -- Variable
  _⊕_ : Expr A n → Expr A n → Expr A n -- Addition
  _⊗_ : Expr A n → Expr A n → Expr A n -- Multiplication
  _⊛_ : Expr A n → ℕ → Expr A n        -- Exponentiation
  ⊝_  : Expr A n → Expr A n            -- Negation


module Eval
  {ℓ₁ ℓ₂} (rawRing : RawRing ℓ₁ ℓ₂)
  (open RawRing rawRing)
  {a} {A : Set a} (⟦_⟧ᵣ : A → Carrier) where

  open import Algebra.Definitions.RawSemiring rawSemiring
    using (_^′_)

  ⟦_⟧ : ∀ {n} → Expr A n → Vec Carrier n → Carrier
  $\begin{pmatrix} \,\href{Tactic.RingSolver.Core.Expression.html#558}{\htmlId{1126}{\htmlClass{InductiveConstructor}{\text{Κ}}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#1128}{\htmlId{1128}{\htmlClass{Bound}{\text{x}}}}\,   \end{pmatrix}$ ρ = $\begin{pmatrix} \,\href{Tactic.RingSolver.Core.Expression.html#1128}{\htmlId{1140}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$
  $\begin{pmatrix} \,\href{Tactic.RingSolver.Core.Expression.html#609}{\htmlId{1149}{\htmlClass{InductiveConstructor}{\text{Ι}}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#1151}{\htmlId{1151}{\htmlClass{Bound}{\text{x}}}}\,   \end{pmatrix}$ ρ = Vec.lookup ρ x
  $\begin{pmatrix} \,\href{Tactic.RingSolver.Core.Expression.html#1180}{\htmlId{1180}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#660}{\htmlId{1182}{\htmlClass{InductiveConstructor Operator}{\text{⊕}}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#1184}{\htmlId{1184}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ρ = $\begin{pmatrix} \,\href{Tactic.RingSolver.Core.Expression.html#1180}{\htmlId{1194}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ρ + $\begin{pmatrix} \,\href{Tactic.RingSolver.Core.Expression.html#1184}{\htmlId{1204}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ρ
  $\begin{pmatrix} \,\href{Tactic.RingSolver.Core.Expression.html#1214}{\htmlId{1214}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#711}{\htmlId{1216}{\htmlClass{InductiveConstructor Operator}{\text{⊗}}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#1218}{\htmlId{1218}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ρ = $\begin{pmatrix} \,\href{Tactic.RingSolver.Core.Expression.html#1214}{\htmlId{1228}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ρ * $\begin{pmatrix} \,\href{Tactic.RingSolver.Core.Expression.html#1218}{\htmlId{1238}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ρ
  $\begin{pmatrix}   \,\href{Tactic.RingSolver.Core.Expression.html#825}{\htmlId{1250}{\htmlClass{InductiveConstructor Operator}{\text{⊝}}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#1252}{\htmlId{1252}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ρ = - $\begin{pmatrix} \,\href{Tactic.RingSolver.Core.Expression.html#1252}{\htmlId{1264}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ρ
  $\begin{pmatrix} \,\href{Tactic.RingSolver.Core.Expression.html#1274}{\htmlId{1274}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#768}{\htmlId{1276}{\htmlClass{InductiveConstructor Operator}{\text{⊛}}}}\, \,\href{Tactic.RingSolver.Core.Expression.html#1278}{\htmlId{1278}{\htmlClass{Bound}{\text{i}}}}\, \end{pmatrix}$ ρ = $\begin{pmatrix} \,\href{Tactic.RingSolver.Core.Expression.html#1274}{\htmlId{1288}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ρ ^′ i