From c0dd4be70abaf0443a44023e5187c9753a1bd87a Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 14 Nov 2024 16:55:46 -0800 Subject: [PATCH] fix: have inherited fields link to their origin The calculation for projection functions was incorrect for fields that came from parents that overlapped with another. It was using the projection function that Lean uses to access the field, not the actual origin projection function. --- DocGen4/Process/StructureInfo.lean | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) diff --git a/DocGen4/Process/StructureInfo.lean b/DocGen4/Process/StructureInfo.lean index 33f39b3..8f9a71a 100644 --- a/DocGen4/Process/StructureInfo.lean +++ b/DocGen4/Process/StructureInfo.lean @@ -32,19 +32,29 @@ def withFields (info : InductiveVal) (k : Array (Name × Name × Expr) → Array fields := fields.push (fieldName, (← inferType proj)) k parents fields -def getFieldTypes (v : InductiveVal) : MetaM (Array StructureParentInfo × Array FieldInfo) := do +/-- +Computes the origin of a field. Returns if the field was directly defined in this structure, and its projection function. +Multiple parents could be the origin of a field, but we say the first parent that provides it is the one that determines the origin. +-/ +partial def getFieldOrigin (structName field : Name) : MetaM (Bool × Name) := do let env ← getEnv + for parent in getStructureParentInfo env structName do + if (findField? env parent.structName field).isSome then + let (_, projFn) ← getFieldOrigin parent.structName field + return (false, projFn) + let some fi := getFieldInfo? env structName field + | throwError "no such field {field} in {structName}" + return (true, fi.projFn) + +def getFieldTypes (v : InductiveVal) : MetaM (Array StructureParentInfo × Array FieldInfo) := do withFields v fun parents fields => do let mut parentInfo : Array StructureParentInfo := #[] let mut fieldInfo : Array FieldInfo := #[] for (_, projFn, type) in parents do parentInfo := parentInfo.push { projFn, type := ← prettyPrintTerm type } for (name, type) in fields do - let some structForField := findField? env v.name name | unreachable! - -- We can't simply do `structForField == v.name` since the field might be from a parent that overlapped with another. - let isDirect := structForField == v.name && !parents.any fun (parent, _) => (getFieldInfo? env parent name).isSome - let some fi := getFieldInfo? env structForField name | unreachable! - fieldInfo := fieldInfo.push { ← NameInfo.ofTypedName fi.projFn type with isDirect } + let (isDirect, projFn) ← getFieldOrigin v.name name + fieldInfo := fieldInfo.push { ← NameInfo.ofTypedName projFn type with isDirect } return (parentInfo, fieldInfo) def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do