From 989130ecd28c5a6e1296f987a91e46e12ea504e4 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Thu, 25 May 2023 13:40:03 -0700
Subject: [PATCH] Add expr.type

---
 Main.lean                | 17 +++++++++++++++++
 Pantograph/Commands.lean |  8 ++++++++
 2 files changed, 25 insertions(+)

diff --git a/Main.lean b/Main.lean
index 1430ec6..9f2d459 100644
--- a/Main.lean
+++ b/Main.lean
@@ -46,6 +46,10 @@ def execute (command: Command): Subroutine Lean.Json := do
     match Lean.fromJson? command.payload with
     | .ok args => inspect args
     | .error x => return errorJson x
+  | "expr.type" =>
+    match Lean.fromJson? command.payload with
+    | .ok args => expr_type args
+    | .error x => return errorJson x
   | "proof.start" =>
     match Lean.fromJson? command.payload with
     | .ok args => proof_start args
@@ -90,6 +94,19 @@ def execute (command: Command): Subroutine Lean.Json := do
         boundExpr? := boundExpr?,
         module? := module?
       }: InspectResult)
+  expr_type (args: ExprType): Subroutine Lean.Json := do
+    let env ← Lean.MonadEnv.getEnv
+    match syntax_from_str env args.expr with
+    | .error str => return errorI "parsing" str
+    | .ok syn => do
+      match (← syntax_to_expr syn) with
+      | .error str => return errorI "elab" str
+      | .ok expr => do
+        try
+          let format ← Lean.Meta.ppExpr (← Lean.Meta.inferType expr)
+          return Lean.toJson <| ({ type := toString format }: ExprTypeResult)
+        catch exception =>
+          return errorI "typing" (← exception.toMessageData.toString)
   proof_start (args: ProofStart): Subroutine Lean.Json := do
     let state ← get
     let env ← Lean.MonadEnv.getEnv
diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean
index 751510a..d3b3f60 100644
--- a/Pantograph/Commands.lean
+++ b/Pantograph/Commands.lean
@@ -42,6 +42,14 @@ structure InspectResult where
   module?: Option String
   deriving Lean.ToJson
 
+-- Get the type of an expression
+structure ExprType where
+  expr: String
+  deriving Lean.FromJson
+structure ExprTypeResult where
+  type: String
+  deriving Lean.ToJson
+
 structure ProofStart where
   name: Option String     -- Identifier of the proof
   -- Only one of the fields below may be populated.