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}"