withRestoreOrSaveFull: old? ~> reusableResult?

src/Lean/CoreM.lean

@@ -219,25 +219,25 @@ def saveState : CoreM SavedState := do
   return { toState := s, passedHearbeats := 0 }
 
 /--
-Incremental reuse primitive: if `old?` is `none`, runs `cont` with an action `save` that on
-execution returns the saved monadic state at this point including the heartbeats used by `cont` so
-far. If `old?` on the other hand is `some (a, state)`, restores full `state` including heartbeats
-used and returns `a`.
-
-The intention is for steps that support incremental reuse to initially pass `none` as `old?` and
-call `save` as late as possible in `cont`. In a further run, if reuse is possible, `old?` should be
-set to the previous state and result, ensuring that the state after running `withRestoreOrSaveFull`
-is identical in both runs. Note however that necessarily this is only an approximation in the case
-of heartbeats as heartbeats used by `withRestoreOrSaveFull`, by the remainder of `cont` after
-calling `save`, as well as by reuse-handling code such as the one supplying `old?` are not accounted
-for.
+Incremental reuse primitive: if `reusableResult?` is `none`, runs `cont` with an action `save` that
+on execution returns the saved monadic state at this point including the heartbeats used by `cont`
+so far. If `reusableResult?` on the other hand is `some (a, state)`, restores full `state` including
+heartbeats used and returns `a`.
+
+The intention is for steps that support incremental reuse to initially pass `none` as
+`reusableResult?` and call `save` as late as possible in `cont`. In a further run, if reuse is
+possible, `reusableResult?` should be set to the previous state and result, ensuring that the state
+after running `withRestoreOrSaveFull` is identical in both runs. Note however that necessarily this
+is only an approximation in the case of heartbeats as heartbeats used by `withRestoreOrSaveFull`, by
+the remainder of `cont` after calling `save`, as well as by reuse-handling code such as the one
+supplying `reusableResult?` are not accounted for.
 -/
-@[specialize] def withRestoreOrSaveFull (old? : Option (α × SavedState))
+@[specialize] def withRestoreOrSaveFull (reusableResult? : Option (α × SavedState))
     (cont : (save : CoreM SavedState) → CoreM α) : CoreM α := do
-  if let some (oldVal, oldState) := old? then
-    set oldState.toState
-    IO.addHeartbeats oldState.passedHearbeats.toUInt64
-    return oldVal
+  if let some (val, state) := reusableResult? then
+    set state.toState
+    IO.addHeartbeats state.passedHearbeats.toUInt64
+    return val
 
   let startHeartbeats ← IO.getNumHeartbeats
   cont (do

src/Lean/Elab/Tactic/Basic.lean

@@ -97,13 +97,13 @@ def SavedState.restore (b : SavedState) (restoreInfo := false) : TacticM Unit :=
   set b.tactic
 
 @[specialize, inherit_doc Core.withRestoreOrSaveFull]
-def withRestoreOrSaveFull (old? : Option (α × SavedState))
+def withRestoreOrSaveFull (reusableResult? : Option (α × SavedState))
     (cont : TacticM SavedState → TacticM α) : TacticM α := do
-  if let some (_, oldState) := old? then
-    set oldState.tactic
-  let old? := old?.map (fun (oldVal, oldState) => (oldVal, oldState.term))
+  if let some (_, state) := reusableResult? then
+    set state.tactic
+  let reusableResult? := reusableResult?.map (fun (val, state) => (val, state.term))
   controlAt TermElabM fun runInBase =>
-    Term.withRestoreOrSaveFull old? fun restore =>
+    Term.withRestoreOrSaveFull reusableResult? fun restore =>
       runInBase <| cont (return { term := (← restore), tactic := (← get) })
 
 protected def getCurrMacroScope : TacticM MacroScope := do pure (← readThe Core.Context).currMacroScope

src/Lean/Elab/Term.lean

@@ -306,13 +306,13 @@ def SavedState.restore (s : SavedState) (restoreInfo : Bool := false) : TermElab
     setInfoState infoState
 
 @[specialize, inherit_doc Core.withRestoreOrSaveFull]
-def withRestoreOrSaveFull (old? : Option (α × SavedState))
+def withRestoreOrSaveFull (reusableResult? : Option (α × SavedState))
     (cont : TermElabM SavedState → TermElabM α) : TermElabM α := do
-  if let some (_, oldState) := old? then
-    set oldState.elab
-  let old? := old?.map (fun (oldVal, oldState) => (oldVal, oldState.meta))
+  if let some (_, state) := reusableResult? then
+    set state.elab
+  let reusableResult? := reusableResult?.map (fun (val, state) => (val, state.meta))
   controlAt MetaM fun runInBase =>
-    Meta.withRestoreOrSaveFull old? fun restore =>
+    Meta.withRestoreOrSaveFull reusableResult? fun restore =>
       runInBase <| cont (return { meta := (← restore), «elab» := (← get) })
 
 instance : MonadBacktrack SavedState TermElabM where

src/Lean/Meta/Basic.lean

@@ -418,13 +418,13 @@ def SavedState.restore (b : SavedState) : MetaM Unit := do
   modify fun s => { s with mctx := b.meta.mctx, zetaDeltaFVarIds := b.meta.zetaDeltaFVarIds, postponed := b.meta.postponed }
 
 @[specialize, inherit_doc Core.withRestoreOrSaveFull]
-def withRestoreOrSaveFull (old? : Option (α × SavedState))
+def withRestoreOrSaveFull (reusableResult? : Option (α × SavedState))
     (cont : MetaM SavedState → MetaM α) : MetaM α := do
-  if let some (_, oldState) := old? then
-    set oldState.meta
-  let old? := old?.map (fun (oldVal, oldState) => (oldVal, oldState.core))
+  if let some (_, state) := reusableResult? then
+    set state.meta
+  let reusableResult? := reusableResult?.map (fun (val, state) => (val, state.core))
   controlAt CoreM fun runInCoreM =>
-    Core.withRestoreOrSaveFull old? fun restore =>
+    Core.withRestoreOrSaveFull reusableResult? fun restore =>
       runInCoreM <| cont (return { core := (← restore), meta := (← get) })
 
 instance : MonadBacktrack SavedState MetaM where