Migrate to `Felix` namespaceHEADhotg

1 files changed, 986 insertions, 0 deletions

diff --git a/source/Felix/Checking/Module.hs b/source/Felix/Checking/Module.hs
new file mode 100644
index 0000000..88c8fef
--- /dev/null
+++ b/source/Felix/Checking/Module.hs
@@ -0,0 +1,986 @@
+{-# 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