chore: move PersistentArray to Std

src/Init/Data.lean

@@ -11,7 +11,6 @@ import Init.Data.String
 import Init.Data.List
 import Init.Data.Int
 import Init.Data.Array
-import Init.Data.PersistentArray
 import Init.Data.ByteArray
 import Init.Data.FloatArray
 import Init.Data.Fin

src/Init/Data/PersistentArray.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.PersistentArray.Basic

src/Lean/Compiler/IR/ElimDeadBranches.lean

@@ -120,7 +120,7 @@ structure InterpContext :=
 
 structure InterpState :=
 (assignments : Array Assignment)
-(funVals     : PArray Value) -- we take snapshots during fixpoint computations
+(funVals     : Std.PArray Value) -- we take snapshots during fixpoint computations
 
 abbrev M := ReaderT InterpContext (StateM InterpState)
 
@@ -267,7 +267,7 @@ def elimDeadBranches (decls : Array Decl) : CompilerM (Array Decl) := do
 s ← get;
 let env := s.env;
 let assignments : Array Assignment := decls.map $ fun _ => {};
-let funVals := mkPArray decls.size Value.bot;
+let funVals := Std.mkPArray decls.size Value.bot;
 let ctx : InterpContext := { decls := decls, env := env };
 let s : InterpState := { assignments := assignments, funVals := funVals };
 let (_, s) := (inferMain () ctx).run s;

src/Lean/LocalContext.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.PersistentArray
 import Lean.Expr
 import Lean.Hygiene
 
@@ -67,7 +68,7 @@ mkFVar decl.fvarId
 
 end LocalDecl
 
-open Std (PersistentHashMap)
+open Std (PersistentHashMap PersistentArray PArray)
 
 structure LocalContext :=
 (fvarIdToDecl : PersistentHashMap FVarId LocalDecl := {})

src/Lean/Message.lean

@@ -142,7 +142,7 @@ instance : HasToString Message :=
 end Message
 
 structure MessageLog :=
-(msgs : PersistentArray Message := {})
+(msgs : Std.PersistentArray Message := {})
 
 namespace MessageLog
 def empty : MessageLog := ⟨{}⟩

src/Lean/Meta/Basic.lean

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

src/Lean/Meta/LevelDefEq.lean

@@ -146,6 +146,8 @@ def isListLevelDefEqAux : List Level → List Level → MetaM Bool
 private def getNumPostponed : MetaM Nat := do
 s ← get; pure s.postponed.size
 
+open Std (PersistentArray)
+
 private def getResetPostponed : MetaM (PersistentArray PostponedEntry) := do
 s ← get;
 let ps := s.postponed;

src/Lean/Util/Trace.lean

@@ -8,6 +8,8 @@ universe u
 
 namespace Lean
 
+open Std (PersistentArray)
+
 class MonadTracer (m : Type → Type u) :=
 (traceCtx {α} : Name → m α → m α)
 (trace  : Name → (Unit → MessageData) → m PUnit)

src/Std/Data.lean

@@ -9,6 +9,7 @@ import Std.Data.Stack
 import Std.Data.Queue
 import Std.Data.HashMap
 import Std.Data.HashSet
+import Std.Data.PersistentArray
 import Std.Data.PersistentHashMap
 import Std.Data.PersistentHashSet
 import Std.Data.AssocList

src/Std/Data/PersistentArray.lean

@@ -3,11 +3,10 @@ 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.Control.Conditional
-import Init.Data.Array
 universes u v w
 
+namespace Std
+
 inductive PersistentArrayNode (α : Type u)
 | node (cs : Array PersistentArrayNode) : PersistentArrayNode
 | leaf (vs : Array α)                   : PersistentArrayNode
@@ -42,7 +41,7 @@ namespace PersistentArray
 /- TODO: use proofs for showing that array accesses are not out of bounds.
    We can do it after we reimplement the tactic framework. -/
 variables {α : Type u}
-open PersistentArrayNode
+open Std.PersistentArrayNode
 
 def empty : PersistentArray α :=
 {}
@@ -322,6 +321,16 @@ instance : HasToString Stats := ⟨Stats.toString⟩
 
 end PersistentArray
 
+def mkPersistentArray {α : Type u} (n : Nat) (v : α) : PArray α :=
+n.fold (fun i p => p.push v) PersistentArray.empty
+
+@[inline] def mkPArray {α : Type u} (n : Nat) (v : α) : PArray α :=
+mkPersistentArray n v
+
+end Std
+
+open Std (PersistentArray PersistentArray.empty)
+
 def List.toPersistentArrayAux {α : Type u} : List α → PersistentArray α → PersistentArray α
 | [],    t => t
 | x::xs, t => List.toPersistentArrayAux xs (t.push x)
@@ -334,9 +343,3 @@ xs.foldl (fun p x => p.push x) PersistentArray.empty
 
 @[inline] def Array.toPArray {α : Type u} (xs : Array α) : PersistentArray α :=
 xs.toPersistentArray
-
-def mkPersistentArray {α : Type u} (n : Nat) (v : α) : PArray α :=
-n.fold (fun i p => p.push v) PersistentArray.empty
-
-@[inline] def mkPArray {α : Type u} (n : Nat) (v : α) : PArray α :=
-mkPersistentArray n v