blob: cd88d6dbca7ac1d8b4458980d5596f4fc46fc895 (
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
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- Bounded vectors
------------------------------------------------------------------------
-- Vectors of a specified maximum length.
module Data.BoundedVec where
open import Data.Nat
open import Data.List.Base as List using (List)
open import Data.Vec as Vec using (Vec)
import Data.BoundedVec.Inefficient as Ineff
open import Relation.Binary.PropositionalEquality
open import Data.Nat.Solver
open +-*-Solver
------------------------------------------------------------------------
-- The type
abstract
data BoundedVec {a} (A : Set a) : ℕ → Set a where
bVec : ∀ {m n} (xs : Vec A n) → BoundedVec A (n + m)
[] : ∀ {a n} {A : Set a} → BoundedVec A n
[] = bVec Vec.[]
infixr 5 _∷_
_∷_ : ∀ {a n} {A : Set a} →
A → BoundedVec A n → BoundedVec A (suc n)
x ∷ bVec xs = bVec (Vec._∷_ x xs)
------------------------------------------------------------------------
-- Pattern matching
infixr 5 _∷v_
data View {a} (A : Set a) : ℕ → Set a where
[]v : ∀ {n} → View A n
_∷v_ : ∀ {n} (x : A) (xs : BoundedVec A n) → View A (suc n)
abstract
view : ∀ {a n} {A : Set a} → BoundedVec A n → View A n
view (bVec Vec.[]) = []v
view (bVec (Vec._∷_ x xs)) = x ∷v bVec xs
------------------------------------------------------------------------
-- Increasing the bound
abstract
↑ : ∀ {a n} {A : Set a} → BoundedVec A n → BoundedVec A (suc n)
↑ {A = A} (bVec {m = m} {n = n} xs) =
subst (BoundedVec A) lemma
(bVec {m = suc m} xs)
where
lemma : n + (1 + m) ≡ 1 + (n + m)
lemma = solve 2 (λ m n → n :+ (con 1 :+ m) := con 1 :+ (n :+ m))
refl m n
------------------------------------------------------------------------
-- Conversions
module _ {a} {A : Set a} where
abstract
fromList : (xs : List A) → BoundedVec A (List.length xs)
fromList xs =
subst (BoundedVec A) lemma
(bVec {m = zero} (Vec.fromList xs))
where
lemma : List.length xs + 0 ≡ List.length xs
lemma = solve 1 (λ m → m :+ con 0 := m) refl _
toList : ∀ {n} → BoundedVec A n → List A
toList (bVec xs) = Vec.toList xs
toInefficient : ∀ {n} → BoundedVec A n → Ineff.BoundedVec A n
toInefficient xs with view xs
... | []v = Ineff.[]
... | y ∷v ys = y Ineff.∷ toInefficient ys
fromInefficient : ∀ {n} → Ineff.BoundedVec A n → BoundedVec A n
fromInefficient Ineff.[] = []
fromInefficient (x Ineff.∷ xs) = x ∷ fromInefficient xs
|
