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