max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add Compiler.jp trace class

Browse source
This commit is contained in:
Leonardo de Moura 2022-08-17 16:22:09 -07:00
parent f0791559b8
commit d7acf1f844
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Compiler/Main.lean
View file

@ -53,6 +53,7 @@ def compileStage1Impl (declNames : Array Name) : CoreM (Array Decl) := do
checkpoint `init decls { terminalCasesOnly := false }
let decls ← decls.mapM (·.terminalCases)
checkpoint `terminalCases decls
decls.forM fun decl => do trace[Compiler.jp] "{decl.name}: {(← JoinPoints.JoinPointFinder.findJoinPoints decl.value |>.run' {})}"
let decls ← decls.mapM (·.simp)
checkpoint `simp decls
-- Remark: add simplification step here, `cse` is useful after simplification
@ -74,5 +75,6 @@ builtin_initialize
registerTraceClass `Compiler.terminalCases (inherited := true)
registerTraceClass `Compiler.simp (inherited := true)
registerTraceClass `Compiler.cse (inherited := true)
registerTraceClass `Compiler.jp
end Lean.Compiler