1
------------------------------------------------------------------------
3
------------------------------------------------------------------------
4
{-# OPTIONS --universe-polymorphism #-}
9
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂)
11
open import Data.Maybe using (Maybe; nothing; just)
12
open import Data.Product as Prod using (_×_; _,_)
13
open import Data.Function
15
import Relation.Binary.PropositionalEquality as PropEq
16
import Algebra.FunctionProperties as FunProp
20
------------------------------------------------------------------------
23
data List {a} (A : Set a) : Set a where
25
_∷_ : (x : A) (xs : List A) → List A
27
{-# BUILTIN LIST List #-}
28
{-# BUILTIN NIL [] #-}
29
{-# BUILTIN CONS _∷_ #-}
31
------------------------------------------------------------------------
36
[_] : ∀ {a} {A : Set a} → A → List A
39
_++_ : ∀ {a} {A : Set a} → List A → List A → List A
41
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
47
_∷ʳ_ : ∀ {a} {A : Set a} → List A → A → List A
50
null : ∀ {a} {A : Set a} → List A → Bool
54
-- * List transformations
56
map : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → List A → List B
58
map f (x ∷ xs) = f x ∷ map f xs
60
reverse : ∀ {a} {A : Set a} → List A → List A
61
reverse xs = rev xs []
63
rev : ∀ {a} {A : Set a} → List A → List A → List A
65
rev (x ∷ xs) ys = rev xs (x ∷ ys)
67
replicate : ∀ {a} {A : Set a} → (n : ℕ) → A → List A
69
replicate (suc n) x = x ∷ replicate n x
71
zipWith : ∀ {a b c} {A : Set a} {B : Set b} {C : Set c}
72
→ (A → B → C) → List A → List B → List C
73
zipWith f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith f xs ys
76
zip : ∀ {a b} {A : Set a} {B : Set b} → List A → List B → List (A × B)
79
intersperse : ∀ {a} {A : Set a} → A → List A → List A
81
intersperse x (y ∷ []) = [ y ]
82
intersperse x (y ∷ z ∷ zs) = y ∷ x ∷ intersperse x (z ∷ zs)
84
-- * Reducing lists (folds)
86
foldr : ∀ {a b} {A : Set a} {B : Set b} → (A → B → B) → B → List A → B
88
foldr c n (x ∷ xs) = c x (foldr c n xs)
90
foldl : ∀ {a b} {A : Set a} {B : Set b} → (A → B → A) → A → List B → A
92
foldl c n (x ∷ xs) = foldl c (c n x) xs
96
concat : ∀ {a} {A : Set a} → List (List A) → List A
97
concat = foldr _++_ []
99
concatMap : ∀ {a b} {A : Set a} {B : Set b} →
100
(A → List B) → List A → List B
101
concatMap f = concat ∘ map f
103
and : List Bool → Bool
106
or : List Bool → Bool
109
any : ∀ {a} {A : Set a} → (A → Bool) → List A → Bool
112
all : ∀ {a} {A : Set a} → (A → Bool) → List A → Bool
119
product = foldr _*_ 1
121
length : ∀ {a} {A : Set a} → List A → ℕ
122
length = foldr (λ _ → suc) 0
128
scanr : ∀ {a b} {A : Set a} {B : Set b} →
129
(A → B → B) → B → List A → List B
130
scanr f e [] = e ∷ []
131
scanr f e (x ∷ xs) with scanr f e xs
132
... | [] = [] -- dead branch
133
... | y ∷ ys = f x y ∷ y ∷ ys
135
scanl : ∀ {a b} {A : Set a} {B : Set b} →
136
(A → B → A) → A → List B → List A
137
scanl f e [] = e ∷ []
138
scanl f e (x ∷ xs) = e ∷ scanl f (f e x) xs
142
-- Unfold. Uses a measure (a natural number) to ensure termination.
144
unfold : ∀ {a b} {A : Set a} (B : ℕ → Set b)
145
(f : ∀ {n} → B (suc n) → Maybe (A × B n)) →
147
unfold B f {n = zero} s = []
148
unfold B f {n = suc n} s with f s
150
... | just (x , s') = x ∷ unfold B f s'
152
-- downFrom 3 = 2 ∷ 1 ∷ 0 ∷ [].
154
downFrom : ℕ → List ℕ
155
downFrom n = unfold Singleton f (wrap n)
157
data Singleton : ℕ → Set where
158
wrap : (n : ℕ) → Singleton n
160
f : ∀ {n} → Singleton (suc n) → Maybe (ℕ × Singleton n)
161
f {n} (wrap .(suc n)) = just (n , wrap n)
165
fromMaybe : ∀ {a} {A : Set a} → Maybe A → List A
166
fromMaybe (just x) = [ x ]
167
fromMaybe nothing = []
171
-- ** Extracting sublists
173
take : ∀ {a} {A : Set a} → ℕ → List A → List A
176
take (suc n) (x ∷ xs) = x ∷ take n xs
178
drop : ∀ {a} {A : Set a} → ℕ → List A → List A
181
drop (suc n) (x ∷ xs) = drop n xs
183
splitAt : ∀ {a} {A : Set a} → ℕ → List A → (List A × List A)
184
splitAt zero xs = ([] , xs)
185
splitAt (suc n) [] = ([] , [])
186
splitAt (suc n) (x ∷ xs) with splitAt n xs
187
... | (ys , zs) = (x ∷ ys , zs)
189
takeWhile : ∀ {a} {A : Set a} → (A → Bool) → List A → List A
191
takeWhile p (x ∷ xs) with p x
192
... | true = x ∷ takeWhile p xs
195
dropWhile : ∀ {a} {A : Set a} → (A → Bool) → List A → List A
197
dropWhile p (x ∷ xs) with p x
198
... | true = dropWhile p xs
201
span : ∀ {a} {A : Set a} → (A → Bool) → List A → (List A × List A)
202
span p [] = ([] , [])
203
span p (x ∷ xs) with p x
204
... | true = Prod.map (_∷_ x) id (span p xs)
205
... | false = ([] , x ∷ xs)
207
break : ∀ {a} {A : Set a} → (A → Bool) → List A → (List A × List A)
208
break p = span (not ∘ p)
210
inits : ∀ {a} {A : Set a} → List A → List (List A)
212
inits (x ∷ xs) = [] ∷ map (_∷_ x) (inits xs)
214
tails : ∀ {a} {A : Set a} → List A → List (List A)
216
tails (x ∷ xs) = (x ∷ xs) ∷ tails xs
220
data InitLast {a} {A : Set a} : List A → Set a where
222
_∷ʳ'_ : (xs : List A) (x : A) → InitLast (xs ∷ʳ x)
224
initLast : ∀ {a} {A : Set a} (xs : List A) → InitLast xs
226
initLast (x ∷ xs) with initLast xs
227
initLast (x ∷ .[]) | [] = [] ∷ʳ' x
228
initLast (x ∷ .(ys ∷ʳ y)) | ys ∷ʳ' y = (x ∷ ys) ∷ʳ' y
232
-- ** Searching with a predicate
234
-- A generalised variant of filter.
236
gfilter : ∀ {a b} {A : Set a} {B : Set b} →
237
(A → Maybe B) → List A → List B
239
gfilter p (x ∷ xs) with p x
240
... | just y = y ∷ gfilter p xs
241
... | nothing = gfilter p xs
243
filter : ∀ {a} {A : Set a} → (A → Bool) → List A → List A
244
filter p = gfilter (λ x → if p x then just x else nothing)
246
partition : ∀ {a} {A : Set a} → (A → Bool) → List A → (List A × List A)
247
partition p [] = ([] , [])
248
partition p (x ∷ xs) with p x | partition p xs
249
... | true | (ys , zs) = (x ∷ ys , zs)
250
... | false | (ys , zs) = (ys , x ∷ zs)
252
------------------------------------------------------------------------
255
monoid : Set → Monoid
262
{ isSemigroup = record
263
{ isEquivalence = PropEq.isEquivalence
265
; ∙-cong = cong₂ _++_
267
; identity = ((λ _ → refl) , identity)
274
identity : RightIdentity [] _++_
276
identity (x ∷ xs) = cong (_∷_ x) (identity xs)
278
assoc : Associative _++_
279
assoc [] ys zs = refl
280
assoc (x ∷ xs) ys zs = cong (_∷_ x) (assoc xs ys zs)
282
------------------------------------------------------------------------
285
open import Category.Monad
287
monad : RawMonad List
289
{ return = λ x → x ∷ []
290
; _>>=_ = λ xs f → concat (map f xs)
293
monadZero : RawMonadZero List
299
monadPlus : RawMonadPlus List
301
{ monadZero = monadZero
305
------------------------------------------------------------------------
309
module Monadic {M} (Mon : RawMonad M) where
313
sequence : ∀ {A : Set} → List (M A) → M (List A)
314
sequence [] = return []
315
sequence (x ∷ xs) = _∷_ <$> x ⊛ sequence xs
317
mapM : ∀ {a} {A : Set a} {B} → (A → M B) → List A → M (List B)
318
mapM f = sequence ∘ map f
added
removed
src/Data/List.agda
