------------------------------------------------------------------------
-- 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  _⊕_
infixl  _⊗_
infixr  _⊛_
infix  ⊝_

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
  ⟦ Κ x   ⟧ ρ = ⟦ x ⟧ᵣ
  ⟦ Ι x   ⟧ ρ = Vec.lookup ρ x
  ⟦ x ⊕ y ⟧ ρ = ⟦ x ⟧ ρ + ⟦ y ⟧ ρ
  ⟦ x ⊗ y ⟧ ρ = ⟦ x ⟧ ρ * ⟦ y ⟧ ρ
  ⟦   ⊝ x ⟧ ρ = - ⟦ x ⟧ ρ
  ⟦ x ⊛ i ⟧ ρ = ⟦ x ⟧ ρ ^′ i