Pantograph.lean

@@ -103,18 +103,25 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
       }
   env_add (args: Protocol.EnvAdd): MainM (CR Protocol.EnvAddResult) := do
     let env ← Lean.MonadEnv.getEnv
-    let type ← match syntax_from_str env args.type with
+    let tv?: Except String (Lean.Expr × Lean.Expr) ← runTermElabM (do
-      | .ok syn => do
+        let type ← match syntax_from_str env args.type with
-        match ← (syntax_to_expr syn |> runTermElabM) with
+          | .ok syn => do
-        | .error e => return .error $ errorExpr e
+            match ← syntax_to_expr syn with
-        | .ok expr => pure expr
+            | .error e => return .error e
-      | .error e => return .error $ errorExpr e
+            | .ok expr => pure expr
-    let value ← match syntax_from_str env args.value with
+          | .error e => return .error e
-      | .ok syn => do
+        let value ← match syntax_from_str env args.value with
-        try
+          | .ok syn => do
-          let expr ← Lean.Elab.Term.elabTerm (stx := syn) (expectedType? := .some type) |> runTermElabM
+            try
-          pure $ expr
+              let expr ← Lean.Elab.Term.elabTerm (stx := syn) (expectedType? := .some type)
-        catch ex => return .error $ errorExpr (← ex.toMessageData.toString)
+              let expr ← Lean.instantiateMVars expr
+              pure $ expr
+            catch ex => return .error (← ex.toMessageData.toString)
+          | .error e => return .error e
+        pure $ .ok (type, value)
+      )
+    let (type, value) ← match tv? with
+      | .ok t => pure t
       | .error e => return .error $ errorExpr e
     let constant := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx
       (name := args.name.toName)
@@ -135,9 +142,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
   expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do
     let state ← get
     let env ← Lean.MonadEnv.getEnv
-    match syntax_from_str env args.expr with
+    let syn ← match syntax_from_str env args.expr with
-    | .error str => return .error $ errorI "parsing" str
+      | .error str => return .error $ errorI "parsing" str
-    | .ok syn => runTermElabM do
+      | .ok syn => pure syn
+    runTermElabM (do
       match ← syntax_to_expr syn with
       | .error str => return .error $ errorI "elab" str
       | .ok expr => do
@@ -148,7 +156,7 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
               expr := (← serialize_expression (options := state.options) expr)
           }
         catch exception =>
-          return .error $ errorI "typing" (← exception.toMessageData.toString)
+          return .error $ errorI "typing" (← exception.toMessageData.toString))
   options_set (args: Protocol.OptionsSet): MainM (CR Protocol.OptionsSetResult) := do
     let state ← get
     let options := state.options

Test/Integration.lean

@@ -112,12 +112,33 @@ def test_tactic : IO LSpec.TestSeq :=
       Protocol.GoalTacticResult))
   ]
 
+def test_env : IO LSpec.TestSeq :=
+  let name := "Pantograph.Mystery"
+  subroutine_runner [
+    subroutine_step "env.add"
+      [
+        ("name", .str name),
+        ("type", .str "Prop → Prop → Prop"),
+        ("value", .str "λ (a b: Prop) => Or a b"),
+        ("isTheorem", .bool false)
+      ]
+     (Lean.toJson ({}: Protocol.EnvAddResult)),
+    subroutine_step "env.inspect"
+      [("name", .str name)]
+     (Lean.toJson ({
+       value? := .some { pp? := .some "fun a b => a ∨ b" },
+       type := { pp? := .some "Prop → Prop → Prop" },
+     }:
+      Protocol.EnvInspectResult))
+  ]
+
 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 "Tactic" (← test_tactic))
+    (LSpec.group "Tactic" (← test_tactic)) ++
+    (LSpec.group "Env" (← test_env))
 
 
 end Pantograph.Test.Integration