{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE NoImplicitPrelude #-} -- | Coordinator-owned access to the disposable SQLite store. module Felix.Store ( Store , storeTheoryId , StoreSelection(..) , StorePlan , StorePath , storePathFilePath , storeRollbackJournalPath , StorePlanningError(..) , renderStorePlanningError , planStore , StoreLease , storeLeasePath , withStoreLease , StoreLifecycleError(..) , renderStoreLifecycleError , withOpenStore , StoreStartup(..) , StoreCompatibility(..) , currentStoreCompatibility , StoreIncompatibility(..) , renderStoreIncompatibility , StoreOpenError(..) , renderStoreOpenError , StoreRelation(..) , StoreFailure(..) , renderStoreFailure , openStore , closeStore , loadProofValidation , loadDeclarationValidation , loadParsedArtifact , writeParsedArtifact , CachedModuleInstallation , cachedInstallationSyntax , cachedInstallationSemantic , cachedInstallationObjects , cachedInstallationPropositions , cachedInstallationFinalPrefix , loadCachedModuleInstallation , writePendingModulePrefix , writeSealedModule , StoreMemo , newStoreMemo , StoreMemoVisits(..) , storeMemoVisits , StoreCoordinator , newStoreCoordinator , withStoreCoordinator ) where import Base import Felix.Checking.Core import Felix.Checking.Declaration qualified as Declaration import Felix.Checking.Identity import Felix.Checking.Materialization qualified as Materialization import Felix.Checking.Semantic import Felix.Cache.Codec import Felix.Module (ModuleName) import Felix.Parsed.Identity qualified as Parsed import Felix.Parsed.Payload qualified as ParsedPayload import Felix.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 import Data.Bifunctor (first) import Data.ByteString (ByteString) import Data.Int (Int64) import Data.Map.Strict qualified as Map import Data.Set qualified as Set import Data.Text qualified as Text import Data.Word (Word32) import Data.IORef qualified as IORef import Database.SQLite.Simple qualified as SQLite import Database.SQLite.Simple.Types (Only(..), Query(..)) import System.Directory qualified as Directory import System.FilePath.Posix qualified as Posix import System.IO.Temp qualified as Temp data Store = Store !FilePath !TheoryId !SQLite.Connection storeTheoryId :: Store -> TheoryId storeTheoryId (Store _path theory _connection) = theory -- | 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 !Syntax.ModuleSyntaxInterface !SemanticInterface ![AssertedObject] ![CheckedPropositionContent] !PrefixContextId cachedInstallationSyntax :: CachedModuleInstallation -> Syntax.ModuleSyntaxInterface cachedInstallationSyntax (CachedModuleInstallation syntax _semantic _objects _propositions _prefix) = syntax cachedInstallationSemantic :: CachedModuleInstallation -> SemanticInterface cachedInstallationSemantic (CachedModuleInstallation _syntax semantic _objects _propositions _prefix) = semantic cachedInstallationObjects :: CachedModuleInstallation -> [AssertedObject] cachedInstallationObjects (CachedModuleInstallation _syntax _semantic objects _propositions _prefix) = objects cachedInstallationPropositions :: CachedModuleInstallation -> [CheckedPropositionContent] cachedInstallationPropositions (CachedModuleInstallation _syntax _semantic _objects propositions _prefix) = propositions cachedInstallationFinalPrefix :: CachedModuleInstallation -> PrefixContextId cachedInstallationFinalPrefix (CachedModuleInstallation _syntax _semantic _objects _propositions prefix) = prefix -- | Invocation-local decoded row memo. It never changes a persistent row -- and is discarded with the coordinator invocation. Its ordinary IORefs are -- coordinator-confined: operations on one memo must remain sequential or be -- serialized by that coordinator. data StoreMemo = StoreMemo { memoArtifactRows :: !(IORef.IORef (Map ModuleArtifactId (Either StoreFailure (Maybe ModuleArtifactResult)))) , memoSyntaxRows :: !(IORef.IORef (Map Syntax.SyntaxInterfaceId (Either StoreFailure (Maybe Syntax.ModuleSyntaxInterface)))) , memoSemanticRows :: !(IORef.IORef (Map SemanticInterfaceId (Either StoreFailure (Maybe SemanticInterface)))) , memoObjectRows :: !(IORef.IORef (Map ObjectId (Either StoreFailure (Maybe AssertedObject)))) , memoPropositionRows :: !(IORef.IORef (Map PropositionId (Either StoreFailure (Maybe (CanonicalTerm ObjectId))))) , memoValidatedSyntax :: !(IORef.IORef (Set Syntax.SyntaxInterfaceId)) , memoValidatedSemantic :: !(IORef.IORef (Set SemanticInterfaceId)) , memoCheckedObjects :: !(IORef.IORef CheckedObjectClosure) , memoValidatedPropositions :: !(IORef.IORef (Map PropositionId CheckedPropositionContent)) , memoValidatedArtifacts :: !(IORef.IORef (Set ModuleArtifactId)) , memoSyntaxValidationVisits :: !(IORef.IORef Int) , memoSemanticValidationVisits :: !(IORef.IORef Int) , memoObjectValidationVisits :: !(IORef.IORef Int) , memoPropositionValidationVisits :: !(IORef.IORef Int) , memoArtifactValidationVisits :: !(IORef.IORef Int) } -- 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) !(Map SemanticGlobalKey SemanticGlobalTarget) data StoreMemoVisits = StoreMemoVisits { storeArtifactRowsDecoded :: !Int , storeSyntaxRowsDecoded :: !Int , storeSyntaxRowsValidated :: !Int , storeSemanticRowsDecoded :: !Int , storeSemanticRowsValidated :: !Int , storeObjectRowsDecoded :: !Int , storeObjectRowsValidated :: !Int , storePropositionRowsDecoded :: !Int , storePropositionRowsValidated :: !Int , storeArtifactsValidated :: !Int } deriving stock (Show, Eq) newStoreMemo :: Store -> IO StoreMemo newStoreMemo (Store _path theory _connection) = do emptyClosure <- case validateObjectClosure theory [] of Right closure -> pure closure Left _ -> impossible "empty store object closure is invalid" artifactRows <- IORef.newIORef Map.empty syntaxRows <- IORef.newIORef Map.empty semanticRows <- IORef.newIORef Map.empty objectRows <- IORef.newIORef Map.empty propositionRows <- IORef.newIORef Map.empty validatedSyntax <- IORef.newIORef Set.empty validatedSemantic <- IORef.newIORef Set.empty checkedObjects <- IORef.newIORef emptyClosure validatedPropositions <- IORef.newIORef Map.empty validatedArtifacts <- IORef.newIORef Set.empty syntaxVisits <- IORef.newIORef 0 semanticVisits <- IORef.newIORef 0 objectVisits <- IORef.newIORef 0 propositionVisits <- IORef.newIORef 0 artifactVisits <- IORef.newIORef 0 pure StoreMemo { memoArtifactRows = artifactRows , memoSyntaxRows = syntaxRows , memoSemanticRows = semanticRows , memoObjectRows = objectRows , memoPropositionRows = propositionRows , memoValidatedSyntax = validatedSyntax , memoValidatedSemantic = validatedSemantic , memoCheckedObjects = checkedObjects , memoValidatedPropositions = validatedPropositions , memoValidatedArtifacts = validatedArtifacts , memoSyntaxValidationVisits = syntaxVisits , memoSemanticValidationVisits = semanticVisits , memoObjectValidationVisits = objectVisits , memoPropositionValidationVisits = propositionVisits , memoArtifactValidationVisits = artifactVisits } storeMemoVisits :: StoreMemo -> IO StoreMemoVisits storeMemoVisits memo = do artifactRows <- IORef.readIORef (memoArtifactRows memo) syntaxRows <- IORef.readIORef (memoSyntaxRows memo) semanticRows <- IORef.readIORef (memoSemanticRows memo) objectRows <- IORef.readIORef (memoObjectRows memo) propositionRows <- IORef.readIORef (memoPropositionRows memo) syntaxVisits <- IORef.readIORef (memoSyntaxValidationVisits memo) semanticVisits <- IORef.readIORef (memoSemanticValidationVisits memo) objectVisits <- IORef.readIORef (memoObjectValidationVisits memo) propositionVisits <- IORef.readIORef (memoPropositionValidationVisits memo) artifactVisits <- IORef.readIORef (memoArtifactValidationVisits memo) pure StoreMemoVisits { storeArtifactRowsDecoded = Map.size artifactRows , storeSyntaxRowsDecoded = Map.size syntaxRows , storeSyntaxRowsValidated = syntaxVisits , storeSemanticRowsDecoded = Map.size semanticRows , storeSemanticRowsValidated = semanticVisits , storeObjectRowsDecoded = Map.size objectRows , storeObjectRowsValidated = objectVisits , storePropositionRowsDecoded = Map.size propositionRows , storePropositionRowsValidated = propositionVisits , storeArtifactsValidated = artifactVisits } data StoreSelection = DefaultStore | ExplicitStore !FilePath | FreshTemporaryStore deriving stock (Show, Eq) data StorePlan = DefaultStorePlan !StorePath | ExplicitStorePlan !StorePath | FreshStorePlan deriving stock (Show, Eq) newtype StorePath = StorePath FilePath deriving stock (Show, Eq, Ord) storePathFilePath :: StorePath -> FilePath storePathFilePath (StorePath path) = path storeRollbackJournalPath :: StorePath -> FilePath storeRollbackJournalPath storePath = storePathFilePath storePath <> "-journal" data StorePlanningError = StorePathResolutionFailed !FilePath !Text | ExplicitStoreParentMissing !FilePath | ExplicitStoreParentNotDirectory !FilePath deriving stock (Show, Eq) renderStorePlanningError :: StorePlanningError -> Text renderStorePlanningError = \case StorePathResolutionFailed path reason -> "could not resolve store path " <> quotePath path <> ": " <> reason ExplicitStoreParentMissing parent -> "the parent of --store does not exist: " <> quotePath parent ExplicitStoreParentNotDirectory parent -> "the parent of --store is not a directory: " <> quotePath parent data StoreLease = StoreLease !StorePlan !StorePath storeLeasePath :: StoreLease -> StorePath storeLeasePath (StoreLease _plan path) = path data StoreLifecycleError = StoreParentCreationFailed !FilePath !Text | StoreLifecycleOpenFailed !StoreOpenError | StoreCloseFailed !StoreFailure deriving stock (Show, Eq) renderStoreLifecycleError :: StoreLifecycleError -> Text renderStoreLifecycleError = \case StoreParentCreationFailed parent reason -> "could not create default store directory " <> quotePath parent <> ": " <> reason StoreLifecycleOpenFailed failure -> renderStoreOpenError failure StoreCloseFailed failure -> "could not close the selected store: " <> renderStoreFailure failure data StoreStartup = InitializedNewStore | OpenedCurrentStore deriving stock (Show, Eq) planStore :: StoreSelection -> IO (Either StorePlanningError StorePlan) planStore = \case DefaultStore -> do resolved <- trySynchronous do cacheDirectory <- Directory.getXdgDirectory Directory.XdgCache "felix" normalizeAbsolutePath (cacheDirectory Posix. "store.sqlite") pure (case resolved of Left failure -> Left (StorePathResolutionFailed "felix/store.sqlite" (exceptionText failure)) Right path -> Right (DefaultStorePlan (StorePath path))) ExplicitStore requested -> do resolved <- trySynchronous (normalizeAbsolutePath requested) case resolved of Left failure -> pure (Left (StorePathResolutionFailed requested (exceptionText failure))) Right path -> do let parent = Posix.takeDirectory path inspected <- trySynchronous do exists <- Directory.doesPathExist parent directory <- Directory.doesDirectoryExist parent pure (exists, directory) pure (case inspected of Left failure -> Left (StorePathResolutionFailed parent (exceptionText failure)) Right (False, _isDirectory) -> Left (ExplicitStoreParentMissing parent) Right (True, False) -> Left (ExplicitStoreParentNotDirectory parent) Right (True, True) -> Right (ExplicitStorePlan (StorePath path))) FreshTemporaryStore -> pure (Right FreshStorePlan) withStoreLease :: StorePlan -> (StoreLease -> IO value) -> IO value withStoreLease plan action = case plan of DefaultStorePlan path -> action (StoreLease plan path) ExplicitStorePlan path -> action (StoreLease plan path) FreshStorePlan -> Temp.withSystemTempDirectory "felix-store" \directory -> do path <- normalizeAbsolutePath (directory Posix. "store.sqlite") action (StoreLease plan (StorePath path)) withOpenStore :: StoreLease -> TheoryId -> (StoreStartup -> Store -> IO value) -> IO (Either StoreLifecycleError value) withOpenStore (StoreLease plan path@(StorePath filePath)) theory action = do prepared <- prepareStoreParent plan path case prepared of Left failure -> pure (Left failure) Right () -> Exception.mask \restore -> do opened <- restore (openStore filePath theory) case opened of Left failure -> pure (Left (StoreLifecycleOpenFailed failure)) Right (startup, store) -> do result <- Exception.try (restore (action startup store)) closed <- trySynchronous (closeStore store) case result of Left failure -> Exception.throwIO (failure :: Exception.SomeException) Right value -> pure (case closed of Left failure -> Left (StoreCloseFailed (operationFailure "close store" failure)) Right () -> Right value) prepareStoreParent :: StorePlan -> StorePath -> IO (Either StoreLifecycleError ()) prepareStoreParent plan (StorePath path) = case plan of DefaultStorePlan _ -> do let parent = Posix.takeDirectory path created <- trySynchronous (Directory.createDirectoryIfMissing True parent) pure (case created of Left failure -> Left (StoreParentCreationFailed parent (exceptionText failure)) Right () -> Right ()) ExplicitStorePlan _ -> pure (Right ()) FreshStorePlan -> pure (Right ()) normalizeAbsolutePath :: FilePath -> IO FilePath normalizeAbsolutePath path = Posix.normalise <$> Directory.makeAbsolute path data StoreCompatibility = StoreCompatibility !CacheEpoch !TheoryId deriving stock (Show, Eq) currentStoreCompatibility :: TheoryId -> StoreCompatibility currentStoreCompatibility = StoreCompatibility currentCacheEpoch data StoreIncompatibility = StoreCompatibilityMissing | StoreCompatibilityMalformed !Text | StoreCompatibilityMismatch !StoreCompatibility !StoreCompatibility deriving stock (Show, Eq) renderStoreIncompatibility :: StoreIncompatibility -> Text renderStoreIncompatibility = \case StoreCompatibilityMissing -> "compatibility metadata is missing" StoreCompatibilityMalformed reason -> "compatibility metadata is malformed: " <> reason StoreCompatibilityMismatch expected actual -> "compatibility differs: expected " <> renderCompatibility expected <> ", found " <> renderCompatibility actual renderCompatibility :: StoreCompatibility -> Text renderCompatibility (StoreCompatibility epoch theory) = "cache epoch " <> Text.pack (show (cacheEpochValue epoch)) <> " and theory " <> Text.pack (show theory) data StoreOpenError = IncompatibleStore !StoreIncompatibility | FatalStoreStartup !StoreFailure deriving stock (Show, Eq) renderStoreOpenError :: StoreOpenError -> Text renderStoreOpenError = \case IncompatibleStore incompatibility -> renderStoreIncompatibility incompatibility FatalStoreStartup failure -> renderStoreFailure failure data StoreRelation = CanonicalObjects | CanonicalPropositions | ProofValidations | DeclarationValidations | SyntaxInterfaces | SemanticInterfaces | ModuleArtifacts | ParsedArtifacts deriving stock (Show, Eq, Ord) data StoreFailure = StoreOperationFailed !Text !Text | StoreSchemaIntegrityFailure !Text | StoreConfigurationFailure !Text | StoreRowPayloadMismatch !StoreRelation !ByteString | StoreRowDecodeFailure !StoreRelation !ByteString !CacheDecodeError | StoreObjectValidationFailure !ObjectValidationError | StorePropositionValidationFailure !PropositionValidationError | StoreValidationRecordKeyMismatch !StoreRelation | StoreInterfaceIdMismatch !StoreRelation | StoreSyntaxInterfaceValidationFailure !Syntax.SyntaxInterfaceError | StoreSemanticInterfaceValidationFailure !SemanticInterfaceError | StoreModuleArtifactIdMismatch | StoreParsedArtifactIdMismatch | StoreModuleArtifactColumnsMismatch | StoreModuleArtifactSyntaxMismatch !Syntax.SyntaxInterfaceId !Syntax.SyntaxInterfaceId | StoreModuleArtifactOwnerMismatch !ModuleName !ModuleName | StoreModuleArtifactDirectMismatch ![SemanticInterfaceId] ![SemanticInterfaceId] | StoreModuleArtifactTheoryMismatch !TheoryId !TheoryId | StoreModulePrefixFailure !PrefixContextError | StoreModulePrefixMismatch | StoreImportedOccurrenceValidationFailure !Materialization.MaterializationError | StoreSemanticAliasTargetMissing !SemanticFactOccurrenceFingerprint | StoreSemanticAliasCollision !SemanticName | StoreSemanticGlobalTargetFailure !SemanticGlobalKey !SemanticGlobalTarget !SemanticGlobalTargetError | StoreSemanticGlobalCollision !SemanticGlobalKey !SemanticGlobalTarget !SemanticGlobalTarget | StoreAssertedChildMissing !StoreRelation !ByteString deriving stock (Show, Eq) renderStoreFailure :: StoreFailure -> Text renderStoreFailure = \case StoreOperationFailed operation reason -> operation <> " failed: " <> reason StoreSchemaIntegrityFailure reason -> "current store schema is incomplete or inconsistent: " <> reason StoreConfigurationFailure reason -> "could not configure the current store: " <> reason StoreRowPayloadMismatch relation _key -> "stored canonical payload disagrees with an equal key in " <> renderStoreRelation relation StoreRowDecodeFailure relation _key _failure -> "stored canonical payload is malformed in " <> renderStoreRelation relation StoreObjectValidationFailure{} -> "stored canonical object failed identity validation" StorePropositionValidationFailure{} -> "stored canonical proposition failed identity validation" StoreValidationRecordKeyMismatch relation -> "stored validation row has the wrong key in " <> renderStoreRelation relation StoreInterfaceIdMismatch relation -> "stored interface row has the wrong asserted identity in " <> renderStoreRelation relation StoreSyntaxInterfaceValidationFailure failure -> "supplied syntax interface failed validation: " <> Text.pack (show failure) StoreSemanticInterfaceValidationFailure failure -> "supplied semantic interface failed validation: " <> Text.pack (show failure) StoreModuleArtifactIdMismatch -> "stored module artifact row has the wrong identity" StoreParsedArtifactIdMismatch -> "parsed artifact identity disagrees with its key and payload" StoreModuleArtifactColumnsMismatch -> "stored module artifact columns disagree with its canonical payload" StoreModuleArtifactSyntaxMismatch{} -> "stored module artifact does not match the current syntax interface" StoreModuleArtifactOwnerMismatch{} -> "stored module artifact has the wrong semantic owner" StoreModuleArtifactDirectMismatch{} -> "stored module artifact has the wrong direct semantic inputs" StoreModuleArtifactTheoryMismatch{} -> "stored module artifact belongs to a different theory" StoreModulePrefixFailure{} -> "stored module artifact has an invalid initial prefix" StoreModulePrefixMismatch -> "published module prefix does not match its semantic interface" StoreImportedOccurrenceValidationFailure{} -> "stored semantic occurrence failed authority validation" StoreSemanticAliasTargetMissing{} -> "stored semantic alias targets a missing occurrence" StoreSemanticAliasCollision{} -> "stored semantic aliases conflict across the import closure" StoreSemanticGlobalTargetFailure{} -> "stored semantic global has an invalid target" StoreSemanticGlobalCollision{} -> "stored semantic globals conflict across the import closure" StoreAssertedChildMissing relation _key -> "a module row asserts a missing child in " <> renderStoreRelation relation renderStoreRelation :: StoreRelation -> Text renderStoreRelation = \case CanonicalObjects -> "canonical_objects" CanonicalPropositions -> "canonical_propositions" ProofValidations -> "proof_validations" DeclarationValidations -> "declaration_validations" SyntaxInterfaces -> "syntax_interfaces" SemanticInterfaces -> "semantic_interfaces" ModuleArtifacts -> "module_artifacts" ParsedArtifacts -> "parsed_artifacts" quotePath :: FilePath -> Text quotePath = Text.pack . show newtype StoreAbort = StoreAbort StoreFailure deriving stock (Show) instance Exception.Exception StoreAbort openStore :: FilePath -> TheoryId -> IO (Either StoreOpenError (StoreStartup, Store)) openStore path theory = Exception.mask \restore -> do opened <- trySynchronous (SQLite.open path) case opened of Left failure -> pure (Left (FatalStoreStartup (operationFailure "open store" failure))) Right connection -> do startup <- trySynchronous (restore (classifyAndStart connection theory)) `Exception.onException` closeIgnoringFailure connection case startup of Left failure -> do closeIgnoringFailure connection pure (Left (FatalStoreStartup (operationFailure "start store" failure))) Right (Left openError) -> do closeIgnoringFailure connection pure (Left openError) Right (Right status) -> pure (Right ( status , Store path theory connection )) closeStore :: Store -> IO () closeStore (Store _path _theory connection) = SQLite.close connection classifyAndStart :: SQLite.Connection -> TheoryId -> IO (Either StoreOpenError StoreStartup) classifyAndStart connection theory = do objects <- userSchemaObjects connection if null objects then do SQLite.withTransaction connection (initializeSchema connection theory) schema <- validateCurrentSchema connection case schema of Left failure -> pure (Left (FatalStoreStartup failure)) Right () -> do configuration <- configureConnection connection pure (case configuration of Left failure -> Left (FatalStoreStartup failure) Right () -> Right InitializedNewStore) else do compatibility <- readExistingCompatibility connection objects case compatibility of Left incompatibility -> pure (Left (IncompatibleStore incompatibility)) Right actual | actual /= expected -> pure (Left (IncompatibleStore (StoreCompatibilityMismatch expected actual))) | otherwise -> do schema <- validateCurrentSchema connection case schema of Left failure -> pure (Left (FatalStoreStartup failure)) Right () -> do configuration <- configureConnection connection pure (case configuration of Left failure -> Left (FatalStoreStartup failure) Right () -> Right OpenedCurrentStore) where expected = currentStoreCompatibility theory userSchemaObjects :: SQLite.Connection -> IO [Text] userSchemaObjects connection = fmap (\(Only value) -> value) <$> (SQLite.query_ connection "SELECT name FROM sqlite_master \ \WHERE type IN ('table', 'index', 'view', 'trigger') \ \AND name NOT LIKE 'sqlite_%' ORDER BY type, name" :: IO [Only Text]) readExistingCompatibility :: SQLite.Connection -> [Text] -> IO (Either StoreIncompatibility StoreCompatibility) readExistingCompatibility connection objects | compatibilityTableName `notElem` objects = pure (Left StoreCompatibilityMissing) | otherwise = do shapeResult <- trySynchronous (SQLite.query_ connection "SELECT typeof(cache_epoch), typeof(theory_id) \ \FROM store_compatibility ORDER BY singleton" :: IO [(Text, Text)]) case shapeResult of Left failure -> pure (Left (StoreCompatibilityMalformed (exceptionText failure))) Right [("integer", "blob")] -> do rowResult <- trySynchronous (SQLite.query_ connection "SELECT cache_epoch, theory_id \ \FROM store_compatibility ORDER BY singleton" :: IO [(Int64, ByteString)]) pure (case rowResult of Left failure -> Left (StoreCompatibilityMalformed (exceptionText failure)) Right [row] -> decodeCompatibility row Right rows -> Left (StoreCompatibilityMalformed ("expected one compatibility row, found " <> Text.pack (show (length rows))))) Right rows -> pure (Left (StoreCompatibilityMalformed ("unexpected compatibility field types: " <> Text.pack (show rows)))) decodeCompatibility :: (Int64, ByteString) -> Either StoreIncompatibility StoreCompatibility decodeCompatibility (epoch, theoryBytes) | epoch < 0 || toInteger epoch > toInteger (maxBound :: Word32) = Left (StoreCompatibilityMalformed "cache epoch is outside the Word32 range") | otherwise = case decodeCache getTheoryIdCache theoryBytes of Left failure -> Left (StoreCompatibilityMalformed (Text.pack (show failure))) Right theory -> Right (StoreCompatibility (cacheEpochFromValue (fromIntegral epoch)) theory) initializeSchema :: SQLite.Connection -> TheoryId -> IO () initializeSchema connection theory = do traverse_ (SQLite.execute_ connection . schemaQuery . snd) schemaStatements SQLite.execute connection "INSERT INTO store_compatibility \ \(singleton, cache_epoch, theory_id) VALUES (1, ?, ?)" ( fromIntegral (cacheEpochValue currentCacheEpoch) :: Int64 , encodeCache (putTheoryIdCache theory) ) validateCurrentSchema :: SQLite.Connection -> IO (Either StoreFailure ()) validateCurrentSchema connection = do actual <- SQLite.query_ connection "SELECT name, sql FROM sqlite_master \ \WHERE type = 'table' AND name NOT LIKE 'sqlite_%' \ \ORDER BY name" :: IO [(Text, Text)] let expected = Map.fromList [ (name, normalizeSchema statement) | (name, statement) <- schemaStatements ] found = Map.fromList [ (name, normalizeSchema statement) | (name, statement) <- actual ] pure (if found == expected then Right () else Left (StoreSchemaIntegrityFailure (schemaDifference expected found))) configureConnection :: SQLite.Connection -> IO (Either StoreFailure ()) configureConnection connection = do journal <- SQLite.query_ connection "PRAGMA journal_mode = DELETE" :: IO [Only Text] SQLite.execute_ connection "PRAGMA synchronous = NORMAL" synchronous <- SQLite.query_ connection "PRAGMA synchronous" :: IO [Only Int] SQLite.execute_ connection "PRAGMA foreign_keys = ON" foreignKeys <- SQLite.query_ connection "PRAGMA foreign_keys" :: IO [Only Int] pure do unless (journal == [Only "delete"]) (Left (StoreConfigurationFailure ("unexpected journal mode: " <> Text.pack (show journal)))) unless (synchronous == [Only 1]) (Left (StoreConfigurationFailure ("unexpected synchronous mode: " <> Text.pack (show synchronous)))) unless (foreignKeys == [Only 1]) (Left (StoreConfigurationFailure ("foreign keys were not enabled: " <> Text.pack (show foreignKeys)))) writeCanonicalRows :: Store -> [AssertedObject] -> [CheckedPropositionContent] -> Except.ExceptT StoreFailure IO () writeCanonicalRows store objects propositions = do let Store _path theory connection = store proposed <- Except.liftEither (indexProposedObjects objects) stored <- loadReferencedObjects store proposed (Set.unions ( (objectReferences . assertedObjectContent <$> objects) <> (termReferences . frozenCoreTerm . checkedPropositionTerm <$> propositions) )) closure <- Except.liftEither (first StoreObjectValidationFailure (validateObjectClosure theory (Map.elems proposed <> Map.elems stored))) checkedPropositions <- traverse (Except.liftEither . first StorePropositionValidationFailure . revalidateProposition closure) propositions traverse_ (insertObject connection) objects traverse_ (insertProposition connection) checkedPropositions loadCanonicalObject :: Store -> ObjectId -> IO (Either StoreFailure (Maybe AssertedObject)) loadCanonicalObject store identity = runStoreOperation "load canonical object" do root <- Except.runExceptT (loadObjectRow store identity) case root of Left failure -> throwIO (StoreAbort failure) Right Nothing -> pure Nothing Right (Just asserted) -> do let proposed = Map.singleton identity asserted storedResult <- Except.runExceptT (loadReferencedObjects store proposed (objectReferences (assertedObjectContent asserted))) stored <- either (throwIO . StoreAbort) pure storedResult closure <- either (throwIO . StoreAbort . StoreObjectValidationFailure) pure (validateObjectClosure theory (asserted : Map.elems stored)) pure (assertedObject identity <$> lookupCheckedObjectContent identity closure) where Store _path theory _connection = store loadCanonicalProposition :: Store -> PropositionId -> IO (Either StoreFailure (Maybe CheckedPropositionContent)) loadCanonicalProposition store identity = runStoreOperation "load canonical proposition" do rowResult <- Except.runExceptT (loadPayload CanonicalPropositions propositionSelect (encodeCache (putPropositionIdCache identity)) connection) row <- either (throwIO . StoreAbort) pure rowResult case row of Nothing -> pure Nothing Just payload -> do term <- either (throwIO . StoreAbort . StoreRowDecodeFailure CanonicalPropositions (encodeCache (putPropositionIdCache identity))) pure (decodeCache (getCanonicalTermCache getObjectIdCache) payload) storedResult <- Except.runExceptT (loadReferencedObjects store Map.empty (termReferences term)) stored <- either (throwIO . StoreAbort) pure storedResult closure <- either (throwIO . StoreAbort . StoreObjectValidationFailure) pure (validateObjectClosure theory (Map.elems stored)) Just <$> either (throwIO . StoreAbort . StorePropositionValidationFailure) pure (validateAssertedPropositionContent closure identity term) where Store _path theory connection = store loadProofValidation :: Store -> ProofValidationKey -> IO (Either StoreFailure (Maybe ProofValidationRecord)) loadProofValidation store key = loadExactTyped store ProofValidations (cacheDigestBytes (proofValidationKeyDigest key)) proofValidationSelect getProofValidationRecordCache (\record -> proofValidationRecordKey record == key) StoreValidationRecordKeyMismatch loadDeclarationValidation :: Store -> DeclarationValidationKey -> IO (Either StoreFailure (Maybe DeclarationValidationRecord)) loadDeclarationValidation store key = loadExactTyped store DeclarationValidations (cacheDigestBytes (declarationValidationKeyDigest key)) declarationValidationSelect getDeclarationValidationRecordCache (\record -> declarationValidationRecordKey record == key) StoreValidationRecordKeyMismatch loadParsedArtifact :: Store -> Parsed.ParsedModuleKey -> IO (Either StoreFailure (Maybe ParsedPayload.ParsedArtifact)) loadParsedArtifact (Store _path _theory connection) key = runStoreOperation "load parsed artifact" do result <- Except.runExceptT do let encodedKey = cacheDigestBytes (Parsed.parsedModuleKeyDigest key) rows <- liftIO (SQLite.query connection parsedArtifactSelect (Only encodedKey) :: IO [(ByteString, ByteString)]) case rows of [] -> pure Nothing [(encodedIdentity, encodedPayload)] -> do claimedIdentity <- Except.liftEither (first (StoreRowDecodeFailure ParsedArtifacts encodedKey) (decodeCache Parsed.getParsedModuleIdCache encodedIdentity)) payload <- Except.liftEither (first (StoreRowDecodeFailure ParsedArtifacts encodedKey) (ParsedPayload.canonicalParsedPayloadFromBytes encodedPayload)) let artifact = ParsedPayload.parsedArtifact key payload unless (claimedIdentity == ParsedPayload.parsedArtifactId artifact) (Except.throwError StoreParsedArtifactIdMismatch) pure (Just artifact) _ -> Except.throwError (StoreSchemaIntegrityFailure "primary key returned several parsed artifact rows") either (throwIO . StoreAbort) pure result writeParsedArtifact :: Store -> Parsed.ParsedModuleKey -> ParsedPayload.ParsedArtifact -> IO (Either StoreFailure ParsedPayload.ParsedArtifact) writeParsedArtifact (Store _path _theory connection) key artifact = runStoreOperation "write parsed artifact" do SQLite.withTransaction connection do outcome <- Except.runExceptT do let payload = ParsedPayload.parsedArtifactPayload artifact checked = ParsedPayload.parsedArtifact key payload unless (ParsedPayload.parsedArtifactId artifact == ParsedPayload.parsedArtifactId checked) (Except.throwError StoreParsedArtifactIdMismatch) insertParsedArtifact connection key checked either (throwIO . StoreAbort) (const (pure artifact)) outcome loadSyntaxInterface :: Store -> Syntax.SyntaxInterfaceId -> IO (Either StoreFailure (Maybe Syntax.ModuleSyntaxInterface)) loadSyntaxInterface store key = loadExactTyped store SyntaxInterfaces (cacheDigestBytes (Syntax.syntaxInterfaceIdDigest key)) syntaxInterfaceSelect Syntax.getModuleSyntaxInterfaceCache (\interface -> Syntax.moduleSyntaxAssertedId interface == key) StoreInterfaceIdMismatch loadSemanticInterface :: Store -> SemanticInterfaceId -> IO (Either StoreFailure (Maybe SemanticInterface)) loadSemanticInterface store key = loadExactTyped store SemanticInterfaces (cacheDigestBytes (semanticInterfaceIdDigest key)) semanticInterfaceSelect getSemanticInterfaceCache (\interface -> semanticInterfaceAssertedId interface == key) StoreInterfaceIdMismatch loadModuleArtifactResult :: Store -> ModuleArtifactId -> IO (Either StoreFailure (Maybe ModuleArtifactResult)) loadModuleArtifactResult (Store _path _theory connection) key = runStoreOperation "load module artifact" do result <- Except.runExceptT (loadModuleArtifactRow connection key) either (throwIO . StoreAbort) pure result loadModuleArtifactRow :: SQLite.Connection -> ModuleArtifactId -> Except.ExceptT StoreFailure IO (Maybe ModuleArtifactResult) loadModuleArtifactRow connection key = do let encodedKey = cacheDigestBytes (moduleArtifactIdDigest key) rows <- liftIO (SQLite.query connection moduleArtifactSelect (Only encodedKey) :: IO [(ByteString, ByteString, ByteString)]) case rows of [] -> pure Nothing [(syntaxColumn, semanticColumn, payload)] -> do result <- Except.liftEither (first (StoreRowDecodeFailure ModuleArtifacts encodedKey) (decodeCache (getModuleArtifactResultCache key) payload)) unless (moduleArtifactResultId result == key) (Except.throwError StoreModuleArtifactIdMismatch) let expectedSyntax = cacheDigestBytes (Syntax.syntaxInterfaceIdDigest (moduleArtifactResultSyntax result)) expectedSemantic = cacheDigestBytes (semanticInterfaceIdDigest (moduleArtifactResultSemantic result)) unless (syntaxColumn == expectedSyntax && semanticColumn == expectedSemantic) (Except.throwError StoreModuleArtifactColumnsMismatch) pure (Just result) _ -> Except.throwError (StoreSchemaIntegrityFailure "primary key returned several module artifact rows") -- | Validate one exact current module hit before returning any data that can -- be adopted as runtime authority. loadCachedModuleInstallation :: StoreMemo -> Store -> ModuleArtifactKey -> Syntax.SyntaxInterfaceId -> IO (Either StoreFailure (Maybe CachedModuleInstallation)) loadCachedModuleInstallation memo store expectedKey expectedSyntax = do let expectedArtifact = moduleArtifactId expectedKey Store _path storeTheory _connection = store if moduleArtifactKeyTheory expectedKey /= storeTheory then pure (Left (StoreModuleArtifactTheoryMismatch storeTheory (moduleArtifactKeyTheory expectedKey))) else validateModuleArtifactClosure memo store expectedArtifact >>= \case Left failure -> pure (Left failure) Right Nothing -> pure (Right Nothing) Right (Just artifact) | moduleArtifactResultSyntax artifact /= expectedSyntax -> pure (Left (StoreModuleArtifactSyntaxMismatch expectedSyntax (moduleArtifactResultSyntax artifact))) | otherwise -> do loaded <- loadValidatedModuleForImport memo store expectedArtifact case loaded of Left failure -> pure (Left failure) Right Nothing -> pure (Left (StoreAssertedChildMissing ModuleArtifacts (cacheDigestBytes (moduleArtifactIdDigest expectedArtifact)))) Right (Just (semantic, objects, propositions)) -> finish semantic objects propositions where finish semantic objects propositions | semanticInterfaceOwner semantic /= moduleArtifactKeyOwner expectedKey = pure (Left (StoreModuleArtifactOwnerMismatch (moduleArtifactKeyOwner expectedKey) (semanticInterfaceOwner semantic))) | semanticInterfaceDirectInputs semantic /= moduleArtifactKeyDirectSemanticInputs expectedKey = pure (Left (StoreModuleArtifactDirectMismatch (moduleArtifactKeyDirectSemanticInputs expectedKey) (semanticInterfaceDirectInputs semantic))) | otherwise = do syntaxResult <- memoSyntax memo store expectedSyntax case syntaxResult of Left failure -> pure (Left failure) Right Nothing -> pure (Left (StoreAssertedChildMissing SyntaxInterfaces (cacheDigestBytes (Syntax.syntaxInterfaceIdDigest expectedSyntax)))) Right (Just syntax) -> pure do initial <- first StoreModulePrefixFailure (initialPrefixContextId (moduleArtifactKeyTheory expectedKey) (moduleArtifactKeyOwner expectedKey) (moduleArtifactKeyDirectSemanticInputs expectedKey)) let final = foldl' nextPrefixContextId initial (semanticInterfaceDeclarations semantic) pure (Just (CachedModuleInstallation syntax semantic objects propositions final)) -- | Flush only completed declaration batches. This operation does not make -- any interface or module root visible to importers. writePendingModulePrefix :: Store -> Declaration.PendingModulePrefix -> IO (Either StoreFailure ()) writePendingModulePrefix store prefix = runStoreOperation "write pending module prefix" do SQLite.withTransaction connection do outcome <- Except.runExceptT do writeCanonicalRows store objects propositions traverse_ (insertProofValidation connection) proofValidations traverse_ (insertDeclarationValidation connection) declarationValidations either (throwIO . StoreAbort) pure outcome where Store _path _theory connection = store batches = Declaration.pendingModulePrefixBatches prefix objects = concatMap Declaration.committedBatchObjects batches propositions = concatMap Declaration.committedBatchPropositions batches proofValidations = concatMap Declaration.committedBatchProofValidations batches declarationValidations = [ validation | batch <- batches , Just validation <- [Declaration.committedBatchDeclarationValidation batch] ] -- | Publish a completed prefix and its sealed interface/root as one short -- transaction. The supplied interface lists are the rows needed by the -- module root; each is checked by its canonical validator before insertion. writeSealedModule :: Store -> Declaration.PendingModulePrefix -> [Syntax.ModuleSyntaxInterface] -> [SemanticInterface] -> ModuleArtifactResult -> IO (Either StoreFailure ModuleArtifactResult) writeSealedModule store prefix syntaxInterfaces semanticInterfaces artifact = runStoreOperation "write sealed module" do SQLite.withTransaction connection do outcome <- Except.runExceptT do writeCanonicalRows store objects propositions traverse_ validateSuppliedSyntaxInterface syntaxInterfaces traverse_ validateSuppliedSemanticInterface semanticInterfaces traverse_ (validateSyntaxInputs store syntaxInterfaces) syntaxInterfaces traverse_ (validateSemanticInputs store semanticInterfaces) semanticInterfaces requireSyntax store syntaxInterfaces (moduleArtifactResultSyntax artifact) requireSemantic store semanticInterfaces (moduleArtifactResultSemantic artifact) rootSemantic <- maybe (Except.throwError StoreModulePrefixMismatch) pure (find ((== moduleArtifactResultSemantic artifact) . semanticInterfaceAssertedId) semanticInterfaces) validatePublishedPrefix rootSemantic traverse_ (insertProofValidation connection) proofValidations traverse_ (insertDeclarationValidation connection) declarationValidations traverse_ (insertSyntaxInterface connection) syntaxInterfaces traverse_ (insertSemanticInterface connection) semanticInterfaces insertModuleArtifact connection artifact either (throwIO . StoreAbort) (const (pure artifact)) outcome where Store _path theory connection = store batches = Declaration.pendingModulePrefixBatches prefix objects = concatMap Declaration.committedBatchObjects batches propositions = concatMap Declaration.committedBatchPropositions batches proofValidations = concatMap Declaration.committedBatchProofValidations batches declarationValidations = [ validation | batch <- batches , Just validation <- [Declaration.committedBatchDeclarationValidation batch] ] validateSuppliedSyntaxInterface interface = Except.liftEither (first StoreSyntaxInterfaceValidationFailure (Syntax.validateModuleSyntaxInterface (Syntax.moduleSyntaxBase interface) (Syntax.moduleSyntaxDirectInputs interface) (Syntax.moduleSyntaxLocalDelta interface) (Syntax.moduleSyntaxAssertedId interface))) validateSuppliedSemanticInterface interface = Except.liftEither (first StoreSemanticInterfaceValidationFailure (validateSemanticInterface (semanticInterfaceOwner interface) (semanticInterfaceDirectInputs interface) (semanticInterfaceDeclarations interface) (semanticInterfaceAssertedId interface))) validatePublishedPrefix interface = do initial <- Except.liftEither (first StoreModulePrefixFailure (initialPrefixContextId theory (semanticInterfaceOwner interface) (semanticInterfaceDirectInputs interface))) let declarations = semanticInterfaceDeclarations interface publishedBatches = Declaration.pendingModulePrefixBatches prefix expectedFinal = foldl' nextPrefixContextId initial declarations unless ( (Declaration.committedBatchDelta <$> publishedBatches) == declarations && Declaration.pendingModulePrefixCurrent prefix == expectedFinal ) (Except.throwError StoreModulePrefixMismatch) validateSyntaxInputs :: Store -> [Syntax.ModuleSyntaxInterface] -> Syntax.ModuleSyntaxInterface -> Except.ExceptT StoreFailure IO () validateSyntaxInputs store supplied interface = do traverse_ (requireSyntax store supplied) (Syntax.moduleSyntaxDirectInputs interface) requireSyntax :: Store -> [Syntax.ModuleSyntaxInterface] -> Syntax.SyntaxInterfaceId -> Except.ExceptT StoreFailure IO () requireSyntax store supplied identity = do let local = find ((== identity) . Syntax.moduleSyntaxAssertedId) supplied case local of Just _ -> pure () Nothing -> do loaded <- Except.liftIO (loadSyntaxInterface store identity) case loaded of Left failure -> Except.throwError failure Right (Just _) -> pure () Right Nothing -> Except.throwError (StoreAssertedChildMissing SyntaxInterfaces (cacheDigestBytes (Syntax.syntaxInterfaceIdDigest identity))) validateSemanticInputs :: Store -> [SemanticInterface] -> SemanticInterface -> Except.ExceptT StoreFailure IO () validateSemanticInputs store supplied interface = do traverse_ (requireSemantic store supplied) (semanticInterfaceDirectInputs interface) let declarations = semanticInterfaceDeclarations interface objectIds = concatMap declarationDeltaObjects declarations <> [ semanticGlobalTargetObject (semanticGlobalBindingTarget binding) | declaration <- declarations , binding <- semanticEnvironmentBindings (declarationDeltaEnvironment declaration) ] propositionIds = concatMap declarationDeltaPropositions declarations <> [ semanticFactProposition occurrence | declaration <- declarations , occurrence <- declarationDeltaFacts declaration ] traverse_ (requireObject store) (nubOrd objectIds) traverse_ (requireProposition store) (nubOrd propositionIds) requireSemantic :: Store -> [SemanticInterface] -> SemanticInterfaceId -> Except.ExceptT StoreFailure IO () requireSemantic store supplied identity = do let local = find ((== identity) . semanticInterfaceAssertedId) supplied case local of Just _ -> pure () Nothing -> do loaded <- Except.liftIO (loadSemanticInterface store identity) case loaded of Left failure -> Except.throwError failure Right (Just _) -> pure () Right Nothing -> Except.throwError (StoreAssertedChildMissing SemanticInterfaces (cacheDigestBytes (semanticInterfaceIdDigest identity))) requireObject :: Store -> ObjectId -> Except.ExceptT StoreFailure IO () requireObject store identity = do loaded <- Except.liftIO (loadCanonicalObject store identity) case loaded of Left failure -> Except.throwError failure Right (Just _) -> pure () Right Nothing -> Except.throwError (StoreAssertedChildMissing CanonicalObjects (encodeCache (putObjectIdCache identity))) requireProposition :: Store -> PropositionId -> Except.ExceptT StoreFailure IO () requireProposition store identity = do loaded <- Except.liftIO (loadCanonicalProposition store identity) case loaded of Left failure -> Except.throwError failure Right (Just _) -> pure () Right Nothing -> Except.throwError (StoreAssertedChildMissing CanonicalPropositions (encodeCache (putPropositionIdCache identity))) loadExactTyped :: Store -> StoreRelation -> ByteString -> Query -> CacheGet value -> (value -> Bool) -> (StoreRelation -> StoreFailure) -> IO (Either StoreFailure (Maybe value)) loadExactTyped store relation key selectRow decoder validates identityFailure = runStoreOperation ("load " <> relationName relation) do row <- Except.runExceptT (loadPayload relation selectRow key connection) payload <- either (throwIO . StoreAbort) pure row case payload of Nothing -> pure Nothing Just bytes -> case decodeCache decoder bytes of Left failure -> throwIO (StoreAbort (StoreRowDecodeFailure relation key failure)) Right value | validates value -> pure (Just value) | otherwise -> throwIO (StoreAbort (identityFailure relation)) where Store _path _theory connection = store -- | Validate one complete module-artifact closure. Every successful decode -- (including an ordinary miss) is memoized for the lifetime of this -- invocation, so repeated roots and import diamonds do not re-enter the -- store boundary. validateModuleArtifactClosure :: StoreMemo -> Store -> ModuleArtifactId -> IO (Either StoreFailure (Maybe ModuleArtifactResult)) validateModuleArtifactClosure memo store root = do loaded <- memoArtifact memo store root case loaded of Left failure -> pure (Left failure) Right Nothing -> pure (Right Nothing) Right (Just artifact) -> do validated <- IORef.readIORef (memoValidatedArtifacts memo) if root `Set.member` validated then pure (Right (Just artifact)) else do IORef.modifyIORef' (memoArtifactValidationVisits memo) (+ 1) checked <- Except.runExceptT do validateSyntax Set.empty (moduleArtifactResultSyntax artifact) validateSemantic Set.empty (moduleArtifactResultSemantic artifact) void (validateSemanticInventory (moduleArtifactResultSemantic artifact)) case checked of Left failure -> pure (Left failure) Right () -> do IORef.modifyIORef' (memoValidatedArtifacts memo) (Set.insert root) pure (Right (Just artifact)) where validateSyntax path identity = do validated <- Except.liftIO (IORef.readIORef (memoValidatedSyntax memo)) if identity `Set.member` validated || identity `Set.member` path then pure () else do Except.liftIO (IORef.modifyIORef' (memoSyntaxValidationVisits memo) (+ 1)) interface <- requireMemo SyntaxInterfaces (cacheDigestBytes (Syntax.syntaxInterfaceIdDigest identity)) (memoSyntax memo store identity) traverse_ (validateSyntax (Set.insert identity path)) (Syntax.moduleSyntaxDirectInputs interface) Except.liftIO (IORef.modifyIORef' (memoValidatedSyntax memo) (Set.insert identity)) validateSemantic path identity = do validated <- Except.liftIO (IORef.readIORef (memoValidatedSemantic memo)) if identity `Set.member` validated || identity `Set.member` path then pure () else do Except.liftIO (IORef.modifyIORef' (memoSemanticValidationVisits memo) (+ 1)) interface <- requireMemo SemanticInterfaces (cacheDigestBytes (semanticInterfaceIdDigest identity)) (memoSemantic memo store identity) let declarations = semanticInterfaceDeclarations interface bindings = [ binding | declaration <- declarations , binding <- semanticEnvironmentBindings (declarationDeltaEnvironment declaration) ] objects = nubOrd ( concatMap declarationDeltaObjects declarations <> ( semanticGlobalTargetObject . semanticGlobalBindingTarget <$> bindings ) ) propositions = nubOrd ( concatMap declarationDeltaPropositions declarations <> [ semanticFactProposition occurrence | declaration <- declarations , occurrence <- declarationDeltaFacts declaration ] ) traverse_ (validateSemantic (Set.insert identity path)) (semanticInterfaceDirectInputs interface) operationBindings <- semanticOperationBindings Set.empty identity validateObjectRoots objects closure <- Except.liftIO (IORef.readIORef (memoCheckedObjects memo)) traverse_ (\binding -> Except.liftEither (first (StoreSemanticGlobalTargetFailure (semanticGlobalBindingKey binding) (semanticGlobalBindingTarget binding)) (validateSemanticGlobalBindingTarget operationBindings closure binding))) bindings traverse_ validateProposition propositions traverse_ validateOccurrence [ occurrence | declaration <- declarations , occurrence <- declarationDeltaFacts declaration ] Except.liftIO (IORef.modifyIORef' (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)) additions <- collectObjects (checkedObjectIds closure) Map.empty identities unless (Map.null additions) do Except.liftIO (IORef.modifyIORef' (memoObjectValidationVisits memo) (+ Map.size additions)) extended <- Except.liftEither (first StoreObjectValidationFailure (extendObjectClosure closure (Map.elems additions))) Except.liftIO (IORef.writeIORef (memoCheckedObjects memo) extended) collectObjects checked collected = \case [] -> pure collected identity : remaining | identity `Set.member` checked || Map.member identity collected -> collectObjects checked collected remaining | otherwise -> do asserted <- requireMemo CanonicalObjects (encodeCache (putObjectIdCache identity)) (memoObject memo store identity) let collected' = Map.insert identity asserted collected dependencies = Set.toAscList (objectReferences (assertedObjectContent asserted)) withDependencies <- collectObjects checked collected' dependencies collectObjects checked withDependencies remaining validateProposition identity = do validated <- Except.liftIO (IORef.readIORef (memoValidatedPropositions memo)) unless (Map.member identity validated) do Except.liftIO (IORef.modifyIORef' (memoPropositionValidationVisits memo) (+ 1)) term <- requireMemo CanonicalPropositions (encodeCache (putPropositionIdCache identity)) (memoPropositionRow memo store identity) validateObjectRoots (Set.toAscList (termReferences term)) closure <- Except.liftIO (IORef.readIORef (memoCheckedObjects memo)) proposition <- Except.liftEither (first StorePropositionValidationFailure (validateAssertedPropositionContent closure identity term)) Except.liftIO (IORef.modifyIORef' (memoValidatedPropositions memo) (Map.insert identity proposition)) checkedProposition identity = do validateProposition identity validated <- Except.liftIO (IORef.readIORef (memoValidatedPropositions memo)) case Map.lookup identity validated of Just proposition -> pure proposition Nothing -> impossible "validated proposition is absent" validateOccurrence occurrence = do proposition <- checkedProposition (semanticFactProposition occurrence) void (Except.liftEither (first StoreImportedOccurrenceValidationFailure (Materialization.checkImportedOccurrence theory (semanticFactFingerprint occurrence) occurrence proposition (semanticFactAuthority occurrence)))) 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 (semanticGlobalBindingKey binding) (semanticGlobalBindingTarget binding) globals insertGlobalBinding key target globals = case Map.lookup key globals of Nothing -> pure (Map.insert key target globals) Just existing | existing == target -> pure globals | otherwise -> Except.throwError (StoreSemanticGlobalCollision key existing target) insertAlias facts aliases alias = do let target = semanticAliasTarget alias unless (target `Set.member` facts) (Except.throwError (StoreSemanticAliasTargetMissing target)) insertNamedAlias (semanticAliasName alias) target aliases insertNamedAlias name target aliases = case Map.lookup name aliases of Nothing -> pure (Map.insert name target aliases) Just existing | existing == target -> pure aliases | otherwise -> Except.throwError (StoreSemanticAliasCollision name) requireMemo relation key loaded = do result <- Except.liftIO loaded case result of Left failure -> Except.throwError failure Right (Just value) -> pure value Right Nothing -> Except.throwError (StoreAssertedChildMissing relation key) Store _path theory _connection = store -- | Load the semantic payload needed for an importer only after the complete -- module-artifact closure has validated. The returned rows remain inert; -- Declaration creates fresh builder authority from them. loadValidatedModuleForImport :: StoreMemo -> Store -> ModuleArtifactId -> IO (Either StoreFailure (Maybe ( SemanticInterface , [AssertedObject] , [CheckedPropositionContent] ))) loadValidatedModuleForImport memo store root = do validateModuleArtifactClosure memo store root >>= \case Left failure -> pure (Left failure) Right Nothing -> pure (Right Nothing) Right (Just artifact) -> do semanticResult <- memoSemantic memo store (moduleArtifactResultSemantic artifact) case semanticResult of Left failure -> pure (Left failure) Right Nothing -> pure (Left (StoreAssertedChildMissing SemanticInterfaces (encodeCache (putSemanticInterfaceIdCache (moduleArtifactResultSemantic artifact))))) Right (Just semantic) -> do let declarations = semanticInterfaceDeclarations semantic propositionIds = nubOrd ( concatMap declarationDeltaPropositions declarations <> [ semanticFactProposition occurrence | declaration <- declarations , occurrence <- declarationDeltaFacts declaration ] ) objectIds = nubOrd (concatMap declarationDeltaObjects declarations) validatedPropositions <- IORef.readIORef (memoValidatedPropositions memo) case traverse (`Map.lookup` validatedPropositions) propositionIds of Nothing -> pure (Left (StoreSchemaIntegrityFailure "validated proposition evidence is absent")) Just propositions -> do loadedObjects <- traverse (memoObject memo store) objectIds case sequence loadedObjects of Left failure -> pure (Left failure) Right objects -> case sequence objects of Nothing -> pure (Left (StoreSchemaIntegrityFailure "validated object evidence is absent")) Just asserted -> pure (Right (Just ( semantic , asserted , propositions ))) memoArtifact :: StoreMemo -> Store -> ModuleArtifactId -> IO (Either StoreFailure (Maybe ModuleArtifactResult)) memoArtifact memo store identity = memoized (memoArtifactRows memo) identity (loadModuleArtifactResult store identity) memoSyntax :: StoreMemo -> Store -> Syntax.SyntaxInterfaceId -> IO (Either StoreFailure (Maybe Syntax.ModuleSyntaxInterface)) memoSyntax memo store identity = memoized (memoSyntaxRows memo) identity (loadSyntaxInterface store identity) memoSemantic :: StoreMemo -> Store -> SemanticInterfaceId -> IO (Either StoreFailure (Maybe SemanticInterface)) memoSemantic memo store identity = memoized (memoSemanticRows memo) identity (loadSemanticInterface store identity) memoObject :: StoreMemo -> Store -> ObjectId -> IO (Either StoreFailure (Maybe AssertedObject)) memoObject memo store identity = memoized (memoObjectRows memo) identity (loadShallowObject store identity) memoPropositionRow :: StoreMemo -> Store -> PropositionId -> IO (Either StoreFailure (Maybe (CanonicalTerm ObjectId))) memoPropositionRow memo store identity = memoized (memoPropositionRows memo) identity (loadShallowProposition store identity) loadShallowObject :: Store -> ObjectId -> IO (Either StoreFailure (Maybe AssertedObject)) loadShallowObject store@(Store _path theory _connection) identity = runStoreOperation "load shallow canonical object" do row <- Except.runExceptT (loadObjectRow store identity) asserted <- either (throwIO . StoreAbort) pure row traverse_ (\object -> either (throwIO . StoreAbort . StoreObjectValidationFailure) pure (validateObjectEnvelope theory object)) asserted pure asserted loadShallowProposition :: Store -> PropositionId -> IO (Either StoreFailure (Maybe (CanonicalTerm ObjectId))) loadShallowProposition (Store _path _theory connection) identity = runStoreOperation "load shallow canonical proposition" do result <- Except.runExceptT do let key = encodeCache (putPropositionIdCache identity) payload <- loadPayload CanonicalPropositions propositionSelect key connection traverse (\bytes -> do term <- Except.liftEither (first (StoreRowDecodeFailure CanonicalPropositions key) (decodeCache (getCanonicalTermCache getObjectIdCache) bytes)) let computed = propositionIdOf term unless (computed == identity) (Except.throwError (StorePropositionValidationFailure (PropositionIdPayloadMismatch identity computed))) pure term) payload either (throwIO . StoreAbort) pure result validateObjectEnvelope :: TheoryId -> AssertedObject -> Either ObjectValidationError () validateObjectEnvelope expectedTheory asserted = do let identity = assertedObjectId asserted content = assertedObjectContent asserted actualTheory = objectContentTheory content expectedFamily = case content of IntrinsicObjectContent{} -> IntrinsicObject TransparentObjectContent{} -> TransparentObject OpaqueObjectContent{} -> OpaqueObject actualFamily = objectIdFamily identity unless (actualTheory == expectedTheory) (Left (ObjectContentTheoryMismatch identity expectedTheory actualTheory)) unless (actualFamily == expectedFamily) (Left (ObjectContentFamilyMismatch identity expectedFamily actualFamily)) computed <- case content of IntrinsicObjectContent theory tag coreType -> do let requiredType = coreIntrinsicType tag unless (coreType == requiredType) (Left (IntrinsicObjectTypeMismatch identity tag requiredType coreType)) pure (intrinsicObjectId theory tag coreType) TransparentObjectContent theory coreType body -> pure (transparentObjectId theory coreType body) OpaqueObjectContent theory seed coreType -> pure (opaqueObjectId theory seed coreType) unless (identity == computed) (Left (ObjectIdPayloadMismatch identity computed)) memoized :: Ord key => IORef.IORef (Map key (Either StoreFailure (Maybe value))) -> key -> IO (Either StoreFailure (Maybe value)) -> IO (Either StoreFailure (Maybe value)) memoized reference key action = do entries <- IORef.readIORef reference case Map.lookup key entries of Just result -> pure result Nothing -> do result <- action IORef.modifyIORef' reference (Map.insert key result) pure result indexProposedObjects :: [AssertedObject] -> Either StoreFailure (Map ObjectId AssertedObject) indexProposedObjects = foldM insertOne Map.empty where insertOne indexed asserted | Map.member identity indexed = Left (StoreObjectValidationFailure (DuplicateAssertedObjectId identity)) | otherwise = Right (Map.insert identity asserted indexed) where identity = assertedObjectId asserted loadReferencedObjects :: Store -> Map ObjectId AssertedObject -> Set ObjectId -> Except.ExceptT StoreFailure IO (Map ObjectId AssertedObject) loadReferencedObjects store proposed = go Set.empty Map.empty . Set.toAscList where go _seen loaded [] = pure loaded go seen loaded (identity : remaining) | identity `Set.member` seen || Map.member identity proposed = go seen loaded remaining | otherwise = do row <- loadObjectRow store identity case row of Nothing -> go (Set.insert identity seen) loaded remaining Just asserted -> go (Set.insert identity seen) (Map.insert identity asserted loaded) ( Set.toAscList (objectReferences (assertedObjectContent asserted)) <> remaining ) loadObjectRow :: Store -> ObjectId -> Except.ExceptT StoreFailure IO (Maybe AssertedObject) loadObjectRow (Store _path _theory connection) identity = do let key = encodeCache (putObjectIdCache identity) payload <- loadPayload CanonicalObjects objectSelect key connection traverse (fmap (assertedObject identity) . Except.liftEither . first (StoreRowDecodeFailure CanonicalObjects key) . decodeCache getObjectContentCache) payload revalidateProposition :: CheckedObjectClosure -> CheckedPropositionContent -> Either PropositionValidationError CheckedPropositionContent revalidateProposition closure proposition = validateAssertedPropositionContent closure (checkedPropositionId proposition) (frozenCoreTerm (checkedPropositionTerm proposition)) insertObject :: SQLite.Connection -> AssertedObject -> Except.ExceptT StoreFailure IO () insertObject connection asserted = insertExact CanonicalObjects objectSelect objectInsert (encodeCache (putObjectIdCache (assertedObjectId asserted))) (encodeCache (putObjectContentCache (assertedObjectContent asserted))) connection insertProposition :: SQLite.Connection -> CheckedPropositionContent -> Except.ExceptT StoreFailure IO () insertProposition connection proposition = insertExact CanonicalPropositions propositionSelect propositionInsert (encodeCache (putPropositionIdCache (checkedPropositionId proposition))) (encodeCache (putCanonicalTermCache putObjectIdCache (frozenCoreTerm (checkedPropositionTerm proposition)))) connection insertProofValidation :: SQLite.Connection -> ProofValidationRecord -> Except.ExceptT StoreFailure IO () insertProofValidation connection record = insertExact ProofValidations proofValidationSelect proofValidationInsert (cacheDigestBytes (proofValidationKeyDigest (proofValidationRecordKey record))) (encodeCache (putProofValidationRecordCache record)) connection insertDeclarationValidation :: SQLite.Connection -> DeclarationValidationRecord -> Except.ExceptT StoreFailure IO () insertDeclarationValidation connection record = insertExact DeclarationValidations declarationValidationSelect declarationValidationInsert (cacheDigestBytes (declarationValidationKeyDigest (declarationValidationRecordKey record))) (encodeCache (putDeclarationValidationRecordCache record)) connection insertSyntaxInterface :: SQLite.Connection -> Syntax.ModuleSyntaxInterface -> Except.ExceptT StoreFailure IO () insertSyntaxInterface connection interface = insertExact SyntaxInterfaces syntaxInterfaceSelect syntaxInterfaceInsert (cacheDigestBytes (Syntax.syntaxInterfaceIdDigest (Syntax.moduleSyntaxAssertedId interface))) (encodeCache (Syntax.putModuleSyntaxInterfaceCache interface)) connection insertSemanticInterface :: SQLite.Connection -> SemanticInterface -> Except.ExceptT StoreFailure IO () insertSemanticInterface connection interface = insertExact SemanticInterfaces semanticInterfaceSelect semanticInterfaceInsert (cacheDigestBytes (semanticInterfaceIdDigest (semanticInterfaceAssertedId interface))) (encodeCache (putSemanticInterfaceCache interface)) connection insertModuleArtifact :: SQLite.Connection -> ModuleArtifactResult -> Except.ExceptT StoreFailure IO () insertModuleArtifact connection result = do let key = cacheDigestBytes (moduleArtifactIdDigest (moduleArtifactResultId result)) syntax = cacheDigestBytes (Syntax.syntaxInterfaceIdDigest (moduleArtifactResultSyntax result)) semantic = cacheDigestBytes (semanticInterfaceIdDigest (moduleArtifactResultSemantic result)) payload = encodeCache (putModuleArtifactResultCache result) rows <- liftIO (SQLite.query connection moduleArtifactSelect (Only key) :: IO [(ByteString, ByteString, ByteString)]) existing <- case rows of [] -> pure Nothing [row] -> pure (Just row) _ -> Except.throwError (StoreSchemaIntegrityFailure "primary key returned several module artifact rows") case existing of Just stored | stored /= (syntax, semantic, payload) -> Except.throwError (StoreRowPayloadMismatch ModuleArtifacts key) | otherwise -> pure () _ -> liftIO (SQLite.execute connection moduleArtifactInsert ( key , syntax , semantic , payload )) insertParsedArtifact :: SQLite.Connection -> Parsed.ParsedModuleKey -> ParsedPayload.ParsedArtifact -> Except.ExceptT StoreFailure IO () insertParsedArtifact connection key artifact = do let encodedKey = cacheDigestBytes (Parsed.parsedModuleKeyDigest key) encodedIdentity = cacheDigestBytes (Parsed.parsedModuleIdDigest (ParsedPayload.parsedArtifactId artifact)) encodedPayload = ParsedPayload.canonicalParsedPayloadBytes (ParsedPayload.parsedArtifactPayload artifact) rows <- liftIO (SQLite.query connection parsedArtifactSelect (Only encodedKey) :: IO [(ByteString, ByteString)]) case rows of [] -> liftIO (SQLite.execute connection parsedArtifactInsert ( encodedKey , encodedIdentity , encodedPayload )) [stored] | stored == (encodedIdentity, encodedPayload) -> pure () | otherwise -> Except.throwError (StoreRowPayloadMismatch ParsedArtifacts encodedKey) _ -> Except.throwError (StoreSchemaIntegrityFailure "primary key returned several parsed artifact rows") insertExact :: StoreRelation -> Query -> Query -> ByteString -> ByteString -> SQLite.Connection -> Except.ExceptT StoreFailure IO () insertExact relation selectRow insertRow key payload connection = do existing <- loadPayload relation selectRow key connection case existing of Nothing -> liftIO (SQLite.execute connection insertRow (key, payload)) Just stored | stored == payload -> pure () | otherwise -> Except.throwError (StoreRowPayloadMismatch relation key) loadPayload :: StoreRelation -> Query -> ByteString -> SQLite.Connection -> Except.ExceptT StoreFailure IO (Maybe ByteString) loadPayload relation selectRow key connection = do rows <- liftIO (SQLite.query connection selectRow (Only key) :: IO [Only ByteString]) case rows of [] -> pure Nothing [Only payload] -> pure (Just payload) _ -> Except.throwError (StoreSchemaIntegrityFailure ("primary key returned several " <> relationName relation <> " rows")) objectReferences :: ObjectContent -> Set ObjectId objectReferences = \case IntrinsicObjectContent{} -> Set.empty TransparentObjectContent _theory _coreType body -> termReferences body OpaqueObjectContent{} -> Set.empty termReferences :: CanonicalTerm ObjectId -> Set ObjectId termReferences = \case CBound{} -> Set.empty CGlobal identity -> Set.singleton identity CIntrinsic{} -> Set.empty COpaqueInteger{} -> Set.empty CApp function argument -> termReferences function <> termReferences argument CLam _binderType body -> termReferences body CFalsum -> Set.empty CImp premise conclusion -> termReferences premise <> termReferences conclusion CEq _operandType left right -> termReferences left <> termReferences right CForall _binderType body -> termReferences body schemaStatements :: [(Text, Text)] schemaStatements = [ ( compatibilityTableName , "CREATE TABLE store_compatibility ( \ \singleton INTEGER NOT NULL PRIMARY KEY CHECK (singleton = 1), \ \cache_epoch INTEGER NOT NULL CHECK (cache_epoch >= 0), \ \theory_id BLOB NOT NULL CHECK (length(theory_id) = 32) )" ) , exactRow "canonical_objects" "object_id" 33 , exactRow "canonical_propositions" "proposition_id" 32 , exactRow "proof_validations" "validation_key" 32 , exactRow "declaration_validations" "validation_key" 32 , exactRow "syntax_interfaces" "syntax_interface_id" 32 , exactRow "semantic_interfaces" "semantic_interface_id" 32 , ( "module_artifacts" , "CREATE TABLE module_artifacts ( \ \module_artifact_id BLOB NOT NULL PRIMARY KEY \ \CHECK (length(module_artifact_id) = 32), \ \syntax_interface_id BLOB NOT NULL \ \CHECK (length(syntax_interface_id) = 32), \ \semantic_interface_id BLOB NOT NULL \ \CHECK (length(semantic_interface_id) = 32), \ \payload BLOB NOT NULL, \ \FOREIGN KEY (syntax_interface_id) \ \REFERENCES syntax_interfaces(syntax_interface_id), \ \FOREIGN KEY (semantic_interface_id) \ \REFERENCES semantic_interfaces(semantic_interface_id) )" ) , ( "parsed_artifacts" , "CREATE TABLE parsed_artifacts ( \ \parsed_module_key BLOB NOT NULL PRIMARY KEY \ \CHECK (length(parsed_module_key) = 32), \ \parsed_module_id BLOB NOT NULL \ \CHECK (length(parsed_module_id) = 32), \ \payload BLOB NOT NULL )" ) ] where exactRow :: Text -> Text -> Int -> (Text, Text) exactRow table key keyBytes = ( table , "CREATE TABLE " <> table <> " ( " <> key <> " BLOB NOT NULL PRIMARY KEY " <> "CHECK (length(" <> key <> ") = " <> Text.pack (show keyBytes) <> "), " <> "payload BLOB NOT NULL )" ) compatibilityTableName :: Text compatibilityTableName = "store_compatibility" schemaQuery :: Text -> Query schemaQuery = Query normalizeSchema :: Text -> Text normalizeSchema = Text.unwords . Text.words . Text.dropWhileEnd (== ';') schemaDifference :: Map Text Text -> Map Text Text -> Text schemaDifference expected actual = "expected current schema " <> Text.pack (show (Map.keys expected)) <> ", found " <> Text.pack (show (Map.keys actual)) <> changed where altered = [ name | name <- Map.keys expected , Map.lookup name expected /= Map.lookup name actual , Map.member name actual ] changed | null altered = "" | otherwise = "; altered definitions: " <> Text.pack (show altered) objectSelect, objectInsert, propositionSelect, propositionInsert :: Query objectSelect = "SELECT payload FROM canonical_objects WHERE object_id = ?" objectInsert = "INSERT INTO canonical_objects (object_id, payload) VALUES (?, ?)" propositionSelect = "SELECT payload FROM canonical_propositions WHERE proposition_id = ?" propositionInsert = "INSERT INTO canonical_propositions (proposition_id, payload) VALUES (?, ?)" proofValidationSelect, proofValidationInsert :: Query proofValidationSelect = "SELECT payload FROM proof_validations WHERE validation_key = ?" proofValidationInsert = "INSERT INTO proof_validations (validation_key, payload) VALUES (?, ?)" declarationValidationSelect, declarationValidationInsert :: Query declarationValidationSelect = "SELECT payload FROM declaration_validations WHERE validation_key = ?" declarationValidationInsert = "INSERT INTO declaration_validations (validation_key, payload) VALUES (?, ?)" syntaxInterfaceSelect, syntaxInterfaceInsert :: Query syntaxInterfaceSelect = "SELECT payload FROM syntax_interfaces WHERE syntax_interface_id = ?" syntaxInterfaceInsert = "INSERT INTO syntax_interfaces (syntax_interface_id, payload) VALUES (?, ?)" semanticInterfaceSelect, semanticInterfaceInsert :: Query semanticInterfaceSelect = "SELECT payload FROM semantic_interfaces WHERE semantic_interface_id = ?" semanticInterfaceInsert = "INSERT INTO semantic_interfaces (semantic_interface_id, payload) VALUES (?, ?)" moduleArtifactSelect, moduleArtifactInsert :: Query moduleArtifactSelect = "SELECT syntax_interface_id, semantic_interface_id, payload \ \FROM module_artifacts WHERE module_artifact_id = ?" moduleArtifactInsert = "INSERT INTO module_artifacts \ \(module_artifact_id, syntax_interface_id, semantic_interface_id, payload) \ \VALUES (?, ?, ?, ?)" parsedArtifactSelect, parsedArtifactInsert :: Query parsedArtifactSelect = "SELECT parsed_module_id, payload FROM parsed_artifacts \ \WHERE parsed_module_key = ?" parsedArtifactInsert = "INSERT INTO parsed_artifacts \ \(parsed_module_key, parsed_module_id, payload) VALUES (?, ?, ?)" relationName :: StoreRelation -> Text relationName = \case CanonicalObjects -> "canonical object" CanonicalPropositions -> "canonical proposition" ProofValidations -> "proof validation" DeclarationValidations -> "declaration validation" SyntaxInterfaces -> "syntax interface" SemanticInterfaces -> "semantic interface" ModuleArtifacts -> "module artifact" ParsedArtifacts -> "parsed artifact" runStoreOperation :: Text -> IO value -> IO (Either StoreFailure value) runStoreOperation label action = do result <- trySynchronous action pure (case result of Right value -> Right value Left failure -> case Exception.fromException failure of Just (StoreAbort storeFailure) -> Left storeFailure Nothing -> Left (operationFailure label failure)) operationFailure :: Text -> Exception.SomeException -> StoreFailure operationFailure label = StoreOperationFailed label . exceptionText exceptionText :: Exception.SomeException -> Text exceptionText = Text.pack . Exception.displayException trySynchronous :: IO value -> IO (Either Exception.SomeException value) trySynchronous action = do result <- Exception.try action case result of Left failure -> case Exception.fromException failure :: Maybe Exception.AsyncException of Just asynchronous -> Exception.throwIO asynchronous Nothing -> pure (Left failure) Right value -> pure (Right value) closeIgnoringFailure :: SQLite.Connection -> IO () closeIgnoringFailure connection = void (trySynchronous (SQLite.close connection))