Creating and registering structures without `elabCommand`

Stream: metaprogramming / tactics

[Ghilain Bergeron]

Is there any way, ideally without resorting to implementing the compiler logic from https://github.com/leanprover/lean4/blob/2fcce7258eeb6e324366bc25f9058293b04b7547/src/Lean/Elab/Structure.lean#L1506-L1570 myself, of generating structures (with parents/subobjects) and all their associated functions like projections (including to the field of its transitive parents) from an array of fields of type Array (Name × Expr)?
I am not sure if I simply missed a couple of functions which would do all that or not.
Calling elabCommand on raw syntax is not really doable in my case (at least I don't think) since I am already managing Exprs, not Terms.

[Robin Arnez]

At the end this uses publicly accessible meta functions so here's kinda what calling them directly looks like (no guarantee that it's complete though):

import Lean
import Qq

open Lean Meta Qq

run_meta
  let u : Level := .param `u
  withLocalDeclQ `α .implicit q(Type u) fun α => do
  withLocalDeclDQ `thing q($α) fun thing => do
  withLocalDeclDQ `foo q(Nat) fun foo => do
  withLocalDeclDQ `bar q(Fin $foo) fun bar => do

  let typeName := `Test
  let self : Q(Type u → Type u) := .const typeName [u]
  let projNames := #[`thing, `foo, `bar]
  let vars := #[α, thing, foo, bar]

  let ctor : Constructor := {
    name := typeName ++ `mk
    type := ← mkForallFVars vars q($self $α)
  }
  let indType : InductiveType := {
    name := typeName
    type := ← mkForallFVars #[α] q(Type u)
    ctors := [ctor]
  }
  addDecl (.inductDecl [`u] 1 [indType] false)

  -- see mkAuxConstructions in Lean.Elab.MutualInductive
  mkRecOn typeName
  mkCasesOn typeName
  mkCtorElim typeName
  mkNoConfusion typeName

  mkProjections typeName (projNames.map fun n => { ref := .missing, projName := typeName ++ n })
    (instImplicit := false) -- true for classes

  -- this is "simple" here because we don't have extends
  let flatCtorType := ctor.type
  let flatCtorValue ← mkLambdaFVars vars (mkAppN (.const ctor.name [u]) vars)
  addDecl <| Declaration.defnDecl {
    name := mkFlatCtorOfStructCtorName ctor.name
    levelParams := [`u]
    type := flatCtorType
    value := flatCtorValue
    hints := .abbrev
    safety := .safe
  }

  modifyEnv fun env => registerStructure env {
    structName := typeName
    fields := projNames.map fun n => {
      fieldName := n
      projFn := typeName ++ n
      subobject? := none -- would be some for parent projections
      binderInfo := .default
    }
  }

#print Test

This is certainly not ideal though, it'd be nice if there were helper functions to make this process easier (and also make it rely less on implementation details).

[Ghilain Bergeron]

This is what I kind of already have yes, although in my case I have to handle parent structures as well (not as subobjects though).
The logic used in Lean.Elab.Command.Structure.elabStructureCommand unfortunately is too coupled with the syntax itself (although with a lot less checks), and I am just reimplementing the logic itself, which as you said is less than ideal and I believe barely maintainable.