← Back to branch summary

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

« back to all changes in this revision

Viewing changes to examples/simple-lib/Lib/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/simple-lib/Lib/List.agda
1
 
 
2
 
module Lib.List where
3
 
 
4
 
open import Lib.Prelude
5
 
open import Lib.Id
6
 
 
7
 
infix  30 _∈_
8
 
infixr 40 _::_ _++_
9
 
infix  45 _!_
10
 
 
11
 
data List (A : Set) : Set where
12
 
  []   : List A
13
 
  _::_ : A -> List A -> List A
14
 
 
15
 
{-# COMPILED_DATA List [] [] (:) #-}
16
 
{-# BUILTIN LIST List #-}
17
 
{-# BUILTIN NIL [] #-}
18
 
{-# BUILTIN CONS _::_ #-}
19
 
 
20
 
_++_ : {A : Set} -> List A -> List A -> List A
21
 
[]        ++ ys = ys
22
 
(x :: xs) ++ ys = x :: (xs ++ ys)
23
 
 
24
 
foldr : {A B : Set} -> (A -> B -> B) -> B -> List A -> B
25
 
foldr f z [] = z
26
 
foldr f z (x :: xs) = f x (foldr f z xs)
27
 
 
28
 
map : {A B : Set} -> (A -> B) -> List A -> List B
29
 
map f [] = []
30
 
map f (x :: xs) = f x :: map f xs
31
 
 
32
 
map-id : forall {A}(xs : List A) -> map id xs ≡ xs
33
 
map-id [] = refl
34
 
map-id (x :: xs) with map id xs | map-id xs
35
 
... | .xs | refl = refl
36
 
 
37
 
data _∈_ {A : Set} : A -> List A -> Set where
38
 
  hd : forall {x xs}   ->           x ∈ x :: xs
39
 
  tl : forall {x y xs} -> x ∈ xs -> x ∈ y :: xs
40
 
 
41
 
data All {A : Set}(P : A -> Set) : List A -> Set where
42
 
  []   : All P []
43
 
  _::_ : forall {x xs} -> P x -> All P xs -> All P (x :: xs)
44
 
 
45
 
head : forall {A}{P : A -> Set}{x xs} -> All P (x :: xs) -> P x
46
 
head (x :: xs) = x
47
 
 
48
 
tail : forall {A}{P : A -> Set}{x xs} -> All P (x :: xs) -> All P xs
49
 
tail (x :: xs) = xs
50
 
 
51
 
_!_ : forall {A}{P : A -> Set}{x xs} -> All P xs -> x ∈ xs -> P x
52
 
xs ! hd   = head xs
53
 
xs ! tl n = tail xs ! n
54
 
 
55
 
tabulate : forall {A}{P : A -> Set}{xs} -> ({x : A} -> x ∈ xs -> P x) -> All P xs
56
 
tabulate {xs = []}      f = [] 
57
 
tabulate {xs = x :: xs} f = f hd :: tabulate (f ∘ tl)
58
 
 
59
 
mapAll : forall {A B}{P : A -> Set}{Q : B -> Set}{xs}(f : A -> B) ->
60
 
         ({x : A} -> P x -> Q (f x)) -> All P xs -> All Q (map f xs)
61
 
mapAll f h [] = []
62
 
mapAll f h (x :: xs) = h x :: mapAll f h xs
63
 
 
64
 
mapAll- : forall {A}{P Q : A -> Set}{xs} ->
65
 
          ({x : A} -> P x -> Q x) -> All P xs -> All Q xs
66
 
mapAll- {xs = xs} f zs with map id xs | map-id xs | mapAll id f zs
67
 
... | .xs | refl | r = r
68
 
 
69
 
infix 20 _⊆_
70
 
 
71
 
data _⊆_ {A : Set} : List A -> List A -> Set where
72
 
  stop : [] ⊆ []
73
 
  drop : forall {xs y ys} -> xs ⊆ ys -> xs ⊆ y :: ys
74
 
  keep : forall {x xs ys} -> xs ⊆ ys -> x :: xs ⊆ x :: ys
75
 
 
76
 
⊆-refl : forall {A}{xs : List A} -> xs ⊆ xs
77
 
⊆-refl {xs = []}      = stop
78
 
⊆-refl {xs = x :: xs} = keep ⊆-refl
79
 
 
80
 
_∣_ : forall {A}{P : A -> Set}{xs ys} -> All P ys -> xs ⊆ ys -> All P xs
81
 
[]        ∣ stop   = []
82
 
(x :: xs) ∣ drop p = xs ∣ p
83
 
(x :: xs) ∣ keep p = x :: (xs ∣ p)