diff options
Diffstat (limited to 'source/Checking/Module.hs')
| -rw-r--r-- | source/Checking/Module.hs | 986 |
1 files changed, 0 insertions, 986 deletions
diff --git a/source/Checking/Module.hs b/source/Checking/Module.hs deleted file mode 100644 index d0e1d52..0000000 --- a/source/Checking/Module.hs +++ /dev/null @@ -1,986 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} -{-# LANGUAGE RankNTypes #-} - --- | Explicit inputs and sealed outputs for the typed module driver. -module 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 Checking.Declaration qualified as Declaration -import Checking.Exact qualified as Exact -import Checking.Exact.Datatype qualified as ExactDatatype -import Checking.Exact.Inductive qualified as ExactInductive -import Checking.Exact.Proof qualified as ExactProof -import Checking.FinalPrelude qualified as FinalPrelude -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 Felix.Store qualified as Store -import Report.Location -import Syntax.Interface -import 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 |