open import Algebra

module Semantics (CM : CommutativeMonoid) where

open import Basics
open import Expr
open CommutativeMonoid CM
  renaming (carrier to C; setoid to C-setoid)
open import Relation.Binary.PropositionalEquality
  hiding (sym; trans)
  renaming (refl to ≡-refl)

import Relation.Binary.EqReasoning as EqR
  renaming (_≈⟨_⟩_ to _≈<_>_; _≡⟨_⟩_ to _≡<_>_)

open EqR C-setoid

Env : ℕ → Set
Env n = Vec C n

[_] : ∀ {n} → Expr n → Env n → C
[ var i ] ρ = ρ ! i
[ a ⊕ b ] ρ = [ a ] ρ ∙ [ b ] ρ
[ zero  ] ρ = ε

[∣_∣] : ∀ {n} → Eqn n → Env n → Set
[∣ a == b ∣] ρ = [ a ] ρ ≈ [ b ] ρ

_≅_ : ∀ {n} → Expr n → Expr n → Set
a ≅ b = ∀ ρ → [ a ] ρ ≈ [ b ] ρ

-- Soundness

open import Data.Product

sound-zero : ∀ {n m} (es : Vec (Expr m) n) →
             zero ≅ poly (const ) es
sound-zero {zero}  []       ρ = refl
sound-zero {suc n} (_ ∷ es) ρ = 
  begin
    ε
      ≈< sym (proj₁ identity _) >
    ε ∙ ε
      ≈< ∙-pres-≈ refl (sound-zero es ρ) >
    ε ∙ [ poly (const ) es ] ρ
  ∎

distr : ∀ {n} k j (e : Expr n) → k ⊗ e ⊕ j ⊗ e ≅ (k + j) ⊗ e
distr zero    j e ρ = proj₁ identity _
distr (suc k) j e ρ =
  begin
    [ (e ⊕ k ⊗ e) ⊕ j ⊗ e ] ρ
      ≈< assoc _ _ _ >
    [ e ⊕ (k ⊗ e ⊕ j ⊗ e) ] ρ
      ≈< ∙-pres-≈ refl (distr k j e ρ) >
    [ e ⊕ (k + j) ⊗ e ] ρ
  ∎

sound-plus : ∀ {n m} (ks js : Vec ℕ n) (xs : Vec (Expr m) n) →
             poly ks xs ⊕ poly js xs ≅
             poly (zipWith _+_ ks js) xs
sound-plus [] [] [] ρ = proj₁ identity _
sound-plus (k ∷ ks) (j ∷ js) (x ∷ xs) ρ =
  begin
    [ (k ⊗ x ⊕ poly ks xs) ⊕ (j ⊗ x ⊕ poly js xs) ] ρ
      ≈< shuffle (k ⊗ x) (poly ks xs) (j ⊗ x) (poly js xs) ρ >
    [ (k ⊗ x ⊕ j ⊗ x) ⊕ (poly ks xs ⊕ poly js xs) ] ρ
      ≈< ∙-pres-≈ (distr k j x ρ) (sound-plus ks js xs ρ) >
    [ (k + j) ⊗ x ⊕ poly (zipWith _+_ ks js) xs ] ρ
  ∎
  where
    shuffle : ∀ {n} (a b c d : Expr n) →
              (a ⊕ b) ⊕ (c ⊕ d) ≅ (a ⊕ c) ⊕ (b ⊕ d)
    shuffle a b c d ρ =
      begin
        [ (a ⊕ b) ⊕ (c ⊕ d) ] ρ
          ≈< assoc _ _ _ >
        [ a ⊕ (b ⊕ (c ⊕ d)) ] ρ
          ≈< ∙-pres-≈ refl (sym (assoc _ _ _)) >
        [ a ⊕ ((b ⊕ c) ⊕ d) ] ρ
          ≈< ∙-pres-≈ refl (∙-pres-≈ (comm _ _) refl) >
        [ a ⊕ ((c ⊕ b) ⊕ d) ] ρ
          ≈< ∙-pres-≈ refl (assoc _ _ _) >
        [ a ⊕ (c ⊕ (b ⊕ d)) ] ρ
          ≈< sym (assoc _ _ _) >
        [ (a ⊕ c) ⊕ (b ⊕ d) ] ρ
      ∎

sound-var : ∀ {n m} (i : Fin n) (es : Vec (Expr m) n) →
            (es ! i) ≅ poly (unit i) es
sound-var zero (e ∷ es) ρ =
  begin
    [ e ] ρ
      ≈< sym (proj₂ identity _) >
    [ e ⊕ zero ] ρ
      ≈< sym (proj₂ identity _) >
    [ (e ⊕ zero) ⊕ zero ] ρ
      ≈< ∙-pres-≈ refl (sound-zero es ρ) >
    [ (e ⊕ zero) ⊕ poly (const ) es ] ρ
  ∎
sound-var (suc i) (e ∷ es) ρ =
  begin
    [ es ! i ] ρ
      ≈< sound-var i es ρ >
    [ poly (unit i) es ] ρ
      ≈< sym (proj₁ identity _) >
    [ zero ⊕ poly (unit i) es ] ρ
  ∎

sound : ∀ {n} (e : Expr n) → e ≅ norm e
sound (var i) ρ =
  begin
    [ var i ] ρ
      ≡< cong (λ e → [ e ] ρ) (lem-tabulate-! var i) >
    [ vars ! i ] ρ
      ≈< sound-var i vars ρ >
    [ norm (var i) ] ρ
  ∎
sound (a ⊕ b) ρ =
  begin
    [ a ⊕ b ] ρ
      ≈< ∙-pres-≈ (sound a ρ) (sound b ρ) >
    [ norm a ⊕ norm b ] ρ
      ≈< sound-plus (eval a) (eval b) vars ρ >
    [ norm (a ⊕ b) ] ρ
  ∎
sound zero    ρ = sound-zero vars ρ


-- sound : ∀ {n}(a : Expr n) → a ≅ norm a
-- sound a ρ = {!!}

prove : ∀ {n}(eq : Eqn n) ρ → [∣ normEqn eq ∣] ρ → [∣ eq ∣] ρ
prove (a == b) ρ prf =
  begin
    [ a ] ρ
      ≈< sound a ρ >
    [ norm a ] ρ
      ≈< prf >
    [ norm b ] ρ
      ≈< sym (sound b ρ) >
    [ b ] ρ
  ∎