Changeset 236 for Deliverables/D4.1/Matita/BitVector.ma
 Timestamp:
 Nov 12, 2010, 4:01:48 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r235 r236 1 (* ===================================== *) 2 (* BitVector.ma: Fixed length bitvectors, and common operations on them. *) 3 (* ===================================== *) 4 1 5 include "Vector.ma". 2 6 include "List.ma". 3 7 include "Nat.ma". 4 8 include "Bool.ma". 9 10 (* ===================================== *) 11 (* Common synonyms. *) 12 (* ===================================== *) 5 13 6 14 ndefinition BitVector ≝ λn: Nat. Vector Bool n. … … 11 19 ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))). 12 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 *) 13 28 ndefinition zero ≝ 14 29 λn: Nat. 15 30 replicate Bool n False. 16 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 *) 17 46 ndefinition conjunction ≝ 18 47 λn: Nat. … … 20 49 λc: BitVector n. 21 50 zip Bool Bool Bool n conjunction b c. 22 51 52 (* 53 @name: inclusive_disjunction 54 @desc: The logical inclusive disjunction of two bitvectors of length 55 <tt>n</tt>. 56 *) 23 57 ndefinition inclusive_disjunction ≝ 24 58 λn: Nat. … … 27 61 zip Bool Bool Bool n inclusive_disjunction b c. 28 62 63 (* 64 @name: exclusive_disjunction 65 @desc: The logical exclusive disjunction of two bitvectors of length 66 <tt>n</tt>. (XOR). 67 *) 29 68 ndefinition exclusive_disjunction ≝ 30 69 λn: Nat. … … 33 72 zip Bool Bool Bool n exclusive_disjunction b c. 34 73 74 (* 75 @name: complement 76 @desc: The logical complement of a bitvector of length <tt>n</tt>. 77 *) 35 78 ndefinition complement ≝ 36 79 λn: Nat. 37 80 λb: BitVector n. 38 81 map Bool Bool n (negation) b. 82 83 (* ===================================== *) 84 (* Conversions to and from lists and natural numbers. *) 85 (* ===================================== *) 39 86 40 87 ndefinition divide_with_remainder ≝ 41 88 λm, n: Nat. 42 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. 43 100 44 101 nlet rec bitvector_of_nat_aux (n: Nat) on n ≝ … … 58 115 ] 59 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.
Note: See TracChangeset
for help on using the changeset viewer.