diff --git a/Pantograph/Frontend/InfoTree.lean b/Pantograph/Frontend/InfoTree.lean index 6fe9370..cbf2b71 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 @@ -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 new file mode 100644 index 0000000..9847d49 --- /dev/null +++ b/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}" diff --git a/lakefile.lean b/lakefile.lean index ddf721a..194fbfc 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 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 {