From 66d68484afa7923c92427c1847aaf36151c230f1 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Wed, 30 Oct 2024 18:22:34 -0700 Subject: [PATCH] fix: make structure parent info persist (#5890) Modifies the `structureExt` from being a `SimplePersistentEnvExtension` to a `PersistentEnvExtension`. The simple version contains a `List` of all added entries, which we do not need since we already have a `PersistentHashMap` of them in the state. The oversight was that this `List` contained duplicate entries due to `setStructureParents` re-adding entries. --- src/Lean/Structure.lean | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/Lean/Structure.lean b/src/Lean/Structure.lean index 235bf55b6ef9..5cbee766c5e3 100644 --- a/src/Lean/Structure.lean +++ b/src/Lean/Structure.lean @@ -80,10 +80,11 @@ private structure StructureState where map : PersistentHashMap Name StructureInfo := {} deriving Inhabited -builtin_initialize structureExt : SimplePersistentEnvExtension StructureInfo StructureState ← registerSimplePersistentEnvExtension { - addImportedFn := fun _ => {} - addEntryFn := fun s e => { s with map := s.map.insert e.structName e } - toArrayFn := fun es => es.toArray.qsort StructureInfo.lt +builtin_initialize structureExt : PersistentEnvExtension StructureInfo StructureInfo (Unit × StructureState) ← registerPersistentEnvExtension { + mkInitial := pure ((), {}) + addImportedFn := fun _ => pure ((), {}) + addEntryFn := fun (_, s) e => ((), { s with map := s.map.insert e.structName e }) + exportEntriesFn := fun (_, s) => s.map.toArray |>.map (·.snd) |>.qsort StructureInfo.lt } /-- @@ -113,7 +114,7 @@ Set parent projection info for a structure defined in the current module. Throws an error if the structure has not already been registered with `Lean.registerStructure`. -/ def setStructureParents [Monad m] [MonadEnv m] [MonadError m] (structName : Name) (parentInfo : Array StructureParentInfo) : m Unit := do - let some info := structureExt.getState (← getEnv) |>.map.find? structName + let some info := structureExt.getState (← getEnv) |>.snd.map.find? structName | throwError "cannot set structure parents for '{structName}', structure not defined in current module" modifyEnv fun env => structureExt.addEntry env { info with parentInfo } @@ -121,7 +122,7 @@ def setStructureParents [Monad m] [MonadEnv m] [MonadError m] (structName : Name def getStructureInfo? (env : Environment) (structName : Name) : Option StructureInfo := match env.getModuleIdxFor? structName with | some modIdx => structureExt.getModuleEntries env modIdx |>.binSearch { structName } StructureInfo.lt - | none => structureExt.getState env |>.map.find? structName + | none => structureExt.getState env |>.snd.map.find? structName /-- Gets the `StructureInfo` for `structName`, which is assumed to have been declared as a structure to the elaborator.