From 161209778899eb658ec0d1bf875539725b9fa08c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 25 Jun 2020 12:45:25 -0700
Subject: [PATCH] chore: move `HashMap` and `HashSet` to `Std`

---
 src/Init/Data.lean                                     |  1 -
 src/Init/Data/HashMap.lean                             |  7 -------
 src/Lean/Attributes.lean                               |  2 +-
 src/Lean/Compiler/IR/Borrow.lean                       |  4 ++--
 src/Lean/Compiler/IR/CompilerM.lean                    |  2 ++
 src/Lean/Compiler/IR/ElimDeadBranches.lean             |  2 +-
 src/Lean/Compiler/IR/EmitUtil.lean                     |  4 ++--
 src/Lean/Compiler/IR/ExpandResetReuse.lean             |  2 +-
 src/Lean/Data/Name.lean                                | 10 +++++-----
 src/Lean/Data/SMap.lean                                |  3 ++-
 src/Lean/Elab/StructInst.lean                          |  2 ++
 src/Lean/Environment.lean                              |  3 +++
 src/Lean/Expr.lean                                     |  2 +-
 src/Lean/Level.lean                                    |  4 +++-
 src/Lean/Meta/AbstractMVars.lean                       |  2 ++
 src/Lean/Meta/SynthInstance.lean                       |  2 ++
 src/Lean/MetavarContext.lean                           |  2 +-
 src/Lean/Util/MonadCache.lean                          |  4 +++-
 src/Std/Data.lean                                      |  2 ++
 .../Data/HashMap/Basic.lean => Std/Data/HashMap.lean}  | 10 ++++------
 src/{Init => Std}/Data/HashSet.lean                    |  7 ++-----
 src/Std/ShareCommon.lean                               |  3 ++-
 tests/lean/run/frontend1.lean                          |  2 +-
 23 files changed, 44 insertions(+), 38 deletions(-)
 delete mode 100644 src/Init/Data/HashMap.lean
 rename src/{Init/Data/HashMap/Basic.lean => Std/Data/HashMap.lean} (98%)
 rename src/{Init => Std}/Data/HashSet.lean (98%)

diff --git a/src/Init/Data.lean b/src/Init/Data.lean
index db3b6c1855..dc831447b4 100644
--- a/src/Init/Data.lean
+++ b/src/Init/Data.lean
@@ -20,5 +20,4 @@ import Init.Data.Float
 import Init.Data.RBTree
 import Init.Data.RBMap
 import Init.Data.Option
-import Init.Data.HashMap
 import Init.Data.Random
diff --git a/src/Init/Data/HashMap.lean b/src/Init/Data/HashMap.lean
deleted file mode 100644
index 1c6779cedf..0000000000
--- a/src/Init/Data/HashMap.lean
+++ /dev/null
@@ -1,7 +0,0 @@
-/-
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura
--/
-prelude
-import Init.Data.HashMap.Basic
diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean
index 0f57d9a150..630546efca 100644
--- a/src/Lean/Attributes.lean
+++ b/src/Lean/Attributes.lean
@@ -57,7 +57,7 @@ unless initializing $ throw (IO.userError ("failed to register attribute, attrib
 attributeMapRef.modify (fun m => m.insert attr.name attr)
 
 abbrev AttributeImplBuilder := List DataValue → Except String AttributeImpl
-abbrev AttributeImplBuilderTable := HashMap Name AttributeImplBuilder
+abbrev AttributeImplBuilderTable := Std.HashMap Name AttributeImplBuilder
 
 def mkAttributeImplBuilderTable : IO (IO.Ref AttributeImplBuilderTable) := IO.mkRef {}
 @[init mkAttributeImplBuilderTable] constant attributeImplBuilderTableRef : IO.Ref AttributeImplBuilderTable := arbitrary _
diff --git a/src/Lean/Compiler/IR/Borrow.lean b/src/Lean/Compiler/IR/Borrow.lean
index ecdac56b3c..30791da8a6 100644
--- a/src/Lean/Compiler/IR/Borrow.lean
+++ b/src/Lean/Compiler/IR/Borrow.lean
@@ -23,7 +23,7 @@ def getHash : Key → USize
 instance : Hashable Key := ⟨getHash⟩
 end OwnedSet
 
-abbrev OwnedSet := HashMap OwnedSet.Key Unit
+abbrev OwnedSet := Std.HashMap OwnedSet.Key Unit
 def OwnedSet.insert (s : OwnedSet) (k : OwnedSet.Key) : OwnedSet := s.insert k ()
 def OwnedSet.contains (s : OwnedSet) (k : OwnedSet.Key) : Bool := s.contains k
 
@@ -51,7 +51,7 @@ def getHash : Key → USize
 instance : Hashable Key := ⟨getHash⟩
 end ParamMap
 
-abbrev ParamMap := HashMap ParamMap.Key (Array Param)
+abbrev ParamMap := Std.HashMap ParamMap.Key (Array Param)
 
 def ParamMap.fmt (map : ParamMap) : Format :=
 let fmts := map.fold (fun fmt k ps =>
diff --git a/src/Lean/Compiler/IR/CompilerM.lean b/src/Lean/Compiler/IR/CompilerM.lean
index 31c6f46040..e823679f11 100644
--- a/src/Lean/Compiler/IR/CompilerM.lean
+++ b/src/Lean/Compiler/IR/CompilerM.lean
@@ -66,6 +66,8 @@ logMessageIfAux tracePrefixOptionName a
 @[inline] def modifyEnv (f : Environment → Environment) : CompilerM Unit :=
 modify $ fun s => { s with env := f s.env }
 
+open Std (HashMap)
+
 abbrev DeclMap := SMap Name Decl
 
 /- Create an array of decls to be saved on .olean file.
diff --git a/src/Lean/Compiler/IR/ElimDeadBranches.lean b/src/Lean/Compiler/IR/ElimDeadBranches.lean
index ae3d02bbef..960c105ad8 100644
--- a/src/Lean/Compiler/IR/ElimDeadBranches.lean
+++ b/src/Lean/Compiler/IR/ElimDeadBranches.lean
@@ -110,7 +110,7 @@ functionSummariesExt.addEntry env (fid, v)
 def getFunctionSummary? (env : Environment) (fid : FunId) : Option Value :=
 (functionSummariesExt.getState env).find? fid
 
-abbrev Assignment := HashMap VarId Value
+abbrev Assignment := Std.HashMap VarId Value
 
 structure InterpContext :=
 (currFnIdx : Nat := 0)
diff --git a/src/Lean/Compiler/IR/EmitUtil.lean b/src/Lean/Compiler/IR/EmitUtil.lean
index f017623a5a..18feb899cb 100644
--- a/src/Lean/Compiler/IR/EmitUtil.lean
+++ b/src/Lean/Compiler/IR/EmitUtil.lean
@@ -51,8 +51,8 @@ end CollectUsedDecls
 def collectUsedDecls (env : Environment) (decl : Decl) (used : NameSet := {}) : NameSet :=
 (CollectUsedDecls.collectDecl decl env).run' used
 
-abbrev VarTypeMap  := HashMap VarId IRType
-abbrev JPParamsMap := HashMap JoinPointId (Array Param)
+abbrev VarTypeMap  := Std.HashMap VarId IRType
+abbrev JPParamsMap := Std.HashMap JoinPointId (Array Param)
 
 namespace CollectMaps
 abbrev Collector := (VarTypeMap × JPParamsMap) → (VarTypeMap × JPParamsMap)
diff --git a/src/Lean/Compiler/IR/ExpandResetReuse.lean b/src/Lean/Compiler/IR/ExpandResetReuse.lean
index 663be41687..cc2485a306 100644
--- a/src/Lean/Compiler/IR/ExpandResetReuse.lean
+++ b/src/Lean/Compiler/IR/ExpandResetReuse.lean
@@ -11,7 +11,7 @@ namespace Lean
 namespace IR
 namespace ExpandResetReuse
 /- Mapping from variable to projections -/
-abbrev ProjMap  := HashMap VarId Expr
+abbrev ProjMap  := Std.HashMap VarId Expr
 namespace CollectProjMap
 abbrev Collector := ProjMap → ProjMap
 @[inline] def collectVDecl (x : VarId) (v : Expr) : Collector :=
diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean
index bb4f33ddb0..138abcd5a8 100644
--- a/src/Lean/Data/Name.lean
+++ b/src/Lean/Data/Name.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-import Init.Data.HashSet -- TODO
+import Std.Data.HashSet
 namespace Lean
 
 instance stringToName : HasCoe String Name :=
@@ -156,14 +156,14 @@ def contains (s : NameSet) (n : Name) : Bool := RBMap.contains s n
 
 end NameSet
 
-def NameHashSet := HashSet Name
+def NameHashSet := Std.HashSet Name
 
 namespace NameHashSet
-@[inline] def empty : NameHashSet := HashSet.empty
+@[inline] def empty : NameHashSet := Std.HashSet.empty
 instance : HasEmptyc NameHashSet := ⟨empty⟩
 instance : Inhabited NameHashSet := ⟨{}⟩
-def insert (s : NameHashSet) (n : Name) := HashSet.insert s n
-def contains (s : NameHashSet) (n : Name) : Bool := HashSet.contains s n
+def insert (s : NameHashSet) (n : Name) := s.insert n
+def contains (s : NameHashSet) (n : Name) : Bool := s.contains n
 end NameHashSet
 
 end Lean
diff --git a/src/Lean/Data/SMap.lean b/src/Lean/Data/SMap.lean
index 1c33dde832..e6c61d62b8 100644
--- a/src/Lean/Data/SMap.lean
+++ b/src/Lean/Data/SMap.lean
@@ -3,12 +3,13 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Std.Data.HashMap
 import Std.Data.PersistentHashMap
 universes u v w w'
 
 namespace Lean
 
-open Std (PHashMap)
+open Std (HashMap PHashMap)
 
 /- Staged map for implementing the Environment. The idea is to store
    imported entries into a hashtable and local entries into a persistent hashtable.
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 1b98501a5f..c9f5a50a73 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -13,6 +13,8 @@ namespace Elab
 namespace Term
 namespace StructInst
 
+open Std (HashMap)
+
 /- parser! "{" >> optional (try (termParser >> "with")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> "}" -/
 
 /-
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 6e587c8dbd..cfcb8251d0 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Std.Data.HashMap
 import Lean.Data.SMap
 import Lean.Declaration
 import Lean.LocalContext
@@ -36,6 +37,8 @@ structure EnvironmentHeader :=
 (imports      : Array Import := #[]) -- direct imports
 (moduleNames  : NameSet      := {})  -- all imported .lean modules
 
+open Std (HashMap)
+
 structure Environment :=
 (const2ModIdx : HashMap Name ModuleIdx)
 (constants    : ConstMap)
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index 11be5d8dd4..9a010c7f43 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -635,7 +635,7 @@ mkAppB (mkConst `Decidable.isTrue) pred proof
 def mkDecIsFalse (pred proof : Expr) :=
 mkAppB (mkConst `Decidable.isFalse) pred proof
 
-open Std (PHashMap PHashSet)
+open Std (HashMap HashSet PHashMap PHashSet)
 
 abbrev ExprMap (α : Type)  := HashMap Expr α
 abbrev PersistentExprMap (α : Type) := PHashMap Expr α
diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean
index 6af327b70a..0b9b169348 100644
--- a/src/Lean/Level.lean
+++ b/src/Lean/Level.lean
@@ -3,6 +3,8 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Std.Data.HashMap
+import Std.Data.HashSet
 import Std.Data.PersistentHashMap
 import Std.Data.PersistentHashSet
 import Lean.Data.Name
@@ -462,7 +464,7 @@ match lvl with
 
 end Level
 
-open Std (PHashMap PHashSet)
+open Std (HashMap HashSet PHashMap PHashSet)
 
 abbrev LevelMap (α : Type)  := HashMap Level α
 abbrev PersistentLevelMap (α : Type) := PHashMap Level α
diff --git a/src/Lean/Meta/AbstractMVars.lean b/src/Lean/Meta/AbstractMVars.lean
index 3e625f244d..ce932d7879 100644
--- a/src/Lean/Meta/AbstractMVars.lean
+++ b/src/Lean/Meta/AbstractMVars.lean
@@ -22,6 +22,8 @@ instance AbstractMVarsResult.hasBeq : HasBeq AbstractMVarsResult := ⟨AbstractM
 
 namespace AbstractMVars
 
+open Std (HashMap)
+
 structure State :=
 (ngen         : NameGenerator)
 (lctx         : LocalContext)
diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index de0b5a5a05..4d935454f9 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -15,6 +15,8 @@ namespace Lean
 namespace Meta
 namespace SynthInstance
 
+open Std (HashMap)
+
 def mkInferTCGoalsLRAttr : IO TagAttribute :=
 registerTagAttribute `inferTCGoalsLR "instruct type class resolution procedure to solve goals from left to right for this instance"
 
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index c9bff0de9e..1f0e953978 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -272,7 +272,7 @@ structure DelayedMetavarAssignment :=
 (fvars    : Array Expr)
 (val      : Expr)
 
-open Std (PersistentHashMap)
+open Std (HashMap PersistentHashMap)
 
 structure MetavarContext :=
 (depth       : Nat := 0)
diff --git a/src/Lean/Util/MonadCache.lean b/src/Lean/Util/MonadCache.lean
index e23962bf2d..a4f96c7888 100644
--- a/src/Lean/Util/MonadCache.lean
+++ b/src/Lean/Util/MonadCache.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-
+import Std.Data.HashMap
 namespace Lean
 /-- Interface for caching results.  -/
 class MonadCache (α β : Type) (m : Type → Type) :=
@@ -29,6 +29,8 @@ instance exceptLift {α β ε : Type} {m : Type → Type} [MonadCache α β m] [
 { findCached? := fun a   => ExceptT.lift $ MonadCache.findCached? a,
   cache       := fun a b => ExceptT.lift $ MonadCache.cache a b }
 
+open Std (HashMap)
+
 /-- Adapter for implementing `MonadCache` interface using `HashMap`s.
     We just have to specify how to extract/modify the `HashMap`. -/
 class MonadHashMapCacheAdapter (α β : Type) (m : Type → Type) [HasBeq α] [Hashable α] :=
diff --git a/src/Std/Data.lean b/src/Std/Data.lean
index 20036a4dd2..e4cfd31581 100644
--- a/src/Std/Data.lean
+++ b/src/Std/Data.lean
@@ -7,5 +7,7 @@ import Std.Data.BinomialHeap
 import Std.Data.DList
 import Std.Data.Stack
 import Std.Data.Queue
+import Std.Data.HashMap
+import Std.Data.HashSet
 import Std.Data.PersistentHashMap
 import Std.Data.PersistentHashSet
diff --git a/src/Init/Data/HashMap/Basic.lean b/src/Std/Data/HashMap.lean
similarity index 98%
rename from src/Init/Data/HashMap/Basic.lean
rename to src/Std/Data/HashMap.lean
index 97459d3b7c..8fd9ee6de8 100644
--- a/src/Init/Data/HashMap/Basic.lean
+++ b/src/Std/Data/HashMap.lean
@@ -3,11 +3,8 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-prelude
-import Init.Data.Array.Basic
-import Init.Data.AssocList
-import Init.Data.Option.Basic
-import Init.Data.Hashable
+import Init.Data.AssocList -- TODO
+namespace Std
 universes u v w
 
 def HashMapBucket (α : Type u) (β : Type v) :=
@@ -126,7 +123,7 @@ end HashMapImp
 def HashMap (α : Type u) (β : Type v) [HasBeq α] [Hashable α] :=
 { m : HashMapImp α β // m.WellFormed }
 
-open HashMapImp
+open Std.HashMapImp
 
 def mkHashMap {α : Type u} {β : Type v} [HasBeq α] [Hashable α] (nbuckets := 8) : HashMap α β :=
 ⟨ mkHashMapImp nbuckets, WellFormed.mkWff nbuckets ⟩
@@ -199,3 +196,4 @@ def numBuckets (m : HashMap α β) : Nat :=
 m.val.buckets.val.size
 
 end HashMap
+end Std
diff --git a/src/Init/Data/HashSet.lean b/src/Std/Data/HashSet.lean
similarity index 98%
rename from src/Init/Data/HashSet.lean
rename to src/Std/Data/HashSet.lean
index ff9e65d498..0186c596f9 100644
--- a/src/Init/Data/HashSet.lean
+++ b/src/Std/Data/HashSet.lean
@@ -3,11 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-prelude
-import Init.Data.Array.Basic
-import Init.Data.List.Control
-import Init.Data.Option.Basic
-import Init.Data.Hashable
+namespace Std
 universes u v w
 
 def HashSetBucket (α : Type u) :=
@@ -178,3 +174,4 @@ def numBuckets (m : HashSet α) : Nat :=
 m.val.buckets.val.size
 
 end HashSet
+end Std
diff --git a/src/Std/ShareCommon.lean b/src/Std/ShareCommon.lean
index deca16fe81..e4e1a6b423 100644
--- a/src/Std/ShareCommon.lean
+++ b/src/Std/ShareCommon.lean
@@ -3,7 +3,8 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import Init.Data.HashSet
+import Std.Data.HashSet
+import Std.Data.HashMap
 import Std.Data.PersistentHashMap
 import Std.Data.PersistentHashSet
 namespace Std
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index c2390a8796..45488cd324 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -88,7 +88,7 @@ structure S (α : Type) :=
 (field3 : α)
 (field4 : List α × Nat := ([], 0))
 (vec : Array (α × α) := #[])
-(map : HashMap String α := {})
+(map : Std.HashMap String α := {})
 
 inductive D (α : Type)
 | mk (a : α) (s : S4) : D