← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Data/Vec.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2011-05-24 10:26:15 UTC
  • mfrom: (1.1.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20110524102615-9tontf43bq9ym690
Tags: 0.5-1
http://bugs.debian.org/573807
http://bugs.debian.org/598708
* [9251e0b] Imported Upstream version 0.5
* [ba20206] Make package architecture independent (Closes: #573807, #598708,
  #599958)
* [2c82171] Add watch file
* [0518fa6] No longer need procps | hurd BD as we no longer have the ticker
* [daf2445] Don't use upstream's make install — handled ourselves by
  dh_install
* [1b86533] Update watchfile to point at new location
* [637f47d] Remove debian/gbp.conf as we are no longer building for exp
* [cc88671] Require Agda 2.2.10
* [e99dab5] Set maximum stack size to 1G to prevent overflows in the build
* [251cd1d] Run the test suite manually
* [a7db697] Set the variable in the emacs loading script properly
* [540ca3f] Improve short description
* [6b3e794] Add dependencies on compatible versions of the Agda library
* [7127678] Standards-Version bump to 3.9.2, no changes required
* [9d0ae30] Update to use ghc instead of ghc6
* [3f6879a] Set Maintainer to my d.o email address

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Vec.agda
6
6
 
7
7
module Data.Vec where
8
8
 
 
9
open import Category.Applicative
9
10
open import Data.Nat
10
11
open import Data.Fin using (Fin; zero; suc)
11
12
open import Data.List as List using (List)
12
13
open import Data.Product using (∃; ∃₂; _×_; _,_)
 
14
open import Function
13
15
open import Level
14
16
open import Relation.Binary.PropositionalEquality
15
17
 
54
56
[]       ++ ys = ys
55
57
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
56
58
 
 
59
infixl 4 _⊛_
 
60
 
 
61
_⊛_ : ∀ {a b n} {A : Set a} {B : Set b} →
 
62
      Vec (A → B) n → Vec A n → Vec B n
 
63
[]       ⊛ []       = []
 
64
(f ∷ fs) ⊛ (x ∷ xs) = f x ∷ (fs ⊛ xs)
 
65
 
 
66
replicate : ∀ {a n} {A : Set a} → A → Vec A n
 
67
replicate {n = zero}  x = []
 
68
replicate {n = suc n} x = x ∷ replicate x
 
69
 
 
70
applicative : ∀ {a n} → RawApplicative (λ (A : Set a) → Vec A n)
 
71
applicative = record
 
72
  { pure = replicate
 
73
  ; _⊛_  = _⊛_
 
74
  }
 
75
 
57
76
map : ∀ {a b n} {A : Set a} {B : Set b} →
58
77
      (A → B) → Vec A n → Vec B n
59
 
map f []       = []
60
 
map f (x ∷ xs) = f x ∷ map f xs
 
78
map f xs = replicate f ⊛ xs
61
79
 
62
80
zipWith : ∀ {a b c n} {A : Set a} {B : Set b} {C : Set c} →
63
81
          (A → B → C) → Vec A n → Vec B n → Vec C n
64
 
zipWith _⊕_ []       []       = []
65
 
zipWith _⊕_ (x ∷ xs) (y ∷ ys) = (x ⊕ y) ∷ zipWith _⊕_ xs ys
 
82
zipWith _⊕_ xs ys = replicate _⊕_ ⊛ xs ⊛ ys
66
83
 
67
84
zip : ∀ {a b n} {A : Set a} {B : Set b} →
68
85
      Vec A n → Vec B n → Vec (A × B) n
69
86
zip = zipWith _,_
70
87
 
71
 
replicate : ∀ {a n} {A : Set a} → A → Vec A n
72
 
replicate {n = zero}  x = []
73
 
replicate {n = suc n} x = x ∷ replicate x
74
 
 
75
88
foldr : ∀ {a b} {A : Set a} (B : ℕ → Set b) {m} →
76
89
        (∀ {n} → A → B n → B (suc n)) →
77
90
        B zero →
166
179
        Vec A m → (A → Vec B n) → Vec B (m * n)
167
180
xs >>= f = concat (map f xs)
168
181
 
169
 
infixl 4 _⊛_
 
182
infixl 4 _⊛*_
170
183
 
171
 
_⊛_ : ∀ {a b m n} {A : Set a} {B : Set b} →
172
 
      Vec (A → B) m → Vec A n → Vec B (m * n)
173
 
fs ⊛ xs = fs >>= λ f → map f xs
 
184
_⊛*_ : ∀ {a b m n} {A : Set a} {B : Set b} →
 
185
       Vec (A → B) m → Vec A n → Vec B (m * n)
 
186
fs ⊛* xs = fs >>= λ f → map f xs
174
187
 
175
188
-- Interleaves the two vectors.
176
189
 
181
194
[]       ⋎ ys = ys
182
195
(x ∷ xs) ⋎ ys = x ∷ (ys ⋎ xs)
183
196
 
 
197
-- A lookup function.
 
198
 
184
199
lookup : ∀ {a n} {A : Set a} → Fin n → Vec A n → A
185
200
lookup zero    (x ∷ xs) = x
186
201
lookup (suc i) (x ∷ xs) = lookup i xs
187
202
 
 
203
-- An inverse of flip lookup.
 
204
 
 
205
tabulate : ∀ {n a} {A : Set a} → (Fin n → A) → Vec A n
 
206
tabulate {zero}  f = []
 
207
tabulate {suc n} f = f zero ∷ tabulate (f ∘ suc)
 
208
 
188
209
-- Update.
189
210
 
190
211
infixl 6 _[_]≔_
195
216
(x ∷ xs) [ suc i ]≔ y = x ∷ xs [ i ]≔ y
196
217
 
197
218
-- Generates a vector containing all elements in Fin n. This function
 
219
-- is not placed in Data.Fin because Data.Vec depends on Data.Fin.
 
220
--
 
221
-- The implementation was suggested by Conor McBride ("Fwd: how to
 
222
-- count 0..n-1", http://thread.gmane.org/gmane.comp.lang.agda/2554).
198
223
 
199
224
allFin : ∀ n → Vec (Fin n) n
200
 
allFin zero    = []
201
 
allFin (suc n) = zero ∷ map suc (allFin n)
 
225
allFin _ = tabulate id