← Back to branch summary

~ubuntu-branches/ubuntu/raring/agda-stdlib/raring-proposed

« back to all changes in this revision

Viewing changes to src/Data/DifferenceVec.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2011-11-29 17:00:35 UTC
  • mfrom: (1.1.3)
  • Revision ID: package-import@ubuntu.com-20111129170035-00v3pq4mmhoo5ulf
Tags: 0.6~darcs20111129t1640-1
* [ef445ab] Imported Upstream version 0.6~darcs20111129t1640
  + Darcs snapshot required for Agda 2.3.0 compatibility
* [f801f83] Update BDs and deps to require Agda 2.3.0
* [c52be90] Use 3.0 (quilt) for bz2 orig

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/DifferenceVec.agda
1
1
------------------------------------------------------------------------
 
2
-- The Agda standard library
 
3
--
2
4
-- Vectors with fast append
3
5
------------------------------------------------------------------------
4
6
 
11
13
 
12
14
infixr 5 _∷_ _++_
13
15
 
14
 
DiffVec : Set → Diffℕ → Set
 
16
DiffVec : ∀ {ℓ} → Set ℓ → Diffℕ → Set ℓ
15
17
DiffVec A m = ∀ {n} → Vec A n → Vec A (m n)
16
18
 
17
 
[] : ∀ {A} → DiffVec A 0#
 
19
[] : ∀ {a} {A : Set a} → DiffVec A 0#
18
20
[] = λ k → k
19
21
 
20
 
_∷_ : ∀ {A n} → A → DiffVec A n → DiffVec A (suc n)
 
22
_∷_ : ∀ {a} {A : Set a} {n} → A → DiffVec A n → DiffVec A (suc n)
21
23
x ∷ xs = λ k → V._∷_ x (xs k)
22
24
 
23
 
[_] : ∀ {A} → A → DiffVec A 1#
 
25
[_] : ∀ {a} {A : Set a} → A → DiffVec A 1#
24
26
[ x ] = x ∷ []
25
27
 
26
 
_++_ : ∀ {A m n} → DiffVec A m → DiffVec A n → DiffVec A (m + n)
 
28
_++_ : ∀ {a} {A : Set a} {m n} →
 
29
       DiffVec A m → DiffVec A n → DiffVec A (m + n)
27
30
xs ++ ys = λ k → xs (ys k)
28
31
 
29
 
toVec : ∀ {A n} → DiffVec A n → Vec A (toℕ n)
 
32
toVec : ∀ {a} {A : Set a} {n} → DiffVec A n → Vec A (toℕ n)
30
33
toVec xs = xs V.[]
31
34
 
32
35
-- fromVec xs is linear in the length of xs.
33
36
 
34
 
fromVec : ∀ {A n} → Vec A n → DiffVec A (fromℕ n)
 
37
fromVec : ∀ {a} {A : Set a} {n} → Vec A n → DiffVec A (fromℕ n)
35
38
fromVec xs = λ k → xs ⟨ V._++_ ⟩ k
36
39
 
37
 
head : ∀ {A n} → DiffVec A (suc n) → A
 
40
head : ∀ {a} {A : Set a} {n} → DiffVec A (suc n) → A
38
41
head xs = V.head (toVec xs)
39
42
 
40
 
tail : ∀ {A n} → DiffVec A (suc n) → DiffVec A n
 
43
tail : ∀ {a} {A : Set a} {n} → DiffVec A (suc n) → DiffVec A n
41
44
tail xs = λ k → V.tail (xs k)
42
45
 
43
 
take : ∀ {a} m {n} → DiffVec a (fromℕ m + n) → DiffVec a (fromℕ m)
 
46
take : ∀ {a} {A : Set a} m {n} →
 
47
       DiffVec A (fromℕ m + n) → DiffVec A (fromℕ m)
44
48
take N.zero    xs = []
45
49
take (N.suc m) xs = head xs ∷ take m (tail xs)
46
50
 
47
 
drop : ∀ {a} m {n} → DiffVec a (fromℕ m + n) → DiffVec a n
 
51
drop : ∀ {a} {A : Set a} m {n} →
 
52
       DiffVec A (fromℕ m + n) → DiffVec A n
48
53
drop N.zero    xs = xs
49
54
drop (N.suc m) xs = drop m (tail xs)