File size: 1,238 Bytes
0115dcf | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 | /- 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: Frontend.FrontendM _ :=
Frontend.mapCompilationSteps Ξ» step => do
IO.println s!"{step.stx}"
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 {} |>.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}"
|