From 1be221a1f4d09829e93c7b570fe73ae294aa5014 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 25 Jun 2020 11:56:00 -0700 Subject: [PATCH] chore: move `PersistentHashMap` and `PersistentHashSet` to `Std` --- src/Init/Data/PersistentHashMap.lean | 7 ------- src/Lean/Attributes.lean | 2 ++ src/Lean/Data/SMap.lean | 4 +++- src/Lean/Expr.lean | 2 ++ src/Lean/Level.lean | 6 ++++-- src/Lean/LocalContext.lean | 2 ++ src/Lean/Meta/Basic.lean | 2 ++ src/Lean/Meta/DiscrTreeTypes.lean | 1 + src/Lean/MetavarContext.lean | 2 ++ src/Lean/Parser/Parser.lean | 4 ++-- src/Std/Data.lean | 2 ++ .../Basic.lean => Std/Data/PersistentHashMap.lean} | 5 ++--- src/{Init => Std}/Data/PersistentHashSet.lean | 5 +++-- src/Std/ShareCommon.lean | 4 ++-- 14 files changed, 29 insertions(+), 19 deletions(-) delete mode 100644 src/Init/Data/PersistentHashMap.lean rename src/{Init/Data/PersistentHashMap/Basic.lean => Std/Data/PersistentHashMap.lean} (99%) rename src/{Init => Std}/Data/PersistentHashSet.lean (96%) diff --git a/src/Init/Data/PersistentHashMap.lean b/src/Init/Data/PersistentHashMap.lean deleted file mode 100644 index ff75ec38e4..0000000000 --- a/src/Init/Data/PersistentHashMap.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.PersistentHashMap.Basic diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index a065dc8074..0f57d9a150 100644 --- a/src/Lean/Attributes.lean +++ b/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 {} diff --git a/src/Lean/Data/SMap.lean b/src/Lean/Data/SMap.lean index 52a9110be1..1c33dde832 100644 --- a/src/Lean/Data/SMap.lean +++ b/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. diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index 76648f442e..11be5d8dd4 100644 --- a/src/Lean/Expr.lean +++ b/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 diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean index 52c4f91c8f..6af327b70a 100644 --- a/src/Lean/Level.lean +++ b/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 diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean index bea8fde949..ca85e43ff3 100644 --- a/src/Lean/LocalContext.lean +++ b/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) := {}) diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 84130c43bb..1c5d0be020 100644 --- a/src/Lean/Meta/Basic.lean +++ b/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 := {}) diff --git a/src/Lean/Meta/DiscrTreeTypes.lean b/src/Lean/Meta/DiscrTreeTypes.lean index b267b41245..dad9d787b3 100644 --- a/src/Lean/Meta/DiscrTreeTypes.lean +++ b/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 α) := {}) diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 23066e9310..c9bff0de9e 100644 --- a/src/Lean/MetavarContext.lean +++ b/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 := {}) diff --git a/src/Lean/Parser/Parser.lean b/src/Lean/Parser/Parser.lean index c7aeb6c75e..4d24f21a04 100644 --- a/src/Lean/Parser/Parser.lean +++ b/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; diff --git a/src/Std/Data.lean b/src/Std/Data.lean index a75874df73..20036a4dd2 100644 --- a/src/Std/Data.lean +++ b/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 diff --git a/src/Init/Data/PersistentHashMap/Basic.lean b/src/Std/Data/PersistentHashMap.lean similarity index 99% rename from src/Init/Data/PersistentHashMap/Basic.lean rename to src/Std/Data/PersistentHashMap.lean index 69ba4d189d..bb880e040f 100644 --- a/src/Init/Data/PersistentHashMap/Basic.lean +++ b/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 diff --git a/src/Init/Data/PersistentHashSet.lean b/src/Std/Data/PersistentHashSet.lean similarity index 96% rename from src/Init/Data/PersistentHashSet.lean rename to src/Std/Data/PersistentHashSet.lean index c1ae1bb15a..ed2947da7d 100644 --- a/src/Init/Data/PersistentHashSet.lean +++ b/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 diff --git a/src/Std/ShareCommon.lean b/src/Std/ShareCommon.lean index 168a9b9b11..deca16fe81 100644 --- a/src/Std/ShareCommon.lean +++ b/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