refactor: Less manual manipulation of expressions

DocGen4/Process/StructureInfo.lean

@@ -12,24 +12,24 @@ namespace DocGen4.Process
 
 open Lean Meta 
 
--- TODO: replace with Leos variant from Zulip
-def dropArgs (type : Expr) (n : Nat) : (Expr × List (Name × Expr)) :=
-  match type, n with
-  | e, 0 => (e, [])
-  | Expr.forallE name type body _, x + 1 =>
-    let body := body.instantiate1 <| mkFVar ⟨name⟩
-    let next := dropArgs body x
-    { next with snd := (name, type) :: next.snd}
-  | _, _ + 1 => panic! s!"No forallE left"
+/--
+  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 (info : InductiveVal) (k : Array (Name × Expr) → MetaM α) (includeSubobjectFields : Bool := false) : MetaM α := do
+  let structName := info.name
+  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 getFieldTypes (struct : Name) (ctor : ConstructorVal) (parents : Nat) : MetaM (Array NameInfo) := do
-  let type := ctor.type
-  let (fieldFunction, _) := dropArgs type (ctor.numParams + parents)
-  let (_, fields) := dropArgs fieldFunction (ctor.numFields - parents)
-  let mut fieldInfos := #[]
-  for (name, type) in fields do
-    fieldInfos := fieldInfos.push <| ← NameInfo.ofTypedName (struct.append name) type
-  return fieldInfos
+def getFieldTypes (v : InductiveVal) : MetaM (Array NameInfo) := do
+  withFields v fun fields =>
+    fields.foldlM (init := #[]) (fun acc (name, type) => do return acc.push (← NameInfo.ofTypedName (v.name.append name) type))
 
 def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
@@ -42,7 +42,7 @@ def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
     if i.fieldNames.size - parents.size > 0 then
       return {
         toInfo := info,
-        fieldInfo := ← getFieldTypes v.name ctorVal parents.size,
+        fieldInfo := ← getFieldTypes v,
         parents,
         ctor
       }