-
Notifications
You must be signed in to change notification settings - Fork 87
/
SavedState.lean
50 lines (41 loc) · 1.55 KB
/
SavedState.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
/-
Copyright (c) 2022 Jannis Limperg. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jannis Limperg
-/
import Batteries.Lean.Meta.Basic
import Batteries.Lean.MonadBacktrack
namespace Lean.Meta.SavedState
/--
Run the action `x` in state `s`. Returns the result of `x` and the state after
`x` was executed. The global state remains unchanged.
-/
def runMetaM (s : Meta.SavedState) (x : MetaM α) :
MetaM (α × Meta.SavedState) :=
withoutModifyingState' do restoreState s; x
/--
Run the action `x` in state `s`. Returns the result of `x`. The global state
remains unchanged.
-/
def runMetaM' (s : Meta.SavedState) (x : MetaM α) : MetaM α :=
withoutModifyingState do restoreState s; x
end SavedState
/--
Returns the mvars that are not declared in `preState`, but declared and
unassigned in `postState`. Delayed-assigned mvars are considered assigned.
-/
def getIntroducedExprMVars (preState postState : SavedState) :
MetaM (Array MVarId) := do
let unassignedPost ← postState.runMetaM' getUnassignedExprMVars
preState.runMetaM' do
unassignedPost.filterM fun mvarId => return ! (← mvarId.isDeclared)
/--
Returns the mvars that are declared but unassigned in `preState`, and
assigned in `postState`. Delayed-assigned mvars are considered assigned.
-/
def getAssignedExprMVars (preState postState : SavedState) :
MetaM (Array MVarId) := do
let unassignedPre ← preState.runMetaM' getUnassignedExprMVars
postState.runMetaM' do
unassignedPre.filterM (·.isAssignedOrDelayedAssigned)
end Lean.Meta