Pantograph.lean

@@ -140,8 +140,6 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         return .ok { parseError? := .some message }
       | .ok (.indexError goalId) =>
         return .error $ errorIndex s!"Invalid goal id index {goalId}"
-      | .ok (.invalidAction message) =>
-        return .error $ errorI "invalid" message
       | .ok (.failure messages) =>
         return .ok { tacticErrors? := .some messages }
   goal_continue (args: Protocol.GoalContinue): MainM (CR Protocol.GoalContinueResult) := do

Pantograph/Goal.lean

@@ -31,9 +31,6 @@ structure GoalState where
   -- Parent state metavariable source
   parentMVar: Option MVarId
 
-  -- Existence of this field shows that we are currently in `conv` mode.
-  convMVar: Option (MVarId × MVarId × List 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.
   -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
@@ -103,8 +100,6 @@ inductive TacticResult where
   | parseError (message: String)
   -- The goal index is out of bounds
   | indexError (goalId: Nat)
-  -- The given action cannot be executed in the state
-  | invalidAction (message: String)
 
 /-- Execute tactic on given state -/
 protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String):
@@ -127,11 +122,11 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri
   | .ok nextSavedState =>
     -- Assert that the definition of metavariables are the same
     let nextMCtx := nextSavedState.term.meta.meta.mctx
-    let prevMCtx := state.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.
     return .success {
-      state with
+      root := state.root,
       savedState := nextSavedState
       newMVars := newMVarSet prevMCtx nextMCtx,
       parentMVar := .some goal,
@@ -151,7 +146,7 @@ protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr):
         return .some s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} != {← Meta.ppExpr goalType}"
     )
     if let .some error := error? then
-      return .parseError error
+      return .failure #["Type unification failed", error]
     goal.checkNotAssigned `GoalState.assign
     goal.assign expr
     if (← getThe Core.State).messages.hasErrors then
@@ -251,45 +246,35 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St
     return .failure #[← exception.toMessageData.toString]
 
 /-- Enter conv tactic mode -/
-protected def GoalState.conv (state: GoalState) (goalId: Nat):
+protected def GoalState.tryConv (state: GoalState) (goalId: Nat):
       Elab.TermElabM TacticResult := do
-  if state.convMVar.isSome then
-    return .invalidAction "Already in conv state"
   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 × MVarId) := do
+  let tacticM :  Elab.Tactic.TacticM Elab.Tactic.SavedState:= do
     state.restoreTacticM goal
 
     -- TODO: Fail if this is already in conv
 
     -- See Lean.Elab.Tactic.Conv.convTarget
-    let convMVar ← Elab.Tactic.withMainContext do
+    Elab.Tactic.withMainContext do
       -- TODO: Memorize this `rhs` as a conv resultant goal
       let (rhs, newGoal) ← Elab.Tactic.Conv.mkConvGoalFor (← Elab.Tactic.getMainTarget)
       Elab.Tactic.setGoals [newGoal.mvarId!]
-      pure rhs.mvarId!
-    return (← MonadBacktrack.saveState, convMVar)
-  try
-    let (nextSavedState, convRhs) ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
-    let prevMCtx := state.mctx
+    --Elab.Tactic.liftMetaTactic1 fun mvarId => mvarId.replaceTargetEq rhs proof
+    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
   return .success {
     root := state.root,
     savedState := nextSavedState
     newMVars := newMVarSet prevMCtx nextMCtx,
     parentMVar := .some goal,
-      convMVar := .some (convRhs, goal, state.goals),
   }
-  catch exception =>
-    return .failure #[← exception.toMessageData.toString]
 
-/-- Execute a tactic in conv mode -/
 protected def GoalState.tryConvTactic (state: GoalState) (goalId: Nat) (convTactic: String):
       Elab.TermElabM TacticResult := do
-  let _ ← match state.convMVar with
-    | .some mvar => pure mvar
-    | .none => return .invalidAction "Not in conv state"
   let goal ← match state.savedState.tactic.goals.get? goalId with
     | .some goal => pure goal
     | .none => return .indexError goalId
@@ -304,60 +289,15 @@ protected def GoalState.tryConvTactic (state: GoalState) (goalId: Nat) (convTact
     state.restoreTacticM goal
     Elab.Tactic.evalTactic convTactic
     MonadBacktrack.saveState
-  try
-    let prevMCtx := state.mctx
   let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
   let nextMCtx := nextSavedState.term.meta.meta.mctx
-    return .success {
-      state with
-      savedState := nextSavedState
-      newMVars := newMVarSet prevMCtx nextMCtx,
-      parentMVar := .some goal,
-    }
-  catch exception =>
-    return .failure #[← exception.toMessageData.toString]
-
-protected def GoalState.convExit (state: GoalState):
-      Elab.TermElabM TacticResult := do
-  let (convRhs, convGoal, savedGoals) ← match state.convMVar with
-    | .some mvar => pure mvar
-    | .none => return .invalidAction "Not in conv state"
-  let tacticM :  Elab.Tactic.TacticM Elab.Tactic.SavedState:= do
-    -- Vide `Lean.Elab.Tactic.Conv.convert`
-    state.savedState.restore
-
-    IO.println "Restored state"
-
-    -- Close all existing goals with `refl`
-    for mvarId in (← Elab.Tactic.getGoals) do
-      liftM <| mvarId.refl <|> mvarId.inferInstance <|> pure ()
-    Elab.Tactic.pruneSolvedGoals
-    unless (← Elab.Tactic.getGoals).isEmpty do
-      throwError "convert tactic failed, there are unsolved goals\n{Elab.goalsToMessageData (← Elab.Tactic.getGoals)}"
-
-    IO.println "Caching"
-    Elab.Tactic.setGoals savedGoals
-
-    let targetNew ← instantiateMVars (.mvar convRhs)
-    let proof ← instantiateMVars (.mvar convGoal)
-
-    Elab.Tactic.liftMetaTactic1 fun mvarId => mvarId.replaceTargetEq targetNew proof
-    MonadBacktrack.saveState
-  try
-    let nextSavedState ← tacticM { elaborator := .anonymous } |>.run' state.savedState.tactic
-    IO.println "Finished caching"
-    let nextMCtx := nextSavedState.term.meta.meta.mctx
   let prevMCtx := state.savedState.term.meta.meta.mctx
   return .success {
     root := state.root,
     savedState := nextSavedState
     newMVars := newMVarSet prevMCtx nextMCtx,
-      parentMVar := .some convGoal,
-      convMVar := .none
+    parentMVar := .some goal,
   }
-  catch exception =>
-    return .failure #[← exception.toMessageData.toString]
-
 
 
 /--

Pantograph/Serial.lean

@@ -160,12 +160,14 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
   of_name (name: Name) := name_to_ast name sanitize
 
 def serialize_expression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
-  let pp?: Option String ← match options.printExprPretty with
-    | true => pure $ .some $ toString $ ← Meta.ppExpr e
-    | false => pure $ .none
-  let sexp?: Option String ← match options.printExprAST with
-    | true => pure $ .some $ ← serialize_expression_ast e
-    | false => pure $ .none
+  let pp := toString (← Meta.ppExpr e)
+  let pp?: Option String := match options.printExprPretty with
+    | true => .some pp
+    | false => .none
+  let sexp: String ← serialize_expression_ast e
+  let sexp?: Option String := match options.printExprAST with
+    | true => .some sexp
+    | false => .none
   return {
     pp?,
     sexp?

Test/Common.lean

@@ -37,7 +37,6 @@ def TacticResult.toString : TacticResult → String
     s!".failure {messages}"
   | .parseError error => s!".parseError {error}"
   | .indexError index => s!".indexError {index}"
-  | .invalidAction error => s!".invalidAction {error}"
 
 namespace Test
 

Test/Proofs.lean

@@ -361,48 +361,47 @@ def test_have: TestM Unit := do
 
   addTest $ LSpec.check "(4 root)" state4.rootExpr?.isSome
 
-example : ∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2 := by
-  intro a b c1 c2 h
+example : ∀ (a b c: Nat), (a + b) + c = (b + a) + c := by
+  intro a b c
   conv =>
     lhs
     congr
-    . rw [Nat.add_comm]
-    . rfl
-  exact h
+    rw [Nat.add_comm]
+    rfl
 
 def test_conv: TestM Unit := do
-  let state? ← startProof (.expr "∀ (a b c1 c2: Nat), (b + a) + c1 = (b + a) + c2 → (a + b) + c1 = (b + a) + c2")
+  let state? ← startProof (.expr "∀ (a b c: Nat), (a + b) + c = (b + a) + c")
   let state0 ← match state? with
     | .some state => pure state
     | .none => do
       addTest $ assertUnreachable "Goal could not parse"
       return ()
-
-  let tactic := "intro a b c1 c2 h"
+  let tactic := "intro a b c"
   let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := tactic) with
     | .success state => pure state
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check tactic ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[interiorGoal [] "a + b + c1 = b + a + c2"])
+    #[buildGoal [("a", "Nat"), ("b", "Nat"), ("c", "Nat")] "a + b + c = b + a + c"])
 
-  let state2 ← match ← state1.conv (goalId := 0) with
+  -- This solves the state in one-shot
+  let tactic := "conv => { lhs; congr; rw [Nat.add_comm]; rfl }"
+  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 ((← 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) =
-    #[{ interiorGoal [] "a + b + c1 = b + a + c2" 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} (discard)" ((← state3R.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[{ interiorGoal [] "b + a + c2" with isConversion := true }])
+    #[{ buildGoal [("a", "Nat"), ("b", "Nat"), ("c", "Nat")] "a + b + c = b + a + c" with isConversion := true }])
 
   let convTactic := "lhs"
   let state3L ← match ← state2.tryConvTactic (goalId := 0) (convTactic := convTactic) with
@@ -411,73 +410,16 @@ def test_conv: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check s!"  {convTactic}" ((← state3L.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[{ interiorGoal [] "a + b + c1" with isConversion := true }])
+    #[{ buildGoal [("a", "Nat"), ("b", "Nat"), ("c", "Nat")] "a + b + c" with isConversion := true }])
 
-  let convTactic := "congr"
-  let state4 ← match ← state3L.tryConvTactic (goalId := 0) (convTactic := convTactic) with
+  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}" ((← state4.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[
-      { interiorGoal [] "a + b" with isConversion := true, userName? := .some "a" },
-      { interiorGoal [] "c1" with isConversion := true, userName? := .some "a" }
-    ])
-
-  let convTactic := "rw [Nat.add_comm]"
-  let state5_1 ← match ← state4.tryConvTactic (goalId := 0) (convTactic := convTactic) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"  · {convTactic}" ((← state5_1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[{ interiorGoal [] "b + a" with isConversion := true, userName? := .some "a" }])
-
-  let convTactic := "rfl"
-  let state6_1 ← match ← state5_1.tryConvTactic (goalId := 0) (convTactic := convTactic) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"    {convTactic}" ((← state6_1.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[])
-
-  let state4_1 ← match state6_1.continue state4 with
-    | .ok state => pure state
-    | .error e => do
-      addTest $ expectationFailure "continue" e
-      return ()
-
-  let convTactic := "rfl"
-  let state6 ← match ← state4_1.tryConvTactic (goalId := 0) (convTactic := convTactic) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check s!"  · {convTactic}" ((← state6.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[])
-
-  let state1_1 ← match ← state6.convExit with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-
-  let tactic := "exact h"
-  let stateF ← match ← state1_1.tryTactic (goalId := 0) (tactic := tactic) with
-    | .success state => pure state
-    | other => do
-      addTest $ assertUnreachable $ other.toString
-      return ()
-  addTest $ LSpec.check tactic ((← stateF.serializeGoals (options := ← read)).map (·.devolatilize) =
-    #[])
-
-  where
-    h := "b + a + c1 = b + a + c2"
-    interiorGoal (free: List (String × String)) (target: String) :=
-      let free := [("a", "Nat"), ("b", "Nat"), ("c1", "Nat"), ("c2", "Nat"), ("h", h)] ++ free
-      buildGoal free target
+  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