git.iko.soy/Idris-dev
on master help sign in
Additions to the vect.idr file.
1e6c93cDominic Mulligan
lib/prelude/vect.idr+115−30
compare with master
unifiedsplit
@@ -1,56 +1,141 @@
1module prelude.vect
1module prelude.vect
2
2
3−import prelude.nat
4import prelude.fin
3import prelude.fin
4+import prelude.list
5+import prelude.nat
5
6
6%access public
7%access public
7
8
8infixr 10 ::
9infixr 10 ::
9
10
10data Vect : Set -> Nat -> Set where
11data Vect : Set -> Nat -> Set where
11− Nil : Vect a 0
12+ Nil : Vect a O
12− (::) : a -> Vect a k -> Vect a (1 + k)
13+ (::) : a -> Vect a n -> Vect a (S n)
14+
15+--------------------------------------------------------------------------------
16+-- Indexing into vectors
17+--------------------------------------------------------------------------------
13
18
14tail : Vect a (S n) -> Vect a n
19tail : Vect a (S n) -> Vect a n
15−tail (x :: xs) = xs
20+tail (x::xs) = xs
16−
21+tail [] impossible
22+
23+head : Vect a (S n) -> a
24+head (x::xs) = x
25+head [] impossible
26+
27+last : Vect a (S n) -> a
28+last [] impossible
29+last (x::[]) = x
30+last (x::y::ys) = last $ y::ys
31+
32+init : Vect a (S n) -> Vect a n
33+init [] impossible
34+init (x::[]) = []
35+init (x::y::ys) = x :: init (y::ys)
36+
17−lookup : Fin n -> Vect a n -> a
37+index : Fin n -> Vect a n -> a
18−lookup fO (x :: xs) = x
38+index fO (x::xs) = x
19−lookup (fS k) (x :: xs) = lookup k xs
39+index (fS k) (x::xs) = index k xs
20−lookup fO [] impossible
40+index fO [] impossible
21−lookup (fS _) [] impossible
41+index (fS _) [] impossible
22−
42+
43+--------------------------------------------------------------------------------
44+-- Conversions to and from list
45+--------------------------------------------------------------------------------
46+
47+toList : Vect a n -> List a
48+toList [] = []
49+toList (x::xs) = x :: toList xs
50+
51+fromList : (l : List a) -> Vect a (length l)
52+fromList [] = []
53+fromList (x::xs) = x :: fromList xs
54+
55+--------------------------------------------------------------------------------
56+-- Building bigger vectors
57+--------------------------------------------------------------------------------
58+
59+(++) : Vect a m -> Vect a n -> Vect a (m + n)
60+(++) [] ys = ys
61+(++) (x::xs) ys = x :: xs ++ ys
62+
63+--------------------------------------------------------------------------------
64+-- Transformations
65+--------------------------------------------------------------------------------
66+
67+reverse : Vect a n -> Vect a n
68+reverse = reverse' []
69+ where
23−(++) : Vect a n -> Vect a m -> Vect a (n + m)
70+ reverse' : Vect a m -> Vect a n -> Vect a (m + n)
24−(++) [] ys = ys
71+ reverse' acc [] ?= acc
72+ reverse' acc (x::xs) ?= reverse' (x::acc) xs
73+
74+--------------------------------------------------------------------------------
75+-- Maps
76+--------------------------------------------------------------------------------
77+
78+map : (a -> b) -> Vect a n -> Vect b n
79+map f [] = []
25−(++) (x :: xs) ys = x :: xs ++ ys
80+map f (x::xs) = f x :: map f xs
81+
82+--------------------------------------------------------------------------------
83+-- Filters
84+--------------------------------------------------------------------------------
26
85
27filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)
86filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)
28filter p [] = ( _ ** [] )
87filter p [] = ( _ ** [] )
29−filter p (x :: xs)
88+filter p (x::xs) with (filter p xs)
30− = let (_ ** xs') = filter p xs in
89+ | (_ ** tail) =
31− if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
90+ if p x then
91+ (_ ** x::tail)
92+ else
93+ (_ ** tail)
32
94
33−map : (a -> b) -> Vect a n -> Vect b n
95+--------------------------------------------------------------------------------
34−map f [] = []
96+-- Membership tests
35−map f (x :: xs) = f x :: map f xs
97+--------------------------------------------------------------------------------
36
98
37−reverse : Vect a n -> Vect a n
99+elemBy : (a -> a -> Bool) -> a -> Vect a n -> Bool
38−reverse xs = revAcc [] xs where
100+elemBy p e [] = False
101+elemBy p e (x::xs) with (p e x)
102+ | True = True
103+ | False = elemBy p e xs
104+
105+elem : Eq a => a -> Vect a n -> Bool
106+elem = elemBy (==)
107+
108+lookupBy : (a -> a -> Bool) -> a -> Vect (a, b) n -> Maybe b
109+lookupBy p e [] = Nothing
110+lookupBy p e ((l, r)::xs) with (p e l)
111+ | True = Just r
112+ | False = lookupBy p e xs
113+
114+lookup : Eq a => a -> Vect (a, b) n -> Maybe b
115+lookup = lookupBy (==)
116+
39− revAcc : Vect a n -> Vect a m -> Vect a (n + m)
117+hasAnyBy : (a -> a -> Bool) -> Vect a m -> Vect a n -> Bool
40− revAcc acc [] ?= acc
118+hasAnyBy p elems [] = False
41− revAcc acc (x :: xs) ?= revAcc (x :: acc) xs
119+hasAnyBy p elems (x::xs) with (elemBy p x elems)
120+ | True = True
121+ | False = hasAnyBy p elems xs
122+
123+hasAny : Eq a => Vect a m -> Vect a n -> Bool
124+hasAny = hasAnyBy (==)
42
125
126+--------------------------------------------------------------------------------
43−---------- Proofs ----------
127+-- Proofs
128+--------------------------------------------------------------------------------
44
129
45−revAcc_lemma_2 = proof {
130+prelude.vect.reverse'_lemma_2 = proof {
46 intros;
131 intros;
47− rewrite plusSuccRightSucc n k;
132+ rewrite (plusSuccRightSucc m n1);
48 exact value;
133 exact value;
49}
134}
50
135
51−revAcc_lemma_1 = proof {
136+prelude.vect.reverse'_lemma_1 = proof {
52 intros;
137 intros;
53− rewrite sym (plusZeroRightNeutral n);
138+ rewrite sym (plusZeroRightNeutral m);
54 exact value;
139 exact value;
55}
140}
56
141