diff --git a/releases/v4.0.0-m4.md b/releases/v4.0.0-m4.md index 9898f313e46dd..974f54bf86f1f 100644 --- a/releases/v4.0.0-m4.md +++ b/releases/v4.0.0-m4.md @@ -75,7 +75,7 @@ For example, given `f : Nat → Nat` and `g : Nat → Nat`, `f.comp g` is now no * The new `.` notation is now also accepted where a function type is expected. ```lean example (xs : List Nat) : List Nat := .map .succ xs - example (xs : List α) : Std.TreeSet α ord := xs.foldl .insert ∅ + example (xs : List α) : Std.RBTree α ord := xs.foldl .insert ∅ ``` * [Add code folding support to the language server](https://github.com/leanprover/lean4/pull/1014). diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index 95c2fed8017a1..4a06fbc2c70f5 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -142,7 +142,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.foldl (fun a e => a.push e) #[] + let r : Array Name := es.fold (fun a e => a.push e) #[] r.qsort Name.quickLt statsFn := fun s => "tag attribute" ++ Format.line ++ "number of local entries: " ++ format s.size } @@ -192,7 +192,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.foldl (fun a n p => a.push (n, p)) #[] + let r : Array (Name × α) := m.fold (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 } @@ -249,7 +249,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.foldl (fun a n p => a.push (n, p)) #[] + let r : Array (Name × α) := m.fold (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 } diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean index 5f32399d9f371..2e352300208bb 100644 --- a/src/Lean/Compiler/IR/Basic.lean +++ b/src/Lean/Compiler/IR/Basic.lean @@ -8,7 +8,6 @@ import Lean.Data.KVMap import Lean.Data.Name import Lean.Data.Format import Lean.Compiler.ExternAttr -import Std.Data.TreeSet.Basic /-! Implements (extended) λPure and λRc proposed in the article "Counting Immutable Beans", Sebastian Ullrich and Leonardo de Moura. @@ -18,7 +17,6 @@ this part is implemented in C++. The procedures described in the paper above are implemented in Lean. -/ namespace Lean.IR -open Std (TreeMap TreeSet) /-- Function identifier -/ abbrev FunId := Name @@ -447,18 +445,18 @@ end Decl Decl.fdecl f xs ty FnBody.unreachable {} /-- Set of variable and join point names -/ -abbrev IndexSet := TreeSet Index compare +abbrev IndexSet := RBTree Index compare instance : Inhabited IndexSet := ⟨{}⟩ def mkIndexSet (idx : Index) : IndexSet := - TreeSet.empty.insert idx + RBTree.empty.insert idx inductive LocalContextEntry where | param : IRType → LocalContextEntry | localVar : IRType → Expr → LocalContextEntry | joinPoint : Array Param → FnBody → LocalContextEntry -abbrev LocalContext := TreeMap Index LocalContextEntry compare +abbrev LocalContext := RBMap Index LocalContextEntry compare def LocalContext.addLocal (ctx : LocalContext) (x : VarId) (t : IRType) (v : Expr) : LocalContext := ctx.insert x.idx (LocalContextEntry.localVar t v) @@ -473,48 +471,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.get? idx with + match ctx.find? idx with | some (LocalContextEntry.joinPoint _ _) => true | _ => false def LocalContext.getJPBody (ctx : LocalContext) (j : JoinPointId) : Option FnBody := - match ctx.get? j.idx with + match ctx.find? j.idx with | some (LocalContextEntry.joinPoint _ b) => some b | _ => none def LocalContext.getJPParams (ctx : LocalContext) (j : JoinPointId) : Option (Array Param) := - match ctx.get? j.idx with + match ctx.find? j.idx with | some (LocalContextEntry.joinPoint ys _) => some ys | _ => none def LocalContext.isParam (ctx : LocalContext) (idx : Index) : Bool := - match ctx.get? idx with + match ctx.find? idx with | some (LocalContextEntry.param _) => true | _ => false def LocalContext.isLocalVar (ctx : LocalContext) (idx : Index) : Bool := - match ctx.get? idx with + match ctx.find? idx with | some (LocalContextEntry.localVar _ _) => true | _ => false def LocalContext.contains (ctx : LocalContext) (idx : Index) : Bool := - TreeMap.contains ctx idx + RBMap.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.get? x.idx with + match ctx.find? 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.get? x.idx with + match ctx.find? x.idx with | some (LocalContextEntry.localVar _ v) => some v | _ => none -abbrev IndexRenaming := TreeMap Index Index compare +abbrev IndexRenaming := RBMap Index Index compare class AlphaEqv (α : Type) where aeqv : IndexRenaming → α → α → Bool @@ -522,7 +520,7 @@ class AlphaEqv (α : Type) where export AlphaEqv (aeqv) def VarId.alphaEqv (ρ : IndexRenaming) (v₁ v₂ : VarId) : Bool := - match ρ.get? v₁.idx with + match ρ.find? v₁.idx with | some v => v == v₂.idx | none => v₁ == v₂ @@ -605,7 +603,7 @@ def FnBody.beq (b₁ b₂ : FnBody) : Bool := instance : BEq FnBody := ⟨FnBody.beq⟩ -abbrev VarIdSet := TreeSet VarId (fun x y => compare x.idx y.idx) +abbrev VarIdSet := RBTree VarId (fun x y => compare x.idx y.idx) instance : Inhabited VarIdSet := ⟨{}⟩ def mkIf (x : VarId) (t e : FnBody) : FnBody := diff --git a/src/Lean/Compiler/IR/LiveVars.lean b/src/Lean/Compiler/IR/LiveVars.lean index c451a668229e7..fbb6cfc80d650 100644 --- a/src/Lean/Compiler/IR/LiveVars.lean +++ b/src/Lean/Compiler/IR/LiveVars.lean @@ -8,7 +8,6 @@ import Lean.Compiler.IR.Basic import Lean.Compiler.IR.FreeVars namespace Lean.IR -open Std (TreeMap TreeSet) /-! Remark: in the paper "Counting Immutable Beans" the concepts of free and live variables coincide because the paper does *not* consider @@ -81,13 +80,13 @@ def FnBody.hasLiveVar (b : FnBody) (ctx : LocalContext) (x : VarId) : Bool := (IsLive.visitFnBody x.idx b).run' ctx abbrev LiveVarSet := VarIdSet -abbrev JPLiveVarMap := TreeMap JoinPointId LiveVarSet (fun j₁ j₂ => compare j₁.idx j₂.idx) +abbrev JPLiveVarMap := RBMap JoinPointId LiveVarSet (fun j₁ j₂ => compare j₁.idx j₂.idx) instance : Inhabited LiveVarSet where default := {} def mkLiveVarSet (x : VarId) : LiveVarSet := - TreeSet.empty.insert x + RBTree.empty.insert x namespace LiveVars @@ -107,10 +106,10 @@ private def collectArgs (as : Array Arg) : Collector := collectArray as collectArg private def accumulate (s' : LiveVarSet) : Collector := - fun s => s'.foldl (fun s x => s.insert x) s + fun s => s'.fold (fun s x => s.insert x) s private def collectJP (m : JPLiveVarMap) (j : JoinPointId) : Collector := - match m.get? j with + match m.find? 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 f2759bca9214c..32997d302ba27 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.get? x with + match m.find? x with | some y => y | none => x diff --git a/src/Lean/Compiler/IR/RC.lean b/src/Lean/Compiler/IR/RC.lean index 6feab8f65de2e..79d9b09e4d27f 100644 --- a/src/Lean/Compiler/IR/RC.lean +++ b/src/Lean/Compiler/IR/RC.lean @@ -15,15 +15,13 @@ This transformation is applied before lower level optimizations that introduce the instructions `release` and `set` -/ -open Std (TreeMap) - structure VarInfo where ref : Bool := true -- true if the variable may be a reference (aka pointer) at runtime persistent : Bool := false -- true if the variable is statically known to be marked a Persistent at runtime consume : Bool := false -- true if the variable RC must be "consumed" deriving Inhabited -abbrev VarMap := TreeMap VarId VarInfo (fun x y => compare x.idx y.idx) +abbrev VarMap := RBMap VarId VarInfo (fun x y => compare x.idx y.idx) structure Context where env : Environment @@ -38,7 +36,7 @@ def getDecl (ctx : Context) (fid : FunId) : Decl := | none => unreachable! def getVarInfo (ctx : Context) (x : VarId) : VarInfo := - match ctx.varMap.get? x with + match ctx.varMap.find? x with | some info => info | none => unreachable! @@ -48,7 +46,7 @@ def getJPParams (ctx : Context) (j : JoinPointId) : Array Param := | none => unreachable! def getJPLiveVars (ctx : Context) (j : JoinPointId) : LiveVarSet := - match ctx.jpLiveVarMap.get? j with + match ctx.jpLiveVarMap.find? j with | some s => s | none => {} @@ -70,12 +68,12 @@ private def updateRefUsingCtorInfo (ctx : Context) (x : VarId) (c : CtorInfo) : else let m := ctx.varMap { ctx with - varMap := match m.get? x with + varMap := match m.find? x with | some info => m.insert x { info with ref := false } -- I really want a Lenses library + notation | none => m } private def addDecForAlt (ctx : Context) (caseLiveVars altLiveVars : LiveVarSet) (b : FnBody) : FnBody := - caseLiveVars.foldl (init := b) fun b x => + caseLiveVars.fold (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` -/ @@ -157,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.get? x with + | Expr.proj _ x => match m.find? 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 6fd9f7bc95d7e..73e2d67150c58 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).get? fvarId₂ |>.getD fvarId₂ + let fvarId₂ := (← read).find? 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 ed7457be6180f..5d216c29796b3 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.get? fvarId | return .top + let some val := (← read).assignment.find? fvarId | return .top return val def evalArg (arg : Arg) : FixParamM AbsValue := do diff --git a/src/Lean/Compiler/LCNF/JoinPoints.lean b/src/Lean/Compiler/LCNF/JoinPoints.lean index 656e4507a965c..9046b5d6a2796 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.get! jp |>.contains var + return (← read).jpScopes.find! 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.get? fn then + if let some knownArgs := (← get).jpJmpArgs.find? 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.get? decl.fvarId then + if let some reducibleArgs := (← read).jpJmpArgs.find? 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.get! fn + let reducibleArgs := (← read).jpJmpArgs.find! 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 02802fd60bfd8..e2fb96fab0f6d 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).get? fvarId then + if let some mask := (← read).find? 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 30c3216e77cd0..e9cc5cc3100e4 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.get? param.fvarId then + if let some binderName := r.find? 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.get? decl.fvarId then + if let some binderName := r.find? 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 FunDeclCore.applyRenaming (decl : FunDecl) (r : Renaming) : CompilerM FunDecl := do - if let some binderName := r.get? decl.fvarId then + if let some binderName := r.find? 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 76624e266f76b..d6cb3f222bda3 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.get? fvarId + | none => return (← read).discrCtorMap.find? 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 4adeeb4133d54..8413bd47c9d5d 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).get? fvarId then + if let some info := (← get).find? 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).get? decl.fvarId | return none + let some info := (← read).find? 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).get? fvarId | return none - let some info := (← read).get? fvarId | return none + let some ctorJpAltMap := (← get).find? fvarId | return none + let some info := (← read).find? 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 ff5b57f927489..bd3801c1c2886 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.get? fvarId with + match m.find? 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 52384060cf67b..06ec970439220 100644 --- a/src/Lean/Compiler/LCNF/ToLCNF.lean +++ b/src/Lean/Compiler/LCNF/ToLCNF.lean @@ -64,7 +64,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.foldl (init := result) fun result _ altJp => .jp altJp result + let result := s.fold (init := result) fun result _ altJp => .jp altJp result return .jp jpDecl result where visitAlts (alts : Array Alt) : BindCasesM (Array Alt) := @@ -97,7 +97,7 @@ where if binderName.getPrefix == `_alt then if let some funDecl ← findFun? f then eraseLetDecl decl - if let some altJp := (← get).get? f then + if let some altJp := (← get).find? f then /- We already have an auxiliary join point for `f`, then, we just use it. -/ return .jmp altJp.fvarId args else @@ -128,7 +128,7 @@ where return .jmp altJp.fvarId args | _ => pure () let k ← go k - if let some altJp := (← get).get? decl.fvarId then + if let some altJp := (← get).find? 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.lean b/src/Lean/Data.lean index 97c8966e9a4d7..9f6a17d2d71d8 100644 --- a/src/Lean/Data.lean +++ b/src/Lean/Data.lean @@ -27,5 +27,6 @@ import Lean.Data.SMap import Lean.Data.Trie import Lean.Data.Xml import Lean.Data.NameTrie +import Lean.Data.RBTree import Lean.Data.RBMap import Lean.Data.RArray diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean index 1c2b14c7c12f0..8efce0000d28d 100644 --- a/src/Lean/Data/Json/Basic.lean +++ b/src/Lean/Data/Json/Basic.lean @@ -10,10 +10,8 @@ import Init.Data.OfScientific import Init.Data.Hashable import Lean.Data.RBMap import Init.Data.ToString.Macro -import Std.Data.TreeMap.Raw namespace Lean -open Std (TreeMap.Raw) -- mantissa * 10^-exponent structure JsonNumber where @@ -183,7 +181,7 @@ inductive Json where -- 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 : TreeMap.Raw String Json compare) + | obj (kvPairs : RBNode String (fun _ => Json)) deriving Inhabited namespace Json @@ -198,10 +196,10 @@ private partial def beq' : Json → Json → Bool a == b | obj a, obj b => let _ : BEq Json := ⟨beq'⟩ - let szA := a.foldl (init := 0) (fun a _ _ => a + 1) - let szB := b.foldl (init := 0) (fun a _ _ => a + 1) + let szA := a.fold (init := 0) (fun a _ _ => a + 1) + let szB := b.fold (init := 0) (fun a _ _ => a + 1) szA == szB && a.all fun field fa => - match b.get? field with + match b.find compare field with | none => false | some fb => fa == fb | _, _ => false @@ -217,7 +215,7 @@ 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.foldl (init := 7) fun r k v => mixHash r <| mixHash (hash k) (hash' v) + mixHash 29 <| kvPairs.fold (init := 7) fun r k v => mixHash r <| mixHash (hash k) (hash' v) instance : Hashable Json where hash := hash' @@ -225,9 +223,9 @@ instance : Hashable Json where -- 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 := TreeMap.Raw.empty + let mut kvPairs := RBNode.leaf for ⟨k, v⟩ in o do - kvPairs := kvPairs.insert k v + kvPairs := kvPairs.insert compare k v kvPairs instance : Coe Nat Json := ⟨fun n => Json.num n⟩ @@ -240,7 +238,7 @@ def isNull : Json -> Bool | null => true | _ => false -def getObj? : Json → Except String (TreeMap.Raw String Json compare) +def getObj? : Json → Except String (RBNode String (fun _ => Json)) | obj kvs => return kvs | _ => throw "object expected" @@ -270,7 +268,7 @@ def getNum? : Json → Except String JsonNumber def getObjVal? : Json → String → Except String Json | obj kvs, k => - match kvs.get? k with + match kvs.find compare k with | some v => return v | none => throw s!"property not found: {k}" | _ , _ => throw "object expected" @@ -286,7 +284,7 @@ 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 k v + | obj kvs, k, v => obj <| kvs.insert compare k v | _ , _, _ => panic! "Json.setObjVal!: not an object: {j}" open Lean.RBNode in @@ -295,15 +293,15 @@ If `o₁` is not a json object, `o₂` will be returned. -/ def mergeObj : Json → Json → Json | obj kvs₁, obj kvs₂ => - obj <| kvs₂.foldl TreeMap.Raw.insert kvs₁ + obj <| fold (insert compare) kvs₁ kvs₂ | _, j₂ => j₂ inductive Structured where | arr (elems : Array Json) - | obj (kvPairs : TreeMap.Raw String Json compare) + | obj (kvPairs : RBNode String (fun _ => Json)) instance : Coe (Array Json) Structured := ⟨Structured.arr⟩ -instance : Coe (TreeMap.Raw String Json compare) Structured := ⟨Structured.obj⟩ +instance : Coe (RBNode String (fun _ => 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 1526eea337ea2..a6774aff3ddda 100644 --- a/src/Lean/Data/Json/FromToJson.lean +++ b/src/Lean/Data/Json/FromToJson.lean @@ -9,7 +9,6 @@ import Lean.Data.Json.Basic import Lean.Data.Json.Printer namespace Lean -open Std (TreeMap) universe u @@ -141,13 +140,13 @@ instance : FromJson Float where | (Json.num jn) => Except.ok jn.toFloat | _ => Except.error "Expected a number or a string 'Infinity', '-Infinity', 'NaN'." -instance [ToJson α] : ToJson (TreeMap.Raw String α compare) where - toJson m := Json.obj <| TreeMap.Raw.map (fun _ => toJson) <| m +instance [ToJson α] : ToJson (RBMap String α cmp) where + toJson m := Json.obj <| RBNode.map (fun _ => toJson) <| m.val -instance {cmp} [FromJson α] : FromJson (TreeMap.Raw String α cmp) where +instance {cmp} [FromJson α] : FromJson (RBMap String α cmp) where fromJson? j := do let o ← j.getObj? - o.foldlM (fun x k v => x.insert k <$> fromJson? v) ∅ + o.foldM (fun x k v => x.insert k <$> fromJson? v) ∅ namespace Json diff --git a/src/Lean/Data/Json/Parser.lean b/src/Lean/Data/Json/Parser.lean index 550739fa83a43..4d3592525e90e 100644 --- a/src/Lean/Data/Json/Parser.lean +++ b/src/Lean/Data/Json/Parser.lean @@ -6,11 +6,11 @@ Authors: Gabriel Ebner, Marc Huisinga -/ prelude import Lean.Data.Json.Basic +import Lean.Data.RBMap import Std.Internal.Parsec open Std.Internal.Parsec open Std.Internal.Parsec.String -open Std (TreeMap.Raw) namespace Lean.Json.Parser @@ -183,7 +183,7 @@ mutual else fail "unexpected character in array" - partial def objectCore (kvs : TreeMap.Raw String Json compare) : Parser (TreeMap.Raw String Json compare) := do + partial def objectCore (kvs : RBNode String (fun _ => Json)) : Parser (RBNode String (fun _ => Json)) := do lookahead (fun c => c == '"') "\""; skip; let k ← str; ws lookahead (fun c => c == ':') ":"; skip; ws @@ -191,10 +191,10 @@ mutual let c ← any if c == '}' then ws - return kvs.insert k v + return kvs.insert compare k v else if c == ',' then ws - objectCore (kvs.insert k v) + objectCore (kvs.insert compare k v) else fail "unexpected character in object" @@ -214,9 +214,9 @@ mutual let c ← peek! if c == '}' then skip; ws - return Json.obj ∅ + return Json.obj (RBNode.leaf) else - let kvs ← objectCore ∅ + let kvs ← objectCore RBNode.leaf 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 ac797179b0827..d58f5fac298ad 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.foldl (fun acc k j => renderKV k j :: acc) []) ("," ++ Format.line); + let kvs := Format.joinSep (kvs.fold (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.foldl (init := []) (fun acc k j => objectField k j :: acc) ++ [objectEnd] ++ is) + | obj kvs => go (acc ++ "{") (kvs.fold (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/JsonRpc.lean b/src/Lean/Data/JsonRpc.lean index 0ca95ae784c77..24165deb5fb73 100644 --- a/src/Lean/Data/JsonRpc.lean +++ b/src/Lean/Data/JsonRpc.lean @@ -6,6 +6,7 @@ Authors: Marc Huisinga, Wojciech Nawrocki -/ prelude import Init.System.IO +import Lean.Data.RBTree import Lean.Data.Json /-! Implementation of JSON-RPC 2.0 (https://www.jsonrpc.org/specification) diff --git a/src/Lean/Data/Lsp/Basic.lean b/src/Lean/Data/Lsp/Basic.lean index ff259a6813214..98e80e35e3cf8 100644 --- a/src/Lean/Data/Lsp/Basic.lean +++ b/src/Lean/Data/Lsp/Basic.lean @@ -17,7 +17,6 @@ namespace Lean namespace Lsp open Json -open Std (TreeMap) abbrev DocumentUri := String @@ -250,7 +249,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 (TreeMap.Raw DocumentUri TextEditBatch compare) := none + changes? : Option (RBMap DocumentUri TextEditBatch compare) := 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 @@ -271,7 +270,7 @@ structure WorkspaceEdit where Whether clients honor this property depends on the client capability `workspace.changeAnnotationSupport`. -/ - changeAnnotations? : Option (TreeMap.Raw String ChangeAnnotation compare) := none + changeAnnotations? : Option (RBMap String ChangeAnnotation compare) := none deriving ToJson, FromJson namespace WorkspaceEdit diff --git a/src/Lean/Data/Lsp/Internal.lean b/src/Lean/Data/Lsp/Internal.lean index df38c6fbb92a7..5589f3d9360bc 100644 --- a/src/Lean/Data/Lsp/Internal.lean +++ b/src/Lean/Data/Lsp/Internal.lean @@ -162,7 +162,7 @@ instance : ToJson ModuleRefs where instance : FromJson ModuleRefs where fromJson? j := do let node ← j.getObj? - node.foldlM (init := Std.HashMap.empty) fun m k v => + node.foldM (init := Std.HashMap.empty) fun m k v => return m.insert (← RefIdent.fromJson? (← Json.parse k)) (← fromJson? v) /-- diff --git a/src/Lean/Data/NameMap.lean b/src/Lean/Data/NameMap.lean index e604a172892f6..04cd225102cab 100644 --- a/src/Lean/Data/NameMap.lean +++ b/src/Lean/Data/NameMap.lean @@ -6,17 +6,15 @@ Author: Leonardo de Moura prelude import Std.Data.HashSet.Basic import Lean.Data.HashSet +import Lean.Data.RBMap +import Lean.Data.RBTree import Lean.Data.SSet import Lean.Data.Name -import Std.Data.TreeMap.Basic -import Std.Data.TreeSet.AdditionalOperations - namespace Lean -open Std (TreeMap TreeSet) -def NameMap (α : Type) := TreeMap Name α Name.quickCmp +def NameMap (α : Type) := RBMap Name α Name.quickCmp -@[inline] def mkNameMap (α : Type) : NameMap α := TreeMap.empty +@[inline] def mkNameMap (α : Type) : NameMap α := mkRBMap Name α Name.quickCmp namespace NameMap variable {α : Type} @@ -26,47 +24,47 @@ instance (α : Type) : EmptyCollection (NameMap α) := ⟨mkNameMap α⟩ instance (α : Type) : Inhabited (NameMap α) where default := {} -def insert (m : NameMap α) (n : Name) (a : α) := TreeMap.insert m n a +def insert (m : NameMap α) (n : Name) (a : α) := RBMap.insert m n a -def contains (m : NameMap α) (n : Name) : Bool := TreeMap.contains m n +def contains (m : NameMap α) (n : Name) : Bool := RBMap.contains m n -def find? (m : NameMap α) (n : Name) : Option α := TreeMap.get? m n +def find? (m : NameMap α) (n : Name) : Option α := RBMap.find? m n instance : ForIn m (NameMap α) (Name × α) := - inferInstanceAs (ForIn _ (TreeMap ..) ..) + 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 α := TreeMap.filter f m +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 β := TreeMap.filterMap f m +def filterMap (f : Name → α → Option β) (m : NameMap α) : NameMap β := RBMap.filterMap f m end NameMap -def NameSet := TreeSet Name Name.quickCmp +def NameSet := RBTree Name Name.quickCmp namespace NameSet -def empty : NameSet := TreeSet.empty +def empty : NameSet := mkRBTree Name Name.quickCmp instance : EmptyCollection NameSet := ⟨empty⟩ instance : Inhabited NameSet := ⟨empty⟩ -def insert (s : NameSet) (n : Name) : NameSet := TreeSet.insert s n -def contains (s : NameSet) (n : Name) : Bool := TreeSet.contains s n +def insert (s : NameSet) (n : Name) : NameSet := RBTree.insert s n +def contains (s : NameSet) (n : Name) : Bool := RBMap.contains s n instance : ForIn m NameSet Name := - inferInstanceAs (ForIn _ (TreeSet ..) ..) + inferInstanceAs (ForIn _ (RBTree ..) ..) /-- The union of two `NameSet`s. -/ def append (s t : NameSet) : NameSet := - s.merge t + 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 := TreeSet.filter f s +def filter (f : Name → Bool) (s : NameSet) : NameSet := RBTree.filter f s end NameSet diff --git a/src/Lean/Data/Options.lean b/src/Lean/Data/Options.lean index 713750a16222e..e8d7dd2278dc7 100644 --- a/src/Lean/Data/Options.lean +++ b/src/Lean/Data/Options.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.foldl + pure $ decls.fold (fun (r : Array (Name × OptionDecl)) k v => r.push (k, v)) #[] diff --git a/src/Lean/Data/RBMap.lean b/src/Lean/Data/RBMap.lean index e99ec6b0ab22a..2ac041f43c757 100644 --- a/src/Lean/Data/RBMap.lean +++ b/src/Lean/Data/RBMap.lean @@ -279,9 +279,6 @@ def isSingleton (t : RBMap α β cmp) : Bool := @[inline] def fold (f : σ → α → β → σ) : (init : σ) → RBMap α β cmp → σ | b, ⟨t, _⟩ => t.fold f b -@[inline] def foldl (f : σ → α → β → σ) : (init : σ) → RBMap α β cmp → σ - | b, ⟨t, _⟩ => t.fold f b - @[inline] def revFold (f : σ → α → β → σ) : (init : σ) → RBMap α β cmp → σ | b, ⟨t, _⟩ => t.revFold f b diff --git a/src/Lean/Data/RBTree.lean b/src/Lean/Data/RBTree.lean new file mode 100644 index 0000000000000..4265bb1ace6d6 --- /dev/null +++ b/src/Lean/Data/RBTree.lean @@ -0,0 +1,127 @@ +/- +Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Lean.Data.RBMap +namespace Lean +universe u v w + +def RBTree (α : Type u) (cmp : α → α → Ordering) : Type u := + RBMap α Unit cmp + +instance : Inhabited (RBTree α p) where + default := RBMap.empty + +@[inline] def mkRBTree (α : Type u) (cmp : α → α → Ordering) : RBTree α cmp := + mkRBMap α Unit cmp + +instance (α : Type u) (cmp : α → α → Ordering) : EmptyCollection (RBTree α cmp) := + ⟨mkRBTree α cmp⟩ + +namespace RBTree +variable {α : Type u} {β : Type v} {cmp : α → α → Ordering} + +@[inline] def empty : RBTree α cmp := + RBMap.empty + +@[inline] def depth (f : Nat → Nat → Nat) (t : RBTree α cmp) : Nat := + RBMap.depth f t + +@[inline] def fold (f : β → α → β) (init : β) (t : RBTree α cmp) : β := + RBMap.fold (fun r a _ => f r a) init t + +@[inline] def revFold (f : β → α → β) (init : β) (t : RBTree α cmp) : β := + RBMap.revFold (fun r a _ => f r a) init t + +@[inline] def foldM {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (t : RBTree α cmp) : m β := + RBMap.foldM (fun r a _ => f r a) init t + +@[inline] def forM {m : Type v → Type w} [Monad m] (f : α → m PUnit) (t : RBTree α cmp) : m PUnit := + t.foldM (fun _ a => f a) ⟨⟩ + +@[inline] protected def forIn [Monad m] (t : RBTree α cmp) (init : σ) (f : α → σ → m (ForInStep σ)) : m σ := + t.val.forIn init (fun a _ acc => f a acc) + +instance : ForIn m (RBTree α cmp) α where + forIn := RBTree.forIn + +@[inline] def isEmpty (t : RBTree α cmp) : Bool := + RBMap.isEmpty t + +@[specialize] def toList (t : RBTree α cmp) : List α := + t.revFold (fun as a => a::as) [] + +@[specialize] def toArray (t : RBTree α cmp) : Array α := + t.fold (fun as a => as.push a) #[] + +@[inline] protected def min (t : RBTree α cmp) : Option α := + match RBMap.min t with + | some ⟨a, _⟩ => some a + | none => none + +@[inline] protected def max (t : RBTree α cmp) : Option α := + match RBMap.max t with + | some ⟨a, _⟩ => some a + | none => none + +instance [Repr α] : Repr (RBTree α cmp) where + reprPrec t prec := Repr.addAppParen ("Lean.rbtreeOf " ++ repr t.toList) prec + +@[inline] def insert (t : RBTree α cmp) (a : α) : RBTree α cmp := + RBMap.insert t a () + +@[inline] def erase (t : RBTree α cmp) (a : α) : RBTree α cmp := + RBMap.erase t a + +@[specialize] def ofList : List α → RBTree α cmp + | [] => mkRBTree .. + | x::xs => (ofList xs).insert x + +@[inline] def find? (t : RBTree α cmp) (a : α) : Option α := + match RBMap.findCore? t a with + | some ⟨a, _⟩ => some a + | none => none + +@[inline] def contains (t : RBTree α cmp) (a : α) : Bool := + (t.find? a).isSome + +def fromList (l : List α) (cmp : α → α → Ordering) : RBTree α cmp := + l.foldl insert (mkRBTree α cmp) + +def fromArray (l : Array α) (cmp : α → α → Ordering) : RBTree α cmp := + l.foldl insert (mkRBTree α cmp) + +@[inline] def all (t : RBTree α cmp) (p : α → Bool) : Bool := + RBMap.all t (fun a _ => p a) + +@[inline] def any (t : RBTree α cmp) (p : α → Bool) : Bool := + RBMap.any t (fun a _ => p a) + +def subset (t₁ t₂ : RBTree α cmp) : Bool := + t₁.all fun a => (t₂.find? a).isSome + +def seteq (t₁ t₂ : RBTree α cmp) : Bool := + subset t₁ t₂ && subset t₂ t₁ + +def union (t₁ t₂ : RBTree α cmp) : RBTree α cmp := + if t₁.isEmpty then + t₂ + else + t₂.fold .insert t₁ + +def diff (t₁ t₂ : RBTree α cmp) : RBTree α cmp := + t₂.fold .erase t₁ + +/-- +`filter f m` returns the `RBTree` consisting of all +`x` in `m` where `f x` returns `true`. +-/ +def filter (f : α → Bool) (m : RBTree α cmp) : RBTree α cmp := + RBMap.filter (fun a _ => f a) m + +end RBTree + +def rbtreeOf {α : Type u} (l : List α) (cmp : α → α → Ordering) : RBTree α cmp := + RBTree.fromList l cmp diff --git a/src/Lean/Data/Trie.lean b/src/Lean/Data/Trie.lean index df0759f553452..d5457411995bc 100644 --- a/src/Lean/Data/Trie.lean +++ b/src/Lean/Data/Trie.lean @@ -16,7 +16,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 `TreeSet`. +search trees like `RBTree`. 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 9238bb0454afd..c683822ca1318 100644 --- a/src/Lean/Data/Xml/Basic.lean +++ b/src/Lean/Data/Xml/Basic.lean @@ -4,15 +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 namespace Lean namespace Xml -open Std (TreeMap) -def Attributes := TreeMap String String compare -instance : ToString Attributes := ⟨λ as => as.foldl (λ s n v => s ++ s!" {n}=\"{v}\"") ""⟩ +def Attributes := RBMap String String compare +instance : ToString Attributes := ⟨λ as => as.fold (λ 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 e619005d3ebd8..939bb3825f3d5 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 (.fromList attributes.toList compare) + return Element.Element name (RBMap.fromList attributes.toList compare) /-- https://www.w3.org/TR/xml/#NT-EmptyElemTag -/ def EmptyElemTag (elem : Array Content → Element) : Parser Element := do diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 0b669a89cef1a..8a308c7b66d00 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -1215,7 +1215,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 := (← read).auxDeclToFullName.get? localDecl.fvarId then + if let some localDeclFullName := (← read).auxDeclToFullName.find? 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 b6f434e341590..550ee9cbc8c62 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.foldlM (init := Array.mkEmpty st.consts.size) fun mods name => return mods.push (← findModuleOf? name) + let modules ← st.consts.foldM (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/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean index 108dfd54ca4d8..171ec7a939a32 100644 --- a/src/Lean/Elab/Deriving/Inhabited.lean +++ b/src/Lean/Elab/Deriving/Inhabited.lean @@ -9,9 +9,8 @@ import Lean.Elab.Deriving.Basic namespace Lean.Elab open Command Meta Parser Term -open Std (TreeSet) -private abbrev IndexSet := TreeSet Nat compare +private abbrev IndexSet := RBTree Nat compare private abbrev LocalInst2Index := FVarIdMap Nat private def implicitBinderF := Parser.Term.implicitBinder @@ -52,7 +51,7 @@ where let visit {ω} : StateRefT IndexSet (ST ω) Unit := e.forEachWhere Expr.isFVar fun e => let fvarId := e.fvarId! - match localInst2Index.get? fvarId with + match localInst2Index.find? 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 99ab53a8c44a0..57ba1d890cebd 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -17,7 +17,6 @@ namespace Lean.Elab.Term open Lean.Parser.Term open Meta open TSyntax.Compat -open Std (TreeMap) private def getDoSeqElems (doSeq : Syntax) : List Syntax := if doSeq.getKind == ``Parser.Term.doSeqBracketed then @@ -240,7 +239,7 @@ def Code.getRef? : Code → Option Syntax | .matchExpr ref .. => ref | .jmp ref .. => ref -abbrev VarSet := TreeMap Name Syntax Name.cmp +abbrev VarSet := RBMap Name Syntax Name.cmp /-- A code block, and the collection of variables updated by it. -/ structure CodeBlock where @@ -248,7 +247,7 @@ structure CodeBlock where uvars : VarSet := {} -- set of variables updated by `code` private def varSetToArray (s : VarSet) : Array Var := - s.foldl (fun xs _ x => xs.push x) #[] + s.fold (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)) " " @@ -541,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₁.foldl (·.insert ·) s₂ + s₁.fold (·.insert ·) s₂ /-- Given two code blocks `c₁` and `c₂`, make sure they have the same set of updated variables. @@ -1570,7 +1569,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.getD v.getId v + let uvars := uvars.map fun v => ctx.mutableVars.findD 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/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index c10160e2307cd..8e833da85fe07 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -649,7 +649,7 @@ private def modifyUsedFVars (f : UsedFVarsMap → UsedFVarsMap) : M Unit := modi -- merge s₂ into s₁ private def merge (s₁ s₂ : FVarIdSet) : M FVarIdSet := - s₂.foldlM (init := s₁) fun s₁ k => do + s₂.foldM (init := s₁) fun s₁ k => do if s₁.contains k then return s₁ else @@ -658,14 +658,14 @@ private def merge (s₁ s₂ : FVarIdSet) : M FVarIdSet := private def updateUsedVarsOf (fvarId : FVarId) : M Unit := do let usedFVarsMap ← getUsedFVarsMap - match usedFVarsMap.get? fvarId with + match usedFVarsMap.find? fvarId with | none => return () | some fvarIds => - let fvarIdsNew ← fvarIds.foldlM (init := fvarIds) fun fvarIdsNew fvarId' => do + let fvarIdsNew ← fvarIds.foldM (init := fvarIds) fun fvarIdsNew fvarId' => do if fvarId == fvarId' then return fvarIdsNew else - match usedFVarsMap.get? fvarId' with + match usedFVarsMap.find? 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. @@ -698,8 +698,8 @@ private def mkFreeVarMap [Monad m] [MonadMCtx m] let mut freeVarMap := {} for toLift in letRecsToLift do let lctx := toLift.lctx - let fvarIdsSet := usedFVarsMap.get? toLift.fvarId |>.get! - let fvarIds := fvarIdsSet.foldl (init := #[]) fun fvarIds fvarId => + let fvarIdsSet := usedFVarsMap.find? toLift.fvarId |>.get! + let fvarIds := fvarIdsSet.fold (init := #[]) fun fvarIds fvarId => if lctx.contains fvarId && !recFVarIds.contains fvarId then fvarIds.push fvarId else @@ -724,7 +724,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.foldl (init := toProcess) fun toProcess fvarId => + s.fvarSet.fold (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) @@ -803,7 +803,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.get? localDecl.fvarId then + if let some (userName, bi) := userNameBinderInfoMap.find? localDecl.fvarId then localDecl.setBinderInfo bi |>.setUserName userName else localDecl @@ -833,7 +833,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.get? toLift.fvarId).get!) + result := result.push (← mkLetRecClosureFor toLift (freeVarMap.find? toLift.fvarId).get!) return result.toList /-- Mapping from FVarId of mutually recursive functions being defined to "closure" expression. -/ @@ -864,7 +864,7 @@ def Replacement.apply (r : Replacement) (e : Expr) : Expr := e else e.replace fun e => match e with - | .fvar fvarId => match r.get? fvarId with + | .fvar fvarId => match r.find? fvarId with | some c => some c | _ => none | _ => none diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean index 588605eb676e6..0eaf990a13859 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean @@ -23,7 +23,6 @@ open Std.Sat open Std.Tactic.BVDecide open Std.Tactic.BVDecide.Reflect open Lean.Meta -open Std (TreeMap) /-- Given: @@ -38,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 (TreeMap Nat Bool Ord.compare) := {} + let mut sparseMap : Std.HashMap Nat (RBMap Nat Bool Ord.compare) := {} let filter bvBit _ := let (_, _, synthetic) := atomsAssignment.get! bvBit.var !synthetic diff --git a/src/Lean/Elab/Tactic/BVDecide/LRAT/Trim.lean b/src/Lean/Elab/Tactic/BVDecide/LRAT/Trim.lean index 21a8e18a64f61..ea2e6b3509d16 100644 --- a/src/Lean/Elab/Tactic/BVDecide/LRAT/Trim.lean +++ b/src/Lean/Elab/Tactic/BVDecide/LRAT/Trim.lean @@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ prelude +import Lean.Data.RBMap import Std.Tactic.BVDecide.LRAT.Actions import Std.Data.HashMap -import Std.Data.TreeMap.Basic /-! This module implements the LRAT trimming algorithm described in section 4 of @@ -17,7 +17,7 @@ This module implements the LRAT trimming algorithm described in section 4 of namespace Lean.Elab.Tactic.BVDecide namespace LRAT -open Std (TreeMap) +open Lean (RBMap) open Std.Tactic.BVDecide.LRAT (IntAction) namespace trim @@ -43,7 +43,7 @@ structure State where /-- The set of used proof step ids. -/ - used : TreeMap Nat Unit compare := {} + used : RBMap Nat Unit compare := {} /-- A mapping from old proof step ids to new ones. Used such that the proof remains a sequence without gaps. @@ -108,7 +108,7 @@ def markUsed (id : Nat) : M Unit := do modify (fun s => { s with used := s.used.insert id () }) @[inline] -def getUsedSet : M (TreeMap Nat Unit Ord.compare) := do +def getUsedSet : M (RBMap Nat Unit Ord.compare) := do let s ← get return s.used diff --git a/src/Lean/Elab/Tactic/Doc.lean b/src/Lean/Elab/Tactic/Doc.lean index 158d52271dab8..011fabf5126d0 100644 --- a/src/Lean/Elab/Tactic/Doc.lean +++ b/src/Lean/Elab/Tactic/Doc.lean @@ -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.getD tag {} |>.insert tac) + mapping := mapping.insert tag (mapping.findD 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.getD tac {} |>.insert tag) + tacTags := tacTags.insert tac (tacTags.findD 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.getD tac {}, + tags := tacTags.findD tac {}, docString := ← findDocString? env tac, extensionDocs := getTacticExtensions env tac } diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index e6d0518dbb65b..cd228aac3f5d7 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -802,7 +802,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.get? mvarErrorInfo.mvarId with + match (← get).mvarArgNames.find? mvarErrorInfo.mvarId with | none => return msg | some argName => return if argName.hasMacroScopes then msg else msg ++ extra ++ m!" '{argName}'" @@ -1252,7 +1252,7 @@ private def postponeElabTermCore (stx : Syntax) (expectedType? : Option Expr) : return mvar def getSyntheticMVarDecl? (mvarId : MVarId) : TermElabM (Option SyntheticMVarDecl) := - return (← get).syntheticMVars.get? mvarId + return (← get).syntheticMVars.find? mvarId register_builtin_option debug.byAsSorry : Bool := { defValue := false @@ -1621,7 +1621,7 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do let localDecl ← localDecl? if localDecl.isAuxDecl then guard (!skipAuxDecl) - if let some fullDeclName := auxDeclToFullName.get? localDecl.fvarId then + if let some fullDeclName := auxDeclToFullName.find? localDecl.fvarId then matchAuxRecDecl? localDecl fullDeclName givenNameView else matchLocalDecl? localDecl givenName diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean index 768491389bd54..53f43b58c430e 100644 --- a/src/Lean/Expr.lean +++ b/src/Lean/Expr.lean @@ -9,11 +9,8 @@ import Lean.Data.KVMap import Lean.Data.SMap import Lean.Level import Std.Data.HashSet.Basic -import Std.Data.TreeMap.Basic -import Std.Data.TreeSet.Basic namespace Lean -open Std /-- Literal values for `Expr`. -/ inductive Literal where @@ -236,13 +233,13 @@ instance : Repr FVarId where /-- A set of unique free variable identifiers. This is a persistent data structure implemented using red-black trees. -/ -def FVarIdSet := TreeSet FVarId (Name.quickCmp ·.name ·.name) +def FVarIdSet := RBTree FVarId (Name.quickCmp ·.name ·.name) deriving Inhabited, EmptyCollection -instance : ForIn m FVarIdSet FVarId := inferInstanceAs (ForIn _ (TreeSet ..) ..) +instance : ForIn m FVarIdSet FVarId := inferInstanceAs (ForIn _ (RBTree ..) ..) def FVarIdSet.insert (s : FVarIdSet) (fvarId : FVarId) : FVarIdSet := - TreeSet.insert s fvarId + RBTree.insert s fvarId /-- A set of unique free variable identifiers implemented using hashtables. @@ -254,12 +251,12 @@ 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) := TreeMap FVarId α (Name.quickCmp ·.name ·.name) +def FVarIdMap (α : Type) := RBMap FVarId α (Name.quickCmp ·.name ·.name) def FVarIdMap.insert (s : FVarIdMap α) (fvarId : FVarId) (a : α) : FVarIdMap α := - TreeMap.insert s fvarId a + RBMap.insert s fvarId a -instance : EmptyCollection (FVarIdMap α) := inferInstanceAs (EmptyCollection (TreeMap ..)) +instance : EmptyCollection (FVarIdMap α) := inferInstanceAs (EmptyCollection (RBMap ..)) instance : Inhabited (FVarIdMap α) where default := {} @@ -272,22 +269,22 @@ structure MVarId where instance : Repr MVarId where reprPrec n p := reprPrec n.name p -def MVarIdSet := TreeSet MVarId (Name.quickCmp ·.name ·.name) +def MVarIdSet := RBTree MVarId (Name.quickCmp ·.name ·.name) deriving Inhabited, EmptyCollection def MVarIdSet.insert (s : MVarIdSet) (mvarId : MVarId) : MVarIdSet := - TreeSet.insert s mvarId + RBTree.insert s mvarId -instance : ForIn m MVarIdSet MVarId := inferInstanceAs (ForIn _ (TreeSet ..) ..) +instance : ForIn m MVarIdSet MVarId := inferInstanceAs (ForIn _ (RBTree ..) ..) -def MVarIdMap (α : Type) := TreeMap MVarId α (Name.quickCmp ·.name ·.name) +def MVarIdMap (α : Type) := RBMap MVarId α (Name.quickCmp ·.name ·.name) def MVarIdMap.insert (s : MVarIdMap α) (mvarId : MVarId) (a : α) : MVarIdMap α := - TreeMap.insert s mvarId a + RBMap.insert s mvarId a -instance : EmptyCollection (MVarIdMap α) := inferInstanceAs (EmptyCollection (TreeMap ..)) +instance : EmptyCollection (MVarIdMap α) := inferInstanceAs (EmptyCollection (RBMap ..)) -instance : ForIn m (MVarIdMap α) (MVarId × α) := inferInstanceAs (ForIn _ (TreeMap ..) ..) +instance : ForIn m (MVarIdMap α) (MVarId × α) := inferInstanceAs (ForIn _ (RBMap ..) ..) instance : Inhabited (MVarIdMap α) where default := {} diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean index 1591f14e7e671..dd3be8a93bad3 100644 --- a/src/Lean/Level.lean +++ b/src/Lean/Level.lean @@ -12,14 +12,11 @@ import Lean.Data.PersistentHashSet import Lean.Hygiene import Lean.Data.Name import Lean.Data.Format -import Std.Data.TreeMap.Basic -import Std.Data.TreeSet.Basic def Nat.imax (n m : Nat) : Nat := if m = 0 then 0 else Nat.max n m namespace Lean -open Std (TreeMap TreeSet) /-- Cached hash code, cached results, and other data for `Level`. @@ -77,16 +74,16 @@ abbrev LMVarId := LevelMVarId instance : Repr LMVarId where reprPrec n p := reprPrec n.name p -def LMVarIdSet := TreeSet LMVarId (Name.quickCmp ·.name ·.name) +def LMVarIdSet := RBTree LMVarId (Name.quickCmp ·.name ·.name) deriving Inhabited, EmptyCollection -instance : ForIn m LMVarIdSet LMVarId := inferInstanceAs (ForIn _ (TreeSet ..) ..) +instance : ForIn m LMVarIdSet LMVarId := inferInstanceAs (ForIn _ (RBTree ..) ..) -def LMVarIdMap (α : Type) := TreeMap LMVarId α (Name.quickCmp ·.name ·.name) +def LMVarIdMap (α : Type) := RBMap LMVarId α (Name.quickCmp ·.name ·.name) -instance : EmptyCollection (LMVarIdMap α) := inferInstanceAs (EmptyCollection (TreeMap ..)) +instance : EmptyCollection (LMVarIdMap α) := inferInstanceAs (EmptyCollection (RBMap ..)) -instance : ForIn m (LMVarIdMap α) (LMVarId × α) := inferInstanceAs (ForIn _ (TreeMap ..) ..) +instance : ForIn m (LMVarIdMap α) (LMVarId × α) := inferInstanceAs (ForIn _ (RBMap ..) ..) instance : Inhabited (LMVarIdMap α) where default := {} diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 7416ec16c7e3d..ef7014d63fce3 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -443,7 +443,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.merge l₂.loggedKinds + loggedKinds := l₁.loggedKinds.union l₂.loggedKinds instance : Append MessageLog := ⟨MessageLog.append⟩ diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean index e2824b75de556..d7802c3d4c1ad 100644 --- a/src/Lean/Meta/Instances.lean +++ b/src/Lean/Meta/Instances.lean @@ -10,7 +10,6 @@ import Lean.Meta.DiscrTree import Lean.Meta.CollectMVars namespace Lean.Meta -open Std (TreeSet) register_builtin_option synthInstance.checkSynthOrder : Bool := { defValue := true @@ -273,7 +272,7 @@ structure DefaultInstanceEntry where instanceName : Name priority : Nat -abbrev PrioritySet := TreeSet Nat (fun x y => compare y x) +abbrev PrioritySet := RBTree Nat (fun x y => compare y x) structure DefaultInstances where defaultInstances : NameMap (List (Name × Nat)) := {} diff --git a/src/Lean/Meta/Match/MVarRenaming.lean b/src/Lean/Meta/Match/MVarRenaming.lean index c140b383befba..f177c8dc87b56 100644 --- a/src/Lean/Meta/Match/MVarRenaming.lean +++ b/src/Lean/Meta/Match/MVarRenaming.lean @@ -15,11 +15,11 @@ structure MVarRenaming where def MVarRenaming.isEmpty (s : MVarRenaming) : Bool := s.map.isEmpty -def MVarRenaming.get? (s : MVarRenaming) (mvarId : MVarId) : Option MVarId := - s.map.get? mvarId +def MVarRenaming.find? (s : MVarRenaming) (mvarId : MVarId) : Option MVarId := + s.map.find? mvarId def MVarRenaming.find! (s : MVarRenaming) (mvarId : MVarId) : MVarId := - (s.get? mvarId).get! + (s.find? mvarId).get! def MVarRenaming.insert (s : MVarRenaming) (mvarId mvarId' : MVarId) : MVarRenaming := { s with map := s.map.insert mvarId mvarId' } @@ -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.get? mvarId with + | Expr.mvar mvarId => match s.map.find? 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 6be2c00a266f2..9c08c3f01ba13 100644 --- a/src/Lean/Meta/Match/MatchEqs.lean +++ b/src/Lean/Meta/Match/MatchEqs.lean @@ -515,7 +515,7 @@ where for i in [6:args.size] do let arg := argsNew[i]! if arg.isFVar then - match (← read).get? arg.fvarId! with + match (← read).find? arg.fvarId! with | some (altNew, _, _) => argsNew := argsNew.set! i altNew trace[Meta.Match.matchEqs] "arg: {arg} : {← inferType arg}, altNew: {altNew} : {← inferType altNew}" @@ -576,7 +576,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.get? alt.fvarId! | unreachable! + let some (_, numParams, argMask) := m.find? 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 @@ -600,7 +600,7 @@ where return .done (← convertCastEqRec e) else let Expr.fvar fvarId .. := e.getAppFn | return .continue - let some (altNew, numParams, argMask) := (← read).get? fvarId | return .continue + let some (altNew, numParams, argMask) := (← read).find? 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/Cases.lean b/src/Lean/Meta/Tactic/Grind/Cases.lean index 44f92c2c40ad6..448b70064b9ca 100644 --- a/src/Lean/Meta/Tactic/Grind/Cases.lean +++ b/src/Lean/Meta/Tactic/Grind/Cases.lean @@ -7,7 +7,6 @@ prelude import Lean.Meta.Tactic.Cases namespace Lean.Meta.Grind -open Std (TreeSet) /-- Types that `grind` will case-split on. -/ structure CasesTypes where @@ -24,7 +23,7 @@ structure CasesEntry where The goal is to reduce noise in the tactic generated by `grind?` -/ private def builtinEagerCases : NameSet := - TreeSet.fromList [``And, ``Exists, ``True, ``False, ``Unit, ``Empty] + RBTree.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 78412fe126cb1..0e2217cfab8a1 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean @@ -16,7 +16,6 @@ import Lean.Meta.Eqns import Lean.Meta.Tactic.Grind.Util namespace Lean.Meta.Grind -open Std (TreeSet) def mkOffsetPattern (pat : Expr) (k : Nat) : Expr := mkApp2 (mkConst ``Grind.offset) pat (mkRawNatLit k) @@ -480,21 +479,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 := TreeSet.fromList <| xs.toList.map (·.fvarId!) + let thmVars : FVarIdSet := RBTree.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 := TreeSet.fromList patternVars + let mut fvarsFound : FVarIdSet := RBTree.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 := TreeSet.fromList patternVars + let mut processed : FVarIdSet := RBTree.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 1c72eda5908bc..f395c3fe89dce 100644 --- a/src/Lean/Meta/Tactic/Grind/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Proof.lean @@ -8,7 +8,6 @@ import Init.Grind.Lemmas import Lean.Meta.Tactic.Grind.Types namespace Lean.Meta.Grind -open Std (TreeMap) private def isEqProof (h : Expr) : MetaM Bool := do return (← whnfD (← inferType h)).isAppOf ``Eq @@ -50,7 +49,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 : TreeMap Nat Expr compare := {} + let mut visited : RBMap Nat Expr compare := {} let mut it := lhs -- Mark elements found following the path from `lhs` to the root. repeat @@ -62,7 +61,7 @@ private def findCommon (lhs rhs : Expr) : GoalM Expr := do it := rhs repeat let n ← getENode it - if let some common := visited.get? n.idx then + if let some common := visited.find? 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 7f6391b054346..a9ec6b33637c5 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -21,7 +21,6 @@ import Lean.Meta.Tactic.Grind.Arith.Types import Lean.Meta.Tactic.Grind.EMatchTheorem namespace Lean.Meta.Grind -open Std (TreeSet) /-- We use this auxiliary constant to mark delayed congruence proofs. -/ def congrPlaceholderProof := mkConst (Name.mkSimple "[congruence]") @@ -390,7 +389,7 @@ instance : BEq (CongrKey enodes) where abbrev CongrTable (enodes : ENodeMap) := PHashSet (CongrKey enodes) -- Remark: we cannot use pointer addresses here because we have to traverse the tree. -abbrev ParentSet := TreeSet Expr Expr.quickComp +abbrev ParentSet := RBTree Expr Expr.quickComp abbrev ParentMap := PHashMap ENodeKey ParentSet /-- diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index 05cf08973a782..ada06f05764a8 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -785,7 +785,7 @@ where withReducible x private def updateUsedSimpsWithZetaDeltaCore (s : UsedSimps) (usedZetaDelta : FVarIdSet) : UsedSimps := - usedZetaDelta.foldl (init := s) fun s fvarId => + usedZetaDelta.fold (init := s) fun s fvarId => s.insert <| .fvar fvarId private def updateUsedSimpsWithZetaDelta (ctx : Context) (stats : Stats) : MetaM Stats := do diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index db4f08abd1e77..2b7f0984c39e1 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -58,7 +58,6 @@ tokens until the next command keyword on error. -/ namespace Lean.Parser -open Std (TreeMap) def dbgTraceStateFn (label : String) (p : ParserFn) : ParserFn := fun c s => @@ -1578,21 +1577,21 @@ def eoi : Parser := { } /-- A multimap indexed by tokens. Used for indexing parsers by their leading token. -/ -def TokenMap (α : Type) := TreeMap Name (List α) Name.quickCmp +def TokenMap (α : Type) := RBMap Name (List α) Name.quickCmp namespace TokenMap def insert (map : TokenMap α) (k : Name) (v : α) : TokenMap α := - match map.get? k with - | none => TreeMap.insert map k [v] - | some vs => TreeMap.insert map k (v::vs) + match map.find? k with + | none => RBMap.insert map k [v] + | some vs => RBMap.insert map k (v::vs) instance : Inhabited (TokenMap α) where - default := TreeMap.empty + default := RBMap.empty -instance : EmptyCollection (TokenMap α) := ⟨TreeMap.empty⟩ +instance : EmptyCollection (TokenMap α) := ⟨RBMap.empty⟩ -instance : ForIn m (TokenMap α) (Name × List α) := inferInstanceAs (ForIn _ (TreeMap ..) _) +instance : ForIn m (TokenMap α) (Name × List α) := inferInstanceAs (ForIn _ (RBMap ..) _) end TokenMap @@ -1673,7 +1672,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.get? n with + match map.find? n with | some as => (s, as) | _ => (s, []) match stx with @@ -1682,16 +1681,16 @@ def indexed {α : Type} (map : TokenMap α) (c : ParserContext) (s : ParserState match behavior with | .default => find identKind | .symbol => - match map.get? val with + match map.find? val with | some as => (s, as) | none => find identKind | .both => - match map.get? val with + match map.find? val with | some as => if val == identKind then (s, as) -- avoid running the same parsers twice else - match map.get? identKind with + match map.find? 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 6a5281fed6720..87acbcfe343cf 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).getD aliasName {} + return (← parserAliases2infoRef.get).findD 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 1f0e8639f3600..8b4d25cd073a2 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.foldl (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1) + es.fold (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.foldl (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1) + es.fold (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.foldl (init := #[]) (fun arr k v => arr.push (k, v)) + let arr := found.fold (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.getD decl {} |>.insert newTag) + addEntryFn := fun tags (decl, newTag) => tags.insert decl (tags.findD 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.getD x #[] |>.push ext), + addEntryFn := fun es (x, ext) => es.insert x (es.findD x #[] |>.push ext), exportEntriesFn := fun es => - es.foldl (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1) + es.fold (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 13ceb1cf6f849..d4305fdd27fec 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.getD x #[] |>.push rec), + addEntryFn := fun es (rec, xs) => xs.foldl (init := es) fun es x => es.insert x (es.findD x #[] |>.push rec), exportEntriesFn := fun es => - es.foldl (fun a src tgt => a.push (src, tgt)) #[] |>.qsort (Name.quickLt ·.1 ·.1) + es.fold (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 0b4f6306170ef..623ab4d2d1b19 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean @@ -163,7 +163,7 @@ def getExprKind : DelabM Name := do def getOptionsAtCurrPos : DelabM Options := do let ctx ← read let mut opts ← getOptions - if let some opts' := ctx.optionsPerPos.get? (← getPos) then + if let some opts' := ctx.optionsPerPos.find? (← getPos) then for (k, v) in opts' do opts := opts.insert k v return opts @@ -185,7 +185,7 @@ def withOptionAtCurrPos (k : Name) (v : DataValue) (x : DelabM α) : DelabM α : let pos ← getPos withReader (fun ctx => - let opts' := ctx.optionsPerPos.get? pos |>.getD {} |>.insert k v + let opts' := ctx.optionsPerPos.find? 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 bba4539c9482a..44a435655a32b 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -130,7 +130,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.get? pos |>.getD {} + let opts := posOpts.find? pos |>.getD {} posOpts := posOpts.insert pos (opts.insert k v) withReader ({ · with optionsPerPos := posOpts }) $ withMDataExpr x | _ => x diff --git a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean index a96f03bca3da7..30909660e47c1 100644 --- a/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean +++ b/src/Lean/PrettyPrinter/Delaborator/SubExpr.lean @@ -6,6 +6,7 @@ Authors: Sebastian Ullrich, Daniel Selsam, Wojciech Nawrocki prelude import Lean.Meta.Basic import Lean.SubExpr +import Lean.Data.RBMap /-! # Subexpr utilities for delaborator. @@ -14,17 +15,16 @@ in sync with the `Nat` "position" values that refer to them. -/ namespace Lean.PrettyPrinter.Delaborator -open Std (TreeMap) -abbrev OptionsPerPos := TreeMap SubExpr.Pos Options compare +abbrev OptionsPerPos := RBMap SubExpr.Pos Options compare def OptionsPerPos.insertAt (optionsPerPos : OptionsPerPos) (pos : SubExpr.Pos) (name : Name) (value : DataValue) : OptionsPerPos := - let opts := optionsPerPos.get? pos |>.getD {} + let opts := optionsPerPos.find? 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 := - TreeMap.mergeBy (fun _ => KVMap.mergeBy (fun _ _ dv => dv)) + RBMap.mergeBy (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 98e0b659496ed..a0f458e0d8000 100644 --- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean @@ -4,6 +4,7 @@ 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 @@ -327,7 +328,7 @@ def checkKnowsType : AnalyzeM Unit := do throw $ Exception.internal analyzeFailureId def annotateBoolAt (n : Name) (pos : Pos) : AnalyzeM Unit := do - let opts := (← get).annotations.getD pos {} |>.setBool n true + let opts := (← get).annotations.findD 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 38fc491bf267c..ab6bf712c3ac2 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.foldl (fun a n p => a.push (n, p)) #[] + let r : Array (Name × ReducibilityStatus) := m.fold (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 } diff --git a/src/Lean/Server/CodeActions/Attr.lean b/src/Lean/Server/CodeActions/Attr.lean index e59345b66f4ed..231751893d628 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.getD a #[]).push action) } + m.insert a ((m.findD 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 f4f85c0699b0c..97ff51ce9ddfa 100644 --- a/src/Lean/Server/Completion/CompletionCollectors.lean +++ b/src/Lean/Server/Completion/CompletionCollectors.lean @@ -14,7 +14,6 @@ open Elab open Lean.Lsp open Meta open FuzzyMatching -open Std (TreeMap TreeSet) section Infrastructure @@ -303,14 +302,14 @@ 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 := TreeSet Name cmpModPrivate + private def NameSetModPrivate := RBTree Name cmpModPrivate /-- Given a type, try to extract relevant type names for dot notation field completion. We extract the type name, parent struct names, and unfold the type. The process mimics the dot notation elaboration procedure at `App.lean` -/ private partial def getDotCompletionTypeNames (type : Expr) : MetaM NameSetModPrivate := - return (← visit type |>.run TreeSet.empty).2 + return (← visit type |>.run RBTree.empty).2 where visit (type : Expr) : StateRefT NameSetModPrivate MetaM Unit := do let .const typeName _ := type.getAppFn | return () @@ -449,7 +448,7 @@ def dotCompletion let nameSet ← try getDotCompletionTypeNames (← instantiateMVars (← inferType info.expr)) catch _ => - pure TreeSet.empty + pure RBTree.empty if nameSet.isEmpty then return @@ -484,7 +483,7 @@ def dotIdCompletion let nameSet ← try getDotCompletionTypeNames resultTypeFn catch _ => - pure TreeSet.empty + pure RBTree.empty forEligibleDeclsM fun declName c => do let unnormedTypeName := declName.getPrefix @@ -543,7 +542,7 @@ def optionCompletion else (ss.toString, false) -- HACK(WN): unfold the type so ForIn works - let (decls : TreeMap _ _ _) ← getOptionDecls + let (decls : RBMap _ _ _) ← getOptionDecls let opts ← getOptions let mut items := #[] for ⟨name, decl⟩ in decls do diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index db7e7fb946b83..b7a60a4f0cd04 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -8,6 +8,7 @@ prelude import Init.System.IO import Std.Sync.Channel +import Lean.Data.RBMap import Lean.Environment import Lean.Data.Lsp @@ -53,7 +54,6 @@ command that the request is looking for and the request sends a "content changed namespace Lean.Server.FileWorker -open Std (TreeMap) open Lsp open IO open Snapshots @@ -267,7 +267,7 @@ This option can only be set on the command line, not in the lakefile or via `set end Elab -- Pending requests are tracked so they can be canceled -abbrev PendingRequestMap := TreeMap RequestID (Task (Except IO.Error Unit)) compare +abbrev PendingRequestMap := RBMap RequestID (Task (Except IO.Error Unit)) compare structure AvailableImportsCache where availableImports : ImportCompletion.AvailableImports @@ -282,7 +282,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 : TreeMap UInt64 (IO.Ref RpcSession) compare + rpcSessions : RBMap UInt64 (IO.Ref RpcSession) compare abbrev WorkerM := ReaderT WorkerContext <| StateRefT WorkerState IO @@ -403,8 +403,8 @@ section Initialization doc := { doc with reporter } reporterCancelTk srcSearchPathTask := srcSearchPathPromise.result - pendingRequests := ∅ - rpcSessions := ∅ + pendingRequests := RBMap.empty + rpcSessions := RBMap.empty importCachingTask? := none }) where @@ -526,7 +526,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.get? p.sessionId then + if let some seshRef := (← get).rpcSessions.find? p.sessionId then let monoMsNow ← IO.monoMsNow let discardRefs : StateM RpcObjectStore Unit := do for ref in p.refs do @@ -537,7 +537,7 @@ def handleRpcRelease (p : Lsp.RpcReleaseParams) : WorkerM Unit := do { st with objects } def handleRpcKeepAlive (p : Lsp.RpcKeepAliveParams) : WorkerM Unit := do - match (← get).rpcSessions.get? p.sessionId with + match (← get).rpcSessions.find? p.sessionId with | none => return | some seshRef => seshRef.modify (·.keptAlive (← IO.monoMsNow)) @@ -649,7 +649,7 @@ section MessageHandling let params ← parseParams Lsp.RpcCallParams params -- needs access to `EditableDocumentCore.diagnosticsRef` if params.method == `Lean.Widget.getInteractiveDiagnostics then - let some seshRef := st.rpcSessions.get? params.sessionId + let some seshRef := st.rpcSessions.find? params.sessionId | ctx.chanOut.send <| .responseError id .rpcNeedsReconnect "Outdated RPC session" none let params ← IO.ofExcept (fromJson? params.params) let resp ← handleGetInteractiveDiagnosticsRequest params @@ -720,7 +720,7 @@ section MainLoop throwServerError s!"Failed responding to request {id}: {e}" pure <| acc.erase id else pure acc - let pendingRequests ← st.pendingRequests.foldlM (fun acc id task => filterFinishedTasks acc id task) st.pendingRequests + let pendingRequests ← st.pendingRequests.foldM (fun acc id task => filterFinishedTasks acc id task) 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/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean index 027d464b68635..d272c3aadb75e 100644 --- a/src/Lean/Server/FileWorker/RequestHandling.lean +++ b/src/Lean/Server/FileWorker/RequestHandling.lean @@ -18,7 +18,6 @@ open RequestM open Snapshots open Lean.Parser.Tactic.Doc (alternativeOfTactic getTacticExtensionString) -open Std (TreeMap) def findCompletionCmdDataAtPos (doc : EditableDocument) diff --git a/src/Lean/Server/Requests.lean b/src/Lean/Server/Requests.lean index 6eef3d31359d4..26660e4e15c60 100644 --- a/src/Lean/Server/Requests.lean +++ b/src/Lean/Server/Requests.lean @@ -17,7 +17,6 @@ import Lean.Server.FileWorker.Utils import Lean.Server.Rpc.Basic import Std.Sync.Mutex -open Std (TreeMap) namespace Lean.Language @@ -89,7 +88,7 @@ def parseRequestParams (paramType : Type) [FromJson paramType] (params : Json) message := s!"Cannot parse request params: {params.compress}\n{inner}" } structure RequestContext where - rpcSessions : TreeMap UInt64 (IO.Ref FileWorker.RpcSession) compare + rpcSessions : RBMap UInt64 (IO.Ref FileWorker.RpcSession) compare srcSearchPath : SearchPath doc : FileWorker.EditableDocument hLog : IO.FS.Stream diff --git a/src/Lean/Server/Rpc/RequestHandling.lean b/src/Lean/Server/Rpc/RequestHandling.lean index 324d38fa12a37..b4905d359e42b 100644 --- a/src/Lean/Server/Rpc/RequestHandling.lean +++ b/src/Lean/Server/Rpc/RequestHandling.lean @@ -69,7 +69,7 @@ def wrapRpcProcedure (method : Name) paramType respType ⟨fun seshId j => do let rc ← read - let some seshRef := rc.rpcSessions.get? seshId + let some seshRef := rc.rpcSessions.find? seshId | throwThe RequestError { code := JsonRpc.ErrorCode.rpcNeedsReconnect message := s!"Outdated RPC session" } let t ← RequestM.asTask do diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 71d8e1c2918d6..7ff469c0ee9a7 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -8,6 +8,7 @@ prelude import Init.System.IO import Std.Sync.Mutex import Init.Data.ByteArray +import Lean.Data.RBMap import Lean.Util.Paths @@ -70,7 +71,6 @@ state. namespace Lean.Server.Watchdog -open Std (TreeMap TreeSet) open IO open Lsp open JsonRpc @@ -106,7 +106,7 @@ section Utils | crashed (queuedMsgs : Array JsonRpc.Message) (origin : CrashOrigin) | running - abbrev PendingRequestMap := TreeMap RequestID JsonRpc.Message compare + abbrev PendingRequestMap := RBMap RequestID JsonRpc.Message compare end Utils section FileWorker @@ -138,7 +138,7 @@ section FileWorker def errorPendingRequests (fw : FileWorker) (hError : FS.Stream) (code : ErrorCode) (msg : String) : IO Unit := do let pendingRequests ← fw.pendingRequestsRef.modifyGet - fun pendingRequests => (pendingRequests, ∅) + fun pendingRequests => (pendingRequests, RBMap.empty) for ⟨id, _⟩ in pendingRequests do hError.writeLspResponseError { id := id, code := code, message := msg } @@ -174,8 +174,8 @@ section FileWorker end FileWorker section ServerM - abbrev FileWorkerMap := TreeMap DocumentUri FileWorker compare - abbrev ImportMap := TreeMap DocumentUri (TreeSet DocumentUri compare) compare + abbrev FileWorkerMap := RBMap DocumentUri FileWorker compare + abbrev ImportMap := RBMap DocumentUri (RBTree DocumentUri compare) compare /-- Global import data for all open files managed by this watchdog. -/ structure ImportData where @@ -185,15 +185,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 : TreeSet DocumentUri compare) + def ImportData.update (d : ImportData) (uri : DocumentUri) (imports : RBTree DocumentUri compare) : ImportData := Id.run do - let oldImports := d.imports.getD uri ∅ + let oldImports := d.imports.findD uri ∅ let removedImports := oldImports.diff imports let addedImports := imports.diff oldImports let mut importedBy := d.importedBy for removedImport in removedImports do - let importedByRemovedImport' := importedBy.get! removedImport |>.erase uri + let importedByRemovedImport' := importedBy.find! removedImport |>.erase uri if importedByRemovedImport'.isEmpty then importedBy := importedBy.erase removedImport else @@ -201,7 +201,7 @@ section ServerM for addedImport in addedImports do importedBy := - importedBy.getD addedImport ∅ + importedBy.findD addedImport ∅ |>.insert uri |> importedBy.insert addedImport @@ -223,7 +223,7 @@ section ServerM sourceUri : DocumentUri localID : RequestID - abbrev PendingServerRequestMap := TreeMap RequestID RequestIDTranslation compare + abbrev PendingServerRequestMap := RBMap RequestID RequestIDTranslation compare structure ServerRequestData where pendingServerRequests : PendingServerRequestMap @@ -245,7 +245,7 @@ section ServerM (data : ServerRequestData) (globalID : RequestID) : Option RequestIDTranslation × ServerRequestData := - let translation? := data.pendingServerRequests.get? globalID + let translation? := data.pendingServerRequests.find? globalID let data := { data with pendingServerRequests := data.pendingServerRequests.erase globalID } (translation?, data) @@ -270,7 +270,7 @@ section ServerM (←read).fileWorkersRef.modify (fun fileWorkers => fileWorkers.insert val.doc.uri val) def findFileWorker? (uri : DocumentUri) : ServerM (Option FileWorker) := - return (← (←read).fileWorkersRef.get).get? uri + return (← (←read).fileWorkersRef.get).find? uri def eraseFileWorker (uri : DocumentUri) : ServerM Unit := do let s ← read @@ -306,7 +306,7 @@ section ServerM def handleImportClosure (fw : FileWorker) (params : LeanImportClosureParams) : ServerM Unit := do let s ← read s.importData.modify fun importData => - importData.update fw.doc.uri (.fromList params.importClosure.toList) + importData.update fw.doc.uri (.ofList params.importClosure.toList) /-- Creates a Task which forwards a worker's messages into the output stream until an event which must be handled in the main watchdog thread (e.g. an I/O error) happens. -/ @@ -393,7 +393,7 @@ section ServerM setsid := true } let exitCode ← Std.Mutex.new none - let pendingRequestsRef ← IO.mkRef (TreeMap.empty : PendingRequestMap) + let pendingRequestsRef ← IO.mkRef (RBMap.empty : PendingRequestMap) let initialDependencyBuildMode := m.dependencyBuildMode let updatedDependencyBuildMode := if initialDependencyBuildMode matches .once then @@ -749,7 +749,7 @@ def handlePrepareRename (p : PrepareRenameParams) : ServerM (Option Range) := do def handleRename (p : RenameParams) : ServerM 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 (TreeMap Lsp.Position Lsp.Position compare) := ∅ + let mut refs : Std.HashMap DocumentUri (RBMap Lsp.Position Lsp.Position compare) := ∅ 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 @@ -800,7 +800,7 @@ section NotificationHandling let s ← read let fileWorkers ← s.fileWorkersRef.get let importData ← s.importData.get - let dependents := importData.importedBy.getD p.textDocument.uri ∅ + let dependents := importData.importedBy.findD p.textDocument.uri ∅ for ⟨uri, _⟩ in fileWorkers do if ! dependents.contains uri then @@ -817,7 +817,7 @@ section NotificationHandling if ! leanChanges.isEmpty then let importData ← (← read).importData.get for (c, _) in leanChanges do - let dependents := importData.importedBy.getD c.uri ∅ + let dependents := importData.importedBy.findD c.uri ∅ for dependent in dependents do notifyAboutStaleDependency dependent c.uri if ! ileanChanges.isEmpty then @@ -1184,12 +1184,12 @@ def initAndRunWatchdog (args : List String) (i o e : FS.Stream) : IO Unit := do let srcSearchPath ← initSrcSearchPath let references ← IO.mkRef .empty startLoadingReferences references - let fileWorkersRef ← IO.mkRef (TreeMap.empty : FileWorkerMap) + let fileWorkersRef ← IO.mkRef (RBMap.empty : FileWorkerMap) let serverRequestData ← IO.mkRef { - pendingServerRequests := ∅ + pendingServerRequests := RBMap.empty freshServerRequestID := 0 } - let importData ← IO.mkRef ⟨TreeMap.empty, TreeMap.empty⟩ + let importData ← IO.mkRef ⟨RBMap.empty, RBMap.empty⟩ let i ← maybeTee "wdIn.txt" false i let o ← maybeTee "wdOut.txt" true o let e ← maybeTee "wdErr.txt" true e diff --git a/src/Lean/SubExpr.lean b/src/Lean/SubExpr.lean index 33175c5d782f0..309eda5857c33 100644 --- a/src/Lean/SubExpr.lean +++ b/src/Lean/SubExpr.lean @@ -6,10 +6,10 @@ Authors: Sebastian Ullrich, Daniel Selsam, Wojciech Nawrocki, E.W.Ayers prelude import Lean.Meta.Basic import Lean.Data.Json +import Lean.Data.RBMap import Init.Control.Option namespace Lean -open Std (TreeMap) /-- A position of a subexpression in an expression. @@ -171,7 +171,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) := TreeMap Pos α compare +abbrev PosMap (α : Type u) := RBMap Pos α compare def bindingBody! : SubExpr → SubExpr | ⟨.forallE _ _ b _, p⟩ => ⟨b, p.pushBindingBody⟩ diff --git a/src/Lean/Util/FoldConsts.lean b/src/Lean/Util/FoldConsts.lean index d7f4e167abf95..cd1608bf652e7 100644 --- a/src/Lean/Util/FoldConsts.lean +++ b/src/Lean/Util/FoldConsts.lean @@ -63,10 +63,10 @@ def getUsedConstantsAsSet (c : ConstantInfo) : NameSet := c.type.getUsedConstantsAsSet ++ match c.value? with | some v => v.getUsedConstantsAsSet | none => match c with - | .inductInfo val => .fromList val.ctors + | .inductInfo val => .ofList val.ctors | .opaqueInfo val => val.value.getUsedConstantsAsSet | .ctorInfo val => ({} : NameSet).insert val.name - | .recInfo val => .fromList val.all + | .recInfo val => .ofList val.all | _ => {} end ConstantInfo diff --git a/src/Lean/Util/LeanOptions.lean b/src/Lean/Util/LeanOptions.lean index fb42ac11a3da8..9fe332f7dd185 100644 --- a/src/Lean/Util/LeanOptions.lean +++ b/src/Lean/Util/LeanOptions.lean @@ -5,10 +5,8 @@ Authors: Marc Huisinga -/ prelude import Lean.Util.Paths -import Std.Data.TreeMap.Basic namespace Lean -open Std /-- Restriction of `DataValue` that covers exactly those cases that Lean is able to handle when passed via the `-D` flag. -/ inductive LeanOptionValue where @@ -62,7 +60,7 @@ def LeanOptionValue.asCliFlagValue : (v : LeanOptionValue) → String /-- Options that are used by Lean as if they were passed using `-D`. -/ structure LeanOptions where - values : TreeMap Name LeanOptionValue Name.cmp + values : RBMap Name LeanOptionValue Name.cmp deriving Inhabited, Repr def LeanOptions.toOptions (leanOptions : LeanOptions) : Options := Id.run do @@ -72,7 +70,7 @@ def LeanOptions.toOptions (leanOptions : LeanOptions) : Options := Id.run do return options def LeanOptions.fromOptions? (options : Options) : Option LeanOptions := do - let mut values := TreeMap.empty + let mut values := RBMap.empty for ⟨name, dataValue⟩ in options do let optionValue ← LeanOptionValue.ofDataValue? dataValue values := values.insert name optionValue @@ -81,7 +79,7 @@ def LeanOptions.fromOptions? (options : Options) : Option LeanOptions := do instance : FromJson LeanOptions where fromJson? | Json.obj obj => do - let values ← obj.foldlM (init := TreeMap.empty) fun acc k v => do + let values ← obj.foldM (init := RBMap.empty) fun acc k v => do let optionValue ← fromJson? v return acc.insert k.toName optionValue return ⟨values⟩ @@ -89,7 +87,7 @@ instance : FromJson LeanOptions where instance : ToJson LeanOptions where toJson options := - Json.obj <| options.values.foldl (init := ∅) fun acc k v => + Json.obj <| options.values.fold (init := RBNode.leaf) fun acc k v => acc.insert (cmp := compare) k.toString (toJson v) end Lean diff --git a/src/Lean/Util/PPExt.lean b/src/Lean/Util/PPExt.lean index 77677bbd61aa1..61a196311e65f 100644 --- a/src/Lean/Util/PPExt.lean +++ b/src/Lean/Util/PPExt.lean @@ -10,8 +10,6 @@ import Lean.Data.OpenDecl import Lean.Elab.InfoTree.Types namespace Lean -open Std (TreeMap) - register_builtin_option pp.raw : Bool := { defValue := false group := "pp" @@ -41,7 +39,7 @@ structure PPContext where currNamespace : Name := Name.anonymous openDecls : List OpenDecl := [] -abbrev PrettyPrinter.InfoPerPos := TreeMap Nat Elab.Info compare +abbrev PrettyPrinter.InfoPerPos := RBMap Nat Elab.Info compare /-- 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 fdb32c928b707..29195ba6b2359 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 := TreeMap.mergeBy (fun _ _ b => b) a.changesBefore b.changesBefore, - changesAfter := TreeMap.mergeBy (fun _ _ b => b) a.changesAfter b.changesAfter + changesBefore := RBMap.mergeBy (fun _ _ b => b) a.changesBefore b.changesBefore, + changesAfter := RBMap.mergeBy (fun _ _ b => b) a.changesAfter b.changesAfter } instance : ToString ExprDiff where toString x := let f := fun (p : PosMap ExprDiffTag) => - TreeMap.toList p |>.map (fun (k,v) => s!"({toString k}:{toString v})") + RBMap.toList p |>.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 := TreeMap.empty.insert after d - changesBefore := TreeMap.empty.insert before d + { changesAfter := RBMap.empty.insert after d + changesBefore := RBMap.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 := TreeSet.fromArray ms _ + let ms : MVarIdSet := RBTree.fromArray ms _ return s.insert g ms ) let isParent (before after : MVarId) : Bool := - match parentMap.get? before with + match parentMap.find? 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 bfb61b4112bfc..65aaa5f3c2bb3 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.get? info.subexprPos with + match pm.find? 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)) := tt.rewrite fun (n, _) subTt => - match infos.get? n with + match infos.find? 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 33d3a00fb5152..b30e64efd7af5 100644 --- a/src/Lean/Widget/InteractiveDiagnostic.lean +++ b/src/Lean/Widget/InteractiveDiagnostic.lean @@ -11,7 +11,6 @@ import Lean.Widget.InteractiveGoal namespace Lean.Widget open Lsp Server -open Std (TreeMap) inductive StrictOrLazy (α β : Type) : Type | strict : α → StrictOrLazy α β @@ -96,7 +95,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 : TreeMap Nat Elab.Info compare) + | code (ctx : Elab.ContextInfo) (infos : RBMap Nat Elab.Info compare) /-- Nested text is ignored. -/ | goal (ctx : Elab.ContextInfo) (lctx : LocalContext) (g : MVarId) /-- Nested text is ignored. -/ diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean index 32ff8b4f082f6..f4debf21abd1e 100644 --- a/src/Lean/Widget/UserWidget.lean +++ b/src/Lean/Widget/UserWidget.lean @@ -10,7 +10,6 @@ import Lean.Server.Rpc.RequestHandling namespace Lean.Widget open Meta Elab -open Std (TreeMap) /-- A widget module is a unit of source code that can execute in the infoview. @@ -58,7 +57,7 @@ class ToModule (α : Type u) where instance : ToModule Module := ⟨id⟩ -private builtin_initialize builtinModulesRef : IO.Ref (TreeMap UInt64 (Name × Module) compare) ← +private builtin_initialize builtinModulesRef : IO.Ref (RBMap UInt64 (Name × Module) compare) ← IO.mkRef ∅ def addBuiltinModule (id : Name) (m : Module) : IO Unit := @@ -70,7 +69,7 @@ where `inst : ToModule α` is synthesized during registration time and stored thereafter. -/ private abbrev ModuleRegistry := SimplePersistentEnvExtension (UInt64 × Name × Expr) - (TreeMap UInt64 (Name × Expr) compare) + (RBMap UInt64 (Name × Expr) compare) builtin_initialize moduleRegistry : ModuleRegistry ← registerSimplePersistentEnvExtension { @@ -94,9 +93,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).get? mod.javascriptHash then + if let some _ := (← builtinModulesRef.get).find? 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 |>.get? mod.javascriptHash then + if let some (n, _) := moduleRegistry.getState env |>.find? 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 @@ -128,7 +127,7 @@ structure WidgetSource where open Server RequestM in def getWidgetSource (args : GetWidgetSourceParams) : RequestM (RequestTask WidgetSource) := do - if let some (_, m) := (← builtinModulesRef.get).get? args.hash then + if let some (_, m) := (← builtinModulesRef.get).find? args.hash then return .pure { sourcetext := m.javascript } let doc ← readDoc @@ -137,7 +136,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 |>.get? args.hash then + if let some (_, e) := moduleRegistry.getState snap.env |>.find? args.hash then runTermElabM snap do return { sourcetext := (← evalModule e).javascript } else @@ -183,11 +182,11 @@ This is similar to a parametric attribute, except that: which we cannot do owing to the closure. -/ private abbrev PanelWidgetsExt := SimpleScopedEnvExtension (UInt64 × Name) - (TreeMap UInt64 (List PanelWidgetsExtEntry) compare) + (RBMap UInt64 (List PanelWidgetsExtEntry) compare) builtin_initialize panelWidgetsExt : PanelWidgetsExt ← registerSimpleScopedEnvExtension { - addEntry := fun s (h, n) => s.insert h (.global n :: s.getD h []) + addEntry := fun s (h, n) => s.insert h (.global n :: s.findD h []) initial := .empty } @@ -210,7 +209,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.getD wi.javascriptHash []) + s.insert wi.javascriptHash (.local wi :: s.findD wi.javascriptHash []) def erasePanelWidget [Monad m] [MonadEnv m] (h : UInt64) : m Unit := do modifyEnv fun env => panelWidgetsExt.modifyState env fun st => st.erase h @@ -226,7 +225,7 @@ def WidgetInstance.ofHash (hash : UInt64) (props : StateM Server.RpcObjectStore let env ← getEnv let builtins ← builtinModulesRef.get let some id := - (builtins.get? hash |>.map (·.1)) <|> (moduleRegistry.getState env |>.get? hash |>.map (·.1)) + (builtins.find? hash |>.map (·.1)) <|> (moduleRegistry.getState env |>.find? hash |>.map (·.1)) | throwError s!"No widget module with hash {hash} registered" return { id, javascriptHash := hash, props } diff --git a/src/lake/Lake/Build/Store.lean b/src/lake/Lake/Build/Store.lean index 8f1fb1fcb87fb..7b53e46f3169b 100644 --- a/src/lake/Lake/Build/Store.lean +++ b/src/lake/Lake/Build/Store.lean @@ -18,16 +18,15 @@ topological-based build of an initial key's dependencies). namespace Lake open Lean (Name NameMap) -open Std (DTreeMap) /-- A monad equipped with a Lake build store. -/ abbrev MonadBuildStore (m) := MonadDStore BuildKey (Job <| BuildData ·) m /-- The type of the Lake build store. -/ abbrev BuildStore := - DTreeMap BuildKey (Job <| BuildData ·) BuildKey.quickCmp + DRBMap BuildKey (Job <| BuildData ·) BuildKey.quickCmp -@[inline] def BuildStore.empty : BuildStore := DTreeMap.empty +@[inline] def BuildStore.empty : BuildStore := DRBMap.empty namespace BuildStore diff --git a/src/lake/Lake/CLI/Serve.lean b/src/lake/Lake/CLI/Serve.lean index 0da46d98d82ac..ab9056beafd7d 100644 --- a/src/lake/Lake/CLI/Serve.lean +++ b/src/lake/Lake/CLI/Serve.lean @@ -10,7 +10,7 @@ import Lake.Util.MainM import Lean.Util.FileSetupInfo namespace Lake -open Lean Std +open Lean open System (FilePath) /-- Exit code to return if `setup-file` cannot find the config file. -/ @@ -58,7 +58,7 @@ def setupFile let some module := ws.findModule? moduleName | pure ⟨∅⟩ let options := module.serverOptions.map fun opt => ⟨opt.name, opt.value⟩ - pure ⟨TreeMap.fromArray options⟩ + pure ⟨Lean.RBMap.fromArray options Lean.Name.cmp⟩ IO.println <| Json.compress <| toJson { paths, setupOptions diff --git a/src/lake/Lake/CLI/Translate/Lean.lean b/src/lake/Lake/CLI/Translate/Lean.lean index d89d33947a551..ad00fe069120b 100644 --- a/src/lake/Lake/CLI/Translate/Lean.lean +++ b/src/lake/Lake/CLI/Translate/Lean.lean @@ -208,7 +208,7 @@ protected def Dependency.mkSyntax (cfg : Dependency) : RequireDecl := Unhygienic pure none let scope? := if cfg.scope.isEmpty then none else some (quote cfg.scope) let opts? := if cfg.opts.isEmpty then none else some <| Unhygienic.run do - cfg.opts.foldlM (init := mkCIdent ``NameMap.empty) fun stx opt val => + cfg.opts.foldM (init := mkCIdent ``NameMap.empty) fun stx opt val => `($stx |>.insert $(quote opt) $(quote 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 939b91cb3abfc..5f75fa8430912 100644 --- a/src/lake/Lake/CLI/Translate/Toml.lean +++ b/src/lake/Lake/CLI/Translate/Toml.lean @@ -138,7 +138,7 @@ protected def Dependency.toToml (dep : Dependency) (t : Table := {}) : Table := |>.smartInsert `subDir subDir? else t - t.smartInsert `options <| dep.opts.foldl (·.insert · ·) Table.empty + t.smartInsert `options <| dep.opts.fold (·.insert · ·) Table.empty instance : ToToml Dependency := ⟨(toToml ·.toToml)⟩ diff --git a/src/lake/Lake/Config/ExternLib.lean b/src/lake/Lake/Config/ExternLib.lean index 71fb51fe7897b..92020e374ade4 100644 --- a/src/lake/Lake/Config/ExternLib.lean +++ b/src/lake/Lake/Config/ExternLib.lean @@ -20,11 +20,11 @@ structure ExternLib where /-- The external libraries of the package (as an Array). -/ @[inline] def Package.externLibs (self : Package) : Array ExternLib := - self.externLibConfigs.foldl (fun a _ v => a.push ⟨self, _, v⟩) #[] + self.externLibConfigs.fold (fun a _ v => a.push ⟨self, _, v⟩) #[] /-- Try to find a external library in the package with the given name. -/ @[inline] def Package.findExternLib? (name : Name) (self : Package) : Option ExternLib := - self.externLibConfigs.get? name |>.map (⟨self, name, ·⟩) + self.externLibConfigs.find? name |>.map (⟨self, name, ·⟩) namespace ExternLib diff --git a/src/lake/Lake/Config/Module.lean b/src/lake/Lake/Config/Module.lean index 9ade500c33a1c..3ad76f12fa3d4 100644 --- a/src/lake/Lake/Config/Module.lean +++ b/src/lake/Lake/Config/Module.lean @@ -10,7 +10,7 @@ import Lake.Config.OutFormat import Lake.Util.OrdHashSet namespace Lake -open Lean System Std +open Lean System /-- A buildable Lean module of a `LeanLib`. -/ structure Module where @@ -34,8 +34,8 @@ abbrev ModuleSet := Std.HashSet Module abbrev OrdModuleSet := OrdHashSet Module @[inline] def OrdModuleSet.empty : OrdModuleSet := OrdHashSet.empty -abbrev ModuleMap (α) := TreeMap Module α (·.name.quickCmp ·.name) -@[inline] def ModuleMap.empty : ModuleMap α := ∅ +abbrev ModuleMap (α) := RBMap Module α (·.name.quickCmp ·.name) +@[inline] def ModuleMap.empty : ModuleMap α := RBMap.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 e33b8113aecbf..6f5b98f0cba31 100644 --- a/src/lake/Lake/Config/Package.lean +++ b/src/lake/Lake/Config/Package.lean @@ -14,6 +14,7 @@ import Lake.Config.WorkspaceConfig import Lake.Config.Dependency import Lake.Config.Script import Lake.Load.Config +import Lake.Util.DRBMap import Lake.Util.OrdHashSet import Lake.Util.Version diff --git a/src/lake/Lake/Config/TargetConfig.lean b/src/lake/Lake/Config/TargetConfig.lean index 8e82993928b50..375beff496b8c 100644 --- a/src/lake/Lake/Config/TargetConfig.lean +++ b/src/lake/Lake/Config/TargetConfig.lean @@ -37,4 +37,4 @@ hydrate_opaque_type OpaqueTargetConfig TargetConfig pkgName name /-- 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.opaqueTargetConfigs.get? name |>.map (·.get) + self.opaqueTargetConfigs.find? name |>.map (·.get) diff --git a/src/lake/Lake/Config/Workspace.lean b/src/lake/Lake/Config/Workspace.lean index f8c5c1e437bfe..e6bc84cbe4285 100644 --- a/src/lake/Lake/Config/Workspace.lean +++ b/src/lake/Lake/Config/Workspace.lean @@ -84,11 +84,11 @@ 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.get? name + self.packageMap.find? name /-- Try to find a script in the workspace with the given name. -/ protected def findScript? (script : Name) (self : Workspace) : Option Script := - self.packages.findSome? (·.scripts.get? script) + self.packages.findSome? (·.scripts.find? script) /-- Check if the module is local to any package in the workspace. -/ def isLocalModule (mod : Name) (self : Workspace) : Bool := @@ -128,7 +128,7 @@ def addModuleFacetConfig (cfg : ModuleFacetConfig name) (self : Workspace) : Wor /-- Try to find a module facet configuration in the workspace with the given name. -/ def findModuleFacetConfig? (name : Name) (self : Workspace) : Option (ModuleFacetConfig name) := - self.moduleFacetConfigs.get? name + self.moduleFacetConfigs.find? name /-- Add a package facet to the workspace. -/ def addPackageFacetConfig (cfg : PackageFacetConfig name) (self : Workspace) : Workspace := @@ -136,7 +136,7 @@ def addPackageFacetConfig (cfg : PackageFacetConfig name) (self : Workspace) : W /-- Try to find a package facet configuration in the workspace with the given name. -/ def findPackageFacetConfig? (name : Name) (self : Workspace) : Option (PackageFacetConfig name) := - self.packageFacetConfigs.get? name + self.packageFacetConfigs.find? name /-- Add a library facet to the workspace. -/ def addLibraryFacetConfig (cfg : LibraryFacetConfig name) (self : Workspace) : Workspace := @@ -144,7 +144,7 @@ def addLibraryFacetConfig (cfg : LibraryFacetConfig name) (self : Workspace) : W /-- Try to find a library facet configuration in the workspace with the given name. -/ def findLibraryFacetConfig? (name : Name) (self : Workspace) : Option (LibraryFacetConfig name) := - self.libraryFacetConfigs.get? name + self.libraryFacetConfigs.find? name /-- The workspace's binary directories (which are added to `Path`). -/ def binPath (self : Workspace) : SearchPath := diff --git a/src/lake/Lake/DSL/DeclUtil.lean b/src/lake/Lake/DSL/DeclUtil.lean index 4cb91385d4033..6bff854c2f6fa 100644 --- a/src/lake/Lake/DSL/DeclUtil.lean +++ b/src/lake/Lake/DSL/DeclUtil.lean @@ -109,7 +109,7 @@ def elabConfigDecl m := m.insert fieldName {ref := id, val} else logWarningAt id m!"unknown '{.ofConstName tyName}' field '{fieldName}'" - let fs ← m.foldlM (init := #[]) fun a k {ref, val} => withRef ref do + let fs ← m.foldM (init := #[]) fun a k {ref, val} => withRef ref do return a.push <| ← `(Term.structInstField| $(← mkIdentFromRef k true):ident := $val) let ty := mkCIdentFrom (← getRef) tyName let declId ← id do diff --git a/src/lake/Lake/Load/Lean/Eval.lean b/src/lake/Lake/Load/Lean/Eval.lean index c8369300a0f82..244ae86c82131 100644 --- a/src/lake/Lake/Load/Lean/Eval.lean +++ b/src/lake/Lake/Load/Lean/Eval.lean @@ -80,7 +80,7 @@ def Package.loadFromEnv let fn ← IO.ofExcept <| evalConstCheck env opts ScriptFn ``ScriptFn scriptName return {name, fn, doc? := ← findDocString? env scriptName : Script} let defaultScripts ← defaultScriptAttr.getAllEntries env |>.mapM fun name => - if let some script := scripts.get? name then pure script else + if let some script := scripts.find? name then pure script else error s!"package is missing script `{name}` marked as a default" let leanLibConfigs ← IO.ofExcept <| mkOrdTagMap env leanLibAttr fun name => evalConstCheck env opts LeanLibConfig ``LeanLibConfig name @@ -145,7 +145,7 @@ def Package.loadFromEnv -- Fill in the Package return {self with depConfigs, leanLibConfigs, leanExeConfigs, externLibConfigs - opaqueTargetConfigs, defaultTargets, scripts := ⟨scripts⟩, defaultScripts + opaqueTargetConfigs, defaultTargets, scripts, defaultScripts testDriver, lintDriver, postUpdateHooks } diff --git a/src/lake/Lake/Toml/Data/Dict.lean b/src/lake/Lake/Toml/Data/Dict.lean index 57766a6ca5882..ae5476f55cd83 100644 --- a/src/lake/Lake/Toml/Data/Dict.lean +++ b/src/lake/Lake/Toml/Data/Dict.lean @@ -6,22 +6,21 @@ Authors: Mac Malone prelude import Lean.Data.NameMap import Init.Data.Nat.Fold -import Std.Data.TreeMap.Basic /-! # Red-Black Dictionary Defines an **insertion-ordered** key-value mapping backed by an red-black tree. -Implemented via a key-index `TreeMap` into an `Array` of key-value pairs. +Implemented via a key-index `RBMap` into an `Array` of key-value pairs. -/ -open Lean Std +open Lean 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 : TreeMap α Nat cmp + indices : RBMap α Nat cmp deriving Inhabited abbrev NameDict (α : Type u) := RBDict Name α Name.quickCmp @@ -37,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 := ∅) fun i _ indices => + let indices := items.size.fold (init := mkRBMap α Nat cmp) fun i _ indices => indices.insert items[i].1 i {items, indices} @@ -62,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.get? k; if h : i < t.items.size then some ⟨i, h⟩ else none + let i ← t.indices.find? 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 61c6a3c7be5ce..9f13942f89752 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.get? .anonymous |>.getD {} + keyTys := arrKeyTys.find? .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 index 7cd9aa97027cc..c26a11846a858 100644 --- a/src/lake/Lake/Util/Compare.lean +++ b/src/lake/Lake/Util/Compare.lean @@ -5,7 +5,6 @@ Authors: Mac Malone -/ prelude import Init.Data.Ord -import Std.Data.OrderAxioms.LawfulEqOrd namespace Lake @@ -27,10 +26,6 @@ class LawfulCmpEq (α : Type u) (cmp : α → α → Ordering) extends EqOfCmp export LawfulCmpEq (cmp_rfl) -scoped instance [inst : LawfulCmpEq κ cmp] : LawfulEqCmp cmp where - eq_of_compare := inst.eq_of_cmp ∘ beq_iff_eq.mp - compare_self := inst.cmp_rfl - attribute [simp] cmp_rfl @[simp] theorem cmp_iff_eq [LawfulCmpEq α cmp] : cmp a a' = .eq ↔ a = a' := diff --git a/src/lake/Lake/Util/JsonObject.lean b/src/lake/Lake/Util/JsonObject.lean index 6479e46d4231a..38af63fdb8a5a 100644 --- a/src/lake/Lake/Util/JsonObject.lean +++ b/src/lake/Lake/Util/JsonObject.lean @@ -14,15 +14,14 @@ indexing fields more convenient. -/ namespace Lake -open Std (TreeMap.Raw) /-- A JSON object (`Json.obj` data). -/ abbrev JsonObject := - TreeMap.Raw String Json compare + RBNode String (fun _ => Json) namespace JsonObject -@[inline] def mk (val : TreeMap.Raw String Json compare) : JsonObject := +@[inline] def mk (val : RBNode String (fun _ => Json)) : JsonObject := val @[inline] protected def toJson (obj : JsonObject) : Json := @@ -37,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 prop (toJson val) + obj.insert compare 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 prop + inline <| obj.erase compare prop @[inline] def getJson? (obj : JsonObject) (prop : String) : Option Json := - obj.get? prop + obj.find compare 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 ad4108d1aaf9c..4c4c5e198ee0c 100644 --- a/src/lake/Lake/Util/Name.lean +++ b/src/lake/Lake/Util/Name.lean @@ -13,7 +13,6 @@ open Lean namespace Lake open Lean (Name NameMap) -open Std (TreeMap DTreeMap) /-- First tries to convert a string into a legal name. @@ -22,26 +21,26 @@ 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 α := TreeMap.empty +@[inline] def NameMap.empty : NameMap α := RBMap.empty instance : ForIn m (NameMap α) (Name × α) where - forIn self init f := self.forIn (fun n a b => f (n, a) b) init + forIn self init f := self.forIn init f -instance : Coe (TreeMap Name α Name.quickCmp) (NameMap α) := ⟨id⟩ +instance : Coe (RBMap 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 α := DTreeMap Name α Name.quickCmp -@[inline] def DNameMap.empty : DNameMap α := DTreeMap.empty +abbrev DNameMap α := DRBMap Name α Name.quickCmp +@[inline] def DNameMap.empty : DNameMap α := DRBMap.empty instance [ToJson α] : ToJson (NameMap α) where - toJson m := Json.obj <| m.foldl (fun n k v => n.insert k.toString (toJson v)) ∅ + toJson m := Json.obj <| m.fold (fun n k v => n.insert compare k.toString (toJson v)) .leaf instance [FromJson α] : FromJson (NameMap α) where fromJson? j := do - (← j.getObj?).foldlM (init := {}) fun m k v => + (← j.getObj?).foldM (init := {}) fun m k v => let k := k.toName if k.isAnonymous then throw "expected name" diff --git a/src/lake/Lake/Util/StoreInsts.lean b/src/lake/Lake/Util/StoreInsts.lean index bb01e215d72fc..92ccfec75de07 100644 --- a/src/lake/Lake/Util/StoreInsts.lean +++ b/src/lake/Lake/Util/StoreInsts.lean @@ -8,20 +8,16 @@ import Lake.Util.DRBMap import Lake.Util.RBArray import Lake.Util.Family import Lake.Util.Store -import Std.Data.OrderAxioms.LawfulEqOrd open Lean -open Std namespace Lake -variable {cmp : κ → κ → Ordering} - -instance [Monad m] [LawfulEqCmp cmp] : MonadDStore κ β (StateT (DTreeMap κ β cmp) m) where - fetch? k := return (← get).get? k +instance [Monad m] [EqOfCmpWrt κ β cmp] : MonadDStore κ β (StateT (DRBMap κ β cmp) m) where + fetch? k := return (← get).find? k store k a := modify (·.insert k a) -instance [MonadLiftT (ST ω) m] [Monad m] [LawfulEqCmp cmp] : MonadDStore κ β (StateRefT' ω (DTreeMap κ β cmp) m) where - fetch? k := return (← get).get? k +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 diff --git a/src/lake/tests/toml/Test.lean b/src/lake/tests/toml/Test.lean index 82b25635629a3..ca671fc64070c 100644 --- a/src/lake/tests/toml/Test.lean +++ b/src/lake/tests/toml/Test.lean @@ -58,6 +58,9 @@ where if h : i < n then let a ← f ⟨i, h⟩; loop (i+1) else pure () termination_by n - i +local instance [Monad m] : ForIn m (RBNode α β) ((a : α) × β a) where + forIn t init f := t.forIn init (fun a b acc => f ⟨a, b⟩ acc) + def expectBEq [BEq α] [ToString α] (actual expected : α) : Except String Unit := do unless actual == expected do throw s!"expected '{expected}', got '{actual}'" @@ -65,9 +68,9 @@ def expectBEq [BEq α] [ToString α] (actual expected : α) : Except String Unit def expectPrimitive (actualTy : String) (expected : Json) : Except String String := do let .ok expected := expected.getObj? | throw s!"expected non-primitive, got '{actualTy}'" - let some ty := expected.get? "type" + let some ty := expected.find compare "type" | throw s!"expected non-primitive, got '{actualTy}'" - let some val := expected.get? "value" + let some val := expected.find compare "value" | throw s!"expected non-primitive, got '{actualTy}'" let .ok val := val.getStr? | throw s!"expected non-primitive, got '{actualTy}'" diff --git a/tests/lean/run/944.lean b/tests/lean/run/944.lean index de80da449b72c..726536e6b2069 100644 --- a/tests/lean/run/944.lean +++ b/tests/lean/run/944.lean @@ -37,5 +37,5 @@ def f3 : Nat := def f4 (x : Nat) : Nat := .succ x -example (xs : List α) : Std.TreeSet α ord := +example (xs : List α) : Lean.RBTree α ord := xs.foldl .insert ∅