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