diff options
Diffstat (limited to 'source/Checking/Module.hs')
| -rw-r--r-- | source/Checking/Module.hs | 375 |
1 files changed, 267 insertions, 108 deletions
diff --git a/source/Checking/Module.hs b/source/Checking/Module.hs index ad2fb27..bb35277 100644 --- a/source/Checking/Module.hs +++ b/source/Checking/Module.hs @@ -10,6 +10,11 @@ module Checking.Module , identifiedModuleOwner , identifiedModuleBinding , identifiedModuleParsed + , TypedSourceDeclaration + , typedSourceDeclarationBlockIndex + , typedSourceDeclarationHead + , typedSourceDeclarationProof + , typedSourceDeclarations , SealedTypedModule , sealedTypedModuleOwner , sealedTypedModuleSyntax @@ -19,9 +24,12 @@ module Checking.Module , renderCachedTypedModuleError , cachedSealedTypedModule , sealedTypedModulePrefix - , MigrationPreludeSession - , migrationPreludeInput - , migrationPreludeModule + , FinalPreludeSession + , ModuleRootAcquisition(..) + , finalPreludeSource + , finalPreludeInput + , finalPreludeModule + , finalPreludeAcquisition , FinalPreludeReadiness , finalPreludeReadiness , BootstrapPreludeFixture @@ -32,7 +40,7 @@ module Checking.Module , BootstrapError(..) , buildBootstrapPreludeFixture , FinalPreludeReadinessError(..) - , buildFinalPreludeSession + , acquireFinalPreludeSession , TypedModuleInput , TypedModuleInputError(..) , renderTypedModuleInputError @@ -118,6 +126,75 @@ identifiedModuleParsed 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 @@ -197,55 +274,79 @@ cachedSealedTypedModule propositions = Store.cachedInstallationPropositions installation -data MigrationPreludeSession = MigrationPreludeSession +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 -migrationPreludeInput - :: MigrationPreludeSession +finalPreludeInput + :: FinalPreludeSession -> IdentifiedModuleInput -migrationPreludeInput (MigrationPreludeSession input _module) = +finalPreludeInput (FinalPreludeSession _source input _module _acquisition) = input -migrationPreludeModule - :: MigrationPreludeSession +finalPreludeModule + :: FinalPreludeSession -> SealedTypedModule -migrationPreludeModule (MigrationPreludeSession _input sealed) = +finalPreludeModule (FinalPreludeSession _source _input sealed _acquisition) = sealed +finalPreludeAcquisition + :: FinalPreludeSession + -> ModuleRootAcquisition +finalPreludeAcquisition + (FinalPreludeSession _source _input _sealed acquisition) = + acquisition + newtype FinalPreludeReadiness = FinalPreludeReadiness SealedTypedModule finalPreludeReadiness - :: MigrationPreludeSession + :: FinalPreludeSession -> FinalPreludeReadiness finalPreludeReadiness = - FinalPreludeReadiness . migrationPreludeModule + FinalPreludeReadiness . finalPreludeModule +-- | Test-only empty-prelude fixture. +-- +-- It is exported for focused exact-compiler tests. Production acquisition is +-- exclusively 'acquireFinalPreludeSession'. newtype BootstrapPreludeFixture = BootstrapPreludeFixture - MigrationPreludeSession + FinalPreludeSession bootstrapPreludeInput :: BootstrapPreludeFixture -> IdentifiedModuleInput bootstrapPreludeInput (BootstrapPreludeFixture fixture) = - migrationPreludeInput fixture + finalPreludeInput fixture bootstrapPreludeModule :: BootstrapPreludeFixture -> SealedTypedModule bootstrapPreludeModule (BootstrapPreludeFixture fixture) = - migrationPreludeModule fixture + finalPreludeModule fixture --- | Fixture seam for the empty bootstrap compiler input. +-- | Test-only seam for the empty bootstrap compiler input. bootstrapPreludeReadiness :: BootstrapPreludeFixture -> FinalPreludeReadiness bootstrapPreludeReadiness = FinalPreludeReadiness . bootstrapPreludeModule --- | Fixture seam for exercising a nonempty distinguished prelude before the --- final source prelude is constructed. +-- | Test-only seam for exercising a synthetic distinguished prelude. fixtureFinalPreludeReadinessFromSealed :: SealedTypedModule -> FinalPreludeReadiness @@ -259,7 +360,7 @@ data BootstrapError | BootstrapSealFailed !SemanticInterfaceError deriving stock (Show) --- | Construct the empty distinguished prelude used by compiler fixtures. +-- | Construct the empty distinguished prelude used only by compiler fixtures. buildBootstrapPreludeFixture :: CheckedFoundation -> Declaration.VampireResolver @@ -291,7 +392,8 @@ buildBootstrapPreludeFixture foundation resolver = do () semantic prefix _closure) -> Right (BootstrapPreludeFixture - (MigrationPreludeSession + (FinalPreludeSession + Prelude.emptyBootstrapSourceInput input (SealedTypedModule preludeModuleName @@ -301,7 +403,8 @@ buildBootstrapPreludeFixture foundation resolver = do (Declaration.freshImportedModuleEvidence [] semantic - prefix)))) + prefix)) + ModuleRootMiss)) Right (Declaration.DriverFailed (Declaration.DriverDeclarationFailed err) @@ -321,34 +424,35 @@ data FinalPreludeReadinessError | FinalPreludeReadinessBuildOpenFailed !Declaration.DriverOpenError | FinalPreludeReadinessArtifactKeyFailed !ModuleArtifactKeyError | FinalPreludeReadinessStoreFailed !Store.StoreFailure + | FinalPreludeReadinessCachedModuleFailed !CachedTypedModuleError | FinalPreludeReadinessAcknowledgementMismatch !ModuleArtifactResult !ModuleArtifactResult deriving stock (Show) --- | Build and atomically publish the exact packaged final prelude. +-- | Acquire the exact packaged final prelude through its ordinary module root. -- --- A session is returned only after the ordinary module root transaction has --- acknowledged the exact artifact that was requested. -buildFinalPreludeSession - :: Store.Store +-- 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 MigrationPreludeSession) -buildFinalPreludeSession store foundation resolver = - FinalPrelude.buildFinalPreludeCandidate foundation resolver >>= \case - FinalPrelude.FinalPreludeSourceLoadFailed failure -> + -> IO (Either FinalPreludeReadinessError FinalPreludeSession) +acquireFinalPreludeSession memo store foundation resolver = + Prelude.loadReservedPreludeSourceInput >>= \case + Left failure -> pure (Left (FinalPreludeReadinessSourceLoadFailed failure)) - FinalPrelude.FinalPreludeSourceParseFailed failure -> - pure (Left (FinalPreludeReadinessSourceParseFailed failure)) - FinalPrelude.FinalPreludeBuildFailed failure _prefix -> - pure (Left (FinalPreludeReadinessBuildFailed failure)) - FinalPrelude.FinalPreludeBuildOpenFailed failure -> - pure (Left (FinalPreludeReadinessBuildOpenFailed failure)) - FinalPrelude.FinalPreludeBuilt candidate -> - install candidate + Right source -> + Prelude.parseReservedPreludeSource source >>= \case + Left failure -> + pure (Left (FinalPreludeReadinessSourceParseFailed failure)) + Right parsed -> + acquire source parsed where - install candidate = + acquire source parsed = case moduleArtifactKey preludeModuleName parsedId @@ -357,47 +461,83 @@ buildFinalPreludeSession store foundation resolver = Left failure -> pure (Left (FinalPreludeReadinessArtifactKeyFailed failure)) Right key -> do - let artifact = - moduleArtifactResult - key - (moduleSyntaxAssertedId syntax) - (semanticInterfaceAssertedId semantic) - Store.writeSealedModule - store - prefix - [syntax] - [semantic] - artifact >>= \case + Store.loadCachedModuleInstallation + memo store key (moduleSyntaxAssertedId syntax) >>= \case Left failure -> pure (Left (FinalPreludeReadinessStoreFailed failure)) - Right acknowledged - | acknowledged /= artifact -> - pure - (Left - (FinalPreludeReadinessAcknowledgementMismatch - artifact - acknowledged)) - | otherwise -> + Right (Just installation) -> + pure do + sealed <- first FinalPreludeReadinessCachedModuleFailed + (cachedSealedTypedModule + foundation [] installation) pure - (Right - (MigrationPreludeSession - identified - (SealedTypedModule - preludeModuleName - syntax - semantic - prefix - (Declaration.freshImportedModuleEvidence - [] - semantic - prefix)))) + (FinalPreludeSession + source + identified sealed ModuleRootHit) + Right Nothing -> + build source parsed key where - parsed = FinalPrelude.finalPreludeParsed candidate identified = identifiedReservedPrelude parsed parsedId = identifiedParsedModuleId (identifiedModuleParsed identified) - syntax = FinalPrelude.finalPreludeSyntax candidate - semantic = FinalPrelude.finalPreludeSemantic candidate - prefix = FinalPrelude.finalPreludePrefix candidate + 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 @@ -552,10 +692,10 @@ runTypedModule (Declaration.importSealedModuleDriver . sealedTypedModuleEvidence) effectiveDirect - compileBlocks - 0 - (identifiedParsedModuleBlocks - (identifiedModuleParsed identified)) + compileSourceItems + (typedSourceItems + (identifiedParsedModuleBlocks + (identifiedModuleParsed identified))) semanticDirect = semanticInterfaceAssertedId (sealedTypedModuleSemantic prelude) @@ -568,43 +708,45 @@ runTypedModule occurrences = identifiedParsedModuleSyntaxOccurrences (identifiedModuleParsed identified) - compileBlocks _blockIndex [] = + compileSourceItems [] = pure () - compileBlocks blockIndex (block : remaining) = - case block of - Raw.BlockClaim{} -> - case remaining of - Raw.BlockProof _ proof _end : rest -> do - compileClaim block (Just proof) - compileBlocks (blockIndex + 2) rest - _ -> do - compileClaim block Nothing - compileBlocks (blockIndex + 1) remaining - Raw.BlockProof location _proof _end -> + compileSourceItems (item : remaining) = + case item of + TypedUnmatchedSourceProof location -> Declaration.failModuleDriver (TypedUnmatchedProof location) - Raw.BlockSig{} -> do + TypedSourceDeclarationItem declaration -> do + compileDeclaration declaration + compileSourceItems remaining + + compileDeclaration sourceDeclaration = + case block of + Raw.BlockClaim{} -> + compileClaim block explicitProof + Raw.BlockProof{} -> + impossible + "typed declaration association retained a proof head" + Raw.BlockSig{} -> compileSelected block - compileBlocks (blockIndex + 1) remaining - Raw.BlockAbbr{} -> do + Raw.BlockAbbr{} -> compileSelected block - compileBlocks (blockIndex + 1) remaining - Raw.BlockDefn{} -> do + Raw.BlockDefn{} -> compileSelected block - compileBlocks (blockIndex + 1) remaining - Raw.BlockAxiom{} -> do + Raw.BlockAxiom{} -> compileSourceAxiom block - compileBlocks (blockIndex + 1) remaining - Raw.BlockInductive{} -> do + Raw.BlockInductive{} -> compileInductive block - compileBlocks (blockIndex + 1) remaining - Raw.BlockData{} -> do + Raw.BlockData{} -> compileDatatype block - compileBlocks (blockIndex + 1) remaining - _ -> - Declaration.failModuleDriver - (TypedUnsupportedBlock (locate block)) + Raw.BlockStruct{} -> + compileStructure block where + blockIndex = + typedSourceDeclarationBlockIndex sourceDeclaration + block = typedSourceDeclarationHead sourceDeclaration + explicitProof = + typedSourceDeclarationProof sourceDeclaration + compileSelected selected = do prepared <- Exact.prepareExactDeclaration @@ -672,11 +814,28 @@ runTypedModule (ExactDatatype.commitPreparedExactDatatype datatype) - compileClaim selected explicitProof = do + compileStructure selected = do + prepared <- + Exact.prepareExactStructure + selected + [ parsedSyntaxOccurrenceEntry occurrence + | occurrence <- occurrences + , parsedSyntaxOccurrenceBlockIndex occurrence + == blockIndex + ] + case prepared of + Left failure -> + Declaration.failModuleDriver + (TypedExactCompileFailed failure) + Right structure -> + void + (Exact.commitPreparedExactStructure structure) + + compileClaim selected selectedProof = do prepared <- ExactProof.prepareExactProof selected - explicitProof + selectedProof case prepared of Left failure -> Declaration.failModuleDriver |