refactor: Assign into its own tactic

Pantograph/Goal.lean

@@ -178,13 +178,14 @@ inductive TacticResult where
   -- The given action cannot be executed in the state
   | invalidAction (message: String)
 
-protected def GoalState.execute (state: GoalState) (goalId: Nat) (tacticM: Elab.Tactic.TacticM Unit):
+/-- Executes a `TacticM` monads on this `GoalState`, collecting the errors as necessary -/
+protected def GoalState.executeTactic (state: GoalState) (goalId: Nat) (tacticM: Elab.Tactic.TacticM Unit):
       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.execute
+  goal.checkNotAssigned `GoalState.executeTactic
   try
     let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
     if (← getThe Core.State).messages.hasErrors then
@@ -204,7 +205,7 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tacticM: Elab.
   catch exception =>
     return .failure #[← exception.toMessageData.toString]
 
-/-- Execute tactic on given state -/
+/-- Execute a string tactic on given state -/
 protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String):
     Elab.TermElabM TacticResult := do
   let tactic ← match Parser.runParserCategory
@@ -214,68 +215,19 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri
     (fileName := filename) with
     | .ok stx => pure $ stx
     | .error error => return .parseError error
-  state.execute goalId $ Elab.Tactic.evalTactic tactic
+  state.executeTactic goalId $ Elab.Tactic.evalTactic tactic
-
-/-- Assumes elabM has already been restored. Assumes expr has already typechecked -/
-protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr):
-      Elab.TermElabM TacticResult := do
-  let goalType ← goal.getType
-  try
-    -- For some reason this is needed. One of the unit tests will fail if this isn't here
-    let error?: Option String ← goal.withContext do
-      let exprType ← Meta.inferType expr
-      if ← Meta.isDefEq goalType exprType then
-        pure .none
-      else do
-        return .some s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} != {← Meta.ppExpr goalType}"
-    if let .some error := error? then
-      return .parseError error
-    goal.checkNotAssigned `GoalState.assign
-    goal.assign expr
-    if (← getThe Core.State).messages.hasErrors then
-      let messages := (← getThe Core.State).messages.toArray
-      let errors ← (messages.map (·.data)).mapM fun md => md.toString
-      return .failure errors
-    let prevMCtx := state.savedState.term.meta.meta.mctx
-    let nextMCtx ← getMCtx
-    -- 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 := newMVarSet prevMCtx nextMCtx
-    let nextGoals ← newMVars.toList.filterM (not <$> ·.isAssigned)
-    return .success {
-      root := state.root,
-      savedState := {
-        term := ← MonadBacktrack.saveState,
-        tactic := { goals := nextGoals }
-      },
-      newMVars,
-      parentMVar? := .some goal,
-      calcPrevRhs? := .none
-    }
-  catch exception =>
-    return .failure #[← exception.toMessageData.toString]
 
 protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: 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.tryAssign
   let expr ← match Parser.runParserCategory
-    (env := state.env)
+    (env := ← MonadEnv.getEnv)
     (catName := `term)
     (input := expr)
     (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  let goalType ← goal.getType
+  state.executeTactic goalId $ Tactic.evalAssign expr
-  try
-    let expr ← goal.withContext $
-      Elab.Term.elabTermAndSynthesize (stx := expr) (expectedType? := .some goalType)
-    state.assign goal expr
-  catch exception =>
-    return .failure #[← exception.toMessageData.toString]
 
 -- Specialized Tactics
 
@@ -535,7 +487,7 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu
     (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.execute goalId (tacticM := Tactic.motivatedApply recursor)
+  state.executeTactic goalId (tacticM := Tactic.motivatedApply recursor)
 protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String):
       Elab.TermElabM TacticResult := do
   state.restoreElabM
@@ -546,6 +498,6 @@ protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: Strin
     (fileName := filename) with
     | .ok syn => pure syn
     | .error error => return .parseError error
-  state.execute goalId (tacticM := Tactic.noConfuse recursor)
+  state.executeTactic goalId (tacticM := Tactic.noConfuse recursor)
 
 end Pantograph

Pantograph/Library.lean

@@ -154,9 +154,6 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.G
         state.withParentContext do
           serializeExpression options (← instantiateAll expr)),
     }
-@[export pantograph_goal_diag_m]
-def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : CoreM String :=
-  runMetaM $ state.diag diagOptions
 
 @[export pantograph_goal_tactic_m]
 def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): CoreM TacticResult :=
@@ -189,20 +186,4 @@ def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Core
 def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): CoreM TacticResult :=
   runTermElabM <| state.tryNoConfuse goalId eq
 
-inductive SyntheticTactic where
-  | congruenceArg
-  | congruenceFun
-  | congruence
-/-- Executes a synthetic tactic which has no arguments -/
-@[export pantograph_goal_synthetic_tactic_m]
-def goalSyntheticTactic (state: GoalState) (goalId: Nat) (case: SyntheticTactic): CoreM TacticResult :=
-  runTermElabM do
-    state.restoreElabM
-    state.execute goalId $ match case with
-      | .congruenceArg => Tactic.congruenceArg
-      | .congruenceFun => Tactic.congruenceFun
-      | .congruence => Tactic.congruence
-
-
-
 end Pantograph

Pantograph/Serial.lean

@@ -286,7 +286,8 @@ protected def GoalState.serializeGoals
     | .none => throwError s!"Metavariable does not exist in context {goal.name}"
 
 /-- Print the metavariables in a readable format -/
-protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM String := do
+@[export pantograph_goal_state_diag_m]
+protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): MetaM String := do
   goalState.restoreMetaM
   let savedState := goalState.savedState
   let goals := savedState.tactic.goals
@@ -305,7 +306,7 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
   let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) =>
       !(goals.contains mvarId || mvarId == root) && options.printAll)
       |>.mapM (fun (mvarId, decl) => do
-        let pref := if goalState.newMVars.contains mvarId then "~" else " "
+        let pref := if parentHasMVar mvarId then " " else "~"
         printMVar pref mvarId decl
       )
   pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
@@ -345,5 +346,6 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
     userNameToString : Name → String
       | .anonymous => ""
       | other => s!"[{other}]"
+    parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true
 
 end Pantograph

Pantograph/Tactic.lean

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

Pantograph/Tactic/Assign.lean

@@ -0,0 +1,35 @@
+import Lean
+
+open Lean
+
+namespace Pantograph.Tactic
+
+private def newMVarSet (mctxOld: @&MetavarContext) (mctxNew: @&MetavarContext): SSet MVarId :=
+  mctxNew.decls.foldl (fun acc mvarId mvarDecl =>
+    if let .some prevMVarDecl := mctxOld.decls.find? mvarId then
+      assert! prevMVarDecl.type == mvarDecl.type
+      acc
+    else
+      acc.insert mvarId
+    ) SSet.empty
+def assign (goal: MVarId) (expr: Expr): MetaM (List MVarId) := do
+  goal.checkNotAssigned `Pantograph.Tactic.assign
+
+  -- This run of the unifier is critical in resolving mvars in passing
+  let exprType ← Meta.inferType expr
+  let goalType ← goal.getType
+  unless ← Meta.isDefEq goalType exprType do
+    throwError s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} ≠ {← Meta.ppExpr goalType}"
+
+  let nextGoals ← Meta.getMVars expr
+  goal.assign expr
+  nextGoals.toList.filterM (not <$> ·.isAssigned)
+
+def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
+  let goalType ← Elab.Tactic.getMainTarget
+  let expr ← Elab.Term.elabTermAndSynthesize (stx := stx) (expectedType? := .some goalType)
+  let nextGoals ← assign (← Elab.Tactic.getMainGoal) expr
+  Elab.Tactic.setGoals nextGoals
+
+
+end Pantograph.Tactic

Test/Metavar.lean

@@ -198,10 +198,10 @@ def test_proposition_generation: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "Nat → Prop", .some "∀ (x : Nat), ?m.29 x"])
+    #[.some "∀ (x : Nat), ?m.29 x"])
   addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone
 
-  let state3 ← match ← state2.tryAssign (goalId := 1) (expr := "fun x => Eq.refl x") with
+  let state3 ← match ← state2.tryAssign (goalId := 0) (expr := "fun x => Eq.refl x") with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString