Add position info to declTypes

Author: sorgfresser

REPL/JSON.lean

@@ -117,6 +117,20 @@ def Tactic.of (goals tactic : String) (pos endPos : Lean.Position) (proofState :
     proofState,
     usedConstants }
 
+structure DeclType where
+  pos: Pos
+  endPos : Pos
+  type: String
+  pp: String
+deriving ToJson, FromJson
+
+/-- Construct the JSON representation of a Declaration type. -/
+def DeclType.of (type pp : String) (pos endPos : Lean.Position) : DeclType :=
+  { pos := ⟨pos.line, pos.column⟩,
+    endPos := ⟨endPos.line, endPos.column⟩,
+    type,
+    pp }
+
 /--
 A response to a Lean command.
 `env` can be used in later calls, to build on the stored environment.
@@ -126,7 +140,7 @@ structure CommandResponse where
   messages : List Message := []
   sorries : List Sorry := []
   tactics : List Tactic := []
-  decls: List String := []
+  decls: List DeclType := []
   infotree : Option Json := none
 deriving FromJson
 

REPL/Lean/InfoTree.lean

@@ -272,6 +272,14 @@ def tactics (t : InfoTree) : List (ContextInfo × Syntax × List MVarId × List
       range.snd,
       i.getUsedConstantsAsSet.toArray )
 
+def declType (t : InfoTree) : Option (ContextInfo × Expr × Syntax × LocalContext × Position × Position) :=
+  let terms: List (TermInfo × ContextInfo) := t.findTermNodes
+  match terms.getLast? with
+  | some ⟨i, ctx⟩ =>
+    let range := stxRange ctx.fileMap i.stx
+    (ctx, i.expr, i.stx, i.lctx, range.fst, range.snd)
+  | _ => none
+
 def rootGoals (t : InfoTree) : List (ContextInfo × List MVarId × Position) :=
   t.findRootGoals.map fun ⟨i, ctx, rootGoals⟩ =>
     let range := stxRange ctx.fileMap i.stx

REPL/Main.lean

@@ -131,15 +131,17 @@ def tactics (trees : List InfoTree) (env? : Option Environment) : M m (List Tact
       return Tactic.of goals tactic pos endPos proofStateId ns
 
 
-def declTypes (trees: List InfoTree) : M m (List String) := do
-  let terms := trees.map InfoTree.findTermNodes
-  let innermost := (fun (t : TermInfo) => do pure (← Meta.ppExpr (← Lean.Meta.inferType t.expr)).pretty')
-  let inner := (fun t : (TermInfo × ContextInfo) => t.snd.runMetaM t.fst.lctx (innermost t.fst))
-  let optional_decls: List String ← terms.mapM fun treeterms => do
-    match treeterms.getLast? with
-    | none => pure ""
-    | some a => inner a
-  pure (optional_decls.filter (fun s => !s.isEmpty))
+def declTypes (trees: List InfoTree) : M m (List DeclType) := do
+  let exprType: Expr → MetaM String := fun (expr: Expr) => do pure (← Meta.ppExpr (← Lean.Meta.inferType expr)).pretty'
+  let treeDecl := (fun t => do
+    let dt := InfoTree.declType t
+    match dt with
+    | some ⟨ctx, expr, stx, lctx, pos, endPos⟩ =>
+      let type := (← ctx.runMetaM lctx (exprType expr))
+      let pp := Format.pretty stx.prettyPrint
+      pure [DeclType.of type pp pos endPos]
+    | _ => pure [])
+  trees.flatMapM treeDecl
 
 def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) := do
   trees.flatMap InfoTree.rootGoals |>.mapM

test/Mathlib/test/decltypenamespace.expected.out

@@ -6,5 +6,9 @@
    "endPos": {"line": 1, "column": 75},
    "data": "Goals accomplished!"}],
  "env": 1,
- "decls": ["∑ k ∈ Nat.properDivisors 198, k = 270"]}
+ "decls":
+ [{"type": "∑ k ∈ Nat.properDivisors 198, k = 270",
+   "pp": "with_namespace",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 22}}]}
 

test/Mathlib/test/decltypeopen.expected.out

@@ -6,5 +6,9 @@
    "endPos": {"line": 1, "column": 75},
    "data": "Goals accomplished!"}],
  "env": 1,
- "decls": ["∑ k ∈ properDivisors 198, k = 270"]}
+ "decls":
+ [{"type": "∑ k ∈ properDivisors 198, k = 270",
+   "pp": "with_namespace",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 22}}]}
 

test/gettype.expected.out

@@ -4,11 +4,29 @@
    "endPos": {"line": 1, "column": 51},
    "data": "Goals accomplished!"}],
  "env": 0,
- "decls": ["∀ (p : Prop), p → p"]}
+ "decls":
+ [{"type": "∀ (p : Prop), p → p",
+   "pp": "show_p",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 14}}]}
 
-{"env": 1, "decls": ["∀ (p : Prop), p → p"]}
+{"env": 1,
+ "decls":
+ [{"type": "∀ (p : Prop), p → p",
+   "pp": "show_q",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 10}}]}
 
-{"env": 2, "decls": ["∀ (p : Prop), p → p", "∀ (q : Prop), q → q"]}
+{"env": 2,
+ "decls":
+ [{"type": "∀ (p : Prop), p → p",
+   "pp": "show_p",
+   "pos": {"line": 1, "column": 4},
+   "endPos": {"line": 1, "column": 10}},
+  {"type": "∀ (q : Prop), q → q",
+   "pp": "show_q",
+   "pos": {"line": 3, "column": 4},
+   "endPos": {"line": 3, "column": 10}}]}
 
 {"messages":
  [{"severity": "warning",
@@ -17,5 +35,13 @@
    "data":
    "unused variable `p`\nnote: this linter can be disabled with `set_option linter.unusedVariables false`"}],
  "env": 3,
- "decls": ["Prop", "∀ (q : Prop), Type → q → q"]}
+ "decls":
+ [{"type": "Prop",
+   "pp": "q",
+   "pos": {"line": 1, "column": 10},
+   "endPos": {"line": 1, "column": 11}},
+  {"type": "∀ (q : Prop), Type → q → q",
+   "pp": "show_q",
+   "pos": {"line": 2, "column": 4},
+   "endPos": {"line": 2, "column": 10}}]}
 

test/gettype.in

@@ -2,6 +2,6 @@
 
 {"cmd": "def show_q (p : Prop) (h : p) : p := h", "declTypes": true}
 
-{"cmd": "def show_q (p : Prop) (h : p) : p := h\n\ndef show_p (q : Prop) (h : q) : q := h", "declTypes": true}
+{"cmd": "def show_p (p : Prop) (h : p) : p := h\n\ndef show_q (q : Prop) (h : q) : q := h", "declTypes": true}
 
 {"cmd": "variable (q : Prop)\ndef show_q (p : Type) (h : q) : q := h", "declTypes": true}