diff --git a/Pantograph/Goal.lean b/Pantograph/Goal.lean index 57f524b..b0be1d1 100644 --- a/Pantograph/Goal.lean +++ b/Pantograph/Goal.lean @@ -55,10 +55,13 @@ protected def GoalState.env (state: GoalState): Environment := state.savedState.term.meta.core.env private def GoalState.mvars (state: GoalState): SSet MVarId := state.mctx.decls.foldl (init := .empty) fun acc k _ => acc.insert k -private def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit := - state.savedState.term.restore protected def GoalState.restoreMetaM (state: GoalState): MetaM Unit := state.savedState.term.meta.restore +private def GoalState.restoreElabM (state: GoalState): Elab.TermElabM Unit := + state.savedState.term.restore +private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tactic.TacticM Unit := do + state.savedState.restore + Elab.Tactic.setGoals [goal] /-- Inner function for executing tactic on goal state -/ def executeTactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Syntax) : @@ -246,6 +249,84 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St catch exception => return .failure #[← exception.toMessageData.toString] +/-- Enter conv tactic mode -/ +protected def GoalState.tryConv (state: GoalState) (goalId: Nat): + Elab.TermElabM TacticResult := do + let goal ← match state.savedState.tactic.goals.get? goalId with + | .some goal => pure goal + | .none => return .indexError goalId + let tacticM : Elab.Tactic.TacticM Elab.Tactic.SavedState:= do + state.restoreTacticM goal + --let mm ← Meta.matchEq? (← goal.getType) + --if let .some (_, _, rhs) := mm then + -- if rhs.getAppFn.isMVar then + -- IO.println "isMVar ok" + -- else + -- IO.println "isMVar failed" + --else + -- IO.println "matchEq? failed" + IO.println s!"Old goals: {(← Elab.Tactic.getGoals).map (λ x => x.name.toString)}" + --Elab.Tactic.Conv.remarkAsConvGoal + let goalNew ← Elab.Tactic.Conv.markAsConvGoal goal + -- TODO: Error if `goal == goalNew` + Elab.Tactic.setGoals [goalNew] + --Elab.Tactic.Conv.remarkAsConvGoal + IO.println s!"New goals: {(← Elab.Tactic.getGoals).map (λ x => x.name.toString)}" + MonadBacktrack.saveState + let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic + let prevMCtx := state.savedState.term.meta.meta.mctx + let nextMCtx := nextSavedState.term.meta.meta.mctx + -- Generate a list of mvarIds that exist in the parent state; Also test the + -- assertion that the types have not changed on any mvars. + let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do + if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then + assert! prevMVarDecl.type == mvarDecl.type + return acc + else + return acc.insert mvarId + ) SSet.empty + return .success { + root := state.root, + savedState := nextSavedState + newMVars, + parentMVar := .some goal, + } + +protected def GoalState.tryConvTactic (state: GoalState) (goalId: Nat) (convTactic: String): + Elab.TermElabM TacticResult := do + let goal ← match state.savedState.tactic.goals.get? goalId with + | .some goal => pure goal + | .none => return .indexError goalId + let convTactic ← match Parser.runParserCategory + (env := ← MonadEnv.getEnv) + (catName := `conv) + (input := convTactic) + (fileName := filename) with + | .ok stx => pure $ stx + | .error error => return .parseError error + let tacticM : Elab.Tactic.TacticM Elab.Tactic.SavedState:= do + state.restoreTacticM goal + Elab.Tactic.Conv.evalConvTactic convTactic + MonadBacktrack.saveState + let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic + let nextMCtx := nextSavedState.term.meta.meta.mctx + let prevMCtx := state.savedState.term.meta.meta.mctx + -- Generate a list of mvarIds that exist in the parent state; Also test the + -- assertion that the types have not changed on any mvars. + let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do + if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then + assert! prevMVarDecl.type == mvarDecl.type + return acc + else + return acc.insert mvarId + ) SSet.empty + return .success { + root := state.root, + savedState := nextSavedState + newMVars, + parentMVar := .some goal, + } + /-- Brings into scope a list of goals diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 5a25b87..bfc0d4e 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -157,12 +157,13 @@ def test_arith: TestM Unit := do addTest $ assertUnreachable "Goal could not parse" return () - let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intros") with + let tactic := "intros" + let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check "intros" (state1.goals.length = 1) + addTest $ LSpec.check tactic (state1.goals.length = 1) addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *") with | .success state => pure state @@ -171,12 +172,13 @@ def test_arith: TestM Unit := do return () addTest $ LSpec.check "simp ..." (state2.goals.length = 1) addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone - let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := "assumption") with + let tactic := "assumption" + let state3 ← match ← state2.tryTactic (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.test "assumption" state3.goals.isEmpty + addTest $ LSpec.test tactic state3.goals.isEmpty addTest $ LSpec.check "(3 root)" state3.rootExpr?.isSome return () @@ -385,14 +387,40 @@ def test_conv: TestM Unit := do -- This solves the state in one-shot let tactic := "conv => { lhs; congr; rw [Nat.add_comm]; rfl }" - let state2 ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with + let stateT ← match ← state1.tryTactic (goalId := 0) (tactic := tactic) with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () - addTest $ LSpec.check tactic ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = + addTest $ LSpec.check tactic ((← stateT.serializeGoals (options := ← read)).map (·.devolatilize) = #[]) + let state2 ← match ← state1.tryConv (goalId := 0) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check "conv => ..." ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = + #[{ buildGoal [("a", "Nat"), ("b", "Nat"), ("c", "Nat")] "a + b + c" with isConversion := true }]) + + let convTactic := "lhs" + let state3L ← match ← state2.tryConvTactic (goalId := 0) (convTactic := convTactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check s!" {convTactic}" ((← state3L.serializeGoals (options := ← read)).map (·.devolatilize) = + #[{ buildGoal [("a", "Nat"), ("b", "Nat"), ("c", "Nat")] "a + b + c" with isConversion := true }]) + + let convTactic := "rhs" + let state3R ← match ← state2.tryConvTactic (goalId := 0) (convTactic := convTactic) with + | .success state => pure state + | other => do + addTest $ assertUnreachable $ other.toString + return () + addTest $ LSpec.check s!" {convTactic}" ((← state3R.serializeGoals (options := ← read)).map (·.devolatilize) = + #[{ buildGoal [("a", "Nat"), ("b", "Nat"), ("c", "Nat")] "b + a + c" with isConversion := true }]) + example : ∀ (a: Nat), 1 + a + 1 = a + 2 := by intro a calc 1 + a + 1 = a + 1 + 1 := by conv =>