```
module Expr where

open import Data.Nat
open import Data.Function using (_∘_)
open import Basics

infix  20 _==_
infixr 40 _⊕_
infixr 60 _⊗_

data Expr n : Set where
var  : (i : Fin n) → Expr n
_⊕_  : (a b : Expr n) → Expr n
zero : Expr n

data Eqn n : Set where
_==_ : (a b : Expr n) → Eqn n

NF : ℕ → Set
NF n = Vec ℕ n

const : ∀ {n A} → A → Vec A n
const x = tabulate (λ _ → x)

unit : ∀ {n} → Fin n → NF n
unit zero    = 1 ∷ const 0
unit (suc i) = 0 ∷ unit i

eval : ∀ {n} → Expr n → NF n
eval (var i) = unit i
eval (a ⊕ b) = zipWith _+_ (eval a) (eval b)
eval zero    = const 0

_⊗_ : ∀ {n} → ℕ → Expr n → Expr n
zero  ⊗ a = zero
suc n ⊗ a = a ⊕ (n ⊗ a)

Σ : ∀ {n m} → Vec (Expr n) m → Expr n
Σ []       = zero
Σ (x ∷ xs) = x ⊕ Σ xs

poly : ∀ {n m} → Vec ℕ m → Vec (Expr n) m → Expr n
poly ks as = Σ (zipWith _⊗_ ks as)

vars : ∀ {n} → Vec (Expr n) n
vars = tabulate var

reify : ∀ {n} → NF n → Expr n
reify nf = poly nf vars

norm : ∀ {n} → Expr n → Expr n
norm = reify ∘ eval

normEqn : ∀ {n} → Eqn n → Eqn n
normEqn (a == b) = norm a == norm b

-- Example

expr₁ : Expr 3
expr₁ = var zero ⊕ (var (suc zero) ⊕ var zero)

open import Data.Vec.N-ary

build : ∀ {A}(n : ℕ) → N-ary n (Expr n) A → A
build n f = f \$ⁿ vars {n}

expr₂ = build 3 λ a b c → a ⊕ (b ⊕ a)

eqn₁ = build 4 λ a b c d →
(a ⊕ b) ⊕ (c ⊕ d) == (a ⊕ c) ⊕ (b ⊕ d)

```