1 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
2 | (* BitVector.ma: Fixed length bitvectors, and common operations on them. *) |
---|
3 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
4 | |
---|
5 | include "Vector.ma". |
---|
6 | include "List.ma". |
---|
7 | include "Nat.ma". |
---|
8 | include "Bool.ma". |
---|
9 | |
---|
10 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
11 | (* Common synonyms. *) |
---|
12 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
13 | |
---|
14 | ndefinition BitVector ≝ λn: Nat. Vector Bool n. |
---|
15 | ndefinition Bit ≝ BitVector (S Z). |
---|
16 | ndefinition Nibble ≝ BitVector (S (S (S (S Z)))). |
---|
17 | ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))). |
---|
18 | ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))). |
---|
19 | ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))). |
---|
20 | |
---|
21 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
22 | (* Creating bitvectors from scratch. *) |
---|
23 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
24 | |
---|
25 | (* @name: zero |
---|
26 | @desc: Produces a bitvector containing <tt>n</tt> copies of <tt>False</tt>. |
---|
27 | *) |
---|
28 | ndefinition zero ≝ |
---|
29 | λn: Nat. |
---|
30 | replicate Bool n False. |
---|
31 | |
---|
32 | ndefinition max ≝ |
---|
33 | λn: Nat. |
---|
34 | replicate Bool n True. |
---|
35 | |
---|
36 | ndefinition append ≝ append. |
---|
37 | |
---|
38 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
39 | (* Logical operations. *) |
---|
40 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
41 | |
---|
42 | (* |
---|
43 | @name: conjunction |
---|
44 | @desc: The logical conjunction of two bitvectors of length <tt>n</tt>. |
---|
45 | *) |
---|
46 | ndefinition conjunction ≝ |
---|
47 | λn: Nat. |
---|
48 | λb: BitVector n. |
---|
49 | λc: BitVector n. |
---|
50 | zip Bool Bool Bool n conjunction b c. |
---|
51 | |
---|
52 | (* |
---|
53 | @name: inclusive_disjunction |
---|
54 | @desc: The logical inclusive disjunction of two bitvectors of length |
---|
55 | <tt>n</tt>. |
---|
56 | *) |
---|
57 | ndefinition inclusive_disjunction ≝ |
---|
58 | λn: Nat. |
---|
59 | λb: BitVector n. |
---|
60 | λc: BitVector n. |
---|
61 | zip Bool Bool Bool n inclusive_disjunction b c. |
---|
62 | |
---|
63 | (* |
---|
64 | @name: exclusive_disjunction |
---|
65 | @desc: The logical exclusive disjunction of two bitvectors of length |
---|
66 | <tt>n</tt>. (XOR). |
---|
67 | *) |
---|
68 | ndefinition exclusive_disjunction ≝ |
---|
69 | λn: Nat. |
---|
70 | λb: BitVector n. |
---|
71 | λc: BitVector n. |
---|
72 | zip Bool Bool Bool n exclusive_disjunction b c. |
---|
73 | |
---|
74 | (* |
---|
75 | @name: complement |
---|
76 | @desc: The logical complement of a bitvector of length <tt>n</tt>. |
---|
77 | *) |
---|
78 | ndefinition complement ≝ |
---|
79 | λn: Nat. |
---|
80 | λb: BitVector n. |
---|
81 | map Bool Bool n (negation) b. |
---|
82 | |
---|
83 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
84 | (* Conversions to and from lists and natural numbers. *) |
---|
85 | (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *) |
---|
86 | |
---|
87 | ndefinition divide_with_remainder ≝ |
---|
88 | λm, n: Nat. |
---|
89 | mk_Cartesian Nat Nat (m ÷ n) (modulus m n). |
---|
90 | |
---|
91 | (* @name: pad |
---|
92 | @desc: Pads the front of a bitvector of length <tt>n</tt> with <tt>m</tt> |
---|
93 | copies of <tt>False</tt>. |
---|
94 | *) |
---|
95 | ndefinition pad ≝ |
---|
96 | λm, n: Nat. |
---|
97 | λb: BitVector n. |
---|
98 | let padding ≝ replicate Bool m False in |
---|
99 | append Bool m n padding b. |
---|
100 | |
---|
101 | nlet rec bitvector_of_nat_aux (n: Nat) on n ≝ |
---|
102 | let div_rem ≝ divide_with_remainder n (S (S Z)) in |
---|
103 | let div ≝ first Nat Nat div_rem in |
---|
104 | let rem ≝ second Nat Nat div_rem in |
---|
105 | match div with |
---|
106 | [ Z ⇒ |
---|
107 | match rem with |
---|
108 | [ Z ⇒ Empty Bool |
---|
109 | | S r ⇒ True :: (bitvector_of_nat_aux Z) |
---|
110 | ] |
---|
111 | | S d ⇒ |
---|
112 | match rem with |
---|
113 | [ Z ⇒ False :: (bitvector_of_nat_aux (S d)) |
---|
114 | | S r ⇒ True :: (bitvector_of_nat_aux (S d)) |
---|
115 | ] |
---|
116 | ]. |
---|
117 | |
---|
118 | (* @name: bitvector_of_nat |
---|
119 | @desc: Constructs a bitvector whose integer value is the same as <tt>m</tt>. |
---|
120 | Size of the resulting bitvector is clamped to <tt>n</tt>. |
---|
121 | *) |
---|
122 | ndefinition bitvector_of_nat ≝ |
---|
123 | λm, n: Nat. |
---|
124 | let biglist ≝ reverse Bool (bitvector_of_nat_aux m) in |
---|
125 | let size ≝ length Bool biglist in |
---|
126 | let bvector ≝ bitvector_of_list Bool biglist in |
---|
127 | let difference ≝ n - size in |
---|
128 | pad difference size bvector. |
---|
129 | |
---|
130 | ndefinition list_of_bitvector ≝ list_of_vector. |
---|
131 | ndefinition bitvector_of_list ≝ vector_of_list. |
---|