diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean index 9e77ac5de568..77696f079a91 100644 --- a/src/Init/Data/BitVec/Basic.lean +++ b/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 diff --git a/src/Init/Data/BitVec/Bitblast.lean b/src/Init/Data/BitVec/Bitblast.lean index 85583b51238f..b338a944a4c9 100644 --- a/src/Init/Data/BitVec/Bitblast.lean +++ b/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 diff --git a/src/Init/Data/BitVec/Folds.lean b/src/Init/Data/BitVec/Folds.lean index 3dcf8a4b7e14..7c7c7a4a114e 100644 --- a/src/Init/Data/BitVec/Folds.lean +++ b/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 diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 8552ff0ecfcb..7b48426d0f80 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/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 diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean index 13e80a619b18..1fdd1272d578 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean +++ b/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 diff --git a/tests/lean/binop_at_pattern_issue.lean b/tests/lean/binop_at_pattern_issue.lean index d5a4f422c766..b24b5be8830a 100644 --- a/tests/lean/binop_at_pattern_issue.lean +++ b/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 diff --git a/tests/lean/run/bitvec_simproc.lean b/tests/lean/run/bitvec_simproc.lean index 465a0ed21f5e..f3e3ae1bba75 100644 --- a/tests/lean/run/bitvec_simproc.lean +++ b/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