diff options
Diffstat (limited to 'source/Felix/Store.hs')
| -rw-r--r-- | source/Felix/Store.hs | 189 |
1 files changed, 104 insertions, 85 deletions
diff --git a/source/Felix/Store.hs b/source/Felix/Store.hs index 973a172..bf84f6e 100644 --- a/source/Felix/Store.hs +++ b/source/Felix/Store.hs @@ -47,6 +47,9 @@ module Felix.Store , newStoreMemo , StoreMemoVisits(..) , storeMemoVisits + , StoreCoordinator + , newStoreCoordinator + , withStoreCoordinator ) where import Base @@ -61,6 +64,11 @@ import Felix.Parsed.Identity qualified as Parsed import Felix.Parsed.Payload qualified as ParsedPayload import Syntax.Interface qualified as Syntax +import Control.Concurrent.MVar + ( MVar + , newMVar + , withMVar + ) import Control.Exception qualified as Exception import Control.Monad (foldM, unless) import Control.Monad.Except qualified as Except @@ -84,6 +92,18 @@ data Store = Store !TheoryId !SQLite.Connection +-- | The single invocation-local gateway for a store connection and its +-- ordinary 'IORef'-backed validation memo. Module checkers may run in +-- parallel, but every SQLite and memo operation remains coordinator-owned. +newtype StoreCoordinator = StoreCoordinator (MVar ()) + +newStoreCoordinator :: IO StoreCoordinator +newStoreCoordinator = StoreCoordinator <$> newMVar () + +withStoreCoordinator :: StoreCoordinator -> IO value -> IO value +withStoreCoordinator (StoreCoordinator ownership) action = + withMVar ownership (const action) + -- | A completely validated, inert cached module. Runtime authority is -- minted only after this value is adopted by 'Checking.Module'. data CachedModuleInstallation = CachedModuleInstallation @@ -157,8 +177,6 @@ data StoreMemo = StoreMemo , memoCheckedObjects :: !(IORef.IORef CheckedObjectClosure) , memoValidatedPropositions :: !(IORef.IORef (Map PropositionId CheckedPropositionContent)) - , memoSemanticInventories :: !(IORef.IORef - (Map SemanticInterfaceId SemanticInventory)) , memoValidatedArtifacts :: !(IORef.IORef (Set ModuleArtifactId)) , memoSyntaxValidationVisits :: !(IORef.IORef Int) , memoSemanticValidationVisits :: !(IORef.IORef Int) @@ -167,8 +185,9 @@ data StoreMemo = StoreMemo , memoArtifactValidationVisits :: !(IORef.IORef Int) } --- Complete aggregate inventories keep validation direct for the current --- walking subset. Measure long chains before adding Phase 6 sharing. +-- Root-scoped validation carries one flat inventory through a deterministic +-- visited fold. Immutable rows and their validation results are memoized +-- above, but complete transitive inventories are not retained per interface. data SemanticInventory = SemanticInventory !(Set SemanticFactOccurrenceFingerprint) !(Map SemanticName SemanticFactOccurrenceFingerprint) @@ -203,7 +222,6 @@ newStoreMemo (Store _path theory _connection) = do validatedSemantic <- IORef.newIORef Set.empty checkedObjects <- IORef.newIORef emptyClosure validatedPropositions <- IORef.newIORef Map.empty - semanticInventories <- IORef.newIORef Map.empty validatedArtifacts <- IORef.newIORef Set.empty syntaxVisits <- IORef.newIORef 0 semanticVisits <- IORef.newIORef 0 @@ -221,7 +239,6 @@ newStoreMemo (Store _path theory _connection) = do , memoValidatedSemantic = validatedSemantic , memoCheckedObjects = checkedObjects , memoValidatedPropositions = validatedPropositions - , memoSemanticInventories = semanticInventories , memoValidatedArtifacts = validatedArtifacts , memoSyntaxValidationVisits = syntaxVisits , memoSemanticValidationVisits = semanticVisits @@ -1654,7 +1671,6 @@ validateModuleArtifactClosure memo store root = do (moduleArtifactResultSemantic artifact) void (validateSemanticInventory - Set.empty (moduleArtifactResultSemantic artifact)) case checked of Left failure -> @@ -1734,6 +1750,8 @@ validateModuleArtifactClosure memo store root = do traverse_ (validateSemantic (Set.insert identity path)) (semanticInterfaceDirectInputs interface) + operationBindings <- + semanticOperationBindings Set.empty identity validateObjectRoots objects closure <- Except.liftIO (IORef.readIORef (memoCheckedObjects memo)) @@ -1745,7 +1763,7 @@ validateModuleArtifactClosure memo store root = do (semanticGlobalBindingKey binding) (semanticGlobalBindingTarget binding)) (validateSemanticGlobalBindingTarget - closure binding))) + operationBindings closure binding))) bindings traverse_ validateProposition propositions traverse_ validateOccurrence @@ -1758,6 +1776,33 @@ validateModuleArtifactClosure memo store root = do (memoValidatedSemantic memo) (Set.insert identity)) + semanticOperationBindings path identity + | identity `Set.member` path = pure Set.empty + | otherwise = do + interface <- requireMemo + SemanticInterfaces + (cacheDigestBytes + (semanticInterfaceIdDigest identity)) + (memoSemantic memo store identity) + inherited <- + traverse + (semanticOperationBindings + (Set.insert identity path)) + (semanticInterfaceDirectInputs interface) + let local = + Set.fromList + [ ( semanticStructureOperationSymbol operation + , semanticStructureOperationObject operation + ) + | declaration <- + semanticInterfaceDeclarations interface + , descriptor <- semanticEnvironmentStructures + (declarationDeltaEnvironment declaration) + , operation <- + semanticStructureDescriptorOperations descriptor + ] + pure (Set.unions (local : inherited)) + validateObjectRoots identities = do closure <- Except.liftIO (IORef.readIORef (memoCheckedObjects memo)) @@ -1843,83 +1888,57 @@ validateModuleArtifactClosure memo store root = do proposition (semanticFactAuthority occurrence)))) - validateSemanticInventory path identity = do - inventories <- Except.liftIO - (IORef.readIORef (memoSemanticInventories memo)) - case Map.lookup identity inventories of - Just inventory -> - pure inventory - Nothing - | identity `Set.member` path -> - pure - (SemanticInventory - Set.empty Map.empty Map.empty) - | otherwise -> do - interface <- requireMemo - SemanticInterfaces - (cacheDigestBytes - (semanticInterfaceIdDigest identity)) - (memoSemantic memo store identity) - parents <- traverse - (validateSemanticInventory - (Set.insert identity path)) - (semanticInterfaceDirectInputs interface) - SemanticInventory - parentFacts parentAliases parentGlobals <- - foldM mergeInventory - (SemanticInventory - Set.empty Map.empty Map.empty) - parents - let declarations = - semanticInterfaceDeclarations interface - localFacts = Set.fromList - [ semanticFactFingerprint occurrence - | declaration <- declarations - , occurrence <- declarationDeltaFacts declaration - ] - visibleFacts = parentFacts <> localFacts - aliases <- foldM - (insertAlias visibleFacts) - parentAliases - [ alias - | declaration <- declarations - , alias <- declarationDeltaAliases declaration - ] - globals <- foldM - insertGlobal - parentGlobals - [ binding - | declaration <- declarations - , binding <- semanticEnvironmentBindings - (declarationDeltaEnvironment declaration) - ] - let inventory = - SemanticInventory - visibleFacts aliases globals - Except.liftIO - (IORef.modifyIORef' - (memoSemanticInventories memo) - (Map.insert identity inventory)) - pure inventory - - mergeInventory - (SemanticInventory facts aliases globals) - (SemanticInventory moreFacts moreAliases moreGlobals) = do - merged <- foldM - (\current (name, target) -> - insertNamedAlias name target current) - aliases - (Map.toAscList moreAliases) - mergedGlobals <- foldM - (\current (key, target) -> - insertGlobalBinding key target current) - globals - (Map.toAscList moreGlobals) - pure - (SemanticInventory - (facts <> moreFacts) - merged - mergedGlobals) + validateSemanticInventory identity = + snd + <$> foldSemanticInventory + Set.empty + (SemanticInventory Set.empty Map.empty Map.empty) + identity + + foldSemanticInventory visited inventory identity + | identity `Set.member` visited = + pure (visited, inventory) + | otherwise = do + interface <- requireMemo + SemanticInterfaces + (cacheDigestBytes + (semanticInterfaceIdDigest identity)) + (memoSemantic memo store identity) + (parentVisited, parentInventory) <- + foldM + (\(seen, current) parent -> + foldSemanticInventory seen current parent) + (Set.insert identity visited, inventory) + (semanticInterfaceDirectInputs interface) + let declarations = semanticInterfaceDeclarations interface + SemanticInventory + parentFacts parentAliases parentGlobals = + parentInventory + localFacts = Set.fromList + [ semanticFactFingerprint occurrence + | declaration <- declarations + , occurrence <- declarationDeltaFacts declaration + ] + visibleFacts = parentFacts <> localFacts + aliases <- foldM + (insertAlias visibleFacts) + parentAliases + [ alias + | declaration <- declarations + , alias <- declarationDeltaAliases declaration + ] + globals <- foldM + insertGlobal + parentGlobals + [ binding + | declaration <- declarations + , binding <- semanticEnvironmentBindings + (declarationDeltaEnvironment declaration) + ] + pure + ( parentVisited + , SemanticInventory visibleFacts aliases globals + ) insertGlobal globals binding = insertGlobalBinding |