← Back to branch summary

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

« back to all changes in this revision

Viewing changes to src/Data/List/NonEmpty.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/List/NonEmpty.agda
2
2
-- Non-empty lists
3
3
------------------------------------------------------------------------
4
4
 
 
5
{-# OPTIONS --universe-polymorphism #-}
 
6
 
5
7
module Data.List.NonEmpty where
6
8
 
7
9
open import Data.Product hiding (map)
8
10
open import Data.Nat
9
 
open import Data.Function
 
11
open import Function
10
12
open import Data.Vec as Vec using (Vec; []; _∷_)
11
13
open import Data.List as List using (List; []; _∷_)
12
14
open import Category.Monad
14
16
 
15
17
infixr 5 _∷_ _∷ʳ_ _⁺++⁺_ _++⁺_ _⁺++_
16
18
 
17
 
data List⁺ (A : Set) : Set where
 
19
data List⁺ {a} (A : Set a) : Set a where
18
20
  [_] : (x : A) → List⁺ A
19
21
  _∷_ : (x : A) (xs : List⁺ A) → List⁺ A
20
22
 
21
 
length_-1 : ∀ {A} → List⁺ A → ℕ
 
23
length_-1 : ∀ {a} {A : Set a} → List⁺ A → ℕ
22
24
length [ x ]  -1 = 0
23
25
length x ∷ xs -1 = 1 + length xs -1
24
26
 
25
27
------------------------------------------------------------------------
26
28
-- Conversion
27
29
 
28
 
fromVec : ∀ {n A} → Vec A (suc n) → List⁺ A
 
30
fromVec : ∀ {n a} {A : Set a} → Vec A (suc n) → List⁺ A
29
31
fromVec {zero}  (x ∷ _)  = [ x ]
30
32
fromVec {suc n} (x ∷ xs) = x ∷ fromVec xs
31
33
 
32
 
toVec : ∀ {A} (xs : List⁺ A) → Vec A (suc (length xs -1))
 
34
toVec : ∀ {a} {A : Set a} (xs : List⁺ A) → Vec A (suc (length xs -1))
33
35
toVec [ x ]    = Vec.[_] x
34
36
toVec (x ∷ xs) = x ∷ toVec xs
35
37
 
36
 
lift : ∀ {A B} →
 
38
lift : ∀ {a b} {A : Set a} {B : Set b} →
37
39
       (∀ {m} → Vec A (suc m) → ∃ λ n → Vec B (suc n)) →
38
40
       List⁺ A → List⁺ B
39
41
lift f xs = fromVec (proj₂ (f (toVec xs)))
40
42
 
41
 
fromList : ∀ {A} → A → List A → List⁺ A
 
43
fromList : ∀ {a} {A : Set a} → A → List A → List⁺ A
42
44
fromList x xs = fromVec (Vec.fromList (x ∷ xs))
43
45
 
44
 
toList : ∀ {A} → List⁺ A → List A
45
 
toList = Vec.toList ∘ toVec
 
46
toList : ∀ {a} {A : Set a} → List⁺ A → List A
 
47
toList {a} = Vec.toList {a} ∘ toVec
46
48
 
47
49
------------------------------------------------------------------------
48
50
-- Other operations
49
51
 
50
 
head : ∀ {A} → List⁺ A → A
51
 
head = Vec.head ∘ toVec
52
 
 
53
 
tail : ∀ {A} → List⁺ A → List A
54
 
tail = Vec.toList ∘ Vec.tail ∘ toVec
55
 
 
56
 
map : ∀ {A B} → (A → B) → List⁺ A → List⁺ B
 
52
head : ∀ {a} {A : Set a} → List⁺ A → A
 
53
head {a} = Vec.head {a} ∘ toVec
 
54
 
 
55
tail : ∀ {a} {A : Set a} → List⁺ A → List A
 
56
tail {a} = Vec.toList {a} ∘ Vec.tail {a} ∘ toVec
 
57
 
 
58
map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → List⁺ A → List⁺ B
57
59
map f = lift (λ xs → (, Vec.map f xs))
58
60
 
59
61
-- Right fold. Note that s is only applied to the last element (see
60
62
-- the examples below).
61
63
 
62
 
foldr : {A B : Set} → (A → B → B) → (A → B) → List⁺ A → B
 
64
foldr : ∀ {a b} {A : Set a} {B : Set b} →
 
65
        (A → B → B) → (A → B) → List⁺ A → B
63
66
foldr c s [ x ]    = s x
64
67
foldr c s (x ∷ xs) = c x (foldr c s xs)
65
68
 
66
69
-- Left fold. Note that s is only applied to the first element (see
67
70
-- the examples below).
68
71
 
69
 
foldl : {A B : Set} → (B → A → B) → (A → B) → List⁺ A → B
 
72
foldl : ∀ {a b} {A : Set a} {B : Set b} →
 
73
        (B → A → B) → (A → B) → List⁺ A → B
70
74
foldl c s [ x ]    = s x
71
75
foldl c s (x ∷ xs) = foldl c (c (s x)) xs
72
76
 
73
77
-- Append (several variants).
74
78
 
75
 
_⁺++⁺_ : ∀ {A} → List⁺ A → List⁺ A → List⁺ A
 
79
_⁺++⁺_ : ∀ {a} {A : Set a} → List⁺ A → List⁺ A → List⁺ A
76
80
xs ⁺++⁺ ys = foldr _∷_ (λ x → x ∷ ys) xs
77
81
 
78
 
_⁺++_ : ∀ {A} → List⁺ A → List A → List⁺ A
 
82
_⁺++_ : ∀ {a} {A : Set a} → List⁺ A → List A → List⁺ A
79
83
xs ⁺++ ys = foldr _∷_ (λ x → fromList x ys) xs
80
84
 
81
 
_++⁺_ : ∀ {A} → List A → List⁺ A → List⁺ A
 
85
_++⁺_ : ∀ {a} {A : Set a} → List A → List⁺ A → List⁺ A
82
86
xs ++⁺ ys = List.foldr _∷_ ys xs
83
87
 
84
 
concat : ∀ {A} → List⁺ (List⁺ A) → List⁺ A
 
88
concat : ∀ {a} {A : Set a} → List⁺ (List⁺ A) → List⁺ A
85
89
concat [ xs ]     = xs
86
90
concat (xs ∷ xss) = xs ⁺++⁺ concat xss
87
91
 
88
 
monad : RawMonad List⁺
 
92
monad : ∀ {f} → RawMonad (List⁺ {a = f})
89
93
monad = record
90
94
  { return = [_]
91
95
  ; _>>=_  = λ xs f → concat (map f xs)
92
96
  }
93
97
 
94
 
reverse : ∀ {A} → List⁺ A → List⁺ A
 
98
reverse : ∀ {a} {A : Set a} → List⁺ A → List⁺ A
95
99
reverse = lift (,_ ∘′ Vec.reverse)
96
100
 
97
101
-- Snoc.
98
102
 
99
 
_∷ʳ_ : ∀ {A} → List⁺ A → A → List⁺ A
 
103
_∷ʳ_ : ∀ {a} {A : Set a} → List⁺ A → A → List⁺ A
100
104
xs ∷ʳ x = foldr _∷_ (λ y → y ∷ [ x ]) xs
101
105
 
102
106
-- A snoc-view of non-empty lists.
103
107
 
104
108
infixl 5 _∷ʳ′_
105
109
 
106
 
data SnocView {A} : List⁺ A → Set where
 
110
data SnocView {a} {A : Set a} : List⁺ A → Set a where
107
111
  [_]   : (x : A)                → SnocView [ x ]
108
112
  _∷ʳ′_ : (xs : List⁺ A) (x : A) → SnocView (xs ∷ʳ x)
109
113
 
110
 
snocView : ∀ {A} (xs : List⁺ A) → SnocView xs
 
114
snocView : ∀ {a} {A : Set a} (xs : List⁺ A) → SnocView xs
111
115
snocView [ x ]            = [ x ]
112
116
snocView (x ∷ xs)         with snocView xs
113
117
snocView (x ∷ .([ y ]))   | [ y ]    = [ x ] ∷ʳ′ y
115
119
 
116
120
-- The last element in the list.
117
121
 
118
 
last : ∀ {A} → List⁺ A → A
 
122
last : ∀ {a} {A : Set a} → List⁺ A → A
119
123
last xs with snocView xs
120
124
last .([ y ])   | [ y ]    = y
121
125
last .(ys ∷ʳ y) | ys ∷ʳ′ y = y