chore: move PersistentHashMap and PersistentHashSet to Std

src/Init/Data/PersistentHashMap.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.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Data.PersistentHashMap.Basic

src/Lean/Attributes.lean

@@ -40,6 +40,8 @@ structure AttributeImpl :=
 instance AttributeImpl.inhabited : Inhabited AttributeImpl :=
 ⟨{ name := arbitrary _, descr := arbitrary _, add := fun env _ _ _ => pure env }⟩
 
+open Std (PersistentHashMap)
+
 def mkAttributeMapRef : IO (IO.Ref (PersistentHashMap Name AttributeImpl)) :=
 IO.mkRef {}
 

src/Lean/Data/SMap.lean

@@ -3,11 +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 Init.Data.PersistentHashMap
+import Std.Data.PersistentHashMap
 universes u v w w'
 
 namespace Lean
 
+open Std (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/Expr.lean

@@ -635,6 +635,8 @@ mkAppB (mkConst `Decidable.isTrue) pred proof
 def mkDecIsFalse (pred proof : Expr) :=
 mkAppB (mkConst `Decidable.isFalse) pred proof
 
+open Std (PHashMap PHashSet)
+
 abbrev ExprMap (α : Type)  := HashMap Expr α
 abbrev PersistentExprMap (α : Type) := PHashMap Expr α
 abbrev ExprSet := HashSet Expr

src/Lean/Level.lean

@@ -3,8 +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 Init.Data.PersistentHashMap -- TODO
-import Init.Data.PersistentHashSet -- TODO
+import Std.Data.PersistentHashMap
+import Std.Data.PersistentHashSet
 import Lean.Data.Name
 import Lean.Data.Format
 
@@ -462,6 +462,8 @@ match lvl with
 
 end Level
 
+open Std (PHashMap PHashSet)
+
 abbrev LevelMap (α : Type)  := HashMap Level α
 abbrev PersistentLevelMap (α : Type) := PHashMap Level α
 abbrev LevelSet := HashSet Level

src/Lean/LocalContext.lean

@@ -67,6 +67,8 @@ mkFVar decl.fvarId
 
 end LocalDecl
 
+open Std (PersistentHashMap)
+
 structure LocalContext :=
 (fvarIdToDecl : PersistentHashMap FVarId LocalDecl := {})
 (decls        : PersistentArray (Option LocalDecl) := {})

src/Lean/Meta/Basic.lean

@@ -103,6 +103,8 @@ instance : HasBeq InfoCacheKey :=
 ⟨fun ⟨t₁, e₁, n₁⟩ ⟨t₂, e₂, n₂⟩ => t₁ == t₂ && n₁ == n₂ && e₁ == e₂⟩
 end InfoCacheKey
 
+open Std (PersistentHashMap)
+
 structure Cache :=
 (inferType     : PersistentExprStructMap Expr := {})
 (funInfo       : PersistentHashMap InfoCacheKey FunInfo := {})

src/Lean/Meta/DiscrTreeTypes.lean

@@ -46,6 +46,7 @@ inductive Trie (α : Type)
 end DiscrTree
 
 open DiscrTree
+open Std (PersistentHashMap)
 
 structure DiscrTree (α : Type) :=
 (root : PersistentHashMap Key (Trie α) := {})

src/Lean/MetavarContext.lean

@@ -272,6 +272,8 @@ structure DelayedMetavarAssignment :=
 (fvars    : Array Expr)
 (val      : Expr)
 
+open Std (PersistentHashMap)
+
 structure MetavarContext :=
 (depth       : Nat := 0)
 (lDepth      : PersistentHashMap MVarId Nat := {})

src/Lean/Parser/Parser.lean

@@ -103,7 +103,7 @@ def initCacheForInput (input : String) : ParserCache :=
 
 abbrev TokenTable := Trie Token
 
-abbrev SyntaxNodeKindSet := PersistentHashMap SyntaxNodeKind Unit
+abbrev SyntaxNodeKindSet := Std.PersistentHashMap SyntaxNodeKind Unit
 
 def SyntaxNodeKindSet.insert (s : SyntaxNodeKindSet) (k : SyntaxNodeKind) : SyntaxNodeKindSet :=
 s.insert k ()
@@ -1373,7 +1373,7 @@ structure ParserCategory :=
 
 instance ParserCategory.inhabited : Inhabited ParserCategory := ⟨{ tables := {}, leadingIdentAsSymbol := false }⟩
 
-abbrev ParserCategories := PersistentHashMap Name ParserCategory
+abbrev ParserCategories := Std.PersistentHashMap Name ParserCategory
 
 def indexed {α : Type} (map : TokenMap α) (c : ParserContext) (s : ParserState) (leadingIdentAsSymbol : Bool) : ParserState × List α :=
 let (s, stx) := peekToken c s;

src/Std/Data.lean

@@ -7,3 +7,5 @@ import Std.Data.BinomialHeap
 import Std.Data.DList
 import Std.Data.Stack
 import Std.Data.Queue
+import Std.Data.PersistentHashMap
+import Std.Data.PersistentHashSet

src/Std/Data/PersistentHashMap.lean

@@ -3,9 +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
 -/
-prelude
-import Init.Data.Array
-import Init.Data.Hashable
+namespace Std
 universes u v w w'
 
 namespace PersistentHashMap
@@ -317,3 +315,4 @@ def Stats.toString (s : Stats) : String :=
 instance : HasToString Stats := ⟨Stats.toString⟩
 
 end PersistentHashMap
+end Std

src/Std/Data/PersistentHashSet.lean

@@ -3,9 +3,9 @@ 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.PersistentHashMap
+import Std.Data.PersistentHashMap
 
+namespace Std
 universes u v
 
 structure PersistentHashSet (α : Type u) [HasBeq α] [Hashable α] :=
@@ -53,3 +53,4 @@ s.set.foldlM (fun d a _ => f d a) d
 Id.run $ s.foldM f d
 
 end PersistentHashSet
+end Std

src/Std/ShareCommon.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Init.Data.HashSet
-import Init.Data.PersistentHashMap
-import Init.Data.PersistentHashSet
+import Std.Data.PersistentHashMap
+import Std.Data.PersistentHashSet
 namespace Std
 universes u v