From 09de5cd70ea3ef08d3a02ac0db389cd87bc58ea3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Mon, 21 Jul 2025 16:04:45 +0200 Subject: [PATCH] refactor: remove Lean.RBMap usages (#9260) This PR removes uses of `Lean.RBMap` in Lean itself. Furthermore some massaging of the import graph is done in order to avoid having `Std.Data.TreeMap.AdditionalOperations` (which is quite expensive) be the critical path for a large chunk of Lean. In particular we can build `Lean.Meta.Simp` and `Lean.Meta.Grind` without it thanks to these changes. We did previously not conduct this change as `Std.TreeMap` was not outperforming `Lean.RBMap` yet, however this has changed with the new code generator. --- src/Lean/Attributes.lean | 6 +- src/Lean/Compiler/IR/Basic.lean | 28 +- src/Lean/Compiler/IR/LiveVars.lean | 8 +- src/Lean/Compiler/IR/NormIds.lean | 2 +- src/Lean/Compiler/IR/RC.lean | 12 +- src/Lean/Compiler/LCNF/AlphaEqv.lean | 2 +- src/Lean/Compiler/LCNF/FixedParams.lean | 4 +- src/Lean/Compiler/LCNF/JoinPoints.lean | 8 +- src/Lean/Compiler/LCNF/ReduceJpArity.lean | 2 +- src/Lean/Compiler/LCNF/Renaming.lean | 6 +- src/Lean/Compiler/LCNF/Simp/DiscrM.lean | 2 +- src/Lean/Compiler/LCNF/Simp/JpCases.lean | 8 +- src/Lean/Compiler/LCNF/ToExpr.lean | 2 +- src/Lean/Compiler/LCNF/ToLCNF.lean | 6 +- src/Lean/Data/Json/Basic.lean | 35 +-- src/Lean/Data/Json/FromToJson.lean | 266 +----------------- src/Lean/Data/Json/FromToJson/Basic.lean | 258 +++++++++++++++++ src/Lean/Data/Json/FromToJson/Extra.lean | 35 +++ src/Lean/Data/Json/Parser.lean | 12 +- src/Lean/Data/Json/Printer.lean | 4 +- src/Lean/Data/Json/Stream.lean | 1 - src/Lean/Data/JsonRpc.lean | 4 +- src/Lean/Data/KVMap.lean | 4 +- src/Lean/Data/Lsp/Basic.lean | 34 +-- src/Lean/Data/Lsp/BasicAux.lean | 48 ++++ src/Lean/Data/Lsp/Client.lean | 1 - src/Lean/Data/Lsp/CodeActions.lean | 1 - src/Lean/Data/Lsp/Diagnostics.lean | 1 - src/Lean/Data/Lsp/InitShutdown.lean | 1 - src/Lean/Data/Lsp/Internal.lean | 3 +- src/Lean/Data/Lsp/Ipc.lean | 2 +- src/Lean/Data/Lsp/LanguageFeatures.lean | 2 +- src/Lean/Data/Lsp/TextSync.lean | 2 +- src/Lean/Data/Lsp/Utf16.lean | 2 +- src/Lean/Data/Lsp/Window.lean | 2 +- src/Lean/Data/Lsp/Workspace.lean | 2 +- src/Lean/Data/NameMap.lean | 103 +------ .../Data/NameMap/AdditionalOperations.lean | 20 ++ src/Lean/Data/NameMap/Basic.lean | 105 +++++++ src/Lean/Data/Options.lean | 4 +- src/Lean/Data/Position.lean | 2 +- src/Lean/Data/PrefixTree.lean | 50 ++-- src/Lean/Data/Trie.lean | 2 +- src/Lean/Data/Xml/Basic.lean | 6 +- src/Lean/Data/Xml/Parser.lean | 2 +- src/Lean/Elab/App.lean | 2 +- src/Lean/Elab/DeclNameGen.lean | 2 +- src/Lean/Elab/Deriving/FromToJson.lean | 2 +- src/Lean/Elab/Deriving/Inhabited.lean | 4 +- src/Lean/Elab/Do.lean | 8 +- src/Lean/Elab/InfoTree/Types.lean | 2 +- src/Lean/Elab/MutualDef.lean | 24 +- src/Lean/Elab/PatternVar.lean | 2 +- src/Lean/Elab/Print.lean | 2 +- src/Lean/Elab/StructInst.lean | 8 +- src/Lean/Elab/Structure.lean | 4 +- .../Tactic/BVDecide/Frontend/BVDecide.lean | 2 +- src/Lean/Elab/Tactic/Doc.lean | 8 +- src/Lean/Elab/Term.lean | 4 +- src/Lean/Expr.lean | 45 +-- src/Lean/Level.lean | 11 +- src/Lean/Linter/Basic.lean | 6 +- src/Lean/Log.lean | 9 +- src/Lean/Message.lean | 2 +- src/Lean/Meta/Instances.lean | 2 +- src/Lean/Meta/Match/MVarRenaming.lean | 4 +- src/Lean/Meta/Match/MatchEqs.lean | 6 +- .../Tactic/Grind/Arith/CommRing/Types.lean | 3 +- .../Tactic/Grind/Arith/CommRing/Util.lean | 2 +- .../Tactic/Grind/Arith/Cutsat/Search.lean | 2 +- .../Meta/Tactic/Grind/Arith/Cutsat/Types.lean | 2 +- .../Meta/Tactic/Grind/Arith/Linear/Types.lean | 2 +- src/Lean/Meta/Tactic/Grind/Cases.lean | 2 +- src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean | 6 +- src/Lean/Meta/Tactic/Grind/Proof.lean | 4 +- src/Lean/Meta/Tactic/Grind/Types.lean | 2 +- src/Lean/Meta/Tactic/Simp/Types.lean | 2 +- src/Lean/MetavarContext.lean | 2 +- src/Lean/Parser/Basic.lean | 22 +- src/Lean/Parser/Extension.lean | 2 +- src/Lean/Parser/Tactic/Doc.lean | 12 +- src/Lean/Parser/Term/Doc.lean | 4 +- src/Lean/PrettyPrinter/Delaborator/Basic.lean | 4 +- .../PrettyPrinter/Delaborator/Builtins.lean | 4 +- .../PrettyPrinter/Delaborator/SubExpr.lean | 7 +- .../Delaborator/TopDownAnalyze.lean | 3 +- src/Lean/ReducibilityAttrs.lean | 2 +- src/Lean/ResolveName.lean | 2 +- src/Lean/Server/CodeActions/Attr.lean | 2 +- .../Completion/CompletionCollectors.lean | 8 +- src/Lean/Server/FileWorker.lean | 29 +- .../FileWorker/SemanticHighlighting.lean | 6 +- src/Lean/Server/GoTo.lean | 2 +- src/Lean/Server/References.lean | 1 - src/Lean/Server/Requests.lean | 4 +- src/Lean/Server/Rpc/Basic.lean | 2 +- src/Lean/Server/Rpc/RequestHandling.lean | 2 +- src/Lean/Server/Watchdog.lean | 31 +- src/Lean/Setup.lean | 3 +- src/Lean/SubExpr.lean | 5 +- src/Lean/Util/LeanOptions.lean | 7 +- src/Lean/Util/PPExt.lean | 2 +- src/Lean/Widget/Diff.lean | 14 +- src/Lean/Widget/InteractiveCode.lean | 4 +- src/Lean/Widget/InteractiveDiagnostic.lean | 2 +- src/Lean/Widget/TaggedText.lean | 2 +- src/Lean/Widget/UserWidget.lean | 20 +- src/lake/Lake/Build/Common.lean | 4 +- src/lake/Lake/Build/InitFacets.lean | 2 +- src/lake/Lake/Build/Key.lean | 16 +- src/lake/Lake/Build/Module.lean | 6 +- src/lake/Lake/Build/Store.lean | 4 +- src/lake/Lake/CLI/Translate/Lean.lean | 2 +- src/lake/Lake/CLI/Translate/Toml.lean | 2 +- src/lake/Lake/Config/Dependency.lean | 2 +- src/lake/Lake/Config/Module.lean | 4 +- src/lake/Lake/Config/Package.lean | 6 +- src/lake/Lake/Config/TargetConfig.lean | 2 +- src/lake/Lake/Config/Workspace.lean | 4 +- src/lake/Lake/DSL/DeclUtil.lean | 2 +- src/lake/Lake/Load/Lean/Eval.lean | 15 +- src/lake/Lake/Load/Toml.lean | 2 +- src/lake/Lake/Toml/Data/Dict.lean | 10 +- src/lake/Lake/Toml/Elab/Expression.lean | 2 +- src/lake/Lake/Util/Compare.lean | 74 ----- src/lake/Lake/Util/DRBMap.lean | 152 ---------- src/lake/Lake/Util/Family.lean | 10 +- src/lake/Lake/Util/JsonObject.lean | 10 +- src/lake/Lake/Util/Name.lean | 32 +-- src/lake/Lake/Util/RBArray.lean | 17 +- src/lake/Lake/Util/StoreInsts.lean | 18 +- stage0/src/stdlib_flags.h | 2 +- tests/lean/PPRoundtrip.lean | 2 +- tests/lean/run/inductiveIndicesIssue.lean | 8 +- 134 files changed, 883 insertions(+), 1033 deletions(-) create mode 100644 src/Lean/Data/Json/FromToJson/Basic.lean create mode 100644 src/Lean/Data/Json/FromToJson/Extra.lean create mode 100644 src/Lean/Data/Lsp/BasicAux.lean create mode 100644 src/Lean/Data/NameMap/AdditionalOperations.lean create mode 100644 src/Lean/Data/NameMap/Basic.lean delete mode 100644 src/lake/Lake/Util/Compare.lean delete mode 100644 src/lake/Lake/Util/DRBMap.lean diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index e5eea058e2..c1fcea2664 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -144,7 +144,7 @@ def registerTagAttribute (name : Name) (descr : String) addImportedFn := fun _ _ => pure {} addEntryFn := fun (s : NameSet) n => s.insert n exportEntriesFn := fun es => - let r : Array Name := es.fold (fun a e => a.push e) #[] + let r : Array Name := es.foldl (fun a e => a.push e) #[] r.qsort Name.quickLt statsFn := fun s => "tag attribute" ++ Format.line ++ "number of local entries: " ++ format s.size asyncMode := asyncMode @@ -219,7 +219,7 @@ def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (Parame addImportedFn := fun s => impl.afterImport s *> pure {} addEntryFn := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2 exportEntriesFn := fun m => - let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) #[] + let r : Array (Name × α) := m.foldl (fun a n p => a.push (n, p)) #[] r.qsort (fun a b => Name.quickLt a.1 b.1) statsFn := fun s => "parametric attribute" ++ Format.line ++ "number of local entries: " ++ format s.size } @@ -276,7 +276,7 @@ def registerEnumAttributes (attrDescrs : List (Name × String × α)) addImportedFn := fun _ _ => pure {} addEntryFn := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2 exportEntriesFn := fun m => - let r : Array (Name × α) := m.fold (fun a n p => a.push (n, p)) #[] + let r : Array (Name × α) := m.foldl (fun a n p => a.push (n, p)) #[] r.qsort (fun a b => Name.quickLt a.1 b.1) statsFn := fun s => "enumeration attribute extension" ++ Format.line ++ "number of local entries: " ++ format s.size -- We assume (and check below) that, if used asynchronously, enum attributes are set only in the diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean index 85d8ef0305..a6d060ab39 100644 --- a/src/Lean/Compiler/IR/Basic.lean +++ b/src/Lean/Compiler/IR/Basic.lean @@ -383,17 +383,17 @@ def mkDummyExternDecl (f : FunId) (xs : Array Param) (ty : IRType) : Decl := Decl.fdecl f xs ty FnBody.unreachable {} /-- Set of variable and join point names -/ -abbrev IndexSet := RBTree Index compare +abbrev IndexSet := Std.TreeSet Index def mkIndexSet (idx : Index) : IndexSet := - RBTree.empty.insert idx + Std.TreeSet.empty.insert idx inductive LocalContextEntry where | param : IRType → LocalContextEntry | localVar : IRType → Expr → LocalContextEntry | joinPoint : Array Param → FnBody → LocalContextEntry -abbrev LocalContext := RBMap Index LocalContextEntry compare +abbrev LocalContext := Std.TreeMap Index LocalContextEntry def LocalContext.addLocal (ctx : LocalContext) (x : VarId) (t : IRType) (v : Expr) : LocalContext := ctx.insert x.idx (LocalContextEntry.localVar t v) @@ -408,48 +408,48 @@ def LocalContext.addParams (ctx : LocalContext) (ps : Array Param) : LocalContex ps.foldl LocalContext.addParam ctx def LocalContext.isJP (ctx : LocalContext) (idx : Index) : Bool := - match ctx.find? idx with + match ctx.get? idx with | some (LocalContextEntry.joinPoint _ _) => true | _ => false def LocalContext.getJPBody (ctx : LocalContext) (j : JoinPointId) : Option FnBody := - match ctx.find? j.idx with + match ctx.get? j.idx with | some (LocalContextEntry.joinPoint _ b) => some b | _ => none def LocalContext.getJPParams (ctx : LocalContext) (j : JoinPointId) : Option (Array Param) := - match ctx.find? j.idx with + match ctx.get? j.idx with | some (LocalContextEntry.joinPoint ys _) => some ys | _ => none def LocalContext.isParam (ctx : LocalContext) (idx : Index) : Bool := - match ctx.find? idx with + match ctx.get? idx with | some (LocalContextEntry.param _) => true | _ => false def LocalContext.isLocalVar (ctx : LocalContext) (idx : Index) : Bool := - match ctx.find? idx with + match ctx.get? idx with | some (LocalContextEntry.localVar _ _) => true | _ => false def LocalContext.contains (ctx : LocalContext) (idx : Index) : Bool := - RBMap.contains ctx idx + Std.TreeMap.contains ctx idx def LocalContext.eraseJoinPointDecl (ctx : LocalContext) (j : JoinPointId) : LocalContext := ctx.erase j.idx def LocalContext.getType (ctx : LocalContext) (x : VarId) : Option IRType := - match ctx.find? x.idx with + match ctx.get? x.idx with | some (LocalContextEntry.param t) => some t | some (LocalContextEntry.localVar t _) => some t | _ => none def LocalContext.getValue (ctx : LocalContext) (x : VarId) : Option Expr := - match ctx.find? x.idx with + match ctx.get? x.idx with | some (LocalContextEntry.localVar _ v) => some v | _ => none -abbrev IndexRenaming := RBMap Index Index compare +abbrev IndexRenaming := Std.TreeMap Index Index class AlphaEqv (α : Type) where aeqv : IndexRenaming → α → α → Bool @@ -457,7 +457,7 @@ class AlphaEqv (α : Type) where export AlphaEqv (aeqv) def VarId.alphaEqv (ρ : IndexRenaming) (v₁ v₂ : VarId) : Bool := - match ρ.find? v₁.idx with + match ρ.get? v₁.idx with | some v => v == v₂.idx | none => v₁ == v₂ @@ -540,7 +540,7 @@ def FnBody.beq (b₁ b₂ : FnBody) : Bool := instance : BEq FnBody := ⟨FnBody.beq⟩ -abbrev VarIdSet := RBTree VarId (fun x y => compare x.idx y.idx) +abbrev VarIdSet := Std.TreeSet VarId (fun x y => compare x.idx y.idx) def mkIf (x : VarId) (t e : FnBody) : FnBody := FnBody.case `Bool x IRType.uint8 #[ diff --git a/src/Lean/Compiler/IR/LiveVars.lean b/src/Lean/Compiler/IR/LiveVars.lean index 0f4019e4a2..ba8ad6e934 100644 --- a/src/Lean/Compiler/IR/LiveVars.lean +++ b/src/Lean/Compiler/IR/LiveVars.lean @@ -80,10 +80,10 @@ def FnBody.hasLiveVar (b : FnBody) (ctx : LocalContext) (x : VarId) : Bool := (IsLive.visitFnBody x.idx b).run' ctx abbrev LiveVarSet := VarIdSet -abbrev JPLiveVarMap := RBMap JoinPointId LiveVarSet (fun j₁ j₂ => compare j₁.idx j₂.idx) +abbrev JPLiveVarMap := Std.TreeMap JoinPointId LiveVarSet (fun j₁ j₂ => compare j₁.idx j₂.idx) def mkLiveVarSet (x : VarId) : LiveVarSet := - RBTree.empty.insert x + Std.TreeSet.empty.insert x namespace LiveVars @@ -103,10 +103,10 @@ private def collectArgs (as : Array Arg) : Collector := collectArray as collectArg private def accumulate (s' : LiveVarSet) : Collector := - fun s => s'.fold (fun s x => s.insert x) s + fun s => s'.foldl (fun s x => s.insert x) s private def collectJP (m : JPLiveVarMap) (j : JoinPointId) : Collector := - match m.find? j with + match m.get? j with | some xs => accumulate xs | none => skip -- unreachable for well-formed code diff --git a/src/Lean/Compiler/IR/NormIds.lean b/src/Lean/Compiler/IR/NormIds.lean index c8da2e4c1d..4d80c412dc 100644 --- a/src/Lean/Compiler/IR/NormIds.lean +++ b/src/Lean/Compiler/IR/NormIds.lean @@ -39,7 +39,7 @@ namespace NormalizeIds abbrev M := ReaderT IndexRenaming Id def normIndex (x : Index) : M Index := fun m => - match m.find? x with + match m.get? x with | some y => y | none => x diff --git a/src/Lean/Compiler/IR/RC.lean b/src/Lean/Compiler/IR/RC.lean index 393a20ed4e..b124d03219 100644 --- a/src/Lean/Compiler/IR/RC.lean +++ b/src/Lean/Compiler/IR/RC.lean @@ -21,7 +21,7 @@ structure VarInfo where consume : Bool -- true if the variable RC must be "consumed" deriving Inhabited -abbrev VarMap := RBMap VarId VarInfo (fun x y => compare x.idx y.idx) +abbrev VarMap := Std.TreeMap VarId VarInfo (fun x y => compare x.idx y.idx) structure Context where env : Environment @@ -36,7 +36,7 @@ def getDecl (ctx : Context) (fid : FunId) : Decl := | none => unreachable! def getVarInfo (ctx : Context) (x : VarId) : VarInfo := - match ctx.varMap.find? x with + match ctx.varMap.get? x with | some info => info | none => unreachable! @@ -46,7 +46,7 @@ def getJPParams (ctx : Context) (j : JoinPointId) : Array Param := | none => unreachable! def getJPLiveVars (ctx : Context) (j : JoinPointId) : LiveVarSet := - match ctx.jpLiveVarMap.find? j with + match ctx.jpLiveVarMap.get? j with | some s => s | none => {} @@ -68,12 +68,12 @@ private def updateRefUsingCtorInfo (ctx : Context) (x : VarId) (c : CtorInfo) : else let m := ctx.varMap { ctx with - varMap := match m.find? x with + varMap := match m.get? x with | some info => m.insert x { info with type := c.type } | none => m } private def addDecForAlt (ctx : Context) (caseLiveVars altLiveVars : LiveVarSet) (b : FnBody) : FnBody := - caseLiveVars.fold (init := b) fun b x => + caseLiveVars.foldl (init := b) fun b x => if !altLiveVars.contains x && mustConsume ctx x then addDec ctx x b else b /-- `isFirstOcc xs x i = true` if `xs[i]` is the first occurrence of `xs[i]` in `xs` -/ @@ -155,7 +155,7 @@ private def isPersistent : Expr → Bool /-- We do not need to consume the projection of a variable that is not consumed -/ private def consumeExpr (m : VarMap) : Expr → Bool - | Expr.proj _ x => match m.find? x with + | Expr.proj _ x => match m.get? x with | some info => info.consume | none => true | _ => true diff --git a/src/Lean/Compiler/LCNF/AlphaEqv.lean b/src/Lean/Compiler/LCNF/AlphaEqv.lean index c8d8a7c9e2..7b964d6d06 100644 --- a/src/Lean/Compiler/LCNF/AlphaEqv.lean +++ b/src/Lean/Compiler/LCNF/AlphaEqv.lean @@ -17,7 +17,7 @@ namespace AlphaEqv abbrev EqvM := ReaderM (FVarIdMap FVarId) def eqvFVar (fvarId₁ fvarId₂ : FVarId) : EqvM Bool := do - let fvarId₂ := (← read).find? fvarId₂ |>.getD fvarId₂ + let fvarId₂ := (← read).get? fvarId₂ |>.getD fvarId₂ return fvarId₁ == fvarId₂ def eqvType (e₁ e₂ : Expr) : EqvM Bool := do diff --git a/src/Lean/Compiler/LCNF/FixedParams.lean b/src/Lean/Compiler/LCNF/FixedParams.lean index 62df67d888..7e1cb87ba1 100644 --- a/src/Lean/Compiler/LCNF/FixedParams.lean +++ b/src/Lean/Compiler/LCNF/FixedParams.lean @@ -78,7 +78,7 @@ abbrev abort : FixParamM α := do throw () def evalFVar (fvarId : FVarId) : FixParamM AbsValue := do - let some val := (← read).assignment.find? fvarId | return .top + let some val := (← read).assignment.get? fvarId | return .top return val def evalArg (arg : Arg) : FixParamM AbsValue := do @@ -109,7 +109,7 @@ partial def isEquivalentFunDecl? (decl : FunDecl) : FixParamM (Option Nat) := do if args.size != decl.params.size then return none let .return retFVarId := k | return none if retFVarId != fvarId then return none - let some (.val funIdx) := (← read).assignment.find? funFvarId | return none + let some (.val funIdx) := (← read).assignment.get? funFvarId | return none for h : i in [:decl.params.size] do let param := decl.params[i] -- TODO: Eliminate this dynamic bounds check. diff --git a/src/Lean/Compiler/LCNF/JoinPoints.lean b/src/Lean/Compiler/LCNF/JoinPoints.lean index 8ecd79f24e..6e70bdcd97 100644 --- a/src/Lean/Compiler/LCNF/JoinPoints.lean +++ b/src/Lean/Compiler/LCNF/JoinPoints.lean @@ -467,7 +467,7 @@ abbrev ReduceAnalysisM := ReaderT AnalysisCtx StateRefT AnalysisState ScopeM abbrev ReduceActionM := ReaderT AnalysisState CompilerM def isInJpScope (jp : FVarId) (var : FVarId) : ReduceAnalysisM Bool := do - return (← read).jpScopes.find! jp |>.contains var + return (← read).jpScopes.get! jp |>.contains var open ScopeM @@ -542,7 +542,7 @@ where cs.alts.forM visitor | .jmp fn args => let decl ← getFunDecl fn - if let some knownArgs := (← get).jpJmpArgs.find? fn then + if let some knownArgs := (← get).jpJmpArgs.get? fn then let mut newArgs := knownArgs for (param, arg) in decl.params.zip args do if let some knownVal := newArgs[param.fvarId]? then @@ -562,7 +562,7 @@ where goReduce (code : Code) : ReduceActionM Code := do match code with | .jp decl k => - if let some reducibleArgs := (← read).jpJmpArgs.find? decl.fvarId then + if let some reducibleArgs := (← read).jpJmpArgs.get? decl.fvarId then let filter param := do let erasable := reducibleArgs.contains param.fvarId if erasable then @@ -582,7 +582,7 @@ where else return Code.updateFun! code decl (← goReduce k) | .jmp fn args => - let reducibleArgs := (← read).jpJmpArgs.find! fn + let reducibleArgs := (← read).jpJmpArgs.get! fn let decl ← getFunDecl fn let newParams := decl.params.zip args |>.filter (!reducibleArgs.contains ·.fst.fvarId) diff --git a/src/Lean/Compiler/LCNF/ReduceJpArity.lean b/src/Lean/Compiler/LCNF/ReduceJpArity.lean index e2fb96fab0..02802fd60b 100644 --- a/src/Lean/Compiler/LCNF/ReduceJpArity.lean +++ b/src/Lean/Compiler/LCNF/ReduceJpArity.lean @@ -51,7 +51,7 @@ partial def reduce (code : Code) : ReduceM Code := do return code.updateAlts! alts | .return .. | .unreach .. => return code | .jmp fvarId args => - if let some mask := (← read).find? fvarId then + if let some mask := (← read).get? fvarId then let mut argsNew := #[] for keep in mask, arg in args do if keep then diff --git a/src/Lean/Compiler/LCNF/Renaming.lean b/src/Lean/Compiler/LCNF/Renaming.lean index d97179648d..12c207bf1a 100644 --- a/src/Lean/Compiler/LCNF/Renaming.lean +++ b/src/Lean/Compiler/LCNF/Renaming.lean @@ -13,7 +13,7 @@ A mapping from free variable id to binder name. abbrev Renaming := FVarIdMap Name def Param.applyRenaming (param : Param) (r : Renaming) : CompilerM Param := do - if let some binderName := r.find? param.fvarId then + if let some binderName := r.get? param.fvarId then let param := { param with binderName } modifyLCtx fun lctx => lctx.addParam param return param @@ -21,7 +21,7 @@ def Param.applyRenaming (param : Param) (r : Renaming) : CompilerM Param := do return param def LetDecl.applyRenaming (decl : LetDecl) (r : Renaming) : CompilerM LetDecl := do - if let some binderName := r.find? decl.fvarId then + if let some binderName := r.get? decl.fvarId then let decl := { decl with binderName } modifyLCtx fun lctx => lctx.addLetDecl decl return decl @@ -30,7 +30,7 @@ def LetDecl.applyRenaming (decl : LetDecl) (r : Renaming) : CompilerM LetDecl := mutual partial def FunDecl.applyRenaming (decl : FunDecl) (r : Renaming) : CompilerM FunDecl := do - if let some binderName := r.find? decl.fvarId then + if let some binderName := r.get? decl.fvarId then let decl := { decl with binderName } modifyLCtx fun lctx => lctx.addFunDecl decl decl.updateValue (← decl.value.applyRenaming r) diff --git a/src/Lean/Compiler/LCNF/Simp/DiscrM.lean b/src/Lean/Compiler/LCNF/Simp/DiscrM.lean index 66eab280f7..588689cca5 100644 --- a/src/Lean/Compiler/LCNF/Simp/DiscrM.lean +++ b/src/Lean/Compiler/LCNF/Simp/DiscrM.lean @@ -60,7 +60,7 @@ def findCtor? (fvarId : FVarId) : DiscrM (Option CtorInfo) := do let some (.ctorInfo val) := (← getEnv).find? declName | return none return some <| .ctor val args | some _ => return none - | none => return (← read).discrCtorMap.find? fvarId + | none => return (← read).discrCtorMap.get? fvarId def findCtorName? (fvarId : FVarId) : DiscrM (Option Name) := do let some ctorInfo ← findCtor? fvarId | return none diff --git a/src/Lean/Compiler/LCNF/Simp/JpCases.lean b/src/Lean/Compiler/LCNF/Simp/JpCases.lean index 2a19e97bcb..86e0f5429d 100644 --- a/src/Lean/Compiler/LCNF/Simp/JpCases.lean +++ b/src/Lean/Compiler/LCNF/Simp/JpCases.lean @@ -80,7 +80,7 @@ where | .alt ctorName ps k => withDiscrCtor c.discr ctorName ps <| go k | .return .. | .unreach .. => return () | .jmp fvarId args => - if let some info := (← get).find? fvarId then + if let some info := (← get).get? fvarId then let .fvar argFVarId := args[info.paramIdx]! | return () let some ctorName ← findCtorName? argFVarId | return () modify fun map => map.insert fvarId <| { info with ctorNames := info.ctorNames.insert ctorName } @@ -231,7 +231,7 @@ where return code visitJp? (decl : FunDecl) (k : Code) : ReaderT JpCasesInfoMap (StateRefT Ctor2JpCasesAlt DiscrM) (Option Code) := do - let some info := (← read).find? decl.fvarId | return none + let some info := (← read).get? decl.fvarId | return none if info.ctorNames.isEmpty then return none -- This join point satisfies `isJpCases?` and there are jumps with constructors in `info` to it. let (decls, cases) := extractJpCases decl.value @@ -272,8 +272,8 @@ where return LCNF.attachCodeDecls jpAltDecls code visitJmp? (fvarId : FVarId) (args : Array Arg) : ReaderT JpCasesInfoMap (StateRefT Ctor2JpCasesAlt DiscrM) (Option Code) := do - let some ctorJpAltMap := (← get).find? fvarId | return none - let some info := (← read).find? fvarId | return none + let some ctorJpAltMap := (← get).get? fvarId | return none + let some info := (← read).get? fvarId | return none let .fvar argFVarId := args[info.paramIdx]! | return none let some ctorInfo ← findCtor? argFVarId | return none let some jpAlt := ctorJpAltMap.find? ctorInfo.getName | return none diff --git a/src/Lean/Compiler/LCNF/ToExpr.lean b/src/Lean/Compiler/LCNF/ToExpr.lean index d45cefd7fb..d307d94820 100644 --- a/src/Lean/Compiler/LCNF/ToExpr.lean +++ b/src/Lean/Compiler/LCNF/ToExpr.lean @@ -13,7 +13,7 @@ namespace ToExpr private abbrev LevelMap := FVarIdMap Nat private def _root_.Lean.FVarId.toExpr (offset : Nat) (m : LevelMap) (fvarId : FVarId) : Expr := - match m.find? fvarId with + match m.get? fvarId with | some level => .bvar (offset - level - 1) | none => .fvar fvarId diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean index 4d1b114a46..4ce016bd94 100644 --- a/src/Lean/Compiler/LCNF/ToLCNF.lean +++ b/src/Lean/Compiler/LCNF/ToLCNF.lean @@ -66,7 +66,7 @@ partial def bindCases (jpDecl : FunDecl) (cases : Cases) : CompilerM Code := do let (alts, s) ← visitAlts cases.alts |>.run {} let resultType ← mkCasesResultType alts let result := .cases { cases with alts, resultType } - let result := s.fold (init := result) fun result _ altJp => .jp altJp result + let result := s.foldl (init := result) fun result _ altJp => .jp altJp result return .jp jpDecl result where visitAlts (alts : Array Alt) : BindCasesM (Array Alt) := @@ -99,7 +99,7 @@ where if binderName.getPrefix == `_alt then if let some funDecl ← findFun? f then eraseLetDecl decl - if let some altJp := (← get).find? f then + if let some altJp := (← get).get? f then /- We already have an auxiliary join point for `f`, then, we just use it. -/ return .jmp altJp.fvarId args else @@ -130,7 +130,7 @@ where return .jmp altJp.fvarId args | _ => pure () let k ← go k - if let some altJp := (← get).find? decl.fvarId then + if let some altJp := (← get).get? decl.fvarId then -- The new join point depends on this variable. Thus, we must insert it here modify fun s => s.erase decl.fvarId return .let decl (.jp altJp k) diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean index 47e5966d4d..f4c650fed9 100644 --- a/src/Lean/Data/Json/Basic.lean +++ b/src/Lean/Data/Json/Basic.lean @@ -8,8 +8,8 @@ prelude import Init.Data.Range import Init.Data.OfScientific import Init.Data.Hashable -import Lean.Data.RBMap import Init.Data.ToString.Macro +import Std.Data.TreeMap.Raw.Basic namespace Lean @@ -175,10 +175,7 @@ inductive Json where | num (n : JsonNumber) | str (s : String) | arr (elems : Array Json) - -- uses RBNode instead of RBMap because RBMap is a def - -- and thus currently cannot be used to define a type that - -- is recursive in one of its parameters - | obj (kvPairs : RBNode String (fun _ => Json)) + | obj (kvPairs : Std.TreeMap.Raw String Json) deriving Inhabited namespace Json @@ -193,10 +190,10 @@ private partial def beq' : Json → Json → Bool a == b | obj a, obj b => let _ : BEq Json := ⟨beq'⟩ - let szA := a.fold (init := 0) (fun a _ _ => a + 1) - let szB := b.fold (init := 0) (fun a _ _ => a + 1) + let szA := a.foldl (init := 0) (fun a _ _ => a + 1) + let szB := b.foldl (init := 0) (fun a _ _ => a + 1) szA == szB && a.all fun field fa => - match b.find compare field with + match b.get? field with | none => false | some fb => fa == fb | _, _ => false @@ -212,18 +209,13 @@ private partial def hash' : Json → UInt64 | arr elems => mixHash 23 <| elems.foldl (init := 7) fun r a => mixHash r (hash' a) | obj kvPairs => - mixHash 29 <| kvPairs.fold (init := 7) fun r k v => mixHash r <| mixHash (hash k) (hash' v) + mixHash 29 <| kvPairs.foldl (init := 7) fun r k v => mixHash r <| mixHash (hash k) (hash' v) instance : Hashable Json where hash := hash' --- HACK(Marc): temporary ugliness until we can use RBMap for JSON objects def mkObj (o : List (String × Json)) : Json := - obj <| Id.run do - let mut kvPairs := RBNode.leaf - for ⟨k, v⟩ in o do - kvPairs := kvPairs.insert compare k v - kvPairs + obj <| Std.TreeMap.Raw.ofList o instance : Coe Nat Json := ⟨fun n => Json.num n⟩ instance : Coe Int Json := ⟨fun n => Json.num n⟩ @@ -235,7 +227,7 @@ def isNull : Json -> Bool | null => true | _ => false -def getObj? : Json → Except String (RBNode String (fun _ => Json)) +def getObj? : Json → Except String (Std.TreeMap.Raw String Json compare) | obj kvs => return kvs | _ => throw "object expected" @@ -265,7 +257,7 @@ def getNum? : Json → Except String JsonNumber def getObjVal? : Json → String → Except String Json | obj kvs, k => - match kvs.find compare k with + match kvs.get? k with | some v => return v | none => throw s!"property not found: {k}" | _ , _ => throw "object expected" @@ -281,24 +273,23 @@ def getObjValD (j : Json) (k : String) : Json := (j.getObjVal? k).toOption.getD null def setObjVal! : Json → String → Json → Json - | obj kvs, k, v => obj <| kvs.insert compare k v + | obj kvs, k, v => obj <| kvs.insert k v | _ , _, _ => panic! "Json.setObjVal!: not an object: {j}" -open Lean.RBNode in /-- Assuming both inputs `o₁, o₂` are json objects, will compute `{...o₁, ...o₂}`. If `o₁` is not a json object, `o₂` will be returned. -/ def mergeObj : Json → Json → Json | obj kvs₁, obj kvs₂ => - obj <| fold (insert compare) kvs₁ kvs₂ + obj <| kvs₂.foldl Std.TreeMap.Raw.insert kvs₁ | _, j₂ => j₂ inductive Structured where | arr (elems : Array Json) - | obj (kvPairs : RBNode String (fun _ => Json)) + | obj (kvPairs : Std.TreeMap.Raw String Json compare) instance : Coe (Array Json) Structured := ⟨Structured.arr⟩ -instance : Coe (RBNode String (fun _ => Json)) Structured := ⟨Structured.obj⟩ +instance : Coe (Std.TreeMap.Raw String Json) Structured := ⟨Structured.obj⟩ end Json end Lean diff --git a/src/Lean/Data/Json/FromToJson.lean b/src/Lean/Data/Json/FromToJson.lean index f1224cc51b..2f8b20d707 100644 --- a/src/Lean/Data/Json/FromToJson.lean +++ b/src/Lean/Data/Json/FromToJson.lean @@ -5,267 +5,5 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner, Marc Huisinga -/ prelude -import Lean.Data.Json.Basic -import Lean.Data.Json.Printer - -namespace Lean - -universe u - -class FromJson (α : Type u) where - fromJson? : Json → Except String α - -export FromJson (fromJson?) - -class ToJson (α : Type u) where - toJson : α → Json - -export ToJson (toJson) - -instance : FromJson Json := ⟨Except.ok⟩ -instance : ToJson Json := ⟨id⟩ - -instance : FromJson JsonNumber := ⟨Json.getNum?⟩ -instance : ToJson JsonNumber := ⟨Json.num⟩ - -instance : FromJson Empty where - fromJson? j := throw (s!"type Empty has no constructor to match JSON value '{j}'. \ - This occurs when deserializing a value for type Empty, \ - e.g. at type Option Empty with code for the 'some' constructor.") - -instance : ToJson Empty := ⟨nofun⟩ --- looks like id, but there are coercions happening -instance : FromJson Bool := ⟨Json.getBool?⟩ -instance : ToJson Bool := ⟨fun b => b⟩ -instance : FromJson Nat := ⟨Json.getNat?⟩ -instance : ToJson Nat := ⟨fun n => n⟩ -instance : FromJson Int := ⟨Json.getInt?⟩ -instance : ToJson Int := ⟨fun n => Json.num n⟩ -instance : FromJson String := ⟨Json.getStr?⟩ -instance : ToJson String := ⟨fun s => s⟩ - -instance : FromJson System.FilePath := ⟨fun j => System.FilePath.mk <$> Json.getStr? j⟩ -instance : ToJson System.FilePath := ⟨fun p => p.toString⟩ - -protected def _root_.Array.fromJson? [FromJson α] : Json → Except String (Array α) - | Json.arr a => a.mapM fromJson? - | j => throw s!"expected JSON array, got '{j}'" - -instance [FromJson α] : FromJson (Array α) where - fromJson? := Array.fromJson? - -protected def _root_.Array.toJson [ToJson α] (a : Array α) : Json := - Json.arr (a.map toJson) - -instance [ToJson α] : ToJson (Array α) where - toJson := Array.toJson - -protected def _root_.List.fromJson? [FromJson α] (j : Json) : Except String (List α) := - (fromJson? j (α := Array α)).map Array.toList - -instance [FromJson α] : FromJson (List α) where - fromJson? := List.fromJson? - -protected def _root_.List.toJson [ToJson α] (a : List α) : Json := - toJson a.toArray - -instance [ToJson α] : ToJson (List α) where - toJson := List.toJson - -protected def _root_.Option.fromJson? [FromJson α] : Json → Except String (Option α) - | Json.null => Except.ok none - | j => some <$> fromJson? j - -instance [FromJson α] : FromJson (Option α) where - fromJson? := Option.fromJson? - -protected def _root_.Option.toJson [ToJson α] : Option α → Json - | none => Json.null - | some a => toJson a - -instance [ToJson α] : ToJson (Option α) where - toJson := Option.toJson - -protected def _root_.Prod.fromJson? {α : Type u} {β : Type v} [FromJson α] [FromJson β] : Json → Except String (α × β) - | Json.arr #[ja, jb] => do - let ⟨a⟩ : ULift.{v} α := ← (fromJson? ja).map ULift.up - let ⟨b⟩ : ULift.{u} β := ← (fromJson? jb).map ULift.up - return (a, b) - | j => throw s!"expected pair, got '{j}'" - -instance {α : Type u} {β : Type v} [FromJson α] [FromJson β] : FromJson (α × β) where - fromJson? := Prod.fromJson? - -protected def _root_.Prod.toJson [ToJson α] [ToJson β] : α × β → Json - | (a, b) => Json.arr #[toJson a, toJson b] - -instance [ToJson α] [ToJson β] : ToJson (α × β) where - toJson := Prod.toJson - -protected def Name.fromJson? (j : Json) : Except String Name := do - let s ← j.getStr? - if s == "[anonymous]" then - return Name.anonymous - else - let n := s.toName - if n.isAnonymous then throw s!"expected a `Name`, got '{j}'" - return n - -instance : FromJson Name where - fromJson? := Name.fromJson? - -instance : ToJson Name where - toJson n := toString n - -protected def NameMap.fromJson? [FromJson α] : Json → Except String (NameMap α) - | .obj obj => obj.foldM (init := {}) fun m k v => do - if k == "[anonymous]" then - return m.insert .anonymous (← fromJson? v) - else - let n := k.toName - if n.isAnonymous then - throw s!"expected a `Name`, got '{k}'" - else - return m.insert n (← fromJson? v) - | j => throw s!"expected a `NameMap`, got '{j}'" - -instance [FromJson α] : FromJson (NameMap α) where - fromJson? := NameMap.fromJson? - -protected def NameMap.toJson [ToJson α] (m : NameMap α) : Json := - Json.obj <| m.fold (fun n k v => n.insert compare k.toString (toJson v)) .leaf - -instance [ToJson α] : ToJson (NameMap α) where - toJson := NameMap.toJson - -/-- Note that `USize`s and `UInt64`s are stored as strings because JavaScript -cannot represent 64-bit numbers. -/ -def bignumFromJson? (j : Json) : Except String Nat := do - let s ← j.getStr? - let some v := Syntax.decodeNatLitVal? s -- TODO maybe this should be in Std - | throw s!"expected a string-encoded number, got '{j}'" - return v - -def bignumToJson (n : Nat) : Json := - toString n - -protected def _root_.USize.fromJson? (j : Json) : Except String USize := do - let n ← bignumFromJson? j - if n ≥ USize.size then - throw "value '{j}' is too large for `USize`" - return USize.ofNat n - -instance : FromJson USize where - fromJson? := USize.fromJson? - -instance : ToJson USize where - toJson v := bignumToJson (USize.toNat v) - -protected def _root_.UInt64.fromJson? (j : Json) : Except String UInt64 := do - let n ← bignumFromJson? j - if n ≥ UInt64.size then - throw "value '{j}' is too large for `UInt64`" - return UInt64.ofNat n - -instance : FromJson UInt64 where - fromJson? := UInt64.fromJson? - -instance : ToJson UInt64 where - toJson v := bignumToJson (UInt64.toNat v) - -protected def _root_.Float.toJson (x : Float) : Json := - match JsonNumber.fromFloat? x with - | Sum.inl e => Json.str e - | Sum.inr n => Json.num n - -instance : ToJson Float where - toJson := Float.toJson - -protected def _root_.Float.fromJson? : Json → Except String Float - | (Json.str "Infinity") => Except.ok (1.0 / 0.0) - | (Json.str "-Infinity") => Except.ok (-1.0 / 0.0) - | (Json.str "NaN") => Except.ok (0.0 / 0.0) - | (Json.num jn) => Except.ok jn.toFloat - | _ => Except.error "Expected a number or a string 'Infinity', '-Infinity', 'NaN'." - -instance : FromJson Float where - fromJson? := Float.fromJson? - -protected def RBMap.toJson [ToJson α] (m : RBMap String α cmp) : Json := - Json.obj <| RBNode.map (fun _ => toJson) <| m.val - -instance [ToJson α] : ToJson (RBMap String α cmp) where - toJson := RBMap.toJson - -protected def RBMap.fromJson? [FromJson α] (j : Json) : Except String (RBMap String α cmp) := do - let o ← j.getObj? - o.foldM (fun x k v => x.insert k <$> fromJson? v) ∅ - -instance {cmp} [FromJson α] : FromJson (RBMap String α cmp) where - fromJson? := RBMap.fromJson? - -namespace Json - -protected def Structured.fromJson? : Json → Except String Structured - | .arr a => return Structured.arr a - | .obj o => return Structured.obj o - | j => throw s!"expected structured object, got '{j}'" - -instance : FromJson Structured where - fromJson? := Structured.fromJson? - -protected def Structured.toJson : Structured → Json - | .arr a => .arr a - | .obj o => .obj o - -instance : ToJson Structured where - toJson := Structured.toJson - -def toStructured? [ToJson α] (v : α) : Except String Structured := - fromJson? (toJson v) - -def getObjValAs? (j : Json) (α : Type u) [FromJson α] (k : String) : Except String α := - fromJson? <| j.getObjValD k - -def setObjValAs! (j : Json) {α : Type u} [ToJson α] (k : String) (v : α) : Json := - j.setObjVal! k <| toJson v - -def opt [ToJson α] (k : String) : Option α → List (String × Json) - | none => [] - | some o => [⟨k, toJson o⟩] - -/-- Parses a JSON-encoded `structure` or `inductive` constructor. Used mostly by `deriving FromJson`. -/ -def parseTagged - (json : Json) - (tag : String) - (nFields : Nat) - (fieldNames? : Option (Array Name)) : Except String (Array Json) := - if nFields == 0 then - match getStr? json with - | Except.ok s => if s == tag then Except.ok #[] else throw s!"incorrect tag: {s} ≟ {tag}" - | Except.error err => Except.error err - else - match getObjVal? json tag with - | Except.ok payload => - match fieldNames? with - | some fieldNames => - do - let mut fields := #[] - for fieldName in fieldNames do - fields := fields.push (←getObjVal? payload fieldName.getString!) - Except.ok fields - | none => - if nFields == 1 then - Except.ok #[payload] - else - match getArr? payload with - | Except.ok fields => - if fields.size == nFields then - Except.ok fields - else - Except.error s!"incorrect number of fields: {fields.size} ≟ {nFields}" - | Except.error err => Except.error err - | Except.error err => Except.error err - -end Json -end Lean +import Lean.Data.Json.FromToJson.Basic +import Lean.Data.Json.FromToJson.Extra diff --git a/src/Lean/Data/Json/FromToJson/Basic.lean b/src/Lean/Data/Json/FromToJson/Basic.lean new file mode 100644 index 0000000000..c3474c00b4 --- /dev/null +++ b/src/Lean/Data/Json/FromToJson/Basic.lean @@ -0,0 +1,258 @@ +/- +Copyright (c) 2019 Gabriel Ebner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: Gabriel Ebner, Marc Huisinga +-/ +prelude +import Lean.Data.Json.Basic +import Lean.Data.Json.Printer + +namespace Lean + +universe u + +class FromJson (α : Type u) where + fromJson? : Json → Except String α + +export FromJson (fromJson?) + +class ToJson (α : Type u) where + toJson : α → Json + +export ToJson (toJson) + +instance : FromJson Json := ⟨Except.ok⟩ +instance : ToJson Json := ⟨id⟩ + +instance : FromJson JsonNumber := ⟨Json.getNum?⟩ +instance : ToJson JsonNumber := ⟨Json.num⟩ + +instance : FromJson Empty where + fromJson? j := throw (s!"type Empty has no constructor to match JSON value '{j}'. \ + This occurs when deserializing a value for type Empty, \ + e.g. at type Option Empty with code for the 'some' constructor.") + +instance : ToJson Empty := ⟨nofun⟩ +-- looks like id, but there are coercions happening +instance : FromJson Bool := ⟨Json.getBool?⟩ +instance : ToJson Bool := ⟨fun b => b⟩ +instance : FromJson Nat := ⟨Json.getNat?⟩ +instance : ToJson Nat := ⟨fun n => n⟩ +instance : FromJson Int := ⟨Json.getInt?⟩ +instance : ToJson Int := ⟨fun n => Json.num n⟩ +instance : FromJson String := ⟨Json.getStr?⟩ +instance : ToJson String := ⟨fun s => s⟩ + +instance : FromJson System.FilePath := ⟨fun j => System.FilePath.mk <$> Json.getStr? j⟩ +instance : ToJson System.FilePath := ⟨fun p => p.toString⟩ + +protected def _root_.Array.fromJson? [FromJson α] : Json → Except String (Array α) + | Json.arr a => a.mapM fromJson? + | j => throw s!"expected JSON array, got '{j}'" + +instance [FromJson α] : FromJson (Array α) where + fromJson? := Array.fromJson? + +protected def _root_.Array.toJson [ToJson α] (a : Array α) : Json := + Json.arr (a.map toJson) + +instance [ToJson α] : ToJson (Array α) where + toJson := Array.toJson + +protected def _root_.List.fromJson? [FromJson α] (j : Json) : Except String (List α) := + (fromJson? j (α := Array α)).map Array.toList + +instance [FromJson α] : FromJson (List α) where + fromJson? := List.fromJson? + +protected def _root_.List.toJson [ToJson α] (a : List α) : Json := + toJson a.toArray + +instance [ToJson α] : ToJson (List α) where + toJson := List.toJson + +protected def _root_.Option.fromJson? [FromJson α] : Json → Except String (Option α) + | Json.null => Except.ok none + | j => some <$> fromJson? j + +instance [FromJson α] : FromJson (Option α) where + fromJson? := Option.fromJson? + +protected def _root_.Option.toJson [ToJson α] : Option α → Json + | none => Json.null + | some a => toJson a + +instance [ToJson α] : ToJson (Option α) where + toJson := Option.toJson + +protected def _root_.Prod.fromJson? {α : Type u} {β : Type v} [FromJson α] [FromJson β] : Json → Except String (α × β) + | Json.arr #[ja, jb] => do + let ⟨a⟩ : ULift.{v} α := ← (fromJson? ja).map ULift.up + let ⟨b⟩ : ULift.{u} β := ← (fromJson? jb).map ULift.up + return (a, b) + | j => throw s!"expected pair, got '{j}'" + +instance {α : Type u} {β : Type v} [FromJson α] [FromJson β] : FromJson (α × β) where + fromJson? := Prod.fromJson? + +protected def _root_.Prod.toJson [ToJson α] [ToJson β] : α × β → Json + | (a, b) => Json.arr #[toJson a, toJson b] + +instance [ToJson α] [ToJson β] : ToJson (α × β) where + toJson := Prod.toJson + +protected def Name.fromJson? (j : Json) : Except String Name := do + let s ← j.getStr? + if s == "[anonymous]" then + return Name.anonymous + else + let n := s.toName + if n.isAnonymous then throw s!"expected a `Name`, got '{j}'" + return n + +instance : FromJson Name where + fromJson? := Name.fromJson? + +instance : ToJson Name where + toJson n := toString n + +protected def NameMap.fromJson? [FromJson α] : Json → Except String (NameMap α) + | .obj obj => obj.foldlM (init := {}) fun m k v => do + if k == "[anonymous]" then + return m.insert .anonymous (← fromJson? v) + else + let n := k.toName + if n.isAnonymous then + throw s!"expected a `Name`, got '{k}'" + else + return m.insert n (← fromJson? v) + | j => throw s!"expected a `NameMap`, got '{j}'" + +instance [FromJson α] : FromJson (NameMap α) where + fromJson? := NameMap.fromJson? + +protected def NameMap.toJson [ToJson α] (m : NameMap α) : Json := + Json.obj <| m.foldl (fun n k v => n.insert k.toString (toJson v)) ∅ + +instance [ToJson α] : ToJson (NameMap α) where + toJson := NameMap.toJson + +/-- Note that `USize`s and `UInt64`s are stored as strings because JavaScript +cannot represent 64-bit numbers. -/ +def bignumFromJson? (j : Json) : Except String Nat := do + let s ← j.getStr? + let some v := Syntax.decodeNatLitVal? s -- TODO maybe this should be in Std + | throw s!"expected a string-encoded number, got '{j}'" + return v + +def bignumToJson (n : Nat) : Json := + toString n + +protected def _root_.USize.fromJson? (j : Json) : Except String USize := do + let n ← bignumFromJson? j + if n ≥ USize.size then + throw "value '{j}' is too large for `USize`" + return USize.ofNat n + +instance : FromJson USize where + fromJson? := USize.fromJson? + +instance : ToJson USize where + toJson v := bignumToJson (USize.toNat v) + +protected def _root_.UInt64.fromJson? (j : Json) : Except String UInt64 := do + let n ← bignumFromJson? j + if n ≥ UInt64.size then + throw "value '{j}' is too large for `UInt64`" + return UInt64.ofNat n + +instance : FromJson UInt64 where + fromJson? := UInt64.fromJson? + +instance : ToJson UInt64 where + toJson v := bignumToJson (UInt64.toNat v) + +protected def _root_.Float.toJson (x : Float) : Json := + match JsonNumber.fromFloat? x with + | Sum.inl e => Json.str e + | Sum.inr n => Json.num n + +instance : ToJson Float where + toJson := Float.toJson + +protected def _root_.Float.fromJson? : Json → Except String Float + | (Json.str "Infinity") => Except.ok (1.0 / 0.0) + | (Json.str "-Infinity") => Except.ok (-1.0 / 0.0) + | (Json.str "NaN") => Except.ok (0.0 / 0.0) + | (Json.num jn) => Except.ok jn.toFloat + | _ => Except.error "Expected a number or a string 'Infinity', '-Infinity', 'NaN'." + +instance : FromJson Float where + fromJson? := Float.fromJson? + +namespace Json + +protected def Structured.fromJson? : Json → Except String Structured + | .arr a => return Structured.arr a + | .obj o => return Structured.obj o + | j => throw s!"expected structured object, got '{j}'" + +instance : FromJson Structured where + fromJson? := Structured.fromJson? + +protected def Structured.toJson : Structured → Json + | .arr a => .arr a + | .obj o => .obj o + +instance : ToJson Structured where + toJson := Structured.toJson + +def toStructured? [ToJson α] (v : α) : Except String Structured := + fromJson? (toJson v) + +def getObjValAs? (j : Json) (α : Type u) [FromJson α] (k : String) : Except String α := + fromJson? <| j.getObjValD k + +def setObjValAs! (j : Json) {α : Type u} [ToJson α] (k : String) (v : α) : Json := + j.setObjVal! k <| toJson v + +def opt [ToJson α] (k : String) : Option α → List (String × Json) + | none => [] + | some o => [⟨k, toJson o⟩] + +/-- Parses a JSON-encoded `structure` or `inductive` constructor. Used mostly by `deriving FromJson`. -/ +def parseTagged + (json : Json) + (tag : String) + (nFields : Nat) + (fieldNames? : Option (Array Name)) : Except String (Array Json) := + if nFields == 0 then + match getStr? json with + | Except.ok s => if s == tag then Except.ok #[] else throw s!"incorrect tag: {s} ≟ {tag}" + | Except.error err => Except.error err + else + match getObjVal? json tag with + | Except.ok payload => + match fieldNames? with + | some fieldNames => + do + let mut fields := #[] + for fieldName in fieldNames do + fields := fields.push (←getObjVal? payload fieldName.getString!) + Except.ok fields + | none => + if nFields == 1 then + Except.ok #[payload] + else + match getArr? payload with + | Except.ok fields => + if fields.size == nFields then + Except.ok fields + else + Except.error s!"incorrect number of fields: {fields.size} ≟ {nFields}" + | Except.error err => Except.error err + | Except.error err => Except.error err + +end Json +end Lean diff --git a/src/Lean/Data/Json/FromToJson/Extra.lean b/src/Lean/Data/Json/FromToJson/Extra.lean new file mode 100644 index 0000000000..da80268bd6 --- /dev/null +++ b/src/Lean/Data/Json/FromToJson/Extra.lean @@ -0,0 +1,35 @@ +/- +Copyright (c) 2019 Gabriel Ebner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: Gabriel Ebner, Marc Huisinga +-/ +prelude +import Lean.Data.Json.FromToJson.Basic +import Std.Data.TreeMap.AdditionalOperations + +/- +This module exists to cut the dependency on `Std.Data.TreeMap.AdditionalOperations` from a large +chunk of the meta framework. +-/ + +namespace Lean + +private def TreeMap.toJson [ToJson α] (map : Std.TreeMap String α compare) : Json := + let json := Std.TreeMap.map (fun _ => Lean.toJson) <| map + -- TODO(henrik): remove this after Q4 + Json.obj <| Std.TreeMap.Raw.mk <| Std.DTreeMap.Raw.mk json.inner.inner + +private def TreeMap.fromJson? {cmp} [FromJson α] (j : Json) : + Except String (Std.TreeMap String α cmp) := do + let o ← j.getObj? + o.foldlM (fun x k v => x.insert k <$> Lean.fromJson? v) ∅ + +instance [ToJson α] : ToJson (Std.TreeMap String α compare) where + toJson := TreeMap.toJson + +instance {cmp} [FromJson α] : FromJson (Std.TreeMap String α cmp) where + fromJson? := TreeMap.fromJson? + + +end Lean diff --git a/src/Lean/Data/Json/Parser.lean b/src/Lean/Data/Json/Parser.lean index 810d0fcc32..f7cd1bda63 100644 --- a/src/Lean/Data/Json/Parser.lean +++ b/src/Lean/Data/Json/Parser.lean @@ -6,7 +6,6 @@ Authors: Gabriel Ebner, Marc Huisinga -/ prelude import Lean.Data.Json.Basic -import Lean.Data.RBMap import Std.Internal.Parsec open Std.Internal.Parsec @@ -211,7 +210,8 @@ mutual else fail "unexpected character in array" - partial def objectCore (kvs : RBNode String (fun _ => Json)) : Parser (RBNode String (fun _ => Json)) := do + partial def objectCore (kvs : Std.TreeMap.Raw String Json) : + Parser (Std.TreeMap.Raw String Json) := do lookahead (fun c => c == '"') "\""; skip; let k ← str; ws lookahead (fun c => c == ':') ":"; skip; ws @@ -219,10 +219,10 @@ mutual let c ← any if c == '}' then ws - return kvs.insert compare k v + return kvs.insert k v else if c == ',' then ws - objectCore (kvs.insert compare k v) + objectCore (kvs.insert k v) else fail "unexpected character in object" @@ -242,9 +242,9 @@ mutual let c ← peek! if c == '}' then skip; ws - return Json.obj (RBNode.leaf) + return Json.obj ∅ else - let kvs ← objectCore RBNode.leaf + let kvs ← objectCore ∅ return Json.obj kvs else if c == '\"' then skip diff --git a/src/Lean/Data/Json/Printer.lean b/src/Lean/Data/Json/Printer.lean index d58f5fac29..ac797179b0 100644 --- a/src/Lean/Data/Json/Printer.lean +++ b/src/Lean/Data/Json/Printer.lean @@ -96,7 +96,7 @@ partial def render : Json → Format | obj kvs => let renderKV : String → Json → Format := fun k v => Format.group (renderString k ++ ":" ++ Format.line ++ render v); - let kvs := Format.joinSep (kvs.fold (fun acc k j => renderKV k j :: acc) []) ("," ++ Format.line); + let kvs := Format.joinSep (kvs.foldl (fun acc k j => renderKV k j :: acc) []) ("," ++ Format.line); Format.bracket "{" kvs "}" end @@ -124,7 +124,7 @@ where go (acc : String) : List Json.CompressWorkItem → String | num s => go (acc ++ s.toString) is | str s => go (renderString s acc) is | arr elems => go (acc ++ "[") ((elems.map arrayElem).toListAppend (arrayEnd :: is)) - | obj kvs => go (acc ++ "{") (kvs.fold (init := []) (fun acc k j => objectField k j :: acc) ++ [objectEnd] ++ is) + | obj kvs => go (acc ++ "{") (kvs.foldl (init := []) (fun acc k j => objectField k j :: acc) ++ [objectEnd] ++ is) | arrayElem j :: arrayEnd :: is => go acc (json j :: arrayEnd :: is) | arrayElem j :: is => go acc (json j :: comma :: is) | arrayEnd :: is => go (acc ++ "]") is diff --git a/src/Lean/Data/Json/Stream.lean b/src/Lean/Data/Json/Stream.lean index cfd58eb520..6f20da7b01 100644 --- a/src/Lean/Data/Json/Stream.lean +++ b/src/Lean/Data/Json/Stream.lean @@ -8,7 +8,6 @@ prelude import Init.System.IO import Lean.Data.Json.Parser import Lean.Data.Json.Printer -import Lean.Data.Json.FromToJson namespace IO.FS.Stream diff --git a/src/Lean/Data/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean index a53656e8f6..3e0afbbe3e 100644 --- a/src/Lean/Data/JsonRpc.lean +++ b/src/Lean/Data/JsonRpc.lean @@ -6,8 +6,8 @@ Authors: Marc Huisinga, Wojciech Nawrocki -/ prelude import Init.System.IO -import Lean.Data.RBTree -import Lean.Data.Json +import Lean.Data.Json.Stream +import Lean.Data.Json.FromToJson.Basic /-! Implementation of JSON-RPC 2.0 (https://www.jsonrpc.org/specification) for use in the LSP server. -/ diff --git a/src/Lean/Data/KVMap.lean b/src/Lean/Data/KVMap.lean index f56a30e5fd..9c2ed4eebd 100644 --- a/src/Lean/Data/KVMap.lean +++ b/src/Lean/Data/KVMap.lean @@ -59,8 +59,8 @@ instance : Coe Syntax DataValue := ⟨.ofSyntax⟩ /-- A key-value map. We use it to represent user-selected options and `Expr.mdata`. -Remark: we do not use `RBMap` here because we need to manipulate `KVMap` objects in -C++ and `RBMap` is implemented in Lean. So, we use just a `List` until we can +Remark: we do not use a Lean `Std.TreeMap` here because we need to manipulate `KVMap` objects in +C++ and `Std.TreeMap` is implemented in Lean. So, we use just a `List` until we can generate C++ code from Lean code. -/ structure KVMap where diff --git a/src/Lean/Data/Lsp/Basic.lean b/src/Lean/Data/Lsp/Basic.lean index cf38373638..8b0ae443d4 100644 --- a/src/Lean/Data/Lsp/Basic.lean +++ b/src/Lean/Data/Lsp/Basic.lean @@ -6,6 +6,7 @@ Authors: Marc Huisinga, Wojciech Nawrocki -/ prelude import Lean.Data.Json +import Lean.Data.Lsp.BasicAux /-! Defines most of the 'Basic Structures' in the LSP specification (https://microsoft.github.io/language-server-protocol/specifications/specification-current/), @@ -18,31 +19,6 @@ namespace Lsp open Json -abbrev DocumentUri := String - -/-- We adopt the convention that zero-based UTF-16 positions as sent by LSP clients -are represented by `Lsp.Position` while internally we mostly use `String.Pos` UTF-8 -offsets. For diagnostics, one-based `Lean.Position`s are used internally. -`character` is accepted liberally: actual character := min(line length, character) -/ -structure Position where - line : Nat - character : Nat - deriving Inhabited, BEq, Ord, Hashable, ToJson, FromJson, Repr - -instance : ToString Position := ⟨fun p => - "(" ++ toString p.line ++ ", " ++ toString p.character ++ ")"⟩ - -instance : LT Position := ltOfOrd -instance : LE Position := leOfOrd - -structure Range where - start : Position - «end» : Position - deriving Inhabited, BEq, Hashable, ToJson, FromJson, Ord, Repr - -instance : LT Range := ltOfOrd -instance : LE Range := leOfOrd - /-- A `Location` is a `DocumentUri` and a `Range`. -/ structure Location where uri : DocumentUri @@ -249,7 +225,7 @@ instance : FromJson DocumentChange where [reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#workspaceEdit) -/ structure WorkspaceEdit where /-- Changes to existing resources. -/ - changes? : Option (RBMap DocumentUri TextEditBatch compare) := none + changes? : Option (Std.TreeMap DocumentUri TextEditBatch) := none /-- Depending on the client capability `workspace.workspaceEdit.resourceOperations` document changes are either an array of `TextDocumentEdit`s to express changes to n different text @@ -270,7 +246,7 @@ structure WorkspaceEdit where Whether clients honor this property depends on the client capability `workspace.changeAnnotationSupport`. -/ - changeAnnotations? : Option (RBMap String ChangeAnnotation compare) := none + changeAnnotations? : Option (Std.TreeMap String ChangeAnnotation) := none deriving ToJson, FromJson namespace WorkspaceEdit @@ -282,7 +258,7 @@ instance : Append WorkspaceEdit where changes? := match x.changes?, y.changes? with | v, none | none, v => v - | some x, some y => x.mergeBy (fun _ v₁ v₂ => v₁ ++ v₂) y + | some x, some y => x.mergeWith (fun _ v₁ v₂ => v₁ ++ v₂) y documentChanges? := match x.documentChanges?, y.documentChanges? with | v, none | none, v => v @@ -290,7 +266,7 @@ instance : Append WorkspaceEdit where changeAnnotations? := match x.changeAnnotations?, y.changeAnnotations? with | v, none | none, v => v - | some x, some y => x.mergeBy (fun _ _v₁ v₂ => v₂) y + | some x, some y => x.mergeWith (fun _ _v₁ v₂ => v₂) y } def ofTextDocumentEdit (e : TextDocumentEdit) : WorkspaceEdit := diff --git a/src/Lean/Data/Lsp/BasicAux.lean b/src/Lean/Data/Lsp/BasicAux.lean new file mode 100644 index 0000000000..52391a4622 --- /dev/null +++ b/src/Lean/Data/Lsp/BasicAux.lean @@ -0,0 +1,48 @@ +/- +Copyright (c) 2020 Marc Huisinga. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: Marc Huisinga, Wojciech Nawrocki +-/ +prelude +import Lean.Data.Json.FromToJson.Basic + +/- +This module exists to cut the dependency on `Std.Data.TreeMap.AdditionalOperations` from a large +chunk of the meta framework. +-/ + +namespace Lean +namespace Lsp + +open Json + +abbrev DocumentUri := String + +/-- We adopt the convention that zero-based UTF-16 positions as sent by LSP clients +are represented by `Lsp.Position` while internally we mostly use `String.Pos` UTF-8 +offsets. For diagnostics, one-based `Lean.Position`s are used internally. +`character` is accepted liberally: actual character := min(line length, character) -/ +structure Position where + line : Nat + character : Nat + deriving Inhabited, BEq, Ord, Hashable, ToJson, FromJson, Repr + +instance : ToString Position := ⟨fun p => + "(" ++ toString p.line ++ ", " ++ toString p.character ++ ")"⟩ + +instance : LT Position := ltOfOrd +instance : LE Position := leOfOrd + +structure Range where + start : Position + «end» : Position + deriving Inhabited, BEq, Hashable, ToJson, FromJson, Ord, Repr + +instance : LT Range := ltOfOrd +instance : LE Range := leOfOrd + +end Lsp +end Lean + + diff --git a/src/Lean/Data/Lsp/Client.lean b/src/Lean/Data/Lsp/Client.lean index 4b4255c1b0..bdd384c3f6 100644 --- a/src/Lean/Data/Lsp/Client.lean +++ b/src/Lean/Data/Lsp/Client.lean @@ -6,7 +6,6 @@ Authors: Joscha Mennicken -/ prelude import Lean.Data.Lsp.Basic -import Lean.Data.Json namespace Lean namespace Lsp diff --git a/src/Lean/Data/Lsp/CodeActions.lean b/src/Lean/Data/Lsp/CodeActions.lean index f736ea2008..99a03f91d9 100644 --- a/src/Lean/Data/Lsp/CodeActions.lean +++ b/src/Lean/Data/Lsp/CodeActions.lean @@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: E.W.Ayers -/ prelude -import Lean.Data.Json import Lean.Data.Lsp.Basic import Lean.Data.Lsp.Diagnostics diff --git a/src/Lean/Data/Lsp/Diagnostics.lean b/src/Lean/Data/Lsp/Diagnostics.lean index a9180a6ea8..6d7c340590 100644 --- a/src/Lean/Data/Lsp/Diagnostics.lean +++ b/src/Lean/Data/Lsp/Diagnostics.lean @@ -5,7 +5,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Marc Huisinga, Wojciech Nawrocki -/ prelude -import Lean.Data.Json import Lean.Data.Lsp.Basic import Lean.Data.Lsp.Utf16 diff --git a/src/Lean/Data/Lsp/InitShutdown.lean b/src/Lean/Data/Lsp/InitShutdown.lean index d19ccf8493..92287c8f94 100644 --- a/src/Lean/Data/Lsp/InitShutdown.lean +++ b/src/Lean/Data/Lsp/InitShutdown.lean @@ -7,7 +7,6 @@ Authors: Marc Huisinga, Wojciech Nawrocki prelude import Lean.Data.Lsp.Capabilities import Lean.Data.Lsp.Workspace -import Lean.Data.Json /-! Functionality to do with initializing and shutting down the server ("General Messages" section of LSP spec). -/ diff --git a/src/Lean/Data/Lsp/Internal.lean b/src/Lean/Data/Lsp/Internal.lean index c6bcd550c1..fde55bbb65 100644 --- a/src/Lean/Data/Lsp/Internal.lean +++ b/src/Lean/Data/Lsp/Internal.lean @@ -8,7 +8,6 @@ prelude import Lean.Expr import Lean.Data.Lsp.Basic import Lean.Data.JsonRpc -import Std.Data.TreeMap set_option linter.missingDocs true -- keep it documented @@ -196,7 +195,7 @@ instance : ToJson ModuleRefs where instance : FromJson ModuleRefs where fromJson? j := do let node ← j.getObj? - node.foldM (init := ∅) fun m k v => + node.foldlM (init := ∅) fun m k v => return m.insert (← RefIdent.fromJson? (← Json.parse k)) (← fromJson? v) /-- diff --git a/src/Lean/Data/Lsp/Ipc.lean b/src/Lean/Data/Lsp/Ipc.lean index 3c93db5bb9..2fcea7f8b3 100644 --- a/src/Lean/Data/Lsp/Ipc.lean +++ b/src/Lean/Data/Lsp/Ipc.lean @@ -6,7 +6,7 @@ Authors: Marc Huisinga, Wojciech Nawrocki -/ prelude import Init.System.IO -import Lean.Data.Json +import Lean.Data.Json.Basic import Lean.Data.Lsp.Communication import Lean.Data.Lsp.Diagnostics import Lean.Data.Lsp.Extra diff --git a/src/Lean/Data/Lsp/LanguageFeatures.lean b/src/Lean/Data/Lsp/LanguageFeatures.lean index 8f55fa96e0..0824323075 100644 --- a/src/Lean/Data/Lsp/LanguageFeatures.lean +++ b/src/Lean/Data/Lsp/LanguageFeatures.lean @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Wojciech Nawrocki -/ prelude -import Lean.Data.Json +import Lean.Data.Json.FromToJson.Basic import Lean.Data.Lsp.Basic namespace Lean diff --git a/src/Lean/Data/Lsp/TextSync.lean b/src/Lean/Data/Lsp/TextSync.lean index 92be265763..69bb6aca42 100644 --- a/src/Lean/Data/Lsp/TextSync.lean +++ b/src/Lean/Data/Lsp/TextSync.lean @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Marc Huisinga, Wojciech Nawrocki -/ prelude -import Lean.Data.Json +import Lean.Data.Json.FromToJson.Basic import Lean.Data.Lsp.Basic /-! Section "Text Document Synchronization" of the LSP spec. -/ diff --git a/src/Lean/Data/Lsp/Utf16.lean b/src/Lean/Data/Lsp/Utf16.lean index 2d441d6584..81d382ca40 100644 --- a/src/Lean/Data/Lsp/Utf16.lean +++ b/src/Lean/Data/Lsp/Utf16.lean @@ -6,7 +6,7 @@ Authors: Marc Huisinga, Wojciech Nawrocki -/ prelude import Init.Data.String -import Lean.Data.Lsp.Basic +import Lean.Data.Lsp.BasicAux import Lean.Data.Position import Lean.DeclarationRange diff --git a/src/Lean/Data/Lsp/Window.lean b/src/Lean/Data/Lsp/Window.lean index 38379d7705..8ac35250f8 100644 --- a/src/Lean/Data/Lsp/Window.lean +++ b/src/Lean/Data/Lsp/Window.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Marc Huisinga -/ prelude -import Lean.Data.Json +import Lean.Data.Json.FromToJson.Basic open Lean diff --git a/src/Lean/Data/Lsp/Workspace.lean b/src/Lean/Data/Lsp/Workspace.lean index 1a1484cc44..35cb4190e1 100644 --- a/src/Lean/Data/Lsp/Workspace.lean +++ b/src/Lean/Data/Lsp/Workspace.lean @@ -6,7 +6,7 @@ Authors: Wojciech Nawrocki -/ prelude import Lean.Data.Lsp.Basic -import Lean.Data.Json +import Lean.Data.Json.FromToJson.Basic namespace Lean namespace Lsp diff --git a/src/Lean/Data/NameMap.lean b/src/Lean/Data/NameMap.lean index 67fa15bf75..a6daa371e2 100644 --- a/src/Lean/Data/NameMap.lean +++ b/src/Lean/Data/NameMap.lean @@ -4,104 +4,5 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ prelude -import Std.Data.HashSet.Basic -import Lean.Data.RBMap -import Lean.Data.RBTree -import Lean.Data.SSet -import Lean.Data.Name -namespace Lean - -def NameMap (α : Type) := RBMap Name α Name.quickCmp - -@[inline] def mkNameMap (α : Type) : NameMap α := mkRBMap Name α Name.quickCmp - -namespace NameMap -variable {α : Type} - -instance [Repr α] : Repr (NameMap α) := inferInstanceAs (Repr (RBMap Name α Name.quickCmp)) - -instance (α : Type) : EmptyCollection (NameMap α) := ⟨mkNameMap α⟩ - -instance (α : Type) : Inhabited (NameMap α) where - default := {} - -def insert (m : NameMap α) (n : Name) (a : α) := RBMap.insert m n a - -def contains (m : NameMap α) (n : Name) : Bool := RBMap.contains m n - -def find? (m : NameMap α) (n : Name) : Option α := RBMap.find? m n - -instance : ForIn m (NameMap α) (Name × α) := - inferInstanceAs (ForIn _ (RBMap ..) ..) - -/-- `filter f m` returns the `NameMap` consisting of all -"`key`/`val`"-pairs in `m` where `f key val` returns `true`. -/ -def filter (f : Name → α → Bool) (m : NameMap α) : NameMap α := RBMap.filter f m - -/-- `filterMap f m` filters an `NameMap` and simultaneously modifies the filtered values. - -It takes a function `f : Name → α → Option β` and applies `f name` to the value with key `name`. -The resulting entries with non-`none` value are collected to form the output `NameMap`. -/ -def filterMap (f : Name → α → Option β) (m : NameMap α) : NameMap β := RBMap.filterMap f m - -end NameMap - -def NameSet := RBTree Name Name.quickCmp - -namespace NameSet -def empty : NameSet := mkRBTree Name Name.quickCmp -instance : EmptyCollection NameSet := ⟨empty⟩ -instance : Inhabited NameSet := ⟨empty⟩ -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 _ (RBTree ..) ..) - -/-- The union of two `NameSet`s. -/ -def append (s t : NameSet) : NameSet := - s.mergeBy (fun _ _ _ => .unit) t - -instance : Append NameSet where - append := NameSet.append - -/-- `filter f s` returns the `NameSet` consisting of all `x` in `s` where `f x` returns `true`. -/ -def filter (f : Name → Bool) (s : NameSet) : NameSet := RBTree.filter f s - -end NameSet - -def NameSSet := SSet Name - -namespace NameSSet -abbrev empty : NameSSet := SSet.empty -instance : EmptyCollection NameSSet := ⟨empty⟩ -instance : Inhabited NameSSet := ⟨empty⟩ -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 - -namespace NameHashSet -@[inline] def empty : NameHashSet := (∅ : Std.HashSet Name) -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 - -/-- `filter f s` returns the `NameHashSet` consisting of all `x` in `s` where `f x` returns `true`. -/ -def filter (f : Name → Bool) (s : NameHashSet) : NameHashSet := Std.HashSet.filter f s -end NameHashSet - -def MacroScopesView.isPrefixOf (v₁ v₂ : MacroScopesView) : Bool := - v₁.name.isPrefixOf v₂.name && - v₁.scopes == v₂.scopes && - v₁.mainModule == v₂.mainModule && - v₁.imported == v₂.imported - -def MacroScopesView.isSuffixOf (v₁ v₂ : MacroScopesView) : Bool := - v₁.name.isSuffixOf v₂.name && - v₁.scopes == v₂.scopes && - v₁.mainModule == v₂.mainModule && - v₁.imported == v₂.imported - -end Lean +import Lean.Data.NameMap.Basic +import Lean.Data.NameMap.AdditionalOperations diff --git a/src/Lean/Data/NameMap/AdditionalOperations.lean b/src/Lean/Data/NameMap/AdditionalOperations.lean new file mode 100644 index 0000000000..341276d898 --- /dev/null +++ b/src/Lean/Data/NameMap/AdditionalOperations.lean @@ -0,0 +1,20 @@ +/- +Copyright (c) 2018 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Leonardo de Moura +-/ +prelude +import Lean.Data.NameMap.Basic +import Std.Data.TreeSet.AdditionalOperations + +namespace Lean +namespace NameMap + +/-- `filterMap f m` filters an `NameMap` and simultaneously modifies the filtered values. + +It takes a function `f : Name → α → Option β` and applies `f name` to the value with key `name`. +The resulting entries with non-`none` value are collected to form the output `NameMap`. -/ +def filterMap (f : Name → α → Option β) (m : NameMap α) : NameMap β := Std.TreeMap.filterMap f m + +end NameMap +end Lean diff --git a/src/Lean/Data/NameMap/Basic.lean b/src/Lean/Data/NameMap/Basic.lean new file mode 100644 index 0000000000..3127dab44d --- /dev/null +++ b/src/Lean/Data/NameMap/Basic.lean @@ -0,0 +1,105 @@ +/- +Copyright (c) 2018 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Leonardo de Moura +-/ +prelude +import Std.Data.HashSet.Basic +import Std.Data.TreeSet.Basic +import Lean.Data.SSet +import Lean.Data.Name + +namespace Lean + +def NameMap (α : Type) := Std.TreeMap Name α Name.quickCmp + +@[inline] def mkNameMap (α : Type) : NameMap α := Std.TreeMap.empty + +namespace NameMap +variable {α : Type} + +instance [Repr α] : Repr (NameMap α) := inferInstanceAs (Repr (Std.TreeMap _ _ _)) + +instance (α : Type) : EmptyCollection (NameMap α) := ⟨mkNameMap α⟩ + +instance (α : Type) : Inhabited (NameMap α) where + default := {} + +def insert (m : NameMap α) (n : Name) (a : α) := Std.TreeMap.insert m n a + +def contains (m : NameMap α) (n : Name) : Bool := Std.TreeMap.contains m n + +def find? (m : NameMap α) (n : Name) : Option α := Std.TreeMap.get? m n + +instance : ForIn m (NameMap α) (Name × α) := + inferInstanceAs (ForIn _ (Std.TreeMap _ _ _) ..) + +/-- `filter f m` returns the `NameMap` consisting of all +"`key`/`val`"-pairs in `m` where `f key val` returns `true`. -/ +def filter (f : Name → α → Bool) (m : NameMap α) : NameMap α := Std.TreeMap.filter f m + +end NameMap + +def NameSet := Std.TreeSet Name Name.quickCmp + +namespace NameSet +def empty : NameSet := Std.TreeSet.empty +instance : EmptyCollection NameSet := ⟨empty⟩ +instance : Inhabited NameSet := ⟨empty⟩ +def insert (s : NameSet) (n : Name) : NameSet := Std.TreeSet.insert s n +def contains (s : NameSet) (n : Name) : Bool := Std.TreeSet.contains s n +instance : ForIn m NameSet Name := + inferInstanceAs (ForIn _ (Std.TreeSet _ _) ..) + +/-- The union of two `NameSet`s. -/ +def append (s t : NameSet) : NameSet := + s.merge t + +instance : Append NameSet where + append := NameSet.append + +/-- `filter f s` returns the `NameSet` consisting of all `x` in `s` where `f x` returns `true`. -/ +def filter (f : Name → Bool) (s : NameSet) : NameSet := Std.TreeSet.filter f s + +def ofList (l : List Name) : NameSet := Std.TreeSet.ofList l _ + +def ofArray (l : Array Name) : NameSet := Std.TreeSet.ofArray l _ + +end NameSet + +def NameSSet := SSet Name + +namespace NameSSet +abbrev empty : NameSSet := SSet.empty +instance : EmptyCollection NameSSet := ⟨empty⟩ +instance : Inhabited NameSSet := ⟨empty⟩ +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 + +namespace NameHashSet +@[inline] def empty : NameHashSet := (∅ : Std.HashSet Name) +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 + +/-- `filter f s` returns the `NameHashSet` consisting of all `x` in `s` where `f x` returns `true`. -/ +def filter (f : Name → Bool) (s : NameHashSet) : NameHashSet := Std.HashSet.filter f s +end NameHashSet + +def MacroScopesView.isPrefixOf (v₁ v₂ : MacroScopesView) : Bool := + v₁.name.isPrefixOf v₂.name && + v₁.scopes == v₂.scopes && + v₁.mainModule == v₂.mainModule && + v₁.imported == v₂.imported + +def MacroScopesView.isSuffixOf (v₁ v₂ : MacroScopesView) : Bool := + v₁.name.isSuffixOf v₂.name && + v₁.scopes == v₂.scopes && + v₁.mainModule == v₂.mainModule && + v₁.imported == v₂.imported + +end Lean diff --git a/src/Lean/Data/Options.lean b/src/Lean/Data/Options.lean index e8d7dd2278..7adec36b77 100644 --- a/src/Lean/Data/Options.lean +++ b/src/Lean/Data/Options.lean @@ -6,7 +6,7 @@ Authors: Sebastian Ullrich and Leonardo de Moura prelude import Lean.ImportingFlag import Lean.Data.KVMap -import Lean.Data.NameMap +import Lean.Data.NameMap.Basic namespace Lean @@ -46,7 +46,7 @@ def getOptionDecls : IO OptionDecls := optionDeclsRef.get @[export lean_get_option_decls_array] def getOptionDeclsArray : IO (Array (Name × OptionDecl)) := do let decls ← getOptionDecls - pure $ decls.fold + return decls.foldl (fun (r : Array (Name × OptionDecl)) k v => r.push (k, v)) #[] diff --git a/src/Lean/Data/Position.lean b/src/Lean/Data/Position.lean index de64636b8b..6bb0925d80 100644 --- a/src/Lean/Data/Position.lean +++ b/src/Lean/Data/Position.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich -/ prelude import Lean.Data.Format -import Lean.Data.Json +import Lean.Data.Json.FromToJson.Basic import Lean.ToExpr namespace Lean diff --git a/src/Lean/Data/PrefixTree.lean b/src/Lean/Data/PrefixTree.lean index 3ed612bad3..146ee95303 100644 --- a/src/Lean/Data/PrefixTree.lean +++ b/src/Lean/Data/PrefixTree.lean @@ -4,85 +4,85 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import Lean.Data.RBMap +import Std.Data.TreeMap.Raw.Basic namespace Lean /- Similar to trie, but for arbitrary keys -/ -inductive PrefixTreeNode (α : Type u) (β : Type v) where - | Node : Option β → RBNode α (fun _ => PrefixTreeNode α β) → PrefixTreeNode α β +inductive PrefixTreeNode (α : Type u) (β : Type v) (cmp : α → α → Ordering) where + | Node : Option β → Std.TreeMap.Raw α (PrefixTreeNode α β cmp) cmp → PrefixTreeNode α β cmp -instance : Inhabited (PrefixTreeNode α β) where - default := PrefixTreeNode.Node none RBNode.leaf +instance : Inhabited (PrefixTreeNode α β cmp) where + default := PrefixTreeNode.Node none ∅ namespace PrefixTreeNode -def empty : PrefixTreeNode α β := - PrefixTreeNode.Node none RBNode.leaf +def empty : PrefixTreeNode α β cmp := + PrefixTreeNode.Node none ∅ @[specialize] -partial def insert (t : PrefixTreeNode α β) (cmp : α → α → Ordering) (k : List α) (val : β) : PrefixTreeNode α β := - let rec insertEmpty (k : List α) : PrefixTreeNode α β := +partial def insert (cmp : α → α → Ordering) (t : PrefixTreeNode α β cmp) (k : List α) (val : β) : PrefixTreeNode α β cmp := + let rec insertEmpty (k : List α) : PrefixTreeNode α β cmp := match k with - | [] => PrefixTreeNode.Node (some val) RBNode.leaf + | [] => PrefixTreeNode.Node (some val) ∅ | k :: ks => let t := insertEmpty ks - PrefixTreeNode.Node none (RBNode.singleton k t) + PrefixTreeNode.Node none {(k, t)} let rec loop | PrefixTreeNode.Node _ m, [] => PrefixTreeNode.Node (some val) m -- overrides old value | PrefixTreeNode.Node v m, k :: ks => - let t := match RBNode.find cmp m k with + let t := match m.get? k with | none => insertEmpty ks | some t => loop t ks - PrefixTreeNode.Node v (RBNode.insert cmp m k t) + PrefixTreeNode.Node v (m.insert k t) loop t k @[specialize] -partial def find? (t : PrefixTreeNode α β) (cmp : α → α → Ordering) (k : List α) : Option β := +partial def find? (cmp : α → α → Ordering) (t : PrefixTreeNode α β cmp) (k : List α) : Option β := let rec loop | PrefixTreeNode.Node val _, [] => val | PrefixTreeNode.Node _ m, k :: ks => - match RBNode.find cmp m k with + match m.get? k with | none => none | some t => loop t ks loop t k /-- Returns the the value of the longest key in `t` that is a prefix of `k`, if any. -/ @[specialize] -partial def findLongestPrefix? (t : PrefixTreeNode α β) (cmp : α → α → Ordering) (k : List α) : Option β := +partial def findLongestPrefix? (cmp : α → α → Ordering) (t : PrefixTreeNode α β cmp) (k : List α) : Option β := let rec loop acc? | PrefixTreeNode.Node val _, [] => val <|> acc? | PrefixTreeNode.Node val m, k :: ks => - match RBNode.find cmp m k with + match m.get? k with | none => val | some t => loop (val <|> acc?) t ks loop none t k @[specialize] -partial def foldMatchingM [Monad m] (t : PrefixTreeNode α β) (cmp : α → α → Ordering) (k : List α) (init : σ) (f : β → σ → m σ) : m σ := - let rec fold : PrefixTreeNode α β → σ → m σ +partial def foldMatchingM [Monad m] (cmp : α → α → Ordering) (t : PrefixTreeNode α β cmp) (k : List α) (init : σ) (f : β → σ → m σ) : m σ := + let rec fold : PrefixTreeNode α β cmp → σ → m σ | PrefixTreeNode.Node b? n, d => do let d ← match b? with | none => pure d | some b => f b d - n.foldM (init := d) fun d _ t => fold t d - let rec find : List α → PrefixTreeNode α β → σ → m σ + n.foldlM (init := d) fun d _ t => fold t d + let rec find : List α → PrefixTreeNode α β cmp → σ → m σ | [], t, d => fold t d | k::ks, PrefixTreeNode.Node _ m, d => - match RBNode.find cmp m k with + match m.get? k with | none => pure init | some t => find ks t d find k t init -inductive WellFormed (cmp : α → α → Ordering) : PrefixTreeNode α β → Prop where +inductive WellFormed (cmp : α → α → Ordering) : PrefixTreeNode α β cmp → Prop where | emptyWff : WellFormed cmp empty - | insertWff : WellFormed cmp t → WellFormed cmp (insert t cmp k val) + | insertWff : WellFormed cmp t → WellFormed cmp (insert cmp t k val) end PrefixTreeNode def PrefixTree (α : Type u) (β : Type v) (cmp : α → α → Ordering) : Type (max u v) := - { t : PrefixTreeNode α β // t.WellFormed cmp } + { t : PrefixTreeNode α β cmp // t.WellFormed cmp } open PrefixTreeNode diff --git a/src/Lean/Data/Trie.lean b/src/Lean/Data/Trie.lean index f5c31b21ea..566a8a1c80 100644 --- a/src/Lean/Data/Trie.lean +++ b/src/Lean/Data/Trie.lean @@ -17,7 +17,7 @@ namespace Data Tries have typically many nodes with small degree, where a linear scan through the (compact) `ByteArray` is faster than using binary search or -search trees like `RBTree`. +search trees like `Std.TreeMap`. Moreover, many nodes have degree 1, which justifies the special case `Node1` constructor. diff --git a/src/Lean/Data/Xml/Basic.lean b/src/Lean/Data/Xml/Basic.lean index c683822ca1..3a86e6089f 100644 --- a/src/Lean/Data/Xml/Basic.lean +++ b/src/Lean/Data/Xml/Basic.lean @@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Dany Fabian -/ prelude -import Lean.Data.RBMap import Init.Data.ToString.Macro +import Std.Data.TreeMap.Basic namespace Lean namespace Xml -def Attributes := RBMap String String compare -instance : ToString Attributes := ⟨λ as => as.fold (λ s n v => s ++ s!" {n}=\"{v}\"") ""⟩ +def Attributes := Std.TreeMap String String +instance : ToString Attributes := ⟨λ as => as.foldl (λ s n v => s ++ s!" {n}=\"{v}\"") ""⟩ mutual inductive Element diff --git a/src/Lean/Data/Xml/Parser.lean b/src/Lean/Data/Xml/Parser.lean index 939bb3825f..8f39dce7bb 100644 --- a/src/Lean/Data/Xml/Parser.lean +++ b/src/Lean/Data/Xml/Parser.lean @@ -411,7 +411,7 @@ protected def elementPrefix : Parser (Array Content → Element) := do let name ← Name let attributes ← many (attempt <| S *> Attribute) optional S *> pure () - return Element.Element name (RBMap.fromList attributes.toList compare) + return Element.Element name (Std.TreeMap.ofList attributes.toList compare) /-- https://www.w3.org/TR/xml/#NT-EmptyElemTag -/ def EmptyElemTag (elem : Array Content → Element) : Parser Element := do diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 704e4aae7d..e4ba01f887 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -1379,7 +1379,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L let fullName := Name.mkStr structName fieldName for localDecl in (← getLCtx) do if localDecl.isAuxDecl then - if let some localDeclFullName := (← getLCtx).auxDeclToFullName.find? localDecl.fvarId then + if let some localDeclFullName := (← getLCtx).auxDeclToFullName.get? localDecl.fvarId then if fullName == (privateToUserName? localDeclFullName).getD localDeclFullName then /- LVal notation is being used to make a "local" recursive call. -/ return LValResolution.localRec structName fullName localDecl.toExpr diff --git a/src/Lean/Elab/DeclNameGen.lean b/src/Lean/Elab/DeclNameGen.lean index 589436cee4..74f39155be 100644 --- a/src/Lean/Elab/DeclNameGen.lean +++ b/src/Lean/Elab/DeclNameGen.lean @@ -215,7 +215,7 @@ def mkBaseNameWithSuffix (pre : String) (type : Expr) : MetaM Name := do let name := pre ++ name let project := (← getMainModule).getRoot -- Collect the modules for each constant that appeared. - let modules ← st.consts.foldM (init := Array.mkEmpty st.consts.size) fun mods name => return mods.push (← findModuleOf? name) + let modules ← st.consts.foldlM (init := Array.mkEmpty st.consts.size) fun mods name => return mods.push (← findModuleOf? name) -- We can avoid adding the suffix if the instance refers to module-local names. let isModuleLocal := modules.any Option.isNone -- We can also avoid adding the full module suffix if the instance refers to "project"-local names. diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean index a9ff570802..26f0ef5770 100644 --- a/src/Lean/Elab/Deriving/FromToJson.lean +++ b/src/Lean/Elab/Deriving/FromToJson.lean @@ -7,7 +7,7 @@ prelude import Lean.Meta.Transform import Lean.Elab.Deriving.Basic import Lean.Elab.Deriving.Util -import Lean.Data.Json.FromToJson +import Lean.Data.Json.FromToJson.Basic namespace Lean.Elab.Deriving.FromToJson open Lean.Elab.Command diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean index 56344ae37f..765c63f7a2 100644 --- a/src/Lean/Elab/Deriving/Inhabited.lean +++ b/src/Lean/Elab/Deriving/Inhabited.lean @@ -10,7 +10,7 @@ import Lean.Elab.Deriving.Basic namespace Lean.Elab open Command Meta Parser Term -private abbrev IndexSet := RBTree Nat compare +private abbrev IndexSet := Std.TreeSet Nat private abbrev LocalInst2Index := FVarIdMap Nat private def implicitBinderF := Parser.Term.implicitBinder @@ -51,7 +51,7 @@ where let visit {ω} : StateRefT IndexSet (ST ω) Unit := e.forEachWhere Expr.isFVar fun e => let fvarId := e.fvarId! - match localInst2Index.find? fvarId with + match localInst2Index.get? fvarId with | some idx => modify (·.insert idx) | none => pure () runST (fun _ => visit |>.run usedInstIdxs) |>.2 diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index 9a0a951cb5..8945c6b4d5 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -239,7 +239,7 @@ def Code.getRef? : Code → Option Syntax | .matchExpr ref .. => ref | .jmp ref .. => ref -abbrev VarSet := RBMap Name Syntax Name.cmp +abbrev VarSet := Std.TreeMap Name Syntax Name.cmp /-- A code block, and the collection of variables updated by it. -/ structure CodeBlock where @@ -247,7 +247,7 @@ structure CodeBlock where uvars : VarSet := {} -- set of variables updated by `code` private def varSetToArray (s : VarSet) : Array Var := - s.fold (fun xs _ x => xs.push x) #[] + s.foldl (fun xs _ x => xs.push x) #[] private def varsToMessageData (vars : Array Var) : MessageData := MessageData.joinSep (vars.toList.map fun n => MessageData.ofName (n.getId.simpMacroScopes)) " " @@ -540,7 +540,7 @@ partial def extendUpdatedVars (c : CodeBlock) (ws : VarSet) : TermElabM CodeBloc pure { c with uvars := ws } private def union (s₁ s₂ : VarSet) : VarSet := - s₁.fold (·.insert ·) s₂ + s₁.foldl (·.insert ·) s₂ /-- Given two code blocks `c₁` and `c₂`, make sure they have the same set of updated variables. @@ -1578,7 +1578,7 @@ mutual -- semantic no-op that replaces the `uvars`' position information (which all point inside the loop) -- with that of the respective mutable declarations outside the loop, which allows the language -- server to identify them as conceptually identical variables - let uvars := uvars.map fun v => ctx.mutableVars.findD v.getId v + let uvars := uvars.map fun v => ctx.mutableVars.getD v.getId v let uvarsTuple ← liftMacroM do mkTuple uvars if hasReturn forInBodyCodeBlock.code then let forInBody ← liftMacroM <| destructTuple uvars (← `(r)) forInBody diff --git a/src/Lean/Elab/InfoTree/Types.lean b/src/Lean/Elab/InfoTree/Types.lean index 3a770c88f1..39d16ca050 100644 --- a/src/Lean/Elab/InfoTree/Types.lean +++ b/src/Lean/Elab/InfoTree/Types.lean @@ -9,7 +9,7 @@ import Lean.Data.DeclarationRange import Lean.Data.OpenDecl import Lean.MetavarContext import Lean.Environment -import Lean.Data.Json +import Lean.Data.Json.Basic import Lean.Server.Rpc.Basic import Lean.Widget.Types diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 03b97ce1ba..4715075281 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -788,7 +788,7 @@ private def modifyUsedFVars (f : UsedFVarsMap → UsedFVarsMap) : M Unit := modi -- merge s₂ into s₁ private def merge (s₁ s₂ : FVarIdSet) : M FVarIdSet := - s₂.foldM (init := s₁) fun s₁ k => do + s₂.foldlM (init := s₁) fun s₁ k => do if s₁.contains k then return s₁ else @@ -797,14 +797,14 @@ private def merge (s₁ s₂ : FVarIdSet) : M FVarIdSet := private def updateUsedVarsOf (fvarId : FVarId) : M Unit := do let usedFVarsMap ← getUsedFVarsMap - match usedFVarsMap.find? fvarId with + match usedFVarsMap.get? fvarId with | none => return () | some fvarIds => - let fvarIdsNew ← fvarIds.foldM (init := fvarIds) fun fvarIdsNew fvarId' => do + let fvarIdsNew ← fvarIds.foldlM (init := fvarIds) fun fvarIdsNew fvarId' => do if fvarId == fvarId' then return fvarIdsNew else - match usedFVarsMap.find? fvarId' with + match usedFVarsMap.get? fvarId' with | none => return fvarIdsNew /- We are being sloppy here `otherFVarIds` may contain free variables that are not in the context of the let-rec associated with fvarId. @@ -837,8 +837,8 @@ private def mkFreeVarMap [Monad m] [MonadMCtx m] let mut freeVarMap := {} for toLift in letRecsToLift do let lctx := toLift.lctx - let fvarIdsSet := usedFVarsMap.find? toLift.fvarId |>.get! - let fvarIds := fvarIdsSet.fold (init := #[]) fun fvarIds fvarId => + let fvarIdsSet := usedFVarsMap.get? toLift.fvarId |>.get! + let fvarIds := fvarIdsSet.foldl (init := #[]) fun fvarIds fvarId => if lctx.contains fvarId && !recFVarIds.contains fvarId then fvarIds.push fvarId else @@ -863,7 +863,7 @@ private def preprocess (e : Expr) : TermElabM Expr := do /-- Push free variables in `s` to `toProcess` if they are not already there. -/ private def pushNewVars (toProcess : Array FVarId) (s : CollectFVars.State) : Array FVarId := - s.fvarSet.fold (init := toProcess) fun toProcess fvarId => + s.fvarSet.foldl (init := toProcess) fun toProcess fvarId => if toProcess.contains fvarId then toProcess else toProcess.push fvarId private def pushLocalDecl (toProcess : Array FVarId) (fvarId : FVarId) (userName : Name) (type : Expr) (bi : BinderInfo) (kind : LocalDeclKind) @@ -943,7 +943,7 @@ private def mkLetRecClosureFor (toLift : LetRecToLift) (freeVars : Array FVarId) let s ← mkClosureFor freeVars <| xs.map fun x => lctx.get! x.fvarId! /- Apply original type binder info and user-facing names to local declarations. -/ let typeLocalDecls := s.localDecls.map fun localDecl => - if let some (userName, bi) := userNameBinderInfoMap.find? localDecl.fvarId then + if let some (userName, bi) := userNameBinderInfoMap.get? localDecl.fvarId then localDecl.setBinderInfo bi |>.setUserName userName else localDecl @@ -973,7 +973,7 @@ private def mkLetRecClosures (sectionVars : Array Expr) (mainFVarIds : Array FVa -- We have to recompute the `freeVarMap` in this case. This overhead should not be an issue in practice. freeVarMap ← mkFreeVarMap sectionVars mainFVarIds recFVarIds letRecsToLift let toLift := letRecsToLift[i]! - result := result.push (← mkLetRecClosureFor toLift (freeVarMap.find? toLift.fvarId).get!) + result := result.push (← mkLetRecClosureFor toLift (freeVarMap.get? toLift.fvarId).get!) return result.toList /-- Mapping from FVarId of mutually recursive functions being defined to "closure" expression. -/ @@ -998,13 +998,13 @@ def isApplicable (r : Replacement) (e : Expr) : Bool := .done def Replacement.apply (r : Replacement) (e : Expr) : Expr := - -- Remark: if `r` is not a singlenton, then declaration is using `mutual` or `let rec`, + -- Remark: if `r` is not a singleton, then declaration is using `mutual` or `let rec`, -- and there is a big chance `isApplicable r e` is true. - if r.isSingleton && !isApplicable r e then + if r.size == 1 && !isApplicable r e then e else e.replace fun e => match e with - | .fvar fvarId => match r.find? fvarId with + | .fvar fvarId => match r.get? fvarId with | some c => some c | _ => none | _ => none diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean index 822f91bbbd..2777702265 100644 --- a/src/Lean/Elab/PatternVar.lean +++ b/src/Lean/Elab/PatternVar.lean @@ -85,7 +85,7 @@ where .ofFormatWithInfos { fmt := "'" ++ .tag 0 (format n) ++ "'", infos := - .fromList [(0, .ofTermInfo { + .ofList [(0, .ofTermInfo { lctx := .empty, expr := .const n params, stx := .ident .none (toString n).toSubstring n [.decl n []], diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean index 7ee9432e0f..07b5dd9b81 100644 --- a/src/Lean/Elab/Print.lean +++ b/src/Lean/Elab/Print.lean @@ -145,7 +145,7 @@ private partial def printStructure (id : Name) (levelParams : List Name) (numPar let fi ← getFieldOrigin source field let proj := fi.projFn let modifier := if isPrivateName proj then "private " else "" - let ftype ← inferType (fieldMap.find! field) + let ftype ← inferType (fieldMap.get! field) let value ← if let some stx := autoParams.find? field then let stx : TSyntax ``Parser.Tactic.tacticSeq := ⟨stx⟩ diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index 3c46a051af..12dd1f0b3c 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -843,7 +843,7 @@ private def synthOptParamFields : StructInstM Unit := do for pendingField in pendingFields do if (← isFieldNotSolved? pendingField.fieldName).isNone then unsolvedFields := unsolvedFields.insert pendingField.fieldName - let e := (← get).fieldMap.find! pendingField.fieldName + let e := (← get).fieldMap.get! pendingField.fieldName requiredErrors := requiredErrors.push m!"\ Field `{pendingField.fieldName}` must be explicitly provided; its synthesized value is{indentExpr e}" let requiredErrorsMsg := MessageData.joinSep (requiredErrors.map (m!"\n\n" ++ ·)).toList "" @@ -854,7 +854,7 @@ private def synthOptParamFields : StructInstM Unit := do let missing := missingFields |>.map (s!"`{·.fieldName}`") |>.toList let missingFieldsValues ← missingFields.mapM fun field => do if unsolvedFields.contains field.fieldName then - pure <| (field.fieldName, some <| (← get).fieldMap.find! field.fieldName) + pure <| (field.fieldName, some <| (← get).fieldMap.get! field.fieldName) else pure (field.fieldName, none) let missingFieldsHint ← mkMissingFieldsHint missingFieldsValues (← read).view.ref let msg := m!"Fields missing: {", ".intercalate missing}{assignErrorsMsg}{requiredErrorsMsg}{missingFieldsHint}" @@ -926,7 +926,7 @@ where let flatCtorName := mkFlatCtorOfStructCtorName ctor.name let cinfo ← getConstInfo flatCtorName let ctorVal ← instantiateValueLevelParams cinfo us - let fieldArgs := parentFields.map fieldMap.find! + let fieldArgs := parentFields.map (fieldMap.get! ·) -- Normalize the expressions since there might be some projections. let params ← params.mapM normalizeExpr let e' := (ctorVal.beta params).beta fieldArgs @@ -1016,7 +1016,7 @@ private def processField (loop : StructInstM α) (field : ExpandedField) (fieldT else throw ex loop - if let some fvarId' := (← get).liftedFVarRemap.find? fvarId then + if let some fvarId' := (← get).liftedFVarRemap.get? fvarId then processProjAux fvarId' else if (← getLCtx).contains fvarId then processProjAux fvarId diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 9220ec5d1c..0de1fb587e 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -450,7 +450,7 @@ private def hasFieldName (fieldName : Name) : StructElabM Bool := private def findFieldInfoByFVarId? (fvarId : FVarId) : StructElabM (Option StructFieldInfo) := do let s ← get - return s.fvarIdFieldIdx.find? fvarId |>.map fun idx => s.fields[idx]! + return s.fvarIdFieldIdx.get? fvarId |>.map fun idx => s.fields[idx]! /-- Inserts a field info into the current state. @@ -1242,7 +1242,7 @@ private def resolveFieldDefaults (structName : Name) : StructElabM Unit := do if fieldInfo.default?.isSome then replaceFieldInfo { fieldInfo with resolvedDefault? := fieldInfo.default? } else if !fieldInfo.inheritedDefaults.isEmpty then - let inheritedDefaults := fieldInfo.inheritedDefaults.insertionSort fun d1 d2 => resOrderMap.find! d1.1 < resOrderMap.find! d2.1 + let inheritedDefaults := fieldInfo.inheritedDefaults.insertionSort fun d1 d2 => resOrderMap.get! d1.1 < resOrderMap.get! d2.1 trace[Elab.structure] "inherited defaults for '{fieldInfo.name}' are {repr inheritedDefaults}" replaceFieldInfo { fieldInfo with inheritedDefaults diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean index 91cf98da35..97ad83686a 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean @@ -37,7 +37,7 @@ expression - pair values. def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Array (Bool × Nat)) (aigSize : Nat) (atomsAssignment : Std.HashMap Nat (Nat × Expr × Bool)) : Array (Expr × BVExpr.PackedBitVec) := Id.run do - let mut sparseMap : Std.HashMap Nat (RBMap Nat Bool Ord.compare) := {} + let mut sparseMap : Std.HashMap Nat (Std.TreeMap Nat Bool) := {} let filter bvBit _ := let (_, _, synthetic) := atomsAssignment[bvBit.var]! !synthetic diff --git a/src/Lean/Elab/Tactic/Doc.lean b/src/Lean/Elab/Tactic/Doc.lean index 373a7ddfe4..2584af415b 100644 --- a/src/Lean/Elab/Tactic/Doc.lean +++ b/src/Lean/Elab/Tactic/Doc.lean @@ -82,7 +82,7 @@ private def showParserName (n : Name) : MetaM MessageData := do pure <| .ofFormatWithInfos { fmt := "'" ++ .tag 0 tok ++ "'", infos := - .fromList [(0, .ofTermInfo { + .ofList [(0, .ofTermInfo { lctx := .empty, expr := .const n params, stx := .ident .none (toString n).toSubstring n [.decl n []], @@ -102,7 +102,7 @@ Displays all available tactic tags, with documentation. let mut mapping : NameMap NameSet := {} for arr in all do for (tac, tag) in arr do - mapping := mapping.insert tag (mapping.findD tag {} |>.insert tac) + mapping := mapping.insert tag (mapping.getD tag {} |>.insert tac) let showDocs : Option String → MessageData | none => .nil @@ -152,7 +152,7 @@ def allTacticDocs : MetaM (Array TacticDoc) := do let mut tacTags : NameMap NameSet := {} for arr in all do for (tac, tag) in arr do - tacTags := tacTags.insert tac (tacTags.findD tac {} |>.insert tag) + tacTags := tacTags.insert tac (tacTags.getD tac {} |>.insert tag) let mut docs := #[] @@ -171,7 +171,7 @@ def allTacticDocs : MetaM (Array TacticDoc) := do docs := docs.push { internalName := tac, userName := userName, - tags := tacTags.findD tac {}, + tags := tacTags.getD tac {}, docString := ← findDocString? env tac, extensionDocs := getTacticExtensions env tac } diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 19ca391cd4..67d4f6af79 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -815,7 +815,7 @@ where /-- Append the argument name (if available) to the message. Remark: if the argument name contains macro scopes we do not append it. -/ addArgName (msg : MessageData) (extra : String := "") : TermElabM MessageData := do - match (← get).mvarArgNames.find? mvarErrorInfo.mvarId with + match (← get).mvarArgNames.get? mvarErrorInfo.mvarId with | none => return msg | some argName => return if argName.hasMacroScopes then msg else msg ++ extra ++ m!" '{argName}'" @@ -1269,7 +1269,7 @@ private def postponeElabTermCore (stx : Syntax) (expectedType? : Option Expr) : return mvar def getSyntheticMVarDecl? (mvarId : MVarId) : TermElabM (Option SyntheticMVarDecl) := - return (← get).syntheticMVars.find? mvarId + return (← get).syntheticMVars.get? mvarId register_builtin_option debug.byAsSorry : Bool := { defValue := false diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index 519c6cb26c..ce0adf9027 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -10,6 +10,7 @@ import Lean.Data.KVMap import Lean.Data.SMap import Lean.Level import Std.Data.HashSet.Basic +import Std.Data.TreeSet.Basic namespace Lean @@ -214,17 +215,23 @@ instance : Repr FVarId where /-- A set of unique free variable identifiers. -This is a persistent data structure implemented using red-black trees. -/ -def FVarIdSet := RBTree FVarId (Name.quickCmp ·.name ·.name) +This is a persistent data structure implemented using `Std.TreeSet`. -/ +def FVarIdSet := Std.TreeSet FVarId (Name.quickCmp ·.name ·.name) deriving Inhabited, EmptyCollection -instance : ForIn m FVarIdSet FVarId := inferInstanceAs (ForIn _ (RBTree ..) ..) +instance : ForIn m FVarIdSet FVarId := inferInstanceAs (ForIn _ (Std.TreeSet _ _) ..) def FVarIdSet.insert (s : FVarIdSet) (fvarId : FVarId) : FVarIdSet := - RBTree.insert s fvarId + Std.TreeSet.insert s fvarId def FVarIdSet.union (vs₁ vs₂ : FVarIdSet) : FVarIdSet := - vs₁.fold (init := vs₂) (·.insert ·) + vs₁.foldl (init := vs₂) (·.insert ·) + +def FVarIdSet.ofList (l : List FVarId) : FVarIdSet := + Std.TreeSet.ofList l _ + +def FVarIdSet.ofArray (l : Array FVarId) : FVarIdSet := + Std.TreeSet.ofArray l _ /-- A set of unique free variable identifiers implemented using hashtables. @@ -235,13 +242,13 @@ def FVarIdHashSet := Std.HashSet FVarId /-- A mapping from free variable identifiers to values of type `α`. -This is a persistent data structure implemented using red-black trees. -/ -def FVarIdMap (α : Type) := RBMap FVarId α (Name.quickCmp ·.name ·.name) +This is a persistent data structure implemented using `Std.TreeMap`. -/ +def FVarIdMap (α : Type) := Std.TreeMap FVarId α (Name.quickCmp ·.name ·.name) def FVarIdMap.insert (s : FVarIdMap α) (fvarId : FVarId) (a : α) : FVarIdMap α := - RBMap.insert s fvarId a + Std.TreeMap.insert s fvarId a -instance : EmptyCollection (FVarIdMap α) := inferInstanceAs (EmptyCollection (RBMap ..)) +instance : EmptyCollection (FVarIdMap α) := inferInstanceAs (EmptyCollection (Std.TreeMap _ _ _)) instance : Inhabited (FVarIdMap α) where default := {} @@ -254,22 +261,28 @@ structure MVarId where instance : Repr MVarId where reprPrec n p := reprPrec n.name p -def MVarIdSet := RBTree MVarId (Name.quickCmp ·.name ·.name) +def MVarIdSet := Std.TreeSet MVarId (Name.quickCmp ·.name ·.name) deriving Inhabited, EmptyCollection def MVarIdSet.insert (s : MVarIdSet) (mvarId : MVarId) : MVarIdSet := - RBTree.insert s mvarId + Std.TreeSet.insert s mvarId -instance : ForIn m MVarIdSet MVarId := inferInstanceAs (ForIn _ (RBTree ..) ..) +def MVarIdSet.ofList (l : List MVarId) : MVarIdSet := + Std.TreeSet.ofList l _ -def MVarIdMap (α : Type) := RBMap MVarId α (Name.quickCmp ·.name ·.name) +def MVarIdSet.ofArray (l : Array MVarId) : MVarIdSet := + Std.TreeSet.ofArray l _ + +instance : ForIn m MVarIdSet MVarId := inferInstanceAs (ForIn _ (Std.TreeSet _ _) ..) + +def MVarIdMap (α : Type) := Std.TreeMap MVarId α (Name.quickCmp ·.name ·.name) def MVarIdMap.insert (s : MVarIdMap α) (mvarId : MVarId) (a : α) : MVarIdMap α := - RBMap.insert s mvarId a + Std.TreeMap.insert s mvarId a -instance : EmptyCollection (MVarIdMap α) := inferInstanceAs (EmptyCollection (RBMap ..)) +instance : EmptyCollection (MVarIdMap α) := inferInstanceAs (EmptyCollection (Std.TreeMap _ _ _)) -instance : ForIn m (MVarIdMap α) (MVarId × α) := inferInstanceAs (ForIn _ (RBMap ..) ..) +instance : ForIn m (MVarIdMap α) (MVarId × α) := inferInstanceAs (ForIn _ (Std.TreeMap _ _ _) ..) instance : Inhabited (MVarIdMap α) where default := {} diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean index a8223104b1..158559db64 100644 --- a/src/Lean/Level.lean +++ b/src/Lean/Level.lean @@ -11,6 +11,7 @@ import Lean.Hygiene import Lean.Data.Name import Lean.Data.Format import Init.Data.Option.Coe +import Std.Data.TreeSet.Basic def Nat.imax (n m : Nat) : Nat := if m = 0 then 0 else Nat.max n m @@ -70,16 +71,16 @@ abbrev LMVarId := LevelMVarId instance : Repr LMVarId where reprPrec n p := reprPrec n.name p -def LMVarIdSet := RBTree LMVarId (Name.quickCmp ·.name ·.name) +def LMVarIdSet := Std.TreeSet LMVarId (Name.quickCmp ·.name ·.name) deriving Inhabited, EmptyCollection -instance : ForIn m LMVarIdSet LMVarId := inferInstanceAs (ForIn _ (RBTree ..) ..) +instance : ForIn m LMVarIdSet LMVarId := inferInstanceAs (ForIn _ (Std.TreeSet _ _) ..) -def LMVarIdMap (α : Type) := RBMap LMVarId α (Name.quickCmp ·.name ·.name) +def LMVarIdMap (α : Type) := Std.TreeMap LMVarId α (Name.quickCmp ·.name ·.name) -instance : EmptyCollection (LMVarIdMap α) := inferInstanceAs (EmptyCollection (RBMap ..)) +instance : EmptyCollection (LMVarIdMap α) := inferInstanceAs (EmptyCollection (Std.TreeMap _ _ _)) -instance : ForIn m (LMVarIdMap α) (LMVarId × α) := inferInstanceAs (ForIn _ (RBMap ..) ..) +instance : ForIn m (LMVarIdMap α) (LMVarId × α) := inferInstanceAs (ForIn _ (Std.TreeMap _ _ _) ..) instance : Inhabited (LMVarIdMap α) where default := {} diff --git a/src/Lean/Linter/Basic.lean b/src/Lean/Linter/Basic.lean index 3ebb4334f6..041a21d90e 100644 --- a/src/Lean/Linter/Basic.lean +++ b/src/Lean/Linter/Basic.lean @@ -22,8 +22,8 @@ def LinterSets := NameMap (Array Name) `entry.2` contains the names of the set's linter options. -/ def insertLinterSetEntry (map : LinterSets) (setName : Name) (options : NameSet) : LinterSets := - options.fold (init := map) fun map linterName => - map.insert linterName ((map.findD linterName #[]).push setName) + options.foldl (init := map) fun map linterName => + map.insert linterName ((map.getD linterName #[]).push setName) builtin_initialize linterSetsExt : SimplePersistentEnvExtension (Name × NameSet) LinterSets ← Lean.registerSimplePersistentEnvExtension { addImportedFn := mkStateFromImportedEntries (Function.uncurry <| insertLinterSetEntry ·) {} @@ -52,7 +52,7 @@ def _root_.Lean.Options.toLinterOptions [Monad m] [MonadEnv m] (o : Options) : m /-- Return the set of linter sets that this option is contained in. -/ def LinterOptions.getSet (o : LinterOptions) (opt : Lean.Option α) : Array Name := - o.linterSets.findD opt.name #[] + o.linterSets.getD opt.name #[] def getLinterOptions [Monad m] [MonadOptions m] [MonadEnv m] : m LinterOptions := do (← getOptions).toLinterOptions diff --git a/src/Lean/Log.lean b/src/Lean/Log.lean index 9147c3e175..a8083c6536 100644 --- a/src/Lean/Log.lean +++ b/src/Lean/Log.lean @@ -11,6 +11,7 @@ import Lean.DocString.Links -- This import is necessary to ensure that any users of the `logNamedError` macros have access to -- all declared explanations: import Lean.ErrorExplanations +import Lean.Data.Json.Basic namespace Lean @@ -91,10 +92,10 @@ private def MessageData.appendDescriptionWidgetIfNamed (msg : MessageData) : Mes let inst := { id := ``errorDescriptionWidget javascriptHash := errorDescriptionWidget.javascriptHash - props := return json% { - code: $(toString errorName), - explanationUrl: $url - } + props := return Json.mkObj [ + ("code", toString errorName), + ("explanationUrl", url) + ] } -- Note: we do not generate corresponding message data for the widget because it pollutes -- console output diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index e74a3ea6f0..3ea3a8120b 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -570,7 +570,7 @@ def add (msg : Message) (log : MessageLog) : MessageLog := protected def append (l₁ l₂ : MessageLog) : MessageLog where reported := l₁.reported ++ l₂.reported unreported := l₁.unreported ++ l₂.unreported - loggedKinds := l₁.loggedKinds.union l₂.loggedKinds + loggedKinds := l₁.loggedKinds.merge l₂.loggedKinds instance : Append MessageLog := ⟨MessageLog.append⟩ diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean index 1c807ae81a..23c8d17472 100644 --- a/src/Lean/Meta/Instances.lean +++ b/src/Lean/Meta/Instances.lean @@ -286,7 +286,7 @@ structure DefaultInstanceEntry where instanceName : Name priority : Nat -abbrev PrioritySet := RBTree Nat (fun x y => compare y x) +abbrev PrioritySet := Std.TreeSet Nat (fun x y => compare y x) structure DefaultInstances where defaultInstances : NameMap (List (Name × Nat)) := {} diff --git a/src/Lean/Meta/Match/MVarRenaming.lean b/src/Lean/Meta/Match/MVarRenaming.lean index f177c8dc87..9b64027329 100644 --- a/src/Lean/Meta/Match/MVarRenaming.lean +++ b/src/Lean/Meta/Match/MVarRenaming.lean @@ -16,7 +16,7 @@ def MVarRenaming.isEmpty (s : MVarRenaming) : Bool := s.map.isEmpty def MVarRenaming.find? (s : MVarRenaming) (mvarId : MVarId) : Option MVarId := - s.map.find? mvarId + s.map.get? mvarId def MVarRenaming.find! (s : MVarRenaming) (mvarId : MVarId) : MVarId := (s.find? mvarId).get! @@ -28,7 +28,7 @@ def MVarRenaming.apply (s : MVarRenaming) (e : Expr) : Expr := if !e.hasMVar then e else if s.map.isEmpty then e else e.replace fun e => match e with - | Expr.mvar mvarId => match s.map.find? mvarId with + | Expr.mvar mvarId => match s.map.get? mvarId with | none => e | some newMVarId => mkMVar newMVarId | _ => none diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean index 1fcbed0184..9098eba3df 100644 --- a/src/Lean/Meta/Match/MatchEqs.lean +++ b/src/Lean/Meta/Match/MatchEqs.lean @@ -574,7 +574,7 @@ where for i in 6...args.size do let arg := argsNew[i]! if arg.isFVar then - match (← read).find? arg.fvarId! with + match (← read).get? arg.fvarId! with | some (altNew, _, _) => argsNew := argsNew.set! i altNew trace[Meta.Match.matchEqs] "arg: {arg} : {← inferType arg}, altNew: {altNew} : {← inferType altNew}" @@ -635,7 +635,7 @@ where if isAlt[i] then -- `convertTemplate` will correct occurrences of the alternative let alt := args[6+i]! -- Recall that `Eq.ndrec` has 6 arguments - let some (_, numParams, argMask) := m.find? alt.fvarId! | unreachable! + let some (_, numParams, argMask) := m.get? alt.fvarId! | unreachable! -- We add a new entry to `m` to make sure `convertTemplate` will correct the occurrences of the alternative m := m.insert minorArgsNew[i]!.fvarId! (minorArgsNew[i]!, numParams, argMask) unless minorBodyNew.isLambda do @@ -659,7 +659,7 @@ where return .done (← convertCastEqRec e) else let Expr.fvar fvarId .. := e.getAppFn | return .continue - let some (altNew, numParams, argMask) := (← read).find? fvarId | return .continue + let some (altNew, numParams, argMask) := (← read).get? fvarId | return .continue trace[Meta.Match.matchEqs] ">> argMask: {argMask}, e: {e}, {altNew}" let mut newArgs := #[] let argMask := trimFalseTrail argMask diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean index c2fd140749..ab7902cc12 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean @@ -6,7 +6,6 @@ Authors: Leonardo de Moura prelude import Init.Grind.Ring.OfSemiring import Lean.Data.PersistentArray -import Lean.Data.RBTree import Lean.Meta.Tactic.Grind.ExprPtr import Lean.Meta.Tactic.Grind.Arith.Util import Lean.Meta.Tactic.Grind.Arith.CommRing.Poly @@ -45,7 +44,7 @@ protected def EqCnstr.compare (c₁ c₂ : EqCnstr) : Ordering := (compare c₁.p.degree c₂.p.degree) |>.then (compare c₁.id c₂.id) -abbrev Queue : Type := RBTree EqCnstr EqCnstr.compare +abbrev Queue : Type := Std.TreeSet EqCnstr EqCnstr.compare /-- A polynomial equipped with a chain of rewrite steps that justifies its equality to the original input. diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean index 570deac995..28a9cbc756 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean @@ -204,7 +204,7 @@ def isQueueEmpty : RingM Bool := return (← getRing).queue.isEmpty def getNext? : RingM (Option EqCnstr) := do - let some c := (← getRing).queue.min | return none + let some c := (← getRing).queue.min? | return none modifyRing fun s => { s with queue := s.queue.erase c } incSteps return some c diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean index 79eb02be55..efe4b59c60 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean @@ -488,7 +488,7 @@ def resolveConflict (h : UnsatProof) : SearchM Unit := do trace[grind.debug.cutsat.search.backtrack] "resolved diseq split: {← c'.pp}" c'.assert | .cooper pred hs decVars' => - let decVars' := decVars.union decVars' + let decVars' := decVars.merge decVars' let n := pred.numCases let hs := hs.push (c.fvarId, h) trace[grind.debug.cutsat.search.backtrack] "cooper #{hs.size + 1}, {← pred.pp}, {hs.map fun p => p.1.name}" diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean index e0658b8a5d..9e98002941 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean @@ -232,7 +232,7 @@ instance : Inhabited CooperSplitPred where instance : Inhabited CooperSplit where default := { pred := default, k := 0, h := .dec default } -abbrev VarSet := RBTree Var compare +abbrev VarSet := Std.TreeSet Var /-- State of the cutsat procedure. -/ structure State where diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean index c7eac91941..5786efb2a2 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean @@ -77,7 +77,7 @@ instance : Inhabited DiseqCnstr where instance : Inhabited EqCnstr where default := { p := .nil, h := .core default default .zero .zero } -abbrev VarSet := RBTree Var compare +abbrev VarSet := Std.TreeSet Var /-- State for each algebraic structure by this module. diff --git a/src/Lean/Meta/Tactic/Grind/Cases.lean b/src/Lean/Meta/Tactic/Grind/Cases.lean index bd256d9201..eeed6cd9e5 100644 --- a/src/Lean/Meta/Tactic/Grind/Cases.lean +++ b/src/Lean/Meta/Tactic/Grind/Cases.lean @@ -23,7 +23,7 @@ structure CasesEntry where The goal is to reduce noise in the tactic generated by `grind?` -/ private def builtinEagerCases : NameSet := - RBTree.ofList [``And, ``Exists, ``True, ``False, ``Unit, ``Empty] + .ofList [``And, ``Exists, ``True, ``False, ``Unit, ``Empty] /-- Returns `true` if `declName` is the name of inductive type/predicate that diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean index a0a72ccac8..21c9dda3c3 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean @@ -784,21 +784,21 @@ private def checkCoverage (thmProof : Expr) (numParams : Nat) (bvarsFound : Std. assert! numParams == xs.size let patternVars := bvarsFound.toList.map fun bidx => xs[numParams - bidx - 1]!.fvarId! -- `xs` as a `FVarIdSet`. - let thmVars : FVarIdSet := RBTree.ofList <| xs.toList.map (·.fvarId!) + let thmVars := FVarIdSet.ofList <| xs.toList.map (·.fvarId!) -- Collect free variables occurring in `e`, and insert the ones that are in `thmVars` into `fvarsFound` let update (fvarsFound : FVarIdSet) (e : Expr) : FVarIdSet := (collectFVars {} e).fvarIds.foldl (init := fvarsFound) fun s fvarId => if thmVars.contains fvarId then s.insert fvarId else s -- Theorem variables found so far. We initialize with the variables occurring in patterns -- Remark: fvarsFound is a subset of thmVars - let mut fvarsFound : FVarIdSet := RBTree.ofList patternVars + let mut fvarsFound := FVarIdSet.ofList patternVars for patternVar in patternVars do let type ← patternVar.getType fvarsFound := update fvarsFound type if fvarsFound.size == numParams then return .ok -- Now, we keep traversing remaining variables and collecting -- `processed` contains the variables we have already processed. - let mut processed : FVarIdSet := RBTree.ofList patternVars + let mut processed := FVarIdSet.ofList patternVars let mut modified := false repeat modified := false diff --git a/src/Lean/Meta/Tactic/Grind/Proof.lean b/src/Lean/Meta/Tactic/Grind/Proof.lean index 3a53685f7b..4953e02a95 100644 --- a/src/Lean/Meta/Tactic/Grind/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Proof.lean @@ -68,7 +68,7 @@ Recall that this expression must exist since it is the root itself in the worst case. -/ private def findCommon (lhs rhs : Expr) : GoalM Expr := do - let mut visited : RBMap Nat Expr compare := {} + let mut visited : Std.TreeMap Nat Expr := {} let mut it := lhs -- Mark elements found following the path from `lhs` to the root. repeat @@ -80,7 +80,7 @@ private def findCommon (lhs rhs : Expr) : GoalM Expr := do it := rhs repeat let n ← getENode it - if let some common := visited.find? n.idx then + if let some common := visited.get? n.idx then return common let some target := n.target? | unreachable! -- it := target diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index 84a041f9c7..19d4c0ba0c 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -6,7 +6,7 @@ Authors: Leonardo de Moura prelude import Init.Grind.Tactics import Init.Data.Queue -import Std.Data.TreeSet +import Std.Data.TreeSet.Basic import Lean.HeadIndex import Lean.Meta.Basic import Lean.Meta.CongrTheorems diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index 19efe01407..40e92aec11 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -848,7 +848,7 @@ ones that allow zeta-delta reducing fvars not in `zetaDeltaSet` (e.g. `withInfer This also means that `usedZetaDelta` set might be reporting fvars in `zetaDeltaSet` that weren't "used". -/ private def updateUsedSimpsWithZetaDeltaCore (s : UsedSimps) (zetaDeltaSet : FVarIdSet) (usedZetaDelta : FVarIdSet) : UsedSimps := - zetaDeltaSet.fold (init := s) fun s fvarId => + zetaDeltaSet.foldl (init := s) fun s fvarId => if usedZetaDelta.contains fvarId then s.insert <| .fvar fvarId else diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean index c40f118147..d1c539a5e0 100644 --- a/src/Lean/MetavarContext.lean +++ b/src/Lean/MetavarContext.lean @@ -606,7 +606,7 @@ def instantiateLCtxMVars [Monad m] [MonadMCtx m] (lctx : LocalContext) : m Local match ldecl with | .cdecl _ fvarId userName type _ .auxDecl => let type ← instantiateMVars type - let .some fullName := auxDeclToFullName.find? fvarId + let .some fullName := auxDeclToFullName.get? fvarId | panic! s!"Invalid auxiliary declaration found in local context: \ {userName} does not have an associated full name." return lctx.mkAuxDecl fvarId userName type fullName diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index d451f501c5..cd4bd561ce 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -1581,21 +1581,21 @@ def eoi : Parser := { } /-- A multimap indexed by tokens. Used for indexing parsers by their leading token. -/ -def TokenMap (α : Type) := RBMap Name (List α) Name.quickCmp +def TokenMap (α : Type) := Std.TreeMap Name (List α) Name.quickCmp namespace TokenMap def insert (map : TokenMap α) (k : Name) (v : α) : TokenMap α := - match map.find? k with - | none => RBMap.insert map k [v] - | some vs => RBMap.insert map k (v::vs) + match map.get? k with + | none => Std.TreeMap.insert map k [v] + | some vs => Std.TreeMap.insert map k (v::vs) instance : Inhabited (TokenMap α) where - default := RBMap.empty + default := Std.TreeMap.empty -instance : EmptyCollection (TokenMap α) := ⟨RBMap.empty⟩ +instance : EmptyCollection (TokenMap α) := ⟨Std.TreeMap.empty⟩ -instance : ForIn m (TokenMap α) (Name × List α) := inferInstanceAs (ForIn _ (RBMap ..) _) +instance : ForIn m (TokenMap α) (Name × List α) := inferInstanceAs (ForIn _ (Std.TreeMap _ _ _) _) end TokenMap @@ -1680,7 +1680,7 @@ abbrev ParserCategories := PersistentHashMap Name ParserCategory def indexed {α : Type} (map : TokenMap α) (c : ParserContext) (s : ParserState) (behavior : LeadingIdentBehavior) : ParserState × List α := let (s, stx) := peekToken c s let find (n : Name) : ParserState × List α := - match map.find? n with + match map.get? n with | some as => (s, as) | _ => (s, []) match stx with @@ -1689,16 +1689,16 @@ def indexed {α : Type} (map : TokenMap α) (c : ParserContext) (s : ParserState match behavior with | .default => find identKind | .symbol => - match map.find? val with + match map.get? val with | some as => (s, as) | none => find identKind | .both => - match map.find? val with + match map.get? val with | some as => if val == identKind then (s, as) -- avoid running the same parsers twice else - match map.find? identKind with + match map.get? identKind with | some as' => (s, as ++ as') | _ => (s, as) | none => find identKind diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 78965aaca8..2b691d5505 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -218,7 +218,7 @@ builtin_initialize parserAlias2kindRef : IO.Ref (NameMap SyntaxNodeKind) ← IO. builtin_initialize parserAliases2infoRef : IO.Ref (NameMap ParserAliasInfo) ← IO.mkRef {} def getParserAliasInfo (aliasName : Name) : IO ParserAliasInfo := do - return (← parserAliases2infoRef.get).findD aliasName {} + return (← parserAliases2infoRef.get).getD aliasName {} -- Later, we define macro `register_parser_alias` which registers a parser, formatter and parenthesizer def registerAlias (aliasName declName : Name) (p : ParserAliasValue) (kind? : Option SyntaxNodeKind := none) (info : ParserAliasInfo := {}) : IO Unit := do diff --git a/src/Lean/Parser/Tactic/Doc.lean b/src/Lean/Parser/Tactic/Doc.lean index 8b4d25cd07..1f0e8639f3 100644 --- a/src/Lean/Parser/Tactic/Doc.lean +++ b/src/Lean/Parser/Tactic/Doc.lean @@ -36,7 +36,7 @@ builtin_initialize tacticAlternativeExt addImportedFn := fun _ => pure {}, addEntryFn := fun as (src, tgt) => as.insert src tgt, exportEntriesFn := fun es => - es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1) + es.foldl (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1) } /-- @@ -114,7 +114,7 @@ builtin_initialize knownTacticTagExt addImportedFn := fun _ => pure {}, addEntryFn := fun as (src, tgt) => as.insert src tgt, exportEntriesFn := fun es => - es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1) + es.foldl (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1) } /-- @@ -149,7 +149,7 @@ def allTagsWithInfo [Monad m] [MonadEnv m] : m (List (Name × String × Option S for arr in knownTacticTagExt.toEnvExtension.getState env |>.importedEntries do for (tag, info) in arr do found := found.insert tag info - let arr := found.fold (init := #[]) (fun arr k v => arr.push (k, v)) + let arr := found.foldl (init := #[]) (fun arr k v => arr.push (k, v)) pure (arr.qsort (·.1.toString < ·.1.toString) |>.toList) /-- @@ -167,7 +167,7 @@ builtin_initialize tacticTagExt registerPersistentEnvExtension { mkInitial := pure {}, addImportedFn := fun _ => pure {}, - addEntryFn := fun tags (decl, newTag) => tags.insert decl (tags.findD decl {} |>.insert newTag) + addEntryFn := fun tags (decl, newTag) => tags.insert decl (tags.getD decl {} |>.insert newTag) exportEntriesFn := fun tags => Id.run do let mut exported := #[] for (decl, dTags) in tags do @@ -234,9 +234,9 @@ builtin_initialize tacticDocExtExt registerPersistentEnvExtension { mkInitial := pure {}, addImportedFn := fun _ => pure {}, - addEntryFn := fun es (x, ext) => es.insert x (es.findD x #[] |>.push ext), + addEntryFn := fun es (x, ext) => es.insert x (es.getD x #[] |>.push ext), exportEntriesFn := fun es => - es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1) + es.foldl (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1) } /-- Gets the extensions declared for the documentation for the given canonical tactic name -/ diff --git a/src/Lean/Parser/Term/Doc.lean b/src/Lean/Parser/Term/Doc.lean index d4305fdd27..13ceb1cf6f 100644 --- a/src/Lean/Parser/Term/Doc.lean +++ b/src/Lean/Parser/Term/Doc.lean @@ -31,9 +31,9 @@ builtin_initialize recommendedSpellingByNameExt registerPersistentEnvExtension { mkInitial := pure {}, addImportedFn := fun _ => pure {}, - addEntryFn := fun es (rec, xs) => xs.foldl (init := es) fun es x => es.insert x (es.findD x #[] |>.push rec), + addEntryFn := fun es (rec, xs) => xs.foldl (init := es) fun es x => es.insert x (es.getD x #[] |>.push rec), exportEntriesFn := fun es => - es.fold (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1) + es.foldl (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1) } /-- Recommended spellings for notations, stored in such a way that it is easy to generate a table diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean index 44bd3e6354..33892f6d30 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean @@ -165,7 +165,7 @@ def getExprKind : DelabM Name := do def getOptionsAtCurrPos : DelabM Options := do let ctx ← read let mut opts ← getOptions - if let some opts' := ctx.optionsPerPos.find? (← getPos) then + if let some opts' := ctx.optionsPerPos.get? (← getPos) then for (k, v) in opts' do opts := opts.insert k v return opts @@ -187,7 +187,7 @@ def withOptionAtCurrPos (k : Name) (v : DataValue) (x : DelabM α) : DelabM α : let pos ← getPos withReader (fun ctx => - let opts' := ctx.optionsPerPos.find? pos |>.getD {} |>.insert k v + let opts' := ctx.optionsPerPos.get? pos |>.getD {} |>.insert k v { ctx with optionsPerPos := ctx.optionsPerPos.insert pos opts' }) x diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index a672eae2f1..ddf03dbd3d 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -136,7 +136,7 @@ def withMDataOptions [Inhabited α] (x : DelabM α) : DelabM α := do let pos ← getPos for (k, v) in m do if (`pp).isPrefixOf k then - let opts := posOpts.find? pos |>.getD {} + let opts := posOpts.get? pos |>.getD {} posOpts := posOpts.insert pos (opts.insert k v) withReader ({ · with optionsPerPos := posOpts }) $ withMDataExpr x | _ => x @@ -588,7 +588,7 @@ private partial def collectStructFields unless ← getPPOption getPPStructureInstancesDefaults do if let some defFn := getEffectiveDefaultFnForField? (← getEnv) structName fieldName then -- Use `withNewMCtxDepth` to prevent delaborator from solving metavariables. - if let some (_, defValue) ← withNewMCtxDepth <| instantiateStructDefaultValueFn? defFn levels params (pure ∘ fieldValues.find?) then + if let some (_, defValue) ← withNewMCtxDepth <| instantiateStructDefaultValueFn? defFn levels params (pure ∘ fieldValues.get?) then if ← withReducible <| withNewMCtxDepth <| isDefEq defValue (← getExpr) then -- Default value matches, skip the field. return (i + 1, fieldValues, fields) diff --git a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean index 09f49b2696..9aedf5c2d2 100644 --- a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean +++ b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean @@ -6,7 +6,6 @@ Authors: Sebastian Ullrich, Daniel Selsam, Wojciech Nawrocki prelude import Lean.Meta.Basic import Lean.SubExpr -import Lean.Data.RBMap /-! # Subexpr utilities for delaborator. @@ -16,15 +15,15 @@ in sync with the `Nat` "position" values that refer to them. namespace Lean.PrettyPrinter.Delaborator -abbrev OptionsPerPos := RBMap SubExpr.Pos Options compare +abbrev OptionsPerPos := Std.TreeMap SubExpr.Pos Options def OptionsPerPos.insertAt (optionsPerPos : OptionsPerPos) (pos : SubExpr.Pos) (name : Name) (value : DataValue) : OptionsPerPos := - let opts := optionsPerPos.find? pos |>.getD {} + let opts := optionsPerPos.get? pos |>.getD {} optionsPerPos.insert pos <| opts.insert name value /-- Merges two collections of options, where the second overrides the first. -/ def OptionsPerPos.merge : OptionsPerPos → OptionsPerPos → OptionsPerPos := - RBMap.mergeBy (fun _ => KVMap.mergeBy (fun _ _ dv => dv)) + Std.TreeMap.mergeWith (fun _ => KVMap.mergeBy (fun _ _ dv => dv)) namespace SubExpr diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean index 028905a205..c06ab54c89 100644 --- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Daniel Selsam -/ prelude -import Lean.Data.RBMap import Lean.Meta.SynthInstance import Lean.Meta.CtorRecognizer import Lean.Util.FindMVar @@ -328,7 +327,7 @@ def checkKnowsType : AnalyzeM Unit := do throw $ Exception.internal analyzeFailureId def annotateBoolAt (n : Name) (pos : Pos) : AnalyzeM Unit := do - let opts := (← get).annotations.findD pos {} |>.setBool n true + let opts := (← get).annotations.getD pos {} |>.setBool n true trace[pp.analyze.annotate] "{pos} {n}" modify fun s => { s with annotations := s.annotations.insert pos opts } diff --git a/src/Lean/ReducibilityAttrs.lean b/src/Lean/ReducibilityAttrs.lean index 381d47b80b..0313bcb1fb 100644 --- a/src/Lean/ReducibilityAttrs.lean +++ b/src/Lean/ReducibilityAttrs.lean @@ -28,7 +28,7 @@ builtin_initialize reducibilityCoreExt : PersistentEnvExtension (Name × Reducib addImportedFn := fun _ _ => pure {} addEntryFn := fun (s : NameMap ReducibilityStatus) (p : Name × ReducibilityStatus) => s.insert p.1 p.2 exportEntriesFn := fun m => - let r : Array (Name × ReducibilityStatus) := m.fold (fun a n p => a.push (n, p)) #[] + let r : Array (Name × ReducibilityStatus) := m.foldl (fun a n p => a.push (n, p)) #[] r.qsort (fun a b => Name.quickLt a.1 b.1) statsFn := fun s => "reducibility attribute core extension" ++ Format.line ++ "number of local entries: " ++ format s.size asyncMode := .async diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean index 9024a4fc68..634bfe7fd7 100644 --- a/src/Lean/ResolveName.lean +++ b/src/Lean/ResolveName.lean @@ -502,7 +502,7 @@ def resolveLocalName [Monad m] [MonadResolveName m] [MonadEnv m] [MonadLCtx m] ( let localDecl ← localDecl? if localDecl.isAuxDecl then guard (!skipAuxDecl) - if let some fullDeclName := auxDeclToFullName.find? localDecl.fvarId then + if let some fullDeclName := auxDeclToFullName.get? localDecl.fvarId then matchAuxRecDecl? localDecl fullDeclName givenNameView else matchLocalDecl? localDecl givenName diff --git a/src/Lean/Server/CodeActions/Attr.lean b/src/Lean/Server/CodeActions/Attr.lean index 231751893d..e59345b66f 100644 --- a/src/Lean/Server/CodeActions/Attr.lean +++ b/src/Lean/Server/CodeActions/Attr.lean @@ -90,7 +90,7 @@ def CommandCodeActions.insert (self : CommandCodeActions) { self with onAnyCmd := self.onAnyCmd.push action } else { self with onCmd := tacticKinds.foldl (init := self.onCmd) fun m a => - m.insert a ((m.findD a #[]).push action) } + m.insert a ((m.getD a #[]).push action) } builtin_initialize builtinCmdCodeActions : IO.Ref CommandCodeActions ← IO.mkRef {} diff --git a/src/Lean/Server/Completion/CompletionCollectors.lean b/src/Lean/Server/Completion/CompletionCollectors.lean index f7aa554038..b4aad7599e 100644 --- a/src/Lean/Server/Completion/CompletionCollectors.lean +++ b/src/Lean/Server/Completion/CompletionCollectors.lean @@ -314,7 +314,7 @@ section DotCompletionUtils strip the private prefix from deep in the name, letting us reject most names without having to scan the full name first. -/ - private def NameSetModPrivate := RBTree Name cmpModPrivate + private def NameSetModPrivate := Std.TreeSet Name cmpModPrivate /-- Given a type, try to extract relevant type names for dot notation field completion. @@ -427,7 +427,7 @@ def dotCompletion let nameSet ← try getDotCompletionTypeNameSet (← instantiateMVars (← inferType info.expr)) catch _ => - pure RBTree.empty + pure Std.TreeSet.empty if nameSet.isEmpty then return @@ -462,7 +462,7 @@ def dotIdCompletion let nameSet ← try getDotCompletionTypeNameSet resultTypeFn catch _ => - pure RBTree.empty + pure Std.TreeSet.empty forEligibleDeclsWithCancellationM fun declName c => do let unnormedTypeName := declName.getPrefix @@ -545,7 +545,7 @@ def optionCompletion : IO (Array CompletionItem) := ctx.runMetaM {} do -- HACK(WN): unfold the type so ForIn works - let (decls : RBMap _ _ _) ← getOptionDecls + let (decls : Std.TreeMap _ _ _) ← getOptionDecls let opts ← getOptions -- `stx` is from `"set_option " >> ident` return trailingDotCompletion decls stx[1] caps ctx fun name decl textEdit? => { diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index fdee62974f..5f4a7df95a 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -8,11 +8,10 @@ prelude import Init.System.IO import Std.Sync.Channel -import Lean.Data.RBMap import Lean.Environment import Lean.Data.Lsp -import Lean.Data.Json.FromToJson +import Lean.Data.Json.FromToJson.Basic import Lean.LoadDynlib import Lean.Language.Lean @@ -85,7 +84,7 @@ structure WorkerContext where Diagnostics that are included in every single `textDocument/publishDiagnostics` notification. -/ stickyDiagnosticsRef : IO.Ref (Array InteractiveDiagnostic) - partialHandlersRef : IO.Ref (RBMap String PartialHandlerInfo compare) + partialHandlersRef : IO.Ref (Std.TreeMap String PartialHandlerInfo) pendingServerRequestsRef : IO.Ref (Std.TreeMap RequestID (IO.Promise (ServerRequestResponse Json))) hLog : FS.Stream initParams : InitializeParams @@ -100,14 +99,14 @@ structure WorkerContext where def WorkerContext.modifyGetPartialHandler (ctx : WorkerContext) (method : String) (f : PartialHandlerInfo → α × PartialHandlerInfo) : BaseIO α := ctx.partialHandlersRef.modifyGet fun partialHandlers => Id.run do - let h := partialHandlers.find! method + let h := partialHandlers.get! method let (r, h) := f h (r, partialHandlers.insert method h) def WorkerContext.modifyPartialHandler (ctx : WorkerContext) (method : String) (f : PartialHandlerInfo → PartialHandlerInfo) : BaseIO Unit := ctx.partialHandlersRef.modify fun partialHandlers => Id.run do - let some h := partialHandlers.find? method + let some h := partialHandlers.get? method | return partialHandlers partialHandlers.insert method <| f h @@ -341,7 +340,7 @@ structure PendingRequest where cancelTk : RequestCancellationToken -- Pending requests are tracked so they can be canceled -abbrev PendingRequestMap := RBMap RequestID PendingRequest compare +abbrev PendingRequestMap := Std.TreeMap RequestID PendingRequest structure AvailableImportsCache where availableImports : ImportCompletion.AvailableImports @@ -355,7 +354,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 : RBMap UInt64 (IO.Ref RpcSession) compare + rpcSessions : Std.TreeMap UInt64 (IO.Ref RpcSession) abbrev WorkerM := ReaderT WorkerContext <| StateRefT WorkerState IO @@ -443,7 +442,7 @@ section Initialization let pendingServerRequestsRef ← IO.mkRef ∅ let chanOut ← mkLspOutputChannel maxDocVersionRef let timestamp ← IO.monoMsNow - let partialHandlersRef ← IO.mkRef <| RBMap.fromArray (cmp := compare) <| + let partialHandlersRef ← IO.mkRef <| Std.TreeMap.ofArray (cmp := compare) <| (← partialLspRequestHandlerMethods).map fun (method, refreshMethod, _) => (method, { refreshMethod @@ -480,8 +479,8 @@ section Initialization return (ctx, { doc := { doc with reporter } reporterCancelTk - pendingRequests := RBMap.empty - rpcSessions := RBMap.empty + pendingRequests := Std.TreeMap.empty + rpcSessions := Std.TreeMap.empty importCachingTask? := none }) where @@ -599,7 +598,7 @@ section NotificationHandling def handleCancelRequest (p : CancelParams) : WorkerM Unit := do let st ← get - let some r := st.pendingRequests.find? p.id + let some r := st.pendingRequests.get? p.id | return r.cancelTk.cancelByCancelRequest set <| { st with pendingRequests := st.pendingRequests.erase p.id } @@ -629,7 +628,7 @@ section NotificationHandling def handleRpcRelease (p : Lsp.RpcReleaseParams) : WorkerM Unit := do -- NOTE(WN): when the worker restarts e.g. due to changed imports, we may receive `rpc/release` -- for the previous RPC session. This is fine, just ignore. - if let some seshRef := (← get).rpcSessions.find? p.sessionId then + if let some seshRef := (← get).rpcSessions.get? p.sessionId then let monoMsNow ← IO.monoMsNow let discardRefs : StateM RpcObjectStore Unit := do for ref in p.refs do @@ -640,7 +639,7 @@ def handleRpcRelease (p : Lsp.RpcReleaseParams) : WorkerM Unit := do { st with objects } def handleRpcKeepAlive (p : Lsp.RpcKeepAliveParams) : WorkerM Unit := do - match (← get).rpcSessions.find? p.sessionId with + match (← get).rpcSessions.get? p.sessionId with | none => return | some seshRef => seshRef.modify (·.keptAlive (← IO.monoMsNow)) @@ -763,7 +762,7 @@ section MessageHandling let params ← RequestM.parseRequestParams Lsp.RpcCallParams params if params.method != `Lean.Widget.getInteractiveDiagnostics then return none - let some seshRef := st.rpcSessions.find? params.sessionId + let some seshRef := st.rpcSessions.get? params.sessionId | throw RequestError.rpcNeedsReconnect let params ← RequestM.parseRequestParams Widget.GetInteractiveDiagnosticsParams params.params let resp ← handleGetInteractiveDiagnosticsRequest ctx params @@ -914,7 +913,7 @@ section MainLoop throwServerError s!"Failed responding to request {id}: {e}" pure <| acc.erase id else pure acc - let pendingRequests ← st.pendingRequests.foldM (fun acc id r => filterFinishedTasks acc id r.requestTask) st.pendingRequests + let pendingRequests ← st.pendingRequests.foldlM (fun acc id r => filterFinishedTasks acc id r.requestTask) st.pendingRequests st := { st with pendingRequests } -- Opportunistically (i.e. when we wake up on messages) check if any RPC session has expired. diff --git a/src/Lean/Server/FileWorker/SemanticHighlighting.lean b/src/Lean/Server/FileWorker/SemanticHighlighting.lean index 9fca1502a3..664e8bb30b 100644 --- a/src/Lean/Server/FileWorker/SemanticHighlighting.lean +++ b/src/Lean/Server/FileWorker/SemanticHighlighting.lean @@ -25,8 +25,8 @@ def noHighlightKinds : Array SyntaxNodeKind := #[ -- TODO: make extensible, or don't /-- Keywords for which a specific semantic token is provided. -/ -def keywordSemanticTokenMap : RBMap String SemanticTokenType compare := - RBMap.empty +def keywordSemanticTokenMap : Std.TreeMap String SemanticTokenType := + Std.TreeMap.empty |>.insert "sorry" .leanSorryLike |>.insert "admit" .leanSorryLike |>.insert "stop" .leanSorryLike @@ -114,7 +114,7 @@ partial def collectSyntaxBasedSemanticTokens : (stx : Syntax) → Array LeanSema let isHashKeyword := val.length > 1 && val.front == '#' && isIdFirst (val.get ⟨1⟩) if ! isRegularKeyword && ! isHashKeyword then return tokens - return tokens.push ⟨stx, keywordSemanticTokenMap.findD val .keyword⟩ + return tokens.push ⟨stx, keywordSemanticTokenMap.getD val .keyword⟩ /-- Collects all semantic tokens from the given `Elab.InfoTree`. -/ def collectInfoBasedSemanticTokens (i : Elab.InfoTree) : Array LeanSemanticToken := diff --git a/src/Lean/Server/GoTo.lean b/src/Lean/Server/GoTo.lean index 0eece07562..72bdc17705 100644 --- a/src/Lean/Server/GoTo.lean +++ b/src/Lean/Server/GoTo.lean @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Ullrich, Lars König, Wojciech Nawrocki -/ prelude -import Lean.Data.Json.FromToJson +import Lean.Data.Json.FromToJson.Basic import Lean.Util.Path import Lean.Server.Utils diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean index 17a14d6ad0..7e48db8375 100644 --- a/src/Lean/Server/References.lean +++ b/src/Lean/Server/References.lean @@ -8,7 +8,6 @@ prelude import Lean.Data.Lsp.Internal import Lean.Data.Lsp.Extra import Lean.Server.Utils -import Std.Data.TreeMap import Lean.Elab.Import import Std.Data.TreeSet.Basic diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean index cf2878a5a8..13cc8ea228 100644 --- a/src/Lean/Server/Requests.lean +++ b/src/Lean/Server/Requests.lean @@ -7,7 +7,7 @@ Authors: Wojciech Nawrocki, Marc Huisinga prelude import Lean.DeclarationRange -import Lean.Data.Json +import Lean.Data.Json.Basic import Lean.Data.Lsp import Lean.Elab.Command @@ -192,7 +192,7 @@ abbrev ServerRequestEmitter := (method : String) → (param : Json) → BaseIO (ServerTask (ServerRequestResponse Json)) structure RequestContext where - rpcSessions : RBMap UInt64 (IO.Ref FileWorker.RpcSession) compare + rpcSessions : Std.TreeMap UInt64 (IO.Ref FileWorker.RpcSession) doc : FileWorker.EditableDocument hLog : IO.FS.Stream initParams : Lsp.InitializeParams diff --git a/src/Lean/Server/Rpc/Basic.lean b/src/Lean/Server/Rpc/Basic.lean index 1501e7ad3f..6fcfc94eb8 100644 --- a/src/Lean/Server/Rpc/Basic.lean +++ b/src/Lean/Server/Rpc/Basic.lean @@ -6,7 +6,7 @@ Authors: Wojciech Nawrocki -/ prelude import Init.Dynamic -import Lean.Data.Json +import Lean.Data.Json.FromToJson.Basic /-! Allows LSP clients to make Remote Procedure Calls to the server. diff --git a/src/Lean/Server/Rpc/RequestHandling.lean b/src/Lean/Server/Rpc/RequestHandling.lean index 453b016002..dc5dbcd269 100644 --- a/src/Lean/Server/Rpc/RequestHandling.lean +++ b/src/Lean/Server/Rpc/RequestHandling.lean @@ -73,7 +73,7 @@ def wrapRpcProcedure (method : Name) paramType respType wrapper seshId j := do let rc ← read - let some seshRef := rc.rpcSessions.find? seshId + let some seshRef := rc.rpcSessions.get? seshId | throwThe RequestError { code := JsonRpc.ErrorCode.rpcNeedsReconnect message := s!"Outdated RPC session" } diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index f089c12822..6169c93f06 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -7,12 +7,9 @@ Authors: Marc Huisinga, Wojciech Nawrocki prelude import Init.System.IO import Std.Sync.Mutex -import Std.Data.TreeMap import Init.Data.ByteArray -import Lean.Data.RBMap import Lean.Data.FuzzyMatching -import Lean.Data.Json import Lean.Data.Lsp import Lean.Server.Utils import Lean.Server.Requests @@ -260,7 +257,7 @@ end FileWorker section ServerM abbrev FileWorkerMap := Std.TreeMap DocumentUri FileWorker - abbrev ImportMap := RBMap DocumentUri (RBTree DocumentUri compare) compare + abbrev ImportMap := Std.TreeMap DocumentUri (Std.TreeSet DocumentUri) /-- Global import data for all open files managed by this watchdog. -/ structure ImportData where @@ -270,15 +267,15 @@ section ServerM importedBy : ImportMap /-- Updates `d` with the new set of `imports` for the file `uri`. -/ - def ImportData.update (d : ImportData) (uri : DocumentUri) (imports : RBTree DocumentUri compare) + def ImportData.update (d : ImportData) (uri : DocumentUri) (imports : Std.TreeSet DocumentUri) : ImportData := Id.run do - let oldImports := d.imports.findD uri ∅ - let removedImports := oldImports.diff imports - let addedImports := imports.diff oldImports + let oldImports := d.imports.getD uri ∅ + let removedImports := oldImports.eraseMany imports + let addedImports := imports.eraseMany oldImports let mut importedBy := d.importedBy for removedImport in removedImports do - let importedByRemovedImport' := importedBy.find! removedImport |>.erase uri + let importedByRemovedImport' := importedBy.get! removedImport |>.erase uri if importedByRemovedImport'.isEmpty then importedBy := importedBy.erase removedImport else @@ -286,7 +283,7 @@ section ServerM for addedImport in addedImports do importedBy := - importedBy.findD addedImport ∅ + importedBy.getD addedImport ∅ |>.insert uri |> importedBy.insert addedImport @@ -308,7 +305,7 @@ section ServerM sourceUri : DocumentUri localID : RequestID - abbrev PendingServerRequestMap := RBMap RequestID RequestIDTranslation compare + abbrev PendingServerRequestMap := Std.TreeMap RequestID RequestIDTranslation structure ServerRequestData where pendingServerRequests : PendingServerRequestMap @@ -330,7 +327,7 @@ section ServerM (data : ServerRequestData) (globalID : RequestID) : Option RequestIDTranslation × ServerRequestData := - let translation? := data.pendingServerRequests.find? globalID + let translation? := data.pendingServerRequests.get? globalID let data := { data with pendingServerRequests := data.pendingServerRequests.erase globalID } (translation?, data) @@ -1101,7 +1098,7 @@ def handlePrepareRename (p : PrepareRenameParams) : ReaderT ReferenceRequestCont def handleRename (p : RenameParams) : ReaderT ReferenceRequestContext IO Lsp.WorkspaceEdit := do if (String.toName p.newName).isAnonymous then throwServerError s!"Can't rename: `{p.newName}` is not an identifier" - let mut refs : Std.HashMap DocumentUri (RBMap Lsp.Position Lsp.Position compare) := ∅ + let mut refs : Std.HashMap DocumentUri (Std.TreeMap Lsp.Position Lsp.Position) := ∅ for { uri, range } in (← handleReference { p with context.includeDeclaration := true }) do refs := refs.insert uri <| (refs.getD uri ∅).insert range.start range.end -- We have to filter the list of changes to put the ranges in order and @@ -1161,7 +1158,7 @@ section NotificationHandling let s ← read let fileWorkers ← s.fileWorkersRef.get let importData ← s.importData.get - let dependents := importData.importedBy.findD p.textDocument.uri ∅ + let dependents := importData.importedBy.getD p.textDocument.uri ∅ for ⟨uri, _⟩ in fileWorkers do if ! dependents.contains uri then @@ -1178,7 +1175,7 @@ section NotificationHandling if ! leanChanges.isEmpty then let importData ← (← read).importData.get for (c, _) in leanChanges do - let dependents := importData.importedBy.findD c.uri ∅ + let dependents := importData.importedBy.getD c.uri ∅ for dependent in dependents do notifyAboutStaleDependency dependent c.uri if ! ileanChanges.isEmpty then @@ -1595,10 +1592,10 @@ def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do startLoadingReferences referenceData let fileWorkersRef ← IO.mkRef (Std.TreeMap.empty : FileWorkerMap) let serverRequestData ← IO.mkRef { - pendingServerRequests := RBMap.empty + pendingServerRequests := Std.TreeMap.empty freshServerRequestID := 0 } - let importData ← IO.mkRef ⟨RBMap.empty, RBMap.empty⟩ + let importData ← IO.mkRef ⟨Std.TreeMap.empty, Std.TreeMap.empty⟩ let requestData ← RequestDataMutex.new let i ← maybeTee "wdIn.txt" false i let o ← maybeTee "wdOut.txt" true o diff --git a/src/Lean/Setup.lean b/src/Lean/Setup.lean index 433e3705c7..3ae6133539 100644 --- a/src/Lean/Setup.lean +++ b/src/Lean/Setup.lean @@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Mac Malone -/ prelude -import Lean.Data.Json +import Lean.Data.Json.Parser +import Lean.Data.Json.FromToJson.Basic import Lean.Util.LeanOptions /-! diff --git a/src/Lean/SubExpr.lean b/src/Lean/SubExpr.lean index 2b6bbd4668..40c5edd047 100644 --- a/src/Lean/SubExpr.lean +++ b/src/Lean/SubExpr.lean @@ -5,8 +5,7 @@ Authors: Sebastian Ullrich, Daniel Selsam, Wojciech Nawrocki, E.W.Ayers -/ prelude import Lean.Meta.Basic -import Lean.Data.Json -import Lean.Data.RBMap +import Lean.Data.Json.Basic import Init.Control.Option namespace Lean @@ -171,7 +170,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) := RBMap Pos α compare +abbrev PosMap (α : Type u) := Std.TreeMap Pos α def bindingBody! : SubExpr → SubExpr | ⟨.forallE _ _ b _, p⟩ => ⟨b, p.pushBindingBody⟩ diff --git a/src/Lean/Util/LeanOptions.lean b/src/Lean/Util/LeanOptions.lean index fec30882ba..750ac3c7a5 100644 --- a/src/Lean/Util/LeanOptions.lean +++ b/src/Lean/Util/LeanOptions.lean @@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Marc Huisinga -/ prelude -import Lean.Data.Json +import Lean.Data.KVMap +import Lean.Data.Json.FromToJson.Basic namespace Lean @@ -82,7 +83,7 @@ def LeanOptions.ofArray (opts : Array LeanOption) : LeanOptions := /-- Add the options from `new`, overriding those in `self`. -/ protected def LeanOptions.append (self new : LeanOptions) : LeanOptions := - ⟨self.values.mergeBy (fun _ _ b => b) new.values⟩ + ⟨self.values.mergeWith (fun _ _ b => b) new.values⟩ instance : Append LeanOptions := ⟨LeanOptions.append⟩ @@ -99,7 +100,7 @@ def LeanOptions.toOptions (leanOptions : LeanOptions) : Options := Id.run do return options def LeanOptions.fromOptions? (options : Options) : Option LeanOptions := do - let mut values := RBMap.empty + let mut values := Std.TreeMap.empty for ⟨name, dataValue⟩ in options do let optionValue ← LeanOptionValue.ofDataValue? dataValue values := values.insert name optionValue diff --git a/src/Lean/Util/PPExt.lean b/src/Lean/Util/PPExt.lean index 61a196311e..6f44e49081 100644 --- a/src/Lean/Util/PPExt.lean +++ b/src/Lean/Util/PPExt.lean @@ -39,7 +39,7 @@ structure PPContext where currNamespace : Name := Name.anonymous openDecls : List OpenDecl := [] -abbrev PrettyPrinter.InfoPerPos := RBMap Nat Elab.Info compare +abbrev PrettyPrinter.InfoPerPos := Std.TreeMap Nat Elab.Info /-- A format tree with `Elab.Info` annotations. Each `.tag n _` node is annotated with `infos[n]`. This is used to attach semantic data such as expressions diff --git a/src/Lean/Widget/Diff.lean b/src/Lean/Widget/Diff.lean index 44c7465524..1fda3d85a3 100644 --- a/src/Lean/Widget/Diff.lean +++ b/src/Lean/Widget/Diff.lean @@ -58,13 +58,13 @@ structure ExprDiff where instance : EmptyCollection ExprDiff := ⟨{}⟩ instance : Append ExprDiff where append a b := { - changesBefore := RBMap.mergeBy (fun _ _ b => b) a.changesBefore b.changesBefore, - changesAfter := RBMap.mergeBy (fun _ _ b => b) a.changesAfter b.changesAfter + changesBefore := Std.TreeMap.mergeWith (fun _ _ b => b) a.changesBefore b.changesBefore, + changesAfter := Std.TreeMap.mergeWith (fun _ _ b => b) a.changesAfter b.changesAfter } instance : ToString ExprDiff where toString x := let f := fun (p : PosMap ExprDiffTag) => - RBMap.toList p |>.map (fun (k,v) => s!"({toString k}:{toString v})") + p.toList.map (fun (k,v) => s!"({toString k}:{toString v})") s!"before: {f x.changesBefore}\nafter: {f x.changesAfter}" /-- Add a tag at the given position to the `changesBefore` dict. -/ @@ -76,8 +76,8 @@ def ExprDiff.insertAfterChange (p : Pos) (d : ExprDiffTag := .change) (δ : Expr {δ with changesAfter := δ.changesAfter.insert p d} def ExprDiff.withChangePos (before after : Pos) (d : ExprDiffTag := .change) : ExprDiff := - { changesAfter := RBMap.empty.insert after d - changesBefore := RBMap.empty.insert before d + { changesAfter := Std.TreeMap.empty.insert after d + changesBefore := Std.TreeMap.empty.insert before d } /-- Add a tag to the diff at the positions given by `before` and `after`. -/ @@ -257,11 +257,11 @@ def diffInteractiveGoals (useAfter : Bool) (info : Elab.TacticInfo) (igs₁ : In let goals₀ := if useAfter then info.goalsBefore else info.goalsAfter let parentMap : MVarIdMap MVarIdSet ← info.goalsBefore.foldlM (init := ∅) (fun s g => do let ms ← Expr.mvar g |> Lean.Meta.getMVars - let ms : MVarIdSet := RBTree.fromArray ms _ + let ms := MVarIdSet.ofArray ms return s.insert g ms ) let isParent (before after : MVarId) : Bool := - match parentMap.find? before with + match parentMap.get? before with | some xs => xs.contains after | none => false let goals ← igs₁.goals.mapM (fun ig₁ => do diff --git a/src/Lean/Widget/InteractiveCode.lean b/src/Lean/Widget/InteractiveCode.lean index 306b5d3b92..83b3f23ed3 100644 --- a/src/Lean/Widget/InteractiveCode.lean +++ b/src/Lean/Widget/InteractiveCode.lean @@ -46,7 +46,7 @@ abbrev CodeWithInfos := TaggedText SubexprInfo def CodeWithInfos.mergePosMap [Monad m] (merger : SubexprInfo → α → m SubexprInfo) (pm : Lean.SubExpr.PosMap α) (tt : CodeWithInfos) : m CodeWithInfos := if pm.isEmpty then return tt else tt.mapM (fun (info : SubexprInfo) => - match pm.find? info.subexprPos with + match pm.get? info.subexprPos with | some a => merger info a | none => pure info ) @@ -64,7 +64,7 @@ partial def tagCodeInfos (ctx : Elab.ContextInfo) (infos : SubExpr.PosMap Elab.I where go (tt : TaggedText (Nat × Nat)) : BaseIO (TaggedText SubexprInfo) := tt.rewriteM fun (n, _) subTt => do - match infos.find? n with + match infos.get? n with | none => go subTt | some i => let t : SubexprInfo := { diff --git a/src/Lean/Widget/InteractiveDiagnostic.lean b/src/Lean/Widget/InteractiveDiagnostic.lean index 59578755a0..a4705b0dc4 100644 --- a/src/Lean/Widget/InteractiveDiagnostic.lean +++ b/src/Lean/Widget/InteractiveDiagnostic.lean @@ -93,7 +93,7 @@ that would effectively require reimplementing the (stateful, to keep track of in private inductive EmbedFmt /-- Nested tags denote `Info` objects in `infos`. -/ - | code (ctx : Elab.ContextInfo) (infos : RBMap Nat Elab.Info compare) + | code (ctx : Elab.ContextInfo) (infos : Std.TreeMap Nat Elab.Info) /-- Nested text is ignored. -/ | goal (ctx : Elab.ContextInfo) (lctx : LocalContext) (g : MVarId) /-- Nested text is ignored. -/ diff --git a/src/Lean/Widget/TaggedText.lean b/src/Lean/Widget/TaggedText.lean index 6ee95a3604..978fee8f5b 100644 --- a/src/Lean/Widget/TaggedText.lean +++ b/src/Lean/Widget/TaggedText.lean @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Wojciech Nawrocki -/ prelude -import Lean.Data.Json.FromToJson +import Lean.Data.Json.FromToJson.Basic import Lean.Server.Rpc.Basic namespace Lean.Widget diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean index 8ee25fa44a..b41df56de8 100644 --- a/src/Lean/Widget/UserWidget.lean +++ b/src/Lean/Widget/UserWidget.lean @@ -31,7 +31,7 @@ class ToModule (α : Type u) where instance : ToModule Module := ⟨id⟩ -private builtin_initialize builtinModulesRef : IO.Ref (RBMap UInt64 (Name × Module) compare) ← +private builtin_initialize builtinModulesRef : IO.Ref (Std.TreeMap UInt64 (Name × Module)) ← IO.mkRef ∅ def addBuiltinModule (id : Name) (m : Module) : IO Unit := @@ -43,7 +43,7 @@ where `inst : ToModule α` is synthesized during registration time and stored thereafter. -/ private abbrev ModuleRegistry := SimplePersistentEnvExtension (UInt64 × Name × Expr) - (RBMap UInt64 (Name × Expr) compare) + (Std.TreeMap UInt64 (Name × Expr)) builtin_initialize moduleRegistry : ModuleRegistry ← registerSimplePersistentEnvExtension { @@ -67,9 +67,9 @@ builtin_initialize widgetModuleAttrImpl : AttributeImpl ← let mod ← evalModule e let env ← getEnv unless builtin do -- don't warn on collision between previous and current stage - if let some _ := (← builtinModulesRef.get).find? mod.javascriptHash then + if let some _ := (← builtinModulesRef.get).get? mod.javascriptHash then logWarning m!"A builtin widget module with the same hash(JS source code) was already registered." - if let some (n, _) := moduleRegistry.getState env |>.find? mod.javascriptHash then + if let some (n, _) := moduleRegistry.getState env |>.get? mod.javascriptHash then logWarning m!"A widget module with the same hash(JS source code) was already registered at {.ofConstName n true}." let env ← getEnv if builtin then @@ -101,7 +101,7 @@ structure WidgetSource where open Server RequestM in def getWidgetSource (args : GetWidgetSourceParams) : RequestM (RequestTask WidgetSource) := do - if let some (_, m) := (← builtinModulesRef.get).find? args.hash then + if let some (_, m) := (← builtinModulesRef.get).get? args.hash then return .pure { sourcetext := m.javascript } let doc ← readDoc @@ -110,7 +110,7 @@ def getWidgetSource (args : GetWidgetSourceParams) : RequestM (RequestTask Widge withWaitFindSnap doc (notFoundX := notFound) (fun s => s.endPos >= pos || (moduleRegistry.getState s.env).contains args.hash) fun snap => do - if let some (_, e) := moduleRegistry.getState snap.env |>.find? args.hash then + if let some (_, e) := moduleRegistry.getState snap.env |>.get? args.hash then runTermElabM snap do return { sourcetext := (← evalModule e).javascript } else @@ -156,11 +156,11 @@ This is similar to a parametric attribute, except that: which we cannot do owing to the closure. -/ private abbrev PanelWidgetsExt := SimpleScopedEnvExtension (UInt64 × Name) - (RBMap UInt64 (List PanelWidgetsExtEntry) compare) + (Std.TreeMap UInt64 (List PanelWidgetsExtEntry)) builtin_initialize panelWidgetsExt : PanelWidgetsExt ← registerSimpleScopedEnvExtension { - addEntry := fun s (h, n) => s.insert h (.global n :: s.findD h []) + addEntry := fun s (h, n) => s.insert h (.global n :: s.getD h []) initial := .empty } @@ -183,7 +183,7 @@ def addPanelWidgetScoped [Monad m] [MonadEnv m] [MonadResolveName m] (h : UInt64 def addPanelWidgetLocal [Monad m] [MonadEnv m] (wi : WidgetInstance) : m Unit := do modifyEnv fun env => panelWidgetsExt.modifyState env fun s => - s.insert wi.javascriptHash (.local wi :: s.findD wi.javascriptHash []) + s.insert wi.javascriptHash (.local wi :: s.getD wi.javascriptHash []) def erasePanelWidget [Monad m] [MonadEnv m] (h : UInt64) : m Unit := do modifyEnv fun env => panelWidgetsExt.modifyState env fun st => st.erase h @@ -199,7 +199,7 @@ def WidgetInstance.ofHash (hash : UInt64) (props : StateM Server.RpcObjectStore let env ← getEnv let builtins ← builtinModulesRef.get let some id := - (builtins.find? hash |>.map (·.1)) <|> (moduleRegistry.getState env |>.find? hash |>.map (·.1)) + (builtins.get? hash |>.map (·.1)) <|> (moduleRegistry.getState env |>.get? hash |>.map (·.1)) | throwError s!"No widget module with hash {hash} registered" return { id, javascriptHash := hash, props } diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean index 3a17bf428f..67152b163e 100644 --- a/src/lake/Lake/Build/Common.lean +++ b/src/lake/Lake/Build/Common.lean @@ -691,14 +691,14 @@ private partial def mkLinkOrder (libs : Array Dynlib) : JobM (Array Dynlib) := d | .ok (_, order) => pure order | .error cycle => error s!"library dependency cycle:\n{formatCycle cycle}" where - go lib (ps : List String) (v : RBMap String Unit compare) (o : Array Dynlib) := do + go lib (ps : List String) (v : Std.TreeSet String compare) (o : Array Dynlib) := do let o := o.push lib if v.contains lib.name then return (v, o) if ps.contains lib.name then throw (lib.name :: ps) let ps := lib.name :: ps - let v := v.insert lib.name () + let v := v.insert lib.name let (v, o) ← lib.deps.foldlM (init := (v, o)) fun (v, o) lib => go lib ps v o return (v, o) diff --git a/src/lake/Lake/Build/InitFacets.lean b/src/lake/Lake/Build/InitFacets.lean index 7c9cd2e36f..ddd68c300c 100644 --- a/src/lake/Lake/Build/InitFacets.lean +++ b/src/lake/Lake/Build/InitFacets.lean @@ -27,4 +27,4 @@ def initFacetConfigs : DNameMap FacetConfig := |> insert InputDir.initFacetConfigs where insert {k} (group : DNameMap (KFacetConfig k)) map := - group.fold (init := map) fun m k v => m.insert k v.toFacetConfig + group.foldl (init := map) fun m k v => m.insert k v.toFacetConfig diff --git a/src/lake/Lake/Build/Key.lean b/src/lake/Lake/Build/Key.lean index ea6b8c14ee..55423c889a 100644 --- a/src/lake/Lake/Build/Key.lean +++ b/src/lake/Lake/Build/Key.lean @@ -177,7 +177,7 @@ theorem eq_of_quickCmp : intro k'; cases k' case packageTarget p' t' => dsimp only; split - next p_eq => intro t_eq; rw [eq_of_cmp p_eq, eq_of_cmp t_eq] + next p_eq => intro t_eq; rw [Std.LawfulEqCmp.eq_of_compare p_eq, Std.LawfulEqCmp.eq_of_compare t_eq] next => intro; contradiction all_goals (intro; contradiction) | facet t f ih => @@ -185,10 +185,16 @@ theorem eq_of_quickCmp : intro k'; cases k' case facet t' f'' => dsimp only; split - next t_eq => intro f_eq; rw [ih t_eq, eq_of_cmp f_eq] + next t_eq => intro f_eq; rw [ih t_eq, Std.LawfulEqCmp.eq_of_compare f_eq] next => intro; contradiction all_goals (intro; contradiction) -instance : LawfulCmpEq BuildKey quickCmp where - eq_of_cmp := eq_of_quickCmp - cmp_rfl {k} := by induction k <;> simp_all [quickCmp] +instance : Std.LawfulEqCmp quickCmp where + eq_of_compare := eq_of_quickCmp + compare_self {k} := by + induction k + · simp [quickCmp] + · simp [quickCmp] + · simp only [quickCmp] + split <;> simp_all + · simp_all [quickCmp] diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean index 19df467f25..14fb08c4ed 100644 --- a/src/lake/Lake/Build/Module.lean +++ b/src/lake/Lake/Build/Module.lean @@ -170,13 +170,13 @@ private partial def mkLoadOrder (libs : Array Dynlib) : FetchM (Array Dynlib) := | .ok (_, order) => pure order | .error cycle => error s!"library dependency cycle:\n{formatCycle cycle}" where - go lib (ps : List String) (v : RBMap String Unit compare) (o : Array Dynlib) := do + go lib (ps : List String) (v : Std.TreeSet String compare) (o : Array Dynlib) := do if v.contains lib.name then return (v, o) if ps.contains lib.name then throw (lib.name :: ps) let ps := lib.name :: ps - let v := v.insert lib.name () + let v := v.insert lib.name let (v, o) ← lib.deps.foldlM (init := (v, o)) fun (v, o) lib => go lib ps v o let o := o.push lib @@ -558,7 +558,7 @@ private def Module.buildLean mod.computeOutputHashes setup.isModule private def traceOptions (opts : LeanOptions) (caption := "opts") : BuildTrace := - opts.values.fold (init := .nil caption) fun t n v => + opts.values.foldl (init := .nil caption) fun t n v => let opt := s!"-D{n}={v.asCliFlagValue}" t.mix <| .ofHash (pureHash opt) opt diff --git a/src/lake/Lake/Build/Store.lean b/src/lake/Lake/Build/Store.lean index e173527744..f65d000672 100644 --- a/src/lake/Lake/Build/Store.lean +++ b/src/lake/Lake/Build/Store.lean @@ -24,9 +24,9 @@ abbrev MonadBuildStore (m) := MonadDStore BuildKey (Job <| BuildData ·) m /-- The type of the Lake build store. -/ abbrev BuildStore := - DRBMap BuildKey (Job <| BuildData ·) BuildKey.quickCmp + Std.DTreeMap BuildKey (Job <| BuildData ·) BuildKey.quickCmp -@[inline] def BuildStore.empty : BuildStore := DRBMap.empty +@[inline] def BuildStore.empty : BuildStore := Std.DTreeMap.empty namespace BuildStore diff --git a/src/lake/Lake/CLI/Translate/Lean.lean b/src/lake/Lake/CLI/Translate/Lean.lean index 49ad2ca059..36d408ad8d 100644 --- a/src/lake/Lake/CLI/Translate/Lean.lean +++ b/src/lake/Lake/CLI/Translate/Lean.lean @@ -253,7 +253,7 @@ def Dependency.mkRequire (cfg : Dependency) : RequireDecl := Unhygienic.run do pure none let scope? := if cfg.scope.isEmpty then none else some (toLean cfg.scope) let opts? := if cfg.opts.isEmpty then none else some <| Unhygienic.run do - cfg.opts.foldM (init := mkCIdent ``NameMap.empty) fun stx opt val => + cfg.opts.foldlM (init := mkCIdent ``NameMap.empty) fun stx opt val => `($stx |>.insert $(toLean opt) $(toLean val)) `(requireDecl|require $[$scope? /]? $(mkIdent cfg.name):ident $[@ $ver?]? $[from $src?]? $[with $opts?]?) diff --git a/src/lake/Lake/CLI/Translate/Toml.lean b/src/lake/Lake/CLI/Translate/Toml.lean index 306c07bc0f..3a1d4a0cf1 100644 --- a/src/lake/Lake/CLI/Translate/Toml.lean +++ b/src/lake/Lake/CLI/Translate/Toml.lean @@ -137,7 +137,7 @@ protected def Dependency.toToml (dep : Dependency) (t : Table := {}) : Table := |>.smartInsert `subDir subDir? else t - t.smartInsert `options <| dep.opts.fold (·.insert · ·) Table.empty + t.smartInsert `options <| dep.opts.foldl (·.insert · ·) Table.empty instance : ToToml Dependency := ⟨(toToml ·.toToml)⟩ diff --git a/src/lake/Lake/Config/Dependency.lean b/src/lake/Lake/Config/Dependency.lean index 6011edd6cb..51ce736606 100644 --- a/src/lake/Lake/Config/Dependency.lean +++ b/src/lake/Lake/Config/Dependency.lean @@ -6,7 +6,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone prelude import Init.Dynamic import Init.System.FilePath -import Lean.Data.NameMap +import Lean.Data.NameMap.Basic /- # Package Dependency Configuration diff --git a/src/lake/Lake/Config/Module.lean b/src/lake/Lake/Config/Module.lean index bcfff3a443..1d3192fd9f 100644 --- a/src/lake/Lake/Config/Module.lean +++ b/src/lake/Lake/Config/Module.lean @@ -34,8 +34,8 @@ abbrev ModuleSet := Std.HashSet Module abbrev OrdModuleSet := OrdHashSet Module @[inline] def OrdModuleSet.empty : OrdModuleSet := OrdHashSet.empty -abbrev ModuleMap (α) := RBMap Module α (·.name.quickCmp ·.name) -@[inline] def ModuleMap.empty : ModuleMap α := RBMap.empty +abbrev ModuleMap (α) := Std.TreeMap Module α (·.name.quickCmp ·.name) +@[inline] def ModuleMap.empty : ModuleMap α := Std.TreeMap.empty /-- Locate the named, buildable module in the library diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean index 873ede6326..ef88bb2ca2 100644 --- a/src/lake/Lake/Config/Package.lean +++ b/src/lake/Lake/Config/Package.lean @@ -12,7 +12,6 @@ import Lake.Config.ConfigDecl import Lake.Config.Script import Lake.Config.Cache import Lake.Load.Config -import Lake.Util.DRBMap import Lake.Util.OrdHashSet import Lake.Util.Version import Lake.Util.FilePath @@ -301,7 +300,6 @@ configuration PackageConfig (name : Name) extends WorkspaceConfig, LeanConfig wh the `LAKE_ARTIFACT_CACHE` environment variable is set to true. -/ enableArtifactCache?, enableArtifactCache : Option Bool := none - /-- Whether native libraries (of this package) should be prefixed with `lib` on Windows. @@ -312,6 +310,8 @@ configuration PackageConfig (name : Name) extends WorkspaceConfig, LeanConfig wh Defaults to `false`. -/ libPrefixOnWindows : Bool := false +deriving Inhabited + instance : EmptyCollection (PackageConfig n) := ⟨{}⟩ @@ -652,7 +652,7 @@ def inputsFileIn (cache : Cache) (self : Package) : FilePath := /-- Try to find a target configuration in the package with the given name. -/ def findTargetDecl? (name : Name) (self : Package) : Option (NConfigDecl self.name name) := - self.targetDeclMap.find? name + self.targetDeclMap.get? name /-- Whether the given module is considered local to the package. -/ def isLocalModule (mod : Name) (self : Package) : Bool := diff --git a/src/lake/Lake/Config/TargetConfig.lean b/src/lake/Lake/Config/TargetConfig.lean index 681be75dbb..6ec761ecf6 100644 --- a/src/lake/Lake/Config/TargetConfig.lean +++ b/src/lake/Lake/Config/TargetConfig.lean @@ -40,4 +40,4 @@ abbrev TargetDecl := KConfigDecl .anonymous /-- Try to find a target configuration in the package with the given name . -/ def Package.findTargetConfig? (name : Name) (self : Package) : Option (TargetConfig self.name name) := - self.targetDeclMap.find? name |>.bind (·.targetConfig?) + self.targetDeclMap.get? name |>.bind (·.targetConfig?) diff --git a/src/lake/Lake/Config/Workspace.lean b/src/lake/Lake/Config/Workspace.lean index b8138ec273..18010e8923 100644 --- a/src/lake/Lake/Config/Workspace.lean +++ b/src/lake/Lake/Config/Workspace.lean @@ -91,7 +91,7 @@ def addPackage (pkg : Package) (self : Workspace) : Workspace := /-- Try to find a package within the workspace with the given name. -/ @[inline] protected def findPackage? (name : Name) (self : Workspace) : Option (NPackage name) := - self.packageMap.find? name + self.packageMap.get? name /-- Try to find a script in the workspace with the given name. -/ protected def findScript? (script : Name) (self : Workspace) : Option Script := @@ -143,7 +143,7 @@ def addFacetConfig {name} (cfg : FacetConfig name) (self : Workspace) : Workspac /-- Try to find a facet configuration in the workspace with the given name. -/ def findFacetConfig? (name : Name) (self : Workspace) : Option (FacetConfig name) := - self.facetConfigs.find? name + self.facetConfigs.get? name /-- Add a module facet to the workspace. -/ def addModuleFacetConfig (cfg : ModuleFacetConfig name) (self : Workspace) : Workspace := diff --git a/src/lake/Lake/DSL/DeclUtil.lean b/src/lake/Lake/DSL/DeclUtil.lean index 86442c625c..3fb0c3b1ac 100644 --- a/src/lake/Lake/DSL/DeclUtil.lean +++ b/src/lake/Lake/DSL/DeclUtil.lean @@ -116,7 +116,7 @@ def mkConfigFields m := m.insert c {ref := id, val} else logWarningAt id m!"unknown '{.ofConstName tyName}' field '{fieldName}'" - let fs ← m.foldM (init := #[]) fun a k {ref, val} => do + let fs ← m.foldlM (init := #[]) fun a k {ref, val} => do let id := mkIdentFrom ref k true -- An unhygienic quotation is used to avoid introducing source info -- which will break field auto-completion. diff --git a/src/lake/Lake/Load/Lean/Eval.lean b/src/lake/Lake/Load/Lean/Eval.lean index 7c5f986b7b..af672f4f09 100644 --- a/src/lake/Lake/Load/Lean/Eval.lean +++ b/src/lake/Lake/Load/Lean/Eval.lean @@ -46,7 +46,7 @@ opaque evalConstCheck : Except String α /-- Construct a `DNameMap` from the declarations tagged with `attr`. -/ -def mkTagMap +def mkDTagMap (env : Environment) (attr : OrderedTagAttribute) [Monad m] (f : (n : Name) → m (β n)) : m (DNameMap β) := @@ -54,6 +54,15 @@ def mkTagMap entries.foldlM (init := {}) fun map declName => return map.insert declName <| ← f declName +/-- Construct a `NameMap` from the declarations tagged with `attr`. -/ +def mkTagMap + (env : Environment) (attr : OrderedTagAttribute) + [Monad m] (f : (n : Name) → m β) +: m (NameMap β) := + let entries := attr.getAllEntries env + entries.foldlM (init := {}) fun map declName => + return map.insert declName <| ← f declName + /-- Construct a `OrdNameMap` from the declarations tagged with `attr`. -/ def mkOrdTagMap (env : Environment) (attr : OrderedTagAttribute) @@ -95,7 +104,7 @@ def Package.loadFromEnv target '{decl.name}' was defined in package '{decl.pkg}', \ but registered under '{self.name}'" let targetDeclMap ← targetDecls.foldlM (init := {}) fun m decl => do - if let some orig := m.find? decl.name then + if let some orig := m.get? decl.name then error s!"\ {self.name}: target '{decl.name}' was already defined as a '{orig.kind}', \ but then redefined as a '{decl.kind}'" @@ -109,7 +118,7 @@ def Package.loadFromEnv let fn ← IO.ofExcept <| evalConstCheck env opts ScriptFn scriptName return {name, fn, doc? := ← findDocString? env scriptName : Script} let defaultScripts ← defaultScriptAttr.getAllEntries env |>.mapM fun name => - if let some script := scripts.find? name then pure script else + if let some script := scripts.get? name then pure script else error s!"{self.name}: package is missing script '{name}' marked as a default" let postUpdateHooks ← postUpdateAttr.getAllEntries env |>.mapM fun name => match evalConstCheck env opts PostUpdateHookDecl name with diff --git a/src/lake/Lake/Load/Toml.lean b/src/lake/Lake/Load/Toml.lean index 99b829a417..47aa332c18 100644 --- a/src/lake/Lake/Load/Toml.lean +++ b/src/lake/Lake/Load/Toml.lean @@ -402,7 +402,7 @@ where let some name ← tryDecode? <| stringToLegalOrSimpleName <$> t.decode `name | return r let (decls, map) := r - if let some orig := map.find? name then + if let some orig := map.get? name then modify fun es => es.push <| .mk val.ref s!"\ {pkg}: target '{name}' was already defined as a '{orig.kind}', \ but then redefined as a '{kind}'" diff --git a/src/lake/Lake/Toml/Data/Dict.lean b/src/lake/Lake/Toml/Data/Dict.lean index 4e6af6c359..01328ea95d 100644 --- a/src/lake/Lake/Toml/Data/Dict.lean +++ b/src/lake/Lake/Toml/Data/Dict.lean @@ -4,13 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ prelude -import Lean.Data.NameMap +import Lean.Data.NameMap.Basic import Init.Data.Nat.Fold /-! # Red-Black Dictionary Defines an **insertion-ordered** key-value mapping backed by an red-black tree. -Implemented via a key-index `RBMap` into an `Array` of key-value pairs. +Implemented via a key-index `Std.TreeMap` into an `Array` of key-value pairs. -/ open Lean @@ -20,7 +20,7 @@ namespace Lake.Toml /- An insertion-ordered key-value mapping backed by a red-black tree. -/ structure RBDict (α : Type u) (β : Type v) (cmp : α → α → Ordering) where items : Array (α × β) - indices : RBMap α Nat cmp + indices : Std.TreeMap α Nat cmp deriving Inhabited abbrev NameDict (α : Type u) := RBDict Name α Name.quickCmp @@ -36,7 +36,7 @@ def mkEmpty (capacity : Nat) : RBDict α β cmp := {items := .mkEmpty capacity, indices := {}} def ofArray (items : Array (α × β)) : RBDict α β cmp := - let indices := items.size.fold (init := mkRBMap α Nat cmp) fun i _ indices => + let indices := items.size.fold (init := ∅) fun i _ indices => indices.insert items[i].1 i {items, indices} @@ -61,7 +61,7 @@ def contains (k : α) (t : RBDict α β cmp) : Bool := t.indices.contains k def findIdx? (k : α) (t : RBDict α β cmp) : Option (Fin t.size) := do - let i ← t.indices.find? k; if h : i < t.items.size then some ⟨i, h⟩ else none + let i ← t.indices.get? k; if h : i < t.items.size then some ⟨i, h⟩ else none def findEntry? (k : α) (t : RBDict α β cmp) : Option (α × β) := do return t.items[← t.findIdx? k] diff --git a/src/lake/Lake/Toml/Elab/Expression.lean b/src/lake/Lake/Toml/Elab/Expression.lean index f42fbec069..2d4f7c26fe 100644 --- a/src/lake/Lake/Toml/Elab/Expression.lean +++ b/src/lake/Lake/Toml/Elab/Expression.lean @@ -96,7 +96,7 @@ def elabHeaderKeys (ks : Array (TSyntax ``simpleKey)) : TomlElabM Name := do s with arrKeyTys currArrKey := .anonymous - keyTys := arrKeyTys.find? .anonymous |>.getD {} + keyTys := arrKeyTys.get? .anonymous |>.getD {} } ks.foldlM (init := Name.anonymous) fun k kStx => do let k ← k.str <$> elabSimpleKey kStx diff --git a/src/lake/Lake/Util/Compare.lean b/src/lake/Lake/Util/Compare.lean deleted file mode 100644 index fa0ddc8354..0000000000 --- a/src/lake/Lake/Util/Compare.lean +++ /dev/null @@ -1,74 +0,0 @@ -/- -Copyright (c) 2022 Mac Malone. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Mac Malone --/ -prelude -import Init.Data.Ord -import Init.Data.String.Lemmas - -namespace Lake - -/-- -Proof that the equality of a compare function corresponds -to propositional equality. --/ -class EqOfCmp (α : Type u) (cmp : α → α → Ordering) where - eq_of_cmp {a a' : α} : cmp a a' = .eq → a = a' - -export EqOfCmp (eq_of_cmp) - -/-- -Proof that the equality of a compare function corresponds -to propositional equality and vice versa. --/ -class LawfulCmpEq (α : Type u) (cmp : α → α → Ordering) extends EqOfCmp α cmp where - cmp_rfl {a : α} : cmp a a = .eq - -export LawfulCmpEq (cmp_rfl) - -attribute [simp] cmp_rfl - -@[simp] theorem cmp_iff_eq [LawfulCmpEq α cmp] : cmp a a' = .eq ↔ a = a' := - Iff.intro eq_of_cmp fun a_eq => a_eq ▸ cmp_rfl - -/-- -Proof that the equality of a compare function corresponds -to propositional equality with respect to a given function. --/ -class EqOfCmpWrt (α : Type u) {β : Type v} (f : α → β) (cmp : α → α → Ordering) where - eq_of_cmp_wrt {a a' : α} : cmp a a' = .eq → f a = f a' - -export EqOfCmpWrt (eq_of_cmp_wrt) - -instance [EqOfCmp α cmp] : EqOfCmpWrt α f cmp where - eq_of_cmp_wrt h := by rw [eq_of_cmp h] - --- ## Basic Instances - -theorem eq_of_compareOfLessAndEq [LT α] [DecidableEq α] {a a' : α} -[Decidable (a < a')] (h : compareOfLessAndEq a a' = .eq) : a = a' := by - unfold compareOfLessAndEq at h - split at h - next => - simp at h - next => - split at h - next => assumption - next => simp at h - -theorem compareOfLessAndEq_rfl [LT α] [DecidableEq α] {a : α} -[Decidable (a < a)] (lt_irrefl : ¬ a < a) : compareOfLessAndEq a a = .eq := by - simp [compareOfLessAndEq, lt_irrefl] - -instance : LawfulCmpEq Nat compare where - eq_of_cmp := eq_of_compareOfLessAndEq - cmp_rfl := compareOfLessAndEq_rfl <| Nat.lt_irrefl _ - -instance : LawfulCmpEq UInt64 compare where - eq_of_cmp h := eq_of_compareOfLessAndEq h - cmp_rfl := compareOfLessAndEq_rfl <| UInt64.lt_irrefl _ - -instance : LawfulCmpEq String compare where - eq_of_cmp := eq_of_compareOfLessAndEq - cmp_rfl := compareOfLessAndEq_rfl <| String.lt_irrefl _ diff --git a/src/lake/Lake/Util/DRBMap.lean b/src/lake/Lake/Util/DRBMap.lean deleted file mode 100644 index 3451ff1614..0000000000 --- a/src/lake/Lake/Util/DRBMap.lean +++ /dev/null @@ -1,152 +0,0 @@ -/- -Copyright (c) 2022 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura, Mac Malone --/ -prelude -import Lean.Data.RBMap -import Lake.Util.Compare - -namespace Lake -open Lean RBNode - -/-! -This module includes a dependently typed adaption of the `Lean.RBMap` -defined in `Lean.Data.RBMap` module of the Lean core. Most of the code is -copied directly from there with only minor edits. --/ - -instance inhabitedOfEmptyCollection [EmptyCollection α] : Inhabited α where - default := {} - -@[specialize] def RBNode.dFind {α : Type u} {β : α → Type v} -(cmp : α → α → Ordering) [h : EqOfCmpWrt α β cmp] : RBNode α β → (k : α) → Option (β k) - | leaf, _ => none - | node _ a ky vy b, x => - match ho:cmp x ky with - | Ordering.lt => dFind cmp a x - | Ordering.gt => dFind cmp b x - | Ordering.eq => some <| cast (by rw [eq_of_cmp_wrt (f := β) ho]) vy - -/-- A Dependently typed `RBMap`. -/ -def DRBMap (α : Type u) (β : α → Type v) (cmp : α → α → Ordering) : Type (max u v) := - {t : RBNode α β // t.WellFormed cmp } - -instance : Coe (DRBMap α (fun _ => β) cmp) (RBMap α β cmp) := ⟨id⟩ - -@[inline] def mkDRBMap (α : Type u) (β : α → Type v) (cmp : α → α → Ordering) : DRBMap α β cmp := - ⟨leaf, WellFormed.leafWff⟩ - -@[inline] def DRBMap.empty {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} : DRBMap α β cmp := - mkDRBMap .. - -instance (α : Type u) (β : α → Type v) (cmp : α → α → Ordering) : EmptyCollection (DRBMap α β cmp) := - ⟨DRBMap.empty⟩ - -namespace DRBMap -variable {α : Type u} {β : α → Type v} {σ : Type w} {cmp : α → α → Ordering} - -def depth (f : Nat → Nat → Nat) (t : DRBMap α β cmp) : Nat := - t.val.depth f - -@[inline] def fold (f : σ → (k : α) → β k → σ) : (init : σ) → DRBMap α β cmp → σ - | b, ⟨t, _⟩ => t.fold f b - -@[inline] def revFold (f : σ → (k : α) → β k → σ) : (init : σ) → DRBMap α β cmp → σ - | b, ⟨t, _⟩ => t.revFold f b - -@[inline] def foldM [Monad m] (f : σ → (k : α) → β k → m σ) : (init : σ) → DRBMap α β cmp → m σ - | b, ⟨t, _⟩ => t.foldM f b - -@[inline] def forM [Monad m] (f : (k : α) → β k → m PUnit) (t : DRBMap α β cmp) : m PUnit := - t.foldM (fun _ k v => f k v) ⟨⟩ - -@[inline] protected def forIn [Monad m] (t : DRBMap α β cmp) (init : σ) (f : ((k : α) × β k) → σ → m (ForInStep σ)) : m σ := - t.val.forIn init (fun a b acc => f ⟨a, b⟩ acc) - -instance : ForIn m (DRBMap α β cmp) ((k : α) × β k) where - forIn := DRBMap.forIn - -@[inline] def isEmpty : DRBMap α β cmp → Bool - | ⟨leaf, _⟩ => true - | _ => false - -@[specialize] def toList : DRBMap α β cmp → List ((k : α) × β k) - | ⟨t, _⟩ => t.revFold (fun ps k v => ⟨k, v⟩::ps) [] - -@[inline] protected def min : DRBMap α β cmp → Option ((k : α) × β k) - | ⟨t, _⟩ => - match t.min with - | some ⟨k, v⟩ => some ⟨k, v⟩ - | none => none - -@[inline] protected def max : DRBMap α β cmp → Option ((k : α) × β k) - | ⟨t, _⟩ => - match t.max with - | some ⟨k, v⟩ => some ⟨k, v⟩ - | none => none - -instance [Repr ((k : α) × β k)] : Repr (DRBMap α β cmp) where - reprPrec m prec := Repr.addAppParen ("Lake.drbmapOf " ++ repr m.toList) prec - -@[inline] def insert : DRBMap α β cmp → (k : α) → β k → DRBMap α β cmp - | ⟨t, w⟩, k, v => ⟨t.insert cmp k v, WellFormed.insertWff w rfl⟩ - -@[inline] def erase : DRBMap α β cmp → α → DRBMap α β cmp - | ⟨t, w⟩, k => ⟨t.erase cmp k, WellFormed.eraseWff w rfl⟩ - -@[specialize] def ofList : List ((k : α) × β k) → DRBMap α β cmp - | [] => mkDRBMap .. - | ⟨k,v⟩::xs => (ofList xs).insert k v - -@[inline] def findCore? : DRBMap α β cmp → α → Option ((k : α) × β k) - | ⟨t, _⟩, x => t.findCore cmp x - -@[inline] def find? [EqOfCmpWrt α β cmp] : DRBMap α β cmp → (k : α) → Option (β k) - | ⟨t, _⟩, x => RBNode.dFind cmp t x - -@[inline] def findD [EqOfCmpWrt α β cmp] (t : DRBMap α β cmp) (k : α) (v₀ : β k) : β k := - (t.find? k).getD v₀ - -/-- (lowerBound k) retrieves the kv pair of the largest key smaller than or equal to `k`, - if it exists. -/ -@[inline] def lowerBound : DRBMap α β cmp → α → Option ((k : α) × β k) - | ⟨t, _⟩, x => t.lowerBound cmp x none - -@[inline] def contains [EqOfCmpWrt α β cmp] (t : DRBMap α β cmp) (k : α) : Bool := - (t.find? k).isSome - -@[inline] def fromList (l : List ((k : α) × β k)) (cmp : α → α → Ordering) : DRBMap α β cmp := - l.foldl (fun r p => r.insert p.1 p.2) (mkDRBMap α β cmp) - -@[inline] def all : DRBMap α β cmp → ((k : α) → β k → Bool) → Bool - | ⟨t, _⟩, p => t.all p - -@[inline] def any : DRBMap α β cmp → ((k : α) → β k → Bool) → Bool - | ⟨t, _⟩, p => t.any p - -def size (m : DRBMap α β cmp) : Nat := - m.fold (fun sz _ _ => sz+1) 0 - -def maxDepth (t : DRBMap α β cmp) : Nat := - t.val.depth Nat.max - -@[inline] def min! [Inhabited ((k : α) × β k)] (t : DRBMap α β cmp) : (k : α) × β k := - match t.min with - | some p => p - | none => panic! "map is empty" - -@[inline] def max! [Inhabited ((k : α) × β k)] (t : DRBMap α β cmp) : (k : α) × β k := - match t.max with - | some p => p - | none => panic! "map is empty" - -@[inline] def find! [EqOfCmpWrt α β cmp] (t : DRBMap α β cmp) (k : α) [Inhabited (β k)] : β k := - match t.find? k with - | some b => b - | none => panic! "key is not in the map" - -end DRBMap - -def drbmapOf {α : Type u} {β : α → Type v} (l : List ((k : α) × (β k))) (cmp : α → α → Ordering) : DRBMap α β cmp := - DRBMap.fromList l cmp diff --git a/src/lake/Lake/Util/Family.lean b/src/lake/Lake/Util/Family.lean index 34ac2adbb7..ed123e1806 100644 --- a/src/lake/Lake/Util/Family.lean +++ b/src/lake/Lake/Util/Family.lean @@ -100,11 +100,11 @@ Putting this all together, one can do something like the following: ```lean opaque FooFam (idx : Name) : Type -abbrev FooMap := DRBMap Name FooFam Name.quickCmp +abbrev FooMap := Std.DTreeMap Name FooFam Name.quickCmp def FooMap.insert (self : FooMap) (idx : Name) [FamilyOut FooFam idx α] (a : α) : FooMap := - DRBMap.insert self idx (toFamily a) -def FooMap.find? (self : FooMap) (idx : Name) [FamilyOut FooFam idx α] : Option α := - ofFamily <$> DRBMap.find? self idx + Std.DTreeMap.insert self idx (toFamily a) +def FooMap.get? (self : FooMap) (idx : Name) [FamilyOut FooFam idx α] : Option α := + ofFamily <$> Std.DTreeMap.get? self idx family_def bar : FooFam `bar := Nat family_def baz : FooFam `baz := String @@ -112,7 +112,7 @@ def foo := Id.run do let mut map : FooMap := {} map := map.insert `bar 5 map := map.insert `baz "str" - return map.find? `bar + return map.get? `bar #eval foo -- 5 ``` diff --git a/src/lake/Lake/Util/JsonObject.lean b/src/lake/Lake/Util/JsonObject.lean index 38af63fdb8..07a15a9043 100644 --- a/src/lake/Lake/Util/JsonObject.lean +++ b/src/lake/Lake/Util/JsonObject.lean @@ -17,11 +17,11 @@ namespace Lake /-- A JSON object (`Json.obj` data). -/ abbrev JsonObject := - RBNode String (fun _ => Json) + Std.TreeMap.Raw String Json namespace JsonObject -@[inline] def mk (val : RBNode String (fun _ => Json)) : JsonObject := +@[inline] def mk (val : Std.TreeMap.Raw String Json) : JsonObject := val @[inline] protected def toJson (obj : JsonObject) : Json := @@ -36,16 +36,16 @@ instance : ToJson JsonObject := ⟨JsonObject.toJson⟩ instance : FromJson JsonObject := ⟨JsonObject.fromJson?⟩ @[inline] nonrec def insert [ToJson α] (obj : JsonObject) (prop : String) (val : α) : JsonObject := - obj.insert compare prop (toJson val) + obj.insert prop (toJson val) @[inline] def insertSome [ToJson α] (obj : JsonObject) (prop : String) (val? : Option α) : JsonObject := if let some val := val? then obj.insert prop val else obj nonrec def erase (obj : JsonObject) (prop : String) : JsonObject := - inline <| obj.erase compare prop + inline <| obj.erase prop @[inline] def getJson? (obj : JsonObject) (prop : String) : Option Json := - obj.find compare prop + obj.get? prop @[inline] def get [FromJson α] (obj : JsonObject) (prop : String) : Except String α := match obj.getJson? prop with diff --git a/src/lake/Lake/Util/Name.lean b/src/lake/Lake/Util/Name.lean index 433fe51ade..510f9c1e50 100644 --- a/src/lake/Lake/Util/Name.lean +++ b/src/lake/Lake/Util/Name.lean @@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ prelude +import Std.Classes.Ord.String +import Std.Classes.Ord.UInt import Lean.Data.Json -import Lean.Data.NameMap -import Lake.Util.DRBMap +import Lean.Data.NameMap.Basic import Lake.Util.RBArray open Lean @@ -21,19 +22,16 @@ If that fails, defaults to making it a simple name (e.g., `Lean.Name.mkSimple`). def stringToLegalOrSimpleName (s : String) : Name := if s.toName.isAnonymous then Lean.Name.mkSimple s else s.toName -@[inline] def NameMap.empty : NameMap α := RBMap.empty +@[inline] def NameMap.empty : NameMap α := mkNameMap α -instance : ForIn m (NameMap α) (Name × α) where - forIn self init f := self.forIn init f - -instance : Coe (RBMap Name α Name.quickCmp) (NameMap α) := ⟨id⟩ +instance : Coe (Std.TreeMap Name α Name.quickCmp) (NameMap α) := ⟨id⟩ abbrev OrdNameMap α := RBArray Name α Name.quickCmp @[inline] def OrdNameMap.empty : OrdNameMap α := RBArray.empty @[inline] def mkOrdNameMap (α : Type) : OrdNameMap α := RBArray.empty -abbrev DNameMap α := DRBMap Name α Name.quickCmp -@[inline] def DNameMap.empty : DNameMap α := DRBMap.empty +abbrev DNameMap α := Std.DTreeMap Name α Name.quickCmp +@[inline] def DNameMap.empty : DNameMap α := Std.DTreeMap.empty /-! # Name Helpers -/ @@ -72,23 +70,23 @@ theorem eq_anonymous_of_isAnonymous {n : Name} : (h : n.isAnonymous) → n = .an simp only [quickCmpAux]; split <;> simp_all [quickCmpAux_iff_eq] -instance : LawfulCmpEq Name quickCmpAux where - eq_of_cmp := quickCmpAux_iff_eq.mp - cmp_rfl := quickCmpAux_iff_eq.mpr rfl +instance : Std.LawfulEqCmp Name.quickCmpAux where + eq_of_compare := quickCmpAux_iff_eq.mp + compare_self := quickCmpAux_iff_eq.mpr rfl theorem eq_of_quickCmp {n n' : Name} : n.quickCmp n' = .eq → n = n' := by unfold Name.quickCmp intro h_cmp; split at h_cmp - next => exact eq_of_cmp h_cmp + next => exact Std.LawfulEqCmp.eq_of_compare h_cmp next => contradiction theorem quickCmp_rfl {n : Name} : n.quickCmp n = .eq := by unfold Name.quickCmp - split <;> exact cmp_rfl + split <;> exact Std.ReflCmp.compare_self -instance : LawfulCmpEq Name Name.quickCmp where - eq_of_cmp := eq_of_quickCmp - cmp_rfl := quickCmp_rfl +instance : Std.LawfulEqCmp Name.quickCmp where + eq_of_compare := eq_of_quickCmp + compare_self := quickCmp_rfl open Syntax in def quoteFrom (ref : Syntax) (n : Name) (canonical := false) : Term := diff --git a/src/lake/Lake/Util/RBArray.lean b/src/lake/Lake/Util/RBArray.lean index 287e0fd4a4..62cb70faee 100644 --- a/src/lake/Lake/Util/RBArray.lean +++ b/src/lake/Lake/Util/RBArray.lean @@ -4,19 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ prelude -import Lean.Data.RBMap +import Std.Data.TreeMap.Basic namespace Lake -open Lean (RBMap) /-- There are two ways to think of this type: -* As an `Array` of values with an `RBMap` key-value index for the key `α`. -* As an `RBMap` that preserves insertion order, but is optimized for +* As an `Array` of values with a `Std.TreeMap` key-value index for the key `α`. +* As a `Std.TreeMap` that preserves insertion order, but is optimized for iteration-by-values. Thus, it does not store the order of keys. -/ structure RBArray (α : Type u) (β : Type v) (cmp : α → α → Ordering) where - toRBMap : RBMap α β cmp + toTreeMap : Std.TreeMap α β cmp toArray : Array β namespace RBArray @@ -30,17 +29,17 @@ def mkEmpty (size : Nat) : RBArray α β cmp := ⟨.empty, .mkEmpty size⟩ @[inline] def find? (self : RBArray α β cmp) (a : α) : Option β := - self.toRBMap.find? a + self.toTreeMap.get? a @[inline] def contains (self : RBArray α β cmp) (a : α) : Bool := - self.toRBMap.contains a + self.toTreeMap.contains a /-- Insert `b` with the key `a`. Does nothing if the key is already present. -/ def insert (self : RBArray α β cmp) (a : α) (b : β) : RBArray α β cmp := - if self.toRBMap.contains a then + if self.toTreeMap.contains a then self else - ⟨self.toRBMap.insert a b, self.toArray.push b⟩ + ⟨self.toTreeMap.insert a b, self.toArray.push b⟩ @[inline] def all (f : β → Bool) (self : RBArray α β cmp) : Bool := self.toArray.all f diff --git a/src/lake/Lake/Util/StoreInsts.lean b/src/lake/Lake/Util/StoreInsts.lean index 402f248125..b43d053774 100644 --- a/src/lake/Lake/Util/StoreInsts.lean +++ b/src/lake/Lake/Util/StoreInsts.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ prelude -import Lake.Util.DRBMap import Lake.Util.RBArray import Lake.Util.Family import Lake.Util.Store @@ -12,20 +11,12 @@ import Lake.Util.Store open Lean namespace Lake -instance [Monad m] [EqOfCmpWrt κ β cmp] : MonadDStore κ β (StateT (DRBMap κ β cmp) m) where - fetch? k := return (← get).find? k +instance {cmp : κ → κ → Ordering} [Monad m] [Std.LawfulEqCmp cmp] : MonadDStore κ β (StateT (Std.DTreeMap κ β cmp) m) where + fetch? k := return (← get).get? k store k a := modify (·.insert k a) -instance [MonadLiftT (ST ω) m] [Monad m] [EqOfCmpWrt κ β cmp] : MonadDStore κ β (StateRefT' ω (DRBMap κ β cmp) m) where - fetch? k := return (← get).find? k - store k a := modify (·.insert k a) - -instance [Monad m] : MonadStore κ α (StateT (RBMap κ α cmp) m) where - fetch? k := return (← get).find? k - store k a := modify (·.insert k a) - -instance [MonadLiftT (ST ω) m] [Monad m] : MonadStore κ α (StateRefT' ω (RBMap κ α cmp) m) where - fetch? k := return (← get).find? k +instance {cmp : κ → κ → Ordering} [MonadLiftT (ST ω) m] [Monad m] [Std.LawfulEqCmp cmp] : MonadDStore κ β (StateRefT' ω (Std.DTreeMap κ β cmp) m) where + fetch? k := return (← get).get? k store k a := modify (·.insert k a) instance [Monad m] : MonadStore κ α (StateT (RBArray κ α cmp) m) where @@ -36,7 +27,6 @@ instance [MonadLiftT (ST ω) m] [Monad m] : MonadStore κ α (StateRefT' ω (RBA fetch? k := return (← get).find? k store k a := modify (·.insert k a) --- uses the eagerly specialized `RBMap` functions in `NameMap` instance [Monad m] : MonadStore Name α (StateT (NameMap α) m) where fetch? k := return (← get).find? k store k a := modify (·.insert k a) diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58edd..6b964da742 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -11,7 +11,7 @@ options get_default_options() { opts = opts.update({"debug", "terminalTacticsAsSorry"}, false); // switch to `true` for ABI-breaking changes affecting meta code; // see also next option! - opts = opts.update({"interpreter", "prefer_native"}, false); + opts = opts.update({"interpreter", "prefer_native"}, true); // switch to `false` when enabling `prefer_native` should also affect use // of built-in parsers in quotations; this is usually the case, but setting // both to `true` may be necessary for handling non-builtin parsers with diff --git a/tests/lean/PPRoundtrip.lean b/tests/lean/PPRoundtrip.lean index 91d4211b21..ddfe7acfbe 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)) (Lean.RBMap.empty.insert (SubExpr.Pos.ofArray #[1]) $ KVMap.empty.insert `pp.explicit true) +#eval checkM `(id (id Nat)) (Std.TreeMap.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/run/inductiveIndicesIssue.lean b/tests/lean/run/inductiveIndicesIssue.lean index cb4bbbb638..f0e5f99a4d 100644 --- a/tests/lean/run/inductiveIndicesIssue.lean +++ b/tests/lean/run/inductiveIndicesIssue.lean @@ -8,15 +8,15 @@ inductive sublist : List α → List α → Prop namespace Lean.PrefixTreeNode namespace Ex1 -inductive WellFormed (cmp : α → α → Ordering) : PrefixTreeNode α β → Prop where +inductive WellFormed (cmp : α → α → Ordering) : PrefixTreeNode α β cmp → Prop where | emptyWff : WellFormed cmp empty - | insertWff {t : PrefixTreeNode α β} {k : List α} {val : β} : WellFormed cmp t → WellFormed cmp (insert t cmp k val) + | insertWff {t : PrefixTreeNode α β cmp} {k : List α} {val : β} : WellFormed cmp t → WellFormed cmp (insert cmp t k val) end Ex1 namespace Ex2 -inductive WellFormed (cmp : α → α → Ordering) : PrefixTreeNode α β → Prop where +inductive WellFormed (cmp : α → α → Ordering) : PrefixTreeNode α β cmp → Prop where | emptyWff : WellFormed cmp empty - | insertWff : WellFormed cmp t → WellFormed cmp (insert t cmp k val) + | insertWff : WellFormed cmp t → WellFormed cmp (insert cmp t k val) end Ex2 end Lean.PrefixTreeNode