82 lines
2.3 KiB
Coq
82 lines
2.3 KiB
Coq
Require Bvector. (* stdlib uses LSB first (little-endian) representation *)
|
|
Require Vector.
|
|
Require List.
|
|
|
|
(* Convert a nat list to a bitvector. Non-zero values are considered true *)
|
|
Fixpoint list2Bvec_aux (l:list nat) : Bvector.Bvector (List.length l) :=
|
|
match l return Bvector.Bvector (List.length l) with
|
|
| List.cons O xs =>
|
|
Bvector.Bcons false _ (list2Bvec_aux xs)
|
|
| List.cons _ xs =>
|
|
Bvector.Bcons true _ (list2Bvec_aux xs)
|
|
| List.nil => Bvector.Bnil
|
|
end.
|
|
Definition list2Bvec (l:list nat) : Bvector.Bvector (List.length (List.rev l)) :=
|
|
list2Bvec_aux (List.rev l).
|
|
|
|
(* Convert a bitvector to nat. Little-endian representation assumed *)
|
|
Fixpoint bvec2nat_aux {n:nat} (cur:nat) (bv:Bvector.Bvector n): nat :=
|
|
match bv with
|
|
| Vector.cons _ x _ xs =>
|
|
if x then (Nat.pow 2 cur) + bvec2nat_aux (S cur) xs
|
|
else bvec2nat_aux (S cur) xs
|
|
| Vector.nil _ => 0
|
|
end.
|
|
Definition bvec2nat {n:nat} (bv:Bvector.Bvector n): nat := bvec2nat_aux 0 bv.
|
|
|
|
(* Find nth bit of a bitvector *)
|
|
Definition Bnth {z i:nat} (bv: Bvector.Bvector z) (pf:i<z): bool :=
|
|
Vector.nth_order bv pf.
|
|
|
|
(* Find list of set bits in a bitvector *)
|
|
Fixpoint find_set_bits {z:nat} (bv: Bvector.Bvector z) : list nat :=
|
|
match bv with
|
|
| Vector.cons _ x _ xs =>
|
|
if x then List.cons (z-1) (find_set_bits xs)
|
|
else (find_set_bits xs)
|
|
| Vector.nil _ => List.nil
|
|
end.
|
|
|
|
|
|
|
|
Require Import List.
|
|
Import ListNotations.
|
|
Compute list2Bvec [0;0;1;0]. (* 0100₂ ie, 4₁₀ *)
|
|
Check Bvector.BshiftL _ (list2Bvec [0;0;1;0]) false.
|
|
|
|
Check Vector.shiftrepeat (Vector.cons _ 0 _ (Vector.nil _)).
|
|
|
|
Require Import Vector.
|
|
|
|
|
|
Import VectorNotations.
|
|
Compute Bvector.BshiftL 1 (list2Bvec [0;0;1;0]) false.
|
|
(*
|
|
= [false; false; true; false]
|
|
: Bvector (length [0; 0; 1; 0])
|
|
*)
|
|
Compute bvec2nat (list2Bvec [0;0;1;0]).
|
|
(* = 2 : nat *)
|
|
Compute bvec2nat (list2Bvec [0;1;0;0]).
|
|
(* = 4 : nat *)
|
|
|
|
Compute Bnth (list2Bvec [0;0;1;0]) (_:2<_).
|
|
(* = true : bool *)
|
|
Compute Bnth (list2Bvec [0;0;1;0]) (_:1<_).
|
|
(* = false : bool *)
|
|
|
|
|
|
Compute find_set_bits (list2Bvec [0;0;1;0]). (* [2] : list nat *)
|
|
Compute find_set_bits (list2Bvec [1;0;1;0]). (* [2; 0] : list nat *)
|
|
|
|
Check Bvector.BshiftL .
|
|
|
|
Check Bcons.
|
|
|
|
Check Nat.pow.
|
|
Compute Nat.pow 2 3.
|
|
Check Vector.nth_order.
|
|
Check Vector.nth_order (list2Bvec [0;0;1;0]).
|
|
Compute Vector.nth_order (list2Bvec [0;0;1;0]) (_:0<_).
|
|
|