Merge pull request 'feat(frontend): Tomogram' (#220) from frontend/tomogram into dev

Reviewed-on: #220

Pantograph/Frontend/InfoTree.lean

@@ -10,7 +10,7 @@ namespace Lean.Elab
 private def elaboratorToString : Name → String
   | .anonymous => ""
   | n => s!"⟨{n}⟩ "
-private def indent (s : String) : String := "\n".intercalate $ s.splitOn "\n" |>.map ("\t" ++ .)
+private def indent (s : String) : String := "\n".intercalate $ s.splitOn "\n" |>.map ("  " ++ .)
 
 /-- The `Syntax` for a `Lean.Elab.Info`, if there is one. -/
 protected def Info.stx? : Info → Option Syntax
@@ -131,16 +131,16 @@ partial def InfoTree.toString (t : InfoTree) (ctx?: Option Elab.ContextInfo := .
   | .node info children =>
     if let some ctx := ctx? then
       let node : String ← match info with
-      | .ofTermInfo    info => pure s!"[term] {(← info.toString ctx)}"
-      | .ofCommandInfo info => pure s!"[command] {(← info.toString ctx)}"
-      | .ofTacticInfo  info => pure s!"[tactic] {(← info.toString ctx)}"
+      | .ofTermInfo    info => pure s!"[term] {info.stx}"
+      | .ofCommandInfo info => pure s!"[command] {info.stx}"
+      | .ofTacticInfo  info => pure s!"[tactic] {info.stx}"
       | .ofMacroExpansionInfo _ => pure "[macro_exp]"
-      | .ofOptionInfo _ => pure "[option]"
+      | .ofOptionInfo info => pure s!"[option] {info.stx}"
       | .ofFieldInfo _ => pure "[field]"
-      | .ofCompletionInfo _ => pure "[completion]"
+      | .ofCompletionInfo info => pure s!"[completion] {info.stx}"
       | .ofUserWidgetInfo _ => pure "[user_widget]"
       | .ofCustomInfo _ => pure "[custom]"
-      | .ofFVarAliasInfo _ => pure "[fvar]"
+      | .ofFVarAliasInfo _ => pure "[fvar_alias]"
       | .ofFieldRedeclInfo _ => pure "[field_redecl]"
       | .ofChoiceInfo _ => pure "[choice]"
       | .ofPartialTermInfo  _ => pure "[partial_term]"

Tomograph.lean

@@ -0,0 +1,41 @@
+/- A tool for analysing Lean source code. -/
+import Pantograph.Frontend
+import Pantograph.Library
+
+open Lean
+
+namespace Pantograph
+
+def fail (s : String) : IO UInt32 := do
+  IO.eprintln s
+  return 2
+
+def dissect (args : List String) : IO UInt32 := do
+  let fileName :: _args := args | fail s!"Must supply a file name"
+  let file ← IO.FS.readFile fileName
+  let (context, state) ← do Frontend.createContextStateFromFile file fileName (env? := .none) {}
+  let frontendM: Elab.Frontend.FrontendM _ :=
+    Frontend.mapCompilationSteps λ step => do
+      IO.println s!"🐈 {step.stx.getKind.toString}"
+      for (tree, i) in step.trees.zipIdx do
+        IO.println s!"🌲[{i}] {← tree.toString}"
+      for (msg, i) in step.msgs.zipIdx do
+        IO.println s!"🔈[{i}] {← msg.toString}"
+  let (_, _) ← frontendM.run context |>.run state
+  return 0
+
+end Pantograph
+
+open Pantograph
+
+def help : IO UInt32 := do
+  IO.println "Usage: tomograph dissect FILE_NAME"
+  return 1
+
+def main (args : List String) : IO UInt32 := do
+  let command :: args := args | help
+  unsafe do
+    Pantograph.initSearch ""
+  match command with
+  | "dissect" => dissect args
+  | _ => fail s!"Unknown command {command}"

lakefile.lean

@@ -10,6 +10,7 @@ lean_lib Pantograph {
 
 lean_lib Repl {
 }
+
 @[default_target]
 lean_exe repl {
   root := `Main
@@ -17,6 +18,13 @@ lean_exe repl {
   supportInterpreter := true
 }
 
+@[default_target]
+lean_exe tomograph {
+  root := `Tomograph
+  -- Solves the native symbol not found problem
+  supportInterpreter := true
+}
+
 require LSpec from git
   "https://github.com/argumentcomputer/LSpec.git" @ "a6652a48b5c67b0d8dd3930fad6390a97d127e8d"
 lean_lib Test {