chore: move HashMap and HashSet to Std

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

src/Init/Data/HashMap.lean

@@ -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

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 _

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 =>

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.

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)

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)

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 :=

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

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.

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) >> "}" -/
 
 /-

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)

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 α

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 α

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)

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"
 

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)

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 α] :=

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

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

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

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

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