-
Notifications
You must be signed in to change notification settings - Fork 25
/
Check.lean
44 lines (37 loc) · 1.25 KB
/
Check.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
/-
Copyright (c) 2024 Jannis Limperg. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jannis Limperg
-/
import Aesop.Check
import Aesop.Script.UScript
open Lean Lean.Elab.Tactic
open Lean.Parser.Tactic (tacticSeq)
namespace Aesop.Script
def UScript.checkIfEnabled (uscript : UScript) : MetaM Unit := do
unless ← Check.script.steps.isEnabled do
return
try
uscript.validate
catch e =>
throwError "{Check.script.steps.name}: {e.toMessageData}"
end Script
def checkRenderedScriptIfEnabled (script : TSyntax ``tacticSeq)
(preState : Meta.SavedState) (goal : MVarId) (expectCompleteProof : Bool) :
MetaM Unit := do
if ! (← Check.script.isEnabled) then
return
let go : TacticM Unit := do
setGoals [goal]
evalTactic script
if expectCompleteProof && ! (← getUnsolvedGoals).isEmpty then
throwError "script executed successfully but did not solve the main goal"
try
show MetaM Unit from withoutModifyingState do
preState.restore
go.run { elaborator := .anonymous, recover := false }
|>.run' { goals := [goal] }
|>.run'
catch e => throwError
"{Check.script.name}: error while executing generated script:{indentD e.toMessageData}"
end Aesop