Pantograph.lean

@@ -71,10 +71,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     Environment.addDecl args
   expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
     let state ← get
-    let expr ← match ← exprParse args.expr with
+    exprEcho args.expr state.options
-      | .ok expr => pure $ expr
-      | .error e => return .error e
-    exprPrint expr state.options
   options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
     let state ← get
     let options := state.options
@@ -96,13 +93,11 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
     let state ← get
     let env ← Lean.MonadEnv.getEnv
     let expr?: Except _ GoalState ← runTermElabM (match args.expr, args.copyFrom with
-      | .some expr, .none =>
+      | .some expr, .none => do
-        (match syntax_from_str env expr with
+        let expr ← match ← exprParse expr with
-        | .error str => return .error <| errorI "parsing" str
+          | .error e => return .error e
-        | .ok syn => do
+          | .ok expr => pure $ expr
-          (match ← syntax_to_expr syn with
+        return .ok $ ← GoalState.create expr
-          | .error str => return .error <| errorI "elab" str
-          | .ok expr => return .ok (← GoalState.create expr)))
       | .none, .some copyFrom =>
         (match env.find? <| copyFrom.toName with
         | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"

Pantograph/Library.lean

@@ -80,6 +80,23 @@ def createCoreState (imports: Array String): IO Lean.Core.State := do
 def envCatalog: Lean.CoreM Protocol.EnvCatalogResult :=
   Environment.catalog ({}: Protocol.EnvCatalog)
 
+@[export pantograph_mk_options]
+def mkOptions
+  (printJsonPretty: Bool)
+  (printExprPretty: Bool)
+  (printExprAST: Bool)
+  (noRepeat: Bool)
+  (printAuxDecls: Bool)
+  (printImplementationDetailHyps: Bool)
+  : Protocol.Options := {
+    printJsonPretty,
+    printExprPretty,
+    printExprAST,
+    noRepeat,
+    printAuxDecls,
+    printImplementationDetailHyps,
+  }
+
 @[export pantograph_env_inspect_m]
 def envInspect (name: String) (value: Bool) (dependency: Bool) (options: Protocol.Options):
     Lean.CoreM (Protocol.CR Protocol.EnvInspectResult) :=
@@ -92,21 +109,23 @@ 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_m]
+/-- This must be a TermElabM since the parsed expr contains extra information -/
-def exprParse (s: String): Lean.CoreM (Protocol.CR Lean.Expr) := do
+def exprParse (s: String): Lean.Elab.TermElabM (Protocol.CR Lean.Expr) := do
   let env ← Lean.MonadEnv.getEnv
   let syn ← match syntax_from_str env s with
     | .error str => return .error $ errorI "parsing" str
     | .ok syn => pure syn
-  runTermElabM (do
   match ← syntax_to_expr syn with
   | .error str => return .error $ errorI "elab" str
-    | .ok expr => return .ok expr)
+  | .ok expr => return .ok expr
 
-@[export pantograph_expr_print_m]
+@[export pantograph_expr_echo_m]
-def exprPrint (expr: Lean.Expr) (options: @&Protocol.Options):
+def exprEcho (expr: String) (options: @&Protocol.Options):
     Lean.CoreM (Protocol.CR Protocol.ExprEchoResult) := do
-  let termElabM: Lean.Elab.TermElabM _ :=
+  let termElabM: Lean.Elab.TermElabM _ := do
+    let expr ← match ← exprParse expr with
+      | .error e => return .error e
+      | .ok expr => pure expr
     try
       let type ← Lean.Meta.inferType expr
       return .ok {
@@ -117,9 +136,14 @@ def exprPrint (expr: Lean.Expr) (options: @&Protocol.Options):
       return .error $ errorI "typing" (← exception.toMessageData.toString)
   runTermElabM termElabM
 
-@[export pantograph_goal_start_m]
+@[export pantograph_goal_start_expr_m]
-def goalStart (expr: Lean.Expr): Lean.CoreM GoalState :=
+def goalStartExpr (expr: String): Lean.CoreM (Protocol.CR GoalState) :=
-  runTermElabM (GoalState.create expr)
+  let termElabM: Lean.Elab.TermElabM _ := do
+    let expr ← match ← exprParse expr with
+      | .error e => return .error e
+      | .ok expr => pure $ expr
+    return .ok $ ← GoalState.create expr
+  runTermElabM termElabM
 
 @[export pantograph_goal_tactic_m]
 def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): Lean.CoreM TacticResult :=