feat: Evaluation tactic

This commit is contained in:
Leni Aniva 2024-06-23 15:01:51 -07:00
parent 361e2e8926
commit 25a7025c25
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
3 changed files with 35 additions and 1 deletions

View File

@ -302,6 +302,7 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St
Meta.withNewLocalInstances #[fvar] 0 do Meta.withNewLocalInstances #[fvar] 0 do
let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances) let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
(← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous) (← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
-- FIXME: May be redundant?
let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
goal.assign expr goal.assign expr
pure mvarUpstream pure mvarUpstream
@ -537,5 +538,16 @@ protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: Strin
| .ok syn => pure syn | .ok syn => pure syn
| .error error => return .parseError error | .error error => return .parseError error
state.execute goalId (tacticM := Tactic.noConfuse recursor) state.execute goalId (tacticM := Tactic.noConfuse recursor)
protected def GoalState.tryEval (state: GoalState) (goalId: Nat) (binderName: Name) (expr: String) :
Elab.TermElabM TacticResult := do
state.restoreElabM
let expr ← match Parser.runParserCategory
(env := state.env)
(catName := `term)
(input := expr)
(fileName := filename) with
| .ok syn => pure syn
| .error error => return .parseError error
state.execute goalId (tacticM := Tactic.tacticEval binderName expr)
end Pantograph end Pantograph

View File

@ -1,4 +1,4 @@
import Pantograph.Tactic.Congruence import Pantograph.Tactic.Congruence
import Pantograph.Tactic.MotivatedApply import Pantograph.Tactic.MotivatedApply
import Pantograph.Tactic.NoConfuse import Pantograph.Tactic.NoConfuse
import Pantograph.Tactic.Prograde

View File

@ -0,0 +1,22 @@
/- Prograde (forward) reasoning tactics -/
import Lean
open Lean
namespace Pantograph.Tactic
def tacticEval (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do
let goal ← Elab.Tactic.getMainGoal
let nextGoals ← goal.withContext do
let expr ← Elab.Term.elabTerm (stx := expr) (expectedType? := .none)
let type ← Meta.inferType expr
let mvarUpstream ← Meta.withLetDecl binderName type expr λ _ => do
let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
(← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
goal.assign mvarUpstream
pure mvarUpstream
pure [mvarUpstream.mvarId!]
Elab.Tactic.setGoals nextGoals
end Pantograph.Tactic