path: root/source/Checking/Module.hs

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

-- | Explicit inputs and sealed outputs for the typed module driver.
module Checking.Module
    ( LiveModuleBinding(..)
    , IdentifiedModuleInput
    , identifiedPhysicalModule
    , identifiedReservedPrelude
    , identifiedModuleOwner
    , identifiedModuleBinding
    , identifiedModuleParsed
    , SealedTypedModule
    , sealedTypedModuleOwner
    , sealedTypedModuleSyntax
    , sealedTypedModuleSemantic
    , sealedTypedModuleEvidence
    , CachedTypedModuleError(..)
    , renderCachedTypedModuleError
    , cachedSealedTypedModule
    , sealedTypedModulePrefix
    , MigrationPreludeSession
    , migrationPreludeInput
    , migrationPreludeModule
    , BootstrapWalkingReadiness
    , bootstrapWalkingReadiness
    , bootstrapWalkingReadinessFromSealed
    , BootstrapCompilerReadiness
    , bootstrapCompilerReadiness
    , BootstrapError(..)
    , buildBootstrapPreludeSession
    , TypedModuleInput
    , TypedModuleInputError(..)
    , renderTypedModuleInputError
    , typedModuleInput
    , TypedPathError(..)
    , TypedModuleFailure(..)
    , typedModuleFailureLocation
    , renderTypedModuleFailure
    , TypedModuleResult(..)
    , runTypedModule
    ) where

import Base
import Checking.Declaration qualified as Declaration
import Checking.Foundation
import Checking.Identity
import Checking.Semantic
import Felix.Module
import Felix.Parse
import Felix.Prelude qualified as Prelude
import Felix.Source
import Report.Location
import Syntax.Interface

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
    !FreshParsedModule

identifiedPhysicalModule :: ParsedModule -> IdentifiedModuleInput
identifiedPhysicalModule parsed =
    IdentifiedModuleInput
        (moduleName (parsedModuleAddress parsed))
        (PhysicalModuleBinding (parsedModuleResolved parsed))
        (parsedModuleFresh 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
    -> FreshParsedModule
identifiedModuleParsed
        (IdentifiedModuleInput _owner _binding parsed) =
    parsed


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
    = CachedTypedModuleOwnerMismatch !ModuleName !ModuleName
    | CachedTypedModulePrefixError !PrefixContextError
    | CachedTypedModuleMissingEvidence
    deriving stock (Show, Eq)

renderCachedTypedModuleError :: CachedTypedModuleError -> Text
renderCachedTypedModuleError = \case
    CachedTypedModuleOwnerMismatch expected actual ->
        "cached semantic owner mismatch: expected "
            <> Text.pack (show expected)
            <> ", found " <> Text.pack (show actual)
    CachedTypedModulePrefixError{} ->
        "cached semantic module has an invalid initial prefix"
    CachedTypedModuleMissingEvidence ->
        "cached semantic module is missing proposition evidence"

cachedSealedTypedModule
    :: CheckedFoundation
    -> ModuleName
    -> ModuleSyntaxInterface
    -> SemanticInterface
    -> [SealedTypedModule]
    -> [AssertedObject]
    -> [CheckedPropositionContent]
    -> Either CachedTypedModuleError SealedTypedModule
cachedSealedTypedModule
        foundation owner syntax semantic parents objects propositions = do
    unless
        (semanticInterfaceOwner semantic == owner)
        (Left
            (CachedTypedModuleOwnerMismatch
                owner
                (semanticInterfaceOwner semantic)))
    prefix <-
        first CachedTypedModulePrefixError
            (initialPrefixContextId
                (theoryId foundation)
                owner
                (semanticInterfaceDirectInputs semantic))
    evidence <-
        maybe
            (Left CachedTypedModuleMissingEvidence)
            Right
            (Declaration.validatedImportedModuleEvidence
                (theoryId foundation)
                (sealedTypedModuleEvidence <$> parents)
                semantic
                objects
                propositions)
    pure
        (SealedTypedModule
            owner
            syntax
            semantic
            (Declaration.emptyPendingModulePrefix prefix)
            evidence)


data MigrationPreludeSession = MigrationPreludeSession
    !IdentifiedModuleInput
    !SealedTypedModule

migrationPreludeInput
    :: MigrationPreludeSession
    -> IdentifiedModuleInput
migrationPreludeInput (MigrationPreludeSession input _module) =
    input

migrationPreludeModule
    :: MigrationPreludeSession
    -> SealedTypedModule
migrationPreludeModule (MigrationPreludeSession _input sealed) =
    sealed

-- These fixture-only seams are discarded with the final-prelude cutover.
newtype BootstrapWalkingReadiness = BootstrapWalkingReadiness
    SealedTypedModule

bootstrapWalkingReadiness
    :: MigrationPreludeSession
    -> BootstrapWalkingReadiness
bootstrapWalkingReadiness =
    BootstrapWalkingReadiness . migrationPreludeModule

-- | Fixture seam for exercising a nonempty distinguished prelude before the
-- final source prelude is constructed.
bootstrapWalkingReadinessFromSealed
    :: SealedTypedModule
    -> BootstrapWalkingReadiness
bootstrapWalkingReadinessFromSealed =
    BootstrapWalkingReadiness

newtype BootstrapCompilerReadiness = BootstrapCompilerReadiness
    MigrationPreludeSession

bootstrapCompilerReadiness
    :: MigrationPreludeSession
    -> BootstrapCompilerReadiness
bootstrapCompilerReadiness =
    BootstrapCompilerReadiness

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

buildBootstrapPreludeSession
    :: CheckedFoundation
    -> Declaration.VampireResolver
    -> IO (Either BootstrapError MigrationPreludeSession)
buildBootstrapPreludeSession 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 =
                    freshParsedModuleSyntaxInterface
                        (identifiedModuleParsed input)
            driver <-
                Declaration.runModuleDriver
                    foundation
                    preludeModuleName
                    []
                    resolver
                    Declaration.FreshValidation
                    emptyDriver
            pure case driver of
                Left err ->
                    Left (BootstrapDriverOpenFailed err)
                Right succeeded@(Declaration.DriverSucceeded
                        () semantic prefix _closure) ->
                    case Declaration.driverImportedModuleEvidence
                            (theoryId foundation)
                            []
                            succeeded of
                        Just evidence ->
                            Right
                                (MigrationPreludeSession
                                    input
                                    (SealedTypedModule
                                        preludeModuleName
                                        syntax
                                        semantic
                                        prefix
                                        evidence))
                        Nothing ->
                            impossible
                                "sealed bootstrap omitted import evidence"
                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 TypedModuleInput = TypedModuleInput
    !ModuleName
    !IdentifiedModuleInput
    !ModuleSyntaxInterface
    !CheckedFoundation
    !BootstrapWalkingReadiness
    ![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
    -> BootstrapWalkingReadiness
    -> 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 = freshParsedModuleSyntaxInterface (identifiedModuleParsed identified)
    expectedOwners =
        moduleName
            <$> nubOrd
                (parsedImportedAddress
                    <$> parsedModuleImports parsed)
    actualOwners = sealedTypedModuleOwner <$> direct
    expectedSyntax =
        nubOrd
            ( moduleSyntaxAssertedId
                (sealedTypedModuleSyntax prelude)
              : ( moduleSyntaxAssertedId
                    . sealedTypedModuleSyntax
                    <$> direct
                )
            )
    actualSyntax = moduleSyntaxDirectInputs syntax
    BootstrapWalkingReadiness prelude = readiness

data TypedPathError
    = TypedUnsupportedBlock !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 (TypedUnsupportedBlock location) ->
        Just location
    TypedDeclarationFailed{} ->
        Nothing
    TypedSealFailed{} ->
        Nothing

renderTypedModuleFailure :: TypedModuleFailure -> Text
renderTypedModuleFailure = \case
    TypedDeclarationFailed failure ->
        Declaration.renderDeclarationError failure
    TypedActionFailed (TypedUnsupportedBlock location) ->
        locationToText location
            <> ": this source block is not yet supported by the typed checker"
    TypedSealFailed failure ->
        renderSemanticInterfaceError failure

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

runTypedModule :: TypedModuleInput -> IO TypedModuleResult
runTypedModule
        (TypedModuleInput
            owner identified syntax foundation readiness direct resolver
            validationRun) = do
    let BootstrapWalkingReadiness prelude = readiness
        action = do
            traverse_
                (Declaration.importSealedModuleDriver
                    . sealedTypedModuleEvidence)
                effectiveDirect
            case freshParsedModuleBlocks
                    (identifiedModuleParsed identified) of
                [] -> pure ()
                block : _ ->
                    Declaration.failModuleDriver
                        (TypedUnsupportedBlock (locate block))
        semanticDirect =
            semanticInterfaceAssertedId
                (sealedTypedModuleSemantic prelude)
                : ( semanticInterfaceAssertedId
                        . sealedTypedModuleSemantic
                        <$> direct
                  )
        effectiveDirect =
            prelude : direct
    result <-
        Declaration.runModuleDriver
            foundation
            owner
            semanticDirect
            resolver
            validationRun
            action
    pure case result of
        Left err ->
            TypedModuleOpenFailed err
        Right succeeded@(Declaration.DriverSucceeded () semantic prefix _closure) ->
            case Declaration.driverImportedModuleEvidence
                    (theoryId foundation)
                    (sealedTypedModuleEvidence <$> effectiveDirect)
                    succeeded of
                Just evidence ->
                    TypedModuleSucceeded
                        (SealedTypedModule
                            owner
                            syntax
                            semantic
                            prefix
                            evidence)
                Nothing ->
                    impossible
                        "sealed typed module omitted import evidence"
        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