Changeset 2782
 Timestamp:
 Mar 6, 2013, 3:03:02 AM (7 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r2700 r2782 145 145 \fst (sub_with_borrows n b (zero n) true). 146 146 147 (* The following implementation is extremely inefficient*) 147 148 let rec bitvector_of_nat_aux (n,m:nat) (v:BitVector n) on m : BitVector n ≝ 148 149 match m with … … 153 154 definition bitvector_of_nat : ∀n:nat. nat → BitVector n ≝ 154 155 λn,m. bitvector_of_nat_aux n m (zero n). 156 157 (* This one by Paolo is efficient, but it is for the opposite indianess. 158 (* jpb: we already have bitvector_of_nat and friends in the library, maybe 159  * we should unify this in some way *) 160 let rec nat_to_bv (n : nat) (k : nat) on n : BitVector n ≝ 161  match n with 162  [ O ⇒ VEmpty ? 163   S n' ⇒ 164  eqb (k mod 2) 1 ::: nat_to_bv n' (k ÷ 2) 165  ]. 166  167 let rec bv_to_nat (n : nat) (b : BitVector n) on b : nat ≝ 168  match b with 169  [ VEmpty ⇒ 0 170   VCons n' x b' ⇒ (if x then 1 else 0) + bv_to_nat n' b' * 2]. 171  172 *) 155 173 156 174 let rec nat_of_bitvector_aux (n,m:nat) (v:BitVector n) on v : nat ≝ 
src/ASM/BitVector.ma
r2645 r2782 58 58 λm, n: nat. 59 59 λb: BitVector n. pad_vector ? false m n b. 60 61 (* jpb: we already have bitvector_of_nat and friends in the library, maybe62 * we should unify this in some way *)63 let rec nat_to_bv (n : nat) (k : nat) on n : BitVector n ≝64 match n with65 [ O ⇒ VEmpty ?66  S n' ⇒67 eqb (k mod 2) 1 ::: nat_to_bv n' (k ÷ 2)68 ].69 70 let rec bv_to_nat (n : nat) (b : BitVector n) on b : nat ≝71 match b with72 [ VEmpty ⇒ 073  VCons n' x b' ⇒ (if x then 1 else 0) + bv_to_nat n' b' * 2].74 60 75 61 (* ===================================== *)
Note: See TracChangeset
for help on using the changeset viewer.