Obtaining types of structure fields fields

Stream: lean4

[Henrik Böving]

I've been trying to get some very basic things to work for my doc gen tool based on the thing @Mac provided me with and am currently attempting to get information about a structure, especially its fields and their types. My current code is basically this:

def envOfFile (path : FilePath) : IO Environment := do
  let opts := Options.empty
  let mainModuleName := `main
  let input ← IO.FS.readFile path
  let (env, ok) ← Elab.runFrontend input opts path.toString mainModuleName
  unless ok do throw <| IO.userError "could not elaborate file"
  return env

def prettyPrintStructures (path : FilePath) : IO PUnit := do
  let env ← envOfFile path
  for struct in structureExt.getEntries env do
    IO.println <| "structure " ++ struct.structName.toString
    for info in struct.fieldInfo do
      match env.find? info.projFn with
      | some constInfo => IO.println <| "  " ++ info.fieldName.toString ++ " : " ++ constInfo.type.dbgToString
      | none => IO.println "Should not happen"

and while it does correctly find the structures and their fields the type of the projection functions are of course not the actual types of the fields. Now I'm wondering whether I've just overlooked some function in the Lean package that lets me get these types or whether the best way to obtain this would basially be to walk the Expr I get from constInfo.type and remove the outer most foralls (since these will be used for generic structures like for example with: forall {α : Type} {β : Type}, (Point α β) -> β + the left part of the arrow I find after getting rid of the foralls and use that as the type of the field....or whether there is a third and better way I'm not aware of to do this.

[Wojciech Nawrocki]

Seconded, I wasn't able to find functionality for this. Here is an attempt that works for direct fields (i.e. no subobject fields). Getting it to work for parent fields similarly to getStructureFieldsFlattened would be more work since Lean does not generate projections for those, so I think we would have to recursively process parent structures.

def getProjFnInfoForField? (env : Environment) (structName : Name) (fieldName : Name) : Option (Name × ProjectionFunctionInfo) :=
  if let some projFn := getProjFnForField? env structName fieldName then
    (projFn, ·) <$> env.getProjectionFnInfo? projFn
  else
    none

/-- Like `getStructureFields`, but include also the types of fields. Note that when the structure type
has generic parameters, the field types will contain unassigned mvars. These are returned in the second
tuple component. -/
def getTypedStructureFields (structName : Name) : MetaM (Array (Name × Array Expr × Expr)) := do
  let env ← getEnv
  let fields := getStructureFields env structName
  let mut ret := #[]
  for field in fields do
    let some (projFn, projInfo) := getProjFnInfoForField? env structName field
      | throwError "'{structName}.{field}' has no associated projection function"
    let tp ← ConstantInfo.type <$> getConstInfo projFn
    -- make mvars for parameters and the structure argument
    let (mvars, _, cod) ← forallMetaBoundedTelescope tp (projInfo.numParams + 1)
    -- forget the structure argument mvar
    ret := ret.push (field, mvars.pop, cod)
  return ret

[Wojciech Nawrocki]

structure Foo (β : Type) where
  a : Nat
  b : β → β

structure Foo₂ (β : Type) extends Foo β where
  c : String
  d : β → ∀ α, Foo α

elab "TEST" n:ident : command => do IO.println (← liftTermElabM none do getTypedStructureFields n.getId)
/- #[(toFoo, (#[?_uniq.11475], Foo ?_uniq.11475)), (c, (#[?_uniq.11477], String)), (d, (#[?_uniq.11479], ?_uniq.11479 -> (forall (α : Type), Foo α)))] -/
TEST Foo₂

[Henrik Böving]

The way this is done right now in doc-gen4 (this is the way I think @Gabriel Ebner recommended to me) is by parsing the type of the actual constructor like this: https://github.com/leanprover/doc-gen4/blob/main/DocGen4/Process.lean#L257-L264

[Wojciech Nawrocki]

I see, thanks! Looking at the constructor is a good solution to share the index mvars between field types.

[Leonardo de Moura]

Here is a suggestion.

import Lean

open Lean
open Lean.Meta

/--
  Execute `k` with an array containing pairs `(fieldName, fieldType)`.
  `k` is executed in an updated local context which contains local declarations for the `structName` parameters.
-/
def withFields (structName : Name) (k : Array (Name × Expr) → MetaM α) (includeSubobjectFields := true) : MetaM α := do
  let .inductInfo info ← getConstInfo structName | throwError "'{structName}' is not a structure"
  let us := info.levelParams.map mkLevelParam
  forallTelescopeReducing info.type fun params _ =>
  withLocalDeclD `s (mkAppN (mkConst structName us) params) fun s => do
    let mut info := #[]
    for fieldName in getStructureFieldsFlattened (← getEnv) structName includeSubobjectFields do
      let proj ← mkProjection s fieldName
      info := info.push (fieldName, (← inferType proj))
    k info

def printFieldNames (structName : Name) (includeSubobjectFields := true) : MetaM Unit :=
  withFields (includeSubobjectFields := includeSubobjectFields) structName fun fieldTypes =>
    for (fieldName, fieldType) in fieldTypes do
      IO.println s!"{fieldName} : {← ppExpr fieldType}"

structure Foo (β : Type) where
  a : Nat
  b : β → β

structure Foo₂ (β : Type) extends Foo (β × β) where
  c : String
  d : β → ∀ α, Foo α

#eval printFieldNames ``Foo₂
/-
toFoo : Foo (β × β)
a : Nat
b : β × β → β × β
c : String
d : β → (α : Type) → Foo α
-/

#eval printFieldNames (includeSubobjectFields := false) ``Foo₂
/-
a : Nat
b : β × β → β × β
c : String
d : β → (α : Type) → Foo α
-/