diff options
Diffstat (limited to 'source/Felix/Checking/Module.hs')
| -rw-r--r-- | source/Felix/Checking/Module.hs | 986 |
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 |