------------------------------------------------------------------------
-- 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