feat: Prograde tactics #83

Merged
aniva merged 24 commits from tactic/eval into dev 2024-08-31 20:04:39 -07:00
6 changed files with 53 additions and 71 deletions
Showing only changes of commit 7acf1ffdf1 - Show all commits

View File

@ -125,7 +125,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
pure ( Except.ok (← goalAssign goalState args.goalId expr)) pure ( Except.ok (← goalAssign goalState args.goalId expr))
| .none, .none, .some type, .none, .none => do | .none, .none, .some type, .none, .none => do
let binderName := args.binderName?.getD "" let binderName := args.binderName?.getD ""
pure ( Except.ok (← goalHave goalState args.goalId binderName type)) pure ( Except.ok (← goalState.tryHave args.goalId binderName type))
| .none, .none, .none, .some pred, .none => do | .none, .none, .none, .some pred, .none => do
pure ( Except.ok (← goalCalc goalState args.goalId pred)) pure ( Except.ok (← goalCalc goalState args.goalId pred))
| .none, .none, .none, .none, .some true => do | .none, .none, .none, .none, .some true => do

View File

@ -2,7 +2,7 @@
import Pantograph.Protocol import Pantograph.Protocol
import Pantograph.Compile.Frontend import Pantograph.Compile.Frontend
import Pantograph.Compile.Elab import Pantograph.Compile.Elab
import Pantograph.Compile.Parse
open Lean open Lean

View File

@ -0,0 +1,14 @@
import Lean
open Lean
namespace Pantograph.Compile
def parseTermM [Monad m] [MonadEnv m] (s: String): m (Except String Syntax) := do
return Parser.runParserCategory
(env := ← MonadEnv.getEnv)
(catName := `term)
(input := s)
(fileName := "<stdin>")
end Pantograph.Compile

View File

@ -5,6 +5,7 @@ All the functions starting with `try` resume their inner monadic state.
-/ -/
import Pantograph.Protocol import Pantograph.Protocol
import Pantograph.Tactic import Pantograph.Tactic
import Pantograph.Compile.Parse
import Lean import Lean
def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog := def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
@ -277,57 +278,6 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String
-- Specialized Tactics -- Specialized Tactics
protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String):
Elab.TermElabM TacticResult := do
state.restoreElabM
let goal ← match state.savedState.tactic.goals.get? goalId with
| .some goal => pure goal
| .none => return .indexError goalId
goal.checkNotAssigned `GoalState.tryHave
let type ← match Parser.runParserCategory
(env := state.env)
(catName := `term)
(input := type)
(fileName := filename) with
| .ok syn => pure syn
| .error error => return .parseError error
let binderName := binderName.toName
try
-- Implemented similarly to the intro tactic
let nextGoals: List MVarId ← goal.withContext do
let type ← Elab.Term.elabType (stx := type)
let lctx ← MonadLCtx.getLCtx
-- The branch goal inherits the same context, but with a different type
let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
-- Create the context for the `upstream` goal
let fvarId ← mkFreshFVarId
let lctxUpstream := lctx.mkLocalDecl fvarId binderName type
let fvar := mkFVar fvarId
let mvarUpstream ←
withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
Meta.withNewLocalInstances #[fvar] 0 do
let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
(← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
-- FIXME: May be redundant?
let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
goal.assign expr
pure mvarUpstream
pure [mvarBranch.mvarId!, mvarUpstream.mvarId!]
return .success {
root := state.root,
savedState := {
term := ← MonadBacktrack.saveState,
tactic := { goals := nextGoals }
},
newMVars := nextGoals.toSSet,
parentMVar? := .some goal,
calcPrevRhs? := .none
}
catch exception =>
return .failure #[← exception.toMessageData.toString]
protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): protected def GoalState.tryLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String):
Elab.TermElabM TacticResult := do Elab.TermElabM TacticResult := do
state.restoreElabM state.restoreElabM
@ -527,33 +477,21 @@ protected def GoalState.tryCalc (state: GoalState) (goalId: Nat) (pred: String):
protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String):
Elab.TermElabM TacticResult := do Elab.TermElabM TacticResult := do
state.restoreElabM state.restoreElabM
let recursor ← match Parser.runParserCategory let recursor ← match (← Compile.parseTermM recursor) with
(env := state.env)
(catName := `term)
(input := recursor)
(fileName := filename) with
| .ok syn => pure syn | .ok syn => pure syn
| .error error => return .parseError error | .error error => return .parseError error
state.execute goalId (tacticM := Tactic.motivatedApply recursor) state.execute goalId (tacticM := Tactic.motivatedApply recursor)
protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String): protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String):
Elab.TermElabM TacticResult := do Elab.TermElabM TacticResult := do
state.restoreElabM state.restoreElabM
let recursor ← match Parser.runParserCategory let eq ← match (← Compile.parseTermM eq) with
(env := state.env)
(catName := `term)
(input := eq)
(fileName := filename) with
| .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 eq)
protected def GoalState.tryEval (state: GoalState) (goalId: Nat) (binderName: Name) (expr: String) : protected def GoalState.tryEval (state: GoalState) (goalId: Nat) (binderName: Name) (expr: String) :
Elab.TermElabM TacticResult := do Elab.TermElabM TacticResult := do
state.restoreElabM state.restoreElabM
let expr ← match Parser.runParserCategory let expr ← match (← Compile.parseTermM expr) with
(env := state.env)
(catName := `term)
(input := expr)
(fileName := filename) with
| .ok syn => pure syn | .ok syn => pure syn
| .error error => return .parseError error | .error error => return .parseError error
state.execute goalId (tacticM := Tactic.evaluate binderName expr) state.execute goalId (tacticM := Tactic.evaluate binderName expr)

View File

@ -180,8 +180,13 @@ def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): CoreM TacticRe
def goalAssign (state: GoalState) (goalId: Nat) (expr: String): CoreM TacticResult := def goalAssign (state: GoalState) (goalId: Nat) (expr: String): CoreM TacticResult :=
runTermElabM <| state.tryAssign goalId expr runTermElabM <| state.tryAssign goalId expr
@[export pantograph_goal_have_m] @[export pantograph_goal_have_m]
def goalHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := do
runTermElabM <| state.tryHave goalId binderName type let type ← match (← Compile.parseTermM type) with
| .ok syn => pure syn
| .error error => return .parseError error
runTermElabM do
state.restoreElabM
state.execute goalId (Tactic.have_t binderName.toName type)
@[export pantograph_goal_let_m] @[export pantograph_goal_let_m]
def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult := def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult :=
runTermElabM <| state.tryLet goalId binderName type runTermElabM <| state.tryLet goalId binderName type

View File

@ -19,4 +19,29 @@ def evaluate (binderName: Name) (expr: Syntax): Elab.Tactic.TacticM Unit := do
pure [mvarUpstream.mvarId!] pure [mvarUpstream.mvarId!]
Elab.Tactic.setGoals nextGoals Elab.Tactic.setGoals nextGoals
def have_t (binderName: Name) (type: Syntax): Elab.Tactic.TacticM Unit := do
let goal ← Elab.Tactic.getMainGoal
let nextGoals: List MVarId ← goal.withContext do
let type ← Elab.Term.elabType (stx := type)
let lctx ← MonadLCtx.getLCtx
-- The branch goal inherits the same context, but with a different type
let mvarBranch ← Meta.mkFreshExprMVarAt lctx (← Meta.getLocalInstances) type
-- Create the context for the `upstream` goal
let fvarId ← mkFreshFVarId
let lctxUpstream := lctx.mkLocalDecl fvarId binderName type
let fvar := mkFVar fvarId
let mvarUpstream ←
withTheReader Meta.Context (fun ctx => { ctx with lctx := lctxUpstream }) do
Meta.withNewLocalInstances #[fvar] 0 do
let mvarUpstream ← Meta.mkFreshExprMVarAt (← getLCtx) (← Meta.getLocalInstances)
(← goal.getType) (kind := MetavarKind.synthetic) (userName := .anonymous)
--let expr: Expr := .app (.lam binderName type mvarBranch .default) mvarUpstream
goal.assign mvarUpstream
pure mvarUpstream
pure [mvarBranch.mvarId!, mvarUpstream.mvarId!]
Elab.Tactic.setGoals nextGoals
end Pantograph.Tactic end Pantograph.Tactic