path: root/source/Api.hs

{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE RankNTypes #-}

module Api
    ( tokenize, TokStream
    , scan
    , parse
    , parseWorkspace
    , AuthorityFreeParseError(..)
    , renderAuthorityFreeParseError
    , simpleStream
    , builtins
    , ParseException(..)
    , verify, verifyMeasured
    , verifyWithObserverAndStoreMode
    , verifyMeasuredWithObserverAndStoreMode
    , verifyWithObserverAndStoreModeAndJobs
    , verifyMeasuredWithObserverAndStoreModeAndJobs
    , StoreValidationMode(..)
    , WorkPosition
    , workPosition
    , workPositionModuleOrdinal
    , workPositionLocalRequestOrdinal
    , VerificationRequestObserver
    , verificationRequestObserver
    , ProverAnswer
        ( CounterSatisfiable
        , ContradictoryAxioms
        , Uncertain
        , Error
        )
    , pattern Yes
    , VerificationResult(..)
    , VerificationPresentation
    , ReportedEscapeKind(..)
    , ReportedEscape(..)
    , VerificationReport(..)
    , VerificationMeasurements(..)
    , VerificationDriverError(..)
    , FailedVerification(..)
    , VerificationFailureReason(..)
    , prepareVerifiedHtmlExportResult
    , prepareDefaultSourceGraph
    , defaultHtmlMountPrefixes
    ) where


import Base
import Checking.Declaration qualified as Declaration
import Checking.Foundation qualified as Foundation
import Checking.Identity qualified as Identity
import Checking.Module qualified as Typed
import Checking.Semantic qualified as Semantic
import Felix.Module (localDeclarationOrdinal)
import Felix.Parse (ParseException(..), ParseWorkspaceError(..), ParsedSourceWorkspace)
import Felix.Parse qualified as Felix
import Felix.Prelude qualified as Prelude
import Felix.Source
import Felix.Store qualified as Store
import Felix.Source.Graph (ResolvedSourceGraph)
import Felix.Source.Graph qualified as SourceGraph
import Provers
import Render.Html.Export qualified as HtmlExport
import Render.Html.Output (PreparedHtmlArtifact)
import Report.Location
import Syntax.Abstract qualified as Raw
import Syntax.Adapt (scanChunk, ScannedLexicalItem)
import Syntax.Interface qualified as Syntax
import Syntax.Lexicon (builtins)
import Syntax.Token

import Control.Exception qualified as Exception
import Control.Monad.Logger
import Control.Monad (unless)
import Data.Bifunctor (first)
import Data.List.NonEmpty qualified as NonEmpty
import Data.Map.Strict qualified as Map
import Data.Text qualified as StrictText
import Data.Text.Encoding.Error (UnicodeException)
import Data.Text.IO qualified as Text
import Numeric.Natural (Natural)
import System.FilePath.Posix
import Text.Megaparsec hiding (failure, parse, Token, try)
import UnliftIO
import UnliftIO.Async qualified as Async
import UnliftIO.Directory
import UnliftIO.Environment

-- Renderer data follows the established current-directory, configured-library,
-- and debug-directory lookup policy.
findAndReadRendererFile
    :: FilePath
    -> IO (Either HtmlExport.HtmlExportError Text)
findAndReadRendererFile path = do
    rootsResult <- tryRendererIO do
        currentDir <- getCurrentDirectory
        configuredLibrary <- lookupEnv "NAPROCHE_LIB"
        let libraryDir =
                fromMaybe
                    (currentDir </> "library")
                    configuredLibrary
        pure
            [ currentDir </> path
            , libraryDir </> path
            , currentDir </> "debug" </> path
            ]
    case rootsResult of
        Left failure ->
            pure
                (Left
                    (HtmlExport.HtmlRendererDataLookupFailed
                        path
                        (StrictText.pack
                            (displayException failure))))
        Right candidates -> do
            selected <- selectRendererData path candidates
            case selected of
                Left failure ->
                    pure (Left failure)
                Right selectedPath -> do
                    readResult <- tryRendererRead
                        (Text.readFile selectedPath)
                    pure case readResult of
                        Left reason ->
                            Left
                                (HtmlExport.HtmlRendererDataReadFailed
                                    selectedPath
                                    reason)
                        Right contents ->
                            Right contents

selectRendererData
    :: FilePath
    -> [FilePath]
    -> IO (Either HtmlExport.HtmlExportError FilePath)
selectRendererData requested candidates =
    go candidates
  where
    go = \case
        [] ->
            pure
                (Left
                    (HtmlExport.HtmlRendererDataNotFound
                        requested
                        candidates))
        candidate : remaining -> do
            inspected <- tryRendererIO
                (doesFileExist candidate)
            case inspected of
                Left failure ->
                    pure
                        (Left
                            (HtmlExport.HtmlRendererDataLookupFailed
                                candidate
                                (StrictText.pack
                                    (displayException failure))))
                Right True ->
                    pure (Right candidate)
                Right False ->
                    go remaining

tryRendererIO :: IO value -> IO (Either IOException value)
tryRendererIO = Exception.try

tryRendererRead :: IO value -> IO (Either Text value)
tryRendererRead action =
    Exception.catch
        (Exception.catch
            (Right <$> action)
            renderIOException)
        renderUnicodeException
  where
    renderIOException :: IOException -> IO (Either Text value)
    renderIOException =
        pure . Left . StrictText.pack . displayException

    renderUnicodeException
        :: UnicodeException
        -> IO (Either Text value)
    renderUnicodeException =
        pure . Left . StrictText.pack . displayException

lexFile :: MonadIO io => FilePath -> io (Text, [[Located Token]])
lexFile file = do
    prepared <- liftIO (prepareDefaultSourceRequest file)
    (mounts, request) <- either throwWorkspaceError pure prepared
    loaded <-
        liftIO (resolveAndLoadRoot mounts request)
            >>= either throwIO pure
    let source = loadedSource loaded
        raw = loadedText loaded
        locationPath = resolvedSourceLocationPath source
        canonicalPath =
            canonicalPathFilePath
                (resolvedSourceCanonicalPath source)
    registration <-
        registerFilePathWithDisplay
            canonicalPath
            locationPath
    fileId <- either
        (throwIO . SourceLocationRegistrationFailed source)
        pure
        registration
    case runLexer fileId locationPath raw of
        Left tokenError ->
            throwIO (TokenError (errorBundlePretty tokenError))
        Right (_imports, chunks) ->
            pure (raw, chunks)

-- | Throws a 'ParseException' when tokenizing fails.
tokenize :: MonadIO io => FilePath -> io TokStream
tokenize file = do
    (raw, chunks) <- lexFile file
    pure (TokStream raw chunks)

-- | Scan the given file for lexical items. The actual parsing process
-- builds one workspace lexicon instead.
scan :: MonadIO io => FilePath -> io [ScannedLexicalItem]
scan input = do
    tokenStream <- tokenize input
    fmap (concatMap (fmap unLocated)) $
        traverse
            (either (throwIO . LexicalScanFailure) pure . scanChunk)
            (unTokStream tokenStream)


-- | Parse a file. Throws an 'AuthorityFreeParseError' when packaged-prelude
-- loading/parsing or ordinary workspace parsing fails.
parse :: MonadIO io => FilePath -> io [Raw.Block]
parse file = do
    result <- parseWorkspace file
    either throwIO pure result

data AuthorityFreeParseError
    = AuthorityFreePreludeLoadFailed !Prelude.PreludeLoadError
    | AuthorityFreePreludeParseFailed !Prelude.PreludeParseError
    | AuthorityFreeWorkspaceFailed !ParseWorkspaceError
    deriving (Show)

instance Exception AuthorityFreeParseError

renderAuthorityFreeParseError :: AuthorityFreeParseError -> Text
renderAuthorityFreeParseError = \case
    AuthorityFreePreludeLoadFailed failure ->
        "packaged final prelude loading failed: "
            <> Prelude.renderPreludeLoadError failure
    AuthorityFreePreludeParseFailed failure ->
        "packaged final prelude parsing failed: "
            <> Prelude.renderPreludeParseError failure
    AuthorityFreeWorkspaceFailed failure ->
        Felix.renderParseWorkspaceError failure

parseWorkspace
    :: MonadIO io
    => FilePath
    -> io (Either AuthorityFreeParseError [Raw.Block])
parseWorkspace file =
    fmap Felix.importedBeforeImporterBlocks
        <$> liftIO (parseDefaultWorkspaceWithPrelude file)

parseDefaultWorkspaceWithPrelude
    :: FilePath
    -> IO
        (Either
            AuthorityFreeParseError
            ParsedSourceWorkspace)
parseDefaultWorkspaceWithPrelude file =
    Prelude.loadReservedPreludeSourceInput >>= \case
        Left failure ->
            pure (Left (AuthorityFreePreludeLoadFailed failure))
        Right source ->
            Prelude.parseReservedPreludeSource source >>= \case
                Left failure ->
                    pure (Left (AuthorityFreePreludeParseFailed failure))
                Right prelude -> do
                    prepared <- prepareDefaultSourceRequest file
                    case prepared of
                        Left failure ->
                            pure
                                (Left
                                    (AuthorityFreeWorkspaceFailed failure))
                        Right (mounts, request) -> do
                            let syntax =
                                    Felix.identifiedParsedModuleSyntaxInterface
                                        (Prelude.reservedParsedPreludeModule
                                            prelude)
                            fmap
                                (first AuthorityFreeWorkspaceFailed . fmap fst)
                                (Felix.parseSourceWorkspaceMeasuredWithSyntaxInputsAndGraphValidation
                                    mounts
                                    request
                                    (const [syntax])
                                    (Prelude.rejectOrdinaryPreludeSourceGraph
                                        source))

prepareDefaultSourceRequest
    :: FilePath
    -> IO (Either ParseWorkspaceError (SourceMounts, RootRequest))
prepareDefaultSourceRequest file = do
    mountsResult <- prepareDefaultSourceMounts
    requestResult <- classifyRootRequest file
    pure case (mountsResult, requestResult) of
        (Left err, _) ->
            Left (SourceWorkspaceError err)
        (_, Left err) ->
            Left (SourceWorkspaceError err)
        (Right mounts, Right request) ->
            Right (mounts, request)

prepareDefaultSourceGraph
    :: FilePath
    -> IO (Either ParseWorkspaceError ResolvedSourceGraph)
prepareDefaultSourceGraph file = do
    prepared <- prepareDefaultSourceRequest file
    case prepared of
        Left sourceFailure ->
            pure (Left sourceFailure)
        Right (mounts, request) ->
            first SourceWorkspaceError
                <$> SourceGraph.buildResolvedSourceGraph mounts request

prepareDefaultSourceMounts :: IO (Either SourceError SourceMounts)
prepareDefaultSourceMounts = do
    currentDir <- getCurrentDirectory
    configuredLibrary <- lookupEnv "NAPROCHE_LIB"
    let libraryDir = configuredLibrary ?? (currentDir </> "library")
        debugDir = currentDir </> "debug"
    prepareSourceMounts
        [ (sourceMountId "project", currentDir)
        , (sourceMountId "library", libraryDir)
        , (sourceMountId "debug", debugDir)
        ]

classifyRootRequest :: FilePath -> IO (Either SourceError RootRequest)
classifyRootRequest file
    | isAbsolute file =
        existingRoot file
    | otherwise =
        pure (searchedRoot file)

throwWorkspaceError :: MonadIO io => ParseWorkspaceError -> io a
throwWorkspaceError = \case
    SourceWorkspaceError err ->
        throwIO err
    err@(SourceLexiconCollision _) ->
        throwIO err
    err@(SourceSyntaxPragmaError _source _pragmaError) ->
        throwIO err
    err@(SourceSyntaxDeclarationError _source _declarationError) ->
        throwIO err
    err@(SourceSyntaxMaterializationError _materializationError) ->
        throwIO err
    err@(SourceParsedModuleKeyError _source _keyError) ->
        throwIO err
    SourceParseError _source err ->
        throwIO err


simpleStream :: TokStream -> [[Token]]
simpleStream TokStream{unTokStream=chunks} = [unLocated <$> ch | ch <- chunks]

data VerificationResult
    = VerificationCompleted
        !VerificationReport
        !VerificationPresentation
    | CompletedWithExplicitGaps
        !VerificationReport
        !VerificationPresentation
    | VerificationFailure !VerificationReport !FailedVerification
    | VerificationCheckingFailure
        !VerificationReport
        !VerificationDriverError
    deriving (Show)

-- | Strict owner-independent source presentation retained only after the
-- complete typed workspace succeeds.
data VerificationPresentation = VerificationPresentation
    !HtmlExport.HtmlPresentation

instance Show VerificationPresentation where
    show _presentation =
        "VerificationPresentation <HTML presentation>"

data ReportedEscapeKind
    = ReportedSourceAxiom
    | ReportedOmitted
    deriving (Show, Eq)

data ReportedEscape = ReportedEscape
    { reportedEscapeKind :: !ReportedEscapeKind
    , reportedEscapeLocation :: !Location
    }
    deriving (Show, Eq)

data VerificationReport = VerificationReport
    { verificationDirectEscapes :: ![ReportedEscape]
    }
    deriving (Show, Eq)

-- | Invocation-local observation of the verification pipeline.
--
-- Durations use the monotonic clock and are never part of fact authority or
-- deterministic verification results.
data VerificationMeasurements = VerificationMeasurements
    { verificationParseMeasurements :: !Felix.ParseMeasurements
    , verificationSourcePreparationNanoseconds :: !Word64
    , verificationInvocationNanoseconds :: !Word64
    , verificationCheckingNanoseconds :: !Word64
    , verificationModuleCount :: !Int
    , verificationDetectedProcessorCount :: !(Maybe Int)
    , verificationEffectiveJobs :: !Int
    , verificationJobsOverridden :: !Bool
    , verificationMaximumLiveModuleCheckers :: !Int
    , verificationMaximumLiveVampireProcesses :: !Int
    , verificationMaximumReadyModuleCount :: !Int
    , verificationObligationBatchCount :: !Int
    , verificationPreparedObligationCount :: !Int
    , verificationMaximumObligationBatchSize :: !Int
    , verificationPreparedRequestBytes :: !Word64
    , verificationRequestPreparationNanoseconds :: !Word64
    , verificationVampireRunCount :: !Int
    , verificationModuleRootHitCount :: !Int
    , verificationModuleRootMissCount :: !Int
    , verificationFirstVampireStartNanoseconds
        :: !(Maybe Word64)
    , verificationFinalVampireSubmissionNanoseconds
        :: !(Maybe Word64)
    , verificationFinalVampireCompletionNanoseconds
        :: !(Maybe Word64)
    , verificationVampireExecutionNanoseconds :: !Word64
    , verificationLongestVampireExecutionNanoseconds :: !Word64
    }
    deriving (Show, Eq)

data VerificationObservation = VerificationObservation
    { observedModuleCount :: !Int
    , observedDetectedProcessorCount :: !(Maybe Int)
    , observedEffectiveJobs :: !Int
    , observedJobsOverridden :: !Bool
    , observedLiveModuleCheckers :: !Int
    , observedMaximumLiveModuleCheckers :: !Int
    , observedMaximumLiveVampireProcesses :: !Int
    , observedMaximumReadyModuleCount :: !Int
    , observedObligationBatchCount :: !Int
    , observedPreparedObligationCount :: !Int
    , observedMaximumObligationBatchSize :: !Int
    , observedPreparedRequestBytes :: !Word64
    , observedRequestPreparationNanoseconds :: !Word64
    , observedVampireRunCount :: !Int
    , observedModuleRootHitCount :: !Int
    , observedModuleRootMissCount :: !Int
    , observedFirstVampireStart :: !(Maybe Word64)
    , observedFinalVampireSubmission :: !(Maybe Word64)
    , observedFinalVampireCompletion :: !(Maybe Word64)
    , observedVampireExecutionNanoseconds :: !Word64
    , observedLongestVampireExecutionNanoseconds :: !Word64
    }

initialVerificationObservation :: VerificationObservation
initialVerificationObservation =
    VerificationObservation
        { observedModuleCount = 0
        , observedDetectedProcessorCount = Nothing
        , observedEffectiveJobs = 1
        , observedJobsOverridden = False
        , observedLiveModuleCheckers = 0
        , observedMaximumLiveModuleCheckers = 0
        , observedMaximumLiveVampireProcesses = 0
        , observedMaximumReadyModuleCount = 0
        , observedObligationBatchCount = 0
        , observedPreparedObligationCount = 0
        , observedMaximumObligationBatchSize = 0
        , observedPreparedRequestBytes = 0
        , observedRequestPreparationNanoseconds = 0
        , observedVampireRunCount = 0
        , observedModuleRootHitCount = 0
        , observedModuleRootMissCount = 0
        , observedFirstVampireStart = Nothing
        , observedFinalVampireSubmission = Nothing
        , observedFinalVampireCompletion = Nothing
        , observedVampireExecutionNanoseconds = 0
        , observedLongestVampireExecutionNanoseconds = 0
        }

newtype VerificationRequestObserver = VerificationRequestObserver
    { observeVerificationRequest
        :: WorkPosition
        -> PreparedVerificationRequest
        -> IO ()
    }

verificationRequestObserver
    :: (WorkPosition
        -> PreparedVerificationRequest
        -> IO ())
    -> VerificationRequestObserver
verificationRequestObserver =
    VerificationRequestObserver

ignoreVerificationRequests :: VerificationRequestObserver
ignoreVerificationRequests =
    VerificationRequestObserver \_ordinal _request -> pure ()

data FailedVerification = FailedVerification
    { failedVerificationLocation :: !Location
    , failedVerificationReason :: !VerificationFailureReason
    }
    deriving (Show)

data VerificationFailureReason
    = CountermodelFailure !Text
    | ContradictoryInputFailure !Text
    | IndeterminateFailure !Text
    | ProtocolFailure !Text !Text
    | TransportFailure !ProverProcessError
    deriving (Show)

verificationFailureReason
    :: Either ProverProcessError ProverAnswer
    -> Maybe VerificationFailureReason
verificationFailureReason = \case
    Left processError ->
        Just (TransportFailure processError)
    Right Yes ->
        Nothing
    Right (CounterSatisfiable tptp) ->
        Just (CountermodelFailure tptp)
    Right (ContradictoryAxioms tptp) ->
        Just (ContradictoryInputFailure tptp)
    Right (Uncertain tptp) ->
        Just (IndeterminateFailure tptp)
    Right (Error taskLabel message) ->
        Just (ProtocolFailure taskLabel message)

data VerificationDriverError
    = VerificationWorkspaceError
        !ParseWorkspaceError
    | VerificationFoundationManifestError
        !(NonEmpty Foundation.FoundationManifestError)
    | VerificationMissingImportedModule
        !ResolvedSourceAddress
    | VerificationMissingRootModule
        !ResolvedSourceAddress
    | VerificationFinalPreludeReadinessError
        !Typed.FinalPreludeReadinessError
    | VerificationTypedInputError
        !ResolvedSource
        !Typed.TypedModuleInputError
    | VerificationTypedOpenError
        !ResolvedSource
        !Declaration.DriverOpenError
    | VerificationTypedCachedModuleError
        !ResolvedSource
        !Typed.CachedTypedModuleError
    | VerificationTypedModuleError
        !ResolvedSource
        !Typed.TypedModuleFailure
        !Declaration.PendingModulePrefix
    | VerificationValidationIntegrityError
        !ResolvedSource
        !Declaration.ValidationIntegrityError
    | VerificationAdmittedViewError
        !ResolvedSource
        !AdmittedViewError
    | VerificationParsedArtifactIntegrityError
        !ResolvedSource
        !Felix.ParsedArtifactIntegrityError
    | VerificationStoreFailure !Store.StoreFailure
    | VerificationStorePlanningFailure !Store.StorePlanningError
    | VerificationStoreLifecycleFailure !Store.StoreLifecycleError
    | VerificationModuleArtifactKeyError !Semantic.ModuleArtifactKeyError
    | VerificationModuleSchedulerInvariant !Text
    deriving (Show)

instance Exception VerificationDriverError

data TypedWorkspaceOutcome
    = TypedWorkspaceSucceeded
        !AdmittedTypedWorkspace
    | TypedWorkspaceRejected
        !AdmittedTypedWorkspace
        !TypedWorkspaceFailure

data TypedWorkspaceFailure
    = TypedWorkspaceCheckingRejected !VerificationDriverError
    | TypedWorkspaceProverRejected !FailedVerification

data ModuleTask = ModuleTask
    { moduleTaskOrdinal :: !Natural
    , moduleTaskParsed :: !Felix.ParsedModule
    , moduleTaskDirectAddresses :: ![ResolvedSourceAddress]
    }

data ModuleCheckResult
    = ModuleCheckSucceeded
        !ResolvedSourceAddress
        !Typed.SealedTypedModule
        !AdmittedTypedModule
    | ModuleCheckRejected
        !AdmittedTypedModule
        !TypedWorkspaceFailure

data ModuleFailureCandidate = ModuleFailureCandidate
    !Natural
    !AdmittedTypedModule
    !TypedWorkspaceFailure

data AdmittedTypedDeclaration = AdmittedTypedDeclaration
    !Semantic.DeclarationSlot
    !Typed.TypedSourceDeclaration

newtype AdmittedTypedModule = AdmittedTypedModule
    [AdmittedTypedDeclaration]

newtype AdmittedTypedWorkspace = AdmittedTypedWorkspace
    [AdmittedTypedModule]

data AdmittedViewError
    = AdmittedDeclarationCountMismatch
        !Int
        !Int
    | AdmittedDeclarationSlotMismatch
        ![Semantic.DeclarationSlot]
        ![Semantic.DeclarationSlot]
    deriving (Show, Eq)

completeAdmittedModule
    :: Typed.IdentifiedModuleInput
    -> AdmittedTypedModule
completeAdmittedModule input =
    AdmittedTypedModule
        (uncurry AdmittedTypedDeclaration <$> expectedDeclarations input)

checkedAdmittedModule
    :: Bool
    -> Typed.IdentifiedModuleInput
    -> Declaration.PendingModulePrefix
    -> Either AdmittedViewError AdmittedTypedModule
checkedAdmittedModule requireComplete input prefix = do
    let expected = expectedDeclarations input
        expectedSlots = fst <$> expected
        actualSlots =
            Declaration.committedBatchSlot
                <$> Declaration.pendingModulePrefixBatches prefix
        admittedCount = length actualSlots
    if requireComplete
        then unless
            (admittedCount == length expected)
            (Left
                (AdmittedDeclarationCountMismatch
                    (length expected)
                    admittedCount))
        else unless
            (admittedCount <= length expected)
            (Left
                (AdmittedDeclarationCountMismatch
                    (length expected)
                    admittedCount))
    unless
        (actualSlots == take admittedCount expectedSlots)
        (Left
            (AdmittedDeclarationSlotMismatch
                (take admittedCount expectedSlots)
                actualSlots))
    pure
        (AdmittedTypedModule
            [ AdmittedTypedDeclaration slot declaration
            | (slot, declaration) <- take admittedCount expected
            ])

expectedDeclarations
    :: Typed.IdentifiedModuleInput
    -> [(Semantic.DeclarationSlot, Typed.TypedSourceDeclaration)]
expectedDeclarations input =
    zipWith
        (\ordinal declaration ->
            ( Semantic.declarationSlot
                (Typed.identifiedModuleOwner input)
                (localDeclarationOrdinal ordinal)
            , declaration
            ))
        [0..]
        (Typed.typedSourceDeclarations
            (Typed.identifiedModuleParsed input))

data StoreValidationMode
    = FreshStoreValidation
    | WarmStoreValidation
    deriving (Show, Eq)

verifyWithObserverAndStoreMode
    :: (MonadUnliftIO io, MonadLogger io)
    => Store.Store
    -> StoreValidationMode
    -> VerificationRequestObserver
    -> Vampire
    -> FilePath
    -> io (Either VerificationDriverError VerificationResult)
verifyWithObserverAndStoreMode store validationMode observer prover file =
    verifyWithObserverAndStoreModeAndJobs
        store validationMode sequentialJobs observer prover file

verifyWithObserverAndStoreModeAndJobs
    :: (MonadUnliftIO io, MonadLogger io)
    => Store.Store
    -> StoreValidationMode
    -> JobsSelection
    -> VerificationRequestObserver
    -> Vampire
    -> FilePath
    -> io (Either VerificationDriverError VerificationResult)
verifyWithObserverAndStoreModeAndJobs
        store validationMode jobs observer prover file =
    fmap (fmap fst)
        (verifyMeasuredWithObserverAndStoreModeAndJobs
            store validationMode jobs observer prover file)

verifyMeasuredWithObserverAndStoreMode
    :: (MonadUnliftIO io, MonadLogger io)
    => Store.Store
    -> StoreValidationMode
    -> VerificationRequestObserver
    -> Vampire
    -> FilePath
    -> io
        (Either
            VerificationDriverError
            (VerificationResult, VerificationMeasurements))
verifyMeasuredWithObserverAndStoreMode
        store validationMode observer prover file =
    verifyMeasuredWithObserverAndStoreModeAndJobs
        store validationMode sequentialJobs observer prover file

verifyMeasuredWithObserverAndStoreModeAndJobs
    :: (MonadUnliftIO io, MonadLogger io)
    => Store.Store
    -> StoreValidationMode
    -> JobsSelection
    -> VerificationRequestObserver
    -> Vampire
    -> FilePath
    -> io
        (Either
            VerificationDriverError
            (VerificationResult, VerificationMeasurements))
verifyMeasuredWithObserverAndStoreModeAndJobs
        store validationMode jobs observer prover file =
    try
        (verifyMeasuredThrowingWithStore
            store validationMode jobs observer prover file)

sequentialJobs :: JobsSelection
sequentialJobs =
    JobsSelection
        { jobsSelectionDetectedProcessors = Nothing
        , jobsSelectionEffectiveJobs =
            fromMaybe
                (impossible "one is not a positive worker count")
                (effectiveJobs 1)
        , jobsSelectionWasOverridden = True
        }

verifyMeasured
    :: (MonadUnliftIO io, MonadLogger io)
    => Vampire
    -> FilePath
    -> io
        (Either
            VerificationDriverError
            (VerificationResult, VerificationMeasurements))
verifyMeasured prover file =
    verifyMeasuredWithObserver
        ignoreVerificationRequests
        prover
        file

verifyMeasuredWithObserver
    :: (MonadUnliftIO io, MonadLogger io)
    => VerificationRequestObserver
    -> Vampire
    -> FilePath
    -> io
        (Either
            VerificationDriverError
            (VerificationResult, VerificationMeasurements))
verifyMeasuredWithObserver observer prover file =
    try (verifyMeasuredThrowing observer prover file)

verifyMeasuredThrowing
    :: (MonadUnliftIO io, MonadLogger io)
    => VerificationRequestObserver
    -> Vampire
    -> FilePath
    -> io (VerificationResult, VerificationMeasurements)
verifyMeasuredThrowing requestObserver prover file = do
    foundation <-
        either
            (throwIO . VerificationFoundationManifestError)
            pure
            Foundation.checkedFoundation
    planned <- liftIO (Store.planStore Store.FreshTemporaryStore)
    plan <- either
        (throwIO . VerificationStorePlanningFailure)
        pure
        planned
    withRunInIO \runInIO ->
        Store.withStoreLease plan \lease -> do
            opened <- Store.withOpenStore
                lease
                (Identity.theoryId foundation)
                (\_startup store ->
                    runInIO
                        (verifyMeasuredThrowingWithStore
                            store
                            FreshStoreValidation
                            sequentialJobs
                            requestObserver
                            prover
                            file))
            either
                (throwIO . VerificationStoreLifecycleFailure)
                pure
                opened

verifyMeasuredThrowingWithStore
    :: (MonadUnliftIO io, MonadLogger io)
    => Store.Store
    -> StoreValidationMode
    -> JobsSelection
    -> VerificationRequestObserver
    -> Vampire
    -> FilePath
    -> io (VerificationResult, VerificationMeasurements)
verifyMeasuredThrowingWithStore
        store validationMode jobsSelection requestObserver prover file = do
    invocationStart <- liftIO getMonotonicTimeNSec
    memo <- liftIO (Store.newStoreMemo store)
    storeCoordinator <- liftIO Store.newStoreCoordinator
    ( admittedResult
      , parseMeasurements
      , sourcePreparation
      , checkingStart
      , checkingEnd
      , observation
      , parsedPresentation
      ) <-
        liftIO
          (withVampireExecutor
            (jobsSelectionEffectiveJobs jobsSelection)
            prover
            (observeVerificationRequest requestObserver)
            \executor -> do
            observationRef <- newIORef
                initialVerificationObservation
                    { observedDetectedProcessorCount =
                        jobsSelectionDetectedProcessors jobsSelection
                    , observedEffectiveJobs =
                        effectiveJobsValue
                            (jobsSelectionEffectiveJobs jobsSelection)
                    , observedJobsOverridden =
                        jobsSelectionWasOverridden jobsSelection
                    }
            foundation <-
                either
                    (throwIO
                        . VerificationFoundationManifestError)
                    pure
                    Foundation.checkedFoundation
            preparationStart <- getMonotonicTimeNSec
            prepared <-
                prepareDefaultSourceRequest file
                    >>= either
                        (throwIO . VerificationWorkspaceError)
                        pure
            let (mounts, request) = prepared
            preparationEnd <- getMonotonicTimeNSec
            prelude <- withVampireRequestOwner executor \owner -> do
                preludeResolver <-
                    typedVampireResolver
                        owner
                        0
                        observationRef
                Typed.acquireFinalPreludeSession
                    memo store foundation preludeResolver
                    >>= either
                        (throwIO
                            . VerificationFinalPreludeReadinessError)
                        pure
            observeModuleRootAcquisition observationRef
                (Typed.finalPreludeAcquisition prelude)
            let preludeSyntax =
                    Typed.sealedTypedModuleSyntax
                        (Typed.finalPreludeModule prelude)
                syntaxInputs _source = [preludeSyntax]
            (parsed, measured) <-
                Felix.parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndGraphValidation
                    store
                    mounts
                    request
                    syntaxInputs
                    (Prelude.rejectOrdinaryPreludeSourceGraph
                        (Typed.finalPreludeSource prelude))
                    >>= either throwParseExecutionError pure
            checkingStart <- getMonotonicTimeNSec
            outcome <-
                checkTypedWorkspace
                    memo
                    storeCoordinator
                    foundation
                    prelude
                    executor
                    (jobsSelectionEffectiveJobs jobsSelection)
                    validationMode
                    observationRef
                    parsed
                    store
            checkingEnd <- getMonotonicTimeNSec
            executorObserved <- vampireExecutorObservation executor
            mergeExecutorObservation observationRef executorObserved
            observed <- readIORef observationRef
            pure
                ( outcome
                , measured
                , preparationEnd - preparationStart
                , checkingStart
                , checkingEnd
                , observed
                , parsed
                ))
    let result =
            case admittedResult of
                TypedWorkspaceRejected admitted failure ->
                    let report = admittedWorkspaceReport admitted
                    in case failure of
                        TypedWorkspaceCheckingRejected checkingFailure ->
                            VerificationCheckingFailure
                                report checkingFailure
                        TypedWorkspaceProverRejected proverFailure ->
                            VerificationFailure report proverFailure
                TypedWorkspaceSucceeded admitted ->
                    completedResult
                        (admittedWorkspaceReport admitted)
                        (VerificationPresentation
                            (HtmlExport.htmlPresentationFromParsedWorkspace
                                parsedPresentation))
        measurements =
            finalizeVerificationMeasurements
                invocationStart
                checkingStart
                checkingEnd
                parseMeasurements
                sourcePreparation
                observation
    logInfoN
        (renderVerificationMeasurements measurements)
    pure (result, measurements)
  where
    throwParseExecutionError = \case
        Felix.ParseExecutionWorkspaceError failure ->
            throwIO (VerificationWorkspaceError failure)
        Felix.ParseExecutionStoreFailure failure ->
            throwIO (VerificationStoreFailure failure)
        Felix.ParseExecutionArtifactIntegrityFailure source failure ->
            throwIO
                (VerificationParsedArtifactIntegrityError source failure)

checkTypedWorkspace
    :: Store.StoreMemo
    -> Store.StoreCoordinator
    -> Foundation.CheckedFoundation
    -> Typed.FinalPreludeSession
    -> VampireExecutor
    -> EffectiveJobs
    -> StoreValidationMode
    -> IORef VerificationObservation
    -> ParsedSourceWorkspace
    -> Store.Store
    -> IO TypedWorkspaceOutcome
checkTypedWorkspace
        memo
        storeCoordinator
        foundation
        prelude
        executor
        selectedJobs
        validationMode
        observationRef
        workspace
        store = do
    let modules =
            zipWith
                makeTask
                [1..]
                (toList
                    (Felix.parsedWorkspaceImportedBeforeImporter workspace))
        rootAddress =
            Felix.parsedModuleAddress
                (Felix.parsedWorkspaceRootModule workspace)
    atomicModifyIORef' observationRef
        (\observation ->
            ( observation
                { observedModuleCount = length modules
                }
            , ()
            ))
    scheduleModules
        rootAddress
        modules
        Map.empty
        Map.empty
        Map.empty
        Nothing
  where
    workerBound = effectiveJobsValue selectedJobs

    makeTask ordinal parsed =
        ModuleTask
            { moduleTaskOrdinal = ordinal
            , moduleTaskParsed = parsed
            , moduleTaskDirectAddresses =
                nubOrd
                    (Felix.parsedImportedAddress
                        <$> Felix.parsedModuleImports parsed)
            }

    scheduleModules
        rootAddress
        pending
        running
        sealedByAddress
        admittedByOrdinal
        candidate = do
            let readyCount =
                    length
                        [ ()
                        | task <- pending
                        , taskMayStart candidate sealedByAddress task
                        ]
            observeReadyModules observationRef readyCount
            (pending', running') <-
                startReadyModules
                    pending
                    running
                    sealedByAddress
                    candidate
            Exception.onException
              (if Map.null running'
                then case candidate of
                    Just selected
                        | any
                            (\task ->
                                moduleTaskOrdinal task
                                    < candidateOrdinal selected)
                            pending' ->
                                throwIO
                                    (VerificationModuleSchedulerInvariant
                                        "an earlier module is not terminal")
                        | otherwise ->
                            pure
                                (TypedWorkspaceRejected
                                    (admittedWorkspaceThrough
                                        admittedByOrdinal
                                        selected)
                                    (candidateFailure selected))
                    Nothing
                        | null pending' -> do
                            unless
                                (Map.member rootAddress sealedByAddress)
                                (throwIO
                                    (VerificationMissingRootModule
                                        rootAddress))
                            pure
                                (TypedWorkspaceSucceeded
                                    (completeAdmittedWorkspace
                                        admittedByOrdinal))
                        | otherwise ->
                            throwIO
                                (VerificationModuleSchedulerInvariant
                                    "no ready module and no running module")
                else do
                    (_completedAsync, (ordinal, completed)) <-
                        Async.waitAny (Map.elems running')
                    let runningWithoutCompleted =
                            Map.delete ordinal running'
                    case completed of
                        Left fatal -> do
                            cancelModuleCheckers runningWithoutCompleted
                            Exception.throwIO fatal
                        Right (ModuleCheckSucceeded
                                address sealed admittedModule) ->
                            scheduleModules
                                rootAddress
                                pending'
                                runningWithoutCompleted
                                (Map.insert address sealed sealedByAddress)
                                (Map.insert
                                    ordinal
                                    admittedModule
                                    admittedByOrdinal)
                                candidate
                        Right (ModuleCheckRejected
                                admittedModule failure) -> do
                            let selected =
                                    chooseEarlierFailure
                                        candidate
                                        (ModuleFailureCandidate
                                            ordinal
                                            admittedModule
                                            failure)
                                cutoff = candidateOrdinal selected
                                (later, retained) =
                                    Map.partitionWithKey
                                        (\runningOrdinal _async ->
                                            runningOrdinal > cutoff)
                                        runningWithoutCompleted
                            cancelModuleCheckers later
                            scheduleModules
                                rootAddress
                                pending'
                                retained
                                sealedByAddress
                                admittedByOrdinal
                                (Just selected)
              )
              (cancelModuleCheckers running')

    startReadyModules
        pending
        running
        sealedByAddress
        candidate
        | Map.size running >= workerBound =
            pure (pending, running)
        | otherwise =
            case extractFirstReady candidate sealedByAddress pending of
                Nothing ->
                    pure (pending, running)
                Just (task, remaining) -> do
                    checker <- Async.async do
                        completed <-
                            (Exception.try
                                (observeModuleChecker observationRef
                                    (checkModule task sealedByAddress))
                                :: IO
                                    (Either
                                        SomeException
                                        ModuleCheckResult))
                        pure (moduleTaskOrdinal task, completed)
                    startReadyModules
                        remaining
                        (Map.insert
                            (moduleTaskOrdinal task)
                            checker
                            running)
                        sealedByAddress
                        candidate

    checkModule task sealedByAddress =
      withVampireRequestOwner executor \requestOwner -> do
        let parsed = moduleTaskParsed task
            source = Felix.parsedModuleResolved parsed
            address = Felix.parsedModuleAddress parsed
        direct <-
            traverse
                (\directAddress ->
                    maybe
                        (throwIO
                            (VerificationMissingImportedModule
                                directAddress))
                        pure
                        (Map.lookup directAddress sealedByAddress))
                (moduleTaskDirectAddresses task)
        resolver <-
            typedVampireResolver
                requestOwner
                (moduleTaskOrdinal task)
                observationRef
        input <-
            either
                (throwIO . VerificationTypedInputError source)
                pure
                (Typed.typedModuleInput
                    foundation
                    (Typed.finalPreludeReadiness prelude)
                    resolver
                    validationRun
                    parsed
                    direct)
        loadCachedModule parsed direct >>= \case
            Just sealed -> do
                observeModuleRootAcquisition
                    observationRef Typed.ModuleRootHit
                pure
                    (ModuleCheckSucceeded
                        address
                        sealed
                        (completeAdmittedModule
                            (Typed.identifiedPhysicalModule parsed)))
            Nothing -> do
                typedResult <-
                    Exception.catch
                        (Typed.runTypedModule input)
                        (\failure ->
                            throwIO
                                (VerificationValidationIntegrityError
                                    source
                                    failure))
                case typedResult of
                    Typed.TypedModuleOpenFailed err ->
                        throwIO (VerificationTypedOpenError source err)
                    Typed.TypedModuleFailed err prefix -> do
                        let driverFailure =
                                VerificationTypedModuleError
                                    source err prefix
                        case classifyTypedModuleFailure err of
                            TypedIntegrityFailure ->
                                throwIO driverFailure
                            TypedCheckingRejection ->
                                reportFailure
                                    parsed
                                    prefix
                                    (TypedWorkspaceCheckingRejected
                                        driverFailure)
                            TypedVerificationRejection failed ->
                                reportFailure
                                    parsed
                                    prefix
                                    (TypedWorkspaceProverRejected failed)
                            TypedProverFailure failed ->
                                reportFailure
                                    parsed
                                    prefix
                                    (TypedWorkspaceProverRejected failed)
                    Typed.TypedModuleSucceeded sealed -> do
                        admittedModule <-
                            either
                                (throwIO
                                    . VerificationAdmittedViewError source)
                                pure
                                (checkedAdmittedModule
                                    True
                                    (Typed.identifiedPhysicalModule parsed)
                                    (Typed.sealedTypedModulePrefix sealed))
                        persistSealed
                            (Typed.identifiedPhysicalModule parsed)
                            sealed
                        observeModuleRootAcquisition
                            observationRef Typed.ModuleRootMiss
                        pure
                            (ModuleCheckSucceeded
                                address sealed admittedModule)

    reportFailure parsed prefix failure = do
        let source = Felix.parsedModuleResolved parsed
        admittedModule <-
            either
                (throwIO . VerificationAdmittedViewError source)
                pure
                (checkedAdmittedModule
                    False
                    (Typed.identifiedPhysicalModule parsed)
                    prefix)
        Store.withStoreCoordinator storeCoordinator
            (Store.writePendingModulePrefix store prefix)
            >>= either
                (throwIO . VerificationStoreFailure)
                pure
        pure (ModuleCheckRejected admittedModule failure)

    storeValidationLookup lookupStore =
        Declaration.validationLookup
            (\key ->
                Store.withStoreCoordinator storeCoordinator
                    (Store.loadProofValidation lookupStore key)
                    >>= either
                        (throwIO . VerificationStoreFailure)
                        pure)
            (\key ->
                Store.withStoreCoordinator storeCoordinator
                    (Store.loadDeclarationValidation lookupStore key)
                    >>= either
                        (throwIO . VerificationStoreFailure)
                        pure)

    validationRun =
        case validationMode of
            FreshStoreValidation ->
                Declaration.FreshValidation
            WarmStoreValidation ->
                Declaration.WarmValidation
                    (storeValidationLookup store)

    persistSealed input sealed = do
        artifactKey <-
            either
                (throwIO . VerificationModuleArtifactKeyError)
                pure
                (Semantic.moduleArtifactKey
                    (Typed.identifiedModuleOwner input)
                    (Felix.identifiedParsedModuleId
                        (Typed.identifiedModuleParsed input))
                    (Semantic.semanticInterfaceDirectInputs
                        (Typed.sealedTypedModuleSemantic sealed))
                    (Identity.theoryId foundation))
        let artifact =
                Semantic.moduleArtifactResult
                    artifactKey
                    (Syntax.moduleSyntaxAssertedId
                        (Typed.sealedTypedModuleSyntax sealed))
                    (Semantic.semanticInterfaceAssertedId
                        (Typed.sealedTypedModuleSemantic sealed))
        acknowledged <-
            Store.withStoreCoordinator storeCoordinator
                (Store.writeSealedModule
                    store
                    (Typed.sealedTypedModulePrefix sealed)
                    [Typed.sealedTypedModuleSyntax sealed]
                    [Typed.sealedTypedModuleSemantic sealed]
                    artifact)
                >>= either
                    (throwIO . VerificationStoreFailure)
                    pure
        unless
            (acknowledged == artifact)
            (throwIO
                (VerificationStoreFailure
                    Store.StoreModuleArtifactIdMismatch))

    loadCachedModule parsed direct =
        case validationMode of
            WarmStoreValidation -> do
                let owner =
                        Typed.identifiedModuleOwner
                            (Typed.identifiedPhysicalModule parsed)
                    directSemantic =
                        Semantic.semanticInterfaceAssertedId
                            (Typed.sealedTypedModuleSemantic
                                (Typed.finalPreludeModule prelude))
                        : ( Semantic.semanticInterfaceAssertedId
                                . Typed.sealedTypedModuleSemantic
                                <$> direct
                          )
                artifactKey <-
                    either
                        (throwIO . VerificationModuleArtifactKeyError)
                        pure
                        (Semantic.moduleArtifactKey
                            owner
                            (Felix.identifiedParsedModuleId
                                (Typed.identifiedModuleParsed
                                    (Typed.identifiedPhysicalModule parsed)))
                            directSemantic
                            (Identity.theoryId foundation))
                loaded <-
                    Store.withStoreCoordinator storeCoordinator
                        (Store.loadCachedModuleInstallation
                            memo
                            store
                            artifactKey
                            (Syntax.moduleSyntaxAssertedId
                                (Felix.parsedModuleSyntaxInterface parsed)))
                case loaded of
                    Left failure ->
                        throwIO (VerificationStoreFailure failure)
                    Right Nothing ->
                        pure Nothing
                    Right (Just installation) ->
                        either
                            (throwIO
                                . VerificationTypedCachedModuleError
                                    (Felix.parsedModuleResolved parsed))
                            (pure . Just)
                            (Typed.cachedSealedTypedModule
                                foundation
                                (Typed.finalPreludeModule prelude : direct)
                                installation)
            FreshStoreValidation ->
                pure Nothing

    taskMayStart candidate sealedByAddress task =
        maybe True
            (moduleTaskOrdinal task <)
            (candidateOrdinal <$> candidate)
            && all
                (`Map.member` sealedByAddress)
                (moduleTaskDirectAddresses task)

    extractFirstReady candidate sealedByAddress = go []
      where
        go _before [] = Nothing
        go before (task : after)
            | taskMayStart candidate sealedByAddress task =
                Just (task, reverse before <> after)
            | otherwise =
                go (task : before) after

    chooseEarlierFailure Nothing incoming = incoming
    chooseEarlierFailure (Just current) incoming
        | candidateOrdinal incoming < candidateOrdinal current = incoming
        | otherwise = current

    candidateOrdinal (ModuleFailureCandidate ordinal _admitted _failure) =
        ordinal

    candidateFailure (ModuleFailureCandidate _ordinal _admitted failure) =
        failure

    candidateAdmitted (ModuleFailureCandidate _ordinal admitted _failure) =
        admitted

    completeAdmittedWorkspace admittedByOrdinal =
        AdmittedTypedWorkspace
            ( completeAdmittedModule (Typed.finalPreludeInput prelude)
                : fmap snd (Map.toAscList admittedByOrdinal)
            )

    admittedWorkspaceThrough admittedByOrdinal selected =
        let cutoff = candidateOrdinal selected
            earlier = Map.filterWithKey
                (\ordinal _admitted -> ordinal < cutoff)
                admittedByOrdinal
        in AdmittedTypedWorkspace
            ( completeAdmittedModule (Typed.finalPreludeInput prelude)
                : ( fmap snd (Map.toAscList earlier)
                        <> [candidateAdmitted selected]
                  )
            )

    cancelModuleCheckers running = do
        traverse_ Async.cancel (Map.elems running)
        traverse_ Async.waitCatch (Map.elems running)

data TypedFailureClassification
    = TypedCheckingRejection
    | TypedVerificationRejection !FailedVerification
    | TypedProverFailure !FailedVerification
    | TypedIntegrityFailure

-- | Classify failures at the typed checking boundary conservatively.
--
-- Only source elaboration and recognized prover outcomes may retain an
-- admitted source report.  Every declaration/sealing invariant, including a
-- future constructor not explicitly recognized below, remains fatal.
classifyTypedModuleFailure
    :: Typed.TypedModuleFailure
    -> TypedFailureClassification
classifyTypedModuleFailure = \case
    Typed.TypedActionFailed{} ->
        TypedCheckingRejection
    Typed.TypedDeclarationFailed
            (Declaration.ProofObligationFailedAt
                location
                (Declaration.VampireProcessFailed processError)) ->
        classifyTypedProverResult location (Left processError)
    Typed.TypedDeclarationFailed
            (Declaration.ProofObligationFailedAt
                location
                (Declaration.VampireObligationRejected answer)) ->
        classifyTypedProverResult location (Right answer)
    _failure ->
        TypedIntegrityFailure

classifyTypedProverResult
    :: Location
    -> Either ProverProcessError ProverAnswer
    -> TypedFailureClassification
classifyTypedProverResult location result =
    case verificationFailureReason result of
        Nothing ->
            TypedIntegrityFailure
        Just reason ->
            let failed = FailedVerification location reason
            in case reason of
                CountermodelFailure{} ->
                    TypedVerificationRejection failed
                ContradictoryInputFailure{} ->
                    TypedVerificationRejection failed
                IndeterminateFailure{} ->
                    TypedProverFailure failed
                ProtocolFailure{} ->
                    TypedProverFailure failed
                TransportFailure{} ->
                    TypedProverFailure failed

typedVampireResolver
    :: VampireRequestOwner
    -> Natural
    -> IORef VerificationObservation
    -> IO Declaration.VampireResolver
typedVampireResolver
        requestOwner moduleOrdinal observationRef = do
    localOrdinalRef <- newIORef 1
    let reserve requests = do
            let batchSize = NonEmpty.length requests
                ordinalCount = fromIntegral batchSize
            firstOrdinal <- atomicModifyIORef' localOrdinalRef
                (\current -> (current + ordinalCount, current))
            let positions =
                    NonEmpty.fromList
                        [ workPosition moduleOrdinal ordinal
                        | ordinal <-
                            [firstOrdinal .. firstOrdinal + ordinalCount - 1]
                        ]
                preparedBytes =
                    foldl'
                        (\total request ->
                            total
                                + fromIntegral
                                    (preparedVerificationByteCount request))
                        0
                        requests
            atomicModifyIORef' observationRef \observation ->
                ( observation
                    { observedObligationBatchCount =
                        observedObligationBatchCount observation + 1
                    , observedPreparedObligationCount =
                        observedPreparedObligationCount observation + batchSize
                    , observedMaximumObligationBatchSize =
                        max batchSize
                            (observedMaximumObligationBatchSize observation)
                    , observedPreparedRequestBytes =
                        observedPreparedRequestBytes observation
                            + preparedBytes
                    }
                , ()
                )
            pure positions
        submit requests = do
            positions <- reserve requests
            traverse
                (uncurry (submitVampireRequest requestOwner))
                (NonEmpty.zip positions requests)
        observe elapsed =
            atomicModifyIORef' observationRef \observation ->
                ( observation
                    { observedRequestPreparationNanoseconds =
                        observedRequestPreparationNanoseconds observation
                            + elapsed
                    }
                , ()
                )
    pure (Declaration.vampireSubmissionResolver submit observe)

observeModuleRootAcquisition
    :: IORef VerificationObservation
    -> Typed.ModuleRootAcquisition
    -> IO ()
observeModuleRootAcquisition observationRef acquisition =
    atomicModifyIORef' observationRef \observation ->
        ( case acquisition of
            Typed.ModuleRootHit ->
                observation
                    { observedModuleRootHitCount =
                        observedModuleRootHitCount observation + 1
                    }
            Typed.ModuleRootMiss ->
                observation
                    { observedModuleRootMissCount =
                        observedModuleRootMissCount observation + 1
                    }
        , ()
        )

observeReadyModules
    :: IORef VerificationObservation
    -> Int
    -> IO ()
observeReadyModules observationRef readyCount =
    atomicModifyIORef' observationRef \observation ->
        ( observation
            { observedMaximumReadyModuleCount =
                max readyCount
                    (observedMaximumReadyModuleCount observation)
            }
        , ()
        )

observeModuleChecker
    :: IORef VerificationObservation
    -> IO value
    -> IO value
observeModuleChecker observationRef action = do
    atomicModifyIORef' observationRef \observation ->
        let live = observedLiveModuleCheckers observation + 1
        in
            ( observation
                { observedLiveModuleCheckers = live
                , observedMaximumLiveModuleCheckers =
                    max live
                        (observedMaximumLiveModuleCheckers observation)
                }
            , ()
            )
    action `Exception.finally`
        atomicModifyIORef' observationRef
            (\observation ->
                ( observation
                    { observedLiveModuleCheckers =
                        observedLiveModuleCheckers observation - 1
                    }
                , ()
                ))

mergeExecutorObservation
    :: IORef VerificationObservation
    -> VampireExecutorObservation
    -> IO ()
mergeExecutorObservation observationRef executorObserved =
    atomicModifyIORef' observationRef \observation ->
        ( observation
            { observedVampireRunCount =
                vampireExecutorRunCount executorObserved
            , observedMaximumLiveVampireProcesses =
                vampireExecutorMaximumLiveCount executorObserved
            , observedFirstVampireStart =
                vampireExecutorFirstStartNanoseconds executorObserved
            , observedFinalVampireSubmission =
                vampireExecutorFinalSubmissionNanoseconds executorObserved
            , observedFinalVampireCompletion =
                vampireExecutorFinalCompletionNanoseconds executorObserved
            , observedVampireExecutionNanoseconds =
                vampireExecutorExecutionNanoseconds executorObserved
            , observedLongestVampireExecutionNanoseconds =
                vampireExecutorLongestExecutionNanoseconds executorObserved
            }
        , ()
        )

finalizeVerificationMeasurements
    :: Word64
    -> Word64
    -> Word64
    -> Felix.ParseMeasurements
    -> Word64
    -> VerificationObservation
    -> VerificationMeasurements
finalizeVerificationMeasurements
        invocationStart
        checkingStart
        checkingEnd
        parseMeasurements
        sourcePreparation
        observation =
    VerificationMeasurements
        { verificationParseMeasurements =
            parseMeasurements
        , verificationSourcePreparationNanoseconds =
            sourcePreparation
        , verificationInvocationNanoseconds =
            checkingEnd - invocationStart
        , verificationCheckingNanoseconds =
            checkingEnd - checkingStart
        , verificationModuleCount =
            observedModuleCount observation
        , verificationDetectedProcessorCount =
            observedDetectedProcessorCount observation
        , verificationEffectiveJobs =
            observedEffectiveJobs observation
        , verificationJobsOverridden =
            observedJobsOverridden observation
        , verificationMaximumLiveModuleCheckers =
            observedMaximumLiveModuleCheckers observation
        , verificationMaximumLiveVampireProcesses =
            observedMaximumLiveVampireProcesses observation
        , verificationMaximumReadyModuleCount =
            observedMaximumReadyModuleCount observation
        , verificationObligationBatchCount =
            observedObligationBatchCount observation
        , verificationPreparedObligationCount =
            observedPreparedObligationCount observation
        , verificationMaximumObligationBatchSize =
            observedMaximumObligationBatchSize observation
        , verificationPreparedRequestBytes =
            observedPreparedRequestBytes observation
        , verificationRequestPreparationNanoseconds =
            observedRequestPreparationNanoseconds observation
        , verificationVampireRunCount =
            observedVampireRunCount observation
        , verificationModuleRootHitCount =
            observedModuleRootHitCount observation
        , verificationModuleRootMissCount =
            observedModuleRootMissCount observation
        , verificationFirstVampireStartNanoseconds =
            fmap
                (\started -> started - invocationStart)
                (observedFirstVampireStart observation)
        , verificationFinalVampireSubmissionNanoseconds =
            fmap
                (\submitted -> submitted - invocationStart)
                (observedFinalVampireSubmission observation)
        , verificationFinalVampireCompletionNanoseconds =
            fmap
                (\completed -> completed - invocationStart)
                (observedFinalVampireCompletion observation)
        , verificationVampireExecutionNanoseconds =
            observedVampireExecutionNanoseconds observation
        , verificationLongestVampireExecutionNanoseconds =
            observedLongestVampireExecutionNanoseconds observation
        }

renderVerificationMeasurements
    :: VerificationMeasurements
    -> Text
renderVerificationMeasurements measurements =
    StrictText.unwords
        [ "M0"
        , "source_setup_ms="
            <> renderNanoseconds
                (verificationSourcePreparationNanoseconds
                    measurements)
        , "resolution_ms="
            <> renderNanoseconds
                (Felix.parseMeasurementResolutionNanoseconds
                    parseMeasurements)
        , "candidate_probes=" <> renderIntegral
            (Felix.parseMeasurementCandidateProbeCount
                parseMeasurements)
        , "canonicalizations=" <> renderIntegral
            (Felix.parseMeasurementCanonicalizationCount
                parseMeasurements)
        , "target_inspections=" <> renderIntegral
            (Felix.parseMeasurementTargetInspectionCount
                parseMeasurements)
        , "tokenization_ms="
            <> renderNanoseconds
                (Felix.parseMeasurementTokenizationNanoseconds
                    parseMeasurements)
        , "scanning_ms="
            <> renderNanoseconds
                (Felix.parseMeasurementScanningNanoseconds
                    parseMeasurements)
        , "syntax_interface_ms="
            <> renderNanoseconds
                (Felix.parseMeasurementSyntaxInterfaceNanoseconds
                    parseMeasurements)
        , "parsing_ms="
            <> renderNanoseconds
                (Felix.parseMeasurementParsingNanoseconds
                    parseMeasurements)
        , "parsed_hits=" <> renderIntegral
            (Felix.parseMeasurementParsedHitCount parseMeasurements)
        , "parsed_misses=" <> renderIntegral
            (Felix.parseMeasurementParsedMissCount parseMeasurements)
        , "parser_tables=" <> renderIntegral
            (Felix.parseMeasurementParserTableMaterializationCount
                parseMeasurements)
        , "modules=" <> renderIntegral
            (verificationModuleCount measurements)
        , "detected_processors="
            <> maybe
                "unavailable"
                renderIntegral
                (verificationDetectedProcessorCount measurements)
        , "effective_jobs=" <> renderIntegral
            (verificationEffectiveJobs measurements)
        , "jobs_overridden="
            <> if verificationJobsOverridden measurements
                then "yes"
                else "no"
        , "max_module_checkers=" <> renderIntegral
            (verificationMaximumLiveModuleCheckers measurements)
        , "max_vampire_processes=" <> renderIntegral
            (verificationMaximumLiveVampireProcesses measurements)
        , "files_read=" <> renderIntegral
            (Felix.parseMeasurementModuleCount
                parseMeasurements)
        , "import_occurrences=" <> renderIntegral
            (Felix.parseMeasurementImportOccurrenceCount
                parseMeasurements)
        , "chunks=" <> renderIntegral
            (Felix.parseMeasurementChunkCount
                parseMeasurements)
        , "source_bytes=" <> renderIntegral
            (Felix.parseMeasurementSourceByteCount
                parseMeasurements)
        , "checking_ms="
            <> renderNanoseconds
                (verificationCheckingNanoseconds
                    measurements)
        , "batches=" <> renderIntegral
            (verificationObligationBatchCount measurements)
        , "obligations=" <> renderIntegral
            (verificationPreparedObligationCount measurements)
        , "max_batch=" <> renderIntegral
            (verificationMaximumObligationBatchSize
                measurements)
        , "prepared_bytes=" <> renderIntegral
            (verificationPreparedRequestBytes measurements)
        , "request_preparation_ms="
            <> renderNanoseconds
                (verificationRequestPreparationNanoseconds measurements)
        , "vampire_runs=" <> renderIntegral
            (verificationVampireRunCount measurements)
        , "module_root_hits=" <> renderIntegral
            (verificationModuleRootHitCount measurements)
        , "module_root_misses=" <> renderIntegral
            (verificationModuleRootMissCount measurements)
        , "first_vampire_ms="
            <> maybe
                "none"
                renderNanoseconds
                (verificationFirstVampireStartNanoseconds
                    measurements)
        , "vampire_ms="
            <> renderNanoseconds
                (verificationVampireExecutionNanoseconds
                    measurements)
        , "final_submission_ms="
            <> maybe
                "none"
                renderNanoseconds
                (verificationFinalVampireSubmissionNanoseconds
                    measurements)
        , "final_completion_ms="
            <> maybe
                "none"
                renderNanoseconds
                (verificationFinalVampireCompletionNanoseconds
                    measurements)
        , "vampire_span_ms="
            <> maybe
                "none"
                renderNanoseconds
                (vampireExecutionSpan measurements)
        , "longest_vampire_ms="
            <> renderNanoseconds
                (verificationLongestVampireExecutionNanoseconds
                    measurements)
        , "max_ready_modules=" <> renderIntegral
            (verificationMaximumReadyModuleCount
                measurements)
        , "total_ms="
            <> renderNanoseconds
                (verificationInvocationNanoseconds
                    measurements)
        ]
  where
    parseMeasurements =
        verificationParseMeasurements measurements

    vampireExecutionSpan measured = do
        started <- verificationFirstVampireStartNanoseconds measured
        completed <- verificationFinalVampireCompletionNanoseconds measured
        pure (completed - started)

renderNanoseconds :: Word64 -> Text
renderNanoseconds nanoseconds =
    renderIntegral (nanoseconds `div` 1000000)

renderIntegral :: Show number => number -> Text
renderIntegral =
    StrictText.pack . show

admittedWorkspaceReport
    :: AdmittedTypedWorkspace
    -> VerificationReport
admittedWorkspaceReport (AdmittedTypedWorkspace modules) =
    VerificationReport
        { verificationDirectEscapes =
            concatMap admittedModuleEscapes modules
        }

admittedModuleEscapes
    :: AdmittedTypedModule
    -> [ReportedEscape]
admittedModuleEscapes (AdmittedTypedModule declarations) =
    concatMap admittedDeclarationEscapes declarations

admittedDeclarationEscapes
    :: AdmittedTypedDeclaration
    -> [ReportedEscape]
admittedDeclarationEscapes
        (AdmittedTypedDeclaration _slot declaration) =
    axiomEscape <> proofEscapes
  where
    axiomEscape =
        case Typed.typedSourceDeclarationHead declaration of
            Raw.BlockAxiom location _title _marker _axiom ->
                [ReportedEscape ReportedSourceAxiom location]
            _ ->
                []
    proofEscapes =
        maybe [] omittedProofEscapes
            (Typed.typedSourceDeclarationProof declaration)

omittedProofEscapes :: Raw.Proof -> [ReportedEscape]
omittedProofEscapes = \case
    Raw.Omitted location ->
        [ReportedEscape ReportedOmitted location]
    Raw.Qed{} ->
        []
    Raw.Contradiction{} ->
        []
    Raw.ByCase _location cases ->
        concatMap (omittedProofEscapes . Raw.caseProof) cases
    Raw.ByContradiction _location proof ->
        omittedProofEscapes proof
    Raw.BySetInduction _location _term proof ->
        omittedProofEscapes proof
    Raw.ByOrdInduction _location proof ->
        omittedProofEscapes proof
    Raw.Assume _location _statement proof ->
        omittedProofEscapes proof
    Raw.FixSymbolic _location _variables _bound proof ->
        omittedProofEscapes proof
    Raw.FixSuchThat _location _variables _statement proof ->
        omittedProofEscapes proof
    Raw.Calc _location _quantifier _calculation proof ->
        omittedProofEscapes proof
    Raw.TakeVar _location _variables _bound _statement _justification proof ->
        omittedProofEscapes proof
    Raw.TakeNoun _location _noun _justification proof ->
        omittedProofEscapes proof
    Raw.Have _location _condition _statement _justification proof ->
        omittedProofEscapes proof
    Raw.Suffices _location _statement _justification proof ->
        omittedProofEscapes proof
    Raw.Subclaim _location _statement subproof continuation ->
        omittedProofEscapes subproof <> omittedProofEscapes continuation
    Raw.Define _location _variable _expression proof ->
        omittedProofEscapes proof
    Raw.DefineFunction
            _location _function _argument _value _domainVariable _domain
            proof ->
        omittedProofEscapes proof
    Raw.DefineFunctionLocal
            _location _function _argument _domain _target _ruleVariable
            _rules proof ->
        omittedProofEscapes proof

completedResult
    :: VerificationReport
    -> VerificationPresentation
    -> VerificationResult
completedResult report presentation
    | any ((== ReportedOmitted) . reportedEscapeKind)
        (verificationDirectEscapes report) =
            CompletedWithExplicitGaps report presentation
    | otherwise =
        VerificationCompleted report presentation

verify
    :: (MonadUnliftIO io, MonadLogger io)
    => Vampire
    -> FilePath
    -> io (Either VerificationDriverError VerificationResult)
verify prover file =
    fmap fst <$> verifyMeasured prover file

prepareVerifiedHtmlExportResult
    :: MonadIO io
    => VerificationPresentation
    -> io (Either HtmlExport.HtmlExportError [PreparedHtmlArtifact])
prepareVerifiedHtmlExportResult
        (VerificationPresentation workspace) = liftIO do
    hintsResult <- findAndReadRendererFile "lexicon.tsv"
    pure do
        hints <- hintsResult
        HtmlExport.prepareHtmlExport
            defaultHtmlMountPrefixes
            workspace
            hints

defaultHtmlMountPrefixes :: [(SourceMountId, [Text])]
defaultHtmlMountPrefixes =
    [ (sourceMountId "project", [])
    , (sourceMountId "library", ["library"])
    , (sourceMountId "debug", ["debug"])
    ]