diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2026-08-01 13:01:18 +0200 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2026-08-01 13:01:18 +0200 |
| commit | eb1366d6276ebd2bc7f51e5a7cfdcab69746bde4 (patch) | |
| tree | 9746afc9db790c04259aef132e4b4a991b4d9bd6 /source/Checking/Module.hs | |
| parent | 05c64829d25464d83cde8fca31daf98f557d199f (diff) | |
Fold transitive sealed imports
Diffstat (limited to 'source/Checking/Module.hs')
| -rw-r--r-- | source/Checking/Module.hs | 28 |
1 files changed, 21 insertions, 7 deletions
diff --git a/source/Checking/Module.hs b/source/Checking/Module.hs index ac7070f..de292c4 100644 --- a/source/Checking/Module.hs +++ b/source/Checking/Module.hs @@ -24,6 +24,7 @@ module Checking.Module , migrationPreludeModule , BootstrapWalkingReadiness , bootstrapWalkingReadiness + , bootstrapWalkingReadinessFromSealed , BootstrapCompilerReadiness , bootstrapCompilerReadiness , BootstrapError(..) @@ -167,10 +168,12 @@ cachedSealedTypedModule -> ModuleName -> ModuleSyntaxInterface -> SemanticInterface + -> [SealedTypedModule] -> [AssertedObject] -> [CheckedPropositionContent] -> Either CachedTypedModuleError SealedTypedModule -cachedSealedTypedModule foundation owner syntax semantic objects propositions = do +cachedSealedTypedModule + foundation owner syntax semantic parents objects propositions = do unless (semanticInterfaceOwner semantic == owner) (Left @@ -189,6 +192,7 @@ cachedSealedTypedModule foundation owner syntax semantic objects propositions = Right (Declaration.validatedImportedModuleEvidence (theoryId foundation) + (sealedTypedModuleEvidence <$> parents) semantic objects propositions) @@ -219,12 +223,20 @@ migrationPreludeModule (MigrationPreludeSession _input sealed) = -- These fixture-only seams are discarded with the final-prelude cutover. newtype BootstrapWalkingReadiness = BootstrapWalkingReadiness - MigrationPreludeSession + 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 @@ -274,6 +286,7 @@ buildBootstrapPreludeSession foundation resolver = do () semantic prefix _closure) -> case Declaration.driverImportedModuleEvidence (theoryId foundation) + [] succeeded of Just evidence -> Right @@ -370,8 +383,7 @@ typedModuleInput expectedSyntax = nubOrd ( moduleSyntaxAssertedId - (sealedTypedModuleSyntax - (migrationPreludeModule prelude)) + (sealedTypedModuleSyntax prelude) : ( moduleSyntaxAssertedId . sealedTypedModuleSyntax <$> direct @@ -426,7 +438,7 @@ runTypedModule traverse_ (Declaration.importSealedModuleDriver . sealedTypedModuleEvidence) - direct + effectiveDirect case freshParsedModuleBlocks (identifiedModuleParsed identified) of [] -> pure () @@ -435,12 +447,13 @@ runTypedModule (TypedUnsupportedBlock (locate block)) semanticDirect = semanticInterfaceAssertedId - (sealedTypedModuleSemantic - (migrationPreludeModule prelude)) + (sealedTypedModuleSemantic prelude) : ( semanticInterfaceAssertedId . sealedTypedModuleSemantic <$> direct ) + effectiveDirect = + prelude : direct result <- Declaration.runModuleDriver foundation @@ -455,6 +468,7 @@ runTypedModule Right succeeded@(Declaration.DriverSucceeded () semantic prefix _closure) -> case Declaration.driverImportedModuleEvidence (theoryId foundation) + (sealedTypedModuleEvidence <$> effectiveDirect) succeeded of Just evidence -> TypedModuleSucceeded |