← Back to branch summary

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

« back to all changes in this revision

Viewing changes to test/epic/Prelude/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:
test/epic/Prelude/List.agda
1
 
module Prelude.List where
2
 
 
3
 
open import Prelude.Bool
4
 
open import Prelude.Nat
5
 
open import Prelude.Fin
6
 
 
7
 
infixr 40 _::_
8
 
 
9
 
data List (A : Set) : Set where
10
 
  []   : List A
11
 
  _::_ : A -> List A -> List A
12
 
 
13
 
{-# BUILTIN LIST List #-}
14
 
{-# BUILTIN NIL [] #-}
15
 
{-# BUILTIN CONS _::_ #-}
16
 
 
17
 
infixr 30 _++_
18
 
 
19
 
_++_ : {A : Set} -> List A -> List A -> List A
20
 
[]        ++ ys = ys
21
 
(x :: xs) ++ ys = x :: (xs ++ ys) 
22
 
 
23
 
snoc : {A : Set} -> List A -> A -> List A
24
 
snoc []        e = e :: []
25
 
snoc (x :: xs) e = x :: snoc xs e
26
 
 
27
 
length : {A : Set} -> List A -> Nat
28
 
length [] = 0
29
 
length (x :: xs) = 1 + length xs
30
 
 
31
 
zipWith : ∀ {A B C} -> (A -> B -> C) -> List A -> List B -> List C
32
 
zipWith f (x :: xs) (y :: ys) = f x y :: zipWith f xs ys
33
 
zipWith _ _ _ = []
34
 
 
35
 
map : ∀ {A B} -> (A -> B) -> List A -> List B
36
 
map _ []        = []
37
 
map f (x :: xs) = f x :: map f xs
38
 
 
39
 
mapIgen : ∀ {A B} -> (A -> B) -> List A -> List B
40
 
mapIgen = map
41
 
 
42
 
_!_ : ∀ {A} -> (xs : List A) -> Fin (length {A} xs) -> A
43
 
_!_ {A} (x :: xs) (fz .{length xs})   = x
44
 
_!_ {A} (x :: xs) (fs .{length xs} n) = _!_ {A} xs n
45
 
_!_ {A} [] ()
46
 
 
47
 
_[_]=_ : {A : Set} -> (xs : List A) -> Fin (length xs) -> A -> List A
48
 
(a :: as) [ fz ]= e = e :: as
49
 
(a :: as) [ fs n ]= e = a :: (as [ n ]= e)
50
 
[] [ () ]= e
51
 
 
52
 
listEq : {A : Set} -> (A -> A -> Bool) -> List A -> List A -> Bool
53
 
listEq _    []        [] = true
54
 
listEq _==_ (a :: as) (b :: bs) with a == b
55
 
... | true  = listEq _==_ as bs
56
 
... | false = false
57
 
listEq _ _ _ = false
58
 
 
59
 
tail : {A : Set} -> List A -> List A
60
 
tail [] = []
61
 
tail (x :: xs) = xs
62
 
 
63
 
reverse : {A : Set} -> List A -> List A
64
 
reverse [] = []
65
 
reverse (x :: xs) = reverse xs ++ (x :: [])
66
 
 
67
 
init : {A : Set} -> List A -> List A
68
 
init xs = reverse (tail (reverse xs))
69
 
 
70
 
filter : {A : Set} -> (A -> Bool) -> List A -> List A
71
 
filter p [] = []
72
 
filter p (a :: as) with p a
73
 
... | true  = a :: filter p as
74
 
... | false = filter p as