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  

5  include "Cartesian.ma". 

6  include "List.ma". 

7  

8  include "logic/pts.ma". 

9  include "basics/eq.ma". 

10  include "basics/bool.ma". 

11  include "arithmetics/nat.ma". 

12  include "nat/plus.ma". 

13  include "nat/minus.ma". 

14  

15  ninductive 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  

19  nlet 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  

25  nlet 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  

32  nlet 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  

39  nlet 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  

45  nlet 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.