1 files changed, 85 insertions, 11 deletions
diff --git a/Data/System/Values.agda b/Data/System/Values.agda
index bf8fa38..737e34e 100644
--- a/Data/System/Values.agda
+++ b/Data/System/Values.agda
@@ -1,21 +1,95 @@
 {-# OPTIONS --without-K --safe #-}
 
-module Data.System.Values (A : Set) where
+open import Algebra.Bundles using (CommutativeMonoid)
+open import Level using (0ℓ)
+
+module Data.System.Values (A : CommutativeMonoid 0ℓ 0ℓ) where
+
+import Algebra.Properties.CommutativeMonoid.Sum as Sum
+import Data.Vec.Functional.Properties as VecProps
+import Relation.Binary.PropositionalEquality as ≡
 
-open import Data.Nat.Base using (ℕ)
-open import Data.Vec.Functional using (Vector)
+open import Data.Fin using (_↑ˡ_; _↑ʳ_; zero; suc)
+open import Data.Nat using (ℕ; _+_; suc)
+open import Data.Product using (_,_)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
+open import Data.Setoid using (∣_∣)
+open import Data.Vec.Functional as Vec using (Vector; zipWith; replicate)
+open import Data.Vec.Functional.Relation.Binary.Equality.Setoid using (≋-setoid)
+open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_)
 open import Level using (0ℓ)
 open import Relation.Binary using (Rel; Setoid)
-open import Data.Vec.Functional.Relation.Binary.Equality.Setoid using (≋-setoid)
 
-import Relation.Binary.PropositionalEquality as ≡
+open CommutativeMonoid A renaming (Carrier to Value)
+open Func
+open Sum A using (sum)
+
+opaque
+
+  Values : ℕ → Setoid 0ℓ 0ℓ
+  Values = ≋-setoid (≡.setoid Value)
+
+module _ {n : ℕ} where
+
+  opaque
+
+    unfolding Values
+
+    merge : ∣ Values n ∣ → Value
+    merge = sum
+
+    _⊕_ : ∣ Values n ∣ → ∣ Values n ∣ → ∣ Values n ∣
+    xs ⊕ ys = zipWith _∙_ xs ys
+
+    <ε> : ∣ Values n ∣
+    <ε> = replicate n ε
+
+    head : ∣ Values (suc n) ∣ → Value
+    head xs = xs zero
+
+    tail : ∣ Values (suc n) ∣ → ∣ Values n ∣
+    tail xs = xs ∘ suc
+
+  module ≋ = Setoid (Values n)
+
+  _≋_ : Rel ∣ Values n ∣ 0ℓ
+  _≋_ = ≋._≈_
+
+  infix 4 _≋_
+
+opaque
+
+  unfolding Values
+
+  [] : ∣ Values 0 ∣
+  [] = Vec.[]
+
+  []-unique : (xs ys : ∣ Values 0 ∣) → xs ≋ ys
+  []-unique xs ys ()
+
+module _ {n m : ℕ} where
+
+  opaque
+
+    unfolding Values
+
+    _++_ : ∣ Values n ∣ → ∣ Values m ∣ → ∣ Values (n + m) ∣
+    _++_ = Vec._++_
 
-Values : ℕ → Setoid 0ℓ 0ℓ
-Values = ≋-setoid (≡.setoid A)
+    infixr 5 _++_
 
-_≋_ : {n : ℕ} → Rel (Vector A n) 0ℓ
-_≋_ {n} = Setoid._≈_ (Values n)
+    ++-cong
+        : (xs xs′ : ∣ Values n ∣)
+          {ys ys′ : ∣ Values m ∣}
+        → xs ≋ xs′
+        → ys ≋ ys′
+        → xs ++ ys ≋ xs′ ++ ys′
+    ++-cong xs xs′ = VecProps.++-cong xs xs′
 
-infix 4 _≋_
+    splitₛ : Values (n + m) ⟶ₛ Values n ×ₛ Values m
+    to splitₛ v = v ∘ (_↑ˡ m) , v ∘ (n ↑ʳ_)
+    cong splitₛ v₁≋v₂ = v₁≋v₂ ∘ (_↑ˡ m) , v₁≋v₂ ∘ (n ↑ʳ_)
 
-module ≋ {n : ℕ} = Setoid (Values n)
+  ++ₛ : Values n ×ₛ Values m ⟶ₛ Values (n + m)
+  to ++ₛ (xs , ys) = xs ++ ys
+  cong ++ₛ (≗xs , ≗ys) = ++-cong _ _ ≗xs ≗ys