Ignore:
Timestamp:
Mar 6, 2013, 2:59:22 AM (7 years ago)
Author:
sacerdot
Message:

Bug fixed: in BitVector?.ma the functions bv_to_nat and nat_to_bv were
using the wrong indianess. They were also redundant with the good
(but inefficient) ones in Arithmetic.ma.

On a simple test the compiled code runs (I have not checked the
result).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/bitVector.ml

    r2773 r2780  
    6565  Vector.pad_vector Bool.False m n b
    6666
    67 (** val nat_to_bv : Nat.nat -> Nat.nat -> bitVector **)
    68 let rec nat_to_bv n k =
    69   match n with
    70   | Nat.O -> Vector.VEmpty
    71   | Nat.S n' ->
    72     Vector.VCons (n',
    73       (Nat.eqb (Util.modulus k (Nat.S (Nat.S Nat.O))) (Nat.S Nat.O)),
    74       (nat_to_bv n' (Util.division k (Nat.S (Nat.S Nat.O)))))
    75 
    76 (** val bv_to_nat : Nat.nat -> bitVector -> Nat.nat **)
    77 let rec bv_to_nat n = function
    78 | Vector.VEmpty -> Nat.O
    79 | Vector.VCons (n', x, b') ->
    80   Nat.plus
    81     (match x with
    82      | Bool.True -> Nat.S Nat.O
    83      | Bool.False -> Nat.O)
    84     (Nat.times (bv_to_nat n' b') (Nat.S (Nat.S Nat.O)))
    85 
    8667(** val conjunction_bv : Nat.nat -> bitVector -> bitVector -> bitVector **)
    8768let conjunction_bv n b c =
Note: See TracChangeset for help on using the changeset viewer.