chore: move BitVec to top level namespace

Motivation: `Nat`, `Int`, `Fin`, `UInt??` are already in the top level
namespace. We will eventually define `UInt??` and `Int??` using `BitVec`.

src/Init/Data/BitVec/Basic.lean

@@ -9,8 +9,6 @@ import Init.Data.Fin.Basic
 import Init.Data.Nat.Bitwise.Lemmas
 import Init.Data.Nat.Power2
 
-namespace Std
-
 /-!
 We define bitvectors. We choose the `Fin` representation over others for its relative efficiency
 (Lean has special support for `Nat`), alignment with `UIntXY` types which are also represented
@@ -167,7 +165,7 @@ protected def toHex {n : Nat} (x : BitVec n) : String :=
   let t := (List.replicate ((n+3) / 4 - s.length) '0').asString
   t ++ s
 
-instance : Repr (BitVec n) where reprPrec a _ := "0x" ++ (a.toHex : Format) ++ "#" ++ repr n
+instance : Repr (BitVec n) where reprPrec a _ := "0x" ++ (a.toHex : Std.Format) ++ "#" ++ repr n
 instance : ToString (BitVec n) where toString a := toString (repr a)
 
 end repr_toString
@@ -607,3 +605,5 @@ section normalization_eqs
 @[simp] theorem mul_eq (x y : BitVec w)                   : BitVec.mul x y = x * y            := rfl
 @[simp] theorem zero_eq                                   : BitVec.zero n = 0#n               := rfl
 end normalization_eqs
+
+end BitVec

src/Init/Data/BitVec/Bitblast.lean

@@ -32,7 +32,7 @@ open Nat Bool
 
 /-! ### Preliminaries -/
 
-namespace Std.BitVec
+namespace BitVec
 
 private theorem testBit_limit {x i : Nat} (x_lt_succ : x < 2^(i+1)) :
     testBit x i = decide (x ≥ 2^i) := by
@@ -171,3 +171,5 @@ theorem add_eq_adc (w : Nat) (x y : BitVec w) : x + y = (adc x y false).snd := b
 /-- Subtracting `x` from the all ones bitvector is equivalent to taking its complement -/
 theorem allOnes_sub_eq_not (x : BitVec w) : allOnes w - x = ~~~x := by
   rw [← add_not_self x, BitVec.add_comm, add_sub_cancel]
+
+end BitVec

src/Init/Data/BitVec/Folds.lean

@@ -8,7 +8,7 @@ import Init.Data.BitVec.Lemmas
 import Init.Data.Nat.Lemmas
 import Init.Data.Fin.Iterate
 
-namespace Std.BitVec
+namespace BitVec
 
 /--
 iunfoldr is an iterative operation that applies a function `f` repeatedly.
@@ -57,3 +57,5 @@ theorem iunfoldr_replace
     (step : ∀(i : Fin w), f i (state i.val) = (state (i.val+1), value.getLsb i.val)) :
     iunfoldr f a = (state w, value) := by
   simp [iunfoldr.eq_test state value a init step]
+
+end BitVec

src/Init/Data/BitVec/Lemmas.lean

@@ -9,7 +9,7 @@ import Init.Data.BitVec.Basic
 import Init.Data.Fin.Lemmas
 import Init.Data.Nat.Lemmas
 
-namespace Std.BitVec
+namespace BitVec
 
 /--
 This normalized a bitvec using `ofFin` to `ofNat`.
@@ -530,3 +530,5 @@ protected theorem lt_of_le_ne (x y : BitVec n) (h1 : x <= y) (h2 : ¬ x = y) : x
   let ⟨y, lt⟩ := y
   simp
   exact Nat.lt_of_le_of_ne
+
+end BitVec

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean

@@ -8,7 +8,7 @@ import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
 import Init.Data.BitVec.Basic
 
-namespace Std.BitVec
+namespace BitVec
 open Lean Meta Simp
 
 /-- A bit-vector literal -/
@@ -30,16 +30,16 @@ private def fromOfNatExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
   return { n, value := BitVec.ofNat n v }
 
 /--
-Try to convert an `Std.BitVec.ofNat`-application into a bitvector literal.
+Try to convert an `BitVec.ofNat`-application into a bitvector literal.
 -/
 private def fromBitVecExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
-  guard (e.isAppOfArity ``Std.BitVec.ofNat 2)
+  guard (e.isAppOfArity ``BitVec.ofNat 2)
   let n ← Nat.fromExpr? e.appFn!.appArg!
   let v ← Nat.fromExpr? e.appArg!
   return { n, value := BitVec.ofNat n v }
 
 /--
-Try to convert `OfNat.ofNat`/`Std.BitVec.OfNat` application into a
+Try to convert `OfNat.ofNat`/`BitVec.OfNat` application into a
 bitvector literal.
 -/
 def fromExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
@@ -48,9 +48,9 @@ def fromExpr? (e : Expr) : SimpM (Option Literal) := OptionT.run do
 /--
 Convert a bitvector literal into an expression.
 -/
--- Using `Std.BitVec.ofNat` because it is being used in `simp` theorems
+-- Using `BitVec.ofNat` because it is being used in `simp` theorems
 def Literal.toExpr (lit : Literal) : Expr :=
-  mkApp2 (mkConst ``Std.BitVec.ofNat) (mkNatLit lit.n) (mkNatLit lit.value.toNat)
+  mkApp2 (mkConst ``BitVec.ofNat) (mkNatLit lit.n) (mkNatLit lit.value.toNat)
 
 /--
 Helper function for reducing homogenous unary bitvector operators.
@@ -305,4 +305,4 @@ builtin_simproc [simp, seval] reduceAllOnes (allOnes _) := fun e => do
   let lit : Literal := { n, value := allOnes n }
   return .done { expr := lit.toExpr }
 
-end Std.BitVec
+end BitVec

tests/lean/binop_at_pattern_issue.lean

@@ -1,5 +1,5 @@
-open Std BitVec
-def f4 (v : Std.BitVec 32) : Nat :=
+open BitVec
+def f4 (v : BitVec 32) : Nat :=
   match v with
   | 10#20 ++ 0#12  => 0 -- Should be rejected since `++` does not have `[match_pattern]`
   | _ => 1

tests/lean/run/bitvec_simproc.lean

@@ -5,43 +5,43 @@ Authors: Leonardo de Moura
 -/
 open Std BitVec
 
-example (h : x = (6 : Std.BitVec 3)) : x = -2 := by
+example (h : x = (6 : BitVec 3)) : x = -2 := by
   simp; guard_target =ₛ x = 6#3; assumption
-example (h : x = (5 : Std.BitVec 3)) : x = ~~~2 := by
+example (h : x = (5 : BitVec 3)) : x = ~~~2 := by
   simp; guard_target =ₛ x = 5#3; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = BitVec.abs (-1#32) := by
+example (h : x = (1 : BitVec 32)) : x = BitVec.abs (-1#32) := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (5 : Std.BitVec 3)) : x = 2 + 3 := by
+example (h : x = (5 : BitVec 3)) : x = 2 + 3 := by
   simp; guard_target =ₛ x = 5#3; assumption
-example (h : x = (1 : Std.BitVec 3)) : x = 5 &&& 3 := by
+example (h : x = (1 : BitVec 3)) : x = 5 &&& 3 := by
   simp; guard_target =ₛ x = 1#3; assumption
-example (h : x = (7 : Std.BitVec 3)) : x = 5 ||| 3 := by
+example (h : x = (7 : BitVec 3)) : x = 5 ||| 3 := by
   simp; guard_target =ₛ x = 7#3; assumption
-example (h : x = (6 : Std.BitVec 3)) : x = 5 ^^^ 3 := by
+example (h : x = (6 : BitVec 3)) : x = 5 ^^^ 3 := by
   simp; guard_target =ₛ x = 6#3; assumption
-example (h : x = (3 : Std.BitVec 32)) : x = 5 - 2 := by
+example (h : x = (3 : BitVec 32)) : x = 5 - 2 := by
   simp; guard_target =ₛ x = 3#32; assumption
-example (h : x = (10 : Std.BitVec 32)) : x = 5 * 2 := by
+example (h : x = (10 : BitVec 32)) : x = 5 * 2 := by
   simp; guard_target =ₛ x = 10#32; assumption
-example (h : x = (4 : Std.BitVec 32)) : x = 9 / 2 := by
+example (h : x = (4 : BitVec 32)) : x = 9 / 2 := by
   simp; guard_target =ₛ x = 4#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = 9 % 2 := by
+example (h : x = (1 : BitVec 32)) : x = 9 % 2 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (4 : Std.BitVec 32)) : x = udiv 9 2 := by
+example (h : x = (4 : BitVec 32)) : x = udiv 9 2 := by
   simp; guard_target =ₛ x = 4#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = umod 9 2 := by
+example (h : x = (1 : BitVec 32)) : x = umod 9 2 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (4 : Std.BitVec 32)) : x = sdiv (-9) (-2) := by
+example (h : x = (4 : BitVec 32)) : x = sdiv (-9) (-2) := by
   simp; guard_target =ₛ x = 4#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = smod (-9) 2 := by
+example (h : x = (1 : BitVec 32)) : x = smod (-9) 2 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = - smtUDiv 9 0 := by
+example (h : x = (1 : BitVec 32)) : x = - smtUDiv 9 0 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = - srem (-9) 2 := by
+example (h : x = (1 : BitVec 32)) : x = - srem (-9) 2 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = - smtSDiv 9 0 := by
+example (h : x = (1 : BitVec 32)) : x = - smtSDiv 9 0 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = smtSDiv (-9) 0 := by
+example (h : x = (1 : BitVec 32)) : x = smtSDiv (-9) 0 := by
   simp; guard_target =ₛ x = 1#32; assumption
 example (h : x = false) : x = (4#3).getLsb 0:= by
   simp; guard_target =ₛ x = false; assumption
@@ -51,29 +51,29 @@ example (h : x = true) : x = (4#3).getMsb 0:= by
   simp; guard_target =ₛ x = true; assumption
 example (h : x = false) : x = (4#3).getMsb 2:= by
   simp; guard_target =ₛ x = false; assumption
-example (h : x = (24 : Std.BitVec 32)) : x = 6#32 <<< 2 := by
+example (h : x = (24 : BitVec 32)) : x = 6#32 <<< 2 := by
   simp; guard_target =ₛ x = 24#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = 6#32 >>> 2 := by
+example (h : x = (1 : BitVec 32)) : x = 6#32 >>> 2 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (24 : Std.BitVec 32)) : x = BitVec.shiftLeft 6#32 2 := by
+example (h : x = (24 : BitVec 32)) : x = BitVec.shiftLeft 6#32 2 := by
   simp; guard_target =ₛ x = 24#32; assumption
-example (h : x = (1 : Std.BitVec 32)) : x = BitVec.ushiftRight 6#32 2 := by
+example (h : x = (1 : BitVec 32)) : x = BitVec.ushiftRight 6#32 2 := by
   simp; guard_target =ₛ x = 1#32; assumption
-example (h : x = (2 : Std.BitVec 32)) : x = - BitVec.sshiftRight (- 6#32) 2 := by
+example (h : x = (2 : BitVec 32)) : x = - BitVec.sshiftRight (- 6#32) 2 := by
   simp; guard_target =ₛ x = 2#32; assumption
-example (h : x = (5 : Std.BitVec 3)) : x = BitVec.rotateLeft (6#3) 1 := by
+example (h : x = (5 : BitVec 3)) : x = BitVec.rotateLeft (6#3) 1 := by
   simp; guard_target =ₛ x = 5#3; assumption
-example (h : x = (3 : Std.BitVec 3)) : x = BitVec.rotateRight (6#3) 1 := by
+example (h : x = (3 : BitVec 3)) : x = BitVec.rotateRight (6#3) 1 := by
   simp; guard_target =ₛ x = 3#3; assumption
-example (h : x = (7 : Std.BitVec 5)) : x = 1#3 ++ 3#2 := by
+example (h : x = (7 : BitVec 5)) : x = 1#3 ++ 3#2 := by
   simp; guard_target =ₛ x = 7#5; assumption
-example (h : x = (1 : Std.BitVec 3)) : x = BitVec.cast (by decide : 3=2+1) 1#3 := by
+example (h : x = (1 : BitVec 3)) : x = BitVec.cast (by decide : 3=2+1) 1#3 := by
   simp; guard_target =ₛ x = 1#3; assumption
 example (h : x = 5) : x = (2#3 + 3#3).toNat := by
   simp; guard_target =ₛ x = 5; assumption
 example (h : x = -1) : x = (2#3 - 3#3).toInt := by
   simp; guard_target =ₛ x = -1; assumption
-example (h : x = (1 : Std.BitVec 3)) : x = -BitVec.ofInt 3 (-1) := by
+example (h : x = (1 : BitVec 3)) : x = -BitVec.ofInt 3 (-1) := by
   simp; guard_target =ₛ x = 1#3; assumption
 example (h : x) : x = (1#3 < 3#3) := by
   simp; guard_target =ₛ x; assumption
@@ -99,15 +99,15 @@ example (h : x) : x = (3#3 ≥ 1#3) := by
   simp; guard_target =ₛ x; assumption
 example (h : ¬x) : x = (3#3 ≥ 4#3) := by
   simp; guard_target =ₛ ¬x; assumption
-example (h : x = (5 : Std.BitVec 7)) : x = (5#3).zeroExtend' (by decide) := by
+example (h : x = (5 : BitVec 7)) : x = (5#3).zeroExtend' (by decide) := by
   simp; guard_target =ₛ x = 5#7; assumption
-example (h : x = (80 : Std.BitVec 7)) : x = (5#3).shiftLeftZeroExtend 4 := by
+example (h : x = (80 : BitVec 7)) : x = (5#3).shiftLeftZeroExtend 4 := by
   simp; guard_target =ₛ x = 80#7; assumption
-example (h : x = (5: Std.BitVec 3)) : x = (10#5).extractLsb' 1 3 := by
+example (h : x = (5: BitVec 3)) : x = (10#5).extractLsb' 1 3 := by
   simp; guard_target =ₛ x = 5#3; assumption
-example (h : x = (9: Std.BitVec 6)) : x = (1#3).replicate 2 := by
+example (h : x = (9: BitVec 6)) : x = (1#3).replicate 2 := by
   simp; guard_target =ₛ x = 9#6; assumption
-example (h : x = (5 : Std.BitVec 7)) : x = (5#3).zeroExtend 7 := by
+example (h : x = (5 : BitVec 7)) : x = (5#3).zeroExtend 7 := by
   simp; guard_target =ₛ x = 5#7; assumption
 example (h : -5#10 = x) : signExtend 10 (-5#8) = x := by
   simp; guard_target =ₛ1019#10 = x; assumption