From 82f5494718b6b9383512451baf2ef80833c503f0 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 27 Oct 2023 15:32:59 -0700
Subject: [PATCH] feat: Add REPL command for assigning an expression

---
 Pantograph.lean          | 24 +++++++++++++++---------
 Pantograph/Protocol.lean |  4 +++-
 Test/Integration.lean    | 21 ++++++++++++++++++++-
 3 files changed, 38 insertions(+), 11 deletions(-)

diff --git a/Pantograph.lean b/Pantograph.lean
index 29f9bd5..dd25e9f 100644
--- a/Pantograph.lean
+++ b/Pantograph.lean
@@ -133,9 +133,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
         (match env.find? <| str_to_name copyFrom with
         | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
         | .some cInfo => return .ok cInfo.type)
-      | .none, .none =>
-        return .error <| errorI "arguments" "At least one of {expr, copyFrom} must be supplied"
-      | _, _ => return .error <| errorI "arguments" "Cannot populate both of {expr, copyFrom}")
+      | _, _ =>
+        return .error <| errorI "arguments" "Exactly one of {expr, copyFrom} must be supplied")
     match expr? with
     | .error error => return .error error
     | .ok expr =>
@@ -147,9 +146,16 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let state ← get
     match state.goalStates.get? args.stateId with
     | .none => return .error $ errorIndex s!"Invalid state index {args.stateId}"
-    | .some goalState =>
-      match ← GoalState.execute goalState args.goalId args.tactic with
-      | .success nextGoalState =>
+    | .some goalState => do
+      let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with
+        | .some tactic, .none => do
+          pure ( Except.ok (← GoalState.execute goalState args.goalId tactic))
+        | .none, .some expr => do
+          pure ( Except.ok (← GoalState.tryAssign goalState args.goalId expr))
+        | _, _ => pure (Except.error <| errorI "arguments" "Exactly one of {tactic, expr} must be supplied")
+      match nextGoalState? with
+      | .error error => return .error error
+      | .ok (.success nextGoalState) =>
         let (goalStates, nextStateId) := state.goalStates.insert nextGoalState
         set { state with goalStates }
         let goals ← nextGoalState.serializeGoals (parent := .some goalState) (options := state.options)
@@ -157,11 +163,11 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           nextStateId? := .some nextStateId,
           goals? := .some goals,
         }
-      | .parseError message =>
+      | .ok (.parseError message) =>
         return .ok { parseError? := .some message }
-      | .indexError goalId =>
+      | .ok (.indexError goalId) =>
         return .error $ errorIndex s!"Invalid goal id index {goalId}"
-      | .failure messages =>
+      | .ok (.failure messages) =>
         return .ok { tacticErrors? := .some messages }
   goal_delete (args: Protocol.GoalDelete): MainM (CR Protocol.GoalDeleteResult) := do
     let state ← get
diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean
index b0e7744..62700c4 100644
--- a/Pantograph/Protocol.lean
+++ b/Pantograph/Protocol.lean
@@ -146,7 +146,9 @@ structure GoalTactic where
   -- Identifiers for tree, state, and goal
   stateId: Nat
   goalId: Nat := 0
-  tactic: String
+  -- One of the fields here must be filled
+  tactic?: Option String := .none
+  expr?: Option String := .none
   deriving Lean.FromJson
 structure GoalTacticResult where
   -- The next goal state id. Existence of this field shows success
diff --git a/Test/Integration.lean b/Test/Integration.lean
index b7a5e62..39f145e 100644
--- a/Test/Integration.lean
+++ b/Test/Integration.lean
@@ -82,12 +82,31 @@ def test_malformed_command : IO LSpec.TestSeq :=
        error := "command", desc := s!"Unable to parse json: Pantograph.Protocol.ExprEcho.expr: String expected"}:
       Protocol.InteractionError))
   ]
+def test_tactic : IO LSpec.TestSeq :=
+  let goal: Protocol.Goal := {
+    target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" },
+    vars := #[{ name := "_uniq 9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
+  }
+  subroutine_runner [
+    subroutine_step "goal.start"
+      [("expr", .str "∀ (p q: Prop), p ∨ q → q ∨ p")]
+     (Lean.toJson ({stateId := 0}:
+      Protocol.GoalStartResult)),
+    subroutine_step "goal.tactic"
+      [("stateId", .num 0), ("goalId", .num 0), ("tactic", .str "intro x")]
+     (Lean.toJson ({
+       nextStateId? := .some 1,
+       goals? := #[goal],
+     }:
+      Protocol.GoalTacticResult))
+  ]
 
 def suite: IO LSpec.TestSeq := do
 
   return LSpec.group "Integration" $
     (LSpec.group "Option modify" (← test_option_modify)) ++
-    (LSpec.group "Malformed command" (← test_malformed_command))
+    (LSpec.group "Malformed command" (← test_malformed_command)) ++
+    (LSpec.group "Tactic" (← test_tactic))
 
 
 end Pantograph.Test.Integration