fix: Bindings in prograde tactics #90
|
@ -247,7 +247,7 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat):
|
||||||
-- See Lean.Elab.Tactic.Conv.convTarget
|
-- See Lean.Elab.Tactic.Conv.convTarget
|
||||||
let convMVar ← Elab.Tactic.withMainContext do
|
let convMVar ← Elab.Tactic.withMainContext do
|
||||||
let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget)
|
let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget)
|
||||||
Elab.Tactic.setGoals [newGoal.mvarId!]
|
Elab.Tactic.replaceMainGoal [newGoal.mvarId!]
|
||||||
pure rhs.mvarId!
|
pure rhs.mvarId!
|
||||||
return (← MonadBacktrack.saveState, convMVar)
|
return (← MonadBacktrack.saveState, convMVar)
|
||||||
try
|
try
|
||||||
|
|
|
@ -25,7 +25,7 @@ def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
|
||||||
(tagSuffix := .anonymous )
|
(tagSuffix := .anonymous )
|
||||||
(allowNaturalHoles := true)
|
(allowNaturalHoles := true)
|
||||||
goal.assign expr
|
goal.assign expr
|
||||||
Elab.Tactic.setGoals nextGoals
|
Elab.Tactic.replaceMainGoal nextGoals
|
||||||
|
|
||||||
|
|
||||||
end Pantograph.Tactic
|
end Pantograph.Tactic
|
||||||
|
|
|
@ -31,7 +31,7 @@ def congruenceArg (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
|
||||||
def evalCongruenceArg: Elab.Tactic.TacticM Unit := do
|
def evalCongruenceArg: Elab.Tactic.TacticM Unit := do
|
||||||
let goal ← Elab.Tactic.getMainGoal
|
let goal ← Elab.Tactic.getMainGoal
|
||||||
let nextGoals ← congruenceArg goal
|
let nextGoals ← congruenceArg goal
|
||||||
Elab.Tactic.setGoals nextGoals
|
Elab.Tactic.replaceMainGoal nextGoals
|
||||||
|
|
||||||
def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
|
def congruenceFun (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
|
||||||
mvarId.checkNotAssigned `Pantograph.Tactic.congruenceFun
|
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
|
def evalCongruenceFun: Elab.Tactic.TacticM Unit := do
|
||||||
let goal ← Elab.Tactic.getMainGoal
|
let goal ← Elab.Tactic.getMainGoal
|
||||||
let nextGoals ← congruenceFun goal
|
let nextGoals ← congruenceFun goal
|
||||||
Elab.Tactic.setGoals nextGoals
|
Elab.Tactic.replaceMainGoal nextGoals
|
||||||
|
|
||||||
def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
|
def congruence (mvarId: MVarId): MetaM (List MVarId) := mvarId.withContext do
|
||||||
mvarId.checkNotAssigned `Pantograph.Tactic.congruence
|
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
|
def evalCongruence: Elab.Tactic.TacticM Unit := do
|
||||||
let goal ← Elab.Tactic.getMainGoal
|
let goal ← Elab.Tactic.getMainGoal
|
||||||
let nextGoals ← congruence goal
|
let nextGoals ← congruence goal
|
||||||
Elab.Tactic.setGoals nextGoals
|
Elab.Tactic.replaceMainGoal nextGoals
|
||||||
|
|
||||||
end Pantograph.Tactic
|
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
|
def evalMotivatedApply : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
|
||||||
let recursor ← Elab.Term.elabTerm (stx := stx) .none
|
let recursor ← Elab.Term.elabTerm (stx := stx) .none
|
||||||
let nextGoals ← motivatedApply (← Elab.Tactic.getMainGoal) recursor
|
let nextGoals ← motivatedApply (← Elab.Tactic.getMainGoal) recursor
|
||||||
Elab.Tactic.setGoals $ nextGoals.toList.map (·.mvarId)
|
Elab.Tactic.replaceMainGoal $ nextGoals.toList.map (·.mvarId)
|
||||||
|
|
||||||
end Pantograph.Tactic
|
end Pantograph.Tactic
|
||||||
|
|
|
@ -17,6 +17,6 @@ def evalNoConfuse: Elab.Tactic.Tactic := λ stx => do
|
||||||
let goal ← Elab.Tactic.getMainGoal
|
let goal ← Elab.Tactic.getMainGoal
|
||||||
let h ← goal.withContext $ Elab.Term.elabTerm (stx := stx) .none
|
let h ← goal.withContext $ Elab.Term.elabTerm (stx := stx) .none
|
||||||
noConfuse goal h
|
noConfuse goal h
|
||||||
Elab.Tactic.setGoals []
|
Elab.Tactic.replaceMainGoal []
|
||||||
|
|
||||||
end Pantograph.Tactic
|
end Pantograph.Tactic
|
||||||
|
|
|
@ -5,22 +5,25 @@ open Lean
|
||||||
|
|
||||||
namespace Pantograph.Tactic
|
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 -/
|
/-- Introduces a fvar to the current mvar -/
|
||||||
def define (mvarId: MVarId) (binderName: Name) (expr: Expr): MetaM (FVarId × MVarId) := mvarId.withContext do
|
def define (mvarId: MVarId) (binderName: Name) (expr: Expr): MetaM (FVarId × MVarId) := mvarId.withContext do
|
||||||
mvarId.checkNotAssigned `Pantograph.Tactic.define
|
mvarId.checkNotAssigned `Pantograph.Tactic.define
|
||||||
let type ← Meta.inferType expr
|
let type ← Meta.inferType expr
|
||||||
|
|
||||||
Meta.withLetDecl binderName type expr λ fvar => do
|
Meta.withLetDecl binderName type expr λ fvar => do
|
||||||
let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
|
let mvarUpstream ← mkUpstreamMVar mvarId
|
||||||
(← mvarId.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
|
mvarId.assign $ ← Meta.mkLetFVars #[fvar] mvarUpstream
|
||||||
mvarId.assign mvarUpstream
|
|
||||||
pure (fvar.fvarId!, mvarUpstream.mvarId!)
|
pure (fvar.fvarId!, mvarUpstream.mvarId!)
|
||||||
|
|
||||||
def evalDefine (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do
|
def evalDefine (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do
|
||||||
let goal ← Elab.Tactic.getMainGoal
|
let goal ← Elab.Tactic.getMainGoal
|
||||||
let expr ← goal.withContext $ Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
|
let expr ← goal.withContext $ Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
|
||||||
let (_, mvarId) ← define goal binderName expr
|
let (_, mvarId) ← define goal binderName expr
|
||||||
Elab.Tactic.setGoals [mvarId]
|
Elab.Tactic.replaceMainGoal [mvarId]
|
||||||
|
|
||||||
structure BranchResult where
|
structure BranchResult where
|
||||||
fvarId?: Option FVarId := .none
|
fvarId?: Option FVarId := .none
|
||||||
|
@ -39,10 +42,9 @@ def «have» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResul
|
||||||
let mvarUpstream ←
|
let mvarUpstream ←
|
||||||
withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
|
withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
|
||||||
Meta.withNewLocalInstances #[.fvar fvarId] 0 do
|
Meta.withNewLocalInstances #[.fvar fvarId] 0 do
|
||||||
let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
|
let mvarUpstream ← mkUpstreamMVar mvarId
|
||||||
(← mvarId.getType) (kind := MetavarKind.synthetic) (userName := ← mvarId.getTag)
|
|
||||||
--let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
|
--let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
|
||||||
mvarId.assign mvarUpstream
|
mvarId.assign $ ← Meta.mkLambdaFVars #[.fvar fvarId] mvarUpstream
|
||||||
pure mvarUpstream
|
pure mvarUpstream
|
||||||
|
|
||||||
return {
|
return {
|
||||||
|
@ -57,7 +59,7 @@ def evalHave (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
|
||||||
let type ← Elab.Term.elabType (stx := type)
|
let type ← Elab.Term.elabType (stx := type)
|
||||||
let result ← «have» goal binderName type
|
let result ← «have» goal binderName type
|
||||||
pure [result.branch, result.main]
|
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
|
def «let» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult := mvarId.withContext do
|
||||||
mvarId.checkNotAssigned `Pantograph.Tactic.let
|
mvarId.checkNotAssigned `Pantograph.Tactic.let
|
||||||
|
@ -68,9 +70,8 @@ def «let» (mvarId: MVarId) (binderName: Name) (type: Expr): MetaM BranchResult
|
||||||
|
|
||||||
assert! ¬ type.hasLooseBVars
|
assert! ¬ type.hasLooseBVars
|
||||||
let mvarUpstream ← Meta.withLetDecl binderName type mvarBranch $ λ fvar => do
|
let mvarUpstream ← Meta.withLetDecl binderName type mvarBranch $ λ fvar => do
|
||||||
let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
|
let mvarUpstream ← mkUpstreamMVar mvarId
|
||||||
(type := ← mvarId.getType) (kind := MetavarKind.synthetic) (userName := ← mvarId.getTag)
|
mvarId.assign $ ← Meta.mkLetFVars #[fvar] mvarUpstream
|
||||||
mvarId.assign $ .letE binderName type fvar mvarUpstream (nonDep := false)
|
|
||||||
pure mvarUpstream
|
pure mvarUpstream
|
||||||
|
|
||||||
return {
|
return {
|
||||||
|
@ -82,6 +83,6 @@ def evalLet (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
|
||||||
let goal ← Elab.Tactic.getMainGoal
|
let goal ← Elab.Tactic.getMainGoal
|
||||||
let type ← goal.withContext $ Elab.Term.elabType (stx := type)
|
let type ← goal.withContext $ Elab.Term.elabType (stx := type)
|
||||||
let result ← «let» goal binderName type
|
let result ← «let» goal binderName type
|
||||||
Elab.Tactic.setGoals [result.branch, result.main]
|
Elab.Tactic.replaceMainGoal [result.branch, result.main]
|
||||||
|
|
||||||
end Pantograph.Tactic
|
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 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
|
def parseSentence (s: String): Elab.TermElabM Expr := do
|
||||||
let recursor ← match Parser.runParserCategory
|
let stx ← match Parser.runParserCategory
|
||||||
(env := ← MonadEnv.getEnv)
|
(env := ← MonadEnv.getEnv)
|
||||||
(catName := `term)
|
(catName := `term)
|
||||||
(input := s)
|
(input := s)
|
||||||
(fileName := filename) with
|
(fileName := filename) with
|
||||||
| .ok syn => pure syn
|
| .ok syn => pure syn
|
||||||
| .error error => throwError "Failed to parse: {error}"
|
| .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
|
def runTacticOnMVar (tacticM: Elab.Tactic.TacticM Unit) (goal: MVarId): Elab.TermElabM (List MVarId) := do
|
||||||
let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
|
let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
|
||||||
|
|
|
@ -7,7 +7,7 @@ open Pantograph
|
||||||
|
|
||||||
namespace Pantograph.Test.Tactic.Prograde
|
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 := "forall (p q : Prop) (h: p), And (Or p q) (Or p q)"
|
||||||
let expr ← parseSentence expr
|
let expr ← parseSentence expr
|
||||||
Meta.forallTelescope expr $ λ _ body => do
|
Meta.forallTelescope expr $ λ _ body => do
|
||||||
|
@ -48,9 +48,10 @@ def test_eval : TestT Elab.TermElabM Unit := do
|
||||||
],
|
],
|
||||||
target,
|
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 rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
|
||||||
let state0 ← GoalState.create rootExpr
|
let state0 ← GoalState.create rootExpr
|
||||||
let tactic := "intro p q h"
|
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
|
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 rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
|
||||||
let state0 ← GoalState.create rootExpr
|
let state0 ← GoalState.create rootExpr
|
||||||
let tactic := "intro p q h"
|
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 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
|
def test_let (specialized: Bool): TestT Elab.TermElabM Unit := do
|
||||||
let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
|
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) :=
|
def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
|
||||||
[
|
[
|
||||||
("eval", test_eval),
|
("define", test_define),
|
||||||
("Proof eval", test_proof_eval),
|
("define proof", test_define_proof),
|
||||||
("Proof have", test_proof_have),
|
("define root expr", test_define_root_expr),
|
||||||
|
("have proof", test_have_proof),
|
||||||
("let via assign", test_let false),
|
("let via assign", test_let false),
|
||||||
("let via tryLet", test_let true),
|
("let via tryLet", test_let true),
|
||||||
] |>.map (λ (name, t) => (name, runTestTermElabM env t))
|
] |>.map (λ (name, t) => (name, runTestTermElabM env t))
|
||||||
|
|
Loading…
Reference in New Issue