chore: move RBTree and RBMap to Std

src/Init/Data.lean

@@ -16,7 +16,5 @@ import Init.Data.FloatArray
 import Init.Data.Fin
 import Init.Data.UInt
 import Init.Data.Float
-import Init.Data.RBTree
-import Init.Data.RBMap
 import Init.Data.Option
 import Init.Data.Random

src/Init/Data/RBMap.lean

@@ -1,8 +0,0 @@
-/-
-Copyright (c) 2017 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.RBMap.Basic
-import Init.Data.RBMap.BasicAux

src/Init/Data/RBMap/BasicAux.lean

@@ -1,30 +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.RBMap.Basic
-import Init.Util
-
-universes u v w w'
-
-namespace RBMap
-variables {α : Type u} {β : Type v} {lt : α → α → Bool}
-
-@[inline] def min! [Inhabited α] [Inhabited β] (t : RBMap α β lt) : α × β :=
-match t.min with
-| some p => p
-| none   => panic! "map is empty"
-
-@[inline] def max! [Inhabited α] [Inhabited β] (t : RBMap α β lt) : α × β :=
-match t.max with
-| some p => p
-| none   => panic! "map is empty"
-
-@[inline] def find! [Inhabited β] (t : RBMap α β lt) (k : α) : β :=
-match t.find? k with
-| some b => b
-| none   => panic! "key is not in the map"
-
-end RBMap

src/Init/Data/RBTree.lean

@@ -1,7 +0,0 @@
-/-
-Copyright (c) 2017 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.RBTree.Basic

src/Lean/Compiler/IR/Basic.lean

@@ -425,6 +425,8 @@ end Decl
 @[export lean_ir_mk_extern_decl] def mkExternDecl (f : FunId) (xs : Array Param) (ty : IRType) (e : ExternAttrData) : Decl :=
 Decl.extern f xs ty e
 
+open Std (RBTree RBTree.empty RBMap)
+
 /-- Set of variable and join point names -/
 abbrev IndexSet := RBTree Index Index.lt
 instance vsetInh : Inhabited IndexSet := ⟨{}⟩

src/Lean/Compiler/IR/LiveVars.lean

@@ -81,12 +81,12 @@ def FnBody.hasLiveVar (b : FnBody) (ctx : LocalContext) (x : VarId) : Bool :=
 (IsLive.visitFnBody x.idx b).run' ctx
 
 abbrev LiveVarSet   := VarIdSet
-abbrev JPLiveVarMap := RBMap JoinPointId LiveVarSet (fun j₁ j₂ => j₁.idx < j₂.idx)
+abbrev JPLiveVarMap := Std.RBMap JoinPointId LiveVarSet (fun j₁ j₂ => j₁.idx < j₂.idx)
 
 instance LiveVarSet.inhabited : Inhabited LiveVarSet := ⟨{}⟩
 
 def mkLiveVarSet (x : VarId) : LiveVarSet :=
-RBTree.empty.insert x
+Std.RBTree.empty.insert x
 
 namespace LiveVars
 

src/Lean/Compiler/IR/RC.lean

@@ -20,7 +20,7 @@ structure VarInfo :=
 (persistent : Bool := false) -- true if the variable is statically known to be marked a Persistent at runtime
 (consume    : Bool := false) -- true if the variable RC must be "consumed"
 
-abbrev VarMap := RBMap VarId VarInfo (fun x y => x.idx < y.idx)
+abbrev VarMap := Std.RBMap VarId VarInfo (fun x y => x.idx < y.idx)
 
 structure Context :=
 (env            : Environment)

src/Lean/Data/Json/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Authors: Gabriel Ebner, Marc Huisinga
 -/
-
+import Std.Data.RBTree
 namespace Lean
 
 -- mantissa * 10^-exponent
@@ -82,6 +82,8 @@ end JsonNumber
 
 def strLt (a b : String) := Decidable.decide (a < b)
 
+open Std (RBNode)
+
 inductive Json
 | null
 | bool (b : Bool)

src/Lean/Data/Json/Parser.lean

@@ -8,6 +8,8 @@ import Lean.Data.Json.Basic
 
 namespace Lean
 
+open Std (RBNode RBNode.singleton RBNode.leaf)
+
 inductive Quickparse.Result (α : Type)
 | success (pos : String.Iterator) (res : α) : Quickparse.Result
 | error (pos : String.Iterator) (err : String) : Quickparse.Result

src/Lean/Data/Name.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 import Std.Data.HashSet
+import Std.Data.RBMap
+import Std.Data.RBTree
 namespace Lean
 
 instance stringToName : HasCoe String Name :=
@@ -126,9 +128,11 @@ def isAnonymous : Name → Bool
 
 end Name
 
-def NameMap (α : Type) := RBMap Name α Name.quickLt
+open Std (RBMap RBTree mkRBMap mkRBTree)
 
-@[inline] def mkNameMap (α : Type) : NameMap α := mkRBMap Name α Name.quickLt
+def NameMap (α : Type) := Std.RBMap Name α Name.quickLt
+
+@[inline] def mkNameMap (α : Type) : NameMap α := Std.mkRBMap Name α Name.quickLt
 
 namespace NameMap
 variable {α : Type}
@@ -137,11 +141,11 @@ instance (α : Type) : HasEmptyc (NameMap α) := ⟨mkNameMap α⟩
 
 instance (α : Type) : Inhabited (NameMap α) := ⟨{}⟩
 
-def insert (m : NameMap α) (n : Name) (a : α) := RBMap.insert m n a
+def insert (m : NameMap α) (n : Name) (a : α) := Std.RBMap.insert m n a
 
-def contains (m : NameMap α) (n : Name) : Bool := RBMap.contains m n
+def contains (m : NameMap α) (n : Name) : Bool := Std.RBMap.contains m n
 
-@[inline] def find? (m : NameMap α) (n : Name) : Option α := RBMap.find? m n
+@[inline] def find? (m : NameMap α) (n : Name) : Option α := Std.RBMap.find? m n
 
 end NameMap
 
@@ -151,8 +155,8 @@ namespace NameSet
 def empty : NameSet := mkRBTree Name Name.quickLt
 instance : HasEmptyc NameSet := ⟨empty⟩
 instance : Inhabited NameSet := ⟨{}⟩
-def insert (s : NameSet) (n : Name)  := RBTree.insert s n
-def contains (s : NameSet) (n : Name) : Bool := RBMap.contains s n
+def insert (s : NameSet) (n : Name)  := Std.RBTree.insert s n
+def contains (s : NameSet) (n : Name) : Bool := Std.RBMap.contains s n
 
 end NameSet
 

src/Lean/Data/Trie.lean

@@ -10,6 +10,8 @@ import Lean.Data.Format
 namespace Lean
 namespace Parser
 
+open Std (RBNode RBNode.leaf RBNode.singleton RBNode.find RBNode.insert)
+
 inductive Trie (α : Type)
 | Node : Option α → RBNode Char (fun _ => Trie) → Trie
 

src/Lean/Delaborator.lean

@@ -66,7 +66,7 @@ registerOption `pp.explicit { defValue := false, group := "pp", descr := "(prett
 pure ()
 
 /-- Associate pretty printer options to a specific subterm using a synthetic position. -/
-abbrev OptionsPerPos := RBMap Nat Options (fun a b => a < b)
+abbrev OptionsPerPos := Std.RBMap Nat Options (fun a b => a < b)
 
 namespace Delaborator
 open Lean.Meta

src/Lean/Parser/Parser.lean

@@ -1315,6 +1315,8 @@ fun c s =>
 @[inline] def many1Indent (p : Parser) (errorMsg : String) : Parser :=
 withPosition $ fun pos => many1 (checkColGe pos.column errorMsg >> p)
 
+open Std (RBMap RBMap.empty)
+
 /-- A multimap indexed by tokens. Used for indexing parsers by their leading token. -/
 def TokenMap (α : Type) := RBMap Name (List α) Name.quickLt
 

src/Std/Data.lean

@@ -13,3 +13,5 @@ import Std.Data.PersistentArray
 import Std.Data.PersistentHashMap
 import Std.Data.PersistentHashSet
 import Std.Data.AssocList
+import Std.Data.RBTree
+import Std.Data.RBMap

src/Std/Data/HashMap.lean

@@ -131,10 +131,10 @@ def mkHashMap {α : Type u} {β : Type v} [HasBeq α] [Hashable α] (nbuckets :=
 namespace HashMap
 variables {α : Type u} {β : Type v} [HasBeq α] [Hashable α]
 
-instance : Inhabited (HashMap α β) :=
+instance inhabited : Inhabited (HashMap α β) :=
 ⟨mkHashMap⟩
 
-instance : HasEmptyc (HashMap α β) :=
+instance hasEmptyc : HasEmptyc (HashMap α β) :=
 ⟨mkHashMap⟩
 
 @[inline] def insert (m : HashMap α β) (a : α) (b : β) : HashMap α β :=

src/Std/Data/RBMap.lean

@@ -3,10 +3,7 @@ Copyright (c) 2017 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.Repr
-import Init.Data.Option.Basic
-
+namespace Std
 universes u v w w'
 
 inductive Rbcolor
@@ -19,7 +16,7 @@ inductive RBNode (α : Type u) (β : α → Type v)
 namespace RBNode
 variables {α : Type u} {β : α → Type v} {σ : Type w}
 
-open Rbcolor Nat
+open Std.Rbcolor Nat
 
 def depth (f : Nat → Nat → Nat) : RBNode α β → Nat
 | leaf           => 0
@@ -205,7 +202,7 @@ inductive WellFormed (lt : α → α → Bool) : RBNode α β → Prop
 
 end RBNode
 
-open RBNode
+open Std.RBNode
 
 /- TODO(Leo): define dRBMap -/
 
@@ -303,7 +300,24 @@ m.fold (fun sz _ _ => sz+1) 0
 def maxDepth (t : RBMap α β lt) : Nat :=
 t.val.depth Nat.max
 
+@[inline] def min! [Inhabited α] [Inhabited β] (t : RBMap α β lt) : α × β :=
+match t.min with
+| some p => p
+| none   => panic! "map is empty"
+
+@[inline] def max! [Inhabited α] [Inhabited β] (t : RBMap α β lt) : α × β :=
+match t.max with
+| some p => p
+| none   => panic! "map is empty"
+
+@[inline] def find! [Inhabited β] (t : RBMap α β lt) (k : α) : β :=
+match t.find? k with
+| some b => b
+| none   => panic! "key is not in the map"
+
 end RBMap
 
 def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (lt : α → α → Bool) : RBMap α β lt :=
 RBMap.fromList l lt
+
+end Std

src/Std/Data/RBTree.lean

@@ -3,8 +3,8 @@ Copyright (c) 2017 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.RBMap.Basic
+import Std.Data.RBMap
+namespace Std
 universes u v w
 
 def RBTree (α : Type u) (lt : α → α → Bool) : Type u :=
@@ -13,7 +13,7 @@ RBMap α Unit lt
 @[inline] def mkRBTree (α : Type u) (lt : α → α → Bool) : RBTree α lt :=
 mkRBMap α Unit lt
 
-instance (α : Type u) (lt : α → α → Bool) : HasEmptyc (RBTree α lt) :=
+instance RBTree.hasEmptyc (α : Type u) (lt : α → α → Bool) : HasEmptyc (RBTree α lt) :=
 ⟨mkRBTree α lt⟩
 
 namespace RBTree
@@ -93,3 +93,4 @@ end RBTree
 
 def rbtreeOf {α : Type u} (l : List α) (lt : α → α → Bool) : RBTree α lt :=
 RBTree.fromList l lt
+end Std

tests/compiler/rbmap_library.lean

@@ -1,3 +1,6 @@
+import Std
+open Std
+
 def check (b : Bool) : IO Unit :=
 unless b $ IO.println "ERROR"
 

tests/lean/PPRoundtrip.lean

@@ -39,7 +39,7 @@ section
   #eval check `(List Nat)
   #eval check `(id Nat)
 end
-#eval check `(id (id Nat)) (RBMap.empty.insert 4 $ KVMap.empty.insert `pp.explicit true)
+#eval check `(id (id Nat)) (Std.RBMap.empty.insert 4 $ KVMap.empty.insert `pp.explicit true)
 
 -- specify the expected type of `a` in a way that is not erased by the delaborator
 def typeAs.{u} (α : Type u) (a : α) := ()