feat: Add support for the have, conv, and calc tactics #59

Merged
aniva merged 22 commits from goal/have-conv-calc into dev 2024-04-11 15:36:20 -07:00
1 changed files with 4 additions and 4 deletions
Showing only changes of commit 100cdd885f - Show all commits

View File

@ -32,7 +32,7 @@ structure GoalState where
parentMVar: Option MVarId
-- Existence of this field shows that we are currently in `conv` mode.
convMVar: Option (MVarId × MVarId × List MVarId) := .none
convMVar: Option (MVarId × MVarId) := .none
protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
-- May be necessary to immediately synthesise all metavariables if we need to leave the elaboration context.
@ -278,7 +278,7 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat):
savedState := nextSavedState
newMVars := newMVarSet prevMCtx nextMCtx,
parentMVar := .some goal,
convMVar := .some (convRhs, goal, state.goals),
convMVar := .some (convRhs, goal),
}
catch exception =>
return .failure #[← exception.toMessageData.toString]
@ -286,7 +286,7 @@ protected def GoalState.conv (state: GoalState) (goalId: Nat):
/-- Exit from `conv` mode. Resumes all goals before the mode starts and applys the conv -/
protected def GoalState.convExit (state: GoalState):
Elab.TermElabM TacticResult := do
let (convRhs, convGoal, savedGoals) ← match state.convMVar with
let (convRhs, convGoal) ← match state.convMVar with
| .some mvar => pure mvar
| .none => return .invalidAction "Not in conv state"
let tacticM : Elab.Tactic.TacticM Elab.Tactic.SavedState:= do
@ -303,7 +303,7 @@ protected def GoalState.convExit (state: GoalState):
throwError "convert tactic failed, there are unsolved goals\n{Elab.goalsToMessageData (← Elab.Tactic.getGoals)}"
IO.println "Caching"
Elab.Tactic.setGoals savedGoals
Elab.Tactic.setGoals [convGoal]
let targetNew ← instantiateMVars (.mvar convRhs)
let proof ← instantiateMVars (.mvar convGoal)