metaprogramming: how to create function with structural rec?

Stream: lean4

[Michael Jam]

I'm trying to create a function g with a command. g should have the same body as f.
There is a recursive call in g's body which is causing an issue.
Here is a minimized example :

import Lean
open Lean Elab Command Term Meta

def f : Nat → Nat :=
  fun k => match k with
  | 0 => 42
  | n + 1 => f n

elab "the_answer" : command => do
  let name := `g
  let type <- liftCoreM <| MetaM.run' <| do
    let stx <- `(Nat → Nat)
    let r <- TermElabM.run' <| elabTerm stx .none
    return r
  let val <- liftCoreM <| MetaM.run' <| do
    let stx <- `(
      fun k => match k with
      | 0 => 42
      | n + 1 => g n
    )
    let r <- TermElabM.run' <| withDeclName name <| elabTerm stx (.some type)
    let r <- instantiateMVars r
    return r
  let decl := Declaration.defnDecl <| mkDefinitionValEx name [] type val .opaque .safe
  match (<- getEnv).addAndCompile {} decl with
  | .error e => throwError (e.toMessageData {})
  | .ok env => setEnv env

the_answer
#print g

It fails because it is unaware of g in this function body context. I tried using a let rec, but g remains an unassigned metavariable.
How can I fix my code?

Thanks for suggestions or solutions

[Arthur Paulino]

I do think that let rec is a good solution:

    let stx <- `(
      let rec aux := fun k => match k with
      | 0 => 42
      | n + 1 => aux n
      aux
    )

The other issue (kernel) declaration has metavariables 'g' is related to something else I can't point my finger at yet

[Arthur Paulino]

Unrelated: you probably want to use elabTermEnsuringType

[Alex Keizer]

Alternatively, just generate syntax for the entire definition and feed that to elabCommand

open Lean Lean.Elab.Command in
elab "the_answer" : command => do
  let name := mkIdent `g
  elabCommand <|<- `(
    def $name : Nat → Nat
      | 0 => 42
      | n + 1 => $name n
  )

the_answer

#check g
#eval g 0
#eval g 10

Note the mkIdent needed to ensure hygiene does not mess up the name of your function.

[Michael Jam]

@Alex Keizer Well that doesn't exactly solve my issue, because I was actually working in AttrM where I cannot use elabCommand. But thanks for that idea, I'm probably just gonna change my plans and make a command instead of an attribute...

[Jannis Limperg]

You can lower TermElabM or CommandElabM into CoreM, then lift that into AttrM. Something like this:

def runTermElabMAsCoreM (x : TermElabM α) : CoreM α :=
  x.run' |>.run' {} {}

This runs the elaboration with an empty metavariable context and some dummy elaboration state.

[Jannis Limperg]

(The lifting from CoreM to AttrM is automatic via coercion.)

[Sebastian Ullrich]

AttrM in fact is just an abbrev for CoreM nowadays

[Jannis Limperg]

It's the identity coercion. :innocent:

[Sebastian Ullrich]

Just to summarize the original topic: the structural recursion compiler is part of the command (declaration) elaborator, yes, so elaborating a single term is not sufficient (except for nested let recs, which are kind of separate declarations). If anyone had a need for structural recursion without going through one of the existing declaration elaborators, they would need to look at invoking docs4#Lean.Elab.Structural.structuralRecursion manually.