module Expr where

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

infix   _==_
infixr  _⊕_
infixr  _⊗_

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    =  ∷ const 
unit (suc i) =  ∷ unit i

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

_⊗_ : ∀ {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 
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  λ a b c → a ⊕ (b ⊕ a)

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