source: Deliverables/D4.1/Matita/Vectors.ma @ 224

Last change on this file since 224 was 224, checked in by mulligan, 9 years ago

Changes to bit vectors and vectors.

File size: 1.5 KB
Line 
1(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
2(* Vectors.ma: Fixed length bitvectors, and routine operations on them.       *)
3(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
4
5include "Cartesian.ma".
6include "List.ma".
7
8include "logic/pts.ma".
9include "basics/eq.ma".
10include "basics/bool.ma".
11include "arithmetics/nat.ma".
12include "nat/plus.ma".
13include "nat/minus.ma".
14
15ninductive Vector (A: Type[0]): nat → Type[0] ≝
16  Empty: Vector A 0
17| Cons: ∀n: nat. A → Vector A n → Vector A (S n).
18
19nlet rec map (A: Type[0]) (B: Type[0]) (n: nat) (f: A → B) (v: Vector A n) on v ≝
20  match v with
21    [ Empty ⇒ Empty B
22    | Cons n hd tl ⇒ Cons B n (f hd) (map A B n f tl)
23    ].
24   
25nlet rec fold_right (A: Type[0]) (B: Type[0]) (n: nat)
26                    (f: A → B → B) (x: B) (v: Vector A n) on v ≝
27  match v with
28    [ Empty ⇒ x
29    | Cons n hd tl ⇒ f hd (fold_right A B n f x tl)
30    ].
31   
32nlet rec fold_left (A: Type[0]) (B: Type[0]) (n: nat)
33                    (f: A → B → A) (x: A) (v: Vector B n) on v ≝
34  match v with
35    [ Empty ⇒ x
36    | Cons n hd tl ⇒ f (fold_left A B n f x tl) hd
37    ].
38   
39nlet rec length (A: Type[0]) (n: nat) (v: Vector A n) on v ≝
40  match v with
41    [ Empty ⇒ 0
42    | Cons n hd tl ⇒ S (length A n tl)
43    ].
44
45nlet rec from_list (A: Type[0]) (l: List A) on l ≝
46  match l with
47    [ Empty ⇒ Empty A
48    | Cons hd tl ⇒ Cons (length A tl) hd (from_list A tl)
49    ].
Note: See TracBrowser for help on using the repository browser.