chore: document replaceUnsafeM issue

doc/int.md

@@ -13,7 +13,7 @@ Recall that nonnegative numerals are considered to be a `Nat` if there are no ty
 
 The operator `/` for `Int` implements integer division.
 ```lean
-#eval -10 / 4 -- -3
+#eval -10 / 4 -- -2
 ```
 
 Similar to `Nat`, the internal representation of `Int` is optimized. Small integers are

src/Init/Data/List/Lemmas.lean

@@ -128,6 +128,14 @@ theorem length_pos {l : List α} : 0 < length l ↔ l ≠ [] :=
 theorem length_eq_one {l : List α} : length l = 1 ↔ ∃ a, l = [a] :=
   ⟨fun h => match l, h with | [_], _ => ⟨_, rfl⟩, fun ⟨_, h⟩ => by simp [h]⟩
 
+/-! ### `isEmpty` -/
+
+theorem isEmpty_iff {l : List α} : l.isEmpty ↔ l = [] := by
+  cases l <;> simp
+
+theorem isEmpty_iff_length_eq_zero {l : List α} : l.isEmpty ↔ l.length = 0 := by
+  rw [isEmpty_iff, length_eq_zero]
+
 /-! ## L[i] and L[i]? -/
 
 /-! ### `get` and `get?`.
@@ -467,18 +475,6 @@ theorem forall_getElem (l : List α) (p : α → Prop) :
     decide (y ∈ a :: l) = (y == a || decide (y ∈ l)) := by
   cases h : y == a <;> simp_all
 
-/-! ### `isEmpty` -/
-
-theorem isEmpty_iff {l : List α} : l.isEmpty ↔ l = [] := by
-  cases l <;> simp
-
-theorem isEmpty_false_iff_exists_mem (xs : List α) :
-    (List.isEmpty xs = false) ↔ ∃ x, x ∈ xs := by
-  cases xs <;> simp
-
-theorem isEmpty_iff_length_eq_zero {l : List α} : l.isEmpty ↔ l.length = 0 := by
-  rw [isEmpty_iff, length_eq_zero]
-
 /-! ### any / all -/
 
 theorem any_eq {l : List α} : l.any p = decide (∃ x, x ∈ l ∧ p x) := by induction l <;> simp [*]
@@ -1145,18 +1141,6 @@ theorem head_filterMap_of_eq_some {f : α → Option β} {l : List α} (w : l
     simp only [head_cons] at h
     simp [filterMap_cons, h]
 
-theorem forall_none_of_filterMap_eq_nil (h : List.filterMap f xs = []) : ∀ x ∈ xs, f x = none := by
-  intro x hx
-  induction xs with
-  | nil => contradiction
-  | cons y ys ih =>
-    simp only [filterMap_cons] at h
-    split at h
-    . cases hx with
-      | head => assumption
-      | tail _ hmem => exact ih h hmem
-    . contradiction
-
 /-! ### append -/
 
 theorem getElem?_append_right : ∀ {l₁ l₂ : List α} {n : Nat}, l₁.length ≤ n →
@@ -3411,16 +3395,6 @@ theorem any_map (f : α → β) (l : List α) (p : β → Bool) : (l.map f).any
 theorem all_map (f : α → β) (l : List α) (p : β → Bool) : (l.map f).all p = l.all (p ∘ f) := by
   induction l with simp | cons _ _ ih => rw [ih]
 
-@[simp] theorem any_append {x y : List α} : (x ++ y).any f = (x.any f || y.any f) := by
-  induction x with
-  | nil => rfl
-  | cons h t ih => simp_all [Bool.or_assoc]
-
-@[simp] theorem all_append {x y : List α} : (x ++ y).all f = (x.all f && y.all f) := by
-  induction x with
-  | nil => rfl
-  | cons h t ih => simp_all [Bool.and_assoc]
-
 /-! ## Zippers -/
 
 /-! ### zip -/

src/Init/MetaTypes.lean

@@ -219,13 +219,13 @@ structure Config where
   -/
   index             : Bool := true
   /--
-  When `true` (default: `true`), `simp` will **not** create a proof for a rewriting rule associated
+  When `true` (default: `false`), `simp` will **not** create a proof for a rewriting rule associated
   with an `rfl`-theorem.
   Rewriting rules are provided by users by annotating theorems with the attribute `@[simp]`.
   If the proof of the theorem is just `rfl` (reflexivity), and `implicitDefEqProofs := true`, `simp`
   will **not** create a proof term which is an application of the annotated theorem.
   -/
-  implicitDefEqProofs : Bool := true
+  implicitDefEqProofs : Bool := false
   deriving Inhabited, BEq
 
 -- Configuration object for `simp_all`

src/Init/PropLemmas.lean

@@ -309,11 +309,6 @@ theorem not_forall_of_exists_not {p : α → Prop} : (∃ x, ¬p x) → ¬∀ x,
 @[simp] theorem exists_eq_right_right' : (∃ (a : α), p a ∧ q a ∧ a' = a) ↔ p a' ∧ q a' := by
   simp [@eq_comm _ a']
 
-@[simp] theorem exists_or_eq_left (y : α) (p : α → Prop) : ∃ x : α, x = y ∨ p x := ⟨y, .inl rfl⟩
-@[simp] theorem exists_or_eq_right (y : α) (p : α → Prop) : ∃ x : α, p x ∨ x = y := ⟨y, .inr rfl⟩
-@[simp] theorem exists_or_eq_left' (y : α) (p : α → Prop) : ∃ x : α, y = x ∨ p x := ⟨y, .inl rfl⟩
-@[simp] theorem exists_or_eq_right' (y : α) (p : α → Prop) : ∃ x : α, p x ∨ y = x := ⟨y, .inr rfl⟩
-
 @[simp] theorem exists_prop : (∃ _h : a, b) ↔ a ∧ b :=
   ⟨fun ⟨hp, hq⟩ => ⟨hp, hq⟩, fun ⟨hp, hq⟩ => ⟨hp, hq⟩⟩
 

src/Lean/AuxRecursor.lean

@@ -37,7 +37,7 @@ def isAuxRecursor (env : Environment) (declName : Name) : Bool :=
 
 def isAuxRecursorWithSuffix (env : Environment) (declName : Name) (suffix : String) : Bool :=
   match declName with
-  | .str _ s => (s == suffix || s.startsWith s!"{suffix}_") && isAuxRecursor env declName
+  | .str _ s => s == suffix && isAuxRecursor env declName
   | _ => false
 
 def isCasesOnRecursor (env : Environment) (declName : Name) : Bool :=

src/Lean/Elab/BuiltinTerm.lean

@@ -362,7 +362,4 @@ private opaque evalFilePath (stx : Syntax) : TermElabM System.FilePath
     mkStrLit <$> IO.FS.readFile path
   | _, _ => throwUnsupportedSyntax
 
-@[builtin_term_elab Lean.Parser.Term.namedPattern] def elabNamedPatternErr : TermElab := fun stx _ =>
-  throwError "`<identifier>@<term>` is a named pattern and can only be used in pattern matching contexts{indentD stx}"
-
 end Lean.Elab.Term

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -333,7 +333,7 @@ def tryContradiction (mvarId : MVarId) : MetaM Bool := do
 partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do
   let some eqs ← getEqnsFor? declName | throwError "failed to generate equations for '{declName}'"
   let tryEqns (mvarId : MVarId) : MetaM Bool :=
-    eqs.anyM fun eq => commitWhen do checkpointDefEq (mayPostpone := false) do
+    eqs.anyM fun eq => commitWhen do
       try
         let subgoals ← mvarId.apply (← mkConstWithFreshMVarLevels eq)
         subgoals.allM fun subgoal => do

src/Lean/Elab/PreDefinition/Structural/BRecOn.lean

@@ -245,7 +245,18 @@ def mkBRecOnConst (recArgInfos : Array RecArgInfo) (positions : Positions)
       decLevel brecOnUniv
     else
       pure brecOnUniv
-  let brecOnCons := fun idx => indGroup.brecOn useBInductionOn brecOnUniv idx
+  let brecOnCons := fun idx  =>
+    let brecOn :=
+      if let .some n := indGroup.all[idx]? then
+        if useBInductionOn then .const (mkBInductionOnName n) indGroup.levels
+        else                    .const (mkBRecOnName n) (brecOnUniv :: indGroup.levels)
+      else
+        let n := indGroup.all[0]!
+        let j := idx - indGroup.all.size + 1
+        if useBInductionOn then .const (mkBInductionOnName n |>.appendIndexAfter j) indGroup.levels
+        else                    .const (mkBRecOnName n |>.appendIndexAfter j) (brecOnUniv :: indGroup.levels)
+    mkAppN brecOn indGroup.params
+
   -- Pick one as a prototype
   let brecOnAux := brecOnCons 0
   -- Infer the type of the packed motive arguments

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -21,7 +21,6 @@ namespace Structural
 structure EqnInfo extends EqnInfoCore where
   recArgPos : Nat
   declNames : Array Name
-  numFixed  : Nat
   deriving Inhabited
 
 private partial def mkProof (declName : Name) (type : Expr) : MetaM Expr := do
@@ -82,11 +81,9 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
 
 builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
 
-def registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (recArgPos : Nat)
-    (numFixed : Nat) : CoreM Unit := do
+def registerEqnsInfo (preDef : PreDefinition) (declNames : Array Name) (recArgPos : Nat) : CoreM Unit := do
   ensureEqnReservedNamesAvailable preDef.declName
-  modifyEnv fun env => eqnInfoExt.insert env preDef.declName
-    { preDef with recArgPos, declNames, numFixed }
+  modifyEnv fun env => eqnInfoExt.insert env preDef.declName { preDef with recArgPos, declNames }
 
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   if let some info := eqnInfoExt.find? (← getEnv) declName then

src/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean

@@ -62,19 +62,6 @@ def IndGroupInst.isDefEq (igi1 igi2 : IndGroupInst) : MetaM Bool := do
   unless (← (igi1.params.zip igi2.params).allM (fun (e₁, e₂) => Meta.isDefEqGuarded e₁ e₂)) do return false
   return true
 
-/-- Instantiates the right `.brecOn` or `.bInductionOn` for the given type former index,
-including universe parameters and fixed prefix.  -/
-def IndGroupInst.brecOn (group : IndGroupInst) (ind : Bool) (lvl : Level) (idx : Nat) : Expr :=
-  let e := if let .some n := group.all[idx]? then
-      if ind then .const (mkBInductionOnName n) group.levels
-      else        .const (mkBRecOnName n)      (lvl :: group.levels)
-    else
-      let n := group.all[0]!
-      let j := idx - group.all.size + 1
-      if ind then .const (mkBInductionOnName n |>.appendIndexAfter j) group.levels
-      else        .const (mkBRecOnName n |>.appendIndexAfter j)       (lvl :: group.levels)
-  mkAppN e group.params
-
 /--
 Figures out the nested type formers of an inductive group, with parameters instantiated
 and indices still forall-abstracted.

src/Lean/Elab/PreDefinition/Structural/Main.lean

@@ -128,7 +128,7 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (xs : Array Expr
   return (Array.zip preDefs valuesNew).map fun ⟨preDef, valueNew⟩ => { preDef with value := valueNew }
 
 private def inferRecArgPos (preDefs : Array PreDefinition) (termArg?s : Array (Option TerminationArgument)) :
-    M (Array Nat × (Array PreDefinition) × Nat) := do
+    M (Array Nat × Array PreDefinition) := do
   withoutModifyingEnv do
     preDefs.forM (addAsAxiom ·)
     let fnNames := preDefs.map (·.declName)
@@ -154,7 +154,7 @@ private def inferRecArgPos (preDefs : Array PreDefinition) (termArg?s : Array (O
         withErasedFVars (xs.extract numFixed xs.size |>.map (·.fvarId!)) do
           let xs := xs[:numFixed]
           let preDefs' ← elimMutualRecursion preDefs xs recArgInfos
-          return (recArgPoss, preDefs', numFixed)
+          return (recArgPoss, preDefs')
 
 def reportTermArg (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit := do
   if let some ref := preDef.termination.terminationBy?? then
@@ -167,7 +167,7 @@ def reportTermArg (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit := do
 
 def structuralRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option TerminationArgument)) : TermElabM Unit := do
   let names := preDefs.map (·.declName)
-  let ((recArgPoss, preDefsNonRec, numFixed), state) ← run <| inferRecArgPos preDefs termArg?s
+  let ((recArgPoss, preDefsNonRec), state) ← run <| inferRecArgPos preDefs termArg?s
   for recArgPos in recArgPoss, preDef in preDefs do
     reportTermArg preDef recArgPos
   state.addMatchers.forM liftM
@@ -190,7 +190,7 @@ def structuralRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Opti
         for theorems and definitions that are propositions.
         See issue #2327
         -/
-        registerEqnsInfo preDef (preDefs.map (·.declName)) recArgPos numFixed
+        registerEqnsInfo preDef (preDefs.map (·.declName)) recArgPos
     addSmartUnfoldingDef preDef recArgPos
     markAsRecursive preDef.declName
   applyAttributesOf preDefsNonRec AttributeApplicationTime.afterCompilation

src/Lean/Util/FindExpr.lean

@@ -9,11 +9,48 @@ import Lean.Util.PtrSet
 
 namespace Lean
 namespace Expr
+namespace FindImpl
 
-@[extern "lean_find_expr"]
-opaque findImpl? (p : @& (Expr → Bool)) (e : @& Expr) : Option Expr
+unsafe abbrev FindM := StateT (PtrSet Expr) Id
 
-@[inline] def find? (p : Expr → Bool) (e : Expr) : Option Expr := findImpl? p e
+@[inline] unsafe def checkVisited (e : Expr) : OptionT FindM Unit := do
+  if (← get).contains e then
+    failure
+  modify fun s => s.insert e
+
+unsafe def findM? (p : Expr → Bool) (e : Expr) : OptionT FindM Expr :=
+  let rec visit (e : Expr) := do
+    checkVisited e
+    if p e then
+      pure e
+    else match e with
+      | .forallE _ d b _ => visit d <|> visit b
+      | .lam _ d b _     => visit d <|> visit b
+      | .mdata _ b       => visit b
+      | .letE _ t v b _  => visit t <|> visit v <|> visit b
+      | .app f a         => visit f <|> visit a
+      | .proj _ _ b      => visit b
+      | _                => failure
+  visit e
+
+unsafe def findUnsafe? (p : Expr → Bool) (e : Expr) : Option Expr :=
+  Id.run <| findM? p e |>.run' mkPtrSet
+
+end FindImpl
+
+@[implemented_by FindImpl.findUnsafe?]
+def find? (p : Expr → Bool) (e : Expr) : Option Expr :=
+  /- This is a reference implementation for the unsafe one above -/
+  if p e then
+    some e
+  else match e with
+    | .forallE _ d b _ => find? p d <|> find? p b
+    | .lam _ d b _     => find? p d <|> find? p b
+    | .mdata _ b       => find? p b
+    | .letE _ t v b _  => find? p t <|> find? p v <|> find? p b
+    | .app f a         => find? p f <|> find? p a
+    | .proj _ _ b      => find? p b
+    | _                => none
 
 /-- Return true if `e` occurs in `t` -/
 def occurs (e : Expr) (t : Expr) : Bool :=
@@ -27,13 +64,41 @@ inductive FindStep where
   /-- Search subterms -/ | visit
   /-- Do not search subterms -/ | done
 
-@[extern "lean_find_ext_expr"]
-opaque findExtImpl? (p : @& (Expr → FindStep)) (e : @& Expr) : Option Expr
+namespace FindExtImpl
+
+unsafe def findM? (p : Expr → FindStep) (e : Expr) : OptionT FindImpl.FindM Expr :=
+  visit e
+where
+  visitApp (e : Expr) :=
+    match e with
+    | .app f a .. => visitApp f <|> visit a
+    | e => visit e
+
+  visit (e : Expr) := do
+    FindImpl.checkVisited e
+    match p e with
+      | .done  => failure
+      | .found => pure e
+      | .visit =>
+        match e with
+        | .forallE _ d b _ => visit d <|> visit b
+        | .lam _ d b _     => visit d <|> visit b
+        | .mdata _ b       => visit b
+        | .letE _ t v b _  => visit t <|> visit v <|> visit b
+        | .app ..          => visitApp e
+        | .proj _ _ b      => visit b
+        | _                => failure
+
+unsafe def findUnsafe? (p : Expr → FindStep) (e : Expr) : Option Expr :=
+  Id.run <| findM? p e |>.run' mkPtrSet
+
+end FindExtImpl
 
 /--
   Similar to `find?`, but `p` can return `FindStep.done` to interrupt the search on subterms.
   Remark: Differently from `find?`, we do not invoke `p` for partial applications of an application. -/
-@[inline] def findExt? (p : Expr → FindStep) (e : Expr) : Option Expr := findExtImpl? p e
+@[implemented_by FindExtImpl.findUnsafe?]
+opaque findExt? (p : Expr → FindStep) (e : Expr) : Option Expr
 
 end Expr
 end Lean

src/Lean/Util/ReplaceExpr.lean

@@ -7,13 +7,62 @@ prelude
 import Lean.Expr
 import Lean.Util.PtrSet
 
-namespace Lean.Expr
+namespace Lean
+namespace Expr
 
-@[extern "lean_replace_expr"]
-opaque replaceImpl (f? : @& (Expr → Option Expr)) (e : @& Expr) : Expr
+namespace ReplaceImpl
 
-@[inline] def replace (f? : Expr → Option Expr) (e : Expr) : Expr :=
-  replaceImpl f? e
+unsafe abbrev ReplaceM := StateM (PtrMap Expr Expr)
+
+unsafe def cache (key : Expr) (exclusive : Bool)  (result : Expr) : ReplaceM Expr := do
+  unless exclusive do
+    modify (·.insert key result)
+  pure result
+
+@[specialize]
+unsafe def replaceUnsafeM (f? : Expr → Option Expr) (e : Expr) : ReplaceM Expr := do
+  let rec @[specialize] visit (e : Expr) := do
+    /-
+    TODO: We need better control over RC operations to ensure
+    the following (unsafe) optimization is correctly applied.
+    Optimization goal: only cache results for shared objects.
+
+    The main problem is that the current code generator ignores borrow annotations
+    for code written in Lean. These annotations are only taken into account for extern functions.
+
+    Moveover, the borrow inference heuristic currently tags `e` as "owned" since it may be stored
+    in the cache and is used in "update" functions.
+    Thus, when visiting `e` sub-expressions the code generator increases their RC
+    because we are recursively invoking `visit` :(
+
+    Thus, to fix this issue, we must
+    1- Take borrow annotations into account for code written in Lean.
+    2- Mark `e` is borrowed (i.e., `(e : @& Expr)`)
+    -/
+    let excl := isExclusiveUnsafe e
+    unless excl do
+      if let some result := (← get).find? e then
+        return result
+    match f? e with
+      | some eNew => cache e excl eNew
+      | none      => match e with
+        | .forallE _ d b _   => cache e excl <| e.updateForallE! (← visit d) (← visit b)
+        | .lam _ d b _       => cache e excl <| e.updateLambdaE! (← visit d) (← visit b)
+        | .mdata _ b         => cache e excl <| e.updateMData! (← visit b)
+        | .letE _ t v b _    => cache e excl <| e.updateLet! (← visit t) (← visit v) (← visit b)
+        | .app f a           => cache e excl <| e.updateApp! (← visit f) (← visit a)
+        | .proj _ _ b        => cache e excl <| e.updateProj! (← visit b)
+        | e                  => return e
+  visit e
+
+@[inline]
+unsafe def replaceUnsafe (f? : Expr → Option Expr) (e : Expr) : Expr :=
+  (replaceUnsafeM f? e).run' mkPtrMap
+
+end ReplaceImpl
+
+/- TODO: use withPtrAddr, withPtrEq to avoid unsafe tricks above.
+   We also need an invariant at `State` and proofs for the `uget` operations. -/
 
 @[specialize]
 def replaceNoCache (f? : Expr → Option Expr) (e : Expr) : Expr :=
@@ -28,4 +77,6 @@ def replaceNoCache (f? : Expr → Option Expr) (e : Expr) : Expr :=
     | .proj _ _ b      => let b := replaceNoCache f? b; e.updateProj! b
     | e                => e
 
-end Lean.Expr
+@[implemented_by ReplaceImpl.replaceUnsafe]
+partial def replace (f? : Expr → Option Expr) (e : Expr) : Expr :=
+  e.replaceNoCache f?

src/kernel/cache_stack.h

@@ -0,0 +1,41 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <vector>
+#include <memory>
+#include "runtime/debug.h"
+
+/** \brief Macro for creating a stack of objects of type Cache in thread local storage.
+    The argument \c Arg is provided to every new instance of Cache.
+    The macro provides the helper class Cache_ref that "reuses" cache objects from the stack.
+*/
+#define MK_CACHE_STACK(Cache, Arg)                                      \
+struct Cache ## _stack {                                                \
+    unsigned                                     m_top;                 \
+    std::vector<std::unique_ptr<Cache>> m_cache_stack;                  \
+    Cache ## _stack():m_top(0) {}                                       \
+};                                                                      \
+MK_THREAD_LOCAL_GET_DEF(Cache ## _stack, get_ ## Cache ## _stack);      \
+class Cache ## _ref {                                                   \
+    Cache * m_cache;                                                    \
+public:                                                                 \
+    Cache ## _ref() {                                                   \
+        Cache ## _stack & s = get_ ## Cache ## _stack();                \
+        lean_assert(s.m_top <= s.m_cache_stack.size());                 \
+        if (s.m_top == s.m_cache_stack.size())                          \
+            s.m_cache_stack.push_back(std::unique_ptr<Cache>(new Cache(Arg))); \
+        m_cache = s.m_cache_stack[s.m_top].get();                       \
+        s.m_top++;                                                      \
+    }                                                                   \
+    ~Cache ## _ref() {                                                  \
+        Cache ## _stack & s = get_ ## Cache ## _stack();                \
+        lean_assert(s.m_top > 0);                                       \
+        s.m_top--;                                                      \
+        m_cache->clear();                                               \
+    }                                                                   \
+    Cache * operator->() const { return m_cache; }                      \
+};

src/kernel/declaration.cpp

@@ -161,7 +161,7 @@ bool declaration::is_unsafe() const {
 
 bool use_unsafe(environment const & env, expr const & e) {
     bool found = false;
-    for_each(e, [&](expr const & e) {
+    for_each(e, [&](expr const & e, unsigned) {
             if (found) return false;
             if (is_constant(e)) {
                 if (auto info = env.find(const_name(e))) {
@@ -181,7 +181,7 @@ declaration::declaration():declaration(*g_dummy) {}
 
 static unsigned get_max_height(environment const & env, expr const & v) {
     unsigned h = 0;
-    for_each(v, [&](expr const & e) {
+    for_each(v, [&](expr const & e, unsigned) {
             if (is_constant(e)) {
                 auto d = env.find(const_name(e));
                 if (d && d->get_hints().get_height() > h)

src/kernel/expr.cpp

@@ -498,7 +498,7 @@ optional<expr> has_expr_metavar_strict(expr const & e) {
     if (!has_expr_metavar(e))
         return none_expr();
     optional<expr> r;
-    for_each(e, [&](expr const & e) {
+    for_each(e, [&](expr const & e, unsigned) {
             if (r || !has_expr_metavar(e)) return false;
             if (is_metavar_app(e)) { r = e; return false; }
             return true;

src/kernel/for_each_fn.cpp

@@ -5,221 +5,119 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <vector>
-#include <unordered_map>
 #include <utility>
 #include "runtime/memory.h"
 #include "runtime/interrupt.h"
 #include "runtime/flet.h"
 #include "kernel/for_each_fn.h"
+#include "kernel/cache_stack.h"
+
+#ifndef LEAN_DEFAULT_FOR_EACH_CACHE_CAPACITY
+#define LEAN_DEFAULT_FOR_EACH_CACHE_CAPACITY 1024*8
+#endif
 
 namespace lean {
-
-/*
-If `partial_apps = true`, then given a term `g a b`, we also apply the function `m_f` to `g a`,
-and not only to `g`, `a`, and `b`.
-*/
-template<bool partial_apps> class for_each_fn {
-    std::unordered_set<lean_object *> m_cache;
-    std::function<bool(expr const &)> m_f; // NOLINT
-
-    bool visited(expr const & e) {
-        if (!is_shared(e)) return false;
-        if (m_cache.find(e.raw()) != m_cache.end()) return true;
-        m_cache.insert(e.raw());
-        return false;
-    }
-
-    void apply_fn(expr const & e) {
-        if (is_app(e)) {
-            apply_fn(app_fn(e));
-            apply(app_arg(e));
-        } else {
-            apply(e);
-        }
-    }
-
-    void apply(expr const & e) {
-        switch (e.kind()) {
-        case expr_kind::Const: case expr_kind::BVar: case expr_kind::Sort:
-            m_f(e);
-            return;
-        default:
-            break;
-        }
-
-        if (visited(e))
-            return;
-
-        if (!m_f(e))
-            return;
-
-        switch (e.kind()) {
-        case expr_kind::Const: case expr_kind::BVar:
-        case expr_kind::Sort:  case expr_kind::Lit:
-        case expr_kind::MVar:  case expr_kind::FVar:
-            return;
-        case expr_kind::MData:
-            apply(mdata_expr(e));
-            return;
-        case expr_kind::Proj:
-            apply(proj_expr(e));
-            return;
-        case expr_kind::App:
-            if (partial_apps)
-                apply(app_fn(e));
-            else
-                apply_fn(app_fn(e));
-            apply(app_arg(e));
-            return;
-        case expr_kind::Lambda: case expr_kind::Pi:
-            apply(binding_domain(e));
-            apply(binding_body(e));
-            return;
-        case expr_kind::Let:
-            apply(let_type(e));
-            apply(let_value(e));
-            apply(let_body(e));
-            return;
-        }
-    }
-
-public:
-    for_each_fn(std::function<bool(expr const &)> && f):m_f(f) {}        // NOLINT
-    for_each_fn(std::function<bool(expr const &)> const & f):m_f(f) {}   // NOLINT
-    void operator()(expr const & e) { apply(e); }
-};
-
-class for_each_offset_fn {
-    struct key_hasher {
-        std::size_t operator()(std::pair<lean_object *, unsigned> const & p) const {
-            return hash((size_t)p.first, p.second);
-        }
+struct for_each_cache {
+    struct entry {
+        object const *    m_cell;
+        unsigned          m_offset;
+        entry():m_cell(nullptr) {}
     };
-    std::unordered_set<std::pair<lean_object *, unsigned>, key_hasher> m_cache;
-    std::function<bool(expr const &, unsigned)> m_f; // NOLINT
+    unsigned              m_capacity;
+    std::vector<entry>    m_cache;
+    std::vector<unsigned> m_used;
+    for_each_cache(unsigned c):m_capacity(c), m_cache(c) {}
 
     bool visited(expr const & e, unsigned offset) {
-        if (!is_shared(e)) return false;
-        if (m_cache.find(std::make_pair(e.raw(), offset)) != m_cache.end()) return true;
-        m_cache.insert(std::make_pair(e.raw(), offset));
-        return false;
+        unsigned i = hash(hash(e), offset) % m_capacity;
+        if (m_cache[i].m_cell == e.raw() && m_cache[i].m_offset == offset) {
+            return true;
+        } else {
+            if (m_cache[i].m_cell == nullptr)
+                m_used.push_back(i);
+            m_cache[i].m_cell   = e.raw();
+            m_cache[i].m_offset = offset;
+            return false;
+        }
     }
 
+    void clear() {
+        for (unsigned i : m_used)
+            m_cache[i].m_cell = nullptr;
+        m_used.clear();
+    }
+};
+
+/* CACHE_RESET: NO */
+MK_CACHE_STACK(for_each_cache, LEAN_DEFAULT_FOR_EACH_CACHE_CAPACITY)
+
+class for_each_fn {
+    for_each_cache_ref                          m_cache;
+    std::function<bool(expr const &, unsigned)> m_f; // NOLINT
+
     void apply(expr const & e, unsigned offset) {
-        switch (e.kind()) {
-        case expr_kind::Const: case expr_kind::BVar: case expr_kind::Sort:
-            m_f(e, offset);
-            return;
-        default:
-            break;
-        }
+        buffer<pair<expr const &, unsigned>> todo;
+        todo.emplace_back(e, offset);
+        while (true) {
+          begin_loop:
+            if (todo.empty())
+                break;
+            check_memory("expression traversal");
+            auto p = todo.back();
+            todo.pop_back();
+            expr const & e  = p.first;
+            unsigned offset = p.second;
 
-        if (visited(e, offset))
-            return;
+            switch (e.kind()) {
+            case expr_kind::Const: case expr_kind::BVar:
+            case expr_kind::Sort:
+                m_f(e, offset);
+                goto begin_loop;
+            default:
+                break;
+            }
 
-        if (!m_f(e, offset))
-            return;
+            if (is_shared(e) && m_cache->visited(e, offset))
+                goto begin_loop;
 
-        switch (e.kind()) {
-        case expr_kind::Const: case expr_kind::BVar:
-        case expr_kind::Sort:  case expr_kind::Lit:
-        case expr_kind::MVar:  case expr_kind::FVar:
-            return;
-        case expr_kind::MData:
-            apply(mdata_expr(e), offset);
-            return;
-        case expr_kind::Proj:
-            apply(proj_expr(e), offset);
-            return;
-        case expr_kind::App:
-            apply(app_fn(e), offset);
-            apply(app_arg(e), offset);
-            return;
-        case expr_kind::Lambda: case expr_kind::Pi:
-            apply(binding_domain(e), offset);
-            apply(binding_body(e), offset+1);
-            return;
-        case expr_kind::Let:
-            apply(let_type(e), offset);
-            apply(let_value(e), offset);
-            apply(let_body(e), offset+1);
-            return;
+            if (!m_f(e, offset))
+                goto begin_loop;
+
+            switch (e.kind()) {
+            case expr_kind::Const: case expr_kind::BVar:
+            case expr_kind::Sort:  case expr_kind::Lit:
+            case expr_kind::MVar:  case expr_kind::FVar:
+                goto begin_loop;
+            case expr_kind::MData:
+                todo.emplace_back(mdata_expr(e), offset);
+                goto begin_loop;
+            case expr_kind::Proj:
+                todo.emplace_back(proj_expr(e), offset);
+                goto begin_loop;
+            case expr_kind::App:
+                todo.emplace_back(app_arg(e), offset);
+                todo.emplace_back(app_fn(e), offset);
+                goto begin_loop;
+            case expr_kind::Lambda: case expr_kind::Pi:
+                todo.emplace_back(binding_body(e), offset + 1);
+                todo.emplace_back(binding_domain(e), offset);
+                goto begin_loop;
+            case expr_kind::Let:
+                todo.emplace_back(let_body(e), offset + 1);
+                todo.emplace_back(let_value(e), offset);
+                todo.emplace_back(let_type(e), offset);
+                goto begin_loop;
+            }
         }
     }
 
 public:
-    for_each_offset_fn(std::function<bool(expr const &, unsigned)> && f):m_f(f) {}        // NOLINT
-    for_each_offset_fn(std::function<bool(expr const &, unsigned)> const & f):m_f(f) {}   // NOLINT
+    for_each_fn(std::function<bool(expr const &, unsigned)> && f):m_f(f) {}        // NOLINT
+    for_each_fn(std::function<bool(expr const &, unsigned)> const & f):m_f(f) {}   // NOLINT
     void operator()(expr const & e) { apply(e, 0); }
 };
 
-void for_each(expr const & e, std::function<bool(expr const &)> && f) { // NOLINT
-    return for_each_fn<true>(f)(e);
-}
-
 void for_each(expr const & e, std::function<bool(expr const &, unsigned)> && f) { // NOLINT
-    return for_each_offset_fn(f)(e);
-}
-
-extern "C" LEAN_EXPORT obj_res lean_find_expr(b_obj_arg p, b_obj_arg e_) {
-    lean_object * found = nullptr;
-    expr const & e = TO_REF(expr, e_);
-    for_each_fn<true>([&](expr const & e) {
-        if (found != nullptr) return false;
-        lean_inc(p);
-        lean_inc(e.raw());
-        if (lean_unbox(lean_apply_1(p, e.raw()))) {
-            found = e.raw();
-            return false;
-        }
-        return true;
-    })(e);
-    if (found) {
-        lean_inc(found);
-        lean_object * r = lean_alloc_ctor(1, 1, 0);
-        lean_ctor_set(r, 0, found);
-        return r;
-    } else {
-        return lean_box(0);
-    }
-}
-
-/*
-Similar to `lean_find_expr`, but `p` returns
-```
-inductive FindStep where
-  /-- Found desired subterm -/ | found
-  /-- Search subterms -/ | visit
-  /-- Do not search subterms -/ | done
-```
-*/
-extern "C" LEAN_EXPORT obj_res lean_find_ext_expr(b_obj_arg p, b_obj_arg e_) {
-    lean_object * found = nullptr;
-    expr const & e = TO_REF(expr, e_);
-    // Recall that `findExt?` skips partial applications.
-    for_each_fn<false>([&](expr const & e) {
-        if (found != nullptr) return false;
-        lean_inc(p);
-        lean_inc(e.raw());
-        switch(lean_unbox(lean_apply_1(p, e.raw()))) {
-        case 0: // found
-            found = e.raw();
-            return false;
-        case 1: // visit
-            return true;
-        case 2: // done
-            return false;
-        default:
-            lean_unreachable();
-        }
-    })(e);
-    if (found) {
-        lean_inc(found);
-        lean_object * r = lean_alloc_ctor(1, 1, 0);
-        lean_ctor_set(r, 0, found);
-        return r;
-    } else {
-        return lean_box(0);
-    }
+    return for_each_fn(f)(e);
 }
 }

src/kernel/for_each_fn.h

@@ -13,18 +13,15 @@ Author: Leonardo de Moura
 #include "kernel/expr_sets.h"
 
 namespace lean {
-/**
-\brief Expression visitor.
+/** \brief Expression visitor.
 
-The argument \c f must be a lambda (function object) containing the method
+    The argument \c f must be a lambda (function object) containing the method
 
-<code>
-bool operator()(expr const & e, unsigned offset)
-</code>
+    <code>
+    bool operator()(expr const & e, unsigned offset)
+    </code>
 
-The \c offset is the number of binders under which \c e occurs.
+    The \c offset is the number of binders under which \c e occurs.
 */
 void for_each(expr const & e, std::function<bool(expr const &, unsigned)> && f); // NOLINT
-
-void for_each(expr const & e, std::function<bool(expr const &)> && f); // NOLINT
 }

src/kernel/replace_fn.cpp

@@ -6,35 +6,75 @@ Author: Leonardo de Moura
 */
 #include <vector>
 #include <memory>
-#include <unordered_map>
 #include "kernel/replace_fn.h"
+#include "kernel/cache_stack.h"
+
+#ifndef LEAN_DEFAULT_REPLACE_CACHE_CAPACITY
+#define LEAN_DEFAULT_REPLACE_CACHE_CAPACITY 1024*8
+#endif
 
 namespace lean {
+struct replace_cache {
+    struct entry {
+        object  *  m_cell;
+        unsigned   m_offset;
+        expr       m_result;
+        entry():m_cell(nullptr) {}
+    };
+    unsigned              m_capacity;
+    std::vector<entry>    m_cache;
+    std::vector<unsigned> m_used;
+    replace_cache(unsigned c):m_capacity(c), m_cache(c) {}
+
+    expr * find(expr const & e, unsigned offset) {
+        unsigned i = hash(hash(e), offset) % m_capacity;
+        if (m_cache[i].m_cell == e.raw() && m_cache[i].m_offset == offset)
+            return &m_cache[i].m_result;
+        else
+            return nullptr;
+    }
+
+    void insert(expr const & e, unsigned offset, expr const & v) {
+        unsigned i = hash(hash(e), offset) % m_capacity;
+        if (m_cache[i].m_cell == nullptr)
+            m_used.push_back(i);
+        m_cache[i].m_cell   = e.raw();
+        m_cache[i].m_offset = offset;
+        m_cache[i].m_result = v;
+    }
+
+    void clear() {
+        for (unsigned i : m_used) {
+            m_cache[i].m_cell   = nullptr;
+            m_cache[i].m_result = expr();
+        }
+        m_used.clear();
+    }
+};
+
+/* CACHE_RESET: NO */
+MK_CACHE_STACK(replace_cache, LEAN_DEFAULT_REPLACE_CACHE_CAPACITY)
 
 class replace_rec_fn {
-    struct key_hasher {
-        std::size_t operator()(std::pair<lean_object *, unsigned> const & p) const {
-            return hash((size_t)p.first, p.second);
-        }
-    };
-    std::unordered_map<std::pair<lean_object *, unsigned>, expr, key_hasher> m_cache;
+    replace_cache_ref                                     m_cache;
     std::function<optional<expr>(expr const &, unsigned)> m_f;
     bool                                                  m_use_cache;
 
     expr save_result(expr const & e, unsigned offset, expr const & r, bool shared) {
         if (shared)
-            m_cache.insert(mk_pair(mk_pair(e.raw(), offset), r));
+            m_cache->insert(e, offset, r);
         return r;
     }
 
     expr apply(expr const & e, unsigned offset) {
         bool shared = false;
         if (m_use_cache && is_shared(e)) {
-            auto it = m_cache.find(mk_pair(e.raw(), offset));
-            if (it != m_cache.end())
-                return it->second;
+            if (auto r = m_cache->find(e, offset))
+                return *r;
             shared = true;
         }
+        check_system("replace");
+
         if (optional<expr> r = m_f(e, offset)) {
             return save_result(e, offset, *r, shared);
         } else {
@@ -81,73 +121,4 @@ public:
 expr replace(expr const & e, std::function<optional<expr>(expr const &, unsigned)> const & f, bool use_cache) {
     return replace_rec_fn(f, use_cache)(e);
 }
-
-class replace_fn {
-    std::unordered_map<lean_object *, expr> m_cache;
-    lean_object * m_f;
-
-    expr save_result(expr const & e, expr const & r, bool shared) {
-        if (shared)
-            m_cache.insert(mk_pair(e.raw(), r));
-        return r;
-    }
-
-    expr apply(expr const & e) {
-        bool shared = false;
-        if (is_shared(e)) {
-            auto it = m_cache.find(e.raw());
-            if (it != m_cache.end())
-                return it->second;
-            shared = true;
-        }
-
-        lean_inc(e.raw());
-        lean_inc_ref(m_f);
-        lean_object * r = lean_apply_1(m_f, e.raw());
-        if (!lean_is_scalar(r)) {
-            expr e_new(lean_ctor_get(r, 0), true);
-            lean_dec_ref(r);
-            return save_result(e, e_new, shared);
-        }
-
-        switch (e.kind()) {
-        case expr_kind::Const: case expr_kind::Sort:
-        case expr_kind::BVar:  case expr_kind::Lit:
-        case expr_kind::MVar:  case expr_kind::FVar:
-            return save_result(e, e, shared);
-        case expr_kind::MData: {
-            expr new_e = apply(mdata_expr(e));
-            return save_result(e, update_mdata(e, new_e), shared);
-        }
-        case expr_kind::Proj: {
-            expr new_e = apply(proj_expr(e));
-            return save_result(e, update_proj(e, new_e), shared);
-        }
-        case expr_kind::App: {
-            expr new_f = apply(app_fn(e));
-            expr new_a = apply(app_arg(e));
-            return save_result(e, update_app(e, new_f, new_a), shared);
-        }
-        case expr_kind::Pi: case expr_kind::Lambda: {
-            expr new_d = apply(binding_domain(e));
-            expr new_b = apply(binding_body(e));
-            return save_result(e, update_binding(e, new_d, new_b), shared);
-        }
-        case expr_kind::Let: {
-            expr new_t = apply(let_type(e));
-            expr new_v = apply(let_value(e));
-            expr new_b = apply(let_body(e));
-            return save_result(e, update_let(e, new_t, new_v, new_b), shared);
-        }}
-        lean_unreachable();
-    }
-public:
-    replace_fn(lean_object * f):m_f(f) {}
-    expr operator()(expr const & e) { return apply(e); }
-};
-
-extern "C" LEAN_EXPORT obj_res lean_replace_expr(b_obj_arg f, b_obj_arg e) {
-    expr r = replace_fn(f)(TO_REF(expr, e));
-    return r.steal();
-}
 }

src/kernel/type_checker.cpp

@@ -185,7 +185,7 @@ expr type_checker::infer_app(expr const & e, bool infer_only) {
 
 static void mark_used(unsigned n, expr const * fvars, expr const & b, bool * used) {
     if (!has_fvar(b)) return;
-    for_each(b, [&](expr const & x) {
+    for_each(b, [&](expr const & x, unsigned) {
             if (!has_fvar(x)) return false;
             if (is_fvar(x)) {
                 for (unsigned i = 0; i < n; i++) {

tests/lean/run/4662.lean

@@ -1,15 +0,0 @@
-/--
-error: `<identifier>@<term>` is a named pattern and can only be used in pattern matching contexts
-  p@()
--/
-#guard_msgs in
-def minimal : Unit -> Unit := by
-  intro i
-  let k:p@() := i
-  sorry
-
-def minimal2 : Unit -> Unit := by
-  intro i
-  let p@k:() := i
-  guard_hyp k : p = ()
-  exact ()

tests/lean/run/4673.lean

@@ -1,20 +0,0 @@
-def iscoh_wmap {A:Type _}{B:Type _} : (A -> B) -> Type _ :=
-  fun f => @Subtype (B -> A) fun r => ∀ a , a = r (f a)
-def wmap : Type _ -> Type _ -> Type _ :=
-  fun A B => @Sigma (A -> B) fun f => iscoh_wmap f
-
-def hgroup : Nat -> Type _ -> Type _
-| .zero , T => wmap T T
-| .succ a, T => wmap (hgroup a T) (hgroup a T)
-
-example : hgroup 0 Unit := by
-  unfold hgroup
-  admit
-
--- TODO: we should improve univere inference. It should be
--- hgroup.{u} : Nat → Type u → Type u
-/--
-info: hgroup.{u_1, u_2} : Nat → Type (max u_1 u_2) → Type (max u_1 u_2)
--/
-#guard_msgs in
-#check hgroup

tests/lean/run/funind_structural.lean

@@ -1,3 +1,6 @@
+import Lean.Elab.Command
+import Lean.Elab.PreDefinition.Structural.Eqns
+
 /-!
 This module tests functional induction principles on *structurally* recursive functions.
 -/
@@ -5,7 +8,6 @@ This module tests functional induction principles on *structurally* recursive fu
 def fib : Nat → Nat
   | 0 | 1 => 0
   | n+2 => fib n + fib (n+1)
-termination_by structural x => x
 
 /--
 info: fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
@@ -18,7 +20,6 @@ info: fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
 def binary : Nat → Nat → Nat
   | 0, acc | 1, acc => 1 + acc
   | n+2, acc => binary n (binary (n+1) acc)
-termination_by structural x => x
 
 /--
 info: binary.induct (motive : Nat → Nat → Prop) (case1 : ∀ (acc : Nat), motive 0 acc) (case2 : ∀ (acc : Nat), motive 1 acc)
@@ -33,7 +34,6 @@ info: binary.induct (motive : Nat → Nat → Prop) (case1 : ∀ (acc : Nat), mo
 def binary' : Bool → Nat → Bool
   | acc, 0 | acc , 1 => not acc
   | acc, n+2 => binary' (binary' acc (n+1)) n
-termination_by structural _ x => x
 
 /--
 info: binary'.induct (motive : Bool → Nat → Prop) (case1 : ∀ (acc : Bool), motive acc 0)
@@ -48,7 +48,6 @@ def zip {α β} : List α → List β → List (α × β)
   | [], _ => []
   | _, [] => []
   | x::xs, y::ys => (x, y) :: zip xs ys
-termination_by structural x => x
 
 /--
 info: zip.induct.{u_1, u_2} {α : Type u_1} {β : Type u_2} (motive : List α → List β → Prop)
@@ -85,7 +84,6 @@ def Finn.min (x : Bool) {n : Nat} (m : Nat) : Finn n → (f : Finn n) → Finn n
   | fzero, _ => fzero
   | _, fzero => fzero
   | fsucc i, fsucc j => fsucc (Finn.min (not x) (m + 1) i j)
-termination_by structural n
 
 /--
 info: Finn.min.induct (motive : Bool → {n : Nat} → Nat → Finn n → Finn n → Prop)
@@ -97,6 +95,8 @@ info: Finn.min.induct (motive : Bool → {n : Nat} → Nat → Finn n → Finn n
 #guard_msgs in
 #check Finn.min.induct
 
+
+
 namespace TreeExample
 
 inductive Tree (β : Type v) where
@@ -113,7 +113,6 @@ def Tree.insert (t : Tree β) (k : Nat) (v : β) : Tree β :=
       node left key value (right.insert k v)
     else
       node left k v right
-termination_by structural t
 
 /--
 info: TreeExample.Tree.insert.induct.{u_1} {β : Type u_1} (motive : Tree β → Nat → β → Prop)
@@ -175,7 +174,6 @@ def Term.denote : Term ctx ty → HList Ty.denote ctx → ty.denote
   | .app f a,   env => f.denote env (a.denote env)
   | .lam b,     env => fun x => b.denote (.cons x env)
   | .let a b,   env => b.denote (.cons (a.denote env) env)
-termination_by structural x => x
 
 /--
 info: TermDenote.Term.denote.induct (motive : {ctx : List Ty} → {ty : Ty} → Term ctx ty → HList Ty.denote ctx → Prop)

tests/lean/run/structuralMutual.lean

@@ -215,8 +215,6 @@ namespace EvenOdd
 
 -- Mutual structural recursion over a non-mutual inductive type
 
--- (The functions don't actually implement even/odd, but that isn't the point here.)
-
 mutual
   def Even : Nat → Prop
     | 0 => True
@@ -520,13 +518,13 @@ Too many possible combinations of parameters of type Nattish (or please indicate
 Could not find a decreasing measure.
 The arguments relate at each recursive call as follows:
 (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
-Call from ManyCombinations.f to ManyCombinations.g at 552:15-29:
+Call from ManyCombinations.f to ManyCombinations.g at 550:15-29:
    #1 #2 #3 #4
 #5  ?  ?  ?  ?
 #6  ?  =  ?  ?
 #7  ?  ?  =  ?
 #8  ?  ?  ?  =
-Call from ManyCombinations.g to ManyCombinations.f at 555:15-29:
+Call from ManyCombinations.g to ManyCombinations.f at 553:15-29:
    #5 #6 #7 #8
 #1  _  _  _  _
 #2  _  =  _  _