{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Bundles.Raw using (RawMonoid)
module Algebra.Solver.Monoid.Expression {c ℓ} (M : RawMonoid c ℓ) where
open import Data.Fin.Base using (Fin)
open import Data.Nat.Base using (ℕ)
open import Data.Vec.Base using (Vec; lookup)
open import Level using (suc; _⊔_)
open import Relation.Binary.Definitions using (DecidableEquality)
open RawMonoid M
private
variable
n : ℕ
infixr 5 _⊕_
data Expr (n : ℕ) : Set where
var : Fin n → Expr n
id : Expr n
_⊕_ : Expr n → Expr n → Expr n
Env : ℕ → Set _
Env n = Vec Carrier n
⟦_⟧ : Expr n → Env n → Carrier
⟦ var x ⟧ ρ = lookup ρ x
⟦ id ⟧ ρ = ε
⟦ e₁ ⊕ e₂ ⟧ ρ = ⟦ e₁ ⟧ ρ ∙ ⟦ e₂ ⟧ ρ
record NormalAPI a : Set (suc a ⊔ c ⊔ ℓ) where
infix 5 _≟_
field
Normal : ℕ → Set a
_≟_ : DecidableEquality (Normal n)
normalise : Expr n → Normal n
⟦_⟧⇓ : Normal n → Env n → Carrier
correct : ∀ e ρ → ⟦ normalise {n = n} e ⟧⇓ ρ ≈ ⟦ e ⟧ ρ