From d7001c1b28b2f693ba0a4fb0c9f0533e267104af Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 24 Jun 2025 15:11:51 -0700 Subject: [PATCH 1/6] 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 { From 1a9e4500662318773d80e0e6845bc9e5ea3a5921 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 24 Jun 2025 15:23:59 -0700 Subject: [PATCH 2/6] 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 } From 53ea808c90f35a4ecf5a9c7059a015c5a70098f1 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 24 Jun 2025 15:31:46 -0700 Subject: [PATCH 3/6] 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}" From ec78324f9f605f44a14410f65f8fed5c9ac0b757 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 2 Jul 2025 14:32:24 -0700 Subject: [PATCH 4/6] feat(repl): Improve tomograph's info --- Pantograph/Frontend/InfoTree.lean | 12 ++++++------ Tomograph.lean | 23 +++++++++++++++-------- 2 files changed, 21 insertions(+), 14 deletions(-) diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean index cf3f7eb..cbf2b71 100644 --- a/Pantograph/Frontend/InfoTree.lean +++ b/Pantograph/Frontend/InfoTree.lean @@ -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]" diff --git a/Tomograph.lean b/Tomograph.lean index ca0c21b..b23ec70 100644 --- a/Tomograph.lean +++ b/Tomograph.lean @@ -1,29 +1,36 @@ +/- A tool for analysing Lean source code. -/ import Pantograph.Frontend open Lean namespace Pantograph -def fail (s : String) : IO Unit := do +def fail (s : String) : IO UInt32 := do IO.eprintln s + return 2 -def dissect (args: List String): IO Unit := do +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 - for tree in step.trees do - IO.println s!"{← tree.toString}" + IO.println s!"🐈 {step.stx.getKind.toString}" + for (tree, i) in step.trees.zipIdx do + IO.println s!"🌲[{i}] {← tree.toString}" let (_, _) ← frontendM.run context |>.run state - return () + return 0 end Pantograph open Pantograph -def main (args : List String) : IO Unit := do - let command :: args := args | IO.eprintln "Must supply a command" +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 match command with | "dissect" => dissect args - | _ => IO.eprintln s!"Unknown command {command}" + | _ => fail s!"Unknown command {command}" From 48046b8b5a522e1cb7e7e234c7e2b6f127c4142d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 2 Jul 2025 15:13:43 -0700 Subject: [PATCH 5/6] fix(tomograph): Import search directory --- Tomograph.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/Tomograph.lean b/Tomograph.lean index b23ec70..26db934 100644 --- a/Tomograph.lean +++ b/Tomograph.lean @@ -1,5 +1,6 @@ /- A tool for analysing Lean source code. -/ import Pantograph.Frontend +import Pantograph.Library open Lean @@ -18,6 +19,8 @@ def dissect (args: List String): IO UInt32 := 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 @@ -31,6 +34,8 @@ def help : IO UInt32 := do 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}" From c1c7848bca0fbfec6c1165da4a5ad1be776ed874 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 2 Jul 2025 15:18:02 -0700 Subject: [PATCH 6/6] chore: Format code --- Tomograph.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Tomograph.lean b/Tomograph.lean index 26db934..9847d49 100644 --- a/Tomograph.lean +++ b/Tomograph.lean @@ -10,7 +10,7 @@ def fail (s : String) : IO UInt32 := do IO.eprintln s return 2 -def dissect (args: List String): IO UInt32 := do +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) {}