chore: remove open Std (BitVec) (#535)

... as well as outdated BitVec imports.
opencompl · Aug 15, 2024 · b281345 · b281345
1 parent e7dd381
commit b281345
Show file tree

Hide file tree

Showing 248 changed files with 0 additions and 257 deletions.
diff --git a/SSA/Projects/InstCombine/AliveAutoGenerated.lean b/SSA/Projects/InstCombine/AliveAutoGenerated.lean
@@ -8,7 +8,6 @@ import SSA.Projects.InstCombine.Refinement
 import SSA.Projects.InstCombine.Tactic
 
 open MLIR AST
-open Std (BitVec)
 open Ctxt (Var)
 
 namespace AliveAutoGenerated

diff --git a/SSA/Projects/InstCombine/AliveHandwrittenExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenExamples.lean
@@ -10,7 +10,6 @@ import SSA.Projects.InstCombine.ForStd
 import SSA.Core.ErasedContext
 
 open MLIR AST
-open Std (BitVec)
 open Ctxt (Var DerivedCtxt)
 open InstCombine (MOp)
 

diff --git a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
@@ -114,7 +114,6 @@ def MulDivRem805_rhs (w : ℕ) : Com InstCombine.LLVM
   /- r = -/ Com.var (select w /-%c-/ 1 /-X-/ 5 /-c0-/ 0) <|
   Com.ret ⟨/-r-/0, by simp [Ctxt.snoc]⟩
 
-open Std (BitVec) in
 def alive_simplifyMulDivRem805 (w : Nat) :
   MulDivRem805_lhs w ⊑ MulDivRem805_rhs w := by
   unfold MulDivRem805_lhs MulDivRem805_rhs
@@ -223,7 +222,6 @@ info: 'AliveHandwritten.MulDivRem.alive_simplifyMulDivRem805' depends on axioms:
 -/
 #guard_msgs in #print axioms alive_simplifyMulDivRem805
 
-open Std (BitVec) in
 def alive_simplifyMulDivRem805' (w : Nat) :
   MulDivRem805_lhs w ⊑ MulDivRem805_rhs w := by
   unfold MulDivRem805_lhs MulDivRem805_rhs

diff --git a/SSA/Projects/InstCombine/ForMathlib.lean b/SSA/Projects/InstCombine/ForMathlib.lean
@@ -6,7 +6,6 @@ import Mathlib.Data.Nat.Bitwise
 import Mathlib.Algebra.Group.Fin.Basic
 import Mathlib.Data.Nat.Bits
 import Mathlib.Data.ZMod.Defs
-import Batteries.Data.BitVec
 
 namespace BitVec
 open Nat

diff --git a/SSA/Projects/InstCombine/HackersDelight.lean b/SSA/Projects/InstCombine/HackersDelight.lean
@@ -1,11 +1,6 @@
-import Init.Data.BitVec.Basic
-import Init.Data.BitVec.Lemmas
-import Init.Data.BitVec.Bitblast
 import SSA.Projects.InstCombine.ForMathlib
 import SSA.Projects.InstCombine.ForStd
 import SSA.Projects.InstCombine.TacticAuto
-import Init.Data.Nat.Bitwise.Basic
-import Init.Data.Nat.Bitwise.Lemmas
 
 set_option linter.unusedTactic false
 set_option linter.unreachableTactic false

diff --git a/SSA/Projects/InstCombine/LLVM/EDSL.lean b/SSA/Projects/InstCombine/LLVM/EDSL.lean
@@ -3,7 +3,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 -/
 import Qq
 import SSA.Projects.InstCombine.Base
-import Batteries.Data.BitVec
 import SSA.Core.MLIRSyntax.EDSL
 import SSA.Projects.InstCombine.LLVM.CLITests
 

diff --git a/SSA/Projects/InstCombine/LLVM/Enumerator.lean b/SSA/Projects/InstCombine/LLVM/Enumerator.lean
@@ -2,7 +2,6 @@
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 -- Script that exhaustive enumerates the our LLVM semantics.
-import Batteries.Data.BitVec
 import Init.System.IO
 import SSA.Core.Util
 import SSA.Projects.InstCombine.LLVM.Semantics

diff --git a/SSA/Projects/InstCombine/PaperExamples.lean b/SSA/Projects/InstCombine/PaperExamples.lean
@@ -7,9 +7,6 @@ import SSA.Projects.InstCombine.Tactic
 import SSA.Projects.InstCombine.TacticAuto
 import SSA.Projects.InstCombine.Base
 import SSA.Projects.InstCombine.ForLean
-import Init.Data.BitVec.Bitblast
-import Init.Data.BitVec.Lemmas
-import Init.Data.BitVec.Folds
 import Lean
 
 

diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean
@@ -8,7 +8,6 @@ import SSA.Projects.InstCombine.ForStd
 import Mathlib.Tactic
 import SSA.Core.ErasedContext
 import SSA.Core.Tactic
-import Batteries.Data.BitVec
 
 open MLIR AST
 

diff --git a/SSA/Projects/InstCombine/TacticAuto.lean b/SSA/Projects/InstCombine/TacticAuto.lean
@@ -2,11 +2,8 @@
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
 import Mathlib.Tactic.Ring
-import Batteries.Data.BitVec
 import SSA.Projects.InstCombine.ForLean
-
 import SSA.Projects.InstCombine.LLVM.EDSL
-import Batteries.Data.BitVec
 
 attribute [simp_llvm_case_bash]
   BitVec.Refinement.refl BitVec.Refinement.some_some BitVec.Refinement.none_left

diff --git a/SSA/Projects/InstCombine/TestLLVMOps.lean b/SSA/Projects/InstCombine/TestLLVMOps.lean
@@ -5,7 +5,6 @@ import SSA.Projects.InstCombine.LLVM.PrettyEDSL
 import SSA.Projects.InstCombine.LLVM.CLITests
 
 open MLIR AST
-open Std (BitVec)
 open Ctxt (Var)
 
 -- Hardcoding the i4 for now, should change to w once I get

diff --git a/SSA/Projects/InstCombine/scripts/mlir-tool.py b/SSA/Projects/InstCombine/scripts/mlir-tool.py
@@ -175,7 +175,6 @@ def {name}_after := [llvm|
 open BitVec
 
 open MLIR AST
-open Std (BitVec)
 open Ctxt (Var)
 
 set_option linter.deprecated false

diff --git a/SSA/Projects/InstCombine/scripts/types.py b/SSA/Projects/InstCombine/scripts/types.py
@@ -49,7 +49,6 @@ def process_file(file_path):
     with open(proof_name + ".lean", "a") as file:
         file.write(
             """
-open Std (BitVec)
 """
         )
         for _, n, m in named:

diff --git a/SSA/Projects/InstCombine/tests/LLVM/g2004h02h23hShiftShiftOverflow.lean b/SSA/Projects/InstCombine/tests/LLVM/g2004h02h23hShiftShiftOverflow.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/g2004h02h23hShiftShiftOverflow_proof.lean b/SSA/Projects/InstCombine/tests/LLVM/g2004h02h23hShiftShiftOverflow_proof.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/g2004h11h22hMissedhandhfold.lean b/SSA/Projects/InstCombine/tests/LLVM/g2004h11h22hMissedhandhfold.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/g2004h11h22hMissedhandhfold_proof.lean b/SSA/Projects/InstCombine/tests/LLVM/g2004h11h22hMissedhandhfold_proof.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/g2008h02h16hSDivOverflow2.lean b/SSA/Projects/InstCombine/tests/LLVM/g2008h02h16hSDivOverflow2.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/g2008h02h16hSDivOverflow2_proof.lean b/SSA/Projects/InstCombine/tests/LLVM/g2008h02h16hSDivOverflow2_proof.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/g2008h02h23hMulSub.lean b/SSA/Projects/InstCombine/tests/LLVM/g2008h02h23hMulSub.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/g2008h02h23hMulSub_proof.lean b/SSA/Projects/InstCombine/tests/LLVM/g2008h02h23hMulSub_proof.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/g2008h05h31hAddBool.lean b/SSA/Projects/InstCombine/tests/LLVM/g2008h05h31hAddBool.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/g2008h05h31hAddBool_proof.lean b/SSA/Projects/InstCombine/tests/LLVM/g2008h05h31hAddBool_proof.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/g2008h05h31hBools.lean b/SSA/Projects/InstCombine/tests/LLVM/g2008h05h31hBools.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/g2008h05h31hBools_proof.lean b/SSA/Projects/InstCombine/tests/LLVM/g2008h05h31hBools_proof.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/g2008h07h08hSubAnd.lean b/SSA/Projects/InstCombine/tests/LLVM/g2008h07h08hSubAnd.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/g2008h07h08hSubAnd_proof.lean b/SSA/Projects/InstCombine/tests/LLVM/g2008h07h08hSubAnd_proof.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/g2008h07h09hSubAndError.lean b/SSA/Projects/InstCombine/tests/LLVM/g2008h07h09hSubAndError.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/g2008h07h09hSubAndError_proof.lean b/SSA/Projects/InstCombine/tests/LLVM/g2008h07h09hSubAndError_proof.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/g2008h07h11hRemAnd.lean b/SSA/Projects/InstCombine/tests/LLVM/g2008h07h11hRemAnd.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/g2008h07h11hRemAnd_proof.lean b/SSA/Projects/InstCombine/tests/LLVM/g2008h07h11hRemAnd_proof.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/g2010h11h01hlshrhmask.lean b/SSA/Projects/InstCombine/tests/LLVM/g2010h11h01hlshrhmask.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/g2010h11h01hlshrhmask_proof.lean b/SSA/Projects/InstCombine/tests/LLVM/g2010h11h01hlshrhmask_proof.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/g2010h11h23hDistributed.lean b/SSA/Projects/InstCombine/tests/LLVM/g2010h11h23hDistributed.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/g2010h11h23hDistributed_proof.lean b/SSA/Projects/InstCombine/tests/LLVM/g2010h11h23hDistributed_proof.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/gadd2.lean b/SSA/Projects/InstCombine/tests/LLVM/gadd2.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/gadd2_proof.lean b/SSA/Projects/InstCombine/tests/LLVM/gadd2_proof.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/gadd4.lean b/SSA/Projects/InstCombine/tests/LLVM/gadd4.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/gadd4_proof.lean b/SSA/Projects/InstCombine/tests/LLVM/gadd4_proof.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/gadd_or_sub.lean b/SSA/Projects/InstCombine/tests/LLVM/gadd_or_sub.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/gadd_or_sub_proof.lean b/SSA/Projects/InstCombine/tests/LLVM/gadd_or_sub_proof.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/gaddhmask.lean b/SSA/Projects/InstCombine/tests/LLVM/gaddhmask.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/gaddhmask_proof.lean b/SSA/Projects/InstCombine/tests/LLVM/gaddhmask_proof.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/gaddhmaskhneg.lean b/SSA/Projects/InstCombine/tests/LLVM/gaddhmaskhneg.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/gaddhmaskhneg_proof.lean b/SSA/Projects/InstCombine/tests/LLVM/gaddhmaskhneg_proof.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/gaddhshift.lean b/SSA/Projects/InstCombine/tests/LLVM/gaddhshift.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/gaddhshift_proof.lean b/SSA/Projects/InstCombine/tests/LLVM/gaddhshift_proof.lean
diff --git a/SSA/Projects/InstCombine/tests/LLVM/gaddhshlhsdivhtohsrem.lean b/SSA/Projects/InstCombine/tests/LLVM/gaddhshlhsdivhtohsrem.lean