Normalization in a macro?

Stream: lean4

[Siddharth Bhat]

How do I normalize a term in a macro? I imagine this is possible, since the LEAN kernel implements normalization by evaluation?

For example, consider:

inductive Listlike
| Cons: Listlike -> Listlike
| Done: Listlike


def cons_fn (l: Listlike) : Listlike := Listlike.Cons l

declare_syntax_cat listlike

syntax "Done" :  listlike
syntax "Cons" listlike : listlike

syntax "listlike%" listlike : term

macro_rules
| `(listlike% Done) => `(Listlike.Done)
| `(listlike% Cons $l:listlike) => `(cons_fn (listlike% $l))


def foo : Listlike := (listlike% Cons Cons Done)
#print foo
/-
def foo : Listlike :=
cons_fn (cons_fn Listlike.Done)
-/

I want #print foo to be Listlike.Cons (Listlike.Cons (Listlike.Done)). Is this possible to achieve?

[Sebastian Ullrich]

There is Lean.Meta.reduce, but you will need an elaborator to run it

Siddharth Bhat said:

since the LEAN kernel implements normalization by evaluation?

It doesn't, btw

[Siddharth Bhat]

Is there an example program that uses Lean.Meta.reduce I can read? That'd be super.

It doesn't, btw

Interesting, what algorithm does Lean use to typecheck? I assumed it used NBE from glancing the kernel :)

[Siddharth Bhat]

I found this: https://github.com/digama0/lean-type-theory. Will give it a read!