@@ -1,56 +1,141 @@
11module prelude.vect
22
3−import prelude.nat
43import prelude.fin
4+import prelude.list
5+import prelude.nat
56
67%access public
78
89infixr 10 ::
910
1011data Vect : Set -> Nat -> Set where
11− Nil : Vect a 0
12− (::) : a -> Vect a k -> Vect a (1 + k)
12+ Nil : Vect a O
13+ (::) : a -> Vect a n -> Vect a (S n)
14+
15+--------------------------------------------------------------------------------
16+-- Indexing into vectors
17+--------------------------------------------------------------------------------
1318
1419tail : Vect a (S n) -> Vect a n
15−tail (x :: xs) = xs
16−
17−lookup : Fin n -> Vect a n -> a
18−lookup fO (x :: xs) = x
19−lookup (fS k) (x :: xs) = lookup k xs
20−lookup fO [] impossible
21−lookup (fS _) [] impossible
22−
23−(++) : Vect a n -> Vect a m -> Vect a (n + m)
24−(++) [] ys = ys
25−(++) (x :: xs) ys = x :: xs ++ ys
20+tail (x::xs) = xs
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+
37+index : Fin n -> Vect a n -> a
38+index fO (x::xs) = x
39+index (fS k) (x::xs) = index k xs
40+index fO [] impossible
41+index (fS _) [] impossible
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
70+ reverse' : Vect a m -> Vect a n -> Vect a (m + n)
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 [] = []
80+map f (x::xs) = f x :: map f xs
81+
82+--------------------------------------------------------------------------------
83+-- Filters
84+--------------------------------------------------------------------------------
2685
2786filter : (a -> Bool) -> Vect a n -> (p ** Vect a p)
2887filter p [] = ( _ ** [] )
29−filter p (x :: xs)
30− = let (_ ** xs') = filter p xs in
31− if (p x) then ( _ ** x :: xs' ) else ( _ ** xs' )
88+filter p (x::xs) with (filter p xs)
89+ | (_ ** tail) =
90+ if p x then
91+ (_ ** x::tail)
92+ else
93+ (_ ** tail)
3294
33−map : (a -> b) -> Vect a n -> Vect b n
34−map f [] = []
35−map f (x :: xs) = f x :: map f xs
95+--------------------------------------------------------------------------------
96+-- Membership tests
97+--------------------------------------------------------------------------------
3698
37−reverse : Vect a n -> Vect a n
38−reverse xs = revAcc [] xs where
39− revAcc : Vect a n -> Vect a m -> Vect a (n + m)
40− revAcc acc [] ?= acc
41− revAcc acc (x :: xs) ?= revAcc (x :: acc) xs
99+elemBy : (a -> a -> Bool) -> a -> Vect a n -> Bool
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+
117+hasAnyBy : (a -> a -> Bool) -> Vect a m -> Vect a n -> Bool
118+hasAnyBy p elems [] = False
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 (==)
42125
43−---------- Proofs ----------
126+--------------------------------------------------------------------------------
127+-- Proofs
128+--------------------------------------------------------------------------------
44129
45−revAcc_lemma_2 = proof {
130+prelude.vect.reverse'_lemma_2 = proof {
46131 intros;
47− rewrite plusSuccRightSucc n k;
132+ rewrite (plusSuccRightSucc m n1);
48133 exact value;
49134}
50135
51−revAcc_lemma_1 = proof {
136+prelude.vect.reverse'_lemma_1 = proof {
52137 intros;
53− rewrite sym (plusZeroRightNeutral n);
138+ rewrite sym (plusZeroRightNeutral m);
54139 exact value;
55140}
56141