Changeset 2782 for src/ASM/BitVector.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/BitVector.ma

    r2645 r2782  
    5858  λm, n: nat.
    5959  λb: BitVector n. pad_vector ? false m n b.
    60 
    61 (* jpb: we already have bitvector_of_nat and friends in the library, maybe
    62  * we should unify this in some way *) 
    63 let rec nat_to_bv (n : nat) (k : nat) on n : BitVector n ≝
    64   match n with
    65   [ 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 with
    72   [ VEmpty ⇒ 0
    73   | VCons n' x b' ⇒ (if x then 1 else 0) + bv_to_nat n' b' * 2].
    7460
    7561(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
Note: See TracChangeset for help on using the changeset viewer.