revert changes to Lean and lake

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 `.<identifier>` 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).

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
   }

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,56 +471,56 @@ 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
 
 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 :=

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
 

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
 

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

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

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

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)

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

src/Lean/Compiler/LCNF/Renaming.lean

@@ -13,15 +13,15 @@ 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
   else
     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)

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

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

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