-
Notifications
You must be signed in to change notification settings - Fork 331
/
BuiltinTactic.lean
276 lines (239 loc) · 9.93 KB
/
BuiltinTactic.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
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Elab.Tactic.Basic
import Lean.Elab.Tactic.ElabTerm
namespace Lean.Elab.Tactic
open Meta
@[builtinTactic Lean.Parser.Tactic.«done»] def evalDone : Tactic := fun _ =>
done
@[builtinTactic seq1] def evalSeq1 : Tactic := fun stx => do
let args := stx[0].getArgs
for i in [:args.size] do
if i % 2 == 0 then
evalTactic args[i]
else
saveTacticInfoForToken args[i] -- add `TacticInfo` node for `;`
@[builtinTactic paren] def evalParen : Tactic := fun stx =>
evalTactic stx[1]
/- Evaluate `many (group (tactic >> optional ";")) -/
def evalManyTacticOptSemi (stx : Syntax) : TacticM Unit := do
stx.forArgsM fun seqElem => do
evalTactic seqElem[0]
saveTacticInfoForToken seqElem[1] -- add TacticInfo node for `;`
@[builtinTactic tacticSeq1Indented] def evalTacticSeq1Indented : Tactic := fun stx =>
evalManyTacticOptSemi stx[0]
@[builtinTactic tacticSeqBracketed] def evalTacticSeqBracketed : Tactic := fun stx => do
let initInfo ← mkInitialTacticInfo stx[0]
withRef stx[2] <| closeUsingOrAdmit do
-- save state before/after entering focus on `{`
withInfoContext (pure ()) initInfo
evalManyTacticOptSemi stx[1]
@[builtinTactic Parser.Tactic.focus] def evalFocus : Tactic := fun stx => do
let mkInfo ← mkInitialTacticInfo stx[0]
focus do
-- show focused state on `focus`
withInfoContext (pure ()) mkInfo
evalTactic stx[1]
private def getOptRotation (stx : Syntax) : Nat :=
if stx.isNone then 1 else stx[0].toNat
@[builtinTactic Parser.Tactic.rotateLeft] def evalRotateLeft : Tactic := fun stx => do
let n := getOptRotation stx[1]
setGoals <| (← getGoals).rotateLeft n
@[builtinTactic Parser.Tactic.rotateRight] def evalRotateRight : Tactic := fun stx => do
let n := getOptRotation stx[1]
setGoals <| (← getGoals).rotateRight n
@[builtinTactic Parser.Tactic.open] def evalOpen : Tactic := fun stx => do
try
pushScope
let openDecls ← elabOpenDecl stx[1]
withTheReader Core.Context (fun ctx => { ctx with openDecls := openDecls }) do
evalTactic stx[3]
finally
popScope
@[builtinTactic Parser.Tactic.set_option] def elabSetOption : Tactic := fun stx => do
let options ← Elab.elabSetOption stx[1] stx[2]
withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
evalTactic stx[4]
@[builtinTactic Parser.Tactic.allGoals] def evalAllGoals : Tactic := fun stx => do
let mvarIds ← getGoals
let mut mvarIdsNew := #[]
for mvarId in mvarIds do
unless (← isExprMVarAssigned mvarId) do
setGoals [mvarId]
try
evalTactic stx[1]
mvarIdsNew := mvarIdsNew ++ (← getUnsolvedGoals)
catch ex =>
logException ex
mvarIdsNew := mvarIdsNew.push mvarId
setGoals mvarIdsNew.toList
@[builtinTactic Parser.Tactic.anyGoals] def evalAnyGoals : Tactic := fun stx => do
let mvarIds ← getGoals
let mut mvarIdsNew := #[]
let mut succeeded := false
for mvarId in mvarIds do
unless (← isExprMVarAssigned mvarId) do
setGoals [mvarId]
try
evalTactic stx[1]
mvarIdsNew := mvarIdsNew ++ (← getUnsolvedGoals)
succeeded := true
catch _ =>
mvarIdsNew := mvarIdsNew.push mvarId
unless succeeded do
throwError "failed on all goals"
setGoals mvarIdsNew.toList
@[builtinTactic tacticSeq] def evalTacticSeq : Tactic := fun stx =>
evalTactic stx[0]
partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
if h : i < tactics.size then
let tactic := tactics.get ⟨i, h⟩
catchInternalId unsupportedSyntaxExceptionId
(evalTactic tactic)
(fun _ => evalChoiceAux tactics (i+1))
else
throwUnsupportedSyntax
@[builtinTactic choice] def evalChoice : Tactic := fun stx =>
evalChoiceAux stx.getArgs 0
@[builtinTactic skip] def evalSkip : Tactic := fun stx => pure ()
@[builtinTactic unknown] def evalUnknown : Tactic := fun stx => do
addCompletionInfo <| CompletionInfo.tactic stx (← getGoals)
@[builtinTactic failIfSuccess] def evalFailIfSuccess : Tactic := fun stx => do
let tactic := stx[1]
if (← try evalTactic tactic; pure true catch _ => pure false) then
throwError "tactic succeeded"
@[builtinTactic traceState] def evalTraceState : Tactic := fun stx => do
let gs ← getUnsolvedGoals
logInfo (goalsToMessageData gs)
@[builtinTactic Lean.Parser.Tactic.assumption] def evalAssumption : Tactic := fun stx =>
liftMetaTactic fun mvarId => do Meta.assumption mvarId; pure []
@[builtinTactic Lean.Parser.Tactic.contradiction] def evalContradiction : Tactic := fun stx =>
liftMetaTactic fun mvarId => do Meta.contradiction mvarId; pure []
@[builtinTactic Lean.Parser.Tactic.intro] def evalIntro : Tactic := fun stx => do
match stx with
| `(tactic| intro) => introStep `_
| `(tactic| intro $h:ident) => introStep h.getId
| `(tactic| intro _) => introStep `_
| `(tactic| intro $pat:term) => evalTactic (← `(tactic| intro h; match h with | $pat:term => ?_; try clear h))
| `(tactic| intro $h:term $hs:term*) => evalTactic (← `(tactic| intro $h:term; intro $hs:term*))
| _ => throwUnsupportedSyntax
where
introStep (n : Name) : TacticM Unit :=
liftMetaTactic fun mvarId => do
let (_, mvarId) ← Meta.intro mvarId n
pure [mvarId]
@[builtinTactic Lean.Parser.Tactic.introMatch] def evalIntroMatch : Tactic := fun stx => do
let matchAlts := stx[1]
let stxNew ← liftMacroM <| Term.expandMatchAltsIntoMatchTactic stx matchAlts
withMacroExpansion stx stxNew <| evalTactic stxNew
@[builtinTactic «intros»] def evalIntros : Tactic := fun stx =>
match stx with
| `(tactic| intros) => liftMetaTactic fun mvarId => do
let (_, mvarId) ← Meta.intros mvarId
return [mvarId]
| `(tactic| intros $ids*) => liftMetaTactic fun mvarId => do
let (_, mvarId) ← Meta.introN mvarId ids.size (ids.map getNameOfIdent').toList
return [mvarId]
| _ => throwUnsupportedSyntax
@[builtinTactic Lean.Parser.Tactic.revert] def evalRevert : Tactic := fun stx =>
match stx with
| `(tactic| revert $hs*) => do
let (_, mvarId) ← Meta.revert (← getMainGoal) (← getFVarIds hs)
replaceMainGoal [mvarId]
| _ => throwUnsupportedSyntax
@[builtinTactic Lean.Parser.Tactic.clear] def evalClear : Tactic := fun stx =>
match stx with
| `(tactic| clear $hs*) => do
let fvarIds ← getFVarIds hs
let fvarIds ← withMainContext <| sortFVarIds fvarIds
for fvarId in fvarIds.reverse do
withMainContext do
let mvarId ← clear (← getMainGoal) fvarId
replaceMainGoal [mvarId]
| _ => throwUnsupportedSyntax
def forEachVar (hs : Array Syntax) (tac : MVarId → FVarId → MetaM MVarId) : TacticM Unit := do
for h in hs do
withMainContext do
let fvarId ← getFVarId h
let mvarId ← tac (← getMainGoal) fvarId
replaceMainGoal [mvarId]
@[builtinTactic Lean.Parser.Tactic.subst] def evalSubst : Tactic := fun stx =>
match stx with
| `(tactic| subst $hs*) => forEachVar hs Meta.subst
| _ => throwUnsupportedSyntax
/--
First method searches for a metavariable `g` s.t. `tag` is a suffix of its name.
If none is found, then it searches for a metavariable `g` s.t. `tag` is a prefix of its name. -/
private def findTag? (mvarIds : List MVarId) (tag : Name) : TacticM (Option MVarId) := do
let mvarId? ← mvarIds.findM? fun mvarId => return tag.isSuffixOf (← getMVarDecl mvarId).userName
match mvarId? with
| some mvarId => return mvarId
| none => mvarIds.findM? fun mvarId => return tag.isPrefixOf (← getMVarDecl mvarId).userName
def renameInaccessibles (mvarId : MVarId) (hs : Array Syntax) : TacticM MVarId := do
if hs.isEmpty then
return mvarId
else
let mvarDecl ← getMVarDecl mvarId
let mut lctx := mvarDecl.lctx
let mut hs := hs
let mut found : NameSet := {}
let n := lctx.numIndices
for i in [:n] do
let j := n - i - 1
match lctx.getAt? j with
| none => pure ()
| some localDecl =>
if localDecl.userName.hasMacroScopes || found.contains localDecl.userName then
let h := hs.back
if h.isIdent then
let newName := h.getId
lctx := lctx.setUserName localDecl.fvarId newName
hs := hs.pop
if hs.isEmpty then
break
found := found.insert localDecl.userName
unless hs.isEmpty do
logError m!"too many variable names provided"
let mvarNew ← mkFreshExprMVarAt lctx mvarDecl.localInstances mvarDecl.type MetavarKind.syntheticOpaque mvarDecl.userName
assignExprMVar mvarId mvarNew
return mvarNew.mvarId!
@[builtinTactic «case»] def evalCase : Tactic
| stx@`(tactic| case $tag $hs* =>%$arr $tac:tacticSeq) => do
let gs ← getUnsolvedGoals
let g ←
if tag.isIdent then
let tag := tag.getId
let some g ← findTag? gs tag | throwError "tag not found"
pure g
else
getMainGoal
let gs := gs.erase g
let g ← renameInaccessibles g hs
setGoals [g]
let savedTag ← getMVarTag g
setMVarTag g Name.anonymous
try
withCaseRef arr tac do
closeUsingOrAdmit (withTacticInfoContext stx (evalTactic tac))
finally
setMVarTag g savedTag
done
setGoals gs
| _ => throwUnsupportedSyntax
@[builtinTactic «renameI»] def evalRenameInaccessibles : Tactic
| stx@`(tactic| rename_i $hs*) => do replaceMainGoal [← renameInaccessibles (← getMainGoal) hs]
| _ => throwUnsupportedSyntax
@[builtinTactic «first»] partial def evalFirst : Tactic := fun stx => do
let tacs := stx[1].getArgs
if tacs.isEmpty then throwUnsupportedSyntax
loop tacs 0
where
loop (tacs : Array Syntax) (i : Nat) :=
if i == tacs.size - 1 then
evalTactic tacs[i][1]
else
evalTactic tacs[i][1] <|> loop tacs (i+1)
end Lean.Elab.Tactic