{-# OPTIONS --without-K --safe #-}

-- This module provides the basic expression type for polynomials.

module Polynomial.Expr where

open import Data.Nat using (ℕ)
open import Data.Fin using (Fin)

infixl  _⊕_
infixl  _⊗_
infixr  _⊛_
data Expr  {ℓ} (A : Set ℓ) (n : ℕ) : Set ℓ where
  Κ   : A → Expr A n
  Ι   : Fin n → Expr A n
  _⊕_ : Expr A n → Expr A n → Expr A n
  _⊗_ : Expr A n → Expr A n → Expr A n
  _⊛_ : Expr A n → ℕ → Expr A n
  ⊝_  : Expr A n → Expr A n

open import Polynomial.Parameters

module Eval {r₁ r₂ r₃} (homo : Homomorphism r₁ r₂ r₃) where
  open Homomorphism homo
  open import Polynomial.Exponentiation rawRing

  open import Data.Vec as Vec using (Vec)

  ⟦_⟧ : ∀ {n} → Expr Raw.Carrier 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