max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: finally shouldn't call finalizer when finalizer throws

Browse source
This commit is contained in:
Sebastian Ullrich 2020-07-09 16:58:38 +02:00 • committed by Leonardo de Moura
parent c38f4fe837
commit 719819bf49
1 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/Init/Control/Except.lean
View file

@ -181,7 +181,8 @@ instance (ε m out) [MonadRun out m] : MonadRun (fun α => out (Except ε α)) (
⟨fun α => run⟩
/-- Execute `x` and then execute `finalizer` even if `x` threw an exception -/
@[inline] def finally {ε α : Type u} {m : Type u → Type v} [Monad m] [MonadExcept ε m] (x : m α) (finalizer : m PUnit) : m α :=
catch
(do a ← x; finalizer; pure a)
(fun e => do finalizer; throw e)
@[inline] def finally {ε α : Type u} {m : Type u → Type v} [Monad m] [MonadExcept ε m] (x : m α) (finalizer : m PUnit) : m α := do
r ← catch (Except.ok <$> x) (fun ex => @pure m _ _ $ Except.error ex);
match r with
| Except.ok a => finalizer *> pure a
| Except.error e => finalizer *> throw e