1 files changed, 146 insertions, 0 deletions
diff --git a/Data/System/Values.agda b/Data/System/Values.agda
new file mode 100644
index 0000000..545a835
--- /dev/null
+++ b/Data/System/Values.agda
@@ -0,0 +1,146 @@
+{-# OPTIONS --without-K --safe #-}
+
+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.Relation.Binary.Equality.Setoid as Pointwise
+import Relation.Binary.PropositionalEquality as ≡
+
+open import Data.Fin using (_↑ˡ_; _↑ʳ_; zero; suc; splitAt)
+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.Sum using (inj₁; inj₂)
+open import Data.Vec.Functional as Vec using (Vector; zipWith; replicate)
+open import Function using (Func; _⟶ₛ_; _⟨$⟩_; _∘_)
+open import Level using (0ℓ)
+open import Relation.Binary using (Rel; Setoid; IsEquivalence)
+
+open CommutativeMonoid A renaming (Carrier to Value)
+open Func
+open Sum A using (sum)
+
+open Pointwise setoid using (≋-setoid; ≋-isEquivalence)
+
+opaque
+
+  Values : ℕ → Setoid 0ℓ 0ℓ
+  Values = ≋-setoid
+
+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
+  open Setoid
+  ≋-isEquiv : ∀ n → IsEquivalence (_≈_ (Values n))
+  ≋-isEquiv = ≋-isEquivalence
+
+module _ {n : ℕ} where
+
+  opaque
+    unfolding _⊕_
+
+    ⊕-cong : {x y u v : ≋.Carrier {n}} → x ≋ y → u ≋ v → x ⊕ u ≋ y ⊕ v
+    ⊕-cong x≋y u≋v i = ∙-cong (x≋y i) (u≋v i)
+
+    ⊕-assoc : (x y z : ≋.Carrier {n}) → (x ⊕ y) ⊕ z ≋ x ⊕ (y ⊕ z)
+    ⊕-assoc x y z i = assoc (x i) (y i) (z i)
+
+    ⊕-identityˡ : (x : ≋.Carrier {n}) → <ε> ⊕ x ≋ x
+    ⊕-identityˡ x i = identityˡ (x i)
+
+    ⊕-identityʳ : (x : ≋.Carrier {n}) → x ⊕ <ε> ≋ x
+    ⊕-identityʳ x i = identityʳ (x i)
+
+    ⊕-comm : (x y : ≋.Carrier {n}) → x ⊕ y ≋ y ⊕ x
+    ⊕-comm x y i = comm (x i) (y i)
+
+open CommutativeMonoid
+Valuesₘ : ℕ → CommutativeMonoid 0ℓ 0ℓ
+Valuesₘ n .Carrier = ∣ Values n ∣
+Valuesₘ n ._≈_ = _≋_
+Valuesₘ n ._∙_ = _⊕_
+Valuesₘ n .ε = <ε>
+Valuesₘ n .isCommutativeMonoid = record
+    { isMonoid = record
+        { isSemigroup = record
+            { isMagma = record
+                { isEquivalence = ≋-isEquiv n
+                ; ∙-cong = ⊕-cong
+                }
+            ; assoc = ⊕-assoc
+            }
+        ; identity = ⊕-identityˡ , ⊕-identityʳ
+        }
+    ; comm = ⊕-comm
+    }
+
+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._++_
+
+    infixr 5 _++_
+
+    ++-cong
+        : (xs xs′ : ∣ Values n ∣)
+          {ys ys′ : ∣ Values m ∣}
+        → xs ≋ xs′
+        → ys ≋ ys′
+        → xs ++ ys ≋ xs′ ++ ys′
+    ++-cong xs xs′ xs≋xs′ ys≋ys′ i with splitAt n i
+    ... | inj₁ i = xs≋xs′ i
+    ... | inj₂ i = ys≋ys′ i
+
+    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 ↑ʳ_)
+
+  ++ₛ : Values n ×ₛ Values m ⟶ₛ Values (n + m)
+  to ++ₛ (xs , ys) = xs ++ ys
+  cong ++ₛ (≗xs , ≗ys) = ++-cong _ _ ≗xs ≗ys