/--
diff --git a/DocGen4/Process/Base.lean b/DocGen4/Process/Base.lean
index efa80ed..9e395eb 100644
--- a/DocGen4/Process/Base.lean
+++ b/DocGen4/Process/Base.lean
@@ -16,7 +16,7 @@ structure NameInfo where
/--
The name that has this info attached.
-/
- name : Name
+ name : Name
/--
The pretty printed type of this name.
-/
@@ -27,7 +27,13 @@ structure NameInfo where
doc : Option String
deriving Inhabited
+/--
+Stores information about a structure field.
+-/
structure FieldInfo extends NameInfo where
+ /--
+ Whether or not this field is new to this structure, or instead whether it was inherited from a parent.
+ -/
isDirect : Bool
/--
@@ -122,6 +128,15 @@ structure InductiveInfo extends Info where
isUnsafe : Bool
deriving Inhabited
+/--
+Information about a `structure` parent.
+-/
+structure StructureParentInfo where
+ /-- Name of the projection function. -/
+ projFn : Name
+ /-- Pretty printed type. -/
+ type : CodeWithInfos
+
/--
Information about a `structure` declaration.
-/
@@ -133,7 +148,7 @@ structure StructureInfo extends Info where
/--
All the structures this one inherited from.
-/
- parents : Array Name
+ parents : Array StructureParentInfo
/--
The constructor of the structure.
-/
diff --git a/DocGen4/Process/StructureInfo.lean b/DocGen4/Process/StructureInfo.lean
index 2aff5c1..33f39b3 100644
--- a/DocGen4/Process/StructureInfo.lean
+++ b/DocGen4/Process/StructureInfo.lean
@@ -13,39 +13,49 @@ namespace DocGen4.Process
open Lean Meta
/--
- Execute `k` with an array containing pairs `(fieldName, fieldType)`.
+ Execute `k` with an array containing pairs `(parentName, projFn, parentType)`
+ and 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 α) : MetaM α := do
+def withFields (info : InductiveVal) (k : Array (Name × Name × Expr) → Array (Name × Expr) → MetaM α) : MetaM α := do
let structName := info.name
let us := info.levelParams.map mkLevelParam
forallTelescopeReducing info.type fun params _ =>
withLocalDeclD `self (mkAppN (mkConst structName us) params) fun s => do
- let mut info := #[]
+ let mut parents := #[]
+ for parent in getStructureParentInfo (← getEnv) structName do
+ let proj := mkApp (mkAppN (mkConst parent.projFn us) params) s
+ parents := parents.push (parent.structName, parent.projFn, ← inferType proj)
+ let mut fields := #[]
for fieldName in getStructureFieldsFlattened (← getEnv) structName (includeSubobjectFields := false) do
let proj ← mkProjection s fieldName
- info := info.push (fieldName, (← inferType proj))
- k info
+ fields := fields.push (fieldName, (← inferType proj))
+ k parents fields
-def getFieldTypes (parents : Array Name) (v : InductiveVal) : MetaM (Array FieldInfo) := do
+def getFieldTypes (v : InductiveVal) : MetaM (Array StructureParentInfo × Array FieldInfo) := do
let env ← getEnv
- withFields v fun fields =>
- fields.foldlM (init := #[]) (fun acc (name, type) => 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 isDirect := structForField == v.name && !parents.any fun (parent, _) => (getFieldInfo? env parent name).isSome
let some fi := getFieldInfo? env structForField name | unreachable!
- return acc.push { ← NameInfo.ofTypedName fi.projFn type with isDirect })
+ fieldInfo := fieldInfo.push { ← NameInfo.ofTypedName fi.projFn type with isDirect }
+ return (parentInfo, fieldInfo)
def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
let info ← Info.ofConstantVal v.toConstantVal
let env ← getEnv
- let parents := (getStructureParentInfo env v.name).map fun parent => parent.structName
let ctorVal := getStructureCtor env v.name
let ctor ← NameInfo.ofTypedName ctorVal.name ctorVal.type
+ let (parents, fieldInfo) ← getFieldTypes v
return {
toInfo := info,
- fieldInfo := ← getFieldTypes parents v,
+ fieldInfo,
parents,
ctor
}