/-
Copyright (c) 2022 Jannis Limperg. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jannis Limperg
-/

import Lean.Util.MonadBacktrack

namespace Lean

/--
Execute the action `x`, then restore the initial state. Returns the state after
`x` finished.
-/
def withoutModifyingState': {m : Type → Type} →
  {s α : Type} → [inst : Monad m] → [inst : MonadBacktrack s m] → [inst : MonadFinally m] → m α → m (α × s)
withoutModifyingState' [Monad: (Type ?u.38 → Type ?u.37) → Type (max(?u.38+1)?u.37)
Monad m: ?m.5
m] [MonadBacktrack: outParam Type → (Type → Type) → Type
MonadBacktrack s: ?m.14
s m: ?m.5
m] [MonadFinally: (Type ?u.27 → Type ?u.26) → Type (max(?u.27+1)?u.26)
MonadFinally m: ?m.5
m]
    (x: m α
x : m: ?m.5
m α: ?m.34
α) : m: ?m.5
m (α: ?m.34
α × s: ?m.14
s) :=
  withoutModifyingState: {m : Type → Type} → {s α : Type} → [inst : Monad m] → [inst : MonadFinally m] → [inst : MonadBacktrack s m] → m α → m α
withoutModifyingState do
    let result: ?m.160
result ← x: m α
x
    let finalState: ?m.209
finalState ← saveState: {s : outParam Type} → {m : Type → Type} → [self : MonadBacktrack s m] → m s
saveState
    return (result: ?m.160
result, finalState: ?m.209
finalState)

end Lean