Lean equivalent of MACROEXPAND-1?

Stream: lean4

[David Thrane Christiansen]

Common Lisp has a really handy function called MACROEXPAND-1 that performs one step of macro expansion. It's very useful when trying to understand how syntax from a library works. Is there anything like it in Lean? I imagine something like #expand N STX would do the trick, where N is the number of steps of expansion to perform.

What I'd really like to do is to is to write a macro that uses this for a single steps of testing. That is, it'd be great to be able to write

test macro
  do let x <- foo ; f x
  ===>
  foo >>= fun x => f x
end test

that checks that just one step does this. Today, I use checking definitional equality for this, which works well enough but sometimes accepts more examples than I'd want it to. It's rare that def.eq. is not intensional enough, but such is life.

[Henrik Böving]

I think the issue with this is that macro expansion (simple syntax to syntax translations) and elaboration (syntax to Expr or other funky translations) are an interwoven process so it is not quite obvious what a "step" in macro expansion even means. For example you could have a term elaborator (syntax -> Expr) for some specific syntax that then recursively calls into term elaboration for a bunch of its arguments which in turn happen to call macro expansion and then term elaboration etc.

You could e.g. print every time that elabTerm is called but that won't give you the big picture either since it can be called recursively on subterms etc.

I also don't know what the do elaborator is even doing here. I wouldn't be surprised if the above isn't the syntactic translation that is happening but it is instead building the application of bind directly as an Expr directly or something else.

[David Thrane Christiansen]

It definitely seems plausible that this simple spec is not how do is implemented - sorry for the red herring.

But I think that there is a fairly reasonable definition of a "step" of expansion, and that's with regards to hygiene. My understanding is that each step corresponds to a fresh scope that's applied to a piece of syntax, and further recursive calls inside an elaborator are something more like Racket's local-expand than they are like expansion steps.

This seems like it would be handy for explaining and debugging fairly simple notations, even if it's not going to be useful for big complicated things.

[Henrik Böving]

If you really want to see each step the term elaborator is taking you can do that but:

def foo := some 1
def f (x : Nat) : Option Nat := return 2 * x


set_option trace.Elab.step true in
def bar : Option Nat := do
  let x <- foo ; f x

[Elab.step] expected type: Option Nat, term
    do
      let x <- foo;
      f x
  [Elab.step] expected type: Type → Type, term
      ?m
    [Elab.step.result] ?m
  [Elab.step] expected type: Type, term
      ?m
    [Elab.step.result] ?m
  [Elab.step] expected type: Option Nat, term
      with_annotate_term(Term.doLetArrow "let" [] (Term.doIdDecl `x [] "<-" (Term.doExpr `foo)))
        Bind.bind (foo : ?m _) (fun (x : _) => with_annotate_term(Term.app `f [`x]) f x)
    [Elab.step] expected type: Option Nat, term
        Bind.bind (foo : ?m _) (fun (x : _) => with_annotate_term(Term.app `f [`x]) f x)
...

it's just not a pretty process for do at all. It does work for very simple things okay ish though:

notation "myothernotation " x => 2 * x
notation "mynotation " x => myothernotation x

set_option trace.Elab.step true in
def foo := mynotation 2

gives

[Elab.step] expected type: ?m.952, term
    mynotation 2
  [Elab.step] expected type: ?m.952, term
      myothernotation 2
    [Elab.step] expected type: ?m.952, term
        2 * 2

and then it derails a little into the details.

[Sebastian Ullrich]

If something is indeed a macro and not an elaborator, there is docs4#Lean.Macro.expandMacro?

[David Thrane Christiansen]

These are super handy, thanks!