Pantograph.lean

@@ -49,6 +49,8 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
       errorCommand s!"Unknown command {cmd}"
     return Lean.toJson error
   where
+  errorCommand := errorI "command"
+  errorIndex := errorI "index"
   -- Command Functions
   reset (_: Protocol.Reset): MainM (CR Protocol.StatResult) := do
     let state ← get
@@ -93,14 +95,11 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   goal_start (args: Protocol.GoalStart): MainM (CR Protocol.GoalStartResult) := do
     let state ← get
     let env ← Lean.MonadEnv.getEnv
-    let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
-      | .some expr, .none =>
-        (match syntax_from_str env expr with
-        | .error str => return .error <| errorI "parsing" str
-        | .ok syn => do
-          (match ← syntax_to_expr syn with
-          | .error str => return .error <| errorI "elab" str
-          | .ok expr => return .ok (← GoalState.create expr)))
+    let expr?: Except Protocol.InteractionError GoalState ← runTermElabM (match args.expr, args.copyFrom with
+      | .some expr, .none => do
+          match ← exprParse expr with
+          | .ok expr => return .ok (← GoalState.create expr)
+          | .error e => return .error e
       | .none, .some copyFrom =>
         (match env.find? <| copyFrom.toName with
         | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
@@ -123,9 +122,9 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     | .some goalState => do
       let nextGoalState?: Except _ GoalState ← match args.tactic?, args.expr? with
         | .some tactic, .none => do
-          pure ( Except.ok (← runTermElabM <| GoalState.execute goalState args.goalId tactic))
+          pure ( Except.ok (← goalTactic goalState args.goalId tactic))
         | .none, .some expr => do
-          pure ( Except.ok (← runTermElabM <| GoalState.tryAssign goalState args.goalId expr))
+          pure ( Except.ok (← goalTryAssign 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
@@ -157,8 +156,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           | .none => return .error $ errorIndex s!"Invalid state index {branchId}"
           | .some branch => pure $ target.continue branch
         | .none, .some goals =>
-          let goals := goals.map (λ name => { name := name.toName })
-          pure $ target.resume goals
+          pure $ goalResume target goals
         | _, _ => return .error <| errorI "arguments" "Exactly one of {branch, goals} must be supplied"
       match nextState? with
       | .error error => return .error <| errorI "structure" error
@@ -168,7 +166,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
           goalStates := state.goalStates.insert nextStateId nextGoalState,
           nextId := state.nextId + 1
         }
-        let goals ← nextGoalState.serializeGoals (parent := .none) (options := state.options) |>.run'
+        let goals ← goalSerialize nextGoalState (options := state.options)
         return .ok {
           nextStateId,
           goals,

Pantograph/Library.lean

@@ -1,6 +1,7 @@
 import Pantograph.Environment
 import Pantograph.Goal
 import Pantograph.Protocol
+import Pantograph.Serial
 import Pantograph.Version
 import Lean
 
@@ -44,11 +45,6 @@ def runTermElabM { α } (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α :=
   }) |>.run'
 
 def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }
-def errorCommand := errorI "command"
-def errorIndex := errorI "index"
-
-@[export pantograph_version]
-def pantographVersion: String := version
 
 /-- Adds the given paths to Lean package search path -/
 @[export pantograph_init_search]
@@ -82,30 +78,27 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do
 
 /-- Execute a `CoreM` monad -/
 @[export pantograph_exec_core]
-def execCore {α} (context: Lean.Core.Context) (state: Lean.Core.State) (coreM: Lean.CoreM α): IO (α × Lean.Core.State) :=
+def execCore {α} (context: Lean.Core.Context) (state: Lean.Core.State) (coreM: Lean.CoreM α):
+    IO (α × Lean.Core.State) :=
   coreM.toIO context state
 
-@[export pantograph_env_catalog]
+@[export pantograph_env_catalog_m]
 def envCatalog: Lean.CoreM Protocol.EnvCatalogResult :=
   Environment.catalog ({}: Protocol.EnvCatalog)
 
-@[export pantograph_env_inspect]
-def envInspect (cc: Lean.Core.Context) (cs: Lean.Core.State)
-    (name: String) (value: Bool) (dependency: Bool) (options: Protocol.Options): IO (Protocol.CR Protocol.EnvInspectResult) := do
-  let coreM: Lean.CoreM _ := Environment.inspect ({
+@[export pantograph_env_inspect_m]
+def envInspect (name: String) (value: Bool) (dependency: Bool) (options: Protocol.Options):
+    Lean.CoreM (Protocol.CR Protocol.EnvInspectResult) :=
+  Environment.inspect ({
     name, value? := .some value, dependency?:= .some dependency
   }: Protocol.EnvInspect) options
-  let (result, _) ← coreM.toIO cc cs
-  return result
 
-@[export pantograph_env_add]
-def envAdd (cc: Lean.Core.Context) (cs: Lean.Core.State)
-  (name: String) (type: String) (value: String) (isTheorem: Bool): IO (Protocol.CR Protocol.EnvAddResult) := do
-  let coreM: Lean.CoreM _ := Environment.addDecl { name, type, value, isTheorem }
-  let (result, _) ← coreM.toIO cc cs
-  return result
+@[export pantograph_env_add_m]
+def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
+    Lean.CoreM (Protocol.CR Protocol.EnvAddResult) :=
+  Environment.addDecl { name, type, value, isTheorem }
 
-@[export pantograph_expr_parse]
+@[export pantograph_expr_parse_m]
 def exprParse (s: String): Lean.CoreM (Protocol.CR Lean.Expr) := do
   let env ← Lean.MonadEnv.getEnv
   let syn ← match syntax_from_str env s with
@@ -116,8 +109,9 @@ def exprParse (s: String): Lean.CoreM (Protocol.CR Lean.Expr) := do
     | .error str => return .error $ errorI "elab" str
     | .ok expr => return .ok expr)
 
-@[export pantograph_expr_print]
-def exprPrint (expr: Lean.Expr) (options: @&Protocol.Options): Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do
+@[export pantograph_expr_print_m]
+def exprPrint (expr: Lean.Expr) (options: @&Protocol.Options):
+    Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do
   let termElabM: Lean.Elab.TermElabM _ :=
       try
         let type ← Lean.Meta.inferType expr
@@ -129,8 +123,30 @@ def exprPrint (expr: Lean.Expr) (options: @&Protocol.Options): Lean.CoreM (Proto
         return .error $ errorI "typing" (← exception.toMessageData.toString)
   runTermElabM termElabM
 
-@[export pantograph_goal_start]
+@[export pantograph_goal_start_m]
 def goalStart (expr: Lean.Expr): Lean.CoreM GoalState :=
   runTermElabM (GoalState.create expr)
 
+@[export pantograph_goal_tactic_m]
+def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult :=
+  runTermElabM <| GoalState.execute state goalId tactic
+
+@[export pantograph_goal_try_assign_m]
+def goalTryAssign (state: GoalState) (goalId: Nat) (expr: String): Lean.CoreM TacticResult :=
+  runTermElabM <| GoalState.tryAssign state goalId expr
+
+@[export pantograph_goal_continue]
+def goalContinue (target: GoalState) (branch: GoalState): Except String GoalState :=
+  target.continue branch
+
+@[export pantograph_goal_resume]
+def goalResume (target: GoalState) (goals: Array String): Except String GoalState :=
+  target.resume (goals.map (λ n => { name := n.toName }) |>.toList)
+
+@[export pantograph_goal_serialize_m]
+def goalSerialize (state: GoalState) (options: Protocol.Options): Lean.CoreM (Array Protocol.Goal) :=
+  runMetaM <| state.serializeGoals (parent := .none) options
+
+
+
 end Pantograph

Pantograph/Protocol.lean

@@ -221,7 +221,7 @@ structure GoalContinue where
   -- The state which is an ancestor of `target` where goals will be extracted from
   branch?: Option Nat := .none
   -- Or, the particular goals that should be brought back into scope
-  goals?: Option (List String) := .none
+  goals?: Option (Array String) := .none
   deriving Lean.FromJson
 structure GoalContinueResult where
   nextStateId: Nat

Pantograph/Version.lean

@@ -1,5 +1,6 @@
 namespace Pantograph
 
+@[export pantograph_version]
 def version := "0.2.12-alpha"
 
 end Pantograph