Skip to content

Commit

Permalink
Merge PR coq#18947: deprecate Bvector
Browse files Browse the repository at this point in the history 
Reviewed-by: proux01
Co-authored-by: proux01 <proux01@users.noreply.github.com>
  • Loading branch information
@coqbot-app @proux01
coqbot-app[bot] and proux01 committed Apr 26, 2024
2 parents c5614d0 + fea8e82 commit 5e0a71c
Show file tree
Hide file tree
Showing 2 changed files with 29 additions and 1 deletion.
3 changes: 3 additions & 0 deletions doc/changelog/11-standard-library/18947-deprecate-Bvector.rst
View file
Original file line number Diff line number Diff line change
@@ -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 <https://github.com/coq/coq/pull/18947>`_,
by Andres Erbsen).
27 changes: 26 additions & 1 deletion theories/Bool/Bvector.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,8 @@

(** N.B.: Using this encoding of bit vectors is discouraged.
See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v>. *)
Attributes warn(cats="stdlib vector", note="Using Vector.t is known to be technically difficult, see <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v>.").
Attributes deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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). *)

Expand Down Expand Up @@ -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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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
Expand All @@ -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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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 <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> 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.

0 comments on commit 5e0a71c

Please sign in to comment.