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

feat: add Probe.getJps

Browse source
This commit is contained in:
Leonardo de Moura 2022-10-15 19:28:59 -07:00
parent dac4e6f214
commit 9a41680ec9
1 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/Lean/Compiler/LCNF/Probing.lean
View file

@ -45,6 +45,21 @@ where
start (decls : Array Decl) : StateRefT (Array Expr) CompilerM Unit :=
decls.forM (fun decl => decl.forEachExpr go skipTypes)
partial def getJps : Probe Decl FunDecl := fun decls => do
let (_, res) ← start decls |>.run #[]
return res
where
go (code : Code) : StateRefT (Array FunDecl) CompilerM Unit := do
match code with
| .let _ k => go k
| .fun decl k => go decl.value; go k
| .jp decl k => modify (·.push decl); go decl.value; go k
| .cases cs => cs.alts.forM (go ·.getCode)
| .jmp .. | .return .. | .unreach .. => return ()
start (decls : Array Decl) : StateRefT (Array FunDecl) CompilerM Unit :=
decls.forM fun decl => go decl.value
partial def filterByLet (f : LetDecl → CompilerM Bool) : Probe Decl Decl :=
filter (fun decl => go decl.value)
where