From d7001c1b28b2f693ba0a4fb0c9f0533e267104af Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 24 Jun 2025 15:11:51 -0700
Subject: [PATCH 1/3] chore: Tomogram stub

---
 Tomogram.lean | 3 +++
 lakefile.lean | 8 ++++++++
 2 files changed, 11 insertions(+)
 create mode 100644 Tomogram.lean

diff --git a/Tomogram.lean b/Tomogram.lean
new file mode 100644
index 0000000..3936e71
--- /dev/null
+++ b/Tomogram.lean
@@ -0,0 +1,3 @@
+
+def main : IO Unit := do
+  IO.println "tomogram stub"
diff --git a/lakefile.lean b/lakefile.lean
index ddf721a..5cfaf87 100644
--- a/lakefile.lean
+++ b/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 tomogram {
+  root := `Tomogram
+  -- Solves the native symbol not found problem
+  supportInterpreter := true
+}
+
 require LSpec from git
   "https://github.com/argumentcomputer/LSpec.git" @ "a6652a48b5c67b0d8dd3930fad6390a97d127e8d"
 lean_lib Test {
-- 
2.44.1


From 1a9e4500662318773d80e0e6845bc9e5ea3a5921 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 24 Jun 2025 15:23:59 -0700
Subject: [PATCH 2/3] refactor: Rename `tomogram` to `tomograph`

---
 Tomogram.lean  | 3 ---
 Tomograph.lean | 5 +++++
 lakefile.lean  | 4 ++--
 3 files changed, 7 insertions(+), 5 deletions(-)
 delete mode 100644 Tomogram.lean
 create mode 100644 Tomograph.lean

diff --git a/Tomogram.lean b/Tomogram.lean
deleted file mode 100644
index 3936e71..0000000
--- a/Tomogram.lean
+++ /dev/null
@@ -1,3 +0,0 @@
-
-def main : IO Unit := do
-  IO.println "tomogram stub"
diff --git a/Tomograph.lean b/Tomograph.lean
new file mode 100644
index 0000000..0878b36
--- /dev/null
+++ b/Tomograph.lean
@@ -0,0 +1,5 @@
+
+
+def main (args : List String) : IO Unit := do
+  let command :: args := args | IO.eprintln "Must supply a command"
+  IO.println s!"{command}"
diff --git a/lakefile.lean b/lakefile.lean
index 5cfaf87..194fbfc 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -19,8 +19,8 @@ lean_exe repl {
 }
 
 @[default_target]
-lean_exe tomogram {
-  root := `Tomogram
+lean_exe tomograph {
+  root := `Tomograph
   -- Solves the native symbol not found problem
   supportInterpreter := true
 }
-- 
2.44.1


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 3/3] 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}"
-- 
2.44.1