-
Notifications
You must be signed in to change notification settings - Fork 24
/
TacticState.lean
103 lines (85 loc) · 3.44 KB
/
TacticState.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
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
/-
Copyright (c) 2022--2024 Jannis Limperg. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jannis Limperg
-/
import Aesop.Script.GoalWithMVars
import Aesop.Util.Basic
open Lean
namespace Aesop.Script
variable [Monad m] [MonadError m]
structure TacticState where
visibleGoals : Array GoalWithMVars
invisibleGoals : HashSet MVarId
deriving Inhabited
namespace TacticState
private def throwUnknownGoalError (goal : MVarId) (pre : MessageData) : m α :=
throwError "internal error: {pre}: unknown goal '?{goal.name}'"
def getVisibleGoalIndex? (ts : TacticState) (goal : MVarId) : Option Nat :=
ts.visibleGoals.findIdx? (·.goal == goal)
def getVisibleGoalIndex (ts : TacticState) (goal : MVarId) : m Nat := do
if let (some idx) := ts.getVisibleGoalIndex? goal then
return idx
else
throwUnknownGoalError goal "getVisibleGoalIndex"
def getMainGoal? (ts : TacticState) : Option MVarId :=
ts.visibleGoals[0]?.map (·.goal)
def visibleGoalsHaveMVars (ts : TacticState) : Bool :=
ts.visibleGoals.any λ g => ! g.mvars.isEmpty
def solveVisibleGoals (ts : TacticState) : TacticState :=
{ ts with visibleGoals := #[] }
private def replaceWithArray [BEq α] (xs : Array α) (x : α) (r : Array α) :
Option (Array α) := Id.run do
let mut found := false
let mut ys := Array.mkEmpty (xs.size - 1 + r.size)
for x' in xs do
if x' == x then
ys := ys ++ r
found := true
else
ys := ys.push x'
return if found then some ys else none
def eraseSolvedGoals (ts : TacticState) (preMCtx postMCtx : MetavarContext) :
TacticState := {
ts with
visibleGoals := ts.visibleGoals.filter (! mvarWasSolved ·.goal)
invisibleGoals := HashSet.filter ts.invisibleGoals (! mvarWasSolved ·)
}
where
mvarWasSolved (mvarId : MVarId) : Bool :=
postMCtx.isExprMVarAssignedOrDelayedAssigned mvarId &&
! preMCtx.isExprMVarAssignedOrDelayedAssigned mvarId
def applyTactic (ts : TacticState) (inGoal : MVarId)
(outGoals : Array GoalWithMVars) (preMCtx postMCtx : MetavarContext) :
m TacticState := do
let (some visibleGoals) :=
replaceWithArray ts.visibleGoals ⟨inGoal, {}⟩ outGoals
| throwUnknownGoalError inGoal "applyTactic"
let ts := { ts with visibleGoals }
return eraseSolvedGoals ts preMCtx postMCtx
-- Focus the visible goal `goal` and move all other previously visible goals
-- to `invisibleGoals`.
def focus (ts : TacticState) (goal : MVarId) : m TacticState := do
let (some goalWithMVars) := ts.visibleGoals.find? (·.goal == goal)
| throwUnknownGoalError goal "focus"
let mut invisibleGoals := ts.invisibleGoals
for g in ts.visibleGoals do
if g.goal != goal then
invisibleGoals := invisibleGoals.insert g.goal
return { visibleGoals := #[goalWithMVars], invisibleGoals }
@[inline, always_inline]
def onGoalM (ts : TacticState) (g : MVarId)
(f : TacticState → m (α × TacticState)) : m (α × TacticState) := do
let (a, postTs) ← f (← ts.focus g)
let mut visibleGoals := #[]
for preGoal in ts.visibleGoals do
if preGoal.goal == g then
visibleGoals := visibleGoals ++ postTs.visibleGoals
else if postTs.invisibleGoals.contains preGoal.goal then
visibleGoals := visibleGoals.push preGoal
let mut invisibleGoals := ∅
for g in ts.invisibleGoals do
if postTs.invisibleGoals.contains g then
invisibleGoals := invisibleGoals.insert g
return (a, { visibleGoals, invisibleGoals })
end Aesop.Script.TacticState