Manual derecursification of PreDefinition

Stream: metaprogramming / tactics

[nrs]

Is it in principle possible to manually turn a PreDefinition into a kernel-ready recursion-free expression from within a MetaM declaration? I am looking at Elab/PreDefinition/Structural/BRecOn.lean and it seems like replaceRecApps is the key function here. Will be attempting to do this for educational purposes and editing with progress

[Kyle Miller]

docs#Lean.Elab.addPreDefinitions will do this and add the definition to the environment. You can get the term by reading the environment. It's TermElabM, but you can run TermElabM from within MetaM.

[nrs]

Amazing thanks for the reference! Will attempt a mwe
edit: relevant: #lean4 > How is Nat.below and Nat.brecOn compiled

[Kyle Miller]

Maybe you haven't found elabMutualDef yet? Lean/Elab/MutualDef.lean

That's the main entry point to elaborating definitions/theorems/etc., and I got to addPreDefinitions by just skimming the code.

[nrs]

ah nice I had not seen it yet

[nrs]

I wonder if PreDefinitions are somewhere in the environment or the only way of getting them is by manually building an Expr
edit: oh it seems that the two elabMutualDef are a bit lower level than PreDefinitions, they take variations of Array Syntax
edit2: only the elabMutualDef targeting TermElab uses addPreDefinitions so I'll be focusing on that one to start off. in the DefViews it takes, DefView.value seems to give the body of a definition as a Syntax object
edit3: Lean.Elab.Term.MutualClosure.main seems to be the first function in the body of elabMutualDef that will generate a PreDefinition
edit4: it seems that covers the extent of the existence of PreDefinitions? produced within elabMutualDef by MutualClosure.main, then gets mvars instantiated and universe levels fixed, and then gets passed to addPreDefinitions
edit5: possible ways a PreDefinition gets consumed in addPreDefinitions, if no error:

1. nonrec, noncomputable: addNonRec
2. nonrec, computable : addAndCompileNonRec
3. unsafe: addAndCompileUnsafe
4. partial: addAndCompilePartial
if none of these,

5. structuralRecursion
6. wfRecursion
7. (failure: will attempt addAsAxioms)
edit6: structuralRecursion or wfRecursion chosen by matching PreDefinition.termination.terminationBy? with { structural := true/false, ..}

[nrs]

to more closely follow structuralRecursion and wfRecursion I'm taking a detour and manually creating a PreDefinition from a definition identical to Nat.add. given the above comments I will try to pass this to MutualClosure.main. The main problem will be to get the Expr as it is before it is given to elabMutualDef, I think manually building a let rec Expr should do it

edit: it turns this is not that simple and requires reading the stuff above MutualClosure.main. Am trying to pass the result of applying elabTerm (with maybe toExpr) to let rec add (n m : Nat) : Nat := Nat.casesOn m n (fun mm => add n.succ mm); add to MutualClosure.main

edit2: from MutualDef.lean:

let rec
  f : A := t,
  g : B := s;
body

is encoded as

let f : A := ?m₁;
let g : B := ?m₂;
body

where ?m₁ and ?m₂ are synthetic opaque metavariables. The body of f (or g) is stored the field val of a LetRecToLift.

[nrs]

here is my progress so far, from emulating what happens within elabMutualDef. the following incomplete definition for a PreDefinition requires a successful call to elabHeaders; am currently working on understanding on how it works. any tips/suggestions are welcome

import Lean
import Batteries.Tactic.OpenPrivate

open Lean Elab Command Term
open private elabHeaders from Lean.Elab.MutualDef
open private declValToTerminationHint from Lean.Elab.MutualDef

def mkAddPreDef : TermElabM Unit := do
  let stx : Syntax <- `(def add (n m : Nat) : Nat := Nat.casesOn m n (fun x => add n.succ x))
  let defview := mkDefViewOfDef {} stx[1]
  let headerAr <- elabHeaders #[defview] #[] #[]
  let headerArEmpty := if headerAr.size = 0 then Bool.true else .false
  dbg_trace headerArEmpty -- outputs .true, so call to elabHeaders isn't working properly
  let ifWeHaveHeader : DefViewElabHeader -> TermElabM PreDefinition := fun header => do
    let termination <- declValToTerminationHint header.value
    let predef : PreDefinition := .mk
      defview.ref
      .def
      []
      {}
      header.declName
      header.type
      _ -- PreDefinition.value : Lean.Expr, built within pushMain in MutualDef.lean
      termination
    pure predef
  pure .unit

[nrs]

the following seems to produce a minimal PreDefinition that has not yet undergone derecursification. I don't understand what withAlwaysResolvedPromises is doing, but omitting it makes elabHeaders fail, and attempting to manually create the DefViewElabHeader that elabHeaders returns will result in failure to recognize the variables n, m, in the body, which should be bound by the binders (n : Nat) and (m : Nat). The exact point where going through elabHeaders vs. creating a DefViewElabHeader manually will differ seems to be in the body of elabFunValues, at the line let val ← elabTermEnsuringType valStx type <* synthesizeSyntheticMVarsNoPostponing. Without elabHeaders, the symbols n, m in the body of the declaration will be replaced by a sorry. It seems that TermElabM's Context and State are the exact same in the elabHeaders case vs. the case without, yet the result of the above mentioned line differs. Would be very interested if someone has an explanation for this!

running dbg_trace on the fields of predef seems to have the expected outputs, and the term to derecursify seems to be predef.value. Will attempt to feed this to structuralRecursion.

import Lean
import Batteries.Tactic.OpenPrivate

open Lean Meta Elab Command Term Language
open private elabHeaders from Lean.Elab.MutualDef
open private withFunLocalDecls from Lean.Elab.MutualDef
open private elabFunValues from Lean.Elab.MutualDef

def mkAddPreDef : TermElabM Unit := do
  let stx : Syntax <- `(def add (n : Nat) (m : Nat) : Nat := Nat.casesOn m n (fun x => add n.succ x))
  let defview := mkDefViewOfDef {} stx[1]
  withAlwaysResolvedPromises 1 fun bodyPromises =>
  withAlwaysResolvedPromises 1 fun tacPromises => do
    let headers ← elabHeaders #[defview] bodyPromises tacPromises
    withFunLocalDecls headers fun funFVars => do
      let values ← elabFunValues headers #[] {header := ""}
      let predef := (<- Lean.Elab.Term.MutualClosure.main #[] headers funFVars values [])[0]!
  pure .unit

edit: the code below is a mwe for the case that attempts to avoid elabHeaders (and fails). the #eval will report unknown identifier m/n. From my tracing, it seems to me that bothState and Context in TermElabM are the same as the case above just before the call to elabFunValues, so I don't understand why it fails

import Lean
import Batteries.Tactic.OpenPrivate

open Lean Meta Elab Command Term
open private withFunLocalDecls from Lean.Elab.MutualDef
open private elabFunValues from Lean.Elab.MutualDef

def mkAddPreDef : TermElabM Unit := do
  let stx : Syntax <- `(def add (n : Nat) (m : Nat) : Nat := Nat.casesOn m n (fun x => add n.succ x))
  let defview := mkDefViewOfDef {} stx[1]
  let ⟨shortName, declName, levelNames⟩ <- withRef defview.ref do
    Term.expandDeclId (<- getCurrNamespace) (<- getLevelNames) defview.declId defview.modifiers
  let typeExpr <- elabTerm (<- `(Nat -> Nat -> Nat)) .none
  let binders := defview.binders.getArgs
  let dveh : DefViewElabHeader <- elabBindersEx binders fun xs => do
    Term.synthesizeSyntheticMVarsNoPostponing
    let (binderIds, xs) := xs.unzip
    let proto_dveh_data : DefViewElabHeaderData := {
      declName := declName
      shortDeclName := shortName
      levelNames := levelNames
      binderIds := binderIds
      numParams := xs.size
      type := typeExpr
    }
    let proto_dveh : DefViewElabHeader := {
      defview, proto_dveh_data with bodySnap? := .none, tacSnap? := .none
    }
    pure proto_dveh
  withFunLocalDecls #[dveh] fun fvars => do
    for fvar in fvars do
      addLocalVarInfo defview.declId fvar
    let funvalues <- elabFunValues #[dveh] #[] {header := ""}
  pure .unit
#eval mkAddPreDef

[nrs]

continuing with this today, if anyone has inputs it would be highly appreciated! will edit this comment with incomplete progress
edit: currently working on a way to automatically get dependencies between a declaration within a same file (from env.constants.map\2) in order to make reverse engineering easier