← Back to branch summary

~ubuntu-branches/ubuntu/saucy/agda-stdlib/saucy

« back to all changes in this revision

Viewing changes to src/Data/List.agda

  • Committer: Bazaar Package Importer
  • Author(s): Iain Lane
  • Date: 2011-02-25 22:28:40 UTC
  • mfrom: (1.1.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20110225222840-jt16gl302kca7h0g
Tags: 0.5-1~ubuntu1
https://launchpad.net/bugs/725364
http://bugs.debian.org/573807
http://bugs.debian.org/598708

* Upload to Ubuntu from Debian's VCS due to delays in unstable caused by
  the GHC 7 transition (LP: #725364)
* [ba20206] Make package architecture independent (Closes: #573807, #598708,
  #599958)
* [0fb0600] Standards-Version → 3.9.1, no changes required
* [d3f13b8] Update required Agda version to 2.2.8
* [cc1f5c8] Imported Upstream version 0.4
* [2c82171] Add watch file
* [9251e0b] Imported Upstream version 0.5
* [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

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/Data/List.agda
10
10
open import Data.Bool
11
11
open import Data.Maybe using (Maybe; nothing; just)
12
12
open import Data.Product as Prod using (_×_; _,_)
13
 
open import Data.Function
 
13
open import Function
14
14
open import Algebra
15
15
import Relation.Binary.PropositionalEquality as PropEq
16
16
import Algebra.FunctionProperties as FunProp
57
57
map f []       = []
58
58
map f (x ∷ xs) = f x ∷ map f xs
59
59
 
60
 
reverse : ∀ {a} {A : Set a} → List A → List A
61
 
reverse xs = rev xs []
62
 
  where
63
 
  rev : ∀ {a} {A : Set a} → List A → List A → List A
64
 
  rev []       ys = ys
65
 
  rev (x ∷ xs) ys = rev xs (x ∷ ys)
66
 
 
67
60
replicate : ∀ {a} {A : Set a} → (n : ℕ) → A → List A
68
61
replicate zero    x = []
69
62
replicate (suc n) x = x ∷ replicate n x
121
114
length : ∀ {a} {A : Set a} → List A → ℕ
122
115
length = foldr (λ _ → suc) 0
123
116
 
 
117
reverse : ∀ {a} {A : Set a} → List A → List A
 
118
reverse = foldl (λ rev x → x ∷ rev) []
 
119
 
124
120
-- * Building lists
125
121
 
126
122
-- ** Scans
252
248
------------------------------------------------------------------------
253
249
-- List monoid
254
250
 
255
 
monoid : Set → Monoid
 
251
monoid : ∀ {ℓ} → Set ℓ → Monoid _ _
256
252
monoid A = record
257
253
  { Carrier  = List A
258
254
  ; _≈_      = _≡_
284
280
 
285
281
open import Category.Monad
286
282
 
287
 
monad : RawMonad List
 
283
monad : ∀ {ℓ} → RawMonad (List {ℓ})
288
284
monad = record
289
285
  { return = λ x → x ∷ []
290
286
  ; _>>=_  = λ xs f → concat (map f xs)
291
287
  }
292
288
 
293
 
monadZero : RawMonadZero List
 
289
monadZero : ∀ {ℓ} → RawMonadZero (List {ℓ})
294
290
monadZero = record
295
291
  { monad = monad
296
292
  ; ∅     = []
297
293
  }
298
294
 
299
 
monadPlus : RawMonadPlus List
 
295
monadPlus : ∀ {ℓ} → RawMonadPlus (List {ℓ})
300
296
monadPlus = record
301
297
  { monadZero = monadZero
302
298
  ; _∣_       = _++_
306
302
-- Monadic functions
307
303
 
308
304
private
309
 
 module Monadic {M} (Mon : RawMonad M) where
 
305
 module Monadic {m} {M : Set m → Set m} (Mon : RawMonad M) where
310
306
 
311
307
  open RawMonad Mon
312
308
 
313
 
  sequence : ∀ {A : Set} → List (M A) → M (List A)
 
309
  sequence : ∀ {A} → List (M A) → M (List A)
314
310
  sequence []       = return []
315
311
  sequence (x ∷ xs) = _∷_ <$> x ⊛ sequence xs
316
312