← Back to branch summary

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

« back to all changes in this revision

Viewing changes to examples/lib/Data/List.agda

  • Committer: Package Import Robot
  • Author(s): Iain Lane
  • Date: 2014-08-05 06:38:12 UTC
  • mfrom: (1.1.6)
  • Revision ID: package-import@ubuntu.com-20140805063812-io8e77niomivhd49
Tags: 2.4.0.2-1
* [6e140ac] Imported Upstream version 2.4.0.2
* [2049fc8] Update Build-Depends to match control
* [93dc4d4] Install the new primitives
* [e48f40f] Fix typo dev→doc

Show diffs side-by-side

added added

removed removed

Lines of Context:
examples/lib/Data/List.agda
1
 
 
2
 
module Data.List where
3
 
 
4
 
import Prelude
5
 
import Data.Nat
6
 
import Data.Tuple
7
 
 
8
 
open Prelude
9
 
open Data.Nat
10
 
open Data.Tuple
11
 
 
12
 
infixr 50 _::_ _++_
13
 
 
14
 
data List (A : Set) : Set where
15
 
  []   : List A
16
 
  _::_ : A -> List A -> List A
17
 
 
18
 
{-# BUILTIN LIST List #-}
19
 
{-# BUILTIN NIL  []   #-}
20
 
{-# BUILTIN CONS _::_ #-}
21
 
 
22
 
length : {A : Set} -> List A -> Nat
23
 
length []        = 0
24
 
length (_ :: xs) = 1 + length xs
25
 
 
26
 
map : {A B : Set} -> (A -> B) -> List A -> List B
27
 
map f []        = []
28
 
map f (x :: xs) = f x :: map f xs
29
 
 
30
 
_++_ : {A : Set} -> List A -> List A -> List A
31
 
[]        ++ ys = ys
32
 
(x :: xs) ++ ys = x :: (xs ++ ys)
33
 
 
34
 
zipWith : {A B C : Set} -> (A -> B -> C) -> List A -> List B -> List C
35
 
zipWith f []        []        = []
36
 
zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys
37
 
zipWith f []        (_ :: _)  = []
38
 
zipWith f (_ :: _)  []        = []
39
 
 
40
 
foldr : {A B : Set} -> (A -> B -> B) -> B -> List A -> B
41
 
foldr f z []        = z
42
 
foldr f z (x :: xs) = f x (foldr f z xs)
43
 
 
44
 
foldl : {A B : Set} -> (B -> A -> B) -> B -> List A -> B
45
 
foldl f z []        = z
46
 
foldl f z (x :: xs) = foldl f (f z x) xs
47
 
 
48
 
replicate : {A : Set} -> Nat -> A -> List A
49
 
replicate  zero   x = []
50
 
replicate (suc n) x = x :: replicate n x
51
 
 
52
 
iterate : {A : Set} -> Nat -> (A -> A) -> A -> List A
53
 
iterate  zero   f x = []
54
 
iterate (suc n) f x = x :: iterate n f (f x)
55
 
 
56
 
splitAt : {A : Set} -> Nat -> List A -> List A × List A
57
 
splitAt  zero   xs        = < [] , xs >
58
 
splitAt (suc n) []        = < [] , [] >
59
 
splitAt (suc n) (x :: xs) = add x $ splitAt n xs
60
 
  where
61
 
    add : _ -> List _ × List _ -> List _ × List _
62
 
    add x < ys , zs > = < x :: ys , zs >
63
 
 
64
 
reverse : {A : Set} -> List A -> List A
65
 
reverse xs = foldl (flip _::_) [] xs
66