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