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

-- | Explicit inputs and sealed outputs for the typed module driver.
module Felix.Checking.Module
    ( LiveModuleBinding(..)
    , IdentifiedModuleInput
    , identifiedPhysicalModule
    , identifiedReservedPrelude
    , identifiedModuleOwner
    , identifiedModuleBinding
    , identifiedModuleParsed
    , TypedSourceDeclaration
    , typedSourceDeclarationBlockIndex
    , typedSourceDeclarationHead
    , typedSourceDeclarationProof
    , typedSourceDeclarations
    , SealedTypedModule
    , sealedTypedModuleOwner
    , sealedTypedModuleSyntax
    , sealedTypedModuleSemantic
    , sealedTypedModuleEvidence
    , CachedTypedModuleError(..)
    , renderCachedTypedModuleError
    , cachedSealedTypedModule
    , sealedTypedModulePrefix
    , FinalPreludeSession
    , ModuleRootAcquisition(..)
    , finalPreludeSource
    , finalPreludeInput
    , finalPreludeModule
    , finalPreludeAcquisition
    , FinalPreludeReadiness
    , finalPreludeReadiness
    , BootstrapPreludeFixture
    , bootstrapPreludeInput
    , bootstrapPreludeModule
    , bootstrapPreludeReadiness
    , fixtureFinalPreludeReadinessFromSealed
    , BootstrapError(..)
    , buildBootstrapPreludeFixture
    , FinalPreludeReadinessError(..)
    , acquireFinalPreludeSession
    , TypedModuleInput
    , TypedModuleInputError(..)
    , renderTypedModuleInputError
    , typedModuleInput
    , TypedPathError(..)
    , TypedModuleFailure(..)
    , typedModuleFailureLocation
    , renderTypedModuleFailure
    , TypedModuleResult(..)
    , runTypedModule
    ) where

import Base
import Felix.Checking.Declaration qualified as Declaration
import Felix.Checking.Exact qualified as Exact
import Felix.Checking.Exact.Datatype qualified as ExactDatatype
import Felix.Checking.Exact.Inductive qualified as ExactInductive
import Felix.Checking.Exact.Proof qualified as ExactProof
import Felix.Checking.FinalPrelude qualified as FinalPrelude
import Felix.Checking.Foundation
import Felix.Checking.Identity
import Felix.Checking.Semantic
import Felix.Module
import Felix.Parse
import Felix.Prelude qualified as Prelude
import Felix.Source
import Felix.Store qualified as Store
import Felix.Report.Location
import Felix.Syntax.Interface
import Felix.Syntax.Abstract qualified as Raw

import Control.Monad (unless)
import Data.Bifunctor (first)
import Data.Text qualified as Text


data LiveModuleBinding
    = PhysicalModuleBinding !ResolvedSource
    | ReservedModuleBinding !FileId !FilePath
    deriving stock (Show, Eq)

data IdentifiedModuleInput = IdentifiedModuleInput
    !ModuleName
    !LiveModuleBinding
    !IdentifiedParsedModule

identifiedPhysicalModule :: ParsedModule -> IdentifiedModuleInput
identifiedPhysicalModule parsed =
    IdentifiedModuleInput
        (moduleName (parsedModuleAddress parsed))
        (PhysicalModuleBinding (parsedModuleResolved parsed))
        (parsedModuleIdentified parsed)

identifiedReservedPrelude
    :: Prelude.ReservedParsedPrelude
    -> IdentifiedModuleInput
identifiedReservedPrelude reserved =
    IdentifiedModuleInput
        (freshModuleInputOwner input)
        (ReservedModuleBinding
            (freshModuleInputFileId input)
            (freshModuleInputLocationPath input))
        (Prelude.reservedParsedPreludeModule reserved)
  where
    input = Prelude.reservedParsedPreludeInput reserved

identifiedModuleOwner :: IdentifiedModuleInput -> ModuleName
identifiedModuleOwner (IdentifiedModuleInput owner _binding _parsed) =
    owner

identifiedModuleBinding
    :: IdentifiedModuleInput
    -> LiveModuleBinding
identifiedModuleBinding
        (IdentifiedModuleInput _owner binding _parsed) =
    binding

identifiedModuleParsed
    :: IdentifiedModuleInput
    -> IdentifiedParsedModule
identifiedModuleParsed
        (IdentifiedModuleInput _owner _binding parsed) =
    parsed


-- | One source declaration as consumed by the typed module driver.
--
-- A claim and its immediately following proof occupy one declaration slot.
-- The head block index remains the syntax-occurrence association index.
data TypedSourceDeclaration = TypedSourceDeclaration
    !Int
    !Raw.Block
    !(Maybe Raw.Proof)

typedSourceDeclarationBlockIndex :: TypedSourceDeclaration -> Int
typedSourceDeclarationBlockIndex
        (TypedSourceDeclaration blockIndex _head _proof) =
    blockIndex

typedSourceDeclarationHead :: TypedSourceDeclaration -> Raw.Block
typedSourceDeclarationHead
        (TypedSourceDeclaration _blockIndex headBlock _proof) =
    headBlock

typedSourceDeclarationProof
    :: TypedSourceDeclaration
    -> Maybe Raw.Proof
typedSourceDeclarationProof
        (TypedSourceDeclaration _blockIndex _head proof) =
    proof

typedSourceDeclarations
    :: IdentifiedParsedModule
    -> [TypedSourceDeclaration]
typedSourceDeclarations parsed =
    [ declaration
    | item <- typedSourceItems (identifiedParsedModuleBlocks parsed)
    , Just declaration <- [sourceItemDeclaration item]
    ]

data TypedSourceItem
    = TypedSourceDeclarationItem !TypedSourceDeclaration
    | TypedUnmatchedSourceProof !Location

sourceItemDeclaration
    :: TypedSourceItem
    -> Maybe TypedSourceDeclaration
sourceItemDeclaration = \case
    TypedSourceDeclarationItem declaration -> Just declaration
    TypedUnmatchedSourceProof{} -> Nothing

typedSourceItems :: [Raw.Block] -> [TypedSourceItem]
typedSourceItems = go 0
  where
    go _blockIndex [] = []
    go blockIndex (block@Raw.BlockClaim{} : remaining) =
        case remaining of
            Raw.BlockProof _location proof _end : rest ->
                TypedSourceDeclarationItem
                    (TypedSourceDeclaration blockIndex block (Just proof))
                    : go (blockIndex + 2) rest
            _ ->
                TypedSourceDeclarationItem
                    (TypedSourceDeclaration blockIndex block Nothing)
                    : go (blockIndex + 1) remaining
    go blockIndex (Raw.BlockProof location _proof _end : remaining) =
        TypedUnmatchedSourceProof location
            : go (blockIndex + 1) remaining
    go blockIndex (block : remaining) =
        TypedSourceDeclarationItem
            (TypedSourceDeclaration blockIndex block Nothing)
            : go (blockIndex + 1) remaining


data SealedTypedModule = SealedTypedModule
    !ModuleName
    !ModuleSyntaxInterface
    !SemanticInterface
    !Declaration.PendingModulePrefix
    !Declaration.ImportedModuleEvidence

sealedTypedModuleOwner :: SealedTypedModule -> ModuleName
sealedTypedModuleOwner (SealedTypedModule owner _syntax _semantic _prefix _evidence) =
    owner

sealedTypedModuleSyntax
    :: SealedTypedModule
    -> ModuleSyntaxInterface
sealedTypedModuleSyntax
        (SealedTypedModule _owner syntax _semantic _prefix _evidence) =
    syntax

sealedTypedModuleSemantic
    :: SealedTypedModule
    -> SemanticInterface
sealedTypedModuleSemantic
        (SealedTypedModule _owner _syntax semantic _prefix _evidence) =
    semantic

sealedTypedModulePrefix
    :: SealedTypedModule
    -> Declaration.PendingModulePrefix
sealedTypedModulePrefix
        (SealedTypedModule _owner _syntax _semantic prefix _evidence) =
    prefix

sealedTypedModuleEvidence
    :: SealedTypedModule
    -> Declaration.ImportedModuleEvidence
sealedTypedModuleEvidence
        (SealedTypedModule _owner _syntax _semantic _prefix evidence) =
    evidence

data CachedTypedModuleError
    = CachedTypedModuleEvidenceError !Declaration.DeclarationError
    deriving stock (Show, Eq)

renderCachedTypedModuleError :: CachedTypedModuleError -> Text
renderCachedTypedModuleError = \case
    CachedTypedModuleEvidenceError failure ->
        Declaration.renderDeclarationError failure

cachedSealedTypedModule
    :: CheckedFoundation
    -> [SealedTypedModule]
    -> Store.CachedModuleInstallation
    -> Either CachedTypedModuleError SealedTypedModule
cachedSealedTypedModule
        foundation parents installation = do
    evidence <-
        first CachedTypedModuleEvidenceError
            (Declaration.validateImportedModuleEvidence
                (theoryId foundation)
                (sealedTypedModuleEvidence <$> parents)
                semantic
                objects
                propositions)
    pure
        (SealedTypedModule
            owner
            syntax
            semantic
            (Declaration.emptyPendingModulePrefix
                (Store.cachedInstallationFinalPrefix installation))
            evidence)
  where
    syntax = Store.cachedInstallationSyntax installation
    semantic = Store.cachedInstallationSemantic installation
    owner = semanticInterfaceOwner semantic
    objects = Store.cachedInstallationObjects installation
    propositions = Store.cachedInstallationPropositions installation


data ModuleRootAcquisition
    = ModuleRootHit
    | ModuleRootMiss
    deriving stock (Show, Eq)

data FinalPreludeSession = FinalPreludeSession
    !Prelude.ReservedPreludeSourceInput
    !IdentifiedModuleInput
    !SealedTypedModule
    !ModuleRootAcquisition

finalPreludeSource
    :: FinalPreludeSession
    -> Prelude.ReservedPreludeSourceInput
finalPreludeSource
        (FinalPreludeSession source _input _module _acquisition) =
    source

finalPreludeInput
    :: FinalPreludeSession
    -> IdentifiedModuleInput
finalPreludeInput (FinalPreludeSession _source input _module _acquisition) =
    input

finalPreludeModule
    :: FinalPreludeSession
    -> SealedTypedModule
finalPreludeModule (FinalPreludeSession _source _input sealed _acquisition) =
    sealed

finalPreludeAcquisition
    :: FinalPreludeSession
    -> ModuleRootAcquisition
finalPreludeAcquisition
        (FinalPreludeSession _source _input _sealed acquisition) =
    acquisition

newtype FinalPreludeReadiness = FinalPreludeReadiness
    SealedTypedModule

finalPreludeReadiness
    :: FinalPreludeSession
    -> FinalPreludeReadiness
finalPreludeReadiness =
    FinalPreludeReadiness . finalPreludeModule

-- | Test-only empty-prelude fixture.
--
-- It is exported for focused exact-compiler tests.  Production acquisition is
-- exclusively 'acquireFinalPreludeSession'.
newtype BootstrapPreludeFixture = BootstrapPreludeFixture
    FinalPreludeSession

bootstrapPreludeInput
    :: BootstrapPreludeFixture
    -> IdentifiedModuleInput
bootstrapPreludeInput (BootstrapPreludeFixture fixture) =
    finalPreludeInput fixture

bootstrapPreludeModule
    :: BootstrapPreludeFixture
    -> SealedTypedModule
bootstrapPreludeModule (BootstrapPreludeFixture fixture) =
    finalPreludeModule fixture

-- | Test-only seam for the empty bootstrap compiler input.
bootstrapPreludeReadiness
    :: BootstrapPreludeFixture
    -> FinalPreludeReadiness
bootstrapPreludeReadiness =
    FinalPreludeReadiness . bootstrapPreludeModule

-- | Test-only seam for exercising a synthetic distinguished prelude.
fixtureFinalPreludeReadinessFromSealed
    :: SealedTypedModule
    -> FinalPreludeReadiness
fixtureFinalPreludeReadinessFromSealed =
    FinalPreludeReadiness

data BootstrapError
    = BootstrapParseFailed !Prelude.PreludeParseError
    | BootstrapDriverOpenFailed !Declaration.DriverOpenError
    | BootstrapDeclarationFailed !Declaration.DeclarationError
    | BootstrapSealFailed !SemanticInterfaceError
    deriving stock (Show)

-- | Construct the empty distinguished prelude used only by compiler fixtures.
buildBootstrapPreludeFixture
    :: CheckedFoundation
    -> Declaration.VampireResolver
    -> IO (Either BootstrapError BootstrapPreludeFixture)
buildBootstrapPreludeFixture foundation resolver = do
    parsedResult <-
        Prelude.parseReservedPreludeSource
            Prelude.emptyBootstrapSourceInput
    case parsedResult of
        Left err ->
            pure (Left (BootstrapParseFailed err))
        Right reserved -> do
            let input = identifiedReservedPrelude reserved
                syntax =
                    identifiedParsedModuleSyntaxInterface
                        (identifiedModuleParsed input)
            driver <-
                Declaration.runModuleDriver
                    foundation
                    preludeModuleName
                    []
                    resolver
                    Declaration.FreshValidation
                    emptyDriver
            pure case driver of
                Left err ->
                    Left (BootstrapDriverOpenFailed err)
                Right (Declaration.DriverSucceeded
                        () semantic prefix _closure) ->
                    Right
                        (BootstrapPreludeFixture
                            (FinalPreludeSession
                                Prelude.emptyBootstrapSourceInput
                                input
                                (SealedTypedModule
                                    preludeModuleName
                                    syntax
                                    semantic
                                    prefix
                                    (Declaration.freshImportedModuleEvidence
                                        []
                                        semantic
                                        prefix))
                                ModuleRootMiss))
                Right
                    (Declaration.DriverFailed
                        (Declaration.DriverDeclarationFailed err)
                        _prefix) ->
                            Left (BootstrapDeclarationFailed err)
                Right (Declaration.DriverSealFailed err _prefix) ->
                    Left (BootstrapSealFailed err)
  where
    emptyDriver :: Declaration.ModuleDriver Void ()
    emptyDriver = pure ()


data FinalPreludeReadinessError
    = FinalPreludeReadinessSourceLoadFailed !Prelude.PreludeLoadError
    | FinalPreludeReadinessSourceParseFailed !Prelude.PreludeParseError
    | FinalPreludeReadinessBuildFailed !FinalPrelude.FinalPreludeFailure
    | FinalPreludeReadinessBuildOpenFailed !Declaration.DriverOpenError
    | FinalPreludeReadinessArtifactKeyFailed !ModuleArtifactKeyError
    | FinalPreludeReadinessStoreFailed !Store.StoreFailure
    | FinalPreludeReadinessCachedModuleFailed !CachedTypedModuleError
    | FinalPreludeReadinessAcknowledgementMismatch
        !ModuleArtifactResult
        !ModuleArtifactResult
    deriving stock (Show)

-- | Acquire the exact packaged final prelude through its ordinary module root.
--
-- Loading and parsing happen once before the root lookup.  A hit is validated
-- and materialized through the generic cached-module boundary; a miss reuses
-- that parsed input for confined construction and atomic publication.
acquireFinalPreludeSession
    :: Store.StoreMemo
    -> Store.Store
    -> CheckedFoundation
    -> Declaration.VampireResolver
    -> IO (Either FinalPreludeReadinessError FinalPreludeSession)
acquireFinalPreludeSession memo store foundation resolver =
    Prelude.loadReservedPreludeSourceInput >>= \case
        Left failure ->
            pure (Left (FinalPreludeReadinessSourceLoadFailed failure))
        Right source ->
            Prelude.parseReservedPreludeSource source >>= \case
                Left failure ->
                    pure (Left (FinalPreludeReadinessSourceParseFailed failure))
                Right parsed ->
                    acquire source parsed
  where
    acquire source parsed =
        case moduleArtifactKey
                preludeModuleName
                parsedId
                []
                (theoryId foundation) of
            Left failure ->
                pure (Left (FinalPreludeReadinessArtifactKeyFailed failure))
            Right key -> do
                Store.loadCachedModuleInstallation
                    memo store key (moduleSyntaxAssertedId syntax) >>= \case
                    Left failure ->
                        pure (Left (FinalPreludeReadinessStoreFailed failure))
                    Right (Just installation) ->
                        pure do
                            sealed <- first FinalPreludeReadinessCachedModuleFailed
                                (cachedSealedTypedModule
                                    foundation [] installation)
                            pure
                                (FinalPreludeSession
                                    source
                                    identified sealed ModuleRootHit)
                    Right Nothing ->
                        build source parsed key
      where
        identified = identifiedReservedPrelude parsed
        parsedId = identifiedParsedModuleId (identifiedModuleParsed identified)
        syntax = identifiedParsedModuleSyntaxInterface
            (identifiedModuleParsed identified)

    build source parsed key =
        FinalPrelude.buildParsedFinalPreludeCandidate
            foundation parsed resolver >>= \case
                FinalPrelude.FinalPreludeBuildFailed failure _prefix ->
                    pure (Left (FinalPreludeReadinessBuildFailed failure))
                FinalPrelude.FinalPreludeBuildOpenFailed failure ->
                    pure (Left (FinalPreludeReadinessBuildOpenFailed failure))
                FinalPrelude.FinalPreludeBuilt candidate ->
                    publish source key candidate
                FinalPrelude.FinalPreludeSourceLoadFailed failure ->
                    pure (Left (FinalPreludeReadinessSourceLoadFailed failure))
                FinalPrelude.FinalPreludeSourceParseFailed failure ->
                    pure (Left (FinalPreludeReadinessSourceParseFailed failure))

    publish source key candidate = do
        let parsed = FinalPrelude.finalPreludeParsed candidate
            identified = identifiedReservedPrelude parsed
            syntax = FinalPrelude.finalPreludeSyntax candidate
            semantic = FinalPrelude.finalPreludeSemantic candidate
            prefix = FinalPrelude.finalPreludePrefix candidate
            artifact =
                moduleArtifactResult
                    key
                    (moduleSyntaxAssertedId syntax)
                    (semanticInterfaceAssertedId semantic)
        Store.writeSealedModule
                store
                prefix
                [syntax]
                [semantic]
                artifact >>= \case
            Left failure ->
                pure (Left (FinalPreludeReadinessStoreFailed failure))
            Right acknowledged
                | acknowledged /= artifact ->
                    pure
                        (Left
                            (FinalPreludeReadinessAcknowledgementMismatch
                                artifact
                                acknowledged))
                | otherwise ->
                    pure
                        (Right
                            (FinalPreludeSession
                                source
                                identified
                                (SealedTypedModule
                                    preludeModuleName
                                    syntax
                                    semantic
                                    prefix
                                    (Declaration.freshImportedModuleEvidence
                                        []
                                        semantic
                                        prefix))
                                ModuleRootMiss))


data TypedModuleInput = TypedModuleInput
    !ModuleName
    !IdentifiedModuleInput
    !ModuleSyntaxInterface
    !CheckedFoundation
    !FinalPreludeReadiness
    ![SealedTypedModule]
    !Declaration.VampireResolver
    !Declaration.ValidationRun

data TypedModuleInputError
    = TypedDirectModuleMismatch ![ModuleName] ![ModuleName]
    | TypedSyntaxInputMismatch ![SyntaxInterfaceId] ![SyntaxInterfaceId]
    deriving stock (Show, Eq)

renderTypedModuleInputError :: TypedModuleInputError -> Text
renderTypedModuleInputError = \case
    TypedDirectModuleMismatch expected actual ->
        "direct module inputs differ: expected " <> shown expected
            <> ", found " <> shown actual
    TypedSyntaxInputMismatch expected actual ->
        "direct syntax inputs differ: expected " <> shown expected
            <> ", found " <> shown actual
  where
    shown :: Show value => value -> Text
    shown = Text.pack . show

typedModuleInput
    :: CheckedFoundation
    -> FinalPreludeReadiness
    -> Declaration.VampireResolver
    -> Declaration.ValidationRun
    -> ParsedModule
    -> [SealedTypedModule]
    -> Either TypedModuleInputError TypedModuleInput
typedModuleInput
        foundation readiness resolver validationRun parsed direct = do
    unless (expectedOwners == actualOwners)
        (Left
            (TypedDirectModuleMismatch
                expectedOwners
                actualOwners))
    unless (expectedSyntax == actualSyntax)
        (Left
            (TypedSyntaxInputMismatch
                expectedSyntax
                actualSyntax))
    pure
        (TypedModuleInput
            owner
            identified
            syntax
            foundation
            readiness
            direct
            resolver
            validationRun)
  where
    identified = identifiedPhysicalModule parsed
    owner = identifiedModuleOwner identified
    syntax = identifiedParsedModuleSyntaxInterface (identifiedModuleParsed identified)
    expectedOwners =
        moduleName
            <$> nubOrd
                (parsedImportedAddress
                    <$> parsedModuleImports parsed)
    actualOwners = sealedTypedModuleOwner <$> direct
    expectedSyntax =
        nubOrd
            ( moduleSyntaxAssertedId
                (sealedTypedModuleSyntax prelude)
              : ( moduleSyntaxAssertedId
                    . sealedTypedModuleSyntax
                    <$> direct
                )
            )
    actualSyntax = moduleSyntaxDirectInputs syntax
    FinalPreludeReadiness prelude = readiness

data TypedPathError
    = TypedExactCompileFailed !Exact.ExactCompileError
    | TypedExactDatatypeFailed !ExactDatatype.ExactDatatypeError
    | TypedExactInductiveFailed !ExactInductive.ExactInductiveError
    | TypedExactProofFailed !ExactProof.ExactProofError
    | TypedUnmatchedProof !Location
    deriving stock (Show, Eq)

data TypedModuleFailure
    = TypedDeclarationFailed !Declaration.DeclarationError
    | TypedActionFailed !TypedPathError
    | TypedSealFailed !SemanticInterfaceError
    deriving stock (Show, Eq)

typedModuleFailureLocation :: TypedModuleFailure -> Maybe Location
typedModuleFailureLocation = \case
    TypedActionFailed (TypedExactCompileFailed failure) ->
        Just (Exact.exactCompileErrorLocation failure)
    TypedActionFailed (TypedExactDatatypeFailed failure) ->
        Just (ExactDatatype.exactDatatypeErrorLocation failure)
    TypedActionFailed (TypedExactInductiveFailed failure) ->
        Just (ExactInductive.exactInductiveErrorLocation failure)
    TypedActionFailed (TypedExactProofFailed failure) ->
        Just (ExactProof.exactProofErrorLocation failure)
    TypedActionFailed (TypedUnmatchedProof location) ->
        Just location
    TypedDeclarationFailed failure ->
        Declaration.declarationErrorLocation failure
    TypedSealFailed{} ->
        Nothing

renderTypedModuleFailure :: TypedModuleFailure -> Text
renderTypedModuleFailure = \case
    TypedDeclarationFailed failure ->
        Declaration.renderDeclarationError failure
    TypedActionFailed (TypedExactCompileFailed failure) ->
        Exact.renderExactCompileError failure
    TypedActionFailed (TypedExactDatatypeFailed failure) ->
        ExactDatatype.renderExactDatatypeError failure
    TypedActionFailed (TypedExactInductiveFailed failure) ->
        ExactInductive.renderExactInductiveError failure
    TypedActionFailed (TypedExactProofFailed failure) ->
        ExactProof.renderExactProofError failure
    TypedActionFailed (TypedUnmatchedProof location) ->
        locationToText location
            <> ": this proof does not follow a claim"
    TypedSealFailed failure ->
        renderSemanticInterfaceError failure

data TypedModuleResult
    = TypedModuleOpenFailed !Declaration.DriverOpenError
    | TypedModuleSucceeded !SealedTypedModule
    | TypedModuleFailed
        !TypedModuleFailure
        !Declaration.PendingModulePrefix

data PlannedTypedDeclaration
    = PlannedBinding
        !(Declaration.PlannedDeclaration
            Exact.CheckedExactBindingAuthorization)
    | PlannedSourceAxiom
        !(Declaration.PlannedDeclaration ())
    | PlannedInductive
        !(Declaration.PlannedDeclaration
            ExactInductive.CheckedExactInductiveAuthorization)
    | PlannedDatatype
        !(Declaration.PlannedDeclaration
            ExactDatatype.CheckedExactDatatypeAuthorization)
    | PlannedStructure
        !(Declaration.PlannedDeclaration
            Exact.CheckedExactStructureAuthorization)
    | PlannedProof
        !(Declaration.PlannedDeclaration
            ExactProof.CheckedExactProofAuthorization)

data TypedPlanningFailure
    = TypedPlanningPathFailure !TypedPathError
    | TypedPlanningDeclarationFailure !Declaration.DeclarationError

data TypedModulePlan = TypedModulePlan
    ![PlannedTypedDeclaration]
    !(Maybe TypedPlanningFailure)

runTypedModule :: TypedModuleInput -> IO TypedModuleResult
runTypedModule
        (TypedModuleInput
            owner identified syntax foundation readiness direct resolver
            validationRun) = do
    let FinalPreludeReadiness prelude = readiness
        action = do
            traverse_
                (Declaration.importSealedModuleDriver
                    . sealedTypedModuleEvidence)
                effectiveDirect
            TypedModulePlan planned terminal <-
                Declaration.runProspectiveLoweringDriver
                    (planSourceItems []
                        (typedSourceItems
                            (identifiedParsedModuleBlocks
                                (identifiedModuleParsed identified))))
            traverse_ admitPlannedDeclaration planned
            traverse_ failPlanning terminal
        semanticDirect =
            semanticInterfaceAssertedId
                (sealedTypedModuleSemantic prelude)
                : ( semanticInterfaceAssertedId
                        . sealedTypedModuleSemantic
                        <$> direct
                  )
        effectiveDirect =
            prelude : direct
        occurrences =
            identifiedParsedModuleSyntaxOccurrences
                (identifiedModuleParsed identified)
        planSourceItems completed [] =
            pure (TypedModulePlan (reverse completed) Nothing)
        planSourceItems completed (item : remaining) =
            case item of
                TypedUnmatchedSourceProof location ->
                    pure
                        (TypedModulePlan
                            (reverse completed)
                            (Just
                                (TypedPlanningPathFailure
                                    (TypedUnmatchedProof location))))
                TypedSourceDeclarationItem declaration -> do
                    planDeclaration declaration >>= \case
                        Left failure ->
                            pure
                                (TypedModulePlan
                                    (reverse completed)
                                    (Just failure))
                        Right planned ->
                            planSourceItems (planned : completed) remaining

        planDeclaration sourceDeclaration =
            case block of
                Raw.BlockClaim{} ->
                    planClaim block explicitProof
                Raw.BlockProof{} ->
                    impossible
                        "typed declaration association retained a proof head"
                Raw.BlockSig{} ->
                    planSelected block
                Raw.BlockAbbr{} ->
                    planSelected block
                Raw.BlockDefn{} ->
                    planSelected block
                Raw.BlockAxiom{} ->
                    planSourceAxiom block
                Raw.BlockInductive{} ->
                    planInductive block
                Raw.BlockData{} ->
                    planDatatype block
                Raw.BlockStruct{} ->
                    planStructure block
          where
            blockIndex =
                typedSourceDeclarationBlockIndex sourceDeclaration
            block = typedSourceDeclarationHead sourceDeclaration
            explicitProof =
                typedSourceDeclarationProof sourceDeclaration

            planSelected selected = do
                prepared <-
                    Exact.prepareExactDeclaration
                        selected
                        [ parsedSyntaxOccurrenceEntry occurrence
                        | occurrence <- occurrences
                        , parsedSyntaxOccurrenceBlockIndex occurrence
                            == blockIndex
                        ]
                case prepared of
                    Left failure ->
                        pure
                            (Left
                                (TypedPlanningPathFailure
                                    (TypedExactCompileFailed failure)))
                    Right declaration -> do
                        Exact.lowerPreparedExactBinding declaration >>= \case
                            Left failure -> planningDeclarationFailure failure
                            Right checked ->
                                planChecked PlannedBinding checked

            planSourceAxiom selected = do
                prepared <- Exact.prepareExactSourceAxiom selected
                case prepared of
                    Left failure ->
                        pure
                            (Left
                                (TypedPlanningPathFailure
                                    (TypedExactCompileFailed failure)))
                    Right axiom -> do
                        Exact.lowerPreparedExactSourceAxiom axiom >>= \case
                            Left failure -> planningDeclarationFailure failure
                            Right checked ->
                                planChecked PlannedSourceAxiom checked

            planInductive selected = do
                prepared <-
                    ExactInductive.prepareExactInductive
                        foundation
                        selected
                        [ parsedSyntaxOccurrenceEntry occurrence
                        | occurrence <- occurrences
                        , parsedSyntaxOccurrenceBlockIndex occurrence
                            == blockIndex
                        ]
                case prepared of
                    Left failure ->
                        pure
                            (Left
                                (TypedPlanningPathFailure
                                    (TypedExactInductiveFailed failure)))
                    Right inductive -> do
                        ExactInductive.lowerPreparedExactInductive inductive
                            >>= \case
                                Left failure ->
                                    planningDeclarationFailure failure
                                Right checked ->
                                    planChecked PlannedInductive checked

            planDatatype selected = do
                prepared <-
                    ExactDatatype.prepareExactDatatype
                        selected
                        [ ( parsedSyntaxOccurrenceLocation occurrence
                          , parsedSyntaxOccurrenceMarker occurrence
                          , parsedSyntaxOccurrenceEntry occurrence
                          )
                        | occurrence <- occurrences
                        , parsedSyntaxOccurrenceBlockIndex occurrence
                            == blockIndex
                        ]
                case prepared of
                    Left failure ->
                        pure
                            (Left
                                (TypedPlanningPathFailure
                                    (TypedExactDatatypeFailed failure)))
                    Right datatype -> do
                        ExactDatatype.lowerPreparedExactDatatype datatype
                            >>= \case
                                Left failure ->
                                    planningDeclarationFailure failure
                                Right checked ->
                                    planChecked PlannedDatatype checked

            planStructure selected = do
                prepared <-
                    Exact.prepareExactStructure
                        selected
                        [ parsedSyntaxOccurrenceEntry occurrence
                        | occurrence <- occurrences
                        , parsedSyntaxOccurrenceBlockIndex occurrence
                            == blockIndex
                        ]
                case prepared of
                    Left failure ->
                        pure
                            (Left
                                (TypedPlanningPathFailure
                                    (TypedExactCompileFailed failure)))
                    Right structure -> do
                        Exact.lowerPreparedExactStructure structure >>= \case
                            Left failure -> planningDeclarationFailure failure
                            Right checked ->
                                planChecked PlannedStructure checked

            planClaim selected selectedProof = do
                prepared <-
                    ExactProof.prepareExactProof selected selectedProof
                case prepared of
                    Left failure ->
                        pure
                            (Left
                                (TypedPlanningPathFailure
                                    (TypedExactProofFailed failure)))
                    Right proof -> do
                        ExactProof.lowerPreparedExactProof proof >>= \case
                            Left failure -> planningDeclarationFailure failure
                            Right checked ->
                                planChecked PlannedProof checked

            planChecked
                :: forall body.
                   (Declaration.PlannedDeclaration body
                        -> PlannedTypedDeclaration)
                -> Declaration.CheckedDeclaration body
                -> Declaration.LoweringDriver
                    (Either TypedPlanningFailure PlannedTypedDeclaration)
            planChecked constructor checked =
                Declaration.planCheckedDeclaration checked >>= \case
                    Left failure -> planningDeclarationFailure failure
                    Right planned -> pure (Right (constructor planned))

            planningDeclarationFailure =
                pure . Left . TypedPlanningDeclarationFailure

        admitPlannedDeclaration = \case
            PlannedBinding planned ->
                void
                    (Declaration.admitPlannedCheckedDeclaration
                        planned Exact.authorizeCheckedExactBinding)
            PlannedSourceAxiom planned ->
                void
                    (Declaration.admitPlannedCheckedDeclaration
                        planned Exact.authorizeCheckedExactSourceAxiom)
            PlannedInductive planned ->
                void
                    (Declaration.admitPlannedCheckedDeclaration
                        planned
                        ExactInductive.authorizeCheckedExactInductive)
            PlannedDatatype planned ->
                void
                    (Declaration.admitPlannedCheckedDeclaration
                        planned ExactDatatype.authorizeCheckedExactDatatype)
            PlannedStructure planned ->
                void
                    (Declaration.admitPlannedCheckedDeclaration
                        planned Exact.authorizeCheckedExactStructure)
            PlannedProof planned ->
                void
                    (Declaration.admitPlannedCheckedDeclaration
                        planned ExactProof.authorizeCheckedExactProof)

        failPlanning = \case
            TypedPlanningPathFailure failure ->
                Declaration.failModuleDriver failure
            TypedPlanningDeclarationFailure failure ->
                Declaration.failDeclarationDriver failure
    result <-
        Declaration.runModuleDriver
            foundation
            owner
            semanticDirect
            resolver
            validationRun
            action
    pure case result of
        Left err ->
            TypedModuleOpenFailed err
        Right (Declaration.DriverSucceeded () semantic prefix _closure) ->
            TypedModuleSucceeded
                (SealedTypedModule
                    owner
                    syntax
                    semantic
                    prefix
                    (Declaration.freshImportedModuleEvidence
                        (sealedTypedModuleEvidence <$> effectiveDirect)
                        semantic
                        prefix))
        Right
            (Declaration.DriverFailed failure prefix) ->
                TypedModuleFailed
                    (case failure of
                        Declaration.DriverDeclarationFailed err ->
                            TypedDeclarationFailed err
                        Declaration.DriverActionFailed err ->
                            TypedActionFailed err)
                    prefix
        Right (Declaration.DriverSealFailed err prefix) ->
            TypedModuleFailed (TypedSealFailed err) prefix