fix: Bindings in prograde tactics #90
|
@ -247,7 +247,7 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat):
|
|||
-- See Lean.Elab.Tactic.Conv.convTarget
|
||||
let convMVar ← Elab.Tactic.withMainContext do
|
||||
let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget)
|
||||
Elab.Tactic.setGoals [newGoal.mvarId!]
|
||||
Elab.Tactic.replaceMainGoal [newGoal.mvarId!]
|
||||
pure rhs.mvarId!
|
||||
return (← MonadBacktrack.saveState, convMVar)
|
||||
try
|
||||
|
|
|
@ -25,7 +25,7 @@ def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
|
|||
(tagSuffix := .anonymous )
|
||||
(allowNaturalHoles := true)
|
||||
goal.assign expr
|
||||
Elab.Tactic.setGoals nextGoals
|
||||
Elab.Tactic.replaceMainGoal nextGoals
|
||||
|
||||
|
||||
end Pantograph.Tactic
|
||||
|
|
|
@ -31,7 +31,7 @@ def congruenceArg (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
|
|||
def evalCongruenceArg: Elab.Tactic.TacticM Unit := do
|
||||
let goal ← Elab.Tactic.getMainGoal
|
||||
let nextGoals ← congruenceArg goal
|
||||
Elab.Tactic.setGoals nextGoals
|
||||
Elab.Tactic.replaceMainGoal nextGoals
|
||||
|
||||
def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.congruenceFun
|
||||
|
@ -60,7 +60,7 @@ def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
|
|||
def evalCongruenceFun: Elab.Tactic.TacticM Unit := do
|
||||
let goal ← Elab.Tactic.getMainGoal
|
||||
let nextGoals ← congruenceFun goal
|
||||
Elab.Tactic.setGoals nextGoals
|
||||
Elab.Tactic.replaceMainGoal nextGoals
|
||||
|
||||
def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.congruence
|
||||
|
@ -93,6 +93,6 @@ def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
|
|||
def evalCongruence: Elab.Tactic.TacticM Unit := do
|
||||
let goal ← Elab.Tactic.getMainGoal
|
||||
let nextGoals ← congruence goal
|
||||
Elab.Tactic.setGoals nextGoals
|
||||
Elab.Tactic.replaceMainGoal nextGoals
|
||||
|
||||
end Pantograph.Tactic
|
||||
|
|
|
@ -100,6 +100,6 @@ def motivatedApply (mvarId: MVarId) (recursor: Expr) : MetaM (Array Meta.Inducti
|
|||
def evalMotivatedApply : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
|
||||
let recursor ← Elab.Term.elabTerm (stx := stx) .none
|
||||
let nextGoals ← motivatedApply (← Elab.Tactic.getMainGoal) recursor
|
||||
Elab.Tactic.setGoals $ nextGoals.toList.map (·.mvarId)
|
||||
Elab.Tactic.replaceMainGoal $ nextGoals.toList.map (·.mvarId)
|
||||
|
||||
end Pantograph.Tactic
|
||||
|
|
|
@ -17,6 +17,6 @@ def evalNoConfuse: Elab.Tactic.Tactic := λ stx => do
|
|||
let goal ← Elab.Tactic.getMainGoal
|
||||
let h ← goal.withContext $ Elab.Term.elabTerm (stx := stx) .none
|
||||
noConfuse goal h
|
||||
Elab.Tactic.setGoals []
|
||||
Elab.Tactic.replaceMainGoal []
|
||||
|
||||
end Pantograph.Tactic
|
||||
|
|
|
@ -5,22 +5,25 @@ open Lean
|
|||
|
||||
namespace Pantograph.Tactic
|
||||
|
||||
private def mkUpstreamMVar (goal: MVarId) : MetaM Expr := do
|
||||
Meta.mkFreshExprSyntheticOpaqueMVar (← goal.getType) (tag := ← goal.getTag)
|
||||
|
||||
|
||||
/-- Introduces a fvar to the current mvar -/
|
||||
def define (mvarId: MVarId) (binderName: Name) (expr: Expr): MetaM (FVarId × MVarId) := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.define
|
||||
let type ← Meta.inferType expr
|
||||
|
||||
Meta.withLetDecl binderName type expr λ fvar => do
|
||||
let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
|
||||
(← mvarId.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
|
||||
mvarId.assign mvarUpstream
|
||||
let mvarUpstream ← mkUpstreamMVar mvarId
|
||||
mvarId.assign $ ← Meta.mkLetFVars #[fvar] mvarUpstream
|
||||
pure (fvar.fvarId!, mvarUpstream.mvarId!)
|
||||
|
||||
def evalDefine (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do
|
||||
let goal ← Elab.Tactic.getMainGoal
|
||||
let expr ← goal.withContext $ Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
|
||||
let (_, mvarId) ← define goal binderName expr
|
||||
Elab.Tactic.setGoals [mvarId]
|
||||
Elab.Tactic.replaceMainGoal [mvarId]
|
||||
|
||||
structure BranchResult where
|
||||
fvarId?: Option FVarId := .none
|
||||
|
@ -39,10 +42,9 @@ def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResul
|
|||
let mvarUpstream ←
|
||||
withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
|
||||
Meta.withNewLocalInstances #[.fvar fvarId] 0 do
|
||||
let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
|
||||
(← mvarId.getType) (kind := MetavarKind.synthetic) (userName := ← mvarId.getTag)
|
||||
let mvarUpstream ← mkUpstreamMVar mvarId
|
||||
--let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
|
||||
mvarId.assign mvarUpstream
|
||||
mvarId.assign $ ← Meta.mkLambdaFVars #[.fvar fvarId] mvarUpstream
|
||||
pure mvarUpstream
|
||||
|
||||
return {
|
||||
|
@ -57,7 +59,7 @@ def evalHave (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
|
|||
let type ← Elab.Term.elabType (stx := type)
|
||||
let result ← «have» goal binderName type
|
||||
pure [result.branch, result.main]
|
||||
Elab.Tactic.setGoals nextGoals
|
||||
Elab.Tactic.replaceMainGoal nextGoals
|
||||
|
||||
def «let» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult := mvarId.withContext do
|
||||
mvarId.checkNotAssigned `Pantograph.Tactic.let
|
||||
|
@ -68,9 +70,8 @@ def «let» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult
|
|||
|
||||
assert! ¬ type.hasLooseBVars
|
||||
let mvarUpstream ← Meta.withLetDecl binderName type mvarBranch $ λ fvar => do
|
||||
let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
|
||||
(type := ← mvarId.getType) (kind := MetavarKind.synthetic) (userName := ← mvarId.getTag)
|
||||
mvarId.assign $ .letE binderName type fvar mvarUpstream (nonDep := false)
|
||||
let mvarUpstream ← mkUpstreamMVar mvarId
|
||||
mvarId.assign $ ← Meta.mkLetFVars #[fvar] mvarUpstream
|
||||
pure mvarUpstream
|
||||
|
||||
return {
|
||||
|
@ -82,6 +83,6 @@ def evalLet (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
|
|||
let goal ← Elab.Tactic.getMainGoal
|
||||
let type ← goal.withContext $ Elab.Term.elabType (stx := type)
|
||||
let result ← «let» goal binderName type
|
||||
Elab.Tactic.setGoals [result.branch, result.main]
|
||||
Elab.Tactic.replaceMainGoal [result.branch, result.main]
|
||||
|
||||
end Pantograph.Tactic
|
||||
|
|
|
@ -94,15 +94,22 @@ def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq)
|
|||
|
||||
def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e
|
||||
|
||||
def strToTermSyntax [Monad m] [MonadEnv m] (s: String): m Syntax := do
|
||||
let .ok stx := Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
(input := s)
|
||||
(fileName := filename) | panic! s!"Failed to parse {s}"
|
||||
return stx
|
||||
def parseSentence (s: String): Elab.TermElabM Expr := do
|
||||
let recursor ← match Parser.runParserCategory
|
||||
let stx ← match Parser.runParserCategory
|
||||
(env := ← MonadEnv.getEnv)
|
||||
(catName := `term)
|
||||
(input := s)
|
||||
(fileName := filename) with
|
||||
| .ok syn => pure syn
|
||||
| .error error => throwError "Failed to parse: {error}"
|
||||
Elab.Term.elabTerm (stx := recursor) .none
|
||||
Elab.Term.elabTerm (stx := stx) .none
|
||||
|
||||
def runTacticOnMVar (tacticM: Elab.Tactic.TacticM Unit) (goal: MVarId): Elab.TermElabM (List MVarId) := do
|
||||
let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
|
||||
|
|
|
@ -7,7 +7,7 @@ open Pantograph
|
|||
|
||||
namespace Pantograph.Test.Tactic.Prograde
|
||||
|
||||
def test_eval : TestT Elab.TermElabM Unit := do
|
||||
def test_define : TestT Elab.TermElabM Unit := do
|
||||
let expr := "forall (p q : Prop) (h: p), And (Or p q) (Or p q)"
|
||||
let expr ← parseSentence expr
|
||||
Meta.forallTelescope expr $ λ _ body => do
|
||||
|
@ -48,9 +48,10 @@ def test_eval : TestT Elab.TermElabM Unit := do
|
|||
],
|
||||
target,
|
||||
})
|
||||
addTest $ LSpec.test "assign" ((← getExprMVarAssignment? goal.mvarId!) == .some (.mvar newGoal))
|
||||
let .some e ← getExprMVarAssignment? goal.mvarId! | panic! "Tactic must assign"
|
||||
addTest $ LSpec.test "assign" e.isLet
|
||||
|
||||
def test_proof_eval : TestT Elab.TermElabM Unit := do
|
||||
def test_define_proof : TestT Elab.TermElabM Unit := do
|
||||
let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
|
||||
let state0 ← GoalState.create rootExpr
|
||||
let tactic := "intro p q h"
|
||||
|
@ -103,7 +104,38 @@ def test_proof_eval : TestT Elab.TermElabM Unit := do
|
|||
|
||||
addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome
|
||||
|
||||
def test_proof_have : TestT Elab.TermElabM Unit := do
|
||||
def fun_define_root_expr: ∀ (p: Prop), PProd (Nat → p) Unit → p := by
|
||||
intro p x
|
||||
apply x.fst
|
||||
exact 5
|
||||
|
||||
def test_define_root_expr : TestT Elab.TermElabM Unit := do
|
||||
--let rootExpr ← parseSentence "Nat"
|
||||
--let state0 ← GoalState.create rootExpr
|
||||
--let .success state1 ← state0.tryTactic (goalId := 0) "exact 5" | addTest $ assertUnreachable "exact 5"
|
||||
--let .some rootExpr := state1.rootExpr? | addTest $ assertUnreachable "Root expr"
|
||||
--addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "5")
|
||||
let rootExpr ← parseSentence "∀ (p: Prop), PProd (Nat → p) Unit → p"
|
||||
let state0 ← GoalState.create rootExpr
|
||||
let tactic := "intro p x"
|
||||
let .success state1 ← state0.tryTactic (goalId := 0) tactic | addTest $ assertUnreachable tactic
|
||||
let binderName := `binder
|
||||
let value := "x.fst"
|
||||
let expr ← state1.goals[0]!.withContext $ strToTermSyntax value
|
||||
let tacticM := Tactic.evalDefine binderName expr
|
||||
let .success state2 ← state1.tryTacticM (goalId := 0) tacticM | addTest $ assertUnreachable s!"define {binderName} := {value}"
|
||||
let tactic := s!"apply {binderName}"
|
||||
let .success state3 ← state2.tryTactic (goalId := 0) tactic | addTest $ assertUnreachable tactic
|
||||
let tactic := s!"exact 5"
|
||||
let .success state4 ← state3.tryTactic (goalId := 0) tactic | addTest $ assertUnreachable tactic
|
||||
let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
|
||||
addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p x =>\n let binder := x.fst;\n binder 5")
|
||||
|
||||
--set_option pp.all true
|
||||
--#check @PSigma (α := Prop) (β := λ (p: Prop) => p)
|
||||
--def test_define_root_expr : TestT Elab.TermElabM Unit := do
|
||||
|
||||
def test_have_proof : TestT Elab.TermElabM Unit := do
|
||||
let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
|
||||
let state0 ← GoalState.create rootExpr
|
||||
let tactic := "intro p q h"
|
||||
|
@ -160,7 +192,8 @@ def test_proof_have : TestT Elab.TermElabM Unit := do
|
|||
addTest $ LSpec.check s!":= {expr}" ((← state4.serializeGoals).map (·.devolatilize) =
|
||||
#[])
|
||||
|
||||
addTest $ LSpec.check "(4 root)" state4.rootExpr?.isSome
|
||||
let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
|
||||
addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p q h y => Or.inl y")
|
||||
|
||||
def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
|
||||
let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
|
||||
|
@ -256,9 +289,10 @@ def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
|
|||
|
||||
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
|
||||
[
|
||||
("eval", test_eval),
|
||||
("Proof eval", test_proof_eval),
|
||||
("Proof have", test_proof_have),
|
||||
("define", test_define),
|
||||
("define proof", test_define_proof),
|
||||
("define root expr", test_define_root_expr),
|
||||
("have proof", test_have_proof),
|
||||
("let via assign", test_let false),
|
||||
("let via tryLet", test_let true),
|
||||
] |>.map (λ (name, t) => (name, runTestTermElabM env t))
|
||||
|
|
Loading…
Reference in New Issue