From 9a41680ec969fefcf6e347de3a4e49d07f4ebcd6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 15 Oct 2022 19:28:59 -0700 Subject: [PATCH] feat: add `Probe.getJps` --- src/Lean/Compiler/LCNF/Probing.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/Lean/Compiler/LCNF/Probing.lean b/src/Lean/Compiler/LCNF/Probing.lean index 77dd780efe..4060705b1b 100644 --- a/src/Lean/Compiler/LCNF/Probing.lean +++ b/src/Lean/Compiler/LCNF/Probing.lean @@ -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