From 85119ba9d1035e169a6d8718627314a096c19a29 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sat, 24 Sep 2022 00:09:26 -0400 Subject: [PATCH] chore: move Std.* data structures to Lean.* --- src/Lean/Attributes.lean | 4 +-- src/Lean/Compiler/ClosedTermCache.lean | 2 +- src/Lean/Compiler/IR/Basic.lean | 4 +-- src/Lean/Compiler/IR/Borrow.lean | 8 +++--- src/Lean/Compiler/IR/Boxing.lean | 4 +-- src/Lean/Compiler/IR/CompilerM.lean | 2 -- src/Lean/Compiler/IR/ElimDeadBranches.lean | 6 ++-- src/Lean/Compiler/IR/EmitUtil.lean | 4 +-- src/Lean/Compiler/IR/ExpandResetReuse.lean | 2 +- src/Lean/Compiler/IR/LiveVars.lean | 4 +-- src/Lean/Compiler/IR/RC.lean | 2 +- src/Lean/Compiler/LCNF/CSE.lean | 2 +- src/Lean/Compiler/LCNF/CompilerM.lean | 2 +- src/Lean/Compiler/LCNF/JoinPoints.lean | 10 +++---- src/Lean/Compiler/LCNF/LCtx.lean | 6 ++-- src/Lean/Compiler/LCNF/Level.lean | 3 +- src/Lean/Compiler/LCNF/PhaseExt.lean | 4 +-- src/Lean/Compiler/LCNF/Simp.lean | 2 +- src/Lean/Compiler/LCNF/Specialize.lean | 2 +- src/Lean/Compiler/LCNF/ToLCNF.lean | 6 ++-- src/Lean/Compiler/LCNF/Types.lean | 4 +-- src/Lean/CoreM.lean | 2 +- src/Lean/Data/AssocList.lean | 10 +++---- src/Lean/Data/Format.lean | 2 +- src/Lean/Data/HashMap.lean | 4 +-- src/Lean/Data/HashSet.lean | 2 +- src/Lean/Data/Json/Basic.lean | 2 -- src/Lean/Data/Json/Parser.lean | 6 +--- src/Lean/Data/JsonRpc.lean | 1 - src/Lean/Data/Lsp/Internal.lean | 1 - src/Lean/Data/NameMap.lean | 28 +++++++++---------- src/Lean/Data/PersistentArray.lean | 24 +++++++--------- src/Lean/Data/PersistentHashMap.lean | 2 +- src/Lean/Data/PersistentHashSet.lean | 2 +- src/Lean/Data/PrefixTree.lean | 1 - src/Lean/Data/RBMap.lean | 10 +++---- src/Lean/Data/RBTree.lean | 4 +-- src/Lean/Data/SMap.lean | 2 -- src/Lean/Data/Trie.lean | 2 -- src/Lean/Data/Xml/Basic.lean | 2 +- src/Lean/Data/Xml/Parser.lean | 2 +- src/Lean/DocString.lean | 4 +-- src/Lean/Elab/Command.lean | 4 +-- src/Lean/Elab/Deriving/Inhabited.lean | 2 +- src/Lean/Elab/Do.lean | 2 +- src/Lean/Elab/Extra.lean | 2 +- src/Lean/Elab/InfoTree/Main.lean | 6 +--- src/Lean/Elab/InfoTree/Types.lean | 6 ++-- src/Lean/Elab/PreDefinition/Eqns.lean | 2 +- src/Lean/Elab/Quotation.lean | 2 +- src/Lean/Elab/StructInst.lean | 1 - src/Lean/Elab/SyntheticMVars.lean | 2 +- src/Lean/Elab/Term.lean | 6 ++-- src/Lean/Environment.lean | 6 ++-- src/Lean/Expr.lean | 22 +++++++-------- src/Lean/KeyedDeclsAttribute.lean | 4 +-- src/Lean/Level.lean | 12 ++++---- src/Lean/Linter/MissingDocs.lean | 2 +- src/Lean/LocalContext.lean | 2 -- src/Lean/Message.lean | 2 +- src/Lean/Meta/AbstractMVars.lean | 2 -- src/Lean/Meta/Basic.lean | 2 -- src/Lean/Meta/DiscrTreeTypes.lean | 1 - src/Lean/Meta/Eqns.lean | 2 +- src/Lean/Meta/GlobalInstances.lean | 2 +- src/Lean/Meta/Instances.lean | 8 +++--- src/Lean/Meta/KExprMap.lean | 16 +++++------ src/Lean/Meta/Match/Match.lean | 4 +-- src/Lean/Meta/Match/MatchEqsExt.lean | 2 +- src/Lean/Meta/SynthInstance.lean | 2 -- src/Lean/Meta/Tactic/AC/Main.lean | 4 +-- src/Lean/Meta/Tactic/AuxLemma.lean | 2 +- src/Lean/Meta/Tactic/FVarSubst.lean | 2 +- src/Lean/Meta/Tactic/Simp/Rewrite.lean | 2 +- src/Lean/Meta/Tactic/Simp/SimpTheorems.lean | 12 ++++---- src/Lean/Meta/Tactic/Simp/Types.lean | 2 +- src/Lean/MetavarContext.lean | 2 -- src/Lean/Parser/Basic.lean | 12 ++++---- src/Lean/PrettyPrinter.lean | 2 +- .../PrettyPrinter/Delaborator/SubExpr.lean | 2 +- .../Delaborator/TopDownAnalyze.lean | 7 ++--- src/Lean/ScopedEnvExtension.lean | 4 +-- src/Lean/Server/Completion.lean | 2 +- src/Lean/Server/FileWorker.lean | 11 ++++---- src/Lean/Server/InfoUtils.lean | 12 ++++---- src/Lean/Server/References.lean | 1 - src/Lean/Server/Requests.lean | 4 +-- src/Lean/Server/Rpc/Basic.lean | 5 ++-- src/Lean/Server/Rpc/RequestHandling.lean | 2 +- src/Lean/Server/Snapshots.lean | 6 ++-- src/Lean/Server/Watchdog.lean | 1 - src/Lean/Structure.lean | 2 +- src/Lean/SubExpr.lean | 2 +- src/Lean/Util/HasConstCache.lean | 2 +- src/Lean/Util/MonadCache.lean | 6 ++-- src/Lean/Util/SCC.lean | 3 +- src/Lean/Util/ShareCommon.lean | 1 - src/Lean/Util/Trace.lean | 6 ++-- src/Lean/Widget/InteractiveDiagnostic.lean | 2 +- src/Lean/Widget/UserWidget.lean | 2 +- src/lake | 2 +- tests/bench/liasolver.lean | 10 +++---- tests/bench/rbmap.library.lean | 2 +- tests/compiler/phashmap.lean | 2 +- tests/compiler/phashmap2.lean | 2 +- tests/compiler/phashmap3.lean | 2 +- tests/compiler/rbmap_library.lean | 2 +- tests/lean/1206.lean | 2 +- tests/lean/PPRoundtrip.lean | 2 +- tests/lean/funInfoBug.lean | 6 ++-- tests/lean/funInfoBug.lean.expected.out | 2 +- tests/lean/moduleOf.lean | 2 +- tests/lean/phashmap_inst_coherence.lean | 2 +- tests/lean/run/944.lean | 2 +- tests/lean/run/998Export.lean | 1 - tests/lean/run/KyleAlg.lean | 2 +- tests/lean/run/PPTopDownAnalyze.lean | 4 +-- tests/lean/run/arthur1.lean | 2 +- tests/lean/run/arthur2.lean | 2 +- tests/lean/run/forInPArray.lean | 10 +++---- tests/lean/run/matchEqs.lean | 4 +-- tests/lean/run/parray1.lean | 2 +- tests/lean/run/sizeof6.lean | 2 +- 123 files changed, 223 insertions(+), 291 deletions(-) diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index 0e90a5f7a6..0b60c23553 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -52,8 +52,6 @@ structure AttributeImpl extends AttributeImplCore where erase (decl : Name) : AttrM Unit := throwError "attribute cannot be erased" deriving Inhabited -open Std (PersistentHashMap) - builtin_initialize attributeMapRef : IO.Ref (PersistentHashMap Name AttributeImpl) ← IO.mkRef {} /-- Low level attribute registration function. -/ @@ -304,7 +302,7 @@ end EnumAttributes -/ abbrev AttributeImplBuilder := Name → List DataValue → Except String AttributeImpl -abbrev AttributeImplBuilderTable := Std.HashMap Name AttributeImplBuilder +abbrev AttributeImplBuilderTable := HashMap Name AttributeImplBuilder builtin_initialize attributeImplBuilderTableRef : IO.Ref AttributeImplBuilderTable ← IO.mkRef {} diff --git a/src/Lean/Compiler/ClosedTermCache.lean b/src/Lean/Compiler/ClosedTermCache.lean index 8ebf01b778..69f5b9b302 100644 --- a/src/Lean/Compiler/ClosedTermCache.lean +++ b/src/Lean/Compiler/ClosedTermCache.lean @@ -8,7 +8,7 @@ import Lean.Environment namespace Lean structure ClosedTermCache where - map : Std.PHashMap Expr Name := {} + map : PHashMap Expr Name := {} constNames : NameSet := {} deriving Inhabited diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean index c15664726b..fff3039ed3 100644 --- a/src/Lean/Compiler/IR/Basic.lean +++ b/src/Lean/Compiler/IR/Basic.lean @@ -442,8 +442,6 @@ end Decl @[export lean_ir_mk_dummy_extern_decl] def mkDummyExternDecl (f : FunId) (xs : Array Param) (ty : IRType) : Decl := Decl.fdecl f xs ty FnBody.unreachable {} -open Std (RBTree RBTree.empty RBMap) - /-- Set of variable and join point names -/ abbrev IndexSet := RBTree Index compare instance : Inhabited IndexSet := ⟨{}⟩ @@ -496,7 +494,7 @@ def LocalContext.isLocalVar (ctx : LocalContext) (idx : Index) : Bool := | _ => false def LocalContext.contains (ctx : LocalContext) (idx : Index) : Bool := - Std.RBMap.contains ctx idx + RBMap.contains ctx idx def LocalContext.eraseJoinPointDecl (ctx : LocalContext) (j : JoinPointId) : LocalContext := ctx.erase j.idx diff --git a/src/Lean/Compiler/IR/Borrow.lean b/src/Lean/Compiler/IR/Borrow.lean index 57f839f5a5..d5500fc3bd 100644 --- a/src/Lean/Compiler/IR/Borrow.lean +++ b/src/Lean/Compiler/IR/Borrow.lean @@ -25,9 +25,9 @@ instance : Hashable Key := ⟨getHash⟩ end OwnedSet open OwnedSet (Key) in -abbrev OwnedSet := Std.HashMap Key Unit -def OwnedSet.insert (s : OwnedSet) (k : OwnedSet.Key) : OwnedSet := Std.HashMap.insert s k () -def OwnedSet.contains (s : OwnedSet) (k : OwnedSet.Key) : Bool := Std.HashMap.contains s k +abbrev OwnedSet := HashMap Key Unit +def OwnedSet.insert (s : OwnedSet) (k : OwnedSet.Key) : OwnedSet := HashMap.insert s k () +def OwnedSet.contains (s : OwnedSet) (k : OwnedSet.Key) : Bool := HashMap.contains s k /-! We perform borrow inference in a block of mutually recursive functions. Join points are viewed as local functions, and are identified using @@ -48,7 +48,7 @@ instance : Hashable Key := ⟨getHash⟩ end ParamMap open ParamMap (Key) -abbrev ParamMap := Std.HashMap Key (Array Param) +abbrev ParamMap := HashMap Key (Array Param) def ParamMap.fmt (map : ParamMap) : Format := let fmts := map.fold (fun fmt k ps => diff --git a/src/Lean/Compiler/IR/Boxing.lean b/src/Lean/Compiler/IR/Boxing.lean index fe87373661..75dc80277c 100644 --- a/src/Lean/Compiler/IR/Boxing.lean +++ b/src/Lean/Compiler/IR/Boxing.lean @@ -27,8 +27,6 @@ Assumptions: Reason: `resetreuse.lean` ignores `box` and `unbox` instructions. -/ -open Std (AssocList) - def mkBoxedName (n : Name) : Name := Name.mkStr n "_boxed" @@ -115,7 +113,7 @@ structure BoxingState where processing the same IR declaration. -/ auxDecls : Array Decl := #[] - auxDeclCache : AssocList FnBody Expr := Std.AssocList.empty + auxDeclCache : AssocList FnBody Expr := AssocList.empty nextAuxId : Nat := 1 abbrev M := ReaderT BoxingContext (StateT BoxingState Id) diff --git a/src/Lean/Compiler/IR/CompilerM.lean b/src/Lean/Compiler/IR/CompilerM.lean index 7af84f6b6e..95964faf6d 100644 --- a/src/Lean/Compiler/IR/CompilerM.lean +++ b/src/Lean/Compiler/IR/CompilerM.lean @@ -69,8 +69,6 @@ private def logMessageIfAux {α : Type} [ToFormat α] (optName : Name) (a : α) @[inline] def modifyEnv (f : Environment → Environment) : CompilerM Unit := modify fun s => { s with env := f s.env } -open Std (HashMap) - abbrev DeclMap := SMap Name Decl /-- Create an array of decls to be saved on .olean file. diff --git a/src/Lean/Compiler/IR/ElimDeadBranches.lean b/src/Lean/Compiler/IR/ElimDeadBranches.lean index d85163927c..0848c0547c 100644 --- a/src/Lean/Compiler/IR/ElimDeadBranches.lean +++ b/src/Lean/Compiler/IR/ElimDeadBranches.lean @@ -139,7 +139,7 @@ def addFunctionSummary (env : Environment) (fid : FunId) (v : Value) : Environme def getFunctionSummary? (env : Environment) (fid : FunId) : Option Value := (functionSummariesExt.getState env).find? fid -abbrev Assignment := Std.HashMap VarId Value +abbrev Assignment := HashMap VarId Value structure InterpContext where currFnIdx : Nat := 0 @@ -149,7 +149,7 @@ structure InterpContext where structure InterpState where assignments : Array Assignment - funVals : Std.PArray Value -- we take snapshots during fixpoint computations + funVals : PArray Value -- we take snapshots during fixpoint computations abbrev M := ReaderT InterpContext (StateM InterpState) @@ -316,7 +316,7 @@ def elimDeadBranches (decls : Array Decl) : CompilerM (Array Decl) := do let s ← get let env := s.env let assignments : Array Assignment := decls.map fun _ => {} - let funVals := Std.mkPArray decls.size Value.bot + let funVals := 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/Compiler/IR/EmitUtil.lean b/src/Lean/Compiler/IR/EmitUtil.lean index ca6d2caf6a..e5d0b1087c 100644 --- a/src/Lean/Compiler/IR/EmitUtil.lean +++ b/src/Lean/Compiler/IR/EmitUtil.lean @@ -50,8 +50,8 @@ end CollectUsedDecls def collectUsedDecls (env : Environment) (decl : Decl) (used : NameSet := {}) : NameSet := (CollectUsedDecls.collectDecl decl env).run' used -abbrev VarTypeMap := Std.HashMap VarId IRType -abbrev JPParamsMap := Std.HashMap JoinPointId (Array Param) +abbrev VarTypeMap := HashMap VarId IRType +abbrev JPParamsMap := HashMap JoinPointId (Array Param) namespace CollectMaps abbrev Collector := (VarTypeMap × JPParamsMap) → (VarTypeMap × JPParamsMap) diff --git a/src/Lean/Compiler/IR/ExpandResetReuse.lean b/src/Lean/Compiler/IR/ExpandResetReuse.lean index e49ca41053..aab8af752c 100644 --- a/src/Lean/Compiler/IR/ExpandResetReuse.lean +++ b/src/Lean/Compiler/IR/ExpandResetReuse.lean @@ -9,7 +9,7 @@ import Lean.Compiler.IR.FreeVars namespace Lean.IR.ExpandResetReuse /-- Mapping from variable to projections -/ -abbrev ProjMap := Std.HashMap VarId Expr +abbrev ProjMap := HashMap VarId Expr namespace CollectProjMap abbrev Collector := ProjMap → ProjMap @[inline] def collectVDecl (x : VarId) (v : Expr) : Collector := fun m => diff --git a/src/Lean/Compiler/IR/LiveVars.lean b/src/Lean/Compiler/IR/LiveVars.lean index bbdaa02d0b..64ce289551 100644 --- a/src/Lean/Compiler/IR/LiveVars.lean +++ b/src/Lean/Compiler/IR/LiveVars.lean @@ -79,13 +79,13 @@ def FnBody.hasLiveVar (b : FnBody) (ctx : LocalContext) (x : VarId) : Bool := (IsLive.visitFnBody x.idx b).run' ctx abbrev LiveVarSet := VarIdSet -abbrev JPLiveVarMap := Std.RBMap JoinPointId LiveVarSet (fun j₁ j₂ => compare j₁.idx j₂.idx) +abbrev JPLiveVarMap := RBMap JoinPointId LiveVarSet (fun j₁ j₂ => compare j₁.idx j₂.idx) instance : Inhabited LiveVarSet where default := {} def mkLiveVarSet (x : VarId) : LiveVarSet := - Std.RBTree.empty.insert x + RBTree.empty.insert x namespace LiveVars diff --git a/src/Lean/Compiler/IR/RC.lean b/src/Lean/Compiler/IR/RC.lean index 4071b008cd..557a72de79 100644 --- a/src/Lean/Compiler/IR/RC.lean +++ b/src/Lean/Compiler/IR/RC.lean @@ -19,7 +19,7 @@ structure VarInfo where consume : Bool := false -- true if the variable RC must be "consumed" deriving Inhabited -abbrev VarMap := Std.RBMap VarId VarInfo (fun x y => compare x.idx y.idx) +abbrev VarMap := RBMap VarId VarInfo (fun x y => compare x.idx y.idx) structure Context where env : Environment diff --git a/src/Lean/Compiler/LCNF/CSE.lean b/src/Lean/Compiler/LCNF/CSE.lean index a9edb30507..f1e4884af0 100644 --- a/src/Lean/Compiler/LCNF/CSE.lean +++ b/src/Lean/Compiler/LCNF/CSE.lean @@ -14,7 +14,7 @@ namespace Lean.Compiler.LCNF namespace CSE structure State where - map : Std.PHashMap Expr FVarId := {} + map : PHashMap Expr FVarId := {} subst : FVarSubst := {} abbrev M := StateRefT State CompilerM diff --git a/src/Lean/Compiler/LCNF/CompilerM.lean b/src/Lean/Compiler/LCNF/CompilerM.lean index 6c4c26b9e6..286af8b656 100644 --- a/src/Lean/Compiler/LCNF/CompilerM.lean +++ b/src/Lean/Compiler/LCNF/CompilerM.lean @@ -136,7 +136,7 @@ it is a free variable, a type (or type former), or `lcErased`. `Check.lean` contains a substitution validator. -/ -abbrev FVarSubst := Std.HashMap FVarId Expr +abbrev FVarSubst := HashMap FVarId Expr /-- Replace the free variables in `e` using the given substitution. diff --git a/src/Lean/Compiler/LCNF/JoinPoints.lean b/src/Lean/Compiler/LCNF/JoinPoints.lean index 35c5f864ea..0c0505e4fa 100644 --- a/src/Lean/Compiler/LCNF/JoinPoints.lean +++ b/src/Lean/Compiler/LCNF/JoinPoints.lean @@ -22,7 +22,7 @@ structure CandidateInfo where The set of candidates that rely on this candidate to be a join point. For a more detailed explanation see the documentation of `find` -/ - associated : Std.HashSet FVarId + associated : HashSet FVarId deriving Inhabited /-- @@ -32,14 +32,14 @@ structure FindState where /-- All current join point candidates accessible by their `FVarId`. -/ - candidates : Std.HashMap FVarId CandidateInfo := .empty + candidates : HashMap FVarId CandidateInfo := .empty /-- The `FVarId`s of all `fun` declarations that were declared within the current `fun`. -/ - scope : Std.HashSet FVarId := .empty + scope : HashSet FVarId := .empty -abbrev ReplaceCtx := Std.HashMap FVarId Name +abbrev ReplaceCtx := HashMap FVarId Name abbrev FindM := ReaderT (Option FVarId) StateRefT FindState CompilerM abbrev ReplaceM := ReaderT ReplaceCtx CompilerM @@ -62,7 +62,7 @@ private partial def eraseCandidate (fvarId : FVarId) : FindM Unit := do /-- Combinator for modifying the candidates in `FindM`. -/ -private def modifyCandidates (f : Std.HashMap FVarId CandidateInfo → Std.HashMap FVarId CandidateInfo) : FindM Unit := +private def modifyCandidates (f : HashMap FVarId CandidateInfo → HashMap FVarId CandidateInfo) : FindM Unit := modify (fun state => {state with candidates := f state.candidates }) /-- diff --git a/src/Lean/Compiler/LCNF/LCtx.lean b/src/Lean/Compiler/LCNF/LCtx.lean index 13f978f702..00b9253510 100644 --- a/src/Lean/Compiler/LCNF/LCtx.lean +++ b/src/Lean/Compiler/LCNF/LCtx.lean @@ -12,9 +12,9 @@ namespace Lean.Compiler.LCNF LCNF local context. -/ structure LCtx where - params : Std.HashMap FVarId Param := {} - letDecls : Std.HashMap FVarId LetDecl := {} - funDecls : Std.HashMap FVarId FunDecl := {} + params : HashMap FVarId Param := {} + letDecls : HashMap FVarId LetDecl := {} + funDecls : HashMap FVarId FunDecl := {} deriving Inhabited def LCtx.addParam (lctx : LCtx) (param : Param) : LCtx := diff --git a/src/Lean/Compiler/LCNF/Level.lean b/src/Lean/Compiler/LCNF/Level.lean index 72ec4d8ae2..c0d4d1e9b3 100644 --- a/src/Lean/Compiler/LCNF/Level.lean +++ b/src/Lean/Compiler/LCNF/Level.lean @@ -13,7 +13,6 @@ namespace Lean.Compiler.LCNF -/ namespace NormLevelParam -open Std /-! ## Universe level parameter normalizer @@ -135,4 +134,4 @@ def Decl.setLevelParams (decl : Decl) : Decl := let levelParams := (visitCode decl.value ∘ visitParams decl.params ∘ visitExpr decl.type) {} |>.params.toList { decl with levelParams } -end Lean.Compiler.LCNF \ No newline at end of file +end Lean.Compiler.LCNF diff --git a/src/Lean/Compiler/LCNF/PhaseExt.lean b/src/Lean/Compiler/LCNF/PhaseExt.lean index daa6964918..56f6164149 100644 --- a/src/Lean/Compiler/LCNF/PhaseExt.lean +++ b/src/Lean/Compiler/LCNF/PhaseExt.lean @@ -7,7 +7,7 @@ import Lean.Compiler.LCNF.PassManager namespace Lean.Compiler.LCNF -abbrev BaseExtState := Std.PHashMap Name Decl +abbrev BaseExtState := PHashMap Name Decl private abbrev declLt (a b : Decl) := Name.quickLt a.name b.name @@ -61,4 +61,4 @@ def forEachDecl (f : Decl → CoreM Unit) : CoreM Unit := do f decl baseExt.getState env |>.forM fun _ decl => f decl -end Lean.Compiler.LCNF \ No newline at end of file +end Lean.Compiler.LCNF diff --git a/src/Lean/Compiler/LCNF/Simp.lean b/src/Lean/Compiler/LCNF/Simp.lean index fa2ceb838f..94be282538 100644 --- a/src/Lean/Compiler/LCNF/Simp.lean +++ b/src/Lean/Compiler/LCNF/Simp.lean @@ -72,7 +72,7 @@ structure FunDeclInfoMap where /-- Mapping from local function name to inlining information. -/ - map : Std.HashMap FVarId FunDeclInfo := {} + map : HashMap FVarId FunDeclInfo := {} deriving Inhabited def FunDeclInfoMap.format (s : FunDeclInfoMap) : CompilerM Format := do diff --git a/src/Lean/Compiler/LCNF/Specialize.lean b/src/Lean/Compiler/LCNF/Specialize.lean index 77973e81d2..1c9674edad 100644 --- a/src/Lean/Compiler/LCNF/Specialize.lean +++ b/src/Lean/Compiler/LCNF/Specialize.lean @@ -15,7 +15,7 @@ import Lean.Compiler.LCNF.PhaseExt namespace Lean.Compiler.LCNF namespace Specialize -abbrev Cache := Std.PHashMap Expr Name +abbrev Cache := PHashMap Expr Name builtin_initialize specCacheExt : EnvExtension Cache ← registerEnvExtension (pure {}) diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean index f370945587..a42301e0da 100644 --- a/src/Lean/Compiler/LCNF/ToLCNF.lean +++ b/src/Lean/Compiler/LCNF/ToLCNF.lean @@ -190,11 +190,11 @@ structure State where /-- Local context containing the original Lean types (not LCNF ones). -/ lctx : LocalContext := {} /-- Cache from Lean regular expression to LCNF expression. -/ - cache : Std.PHashMap Expr Expr := {} + cache : PHashMap Expr Expr := {} /-- `toLCNFType` cache -/ - typeCache : Std.HashMap Expr Expr := {} + typeCache : HashMap Expr Expr := {} /-- isTypeFormerType cache -/ - isTypeFormerTypeCache : Std.HashMap Expr Bool := {} + isTypeFormerTypeCache : HashMap Expr Bool := {} /-- LCNF sequence, we chain it to create a LCNF `Code` object. -/ seq : Array Element := #[] /-- diff --git a/src/Lean/Compiler/LCNF/Types.lean b/src/Lean/Compiler/LCNF/Types.lean index acffc6938d..1bba86de2a 100644 --- a/src/Lean/Compiler/LCNF/Types.lean +++ b/src/Lean/Compiler/LCNF/Types.lean @@ -13,7 +13,7 @@ scoped notation:max "⊤" => lcAny namespace LCNF structure LCNFTypeExtState where - types : Std.PHashMap Name Expr := {} + types : PHashMap Name Expr := {} instLevelType : Core.InstantiateLevelCache := {} deriving Inhabited @@ -319,4 +319,4 @@ partial def getArrowArity (e : Expr) := | .forallE _ _ b _ => getArrowArity b + 1 | _ => 0 -end Lean.Compiler.LCNF \ No newline at end of file +end Lean.Compiler.LCNF diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index df399ad68b..ab84d1d1c1 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -22,7 +22,7 @@ register_builtin_option maxHeartbeats : Nat := { def getMaxHeartbeats (opts : Options) : Nat := maxHeartbeats.get opts * 1000 -abbrev InstantiateLevelCache := Std.PersistentHashMap Name (List Level × Expr) +abbrev InstantiateLevelCache := PersistentHashMap Name (List Level × Expr) /-- Cache for the `CoreM` monad -/ structure Cache where diff --git a/src/Lean/Data/AssocList.lean b/src/Lean/Data/AssocList.lean index a0cd18f01e..15f0a14c6f 100644 --- a/src/Lean/Data/AssocList.lean +++ b/src/Lean/Data/AssocList.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ universe u v w w' -namespace Std +namespace Lean /-- List-like type to avoid extra level of indirection -/ inductive AssocList (α : Type u) (β : Type v) where @@ -100,8 +100,8 @@ def all (p : α → β → Bool) : AssocList α β → Bool instance : ForIn m (AssocList α β) (α × β) where forIn := AssocList.forIn -end Std.AssocList +end Lean.AssocList -def List.toAssocList {α : Type u} {β : Type v} : List (α × β) → Std.AssocList α β - | [] => Std.AssocList.nil - | (a,b) :: es => Std.AssocList.cons a b (toAssocList es) +def List.toAssocList' {α : Type u} {β : Type v} : List (α × β) → Lean.AssocList α β + | [] => Lean.AssocList.nil + | (a,b) :: es => Lean.AssocList.cons a b (toAssocList' es) diff --git a/src/Lean/Data/Format.lean b/src/Lean/Data/Format.lean index e555b5e308..7a225d3f13 100644 --- a/src/Lean/Data/Format.lean +++ b/src/Lean/Data/Format.lean @@ -42,7 +42,7 @@ export Std (Format ToFormat Format.nest Format.nil Format.joinSep Format.line Format.sbracket Format.bracket Format.group Format.tag Format.pretty Format.fill Format.paren Format.join) -export Std.ToFormat (format) +export ToFormat (format) instance : ToFormat Name where format n := n.toString diff --git a/src/Lean/Data/HashMap.lean b/src/Lean/Data/HashMap.lean index 355cc5e5b9..060c720be6 100644 --- a/src/Lean/Data/HashMap.lean +++ b/src/Lean/Data/HashMap.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ import Lean.Data.AssocList -namespace Std +namespace Lean universe u v w def HashMapBucket (α : Type u) (β : Type v) := @@ -127,7 +127,7 @@ end HashMapImp def HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] := { m : HashMapImp α β // m.WellFormed } -open Std.HashMapImp +open Lean.HashMapImp def mkHashMap {α : Type u} {β : Type v} [BEq α] [Hashable α] (capacity := 0) : HashMap α β := ⟨ mkHashMapImp capacity, WellFormed.mkWff capacity ⟩ diff --git a/src/Lean/Data/HashSet.lean b/src/Lean/Data/HashSet.lean index f75100d805..8e73ce8036 100644 --- a/src/Lean/Data/HashSet.lean +++ b/src/Lean/Data/HashSet.lean @@ -3,7 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ -namespace Std +namespace Lean universe u v w def HashSetBucket (α : Type u) := diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean index fcd107bbc1..3c55e0dbbc 100644 --- a/src/Lean/Data/Json/Basic.lean +++ b/src/Lean/Data/Json/Basic.lean @@ -166,8 +166,6 @@ end JsonNumber def strLt (a b : String) := Decidable.decide (a < b) -open Std (RBNode RBNode.leaf) - inductive Json where | null | bool (b : Bool) diff --git a/src/Lean/Data/Json/Parser.lean b/src/Lean/Data/Json/Parser.lean index 2408df3a64..5b69170092 100644 --- a/src/Lean/Data/Json/Parser.lean +++ b/src/Lean/Data/Json/Parser.lean @@ -7,11 +7,7 @@ Authors: Gabriel Ebner, Marc Huisinga import Lean.Data.Json.Basic import Lean.Data.Parsec -namespace Lean - -open Std (RBNode RBNode.singleton RBNode.leaf) - -namespace Json.Parser +namespace Lean.Json.Parser open Lean.Parsec diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean index ebf8504394..716232deae 100644 --- a/src/Lean/Data/JsonRpc.lean +++ b/src/Lean/Data/JsonRpc.lean @@ -15,7 +15,6 @@ for use in the LSP server. -/ namespace Lean.JsonRpc open Json -open Std (RBNode) /-- In JSON-RPC, each request from the client editor to the language server comes with a request id so that the corresponding response can be identified or cancelled. -/ diff --git a/src/Lean/Data/Lsp/Internal.lean b/src/Lean/Data/Lsp/Internal.lean index d82a9dae57..d8e3b1cd0a 100644 --- a/src/Lean/Data/Lsp/Internal.lean +++ b/src/Lean/Data/Lsp/Internal.lean @@ -13,7 +13,6 @@ workers. These messages are not visible externally to users of the LSP server. -/ namespace Lean.Lsp -open Std /-! Most reference-related types have custom FromJson/ToJson implementations to reduce the size of the resulting JSON. -/ diff --git a/src/Lean/Data/NameMap.lean b/src/Lean/Data/NameMap.lean index 1b781a5c0a..dae6964c4c 100644 --- a/src/Lean/Data/NameMap.lean +++ b/src/Lean/Data/NameMap.lean @@ -12,11 +12,9 @@ namespace Lean instance : Coe String Name := ⟨Name.mkSimple⟩ -open Std (RBMap RBTree mkRBMap mkRBTree) +def NameMap (α : Type) := RBMap Name α Name.quickCmp -def NameMap (α : Type) := Std.RBMap Name α Name.quickCmp - -@[inline] def mkNameMap (α : Type) : NameMap α := Std.mkRBMap Name α Name.quickCmp +@[inline] def mkNameMap (α : Type) : NameMap α := mkRBMap Name α Name.quickCmp namespace NameMap variable {α : Type} @@ -26,14 +24,14 @@ instance (α : Type) : EmptyCollection (NameMap α) := ⟨mkNameMap α⟩ instance (α : Type) : Inhabited (NameMap α) where default := {} -def insert (m : NameMap α) (n : Name) (a : α) := Std.RBMap.insert m n a +def insert (m : NameMap α) (n : Name) (a : α) := RBMap.insert m n a -def contains (m : NameMap α) (n : Name) : Bool := Std.RBMap.contains m n +def contains (m : NameMap α) (n : Name) : Bool := RBMap.contains m n -@[inline] def find? (m : NameMap α) (n : Name) : Option α := Std.RBMap.find? m n +@[inline] def find? (m : NameMap α) (n : Name) : Option α := RBMap.find? m n instance : ForIn m (NameMap α) (Name × α) := - inferInstanceAs (ForIn _ (Std.RBMap ..) ..) + inferInstanceAs (ForIn _ (RBMap ..) ..) end NameMap @@ -43,10 +41,10 @@ namespace NameSet def empty : NameSet := mkRBTree Name Name.quickCmp instance : EmptyCollection NameSet := ⟨empty⟩ instance : Inhabited NameSet := ⟨empty⟩ -def insert (s : NameSet) (n : Name) : NameSet := Std.RBTree.insert s n -def contains (s : NameSet) (n : Name) : Bool := Std.RBMap.contains s n +def insert (s : NameSet) (n : Name) : NameSet := RBTree.insert s n +def contains (s : NameSet) (n : Name) : Bool := RBMap.contains s n instance : ForIn m NameSet Name := - inferInstanceAs (ForIn _ (Std.RBTree ..) ..) + inferInstanceAs (ForIn _ (RBTree ..) ..) end NameSet @@ -60,14 +58,14 @@ abbrev insert (s : NameSSet) (n : Name) : NameSSet := SSet.insert s n abbrev contains (s : NameSSet) (n : Name) : Bool := SSet.contains s n end NameSSet -def NameHashSet := Std.HashSet Name +def NameHashSet := HashSet Name namespace NameHashSet -@[inline] def empty : NameHashSet := Std.HashSet.empty +@[inline] def empty : NameHashSet := HashSet.empty instance : EmptyCollection NameHashSet := ⟨empty⟩ instance : Inhabited NameHashSet := ⟨{}⟩ -def insert (s : NameHashSet) (n : Name) := Std.HashSet.insert s n -def contains (s : NameHashSet) (n : Name) : Bool := Std.HashSet.contains s n +def insert (s : NameHashSet) (n : Name) := HashSet.insert s n +def contains (s : NameHashSet) (n : Name) : Bool := HashSet.contains s n end NameHashSet def MacroScopesView.isPrefixOf (v₁ v₂ : MacroScopesView) : Bool := diff --git a/src/Lean/Data/PersistentArray.lean b/src/Lean/Data/PersistentArray.lean index a3d578c86d..995a80e9a9 100644 --- a/src/Lean/Data/PersistentArray.lean +++ b/src/Lean/Data/PersistentArray.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura -/ universe u v w -namespace Std +namespace Lean inductive PersistentArrayNode (α : Type u) where | node (cs : Array (PersistentArrayNode α)) : PersistentArrayNode α @@ -41,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. -/ variable {α : Type u} -open Std.PersistentArrayNode +open PersistentArrayNode def empty : PersistentArray α := {} @@ -370,19 +370,15 @@ def mkPersistentArray {α : Type u} (n : Nat) (v : α) : PArray α := @[inline] def mkPArray {α : Type u} (n : Nat) (v : α) : PArray α := mkPersistentArray n v -end Std +end Lean -open Std (PersistentArray PersistentArray.empty) +open Lean (PersistentArray) -def List.toPersistentArrayAux {α : Type u} : List α → PersistentArray α → PersistentArray α +def List.toPArray' {α : Type u} (xs : List α) : PersistentArray α := + let rec loop : List α → PersistentArray α → PersistentArray α | [], t => t - | x::xs, t => toPersistentArrayAux xs (t.push x) + | x::xs, t => loop xs (t.push x) + loop xs {} -def List.toPersistentArray {α : Type u} (xs : List α) : PersistentArray α := - xs.toPersistentArrayAux {} - -def Array.toPersistentArray {α : Type u} (xs : Array α) : PersistentArray α := - xs.foldl (init := PersistentArray.empty) fun p x => p.push x - -@[inline] def Array.toPArray {α : Type u} (xs : Array α) : PersistentArray α := - xs.toPersistentArray +def Array.toPArray' {α : Type u} (xs : Array α) : PersistentArray α := + xs.foldl (init := .empty) fun p x => p.push x diff --git a/src/Lean/Data/PersistentHashMap.lean b/src/Lean/Data/PersistentHashMap.lean index 08e33e6095..0701b41686 100644 --- a/src/Lean/Data/PersistentHashMap.lean +++ b/src/Lean/Data/PersistentHashMap.lean @@ -3,7 +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 -/ -namespace Std +namespace Lean universe u v w w' namespace PersistentHashMap diff --git a/src/Lean/Data/PersistentHashSet.lean b/src/Lean/Data/PersistentHashSet.lean index e3366756d8..0cbcfacb07 100644 --- a/src/Lean/Data/PersistentHashSet.lean +++ b/src/Lean/Data/PersistentHashSet.lean @@ -5,7 +5,7 @@ Author: Leonardo de Moura -/ import Lean.Data.PersistentHashMap -namespace Std +namespace Lean universe u v structure PersistentHashSet (α : Type u) [BEq α] [Hashable α] where diff --git a/src/Lean/Data/PrefixTree.lean b/src/Lean/Data/PrefixTree.lean index bbc9eb5786..a5088b8c6f 100644 --- a/src/Lean/Data/PrefixTree.lean +++ b/src/Lean/Data/PrefixTree.lean @@ -6,7 +6,6 @@ Authors: Leonardo de Moura import Lean.Data.RBMap namespace Lean -open Std /- Similar to trie, but for arbitrary keys -/ inductive PrefixTreeNode (α : Type u) (β : Type v) where diff --git a/src/Lean/Data/RBMap.lean b/src/Lean/Data/RBMap.lean index be2543c4fa..d63c317e30 100644 --- a/src/Lean/Data/RBMap.lean +++ b/src/Lean/Data/RBMap.lean @@ -3,7 +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 -/ -namespace Std +namespace Lean universe u v w w' inductive Rbcolor where @@ -16,7 +16,7 @@ inductive RBNode (α : Type u) (β : α → Type v) where namespace RBNode variable {α : Type u} {β : α → Type v} {σ : Type w} -open Std.Rbcolor Nat +open Rbcolor Nat def depth (f : Nat → Nat → Nat) : RBNode α β → Nat | leaf => 0 @@ -246,7 +246,7 @@ instance : EmptyCollection (RBNode α β) := ⟨leaf⟩ end RBNode -open Std.RBNode +open Lean.RBNode /- TODO(Leo): define dRBMap -/ @@ -310,7 +310,7 @@ instance : ForIn m (RBMap α β cmp) (α × β) where | none => none instance [Repr α] [Repr β] : Repr (RBMap α β cmp) where - reprPrec m prec := Repr.addAppParen ("Std.rbmapOf " ++ repr m.toList) prec + reprPrec m prec := Repr.addAppParen ("Lean.rbmapOf " ++ repr m.toList) prec @[inline] def insert : RBMap α β cmp → α → β → RBMap α β cmp | ⟨t, w⟩, k, v => ⟨t.insert cmp k v, WellFormed.insertWff w rfl⟩ @@ -397,5 +397,3 @@ end RBMap def rbmapOf {α : Type u} {β : Type v} (l : List (α × β)) (cmp : α → α → Ordering) : RBMap α β cmp := RBMap.fromList l cmp - -end Std diff --git a/src/Lean/Data/RBTree.lean b/src/Lean/Data/RBTree.lean index 56f0adb358..3bcd15f477 100644 --- a/src/Lean/Data/RBTree.lean +++ b/src/Lean/Data/RBTree.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ import Lean.Data.RBMap -namespace Std +namespace Lean universe u v w def RBTree (α : Type u) (cmp : α → α → Ordering) : Type u := @@ -66,7 +66,7 @@ instance : ForIn m (RBTree α cmp) α where | none => none instance [Repr α] : Repr (RBTree α cmp) where - reprPrec t prec := Repr.addAppParen ("Std.rbtreeOf " ++ repr t.toList) prec + reprPrec t prec := Repr.addAppParen ("Lean.rbtreeOf " ++ repr t.toList) prec @[inline] def insert (t : RBTree α cmp) (a : α) : RBTree α cmp := RBMap.insert t a () diff --git a/src/Lean/Data/SMap.lean b/src/Lean/Data/SMap.lean index c635b8b498..b1ff44e389 100644 --- a/src/Lean/Data/SMap.lean +++ b/src/Lean/Data/SMap.lean @@ -9,8 +9,6 @@ universe u v w w' namespace Lean -open Std (HashMap 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/Data/Trie.lean b/src/Lean/Data/Trie.lean index fd996d23e9..848284eb22 100644 --- a/src/Lean/Data/Trie.lean +++ b/src/Lean/Data/Trie.lean @@ -10,8 +10,6 @@ import Lean.Data.Format namespace Lean namespace Parser -open Std (RBNode RBNode.leaf RBNode.singleton RBNode.find RBNode.insert) - inductive Trie (α : Type) where | Node : Option α → RBNode Char (fun _ => Trie α) → Trie α diff --git a/src/Lean/Data/Xml/Basic.lean b/src/Lean/Data/Xml/Basic.lean index 14e8a50abb..191251d4ca 100644 --- a/src/Lean/Data/Xml/Basic.lean +++ b/src/Lean/Data/Xml/Basic.lean @@ -9,7 +9,7 @@ import Lean.Data.RBMap namespace Lean namespace Xml -def Attributes := Std.RBMap String String compare +def Attributes := RBMap String String compare instance : ToString Attributes := ⟨λ as => as.fold (λ s n v => s ++ s!" {n}=\"{v}\"") ""⟩ mutual diff --git a/src/Lean/Data/Xml/Parser.lean b/src/Lean/Data/Xml/Parser.lean index c5f7744858..8b8dd40f41 100644 --- a/src/Lean/Data/Xml/Parser.lean +++ b/src/Lean/Data/Xml/Parser.lean @@ -410,7 +410,7 @@ protected def elementPrefix : Parsec (Array Content → Element) := do let name ← Name let attributes ← many (S *> Attribute) optional S *> pure () - return Element.Element name (Std.RBMap.fromList attributes.toList compare) + return Element.Element name (RBMap.fromList attributes.toList compare) /-- https://www.w3.org/TR/xml/#NT-EmptyElemTag -/ def EmptyElemTag (elem : Array Content → Element) : Parsec Element := do diff --git a/src/Lean/DocString.lean b/src/Lean/DocString.lean index 8e5ebcc609..48cbf7fbf4 100644 --- a/src/Lean/DocString.lean +++ b/src/Lean/DocString.lean @@ -71,7 +71,7 @@ structure ModuleDoc where doc : String declarationRange : DeclarationRange -private builtin_initialize moduleDocExt : SimplePersistentEnvExtension ModuleDoc (Std.PersistentArray ModuleDoc) ← registerSimplePersistentEnvExtension { +private builtin_initialize moduleDocExt : SimplePersistentEnvExtension ModuleDoc (PersistentArray ModuleDoc) ← registerSimplePersistentEnvExtension { name := `moduleDocExt addImportedFn := fun _ => {} addEntryFn := fun s e => s.push e @@ -81,7 +81,7 @@ private builtin_initialize moduleDocExt : SimplePersistentEnvExtension ModuleDoc def addMainModuleDoc (env : Environment) (doc : ModuleDoc) : Environment := moduleDocExt.addEntry env doc -def getMainModuleDoc (env : Environment) : Std.PersistentArray ModuleDoc := +def getMainModuleDoc (env : Environment) : PersistentArray ModuleDoc := moduleDocExt.getState env def getModuleDoc? (env : Environment) (moduleName : Name) : Option (Array ModuleDoc) := diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index cf97465221..b55f3c48cd 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -121,7 +121,7 @@ private def mkCoreContext (ctx : Context) (s : State) (heartbeats : Nat) : Core. private def addTraceAsMessagesCore (ctx : Context) (log : MessageLog) (traceState : TraceState) : MessageLog := Id.run do if traceState.traces.isEmpty then return log - let mut traces : Std.HashMap (String.Pos × String.Pos) (Array MessageData) := ∅ + let mut traces : HashMap (String.Pos × String.Pos) (Array MessageData) := ∅ for traceElem in traceState.traces do let ref := replaceRef traceElem.ref ctx.ref let pos := ref.getPos?.getD 0 @@ -221,7 +221,7 @@ opaque mkCommandElabAttribute : IO (KeyedDeclsAttribute CommandElab) builtin_initialize commandElabAttribute : KeyedDeclsAttribute CommandElab ← mkCommandElabAttribute -private def mkInfoTree (elaborator : Name) (stx : Syntax) (trees : Std.PersistentArray InfoTree) : CommandElabM InfoTree := do +private def mkInfoTree (elaborator : Name) (stx : Syntax) (trees : PersistentArray InfoTree) : CommandElabM InfoTree := do let ctx ← read let s ← get let scope := s.scopes.head! diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean index 0fefc397fd..ec19764cf0 100644 --- a/src/Lean/Elab/Deriving/Inhabited.lean +++ b/src/Lean/Elab/Deriving/Inhabited.lean @@ -9,7 +9,7 @@ namespace Lean.Elab open Command open Meta -private abbrev IndexSet := Std.RBTree Nat compare +private abbrev IndexSet := RBTree Nat compare private abbrev LocalInst2Index := FVarIdMap Nat private def implicitBinderF := Parser.Term.implicitBinder diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index 2754e14db5..4bd17366ab 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -213,7 +213,7 @@ def Code.getRef? : Code → Option Syntax | .match ref .. => ref | .jmp ref .. => ref -abbrev VarSet := Std.RBMap Name Syntax Name.cmp +abbrev VarSet := RBMap Name Syntax Name.cmp /-- A code block, and the collection of variables updated by it. -/ structure CodeBlock where diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean index c945d75379..d988dff15f 100644 --- a/src/Lean/Elab/Extra.lean +++ b/src/Lean/Elab/Extra.lean @@ -133,7 +133,7 @@ private inductive Tree where We store the `infoTrees` generated when elaborating `val`. These trees become subtrees of the infotree nodes generated for `op` nodes. -/ - | term (ref : Syntax) (infoTrees : Std.PersistentArray InfoTree) (val : Expr) + | term (ref : Syntax) (infoTrees : PersistentArray InfoTree) (val : Expr) /-- `ref` is the original syntax that expanded into `binop%`. `macroName` is the `macro_rule` that produce the expansion. We store this information diff --git a/src/Lean/Elab/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean index 18500cf951..0c626a034c 100644 --- a/src/Lean/Elab/InfoTree/Main.lean +++ b/src/Lean/Elab/InfoTree/Main.lean @@ -6,11 +6,7 @@ Authors: Wojciech Nawrocki, Leonardo de Moura, Sebastian Ullrich -/ import Lean.Meta.PPGoal -namespace Lean.Elab - -open Std (PersistentArray PersistentArray.empty PersistentHashMap) - -namespace ContextInfo +namespace Lean.Elab.ContextInfo variable [Monad m] [MonadEnv m] [MonadMCtx m] [MonadOptions m] [MonadResolveName m] [MonadNameGenerator m] diff --git a/src/Lean/Elab/InfoTree/Types.lean b/src/Lean/Elab/InfoTree/Types.lean index ab6aa28e46..065b1a7280 100644 --- a/src/Lean/Elab/InfoTree/Types.lean +++ b/src/Lean/Elab/InfoTree/Types.lean @@ -153,7 +153,7 @@ inductive InfoTree where /-- The context object is created by `liftTermElabM` at `Command.lean` -/ | context (i : ContextInfo) (t : InfoTree) /-- The children contain information for nested term elaboration and tactic evaluation -/ - | node (i : Info) (children : Std.PersistentArray InfoTree) + | node (i : Info) (children : PersistentArray InfoTree) /-- The elaborator creates holes (aka metavariables) for tactics and postponed terms -/ | hole (mvarId : MVarId) deriving Inhabited @@ -172,9 +172,9 @@ structure InfoState where /-- Whether info trees should be recorded. -/ enabled : Bool := true /-- Map from holes in the infotree to child infotrees. -/ - assignment : Std.PersistentHashMap MVarId InfoTree := {} + assignment : PersistentHashMap MVarId InfoTree := {} /-- Pending child trees of a node. -/ - trees : Std.PersistentArray InfoTree := {} + trees : PersistentArray InfoTree := {} deriving Inhabited class MonadInfoTree (m : Type → Type) where diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index 9ab0b767f1..379930652d 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Eqns.lean @@ -304,7 +304,7 @@ def tryContradiction (mvarId : MVarId) : MetaM Bool := do mvarId.contradictionCore { genDiseq := true } structure UnfoldEqnExtState where - map : Std.PHashMap Name Name := {} + map : PHashMap Name Name := {} deriving Inhabited /- We generate the unfold equation on demand, and do not save them on .olean files. -/ diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index 0d1f61304e..8591068a69 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -580,7 +580,7 @@ private partial def compileStxMatch (discrs : List Term) (alts : List Alt) : Ter `(let discr := $discr; $stx) | _, _ => unreachable! -abbrev IdxSet := Std.HashSet Nat +abbrev IdxSet := HashSet Nat /-- Given `rhss` the right-hand-sides of a `match`-syntax notation, diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index f21e8a457a..1bd55efe61 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -11,7 +11,6 @@ import Lean.Elab.Binders namespace Lean.Elab.Term.StructInst -open Std (HashMap) open Meta open TSyntax.Compat diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean index 72d007b61d..5f3fbb1590 100644 --- a/src/Lean/Elab/SyntheticMVars.lean +++ b/src/Lean/Elab/SyntheticMVars.lean @@ -278,7 +278,7 @@ private def getSomeSynthethicMVarsRef : TermElabM Syntax := do private def throwStuckAtUniverseCnstr : TermElabM Unit := do -- This code assumes `entries` is not empty. Note that `processPostponed` uses `exceptionOnFailure` to guarantee this property let entries ← getPostponed - let mut found : Std.HashSet (Level × Level) := {} + let mut found : HashSet (Level × Level) := {} let mut uniqueEntries := #[] for entry in entries do let mut lhs := entry.lhs diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 76053e8ddd..39854ee9bc 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -147,8 +147,8 @@ structure CacheKey where Cache for the `save` tactic. -/ structure Cache where - pre : Std.PHashMap CacheKey Snapshot := {} - post : Std.PHashMap CacheKey Snapshot := {} + pre : PHashMap CacheKey Snapshot := {} + post : PHashMap CacheKey Snapshot := {} deriving Inhabited end Tactic @@ -183,7 +183,7 @@ structure Context where `elabTypeWithUnboldImplicit`. Both methods add implicit declarations for the unbound variable and try again. -/ autoBoundImplicit : Bool := false - autoBoundImplicits : Std.PArray Expr := {} + autoBoundImplicits : PArray Expr := {} /-- A name `n` is only eligible to be an auto implicit name if `autoBoundImplicitForbidden n = false`. We use this predicate to disallow `f` to be considered an auto implicit name in a definition such diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 85241a96aa..1292d4a352 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -91,8 +91,6 @@ structure EnvironmentHeader where moduleData : Array ModuleData := #[] deriving Inhabited -open Std (HashMap) - /-- An environment stores declarations provided by the user. The kernel currently supports different kinds of declarations such as definitions, theorems, @@ -698,8 +696,8 @@ partial def importModules (imports : List Import) (opts : Options) (trustLevel : for mod in s.moduleData do numConsts := numConsts + mod.constants.size let mut modIdx : Nat := 0 - let mut const2ModIdx : HashMap Name ModuleIdx := Std.mkHashMap (capacity := numConsts) - let mut constantMap : HashMap Name ConstantInfo := Std.mkHashMap (capacity := numConsts) + let mut const2ModIdx : HashMap Name ModuleIdx := mkHashMap (capacity := numConsts) + let mut constantMap : HashMap Name ConstantInfo := mkHashMap (capacity := numConsts) for mod in s.moduleData do for cinfo in mod.constants do const2ModIdx := const2ModIdx.insert cinfo.name modIdx diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index dd9d83a8a3..ecc8bb50f4 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -246,24 +246,24 @@ instance : Repr FVarId where /-- A set of unique free variable identifiers. This is a persistent data structure implemented using red-black trees. -/ -def FVarIdSet := Std.RBTree FVarId (Name.quickCmp ·.name ·.name) +def FVarIdSet := RBTree FVarId (Name.quickCmp ·.name ·.name) deriving Inhabited, EmptyCollection -instance : ForIn m FVarIdSet FVarId := inferInstanceAs (ForIn _ (Std.RBTree ..) ..) +instance : ForIn m FVarIdSet FVarId := inferInstanceAs (ForIn _ (RBTree ..) ..) /-- A set of unique free variable identifiers implemented using hashtables. Hashtables are faster than red-black trees if they are used linearly. They are not persistent data-structures. -/ -def FVarIdHashSet := Std.HashSet FVarId +def FVarIdHashSet := HashSet FVarId deriving Inhabited, EmptyCollection /-- A mapping from free variable identifiers to values of type `α`. This is a persistent data structure implemented using red-black trees. -/ -def FVarIdMap (α : Type) := Std.RBMap FVarId α (Name.quickCmp ·.name ·.name) +def FVarIdMap (α : Type) := RBMap FVarId α (Name.quickCmp ·.name ·.name) -instance : EmptyCollection (FVarIdMap α) := inferInstanceAs (EmptyCollection (Std.RBMap ..)) +instance : EmptyCollection (FVarIdMap α) := inferInstanceAs (EmptyCollection (RBMap ..)) instance : Inhabited (FVarIdMap α) where default := {} @@ -276,16 +276,16 @@ structure MVarId where instance : Repr MVarId where reprPrec n p := reprPrec n.name p -def MVarIdSet := Std.RBTree MVarId (Name.quickCmp ·.name ·.name) +def MVarIdSet := RBTree MVarId (Name.quickCmp ·.name ·.name) deriving Inhabited, EmptyCollection -instance : ForIn m MVarIdSet MVarId := inferInstanceAs (ForIn _ (Std.RBTree ..) ..) +instance : ForIn m MVarIdSet MVarId := inferInstanceAs (ForIn _ (RBTree ..) ..) -def MVarIdMap (α : Type) := Std.RBMap MVarId α (Name.quickCmp ·.name ·.name) +def MVarIdMap (α : Type) := RBMap MVarId α (Name.quickCmp ·.name ·.name) -instance : EmptyCollection (MVarIdMap α) := inferInstanceAs (EmptyCollection (Std.RBMap ..)) +instance : EmptyCollection (MVarIdMap α) := inferInstanceAs (EmptyCollection (RBMap ..)) -instance : ForIn m (MVarIdMap α) (MVarId × α) := inferInstanceAs (ForIn _ (Std.RBMap ..) ..) +instance : ForIn m (MVarIdMap α) (MVarId × α) := inferInstanceAs (ForIn _ (RBMap ..) ..) instance : Inhabited (MVarIdMap α) where default := {} @@ -1244,8 +1244,6 @@ def mkDecIsTrue (pred proof : Expr) := def mkDecIsFalse (pred proof : Expr) := mkAppB (mkConst `Decidable.isFalse) pred proof -open Std (HashMap HashSet PHashMap PHashSet) - abbrev ExprMap (α : Type) := HashMap Expr α abbrev PersistentExprMap (α : Type) := PHashMap Expr α abbrev ExprSet := HashSet Expr diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean index 64771acfcf..be7634ffbb 100644 --- a/src/Lean/KeyedDeclsAttribute.lean +++ b/src/Lean/KeyedDeclsAttribute.lean @@ -55,8 +55,8 @@ abbrev Table (γ : Type) := SMap Key (List (AttributeEntry γ)) structure ExtensionState (γ : Type) where newEntries : List OLeanEntry := [] table : Table γ := {} - declNames : Std.PHashSet Name := {} - erased : Std.PHashSet Name := {} + declNames : PHashSet Name := {} + erased : PHashSet Name := {} deriving Inhabited abbrev Extension (γ : Type) := ScopedEnvExtension OLeanEntry (AttributeEntry γ) (ExtensionState γ) diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean index a563312384..c90dd68ec0 100644 --- a/src/Lean/Level.lean +++ b/src/Lean/Level.lean @@ -72,16 +72,16 @@ abbrev LMVarId := LevelMVarId instance : Repr LMVarId where reprPrec n p := reprPrec n.name p -def LMVarIdSet := Std.RBTree LMVarId (Name.quickCmp ·.name ·.name) +def LMVarIdSet := RBTree LMVarId (Name.quickCmp ·.name ·.name) deriving Inhabited, EmptyCollection -instance : ForIn m LMVarIdSet LMVarId := inferInstanceAs (ForIn _ (Std.RBTree ..) ..) +instance : ForIn m LMVarIdSet LMVarId := inferInstanceAs (ForIn _ (RBTree ..) ..) -def LMVarIdMap (α : Type) := Std.RBMap LMVarId α (Name.quickCmp ·.name ·.name) +def LMVarIdMap (α : Type) := RBMap LMVarId α (Name.quickCmp ·.name ·.name) -instance : EmptyCollection (LMVarIdMap α) := inferInstanceAs (EmptyCollection (Std.RBMap ..)) +instance : EmptyCollection (LMVarIdMap α) := inferInstanceAs (EmptyCollection (RBMap ..)) -instance : ForIn m (LMVarIdMap α) (LMVarId × α) := inferInstanceAs (ForIn _ (Std.RBMap ..) ..) +instance : ForIn m (LMVarIdMap α) (LMVarId × α) := inferInstanceAs (ForIn _ (RBMap ..) ..) instance : Inhabited (LMVarIdMap α) where default := {} @@ -598,8 +598,6 @@ termination_by _ u v => (u, v) end Level -open Std (HashMap HashSet PHashMap PHashSet) - abbrev LevelMap (α : Type) := HashMap Level α abbrev PersistentLevelMap (α : Type) := PHashMap Level α abbrev LevelSet := HashSet Level diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean index c69016cd68..19e237ad3a 100644 --- a/src/Lean/Linter/MissingDocs.lean +++ b/src/Lean/Linter/MissingDocs.lean @@ -148,7 +148,7 @@ def checkDecl : SimpleHandler := fun stx => do lintField rest[1][0] stx[1] "computed field" else if rest.getKind == ``«structure» then unless rest[5][2].isNone do - let redecls : Std.HashSet String.Pos := + let redecls : HashSet String.Pos := (← get).infoState.trees.foldl (init := {}) fun s tree => tree.foldInfo (init := s) fun _ info s => if let .ofFieldRedeclInfo info := info then diff --git a/src/Lean/LocalContext.lean b/src/Lean/LocalContext.lean index c0c53fedad..d6fd86d9d6 100644 --- a/src/Lean/LocalContext.lean +++ b/src/Lean/LocalContext.lean @@ -102,8 +102,6 @@ def hasExprMVar : LocalDecl → Bool end LocalDecl -open Std (PersistentHashMap PersistentArray PArray) - /-- A LocalContext is an ordered set of local variable declarations. It is used to store the free variables (also known as local constants) that are in scope. diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index d90cb70ba2..43dc3da5ba 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -207,7 +207,7 @@ protected def toString (msg : Message) (includeEndPos := false) : IO String := d end Message structure MessageLog where - msgs : Std.PersistentArray Message := {} + msgs : PersistentArray Message := {} deriving Inhabited namespace MessageLog diff --git a/src/Lean/Meta/AbstractMVars.lean b/src/Lean/Meta/AbstractMVars.lean index 50701eb017..a74ac2fb30 100644 --- a/src/Lean/Meta/AbstractMVars.lean +++ b/src/Lean/Meta/AbstractMVars.lean @@ -15,8 +15,6 @@ structure AbstractMVarsResult where namespace AbstractMVars -open Std (HashMap) - structure State where ngen : NameGenerator lctx : LocalContext diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index c35ce7b3e3..e13bc96cc6 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -205,8 +205,6 @@ instance : Hashable InfoCacheKey := ⟨fun ⟨transparency, expr, nargs⟩ => mixHash (hash transparency) <| mixHash (hash expr) (hash nargs)⟩ end InfoCacheKey -open Std (PersistentArray PersistentHashMap) - abbrev SynthInstanceCache := PersistentHashMap Expr (Option Expr) abbrev InferTypeCache := PersistentExprStructMap Expr diff --git a/src/Lean/Meta/DiscrTreeTypes.lean b/src/Lean/Meta/DiscrTreeTypes.lean index 5300aa4d77..a8f49bbaa1 100644 --- a/src/Lean/Meta/DiscrTreeTypes.lean +++ b/src/Lean/Meta/DiscrTreeTypes.lean @@ -38,7 +38,6 @@ inductive Trie (α : Type) where end DiscrTree open DiscrTree -open Std (PersistentHashMap) structure DiscrTree (α : Type) where root : PersistentHashMap Key (Trie α) := {} diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean index 238f3074a1..3f07258d9d 100644 --- a/src/Lean/Meta/Eqns.lean +++ b/src/Lean/Meta/Eqns.lean @@ -50,7 +50,7 @@ private def shouldGenerateEqnThms (declName : Name) : MetaM Bool := do return false structure EqnsExtState where - map : Std.PHashMap Name (Array Name) := {} + map : PHashMap Name (Array Name) := {} deriving Inhabited /- We generate the equations on demand, and do not save them on .olean files. -/ diff --git a/src/Lean/Meta/GlobalInstances.lean b/src/Lean/Meta/GlobalInstances.lean index 8723c07a49..6178e99269 100644 --- a/src/Lean/Meta/GlobalInstances.lean +++ b/src/Lean/Meta/GlobalInstances.lean @@ -8,7 +8,7 @@ import Lean.ScopedEnvExtension namespace Lean.Meta -builtin_initialize globalInstanceExtension : SimpleScopedEnvExtension Name (Std.PersistentHashMap Name Unit) ← +builtin_initialize globalInstanceExtension : SimpleScopedEnvExtension Name (PersistentHashMap Name Unit) ← registerSimpleScopedEnvExtension { name := `ginstanceExt initial := {} diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean index 0681639e4f..7fb8445a6e 100644 --- a/src/Lean/Meta/Instances.lean +++ b/src/Lean/Meta/Instances.lean @@ -26,8 +26,8 @@ instance : ToFormat InstanceEntry where structure Instances where discrTree : DiscrTree InstanceEntry := DiscrTree.empty - instanceNames : Std.PHashSet Name := {} - erased : Std.PHashSet Name := {} + instanceNames : PHashSet Name := {} + erased : PHashSet Name := {} deriving Inhabited def addInstanceEntry (d : Instances) (e : InstanceEntry) : Instances := @@ -78,7 +78,7 @@ builtin_initialize def getGlobalInstancesIndex : CoreM (DiscrTree InstanceEntry) := return Meta.instanceExtension.getState (← getEnv) |>.discrTree -def getErasedInstances : CoreM (Std.PHashSet Name) := +def getErasedInstances : CoreM (PHashSet Name) := return Meta.instanceExtension.getState (← getEnv) |>.erased def isInstance (declName : Name) : CoreM Bool := @@ -91,7 +91,7 @@ structure DefaultInstanceEntry where instanceName : Name priority : Nat -abbrev PrioritySet := Std.RBTree Nat (fun x y => compare y x) +abbrev PrioritySet := RBTree Nat (fun x y => compare y x) structure DefaultInstances where defaultInstances : NameMap (List (Name × Nat)) := {} diff --git a/src/Lean/Meta/KExprMap.lean b/src/Lean/Meta/KExprMap.lean index 7c37abd29b..d57b33df7d 100644 --- a/src/Lean/Meta/KExprMap.lean +++ b/src/Lean/Meta/KExprMap.lean @@ -10,12 +10,12 @@ namespace Lean.Meta /-- A mapping that indentifies definitionally equal expressions. - We implement it as a mapping from `HeadIndex` to `Std.AssocList Expr α`. + We implement it as a mapping from `HeadIndex` to `AssocList Expr α`. Remark: this map may be quite inefficient if there are many `HeadIndex` collisions. -/ structure KExprMap (α : Type) where - map : Std.PHashMap HeadIndex (Std.AssocList Expr α) := {} + map : PHashMap HeadIndex (AssocList Expr α) := {} deriving Inhabited /-- Return `some v` if there is an entry `e ↦ v` in `m`. -/ @@ -28,20 +28,20 @@ def KExprMap.find? (m : KExprMap α) (e : Expr) : MetaM (Option α) := do return some a return none -private def updateList (ps : Std.AssocList Expr α) (e : Expr) (v : α) : MetaM (Std.AssocList Expr α) := do +private def updateList (ps : AssocList Expr α) (e : Expr) (v : α) : MetaM (AssocList Expr α) := do match ps with - | Std.AssocList.nil => return Std.AssocList.cons e v ps - | Std.AssocList.cons e' v' ps => + | AssocList.nil => return AssocList.cons e v ps + | AssocList.cons e' v' ps => if (← isDefEq e e') then - return Std.AssocList.cons e v ps + return AssocList.cons e v ps else - return Std.AssocList.cons e' v' (← updateList ps e v) + return AssocList.cons e' v' (← updateList ps e v) /-- Insert `e ↦ v` into `m` -/ def KExprMap.insert (m : KExprMap α) (e : Expr) (v : α) : MetaM (KExprMap α) := let k := e.toHeadIndex match m.map.find? k with - | none => return { map := m.map.insert k (Std.AssocList.cons e v Std.AssocList.nil) } + | none => return { map := m.map.insert k (AssocList.cons e v AssocList.nil) } | some ps => return { map := m.map.insert k (← updateList ps e v) } end Lean.Meta diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index 71ff2fd0a3..e9bd6efbef 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -64,7 +64,7 @@ where loop lhss alts minors structure State where - used : Std.HashSet Nat := {} -- used alternatives + used : HashSet Nat := {} -- used alternatives counterExamples : List (List Example) := [] /-- Return true if the given (sub-)problem has been solved. -/ @@ -675,7 +675,7 @@ register_builtin_option bootstrap.genMatcherCode : Bool := { descr := "disable code generation for auxiliary matcher function" } -builtin_initialize matcherExt : EnvExtension (Std.PHashMap (Expr × Bool) Name) ← registerEnvExtension (pure {}) +builtin_initialize matcherExt : EnvExtension (PHashMap (Expr × Bool) Name) ← registerEnvExtension (pure {}) /-- Similar to `mkAuxDefinition`, but uses the cache `matcherExt`. It also returns an Boolean that indicates whether a new matcher function was added to the environment or not. -/ diff --git a/src/Lean/Meta/Match/MatchEqsExt.lean b/src/Lean/Meta/Match/MatchEqsExt.lean index 6484dbc3b7..68be6001ed 100644 --- a/src/Lean/Meta/Match/MatchEqsExt.lean +++ b/src/Lean/Meta/Match/MatchEqsExt.lean @@ -17,7 +17,7 @@ def MatchEqns.size (e : MatchEqns) : Nat := e.eqnNames.size structure MatchEqnsExtState where - map : Std.PHashMap Name MatchEqns := {} + map : PHashMap Name MatchEqns := {} deriving Inhabited /- We generate the equations and splitter on demand, and do not save them on .olean files. -/ diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index 4a3c2be27d..2cf607f805 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/src/Lean/Meta/SynthInstance.lean @@ -29,8 +29,6 @@ namespace SynthInstance def getMaxHeartbeats (opts : Options) : Nat := synthInstance.maxHeartbeats.get opts * 1000 -open Std (HashMap) - builtin_initialize inferTCGoalsRLAttr : TagAttribute ← registerTagAttribute `inferTCGoalsRL "instruct type class resolution procedure to solve goals from right to left for this instance" diff --git a/src/Lean/Meta/Tactic/AC/Main.lean b/src/Lean/Meta/Tactic/AC/Main.lean index d9e8e08b56..3a5fe8cc1b 100644 --- a/src/Lean/Meta/Tactic/AC/Main.lean +++ b/src/Lean/Meta/Tactic/AC/Main.lean @@ -63,9 +63,9 @@ inductive PreExpr def toACExpr (op l r : Expr) : MetaM (Array Expr × ACExpr) := do let (preExpr, vars) ← toPreExpr (mkApp2 op l r) - |>.run Std.HashSet.empty + |>.run HashSet.empty let vars := vars.toArray.insertionSort Expr.lt - let varMap := vars.foldl (fun xs x => xs.insert x xs.size) Std.HashMap.empty |>.find! + let varMap := vars.foldl (fun xs x => xs.insert x xs.size) HashMap.empty |>.find! return (vars, toACExpr varMap preExpr) where diff --git a/src/Lean/Meta/Tactic/AuxLemma.lean b/src/Lean/Meta/Tactic/AuxLemma.lean index 1e9a3ba288..d95ac684de 100644 --- a/src/Lean/Meta/Tactic/AuxLemma.lean +++ b/src/Lean/Meta/Tactic/AuxLemma.lean @@ -9,7 +9,7 @@ namespace Lean.Meta structure AuxLemmas where idx : Nat := 1 - lemmas : Std.PHashMap Expr (Name × List Name) := {} + lemmas : PHashMap Expr (Name × List Name) := {} deriving Inhabited builtin_initialize auxLemmasExt : EnvExtension AuxLemmas ← registerEnvExtension (pure {}) diff --git a/src/Lean/Meta/Tactic/FVarSubst.lean b/src/Lean/Meta/Tactic/FVarSubst.lean index a344950c4a..ebc51dac71 100644 --- a/src/Lean/Meta/Tactic/FVarSubst.lean +++ b/src/Lean/Meta/Tactic/FVarSubst.lean @@ -16,7 +16,7 @@ namespace Lean.Meta to an expression. The free variables occurring in the expression must be defined in the new goal. -/ structure FVarSubst where - map : Std.AssocList FVarId Expr := {} + map : AssocList FVarId Expr := {} deriving Inhabited namespace FVarSubst diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean index a960f76cc6..d5c16b6bdf 100644 --- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean @@ -127,7 +127,7 @@ def tryTheorem? (e : Expr) (thm : SimpTheorem) (discharge? : Expr → SimpM (Opt /-- Remark: the parameter tag is used for creating trace messages. It is irrelevant otherwise. -/ -def rewrite? (e : Expr) (s : DiscrTree SimpTheorem) (erased : Std.PHashSet Origin) (discharge? : Expr → SimpM (Option Expr)) (tag : String) (rflOnly : Bool) : SimpM (Option Result) := do +def rewrite? (e : Expr) (s : DiscrTree SimpTheorem) (erased : PHashSet Origin) (discharge? : Expr → SimpM (Option Expr)) (tag : String) (rflOnly : Bool) : SimpM (Option Result) := do let candidates ← s.getMatchWithExtra e if candidates.isEmpty then trace[Debug.Meta.Tactic.simp] "no theorems found for {tag}-rewriting {e}" diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean index 570fe31c75..dcc99c5cdf 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean +++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean @@ -140,10 +140,10 @@ instance : BEq SimpTheorem where structure SimpTheorems where pre : DiscrTree SimpTheorem := DiscrTree.empty post : DiscrTree SimpTheorem := DiscrTree.empty - lemmaNames : Std.PHashSet Origin := {} - toUnfold : Std.PHashSet Name := {} - erased : Std.PHashSet Origin := {} - toUnfoldThms : Std.PHashMap Name (Array Name) := {} + lemmaNames : PHashSet Origin := {} + toUnfold : PHashSet Name := {} + erased : PHashSet Origin := {} + toUnfoldThms : PHashMap Name (Array Name) := {} deriving Inhabited def addSimpTheoremEntry (d : SimpTheorems) (e : SimpTheorem) : SimpTheorems := @@ -152,7 +152,7 @@ def addSimpTheoremEntry (d : SimpTheorems) (e : SimpTheorem) : SimpTheorems := else { d with pre := d.pre.insertCore e.keys e, lemmaNames := updateLemmaNames d.lemmaNames } where - updateLemmaNames (s : Std.PHashSet Origin) : Std.PHashSet Origin := + updateLemmaNames (s : PHashSet Origin) : PHashSet Origin := s.insert e.origin def SimpTheorems.addDeclToUnfoldCore (d : SimpTheorems) (declName : Name) : SimpTheorems := @@ -367,7 +367,7 @@ def mkSimpExt (extName : Name) : IO SimpExtension := | SimpEntry.toUnfoldThms n thms => d.registerDeclToUnfoldThms n thms } -abbrev SimpExtensionMap := Std.HashMap Name SimpExtension +abbrev SimpExtensionMap := HashMap Name SimpExtension builtin_initialize simpExtensionMapRef : IO.Ref SimpExtensionMap ← IO.mkRef {} diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index 2620e6e54a..5e43fd79f4 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -35,7 +35,7 @@ def Context.isDeclToUnfold (ctx : Context) (declName : Name) : Bool := def Context.mkDefault : MetaM Context := return { config := {}, simpTheorems := #[(← getSimpTheorems)], congrTheorems := (← getSimpCongrTheorems) } -abbrev UsedSimps := Std.HashMap Origin Nat +abbrev UsedSimps := HashMap Origin Nat structure State where cache : Cache := {} diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index 2c3b3faf95..bb77662da1 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -301,8 +301,6 @@ structure DelayedMetavarAssignment where fvars : Array Expr mvarIdPending : MVarId -open Std (HashMap PersistentHashMap) - /-- The metavariable context is a set of metavariable declarations and their assignments. For more information on specifics see the comment in the file that `MetavarContext` is defined in. diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index 9f77a9d61c..d9bd5f77bc 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -98,10 +98,10 @@ def initCacheForInput (input : String) : ParserCache := { abbrev TokenTable := Trie Token -abbrev SyntaxNodeKindSet := Std.PersistentHashMap SyntaxNodeKind Unit +abbrev SyntaxNodeKindSet := PersistentHashMap SyntaxNodeKind Unit def SyntaxNodeKindSet.insert (s : SyntaxNodeKindSet) (k : SyntaxNodeKind) : SyntaxNodeKindSet := - Std.PersistentHashMap.insert s k () + PersistentHashMap.insert s k () /-- Input string and related data. Recall that the `FileMap` is a helper structure for mapping @@ -1550,8 +1550,6 @@ def eoiFn : ParserFn := fun c s => def eoi : Parser := { fn := eoiFn } -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.quickCmp @@ -1559,8 +1557,8 @@ namespace TokenMap def insert (map : TokenMap α) (k : Name) (v : α) : TokenMap α := match map.find? k with - | none => Std.RBMap.insert map k [v] - | some vs => Std.RBMap.insert map k (v::vs) + | none => RBMap.insert map k [v] + | some vs => RBMap.insert map k (v::vs) instance : Inhabited (TokenMap α) := ⟨RBMap.empty⟩ @@ -1641,7 +1639,7 @@ structure ParserCategory where behavior : LeadingIdentBehavior deriving Inhabited -abbrev ParserCategories := Std.PersistentHashMap Name ParserCategory +abbrev ParserCategories := PersistentHashMap Name ParserCategory def indexed {α : Type} (map : TokenMap α) (c : ParserContext) (s : ParserState) (behavior : LeadingIdentBehavior) : ParserState × List α := let (s, stx) := peekToken c s diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean index 0ecf9dc1d9..5b8682616c 100644 --- a/src/Lean/PrettyPrinter.lean +++ b/src/Lean/PrettyPrinter.lean @@ -38,7 +38,7 @@ def ppExpr (e : Expr) : MetaM Format := do /-- Return a `fmt` representing pretty-printed `e` together with a map from tags in `fmt` to `Elab.Info` nodes produced by the delaborator at various subexpressions of `e`. -/ def ppExprWithInfos (e : Expr) (optsPerPos : Delaborator.OptionsPerPos := {}) (delab := Delaborator.delab) - : MetaM (Format × Std.RBMap Nat Elab.Info compare) := do + : MetaM (Format × RBMap Nat Elab.Info compare) := do let lctx := (← getLCtx).sanitizeNames.run' { options := (← getOptions) } Meta.withLCtx lctx #[] do let (stx, infos) ← delabCore e optsPerPos delab diff --git a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean index 7ad38f54d9..e09bddb5a6 100644 --- a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean +++ b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean @@ -15,7 +15,7 @@ in sync with the `Nat` "position" values that refer to them. namespace Lean.PrettyPrinter.Delaborator -abbrev OptionsPerPos := Std.RBMap SubExpr.Pos Options compare +abbrev OptionsPerPos := RBMap SubExpr.Pos Options compare namespace SubExpr diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean index 925764ad49..3b1134f7e6 100644 --- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean @@ -23,10 +23,7 @@ that are not strictly necessary. -/ namespace Lean - -open Lean.Meta -open Lean.SubExpr -open Std (RBMap) +open Meta SubExpr register_builtin_option pp.analyze : Bool := { defValue := false @@ -197,7 +194,7 @@ def isHBinOp (e : Expr) : Bool := Id.run do def replaceLPsWithVars (e : Expr) : MetaM Expr := do if !e.hasLevelParam then return e let lps := collectLevelParams {} e |>.params - let mut replaceMap : Std.HashMap Name Level := {} + let mut replaceMap : HashMap Name Level := {} for lp in lps do replaceMap := replaceMap.insert lp (← mkFreshLevelMVar) return e.replaceLevel fun | Level.param n .. => replaceMap.find! n diff --git a/src/Lean/ScopedEnvExtension.lean b/src/Lean/ScopedEnvExtension.lean index f6e7cde484..475da37e77 100644 --- a/src/Lean/ScopedEnvExtension.lean +++ b/src/Lean/ScopedEnvExtension.lean @@ -20,7 +20,7 @@ structure State (σ : Type) where activeScopes : NameSet := {} structure ScopedEntries (β : Type) where - map : SMap Name (Std.PArray β) := {} + map : SMap Name (PArray β) := {} deriving Inhabited structure StateStack (α : Type) (β : Type) (σ : Type) where @@ -51,7 +51,7 @@ def mkInitial (descr : Descr α β σ) : IO (StateStack α β σ) := def ScopedEntries.insert (scopedEntries : ScopedEntries β) (ns : Name) (b : β) : ScopedEntries β := match scopedEntries.map.find? ns with - | none => { map := scopedEntries.map.insert ns <| ({} : Std.PArray β).push b } + | none => { map := scopedEntries.map.insert ns <| ({} : PArray β).push b } | some bs => { map := scopedEntries.map.insert ns <| bs.push b } def addImportedFn (descr : Descr α β σ) (as : Array (Array (Entry α))) : ImportM (StateStack α β σ) := do diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean index 9794d4fbed..717c1e0c80 100644 --- a/src/Lean/Server/Completion.lean +++ b/src/Lean/Server/Completion.lean @@ -404,7 +404,7 @@ private def optionCompletion (ctx : ContextInfo) (stx : Syntax) (caps : ClientCa else (ss.toString, false) -- HACK(WN): unfold the type so ForIn works - let (decls : Std.RBMap _ _ _) ← getOptionDecls + let (decls : RBMap _ _ _) ← getOptionDecls let opts ← getOptions let mut items := #[] for ⟨name, decl⟩ in decls do diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 8babd5f130..9a3e28e341 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -53,7 +53,6 @@ namespace Lean.Server.FileWorker open Lsp open IO open Snapshots -open Std (RBMap RBMap.empty) open JsonRpc structure WorkerContext where @@ -146,7 +145,7 @@ structure WorkerState where pendingRequests : PendingRequestMap /-- A map of RPC session IDs. We allow asynchronous elab tasks and request handlers to modify sessions. A single `Ref` ensures atomic transactions. -/ - rpcSessions : Std.RBMap UInt64 (IO.Ref RpcSession) compare + rpcSessions : RBMap UInt64 (IO.Ref RpcSession) compare abbrev WorkerM := ReaderT WorkerContext <| StateRefT WorkerState IO @@ -226,9 +225,9 @@ section Initialization Elab.InfoTree.node (Elab.Info.ofCommandInfo { elaborator := `import stx := importStx - }) #[].toPersistentArray - )).toPersistentArray - )].toPersistentArray + }) #[].toPArray' + )).toPArray' + )].toPArray' }} let headerSnap := { beginPos := 0 @@ -261,7 +260,7 @@ section Initialization return (ctx, { doc := doc pendingRequests := RBMap.empty - rpcSessions := Std.RBMap.empty + rpcSessions := RBMap.empty }) end Initialization diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index b7f453b093..7835545405 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -10,8 +10,8 @@ namespace Lean.Elab /-- Visit nodes, passing in a surrounding context (the innermost one) and accumulating results on the way back up. -/ partial def InfoTree.visitM [Monad m] - (preNode : ContextInfo → Info → (children : Std.PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ()) - (postNode : ContextInfo → Info → (children : Std.PersistentArray InfoTree) → List (Option α) → m α) + (preNode : ContextInfo → Info → (children : PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ()) + (postNode : ContextInfo → Info → (children : PersistentArray InfoTree) → List (Option α) → m α) : InfoTree → m (Option α) := go none where go @@ -25,20 +25,20 @@ where go /-- `InfoTree.visitM` specialized to `Unit` return type -/ def InfoTree.visitM' [Monad m] - (preNode : ContextInfo → Info → (children : Std.PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ()) - (postNode : ContextInfo → Info → (children : Std.PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ()) + (preNode : ContextInfo → Info → (children : PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ()) + (postNode : ContextInfo → Info → (children : PersistentArray InfoTree) → m Unit := fun _ _ _ => pure ()) (t : InfoTree) : m Unit := t.visitM preNode (fun ci i cs _ => postNode ci i cs) |> discard /-- Visit nodes bottom-up, passing in a surrounding context (the innermost one) and the union of nested results (empty at leaves). -/ -def InfoTree.collectNodesBottomUp (p : ContextInfo → Info → Std.PersistentArray InfoTree → List α → List α) (i : InfoTree) : List α := +def InfoTree.collectNodesBottomUp (p : ContextInfo → Info → PersistentArray InfoTree → List α → List α) (i : InfoTree) : List α := i.visitM (m := Id) (postNode := fun ci i cs as => p ci i cs (as.filterMap id).join) |>.getD [] /-- For every branch of the `InfoTree`, find the deepest node in that branch for which `p` returns `some _` and return the union of all such nodes. The visitor `p` is given a node together with its innermost surrounding `ContextInfo`. -/ -partial def InfoTree.deepestNodes (p : ContextInfo → Info → Std.PersistentArray InfoTree → Option α) (infoTree : InfoTree) : List α := +partial def InfoTree.deepestNodes (p : ContextInfo → Info → PersistentArray InfoTree → Option α) (infoTree : InfoTree) : List α := infoTree.collectNodesBottomUp fun ctx i cs rs => if rs.isEmpty then match p ctx i cs with diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean index f591a1bacc..711dc74495 100644 --- a/src/Lean/Server/References.lean +++ b/src/Lean/Server/References.lean @@ -101,7 +101,6 @@ end Lean.Lsp.ModuleRefs namespace Lean.Server open IO -open Std open Lsp open Elab diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean index 0fa4afb48c..86b3f749cb 100644 --- a/src/Lean/Server/Requests.lean +++ b/src/Lean/Server/Requests.lean @@ -56,7 +56,7 @@ def parseRequestParams (paramType : Type) [FromJson paramType] (params : Json) message := s!"Cannot parse request params: {params.compress}\n{inner}" } structure RequestContext where - rpcSessions : Std.RBMap UInt64 (IO.Ref FileWorker.RpcSession) compare + rpcSessions : RBMap UInt64 (IO.Ref FileWorker.RpcSession) compare srcSearchPath : SearchPath doc : FileWorker.EditableDocument hLog : IO.FS.Stream @@ -181,7 +181,7 @@ structure RequestHandler where fileSource : Json → Except RequestError Lsp.DocumentUri handle : Json → RequestM (RequestTask Json) -builtin_initialize requestHandlers : IO.Ref (Std.PersistentHashMap String RequestHandler) ← +builtin_initialize requestHandlers : IO.Ref (PersistentHashMap String RequestHandler) ← IO.mkRef {} /-- NB: This method may only be called in `initialize` blocks (user or builtin). diff --git a/src/Lean/Server/Rpc/Basic.lean b/src/Lean/Server/Rpc/Basic.lean index 7318502a08..482c266e8b 100644 --- a/src/Lean/Server/Rpc/Basic.lean +++ b/src/Lean/Server/Rpc/Basic.lean @@ -30,7 +30,6 @@ instance : ToString RpcRef where end Lean.Lsp namespace Lean.Server -open Std structure RpcObjectStore : Type where /-- Objects that are being kept alive for the RPC client, together with their type names, @@ -39,7 +38,7 @@ structure RpcObjectStore : Type where Note that we may currently have multiple references to the same object. It is only disposed of once all of those are gone. This simplifies the client a bit as it can drop every reference received separately. -/ - aliveRefs : Std.PersistentHashMap Lsp.RpcRef Dynamic := {} + aliveRefs : PersistentHashMap Lsp.RpcRef Dynamic := {} /-- Value to use for the next `RpcRef`. It is monotonically increasing to avoid any possible bugs resulting from its reuse. -/ nextRef : USize := 0 @@ -71,7 +70,7 @@ The type wrapper `WithRpcRef` is used for these fields which should be sent as a reference. - Any type with `FromJson` and `ToJson` instance is automatically `RpcEncodable`. -- If a type has an `Std.Dynamic` instance, then `WithRpcRef` can be used for its references. +- If a type has an `Dynamic` instance, then `WithRpcRef` can be used for its references. - `deriving RpcEncodable` acts like `FromJson`/`ToJson` but marshalls any `WithRpcRef` fields as `Lsp.RpcRef`s. -/ diff --git a/src/Lean/Server/Rpc/RequestHandling.lean b/src/Lean/Server/Rpc/RequestHandling.lean index 606bc0b866..04bf080b1a 100644 --- a/src/Lean/Server/Rpc/RequestHandling.lean +++ b/src/Lean/Server/Rpc/RequestHandling.lean @@ -18,7 +18,7 @@ private structure RpcProcedure where /- We store the builtin RPC handlers in a Ref and users' handlers in an extension. This ensures that users don't need to import core Lean modules to make builtin handlers work, but also that they *can* easily create custom handlers and use them in the same file. -/ -builtin_initialize builtinRpcProcedures : IO.Ref (Std.PHashMap Name RpcProcedure) ← +builtin_initialize builtinRpcProcedures : IO.Ref (PHashMap Name RpcProcedure) ← IO.mkRef {} builtin_initialize userRpcProcedures : MapDeclarationExtension Name ← mkMapDeclarationExtension `userRpcProcedures diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean index dc1fdd4403..e03e00d9a7 100644 --- a/src/Lean/Server/Snapshots.lean +++ b/src/Lean/Server/Snapshots.lean @@ -36,7 +36,7 @@ structure Snapshot where /-- We cache interactive diagnostics in order not to invoke the pretty-printer again on messages from previous snapshots when publishing diagnostics for every new snapshot (this is quadratic), as well as not to invoke it once again when handling `$/lean/interactiveDiagnostics`. -/ - interactiveDiags : Std.PersistentArray Widget.InteractiveDiagnostic + interactiveDiags : PersistentArray Widget.InteractiveDiagnostic tacticCache : IO.Ref Tactic.Cache instance : Inhabited Snapshot where @@ -60,7 +60,7 @@ def env (s : Snapshot) : Environment := def msgLog (s : Snapshot) : MessageLog := s.cmdState.messages -def diagnostics (s : Snapshot) : Std.PersistentArray Lsp.Diagnostic := +def diagnostics (s : Snapshot) : PersistentArray Lsp.Diagnostic := s.interactiveDiags.map fun d => d.toDiagnostic def infoTree (s : Snapshot) : InfoTree := @@ -173,7 +173,7 @@ where /-- Compute the current interactive diagnostics log by finding a "diff" relative to the parent snapshot. We need to do this because unlike the `MessageLog` itself, interactive diags are not part of the command state. -/ - withNewInteractiveDiags (msgLog : MessageLog) : IO (Std.PersistentArray Widget.InteractiveDiagnostic) := do + withNewInteractiveDiags (msgLog : MessageLog) : IO (PersistentArray Widget.InteractiveDiagnostic) := do let newMsgCount := msgLog.msgs.size - snap.msgLog.msgs.size let mut ret := snap.interactiveDiags for i in List.iota newMsgCount do diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 98e34eaa7a..b86d2009b6 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -65,7 +65,6 @@ non-standard extensions in case they're needed, for example to communicate tacti namespace Lean.Server.Watchdog open IO -open Std (RBMap RBMap.empty) open Lsp open JsonRpc open System.Uri diff --git a/src/Lean/Structure.lean b/src/Lean/Structure.lean index 2686fcd659..bf06c5fb54 100644 --- a/src/Lean/Structure.lean +++ b/src/Lean/Structure.lean @@ -40,7 +40,7 @@ def StructureInfo.getProjFn? (info : StructureInfo) (i : Nat) : Option Name := /-- Auxiliary state for structures defined in the current module. -/ private structure StructureState where - map : Std.PersistentHashMap Name StructureInfo := {} + map : PersistentHashMap Name StructureInfo := {} deriving Inhabited builtin_initialize structureExt : SimplePersistentEnvExtension StructureInfo StructureState ← registerSimplePersistentEnvExtension { diff --git a/src/Lean/SubExpr.lean b/src/Lean/SubExpr.lean index eb30cf6517..e8c705e9ed 100644 --- a/src/Lean/SubExpr.lean +++ b/src/Lean/SubExpr.lean @@ -168,7 +168,7 @@ def mkRoot (e : Expr) : SubExpr := ⟨e, Pos.root⟩ def isRoot (s : SubExpr) : Bool := s.pos.isRoot /-- Map from subexpr positions to values. -/ -abbrev PosMap (α : Type u) := Std.RBMap Pos α compare +abbrev PosMap (α : Type u) := RBMap Pos α compare def bindingBody! : SubExpr → SubExpr | ⟨.forallE _ _ b _, p⟩ => ⟨b, p.pushBindingBody⟩ diff --git a/src/Lean/Util/HasConstCache.lean b/src/Lean/Util/HasConstCache.lean index bad4046f9b..9972fb70a2 100644 --- a/src/Lean/Util/HasConstCache.lean +++ b/src/Lean/Util/HasConstCache.lean @@ -8,7 +8,7 @@ import Lean.Expr namespace Lean structure HasConstCache (declName : Name) where - cache : Std.HashMapImp Expr Bool := Std.mkHashMapImp + cache : HashMapImp Expr Bool := mkHashMapImp unsafe def HasConstCache.containsUnsafe (e : Expr) : StateM (HasConstCache declName) Bool := do if let some r := (← get).cache.find? (beq := ⟨ptrEq⟩) e then diff --git a/src/Lean/Util/MonadCache.lean b/src/Lean/Util/MonadCache.lean index 0af5ed5654..072a0f1d9c 100644 --- a/src/Lean/Util/MonadCache.lean +++ b/src/Lean/Util/MonadCache.lean @@ -29,8 +29,6 @@ instance {α β ε : Type} {m : Type → Type} [MonadCache α β m] [Monad m] : findCached? a := ExceptT.lift $ MonadCache.findCached? a cache a b := ExceptT.lift $ MonadCache.cache a b -open Std (HashMap) - /-- Adapter for implementing `MonadCache` interface using `HashMap`s. We just have to specify how to extract/modify the `HashMap`. -/ class MonadHashMapCacheAdapter (α β : Type) (m : Type → Type) [BEq α] [Hashable α] where @@ -63,7 +61,7 @@ instance : MonadHashMapCacheAdapter α β (MonadCacheT α β m) where modifyCache f := (modify f : StateRefT' ..) @[inline] def run {σ} (x : MonadCacheT α β m σ) : m σ := - x.run' Std.mkHashMap + x.run' mkHashMap instance : Monad (MonadCacheT α β m) := inferInstanceAs (Monad (StateRefT' _ _ _)) instance : MonadLift m (MonadCacheT α β m) := inferInstanceAs (MonadLift m (StateRefT' _ _ _)) @@ -87,7 +85,7 @@ instance : MonadHashMapCacheAdapter α β (MonadStateCacheT α β m) where modifyCache f := (modify f : StateT ..) @[inline] def run {σ} (x : MonadStateCacheT α β m σ) : m σ := - x.run' Std.mkHashMap + x.run' mkHashMap instance : Monad (MonadStateCacheT α β m) := inferInstanceAs (Monad (StateT _ _)) instance : MonadLift m (MonadStateCacheT α β m) := inferInstanceAs (MonadLift m (StateT _ _)) diff --git a/src/Lean/Util/SCC.lean b/src/Lean/Util/SCC.lean index 605ce49a4a..63d89ca771 100644 --- a/src/Lean/Util/SCC.lean +++ b/src/Lean/Util/SCC.lean @@ -11,7 +11,6 @@ namespace Lean.SCC compiler mutually recursive definitions, where each function (and nested let-rec) in the mutual block is a vertex. So, the graphs are small. -/ -open Std section variable (α : Type) [BEq α] [Hashable α] @@ -24,7 +23,7 @@ structure Data where structure State where stack : List α := [] nextIndex : Nat := 0 - data : Std.HashMap α Data := {} + data : HashMap α Data := {} sccs : List (List α) := [] abbrev M := StateM (State α) diff --git a/src/Lean/Util/ShareCommon.lean b/src/Lean/Util/ShareCommon.lean index 983a265728..5cd559a9de 100644 --- a/src/Lean/Util/ShareCommon.lean +++ b/src/Lean/Util/ShareCommon.lean @@ -10,7 +10,6 @@ import Lean.Data.PersistentHashSet open ShareCommon namespace Lean.ShareCommon -open Std def objectFactory := StateFactory.mk { diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean index e271553093..3cd56affc5 100644 --- a/src/Lean/Util/Trace.lean +++ b/src/Lean/Util/Trace.lean @@ -57,8 +57,6 @@ try to follow these guidelines: namespace Lean -open Std (PersistentArray) - structure TraceElem where ref : Syntax msg : MessageData @@ -68,7 +66,7 @@ structure TraceState where traces : PersistentArray TraceElem := {} deriving Inhabited -builtin_initialize inheritedTraceOptions : IO.Ref (Std.HashSet Name) ← IO.mkRef ∅ +builtin_initialize inheritedTraceOptions : IO.Ref (HashSet Name) ← IO.mkRef ∅ class MonadTrace (m : Type → Type) where modifyTraceState : (TraceState → TraceState) → m Unit @@ -89,7 +87,7 @@ def printTraces : m Unit := do def resetTraceState : m Unit := modifyTraceState (fun _ => {}) -private def checkTraceOption (inherited : Std.HashSet Name) (opts : Options) (cls : Name) : Bool := +private def checkTraceOption (inherited : HashSet Name) (opts : Options) (cls : Name) : Bool := !opts.isEmpty && go (`trace ++ cls) where go (opt : Name) : Bool := diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean index df7c8e5e58..aff5219afb 100644 --- a/src/Lean/Widget/InteractiveDiagnostic.lean +++ b/src/Lean/Widget/InteractiveDiagnostic.lean @@ -57,7 +57,7 @@ private def mkPPContext (nCtx : NamingContext) (ctx : MessageDataContext) : PPCo private inductive EmbedFmt /-- Tags denote `Info` objects. -/ - | expr (ctx : Elab.ContextInfo) (infos : Std.RBMap Nat Elab.Info compare) + | expr (ctx : Elab.ContextInfo) (infos : RBMap Nat Elab.Info compare) | goal (ctx : Elab.ContextInfo) (lctx : LocalContext) (g : MVarId) /-- Some messages (in particular, traces) are too costly to print eagerly. Instead, we allow the user to expand sub-traces interactively. -/ diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean index c6f6d9fb61..d2d07fbf80 100644 --- a/src/Lean/Widget/UserWidget.lean +++ b/src/Lean/Widget/UserWidget.lean @@ -51,7 +51,7 @@ structure UserWidget where private abbrev WidgetSourceRegistry := SimplePersistentEnvExtension (UInt64 × Name) - (Std.RBMap UInt64 Name compare) + (RBMap UInt64 Name compare) -- Mapping widgetSourceId to hash of sourcetext builtin_initialize userWidgetRegistry : MapDeclarationExtension UserWidget ← mkMapDeclarationExtension `widgetRegistry diff --git a/src/lake b/src/lake index 4df4f90ce3..cabb1223b0 160000 --- a/src/lake +++ b/src/lake @@ -1 +1 @@ -Subproject commit 4df4f90ce35124ff015717fd8c30f82749ff8337 +Subproject commit cabb1223b02c6bf799bf99b4329e6b666e2bbc9a diff --git a/tests/bench/liasolver.lean b/tests/bench/liasolver.lean index 78c91a39eb..9a1266f94a 100644 --- a/tests/bench/liasolver.lean +++ b/tests/bench/liasolver.lean @@ -6,7 +6,7 @@ Author: Marc Huisinga import Lean.Data.HashMap -open Std +open Lean namespace Int @@ -23,7 +23,7 @@ namespace Int end Int -namespace Std.AssocList +namespace Lean.AssocList def map (f : α → β → δ) : AssocList α β → AssocList α δ | AssocList.nil => AssocList.nil @@ -37,9 +37,9 @@ namespace Std.AssocList else filter p t -end Std.AssocList +end Lean.AssocList -namespace Std.HashMap +namespace Lean.HashMap variable [BEq α] [Hashable α] @@ -93,7 +93,7 @@ namespace Std.HashMap return some (k, v) return none -end Std.HashMap +end Lean.HashMap structure Equation where id : Nat diff --git a/tests/bench/rbmap.library.lean b/tests/bench/rbmap.library.lean index a3afa97e92..daea811fb3 100644 --- a/tests/bench/rbmap.library.lean +++ b/tests/bench/rbmap.library.lean @@ -1,6 +1,6 @@ import Lean.Data.RBMap -open Std +open Lean abbrev Tree : Type := RBMap Nat Bool compare diff --git a/tests/compiler/phashmap.lean b/tests/compiler/phashmap.lean index ec3fd61c1b..79dd439b31 100644 --- a/tests/compiler/phashmap.lean +++ b/tests/compiler/phashmap.lean @@ -1,7 +1,7 @@ import Lean.Data.PersistentHashMap import Lean.Data.Format -open Lean Std Std.PersistentHashMap +open Lean Std Lean.PersistentHashMap abbrev Map := PersistentHashMap Nat Nat diff --git a/tests/compiler/phashmap2.lean b/tests/compiler/phashmap2.lean index 9e64691687..18745da505 100644 --- a/tests/compiler/phashmap2.lean +++ b/tests/compiler/phashmap2.lean @@ -1,6 +1,6 @@ import Lean.Data.PersistentHashMap import Lean.Data.Format -open Lean Std Std.PersistentHashMap +open Lean Std Lean.PersistentHashMap abbrev Map := PersistentHashMap Nat Nat diff --git a/tests/compiler/phashmap3.lean b/tests/compiler/phashmap3.lean index 006627d135..8f54db813a 100644 --- a/tests/compiler/phashmap3.lean +++ b/tests/compiler/phashmap3.lean @@ -1,6 +1,6 @@ import Lean.Data.PersistentHashMap import Lean.Data.Format -open Lean Std Std.PersistentHashMap +open Lean Std Lean.PersistentHashMap abbrev Map := PersistentHashMap Nat Nat diff --git a/tests/compiler/rbmap_library.lean b/tests/compiler/rbmap_library.lean index bef32dc999..1577cab6b7 100644 --- a/tests/compiler/rbmap_library.lean +++ b/tests/compiler/rbmap_library.lean @@ -1,5 +1,5 @@ import Lean.Data.RBMap -open Std +open Lean def check (b : Bool) : IO Unit := do unless b do IO.println "ERROR" diff --git a/tests/lean/1206.lean b/tests/lean/1206.lean index 9a353d858a..9b617bdb9b 100644 --- a/tests/lean/1206.lean +++ b/tests/lean/1206.lean @@ -2,7 +2,7 @@ import Lean.Data.HashSet set_option linter.unusedVariables true -open Std +open Lean def boo : Id (HashSet Nat) := do let mut vs : HashSet Nat := HashSet.empty diff --git a/tests/lean/PPRoundtrip.lean b/tests/lean/PPRoundtrip.lean index 81e1d98089..91d4211b21 100644 --- a/tests/lean/PPRoundtrip.lean +++ b/tests/lean/PPRoundtrip.lean @@ -58,7 +58,7 @@ section #eval checkM `(id Nat) #eval checkM `(Sum Nat Nat) end -#eval checkM `(id (id Nat)) (Std.RBMap.empty.insert (SubExpr.Pos.ofArray #[1]) $ KVMap.empty.insert `pp.explicit true) +#eval checkM `(id (id Nat)) (Lean.RBMap.empty.insert (SubExpr.Pos.ofArray #[1]) $ 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 : α) := () diff --git a/tests/lean/funInfoBug.lean b/tests/lean/funInfoBug.lean index f65df231b1..2ad39a2a0f 100644 --- a/tests/lean/funInfoBug.lean +++ b/tests/lean/funInfoBug.lean @@ -3,11 +3,11 @@ import Lean.Data.AssocList def l : List (Prod Nat Nat) := [(1, 1), (2, 2)] #eval l -- works -def Std.AssocList.ToList : AssocList α β → List (α × β) +def Lean.AssocList.ToList : AssocList α β → List (α × β) | AssocList.nil => [] | AssocList.cons k v t => (k, v) :: ToList t -instance [Repr α] [Repr β] : Repr (Std.AssocList α β) where +instance [Repr α] [Repr β] : Repr (Lean.AssocList α β) where reprPrec f _ := repr f.ToList -#reduce (l.toAssocList) +#reduce (l.toAssocList') diff --git a/tests/lean/funInfoBug.lean.expected.out b/tests/lean/funInfoBug.lean.expected.out index 924299a583..094d02b5b7 100644 --- a/tests/lean/funInfoBug.lean.expected.out +++ b/tests/lean/funInfoBug.lean.expected.out @@ -1,2 +1,2 @@ [(1, 1), (2, 2)] -Std.AssocList.cons 1 1 (Std.AssocList.cons 2 2 Std.AssocList.nil) +Lean.AssocList.cons 1 1 (Lean.AssocList.cons 2 2 Lean.AssocList.nil) diff --git a/tests/lean/moduleOf.lean b/tests/lean/moduleOf.lean index 3aba1981e2..0ed70033b8 100644 --- a/tests/lean/moduleOf.lean +++ b/tests/lean/moduleOf.lean @@ -8,7 +8,7 @@ def tst : MetaM Unit := do IO.println (← findModuleOf? `HAdd.hAdd) IO.println (← findModuleOf? `Lean.Core.CoreM) IO.println (← findModuleOf? `Lean.Elab.Term.elabTerm) - IO.println (← findModuleOf? `Std.HashMap.insert) + IO.println (← findModuleOf? `Lean.HashMap.insert) IO.println (← findModuleOf? `tst) IO.println (← findModuleOf? `f) IO.println (← findModuleOf? `foo) -- Error: unknown 'foo' diff --git a/tests/lean/phashmap_inst_coherence.lean b/tests/lean/phashmap_inst_coherence.lean index 8fe09722d6..72bba90319 100644 --- a/tests/lean/phashmap_inst_coherence.lean +++ b/tests/lean/phashmap_inst_coherence.lean @@ -1,6 +1,6 @@ import Lean.Data.PersistentHashMap -open Std +open Lean def m : PersistentHashMap Nat Nat := let m : PersistentHashMap Nat Nat := {}; m.insert 1 1 diff --git a/tests/lean/run/944.lean b/tests/lean/run/944.lean index 0bf6ecba1e..31ba45504d 100644 --- a/tests/lean/run/944.lean +++ b/tests/lean/run/944.lean @@ -37,5 +37,5 @@ def f3 : Nat := def f4 (x : Nat) : Nat := .succ x -example (xs : List α) : Std.RBTree α ord := +example (xs : List α) : Lean.RBTree α ord := xs.foldl .insert ∅ diff --git a/tests/lean/run/998Export.lean b/tests/lean/run/998Export.lean index b6a2384f2b..dd02b62466 100644 --- a/tests/lean/run/998Export.lean +++ b/tests/lean/run/998Export.lean @@ -1,6 +1,5 @@ import Lean open Lean -open Std (HashMap HashSet) inductive Entry | name (n : Name) diff --git a/tests/lean/run/KyleAlg.lean b/tests/lean/run/KyleAlg.lean index 2163a80c55..10fb741b21 100644 --- a/tests/lean/run/KyleAlg.lean +++ b/tests/lean/run/KyleAlg.lean @@ -232,7 +232,7 @@ unsafe def Expr.dagSizeUnsafe (e : Expr) : IO Nat := do let (_, s) ← visit e |>.run ({}, 0) return s.2 where - visit (e : Expr) : StateRefT (Std.HashSet USize × Nat) IO Unit := do + visit (e : Expr) : StateRefT (HashSet USize × Nat) IO Unit := do let addr := ptrAddrUnsafe e unless (← get).1.contains addr do modify fun (s, c) => (s.insert addr, c+1) diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean index 37a88a6438..d7a001c02d 100644 --- a/tests/lean/run/PPTopDownAnalyze.lean +++ b/tests/lean/run/PPTopDownAnalyze.lean @@ -345,8 +345,8 @@ set_option pp.analyze.trustSubtypeMk true in #testDelabN Lean.Elab.InfoTree.goalsAt?.match_1 #testDelabN Array.mk.injEq #testDelabN Lean.PrefixTree.empty -#testDelabN Std.PersistentHashMap.getCollisionNodeSize.match_1 -#testDelabN Std.HashMap.size.match_1 +#testDelabN Lean.PersistentHashMap.getCollisionNodeSize.match_1 +#testDelabN Lean.HashMap.size.match_1 #testDelabN and_false -- TODO: this one prints out a structure instance with keyword field `end` diff --git a/tests/lean/run/arthur1.lean b/tests/lean/run/arthur1.lean index 2af0c5043a..73f6d50959 100644 --- a/tests/lean/run/arthur1.lean +++ b/tests/lean/run/arthur1.lean @@ -67,7 +67,7 @@ inductive Value | lam : Lambda → Value deriving Inhabited -abbrev Context := Std.HashMap String Value +abbrev Context := Lean.HashMap String Value inductive ErrorType | name | type | runTime diff --git a/tests/lean/run/arthur2.lean b/tests/lean/run/arthur2.lean index 65e0517013..c4d6a0f997 100644 --- a/tests/lean/run/arthur2.lean +++ b/tests/lean/run/arthur2.lean @@ -67,7 +67,7 @@ inductive Value | lam : Lambda → Value deriving Inhabited -abbrev Context := Std.HashMap String Value +abbrev Context := Lean.HashMap String Value inductive ErrorType | name | type | runTime diff --git a/tests/lean/run/forInPArray.lean b/tests/lean/run/forInPArray.lean index 8df2868abd..4217c55894 100644 --- a/tests/lean/run/forInPArray.lean +++ b/tests/lean/run/forInPArray.lean @@ -4,7 +4,7 @@ def check (x : IO Nat) (expected : IO Nat) : IO Unit := do unless (← x) == (← expected) do throw $ IO.userError "unexpected result" -def f1 (xs : Std.PArray Nat) (top : Nat) : IO Nat := do +def f1 (xs : Lean.PArray Nat) (top : Nat) : IO Nat := do let mut sum := 0 for x in xs do if x % 2 == 0 then @@ -15,11 +15,11 @@ for x in xs do IO.println s!"sum: {sum}" return sum -#eval f1 [1, 2, 3, 4, 5, 10, 20].toPersistentArray 10 +#eval f1 [1, 2, 3, 4, 5, 10, 20].toPArray' 10 -#eval check (f1 [1, 2, 3, 4, 5, 10, 20].toPersistentArray 10) (pure 16) +#eval check (f1 [1, 2, 3, 4, 5, 10, 20].toPArray' 10) (pure 16) -def f2 (xs : Std.PArray Nat) (top : Nat) : IO Nat := do +def f2 (xs : Lean.PArray Nat) (top : Nat) : IO Nat := do let mut sum := 0 for x in xs do if x % 2 == 0 then @@ -30,4 +30,4 @@ for x in xs do IO.println s!"sum: {sum}" return sum -#eval check (f1 (List.iota 100).toPersistentArray 1000) (f2 (List.iota 100).toPersistentArray 1000) +#eval check (f1 (List.iota 100).toPArray' 1000) (f2 (List.iota 100).toPArray' 1000) diff --git a/tests/lean/run/matchEqs.lean b/tests/lean/run/matchEqs.lean index f51dfa0403..23c5c3f6b8 100644 --- a/tests/lean/run/matchEqs.lean +++ b/tests/lean/run/matchEqs.lean @@ -24,5 +24,5 @@ theorem ex (x : List Nat) : f x > 0 := by simp [f] split <;> decide -test% Std.RBNode.balance1.match_1 -#check @Std.RBNode.balance1.match_1.splitter +test% Lean.RBNode.balance1.match_1 +#check @Lean.RBNode.balance1.match_1.splitter diff --git a/tests/lean/run/parray1.lean b/tests/lean/run/parray1.lean index 0e4045e5e4..e31abef640 100644 --- a/tests/lean/run/parray1.lean +++ b/tests/lean/run/parray1.lean @@ -1,7 +1,7 @@ import Lean.Data.PersistentArray def check [BEq α] (as : List α) : Bool := - as.toPersistentArray.foldr (.::.) [] == as + as.toPArray'.foldr (.::.) [] == as def tst1 : IO Unit := do assert! check [1, 2, 3] diff --git a/tests/lean/run/sizeof6.lean b/tests/lean/run/sizeof6.lean index 99cb85f582..cf1f6d67f2 100644 --- a/tests/lean/run/sizeof6.lean +++ b/tests/lean/run/sizeof6.lean @@ -1,7 +1,7 @@ import Lean.Data.PersistentArray inductive Foo where - | mk (args : Std.PersistentArray Foo) + | mk (args : Lean.PersistentArray Foo) #print Foo.mk.sizeOf_spec #print Foo._sizeOf_2_eq