From 11ed7c61952aa4fcc0901bf85d70ba0afe8d77f5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 25 Jun 2020 13:02:21 -0700 Subject: [PATCH] chore: move `PersistentArray` to `Std` --- src/Init/Data.lean | 1 - src/Init/Data/PersistentArray.lean | 7 ------ src/Lean/Compiler/IR/ElimDeadBranches.lean | 4 ++-- src/Lean/LocalContext.lean | 3 ++- src/Lean/Message.lean | 2 +- src/Lean/Meta/Basic.lean | 2 +- src/Lean/Meta/LevelDefEq.lean | 2 ++ src/Lean/Util/Trace.lean | 2 ++ src/Std/Data.lean | 1 + .../Data/PersistentArray.lean} | 23 +++++++++++-------- 10 files changed, 24 insertions(+), 23 deletions(-) delete mode 100644 src/Init/Data/PersistentArray.lean rename src/{Init/Data/PersistentArray/Basic.lean => Std/Data/PersistentArray.lean} (99%) diff --git a/src/Init/Data.lean b/src/Init/Data.lean index dc831447b4..07c4a54f29 100644 --- a/src/Init/Data.lean +++ b/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 diff --git a/src/Init/Data/PersistentArray.lean b/src/Init/Data/PersistentArray.lean deleted file mode 100644 index a30feb7f28..0000000000 --- a/src/Init/Data/PersistentArray.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. -Authors: Leonardo de Moura --/ -prelude -import Init.Data.PersistentArray.Basic diff --git a/src/Lean/Compiler/IR/ElimDeadBranches.lean b/src/Lean/Compiler/IR/ElimDeadBranches.lean index 960c105ad8..3376ab4fce 100644 --- a/src/Lean/Compiler/IR/ElimDeadBranches.lean +++ b/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; diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean index ca85e43ff3..34e4f30919 100644 --- a/src/Lean/LocalContext.lean +++ b/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 := {}) diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 65a37fcdda..b0e984013d 100644 --- a/src/Lean/Message.lean +++ b/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 := ⟨{}⟩ diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 1c5d0be020..e429e077f0 100644 --- a/src/Lean/Meta/Basic.lean +++ b/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 := {}) diff --git a/src/Lean/Meta/LevelDefEq.lean b/src/Lean/Meta/LevelDefEq.lean index 41bddf54af..17530f485a 100644 --- a/src/Lean/Meta/LevelDefEq.lean +++ b/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; diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean index b579079627..87e9537c2b 100644 --- a/src/Lean/Util/Trace.lean +++ b/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) diff --git a/src/Std/Data.lean b/src/Std/Data.lean index a2a8161560..0e715db568 100644 --- a/src/Std/Data.lean +++ b/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 diff --git a/src/Init/Data/PersistentArray/Basic.lean b/src/Std/Data/PersistentArray.lean similarity index 99% rename from src/Init/Data/PersistentArray/Basic.lean rename to src/Std/Data/PersistentArray.lean index 435e05f079..2d053df753 100644 --- a/src/Init/Data/PersistentArray/Basic.lean +++ b/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