Pantograph/Delate.lean

@@ -454,7 +454,6 @@ def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.
     dependentMVars?,
   }
 
-
 /-- Adapted from ppGoal -/
 def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl := .none)
       : MetaM Protocol.Goal := do
@@ -520,7 +519,6 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
     return {
       name := goal.name.toString,
       userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
-      isConversion := isLHSGoal? mvarDecl.type |>.isSome,
       target := (← serializeExpression options (← instantiate mvarDecl.type)),
       vars := vars.reverse.toArray
     }
@@ -535,10 +533,15 @@ protected def GoalState.serializeGoals
   state.restoreMetaM
   let goals := state.goals.toArray
   goals.mapM fun goal => do
+    let fragment := match state.fragments[goal]? with
+      | .none => .tactic
+      | .some $ .calc .. => .calc
+      | .some $ .conv .. => .conv
+      | .some $ .convSentinel .. => .conv
     match state.mctx.findDecl? goal with
     | .some mvarDecl =>
       let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := .none)
-      pure serializedGoal
+      pure { serializedGoal with fragment }
     | .none => throwError s!"Metavariable does not exist in context {goal.name}"
 
 /-- Print the metavariables in a readable format -/

Pantograph/Protocol.lean

@@ -60,16 +60,21 @@ structure Variable where
   type?: Option Expression  := .none
   value?: Option Expression := .none
   deriving Lean.ToJson
+inductive Fragment where
+  | tactic
+  | conv
+  | calc
+  deriving BEq, DecidableEq, Repr, Lean.ToJson
 structure Goal where
-  name: String := ""
   /-- Name of the metavariable -/
-  userName?: Option String  := .none
-  /-- Is the goal in conversion mode -/
-  isConversion: Bool        := false
+  name : String := ""
+  /-- User-facing name -/
+  userName? : Option String  := .none
+  fragment : Fragment := .tactic
   /-- target expression type -/
-  target: Expression
+  target : Expression
   /-- Variables -/
-  vars: Array Variable      := #[]
+  vars : Array Variable      := #[]
   deriving Lean.ToJson
 
 

Test/Tactic/Fragment.lean

@@ -46,7 +46,7 @@ def test_conv_simple: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "conv => ..." ((← state2.serializeGoals).map (·.devolatilize) =
-    #[{ interiorGoal [] "a + b + c1 = b + a + c2" with isConversion := true }])
+    #[{ interiorGoal [] "a + b + c1 = b + a + c2" with fragment := .conv }])
 
   let convTactic := "rhs"
   let state3R ← match ← state2.tacticOn (goalId := 0) convTactic with
@@ -55,7 +55,7 @@ def test_conv_simple: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check s!"  {convTactic} (discard)" ((← state3R.serializeGoals).map (·.devolatilize) =
-    #[{ interiorGoal [] "b + a + c2" with isConversion := true }])
+    #[{ interiorGoal [] "b + a + c2" with fragment := .conv }])
 
   let convTactic := "lhs"
   let state3L ← match ← state2.tacticOn (goalId := 0) convTactic with
@@ -64,7 +64,7 @@ def test_conv_simple: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check s!"  {convTactic}" ((← state3L.serializeGoals).map (·.devolatilize) =
-    #[{ interiorGoal [] "a + b + c1" with isConversion := true }])
+    #[{ interiorGoal [] "a + b + c1" with fragment := .conv }])
 
   let convTactic := "congr"
   let state4 ← match ← state3L.tacticOn (goalId := 0) convTactic with
@@ -74,8 +74,8 @@ def test_conv_simple: TestM Unit := do
       return ()
   addTest $ LSpec.check s!"  {convTactic}" ((← state4.serializeGoals).map (·.devolatilize) =
     #[
-      { interiorGoal [] "a + b" with isConversion := true, userName? := .some "a" },
-      { interiorGoal [] "c1" with isConversion := true, userName? := .some "a" }
+      { interiorGoal [] "a + b" with fragment := .conv, userName? := .some "a" },
+      { interiorGoal [] "c1" with fragment := .conv, userName? := .some "a" }
     ])
 
   let convTactic := "rw [Nat.add_comm]"
@@ -85,7 +85,7 @@ def test_conv_simple: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check s!"  · {convTactic}" ((← state5_1.serializeGoals).map (·.devolatilize) =
-    #[{ interiorGoal [] "b + a" with isConversion := true, userName? := .some "a" }])
+    #[{ interiorGoal [] "b + a" with fragment := .conv, userName? := .some "a" }])
 
   let convTactic := "rfl"
   let state6_1 ← match ← state5_1.tacticOn (goalId := 0) convTactic with
@@ -159,7 +159,7 @@ def test_conv_unshielded : TestM Unit := do
   let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
   checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
     #[
-      { interiorGoal [] "y" with isConversion := true },
+      { interiorGoal [] "y" with fragment := .conv },
       { interiorGoal [] "p" with userName? := "right", },
     ]
   let tactic := "rw [←hi]"
@@ -206,13 +206,13 @@ def test_conv_unfinished : TestM Unit := do
   let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
   checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
     #[
-      { interiorGoal [] "y" with isConversion := true },
+      { interiorGoal [] "y" with fragment := .conv },
     ]
   let tactic := "rw [hyz]"
   let .success state _ ← state.tryTactic .unfocus tactic | fail s!"{tactic} failed"
   checkEq s!"  {tactic}" ((← state.serializeGoals).map (·.devolatilize))
     #[
-      { interiorGoal [] "z" with isConversion := true },
+      { interiorGoal [] "z" with fragment := .conv },
     ]
   checkTrue "  (fragment)" $ state.fragments.contains state.mainGoal?.get!
   checkTrue "  (fragment parent)" $ state.fragments.contains convParent
@@ -260,7 +260,7 @@ def test_calc: TestM Unit := do
   addTest $ LSpec.check s!"calc {pred} := _" ((← state2.serializeGoals).map (·.devolatilize) =
     #[
       { interiorGoal [] "a + b = b + c" with userName? := .some "calc" },
-      interiorGoal [] "b + c = c + d"
+      { interiorGoal [] "b + c = c + d" with fragment := .calc },
     ])
   addTest $ LSpec.test "(2.0 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 0) |>.isNone)
   addTest $ LSpec.test "(2.1 prev rhs)" (state2.calcPrevRhsOf? (state2.get! 1) |>.isSome)

doc/repl.md

@@ -13,7 +13,7 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
   only the values of definitions are printed.
 * `env.save { "path": <fileName> }`, `env.load { "path": <fileName> }`: Save/Load the
   current environment to/from a file
-* `env.module_read { "module": <name }`: Reads a list of symbols from a module
+* `env.module_read { "module": <name> }`: Reads a list of symbols from a module
 * `env.describe {}`: Describes the imports and modules in the current environment
 * `options.set { key: value, ... }`: Set one or more options (not Lean options; those
   have to be set via command line arguments.), for options, see `Pantograph/Protocol.lean`
@@ -28,16 +28,19 @@ See `Pantograph/Protocol.lean` for a description of the parameters and return va
 * `options.print`: Display the current set of options
 * `goal.start {["name": <name>], ["expr": <expr>], ["levels": [<levels>]], ["copyFrom": <symbol>]}`:
   Start a new proof from a given expression or symbol
-* `goal.tactic {"stateId": <id>, "goalId": <id>, ...}`: Execute a tactic string on a
-  given goal. The tactic is supplied as additional key-value pairs in one of the following formats:
-  - `{ "tactic": <tactic> }`: Execute an ordinary tactic
-  - `{ "expr": <expr> }`: Assign the given proof term to the current goal
-  - `{ "have": <expr>, "binderName": <name> }`: Execute `have` and creates a branch goal
-  - `{ "calc": <expr> }`: Execute one step of a `calc` tactic. Each step must
+* `goal.tactic {"stateId": <id>, ["goalId": <id>], ["autoResume": <bool>], ...}`:
+  Execute a tactic string on a given goal site. The tactic is supplied as additional
+  key-value pairs in one of the following formats:
+  - `{ "tactic": <tactic> }`: Executes a tactic in the current mode
+  - `{ "mode": <mode> }`: Enter a different tactic mode. The permitted values
+    are `tactic` (default), `conv`, `calc`. In case of `calc`, each step must
     be of the form `lhs op rhs`. An `lhs` of `_` indicates that it should be set
     to the previous `rhs`.
-  - `{ "conv": <bool> }`: Enter or exit conversion tactic mode.
-  - `{ "draft": <expr> }`: Draft an expression with `sorry`s, turning them into goals. Coupling is not allowed.
+  - `{ "expr": <expr> }`: Assign the given proof term to the current goal
+  - `{ "have": <expr>, "binderName": <name> }`: Execute `have` and creates a branch goal
+  - `{ "let": <expr>, "binderName": <name> }`: Execute `let` and creates a branch goal
+  - `{ "draft": <expr> }`: Draft an expression with `sorry`s, turning them into
+    goals. Coupling is not allowed.
   If the `goals` field does not exist, the tactic execution has failed. Read
   `messages` to find the reason.
 * `goal.continue {"stateId": <id>, ["branch": <id>], ["goals": <names>]}`: