From fea8e8284b55dc64fbe2d39a203c3443beea9261 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 17 Apr 2024 19:35:18 +0000 Subject: deprecate Bvector diff --git a/doc/changelog/11-standard-library/18947-deprecate-Bvector.rst b/doc/changelog/11-standard-library/18947-deprecate-Bvector.rst new file mode 100644 index 0000000..eacd903 --- /dev/null +++ b/doc/changelog/11-standard-library/18947-deprecate-Bvector.rst @@ -0,0 +1,3 @@ +- **Deprecated:** ``Bool.Bvector``. Users are encouraged to consider ``list bool`` instead. Please open an issue if you would like to keep using ``Bvector``. + (`#18947 `_, + by Andres Erbsen). diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index 8016e9b..8a42d5b 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -10,7 +10,8 @@ (** N.B.: Using this encoding of bit vectors is discouraged. See . *) -Attributes warn(cats="stdlib vector", note="Using Vector.t is known to be technically difficult, see ."). +Attributes deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector."). +Local Set Warnings "-deprecated". (** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *) @@ -50,53 +51,72 @@ NOTA BENE: all shift operations expect predecessor of size as parameter (they only work on non-empty vectors). *) +#[deprecated(since="8.20", note="Consider [list bool] instead. Please open an issue if you would like to keep using Bvector.")] Definition Bvector := Vector.t bool. +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Definition Bnil := @Vector.nil bool. +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Definition Bcons := @Vector.cons bool. +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Definition Bvect_true := Vector.const true. +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Definition Bvect_false := Vector.const false. +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Definition Blow := @Vector.hd bool. +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Definition Bhigh := @Vector.tl bool. +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Definition Bsign := @Vector.last bool. +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Definition Bneg := @Vector.map _ _ negb. +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Definition BVand := @Vector.map2 _ _ _ andb. +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Definition BVor := @Vector.map2 _ _ _ orb. +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Definition BVxor := @Vector.map2 _ _ _ xorb. +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Definition BVeq m n := @Vector.eqb bool eqb m n. +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Definition BshiftL (n:nat) (bv:Bvector (S n)) (carry:bool) := Bcons carry n (Vector.shiftout bv). +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Definition BshiftRl (n:nat) (bv:Bvector (S n)) (carry:bool) := Bhigh (S n) (Vector.shiftin carry bv). +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Definition BshiftRa (n:nat) (bv:Bvector (S n)) := Bhigh (S n) (Vector.shiftrepeat bv). +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Fixpoint BshiftL_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) := match p with | O => bv | S p' => BshiftL n (BshiftL_iter n bv p') false end. +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Fixpoint BshiftRl_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) := match p with | O => bv | S p' => BshiftRl n (BshiftRl_iter n bv p') false end. +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) := match p with | O => bv @@ -108,10 +128,15 @@ End BOOLEAN_VECTORS. Module BvectorNotations. Declare Scope Bvector_scope. Delimit Scope Bvector_scope with Bvector. +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Notation "^~ x" := (Bneg _ x) (at level 35, right associativity) : Bvector_scope. +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Infix "^&" := (BVand _) (at level 40, left associativity) : Bvector_scope. +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Infix "^⊕" := (BVxor _) (at level 45, left associativity) : Bvector_scope. +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Infix "^|" := (BVor _) (at level 50, left associativity) : Bvector_scope. +#[deprecated(since="8.20", note="Consider [list bool] instead. See for details. Please open an issue if you would like to keep using Bvector.")] Infix "=?" := (BVeq _ _) (at level 70, no associativity) : Bvector_scope. Open Scope Bvector_scope. End BvectorNotations. -- cgit v0.10.2-6-g49f6