From 53ea808c90f35a4ecf5a9c7059a015c5a70098f1 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 24 Jun 2025 15:31:46 -0700
Subject: [PATCH] feat(frontend): Dissect syntax tree

---
 Pantograph/Frontend/InfoTree.lean |  2 +-
 Tomograph.lean                    | 26 +++++++++++++++++++++++++-
 2 files changed, 26 insertions(+), 2 deletions(-)

diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean
index 6fe9370..cf3f7eb 100644
--- a/Pantograph/Frontend/InfoTree.lean
+++ b/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
diff --git a/Tomograph.lean b/Tomograph.lean
index 0878b36..ca0c21b 100644
--- a/Tomograph.lean
+++ b/Tomograph.lean
@@ -1,5 +1,29 @@
+import Pantograph.Frontend
 
+open Lean
+
+namespace Pantograph
+
+def fail (s : String) : IO Unit := do
+  IO.eprintln s
+
+def dissect (args: List String): IO Unit := 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
+      for tree in step.trees do
+        IO.println s!"{← tree.toString}"
+  let (_, _) ← frontendM.run context |>.run state
+  return ()
+
+end Pantograph
+
+open Pantograph
 
 def main (args : List String) : IO Unit := do
   let command :: args := args | IO.eprintln "Must supply a command"
-  IO.println s!"{command}"
+  match command with
+  | "dissect" => dissect args
+  | _ => IO.eprintln s!"Unknown command {command}"