← Back to branch summary

~ubuntu-branches/ubuntu/lucid/agda-stdlib/lucid

« back to all changes in this revision

Viewing changes to src/Data/Star/Vec.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2010-01-08 23:35:09 UTC
  • Revision ID: james.westby@ubuntu.com-20100108233509-l6ejt9xji64xysfb
Import upstream version 0.3

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/Star/Vec.agda
 
1
------------------------------------------------------------------------
 
2
-- Vectors defined in terms of Data.Star
 
3
------------------------------------------------------------------------
 
4
 
 
5
module Data.Star.Vec where
 
6
 
 
7
open import Data.Star
 
8
open import Data.Star.Nat
 
9
open import Data.Star.Fin using (Fin)
 
10
open import Data.Star.Decoration
 
11
open import Data.Star.Pointer as Pointer hiding (lookup)
 
12
open import Data.Star.List using (List)
 
13
open import Relation.Binary
 
14
open import Relation.Binary.Consequences
 
15
open import Data.Function
 
16
open import Data.Unit
 
17
 
 
18
-- The vector type. Vectors are natural numbers decorated with extra
 
19
-- information (i.e. elements).
 
20
 
 
21
Vec : Set → ℕ → Set
 
22
Vec a = All (λ _ → a)
 
23
 
 
24
-- Nil and cons.
 
25
 
 
26
[] : ∀ {a} → Vec a zero
 
27
[] = ε
 
28
 
 
29
infixr 5 _∷_
 
30
 
 
31
_∷_ : ∀ {a n} → a → Vec a n → Vec a (suc n)
 
32
x ∷ xs = ↦ x ◅ xs
 
33
 
 
34
-- Projections.
 
35
 
 
36
head : ∀ {a n} → Vec a (1# + n) → a
 
37
head (↦ x ◅ _) = x
 
38
 
 
39
tail : ∀ {a n} → Vec a (1# + n) → Vec a n
 
40
tail (↦ _ ◅ xs) = xs
 
41
 
 
42
-- Append.
 
43
 
 
44
infixr 5 _++_
 
45
 
 
46
_++_ : ∀ {a m n} → Vec a m → Vec a n → Vec a (m + n)
 
47
_++_ = _◅◅◅_
 
48
 
 
49
-- Safe lookup.
 
50
 
 
51
lookup : ∀ {a n} → Fin n → Vec a n → a
 
52
lookup i xs with Pointer.lookup i xs
 
53
... | result _ x = x
 
54
 
 
55
------------------------------------------------------------------------
 
56
-- Conversions
 
57
 
 
58
fromList : ∀ {a} → (xs : List a) → Vec a (length xs)
 
59
fromList ε        = []
 
60
fromList (x ◅ xs) = x ∷ fromList xs
 
61
 
 
62
toList : ∀ {a n} → Vec a n → List a
 
63
toList = gmap (const tt) decoration