feat: add more detailed elaboration info tree

Analyzer/Output.lean

@@ -65,6 +65,8 @@ deriving instance ToJson for Variable, Goal
 deriving instance ToJson for LineInfo
 
 section
+deriving instance ToJson for SpecialValue
+
 local instance : ToJson Syntax where
   toJson x := json% {
     kind: $(x.getKind),
@@ -73,6 +75,16 @@ local instance : ToJson Syntax where
     str: $(toString x)
   }
 deriving instance ToJson for TacticElabInfo, TermElabInfo, ElaborationInfo
+
+private partial def go : ElaborationTree → Json
+  | .mk info ref children => json% {
+    info: $(info),
+    ref: $(ref),
+    children: $(children.map go)
+  }
+
+instance : ToJson ElaborationTree where
+  toJson := go
 end
 
 deriving instance ToJson for SourceInfo, Syntax.Preresolved, Syntax

Analyzer/Process/Elaboration.lean

@@ -87,35 +87,53 @@ def getTacticInfo (ci : ContextInfo) (ti : TacticInfo) : IO TacticElabInfo := do
       return do return .mergeObj (← extra) (← dependencies.find? mvar)
 
     pure {
-      tactic := ti.stx,
       references := references ti.stx,
       before := ← Goal.fromTactic (extraFun := getUsedInfo') |>.runWithInfoBefore ci ti,
       after := ← Goal.fromTactic (extraFun := getUsedInfo) |>.runWithInfoAfter ci ti,
       extra? := if extra.isNull then none else extra,
     : TacticElabInfo}
 
+def setOptions (opts : Lean.Options) : Lean.Options :=
+  opts
+    |>.set pp.fieldNotation.name false
+    |>.set pp.fullNames.name true
+
+def getSpecialValue : Expr → Option SpecialValue
+  | .const name .. => some <| .const name
+  | .fvar id .. => some <| .fvar id
+  | _ => none
+
 def getTermInfo (ci : ContextInfo) (ti : TermInfo) : IO TermElabInfo :=
-  ti.runMetaM ci do pure {
-    term := ti.stx,
-    context := ← Goal.printContext,
+  ti.runMetaM ci <| withOptions setOptions do pure {
+    context := ← Goal.printContext
     type := (← ppExpr (← inferType ti.expr)).pretty
     expectedType := ← ti.expectedType?.mapM fun type => do pure (← ppExpr type).pretty
     value := (← ppExpr ti.expr).pretty
+    special? := getSpecialValue ti.expr
   }
 
 
 def onLoad : CommandElabM Unit :=
   enableInfoTree
 
-def getResult : CommandElabM (Array ElaborationInfo) := do
+def getResult : CommandElabM (Array ElaborationTree) := do
   let trees := (← getInfoTrees).toArray
   trees.filterMapM fun tree => do
     tree.visitM (postNode := fun ci info _ children => do
-      let children' := children.filterMap id |>.toArray
-      match info with
-      | .ofTacticInfo ti => .tactic (children := children') <$> getTacticInfo ci ti
-      | .ofTermInfo ti => .term (children := children') <$> getTermInfo ci ti
-      | _ => pure <| .other children'
+      let info' ← match info with
+      | .ofTacticInfo ti => .tactic <$> getTacticInfo ci ti
+      | .ofTermInfo ti => .term <$> getTermInfo ci ti
+      | .ofCommandInfo _ => pure <| .simple "command"
+      | .ofMacroExpansionInfo _ => pure <| .simple "macro"
+      | .ofFieldInfo _ => pure <| .simple "field"
+      | .ofOptionInfo _ => pure <| .simple "option"
+      | .ofCompletionInfo _ => pure <| .simple "completion"
+      | .ofUserWidgetInfo _ => pure <| .simple "uw"
+      | .ofCustomInfo _ => pure <| .simple "custom"
+      | .ofFVarAliasInfo _ => pure <| .simple "alias"
+      | .ofFieldRedeclInfo _ => pure <| .simple "redecl"
+      | .ofOmissionInfo _ => pure <| .simple "omission"
+      pure <| .mk info' info.stx <| children.filterMap id |>.toArray
     )
 
 

Analyzer/Types.lean

@@ -78,24 +78,30 @@ structure Goal where
   extra? : Option Json := none
 
 structure TacticElabInfo where
-  tactic : Syntax
   /-- Names referenced in this tactic, including constants and local hypotheses. -/
   references : HashSet Name
   before : Array Goal
   after : Array Goal
   extra? : Option Json := none
 
+inductive SpecialValue where
+  | const : Name → SpecialValue
+  | fvar : FVarId → SpecialValue
+
 structure TermElabInfo where
-  term : Syntax
   context : Array Variable
   type : String
   expectedType : Option String
   value : String
+  special? : Option SpecialValue
 
 inductive ElaborationInfo where
-  | term (info : TermElabInfo) (children : Array ElaborationInfo) : ElaborationInfo
-  | tactic (info : TacticElabInfo) (children : Array ElaborationInfo) : ElaborationInfo
-  | other (children : Array ElaborationInfo) : ElaborationInfo
+  | term (info : TermElabInfo) : ElaborationInfo
+  | tactic (info : TacticElabInfo) : ElaborationInfo
+  | simple (kind : String) : ElaborationInfo
+
+inductive ElaborationTree where
+  | mk (info : ElaborationInfo) (ref : Syntax) (children : Array ElaborationTree) : ElaborationTree
 
 structure LineInfo where
   start : String.Pos

Example.lean

@@ -32,10 +32,12 @@ theorem rcases_test {x : Nat} (h : ∃ k, x = 2 * k) : ∃ k, x + 2 = 2 * k := b
 theorem comp_test (x : Nat) (h : ∃ k, x = 2 * k) : ∃ k, x + 4 = 2 * k :=
   rcases_test (rcases_test h)
 
-/-- pow_succ x n = pow x n.succ -/
-def pow_succ [Mul α] (x : α) : Nat → α
+/-- pow' x n = x ^ (n + 1) -/
+def pow' [Mul α] (x : α) : Nat → α
   | .zero => x
-  | .succ n => pow_succ x n * x
+  | .succ n => pow' x n * x
+
+theorem pow'_succ [Mul α] (x : α) (n : Nat) : pow' x n.succ = (pow' x n) * x := rfl
 
 structure FermatTriple (k : Nat) : Type where
   x : Nat