Compiling a definition to LCNF

Stream: metaprogramming / tactics

[Dylan Ede]

I have this command that allows me to see what LCNF a definition compiles to and how each pass affects it:

set_option trace.Compiler true
set_option trace.Compiler.result true
open Lean Elab Compiler in
elab "#compile " id:ident : command => Command.liftTermElabM do
  let name <- realizeGlobalConstNoOverloadWithInfo id
  let compiled <- LCNF.compile #[name]

This works, but for some reason it seems like inlining is not applied at all. For example,

@[always_inline]
def bar : Nat -> Nat := id

def foo : Nat -> Nat := bar

#compile foo

produces

def foo a.1 : Nat :=
  let _x.2 := bar a.1;
  return _x.2

I would have expected bar to be inlined. I can see from the trace that the simp pass is being executed, which is where I think inlining is meant to occur, so I'm not sure what I'm doing wrong. Note that I have tried including bar in the list of names to compile, but this does not affect the result. Any ideas what I'm doing wrong?

[Thomas Murrills]

This response is a bit late, so you might have figured this out by now, but note that inlining works as long as you call LCNF.compile separately on #[`bar] first!

I guess LCNF.compile #[name1, name2] doesn’t take into account the result of compiling name1 when compiling name2. I’m not sure if this is intentional or not. (Parallelism, maybe?)