diff options
Diffstat (limited to 'source/Checking/FinalPrelude.hs')
| -rw-r--r-- | source/Checking/FinalPrelude.hs | 170 |
1 files changed, 146 insertions, 24 deletions
diff --git a/source/Checking/FinalPrelude.hs b/source/Checking/FinalPrelude.hs index 1e05199..ac2a941 100644 --- a/source/Checking/FinalPrelude.hs +++ b/source/Checking/FinalPrelude.hs @@ -9,12 +9,15 @@ module Checking.FinalPrelude , finalPreludeSemantic , finalPreludePrefix , finalPreludeObjects + , PreludePublicRole(..) + , expectedFinalPreludePublicRoles , FinalPreludeRoleTarget(..) , finalPreludePublicRole , FinalPreludeValidationError(..) , FinalPreludeFailure(..) , FinalPreludeBuildResult(..) , buildFinalPreludeCandidate + , buildParsedFinalPreludeCandidate ) where import Base hiding (Empty) @@ -28,17 +31,19 @@ import Checking.Identity import Checking.Semantic import Checking.Semantic qualified as Semantic import Felix.Module -import Felix.Migration qualified as Migration import Felix.Parse import Felix.Prelude qualified as Prelude import Felix.Source (ImportRef) import Report.Location import Syntax.Abstract qualified as Raw import Syntax.Interface +import Syntax.Lexicon qualified as Lexicon import Control.Monad (unless) +import Data.Bifunctor (first) import Data.List qualified as List import Data.Map.Strict qualified as Map +import Data.Set qualified as Set data FinalPreludeCandidate = FinalPreludeCandidate @@ -47,7 +52,7 @@ data FinalPreludeCandidate = FinalPreludeCandidate !SemanticInterface !Declaration.PendingModulePrefix !CheckedObjectClosure - !(Map.Map Migration.PreludePublicRole FinalPreludeRoleTarget) + !(Map.Map PreludePublicRole FinalPreludeRoleTarget) finalPreludeParsed :: FinalPreludeCandidate @@ -94,9 +99,23 @@ data FinalPreludeRoleTarget | FinalPreludeTheoremRole !TheoremRef deriving stock (Show, Eq, Ord) +-- | Stable public roles exported by the packaged final prelude. +data PreludePublicRole + = PreludeInfinityTheorem + | PreludeOmegaObject + | PreludeOmegaDefiningEquation + | PreludeNaturalsAlias + | PreludeNaturalsInductiveTheorem + | PreludeNaturalsMinimalTheorem + deriving stock (Show, Eq, Ord, Enum, Bounded) + +expectedFinalPreludePublicRoles :: Set PreludePublicRole +expectedFinalPreludePublicRoles = + Set.fromList [minBound .. maxBound] + finalPreludePublicRole :: FinalPreludeCandidate - -> Migration.PreludePublicRole + -> PreludePublicRole -> Maybe FinalPreludeRoleTarget finalPreludePublicRole (FinalPreludeCandidate _parsed _syntax _semantic _prefix _objects @@ -115,7 +134,8 @@ data FinalPreludeValidationError | FinalPreludeFactContentMismatch !Text | FinalPreludeValidationInventoryMismatch !DeclarationSlot | FinalPreludeAuthorityMismatch !DeclarationSlot - | FinalPreludePublicRoleMismatch !Migration.PreludePublicRole + | FinalPreludeBaseStructureMismatch + | FinalPreludePublicRoleMismatch !PreludePublicRole deriving stock (Show, Eq) data FinalPreludeFailure @@ -157,7 +177,9 @@ buildFinalPreludeCandidate foundation resolver = buildParsedFinalPreludeCandidate foundation parsed resolver --- The packaged loader above is the only entry to final-candidate construction. +-- The production acquisition path establishes packaged provenance before +-- passing its already parsed source here. The explicit parsed seam avoids a +-- second load and parse on a cache miss. buildParsedFinalPreludeCandidate :: CheckedFoundation -> Prelude.ReservedParsedPrelude @@ -225,7 +247,7 @@ buildParsedFinalPreludeCandidate foundation parsed resolver = [] compileBlocks _blockIndex [] = - pure () + commitBaseStructure compileBlocks blockIndex (block : remaining) = case block of Raw.BlockClaim{} -> @@ -249,6 +271,39 @@ buildParsedFinalPreludeCandidate foundation parsed resolver = Declaration.failModuleDriver (FinalPreludeUnsupportedBlock (locate block)) + commitBaseStructure = do + slot <- Declaration.nextDeclarationSlotDriver + theory <- Declaration.currentTheoryDriver + let seed = + opaqueDeclarationSeed + (declarationSlotModule slot) + (declarationSlotOrdinal slot) + StructureDeclaration + (generatedObjectSlot 0) + coreType = TyArrow TySet TySet + content = OpaqueObjectContent theory seed coreType + identity = opaqueObjectId theory seed coreType + asserted = assertedObject identity content + structurePhrase = + semanticStructurePhrase Lexicon._Onesorted + operation = + semanticStructureOperation Raw.CarrierSymbol identity + descriptor <- + either + (Declaration.failModuleDriver + . FinalPreludeDeclarationFailed + . Declaration.DeclarationEnvironmentFailed) + pure + (semanticStructureDescriptor + structurePhrase Nothing [] [operation]) + void + (Declaration.commitCompiledDeclaration + (declarationSyntaxId + "felix-final-prelude-base-structure-v1") do + Declaration.addDeclarationObject asserted + Declaration.stageSemanticStructureDescriptor descriptor + Declaration.authorizeCompiledDeclaration (pure ())) + compileBinding blockIndex block = do prepared <- Exact.prepareExactDeclaration @@ -312,10 +367,12 @@ validateFinalPrelude -> CheckedObjectClosure -> Either FinalPreludeValidationError - (Map.Map Migration.PreludePublicRole FinalPreludeRoleTarget) + (Map.Map PreludePublicRole FinalPreludeRoleTarget) validateFinalPrelude foundation parsed semantic prefix objects = do - declarations <- associatePreludeDeclarations parsed prefix - validateConfinedAuthority foundation semantic objects declarations + (declarations, baseStructure) <- + associatePreludeDeclarations parsed prefix + validateConfinedAuthority + foundation semantic objects declarations baseStructure resolveAndValidatePublicRoles foundation objects declarations resolveAndValidatePublicRoles @@ -324,7 +381,7 @@ resolveAndValidatePublicRoles -> [PreludeDeclaration] -> Either FinalPreludeValidationError - (Map.Map Migration.PreludePublicRole FinalPreludeRoleTarget) + (Map.Map PreludePublicRole FinalPreludeRoleTarget) resolveAndValidatePublicRoles foundation objects declarations = do successor <- expectDefinition @@ -403,30 +460,30 @@ resolveAndValidatePublicRoles foundation objects declarations = do minimalOmega let roles = Map.fromList - [ ( Migration.PreludeInfinityTheorem + [ ( PreludeInfinityTheorem , FinalPreludeTheoremRole infinity ) - , ( Migration.PreludeOmegaObject + , ( PreludeOmegaObject , FinalPreludeObjectRole omegaId ) - , ( Migration.PreludeOmegaDefiningEquation + , ( PreludeOmegaDefiningEquation , FinalPreludeTheoremRole omegaEquation ) - , ( Migration.PreludeNaturalsAlias + , ( PreludeNaturalsAlias , FinalPreludeObjectRole omegaId ) - , ( Migration.PreludeNaturalsInductiveTheorem + , ( PreludeNaturalsInductiveTheorem , FinalPreludeTheoremRole naturalsInductive ) - , ( Migration.PreludeNaturalsMinimalTheorem + , ( PreludeNaturalsMinimalTheorem , FinalPreludeTheoremRole naturalsMinimal ) ] unless - (Map.keysSet roles == Migration.expectedFinalPreludePublicRoles) + (Map.keysSet roles == expectedFinalPreludePublicRoles) (Left (FinalPreludePublicRoleMismatch - Migration.PreludeInfinityTheorem)) + PreludeInfinityTheorem)) pure roles validatePackagedPreludeInput @@ -460,12 +517,19 @@ validatePackagedPreludeInput parsed syntax associatePreludeDeclarations :: Prelude.ReservedParsedPrelude -> Declaration.PendingModulePrefix - -> Either FinalPreludeValidationError [PreludeDeclaration] + -> Either + FinalPreludeValidationError + ([PreludeDeclaration], Declaration.CommittedDeclarationBatch) associatePreludeDeclarations parsed prefix = do - unless - (length sourceDeclarations == length batches) - (Left FinalPreludeDeclarationAssociationMismatch) - pure (zipWith PreludeDeclaration sourceDeclarations batches) + case List.splitAt (length sourceDeclarations) batches of + (sourceBatches, [baseStructure]) + | length sourceBatches == length sourceDeclarations -> + pure + ( zipWith PreludeDeclaration + sourceDeclarations sourceBatches + , baseStructure + ) + _ -> Left FinalPreludeDeclarationAssociationMismatch where sourceDeclarations = [ block @@ -483,8 +547,10 @@ validateConfinedAuthority -> SemanticInterface -> CheckedObjectClosure -> [PreludeDeclaration] + -> Declaration.CommittedDeclarationBatch -> Either FinalPreludeValidationError () -validateConfinedAuthority foundation semantic objects declarations = do +validateConfinedAuthority + foundation semantic objects declarations baseStructure = do unless ( semanticInterfaceOwner semantic == preludeModuleName && null (semanticInterfaceDirectInputs semantic) @@ -499,12 +565,68 @@ validateConfinedAuthority foundation semantic objects declarations = do (declarationBatch declaration)) ] traverse_ (validateDeclarationAuthority foundation objects) declarations + validateBaseStructure foundation objects baseStructure where requireTransparent identity = case lookupCheckedObjectContent identity objects of Just TransparentObjectContent{} -> pure () _ -> Left (FinalPreludeUnexpectedObject identity) +validateBaseStructure + :: CheckedFoundation + -> CheckedObjectClosure + -> Declaration.CommittedDeclarationBatch + -> Either FinalPreludeValidationError () +validateBaseStructure foundation objects batch = do + let slot = Declaration.committedBatchSlot batch + delta = Declaration.committedBatchDelta batch + environment = declarationDeltaEnvironment delta + structurePhrase = semanticStructurePhrase Lexicon._Onesorted + expectedSeed = + opaqueDeclarationSeed + (declarationSlotModule slot) + (declarationSlotOrdinal slot) + StructureDeclaration + (generatedObjectSlot 0) + expectedType = TyArrow TySet TySet + expectedObject = opaqueObjectId (theoryId foundation) expectedSeed expectedType + expectedContent = + OpaqueObjectContent + (theoryId foundation) + expectedSeed + expectedType + descriptor <- + case semanticEnvironmentStructures environment of + [single] -> Right single + _ -> Left FinalPreludeBaseStructureMismatch + expectedDescriptor <- + first (const FinalPreludeBaseStructureMismatch) + (semanticStructureDescriptor + structurePhrase + Nothing + [] + [semanticStructureOperation Raw.CarrierSymbol expectedObject]) + unless + ( declarationSlotModule slot == preludeModuleName + && descriptor == expectedDescriptor + && null (semanticEnvironmentBindings environment) + && declarationDeltaObjects delta == [expectedObject] + && null (declarationDeltaFacts delta) + && null (declarationDeltaAliases delta) + && null (declarationDeltaPropositions delta) + && Declaration.committedBatchObjects batch + == [assertedObject expectedObject expectedContent] + && null (Declaration.committedBatchPropositions batch) + && null (Declaration.committedBatchProofValidations batch) + && maybe + False + (null . declarationValidationRecordCertificates) + (Declaration.committedBatchDeclarationValidation batch) + && lookupCheckedObjectContent expectedObject objects + == Just expectedContent + ) + (Left FinalPreludeBaseStructureMismatch) + validateDeclarationAuthority :: CheckedFoundation -> CheckedObjectClosure |