blob: 737e34e1e9004eecf7adca16d3ee9e76487bd898 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
|
{-# 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.Properties as VecProps
import Relation.Binary.PropositionalEquality as ≡
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 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._++_
infixr 5 _++_
++-cong
: (xs xs′ : ∣ Values n ∣)
{ys ys′ : ∣ Values m ∣}
→ xs ≋ xs′
→ ys ≋ ys′
→ xs ++ ys ≋ xs′ ++ ys′
++-cong xs xs′ = VecProps.++-cong xs xs′
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
|
