34 lines
1.1 KiB
Plaintext
34 lines
1.1 KiB
Plaintext
|
import Lean.Meta
|
|||
|
|
import Lean.Elab
|
|||
|
|
import LSpec
|
|||
|
|
import Test.Common
|
|||
|
|
|
|||
|
|
open Lean
|
|||
|
|
|
|||
|
|
namespace Pantograph.Test.Tactic.Assign
|
|||
|
|
|
|||
|
|
def test_draft : TestT Elab.TermElabM Unit := do
|
|||
|
|
let expr := "forall (p : Prop), (p ∨ p) ∨ p"
|
|||
|
|
let skeleton := "by\nhave a : p ∨ p := sorry\nsorry"
|
|||
|
|
let expr ← parseSentence expr
|
|||
|
|
Meta.forallTelescope expr $ λ _ body => do
|
|||
|
|
let skeleton' ← match Parser.runParserCategory
|
|||
|
|
(env := ← MonadEnv.getEnv)
|
|||
|
|
(catName := `term)
|
|||
|
|
(input := skeleton)
|
|||
|
|
(fileName := ← getFileName) with
|
|||
|
|
| .ok syn => pure syn
|
|||
|
|
| .error error => throwError "Failed to parse: {error}"
|
|||
|
|
-- Apply the tactic
|
|||
|
|
let target ← Meta.mkFreshExprSyntheticOpaqueMVar body
|
|||
|
|
let tactic := Tactic.evalDraft skeleton'
|
|||
|
|
let newGoals ← runTacticOnMVar tactic target.mvarId!
|
|||
|
|
addTest $ LSpec.check "goals" ((← newGoals.mapM (λ g => do exprToStr (← g.getType))) = ["p ∨ p", "(p ∨ p) ∨ p"])
|
|||
|
|
|
|||
|
|
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
|
|||
|
|
[
|
|||
|
|
("draft", test_draft),
|
|||
|
|
] |>.map (λ (name, t) => (name, runTestTermElabM env t))
|
|||
|
|
|
|||
|
|
end Pantograph.Test.Tactic.Assign
|