path: root/source/Felix/Store.hs

{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE NoImplicitPrelude #-}

-- | Coordinator-owned access to the disposable SQLite store.
module Felix.Store
    ( Store
    , 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 Checking.Core
import Checking.Declaration qualified as Declaration
import Checking.Identity
import Checking.Materialization qualified as Materialization
import 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 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

-- | 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))