Changeset 2782 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
Mar 6, 2013, 3:03:02 AM (7 years ago)
Author:
sacerdot
Message:
  1. Paolo's bv_of_nat/nat_of_bv in BitVector? used to work with the wrong indianess! removed
  2. Dominic's nat_of_bitvector/bitvector_of_nat in Arithmetic.ma are inefficient. For the time being I have pasted there Paolo's code in a comment.
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r2700 r2782  
    145145    \fst (sub_with_borrows n b (zero n) true).
    146146
     147(* The following implementation is extremely inefficient*)
    147148let rec bitvector_of_nat_aux (n,m:nat) (v:BitVector n) on m : BitVector n ≝
    148149  match m with
     
    153154definition bitvector_of_nat : ∀n:nat. nat → BitVector n ≝
    154155  λ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*)
    155173
    156174let rec nat_of_bitvector_aux (n,m:nat) (v:BitVector n) on v : nat ≝
Note: See TracChangeset for help on using the changeset viewer.