From d4a67baa8ecb968504459dfebeadb3022bc70621 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 22 Oct 2020 17:40:30 -0700
Subject: [PATCH] refactor: rename `MonadFinally.finally'` =>
 `MonadFinally.tryFinally'`

---
 src/Init/Control/EState.lean |  2 +-
 src/Init/Control/Except.lean | 16 ++++++++++------
 src/Init/Control/Reader.lean |  4 ++--
 src/Init/Control/State.lean  |  6 +++---
 src/Lean/Elab/Do.lean        |  2 +-
 5 files changed, 17 insertions(+), 13 deletions(-)

diff --git a/src/Init/Control/EState.lean b/src/Init/Control/EState.lean
index d63b97bddb..0df0dc933f 100644
--- a/src/Init/Control/EState.lean
+++ b/src/Init/Control/EState.lean
@@ -120,7 +120,7 @@ instance {δ} [Backtrackable δ σ] : MonadExceptOf ε (EStateM ε σ) :=
 { throw := @EStateM.throw _ _, tryCatch := @EStateM.tryCatch _ _ _ _ }
 
 instance : MonadFinally (EStateM ε σ) :=
-{ finally' := fun α β x h s =>
+{ tryFinally' := fun α β x h s =>
   let r := x s;
   match r with
   | Result.ok a s    => match h (some a) s with
diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean
index 14311dc3d3..cae3d1f61f 100644
--- a/src/Init/Control/Except.lean
+++ b/src/Init/Control/Except.lean
@@ -188,23 +188,27 @@ instance ExceptT.monadControl (ε : Type u) (m : Type u → Type v) [Monad m] :
 }
 
 class MonadFinally (m : Type u → Type v) :=
-(finally' {α β} : m α → (Option α → m β) → m (α × β))
+(tryFinally' {α β} : m α → (Option α → m β) → m (α × β))
 
-export MonadFinally (finally')
+export MonadFinally (tryFinally')
 
 /-- Execute `x` and then execute `finalizer` even if `x` threw an exception -/
+@[inline] abbrev tryFinally {m : Type u → Type v} {α β : Type u} [MonadFinally m] [Functor m] (x : m α) (finalizer : m β) : m α := do
+Prod.fst <$> tryFinally' x (fun _ => finalizer)
+
+-- TODO delete
 @[inline] abbrev finally {m : Type u → Type v} {α β : Type u} [MonadFinally m] [Functor m] (x : m α) (finalizer : m β) : m α := do
-Prod.fst <$> finally' x (fun _ => finalizer)
+Prod.fst <$> tryFinally' x (fun _ => finalizer)
 
 instance Id.finally : MonadFinally Id :=
-{ finally' := fun α β x h =>
+{ tryFinally' := fun α β x h =>
    let a := x;
    let b := h (some x);
    pure (a, b) }
 
 instance ExceptT.finally {m : Type u → Type v} {ε : Type u} [MonadFinally m] [Monad m] : MonadFinally (ExceptT ε m) :=
-{ finally' := fun α β x h => ExceptT.mk do
-    r ← finally' x (fun e? => match e? with
+{ tryFinally' := fun α β x h => ExceptT.mk do
+    r ← tryFinally' x (fun e? => match e? with
         | some (Except.ok a) => h (some a)
         | _                  => h none);
     match r with
diff --git a/src/Init/Control/Reader.lean b/src/Init/Control/Reader.lean
index c033ab6442..4306ad1011 100644
--- a/src/Init/Control/Reader.lean
+++ b/src/Init/Control/Reader.lean
@@ -118,8 +118,8 @@ instance ReaderT.monadControl (ρ : Type u) (m : Type u → Type v) : MonadContr
   restoreM := fun α x ctx => x,
 }
 
-instance ReaderT.finally {m : Type u → Type v} {ρ : Type u} [MonadFinally m] [Monad m] : MonadFinally (ReaderT ρ m) :=
-{ finally' := fun α β x h ctx => finally' (x ctx) (fun a? => h a? ctx) }
+instance ReaderT.tryFinally {m : Type u → Type v} {ρ : Type u} [MonadFinally m] [Monad m] : MonadFinally (ReaderT ρ m) :=
+{ tryFinally' := fun α β x h ctx => tryFinally' (x ctx) (fun a? => h a? ctx) }
 
 class MonadWithReaderOf (ρ : Type u) (m : Type u → Type v) :=
 (withReader {α : Type u} : (ρ → ρ) → m α → m α)
diff --git a/src/Init/Control/State.lean b/src/Init/Control/State.lean
index d804bef33a..7b9c4a7989 100644
--- a/src/Init/Control/State.lean
+++ b/src/Init/Control/State.lean
@@ -154,9 +154,9 @@ instance StateT.monadControl (σ : Type u) (m : Type u → Type v) [Monad m] : M
   restoreM := fun α x => do (a, s) ← liftM x; set s; pure a
 }
 
-instance StateT.finally {m : Type u → Type v} {σ : Type u} [MonadFinally m] [Monad m] : MonadFinally (StateT σ m) :=
-{ finally' := fun α β x h s => do
-  ((a, _), (b, s'')) ← finally' (x s)
+instance StateT.tryFinally {m : Type u → Type v} {σ : Type u} [MonadFinally m] [Monad m] : MonadFinally (StateT σ m) :=
+{ tryFinally' := fun α β x h s => do
+  ((a, _), (b, s'')) ← tryFinally' (x s)
     (fun p? => match p? with
       | some (a, s') => h (some a) s'
       | none         => h none s);
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 28364796c3..cac636e53c 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -1400,7 +1400,7 @@ def doTryToCode (doSeqToCode : List Syntax → M CodeBlock) (doTry : Syntax) (do
       if hasBreakContinueReturn finallyCode.code then
         throwError "'finally' currently does 'return', 'break', nor 'continue'"
       let finallyTerm ← liftMacroM $ ToTerm.run finallyCode.code ctx.m {} ToTerm.Kind.regular
-      `(«finally» $term $finallyTerm)
+      `(tryFinally $term $finallyTerm)
   let doElemsNew ← liftMacroM $ ToTerm.matchNestedTermResult ref term uvars a r bc
   doSeqToCode (doElemsNew ++ doElems)