diff options
Diffstat (limited to 'source/Checking/FinalPrelude.hs')
| -rw-r--r-- | source/Checking/FinalPrelude.hs | 1081 |
1 files changed, 0 insertions, 1081 deletions
diff --git a/source/Checking/FinalPrelude.hs b/source/Checking/FinalPrelude.hs deleted file mode 100644 index 5951acc..0000000 --- a/source/Checking/FinalPrelude.hs +++ /dev/null @@ -1,1081 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} -{-# LANGUAGE RankNTypes #-} - --- | Authority-confined construction of the inert final-prelude candidate. -module Checking.FinalPrelude - ( FinalPreludeCandidate - , finalPreludeParsed - , finalPreludeSyntax - , finalPreludeSemantic - , finalPreludePrefix - , finalPreludeObjects - , PreludePublicRole(..) - , expectedFinalPreludePublicRoles - , FinalPreludeRoleTarget(..) - , finalPreludePublicRole - , FinalPreludeValidationError(..) - , FinalPreludeFailure(..) - , FinalPreludeBuildResult(..) - , buildFinalPreludeCandidate - , buildParsedFinalPreludeCandidate - ) where - -import Base hiding (Empty) -import Checking.Authority qualified as Authority -import Checking.Core -import Checking.Declaration qualified as Declaration -import Checking.Exact qualified as Exact -import Checking.Exact.Proof qualified as ExactProof -import Checking.Foundation -import Checking.Identity -import Checking.Semantic -import Checking.Semantic qualified as Semantic -import Felix.Module -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 - !Prelude.ReservedParsedPrelude - !ModuleSyntaxInterface - !SemanticInterface - !Declaration.PendingModulePrefix - !CheckedObjectClosure - !(Map.Map PreludePublicRole FinalPreludeRoleTarget) - -finalPreludeParsed - :: FinalPreludeCandidate - -> Prelude.ReservedParsedPrelude -finalPreludeParsed - (FinalPreludeCandidate parsed _syntax _semantic _prefix _objects - _roles) = - parsed - -finalPreludeSyntax - :: FinalPreludeCandidate - -> ModuleSyntaxInterface -finalPreludeSyntax - (FinalPreludeCandidate _parsed syntax _semantic _prefix _objects - _roles) = - syntax - -finalPreludeSemantic - :: FinalPreludeCandidate - -> SemanticInterface -finalPreludeSemantic - (FinalPreludeCandidate _parsed _syntax semantic _prefix _objects - _roles) = - semantic - -finalPreludePrefix - :: FinalPreludeCandidate - -> Declaration.PendingModulePrefix -finalPreludePrefix - (FinalPreludeCandidate _parsed _syntax _semantic prefix _objects - _roles) = - prefix - -finalPreludeObjects - :: FinalPreludeCandidate - -> CheckedObjectClosure -finalPreludeObjects - (FinalPreludeCandidate _parsed _syntax _semantic _prefix objects - _roles) = - objects - -data FinalPreludeRoleTarget - = FinalPreludeObjectRole !ObjectId - | 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 - -> PreludePublicRole - -> Maybe FinalPreludeRoleTarget -finalPreludePublicRole - (FinalPreludeCandidate _parsed _syntax _semantic _prefix _objects - roles) role = - Map.lookup role roles - -data FinalPreludeValidationError - = FinalPreludePackagedInputMismatch - | FinalPreludeSemanticEnvironmentMismatch - | FinalPreludeDeclarationAssociationMismatch - | FinalPreludeUnexpectedObject !ObjectId - | FinalPreludeDeclarationMissing !Text - | FinalPreludeDeclarationDuplicate !Text - | FinalPreludeDeclarationShapeMismatch !Text - | FinalPreludeDefinitionContentMismatch !Text - | FinalPreludeFactContentMismatch !Text - | FinalPreludeValidationInventoryMismatch !DeclarationSlot - | FinalPreludeAuthorityMismatch !DeclarationSlot - | FinalPreludeBaseStructureMismatch - | FinalPreludePublicRoleMismatch !PreludePublicRole - deriving stock (Show, Eq) - -data FinalPreludeFailure - = FinalPreludeWrongOwner !ModuleName - | FinalPreludeHasImports ![ImportRef] - | FinalPreludeHasSyntaxImports ![SyntaxInterfaceId] - | FinalPreludeUnsupportedBlock !Location - | FinalPreludeUnmatchedProof !Location - | FinalPreludeExactDeclarationFailed !Exact.ExactCompileError - | FinalPreludeExactProofFailed !ExactProof.ExactProofError - | FinalPreludeOmittedProof !Location - | FinalPreludeDeclarationFailed !Declaration.DeclarationError - | FinalPreludeSealFailed !SemanticInterfaceError - | FinalPreludeValidationFailed !FinalPreludeValidationError - deriving stock (Show, Eq) - -data FinalPreludeBuildResult - = FinalPreludeSourceLoadFailed !Prelude.PreludeLoadError - | FinalPreludeSourceParseFailed !Prelude.PreludeParseError - | FinalPreludeBuilt !FinalPreludeCandidate - | FinalPreludeBuildFailed - !FinalPreludeFailure - !Declaration.PendingModulePrefix - | FinalPreludeBuildOpenFailed !Declaration.DriverOpenError - -data PlannedPreludeDeclaration - = PlannedPreludeBinding - !(Declaration.PlannedDeclaration (Maybe ObjectId)) - | PlannedPreludeFoundation - !(Declaration.PlannedDeclaration - ExactProof.CheckedFinalPreludeFoundationAuthorization) - | PlannedPreludeProof - !(Declaration.PlannedDeclaration - ExactProof.CheckedExactProofAuthorization) - | PlannedPreludeBase - !(Declaration.PlannedDeclaration ()) - -data PreludePlanningFailure - = PreludePlanningAction !FinalPreludeFailure - | PreludePlanningDeclaration !Declaration.DeclarationError - -data PreludeModulePlan = PreludeModulePlan - ![PlannedPreludeDeclaration] - !(Maybe PreludePlanningFailure) - -buildFinalPreludeCandidate - :: CheckedFoundation - -> Declaration.VampireResolver - -> IO FinalPreludeBuildResult -buildFinalPreludeCandidate foundation resolver = - Prelude.loadReservedPreludeSourceInput >>= \case - Left failure -> - pure (FinalPreludeSourceLoadFailed failure) - Right source -> - Prelude.parseReservedPreludeSource source >>= \case - Left failure -> - pure (FinalPreludeSourceParseFailed failure) - Right parsed -> - buildParsedFinalPreludeCandidate - foundation parsed resolver - --- 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 - -> Declaration.VampireResolver - -> IO FinalPreludeBuildResult -buildParsedFinalPreludeCandidate foundation parsed resolver = - case validatePackagedPreludeInput parsed syntax of - Left failure -> do - case emptyPrefix of - Left prefixFailure -> - pure - (FinalPreludeBuildOpenFailed - (Declaration.DriverInitialPrefixError - prefixFailure)) - Right prefix -> - pure (FinalPreludeBuildFailed failure prefix) - Right () -> do - outcome <- - Declaration.runModuleDriver - foundation - preludeModuleName - [] - resolver - -- The confined builder never consults stored validation. - Declaration.FreshValidation - do - PreludeModulePlan declarations terminal <- - Declaration.runProspectiveLoweringDriver - (planBlocks [] 0 blocks) - traverse_ admitPreludeDeclaration declarations - traverse_ failPreludePlanning terminal - pure case outcome of - Left failure -> - FinalPreludeBuildOpenFailed failure - Right (Declaration.DriverFailed failure prefix) -> - FinalPreludeBuildFailed - (case failure of - Declaration.DriverDeclarationFailed err -> - FinalPreludeDeclarationFailed err - Declaration.DriverActionFailed err -> - err) - prefix - Right (Declaration.DriverSealFailed failure prefix) -> - FinalPreludeBuildFailed - (FinalPreludeSealFailed failure) - prefix - Right (Declaration.DriverSucceeded - () semantic prefix objects) -> - case validateFinalPrelude - foundation parsed semantic prefix objects of - Left failure -> - FinalPreludeBuildFailed - (FinalPreludeValidationFailed failure) - prefix - Right roles -> - FinalPreludeBuilt - (FinalPreludeCandidate - parsed syntax semantic prefix objects roles) - where - identified = Prelude.reservedParsedPreludeModule parsed - blocks = identifiedParsedModuleBlocks identified - occurrences = identifiedParsedModuleSyntaxOccurrences identified - syntax = identifiedParsedModuleSyntaxInterface identified - - emptyPrefix = - Declaration.emptyPendingModulePrefix - <$> initialPrefixContextId - (theoryId foundation) - preludeModuleName - [] - - planBlocks completed _blockIndex [] = do - planBaseStructure >>= \case - Left failure -> - pure - (PreludeModulePlan - (reverse completed) - (Just failure)) - Right base -> - pure - (PreludeModulePlan - (reverse (base : completed)) - Nothing) - planBlocks completed blockIndex (block : remaining) = - case block of - Raw.BlockClaim{} -> - case remaining of - Raw.BlockProof _location proof _end : rest -> do - continue completed (blockIndex + 2) rest - =<< planOrdinaryProof block (Just proof) - _ -> do - continue completed (blockIndex + 1) remaining - =<< planImplicitClaim block - Raw.BlockProof location _proof _end -> - pure - (PreludeModulePlan - (reverse completed) - (Just - (PreludePlanningAction - (FinalPreludeUnmatchedProof location)))) - Raw.BlockAbbr{} -> do - continue completed (blockIndex + 1) remaining - =<< planBinding blockIndex block - Raw.BlockDefn{} -> do - continue completed (blockIndex + 1) remaining - =<< planBinding blockIndex block - _ -> - pure - (PreludeModulePlan - (reverse completed) - (Just - (PreludePlanningAction - (FinalPreludeUnsupportedBlock - (locate block))))) - where - continue accumulated nextIndex rest = \case - Left failure -> - pure - (PreludeModulePlan - (reverse accumulated) - (Just failure)) - Right declaration -> - planBlocks (declaration : accumulated) nextIndex rest - - planBaseStructure = do - slot <- Declaration.nextDeclarationSlotLowering - theory <- Declaration.currentTheoryLowering - 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 - (pure - . Left - . PreludePlanningDeclaration - . Declaration.DeclarationEnvironmentFailed) - (pure . Right) - (semanticStructureDescriptor - structurePhrase Nothing [] [operation]) - case descriptor of - Left failure -> pure (Left failure) - Right checkedDescriptor -> - planPreludeChecked PlannedPreludeBase - (Declaration.checkedCompiledDeclaration - (declarationSyntaxId - "felix-final-prelude-base-structure-v1") - [asserted] [] [] [checkedDescriptor] [] ()) - - planBinding blockIndex block = do - prepared <- - Exact.prepareExactDeclaration - block - [ parsedSyntaxOccurrenceEntry occurrence - | occurrence <- occurrences - , parsedSyntaxOccurrenceBlockIndex occurrence == blockIndex - ] - case prepared of - Left failure -> - pure - (Left - (PreludePlanningAction - (FinalPreludeExactDeclarationFailed failure))) - Right declaration -> do - Exact.lowerPreparedExactBinding declaration >>= \case - Left failure -> planningDeclarationFailure failure - Right checked -> - planPreludeChecked PlannedPreludeBinding checked - - planImplicitClaim block = do - foundationClaim <- - ExactProof.prepareFinalPreludeFoundationClaim - foundation block Nothing - case foundationClaim of - Right claim -> do - ExactProof.lowerPreparedFinalPreludeFoundationClaim claim - >>= \case - Left failure -> planningDeclarationFailure failure - Right checked -> - planPreludeChecked PlannedPreludeFoundation checked - Left ExactProof.ExactProofFoundationLeafTargetMismatch{} -> - planOrdinaryProof block Nothing - Left ExactProof.ExactProofFoundationLeafRequiresImplicitAuto{} -> - planOrdinaryProof block Nothing - Left failure -> - pure - (Left - (PreludePlanningAction - (FinalPreludeExactProofFailed failure))) - - planOrdinaryProof block explicitProof = do - prepared <- - ExactProof.prepareExactProof block explicitProof - case prepared of - Left failure -> - pure - (Left - (PreludePlanningAction - (FinalPreludeExactProofFailed failure))) - Right proof - | Just location <- - ExactProof.preparedExactProofFirstOmission proof -> - pure - (Left - (PreludePlanningAction - (FinalPreludeOmittedProof location))) - | otherwise -> - ExactProof.lowerPreparedExactProof proof >>= \case - Left failure -> planningDeclarationFailure failure - Right checked -> - planPreludeChecked PlannedPreludeProof checked - - planPreludeChecked - :: forall body. - (Declaration.PlannedDeclaration body - -> PlannedPreludeDeclaration) - -> Declaration.CheckedDeclaration body - -> Declaration.LoweringDriver - (Either PreludePlanningFailure PlannedPreludeDeclaration) - planPreludeChecked constructor checked = - Declaration.planCheckedDeclaration checked >>= \case - Left failure -> planningDeclarationFailure failure - Right planned -> pure (Right (constructor planned)) - - planningDeclarationFailure = - pure . Left . PreludePlanningDeclaration - - admitPreludeDeclaration = \case - PlannedPreludeBinding planned -> - void - (Declaration.admitPlannedCheckedDeclaration - planned Exact.authorizeCheckedExactBinding) - PlannedPreludeFoundation planned -> - void - (Declaration.admitPlannedCheckedDeclaration planned - ExactProof.authorizeCheckedFinalPreludeFoundationClaim) - PlannedPreludeProof planned -> - void - (Declaration.admitPlannedCheckedDeclaration - planned ExactProof.authorizeCheckedExactProof) - PlannedPreludeBase planned -> - void - (Declaration.admitPlannedCheckedDeclaration planned - (\() stages -> - unless - (null stages) - (Declaration.failDeclaration - (Declaration.CheckedAuthorizationCandidateShapeMismatch - 0 (length stages))))) - - failPreludePlanning = \case - PreludePlanningAction failure -> - Declaration.failModuleDriver failure - PreludePlanningDeclaration failure -> - Declaration.failDeclarationDriver failure - -data PreludeDeclaration = PreludeDeclaration - !Raw.Block - !Declaration.CommittedDeclarationBatch - -data PreludeDefinitionKind - = PreludeDefinition - | PreludeAbbreviation - -data PreludeDefinitionView = PreludeDefinitionView - !ObjectId - !SemanticGlobalTarget - -validateFinalPrelude - :: CheckedFoundation - -> Prelude.ReservedParsedPrelude - -> SemanticInterface - -> Declaration.PendingModulePrefix - -> CheckedObjectClosure - -> Either - FinalPreludeValidationError - (Map.Map PreludePublicRole FinalPreludeRoleTarget) -validateFinalPrelude foundation parsed semantic prefix objects = do - (declarations, baseStructure) <- - associatePreludeDeclarations parsed prefix - validateConfinedAuthority - foundation semantic objects declarations baseStructure - resolveAndValidatePublicRoles foundation objects declarations - -resolveAndValidatePublicRoles - :: CheckedFoundation - -> CheckedObjectClosure - -> [PreludeDeclaration] - -> Either - FinalPreludeValidationError - (Map.Map PreludePublicRole FinalPreludeRoleTarget) -resolveAndValidatePublicRoles foundation objects declarations = do - successor <- - expectDefinition - foundation objects declarations - "prelude_successor" - PreludeDefinition - (TyArrow TySet TySet) - expectedSuccessorBody - let successorId = definitionViewObject successor - - inductive <- - expectDefinition - foundation objects declarations - "prelude_inductive" - PreludeDefinition - (TyArrow TySet TyProp) - (expectedInductiveBody successorId) - let inductiveId = definitionViewObject inductive - - u0 <- - expectDefinition - foundation objects declarations - "prelude_u0" - PreludeDefinition - TySet - (applyIntrinsic UnivOf (CIntrinsic Empty)) - let u0Id = definitionViewObject u0 - - let omegaBody = expectedOmegaBody u0Id inductiveId - omega <- - expectDefinition - foundation objects declarations - "prelude_omega" - PreludeDefinition - TySet - omegaBody - let omegaId = definitionViewObject omega - - naturals <- - expectDefinition - foundation objects declarations - "prelude_naturals" - PreludeAbbreviation - TySet - (CGlobal omegaId) - case definitionViewTarget naturals of - TransparentExpansion{} -> pure () - _ -> - Left - (FinalPreludeDefinitionContentMismatch - "prelude_naturals") - - (infinity, infinityTarget) <- - expectClaim declarations "prelude_infinity" - validateInfinityTarget objects inductiveId infinityTarget - omegaEquation <- - fst - <$> expectFactTarget - declarations - "prelude_omega" - (CEq TySet (CGlobal omegaId) omegaBody) - let inductiveOmega = - CApp (CGlobal inductiveId) (CGlobal omegaId) - minimalOmega = expectedMinimality inductiveId omegaId - naturalsInductive <- - fst - <$> expectClaimTarget - declarations - "prelude_naturals_inductive" - inductiveOmega - naturalsMinimal <- - fst - <$> expectClaimTarget - declarations - "prelude_naturals_minimal" - minimalOmega - - let roles = Map.fromList - [ ( PreludeInfinityTheorem - , FinalPreludeTheoremRole infinity - ) - , ( PreludeOmegaObject - , FinalPreludeObjectRole omegaId - ) - , ( PreludeOmegaDefiningEquation - , FinalPreludeTheoremRole omegaEquation - ) - , ( PreludeNaturalsAlias - , FinalPreludeObjectRole omegaId - ) - , ( PreludeNaturalsInductiveTheorem - , FinalPreludeTheoremRole naturalsInductive - ) - , ( PreludeNaturalsMinimalTheorem - , FinalPreludeTheoremRole naturalsMinimal - ) - ] - unless - (Map.keysSet roles == expectedFinalPreludePublicRoles) - (Left - (FinalPreludePublicRoleMismatch - PreludeInfinityTheorem)) - pure roles - -validatePackagedPreludeInput - :: Prelude.ReservedParsedPrelude - -> ModuleSyntaxInterface - -> Either FinalPreludeFailure () -validatePackagedPreludeInput parsed syntax - | freshModuleInputOwner input /= preludeModuleName = - Left (FinalPreludeWrongOwner (freshModuleInputOwner input)) - | not (null (freshModuleInputImports input)) = - Left (FinalPreludeHasImports (freshModuleInputImports input)) - | not (null (moduleSyntaxDirectInputs syntax)) = - Left - (FinalPreludeHasSyntaxImports - (moduleSyntaxDirectInputs syntax)) - | otherwise = do - unless - ( freshModuleInputBinding input == FreshReservedSource - && freshModuleInputLocationPath input - == Prelude.preludeDiagnosticLabel - && freshModuleInputSyntaxInterface input == syntax - && identifiedParsedModuleSyntaxInterface identified == syntax - ) - (Left - (FinalPreludeValidationFailed - FinalPreludePackagedInputMismatch)) - where - input = Prelude.reservedParsedPreludeInput parsed - identified = Prelude.reservedParsedPreludeModule parsed - -associatePreludeDeclarations - :: Prelude.ReservedParsedPrelude - -> Declaration.PendingModulePrefix - -> Either - FinalPreludeValidationError - ([PreludeDeclaration], Declaration.CommittedDeclarationBatch) -associatePreludeDeclarations parsed prefix = do - case List.splitAt (length sourceDeclarations) batches of - (sourceBatches, [baseStructure]) - | length sourceBatches == length sourceDeclarations -> - pure - ( zipWith PreludeDeclaration - sourceDeclarations sourceBatches - , baseStructure - ) - _ -> Left FinalPreludeDeclarationAssociationMismatch - where - sourceDeclarations = - [ block - | block <- - identifiedParsedModuleBlocks - (Prelude.reservedParsedPreludeModule parsed) - , case block of - Raw.BlockProof{} -> False - _ -> True - ] - batches = Declaration.pendingModulePrefixBatches prefix - -validateConfinedAuthority - :: CheckedFoundation - -> SemanticInterface - -> CheckedObjectClosure - -> [PreludeDeclaration] - -> Declaration.CommittedDeclarationBatch - -> Either FinalPreludeValidationError () -validateConfinedAuthority - foundation semantic objects declarations baseStructure = do - unless - ( semanticInterfaceOwner semantic == preludeModuleName - && null (semanticInterfaceDirectInputs semantic) - ) - (Left FinalPreludeSemanticEnvironmentMismatch) - traverse_ requireTransparent - [ identity - | declaration <- declarations - , identity <- - declarationDeltaObjects - (Declaration.committedBatchDelta - (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 - -> PreludeDeclaration - -> Either FinalPreludeValidationError () -validateDeclarationAuthority foundation objects declaration = do - unless - (fmap Authority.validationTarget certificates - == fmap semanticFactAuthority facts) - (Left (FinalPreludeValidationInventoryMismatch slot)) - traverse_ validateOne (zip facts certificates) - where - batch = declarationBatch declaration - delta = Declaration.committedBatchDelta batch - slot = Declaration.committedBatchSlot batch - facts = declarationDeltaFacts delta - certificates = - ( Semantic.proofValidationRecordCertificate - <$> Declaration.committedBatchProofValidations batch - ) - <> maybe - [] - Semantic.declarationValidationRecordCertificates - (Declaration.committedBatchDeclarationValidation batch) - - validateOne (occurrence, certificate) = do - unless - (Authority.factAuthoritySafety - (semanticFactAuthority occurrence) - == Authority.cleanAuthoritySafety) - (Left (FinalPreludeAuthorityMismatch slot)) - proposition <- - maybe - (Left (FinalPreludeValidationInventoryMismatch slot)) - Right - (List.find - ((== semanticFactProposition occurrence) - . checkedPropositionId) - (Declaration.committedBatchPropositions batch)) - let target = frozenCoreTerm (checkedPropositionTerm proposition) - case Authority.validationDirectAuthorization certificate of - Authority.CheckedKernelConstruction - (Authority.FoundationLeaf tag) -> do - let expected = - frozenCoreTerm - (mapFrozenGlobals absurd - (foundationAxiomFrozen foundation tag)) - unless (target == expected) - (Left (FinalPreludeAuthorityMismatch slot)) - Authority.CheckedKernelConstruction - (Authority.CheckedDefinitionEquation identity) -> - case lookupCheckedObjectContent identity objects of - Just (TransparentObjectContent _theory coreType body) -> - unless - (target == CEq coreType (CGlobal identity) body) - (Left (FinalPreludeAuthorityMismatch slot)) - _ -> - Left (FinalPreludeAuthorityMismatch slot) - Authority.CheckedSourceProof requests -> - unless - ( not (null requests) - && case declarationBlock declaration of - Raw.BlockClaim{} -> True - _ -> False - ) - (Left (FinalPreludeAuthorityMismatch slot)) - _ -> - Left (FinalPreludeAuthorityMismatch slot) - -expectDefinition - :: CheckedFoundation - -> CheckedObjectClosure - -> [PreludeDeclaration] - -> Text - -> PreludeDefinitionKind - -> CoreType - -> CanonicalTerm ObjectId - -> Either FinalPreludeValidationError PreludeDefinitionView -expectDefinition foundation objects declarations marker kind coreType body = do - declaration <- findDeclaration marker declarations - let delta = - Declaration.committedBatchDelta - (declarationBatch declaration) - unless - (case (kind, declarationBlock declaration) of - (PreludeDefinition, Raw.BlockDefn{}) -> True - (PreludeAbbreviation, Raw.BlockAbbr{}) -> True - _ -> False) - (Left (FinalPreludeDeclarationShapeMismatch marker)) - binding <- - case semanticEnvironmentBindings - (declarationDeltaEnvironment delta) of - [single] -> Right single - _ -> Left (FinalPreludeDeclarationShapeMismatch marker) - let target = semanticGlobalBindingTarget binding - identity = semanticGlobalTargetObject target - unless - (case (kind, target) of - (PreludeDefinition, GlobalReference{}) -> True - (PreludeAbbreviation, TransparentExpansion{}) -> True - _ -> False) - (Left (FinalPreludeDefinitionContentMismatch marker)) - content <- - maybe - (Left (FinalPreludeDefinitionContentMismatch marker)) - Right - (lookupCheckedObjectContent identity objects) - let expected = - TransparentObjectContent - (theoryId foundation) - coreType - body - unless (content == expected) - (Left (FinalPreludeDefinitionContentMismatch marker)) - pure (PreludeDefinitionView identity target) - -expectClaim - :: [PreludeDeclaration] - -> Text - -> Either - FinalPreludeValidationError - (TheoremRef, CanonicalTerm ObjectId) -expectClaim declarations marker = do - declaration <- findDeclaration marker declarations - unless - (case declarationBlock declaration of - Raw.BlockClaim{} -> True - _ -> False) - (Left (FinalPreludeDeclarationShapeMismatch marker)) - expectFact declarations marker - -expectClaimTarget - :: [PreludeDeclaration] - -> Text - -> CanonicalTerm ObjectId - -> Either - FinalPreludeValidationError - (TheoremRef, CanonicalTerm ObjectId) -expectClaimTarget declarations marker expected = do - result@(_theorem, actual) <- expectClaim declarations marker - unless - (actual == expected) - (Left (FinalPreludeFactContentMismatch marker)) - pure result - -expectFact - :: [PreludeDeclaration] - -> Text - -> Either - FinalPreludeValidationError - (TheoremRef, CanonicalTerm ObjectId) -expectFact declarations marker = do - declaration <- findDeclaration marker declarations - let batch = declarationBatch declaration - delta = Declaration.committedBatchDelta batch - expectedAlias = semanticName marker - occurrence <- case declarationDeltaFacts delta of - [single] -> Right single - _ -> Left (FinalPreludeFactContentMismatch marker) - unless - (declarationDeltaAliases delta - == [semanticAlias expectedAlias - (semanticFactFingerprint occurrence)]) - (Left (FinalPreludeFactContentMismatch marker)) - proposition <- - maybe - (Left (FinalPreludeFactContentMismatch marker)) - Right - (List.find - ((== semanticFactProposition occurrence) - . checkedPropositionId) - (Declaration.committedBatchPropositions batch)) - pure - ( Authority.factAuthorityTheorem - (semanticFactAuthority occurrence) - , frozenCoreTerm (checkedPropositionTerm proposition) - ) - -expectFactTarget - :: [PreludeDeclaration] - -> Text - -> CanonicalTerm ObjectId - -> Either - FinalPreludeValidationError - (TheoremRef, CanonicalTerm ObjectId) -expectFactTarget declarations marker expected = do - result@(_theorem, actual) <- expectFact declarations marker - unless - (actual == expected) - (Left (FinalPreludeFactContentMismatch marker)) - pure result - -validateInfinityTarget - :: CheckedObjectClosure - -> ObjectId - -> CanonicalTerm ObjectId - -> Either FinalPreludeValidationError () -validateInfinityTarget objects inductive = \case - CApp (CGlobal predicate) (CGlobal witness) - | predicate == inductive -> - case lookupCheckedObjectContent witness objects of - Just TransparentObjectContent{} -> pure () - _ -> - Left - (FinalPreludeFactContentMismatch - "prelude_infinity") - _ -> - Left - (FinalPreludeFactContentMismatch - "prelude_infinity") - -findDeclaration - :: Text - -> [PreludeDeclaration] - -> Either FinalPreludeValidationError PreludeDeclaration -findDeclaration marker declarations = - case List.filter ((== marker) . declarationMarker) declarations of - [] -> Left (FinalPreludeDeclarationMissing marker) - [single] -> Right single - _ -> Left (FinalPreludeDeclarationDuplicate marker) - -declarationBlock :: PreludeDeclaration -> Raw.Block -declarationBlock (PreludeDeclaration block _batch) = - block - -declarationBatch - :: PreludeDeclaration - -> Declaration.CommittedDeclarationBatch -declarationBatch (PreludeDeclaration _block batch) = - batch - -declarationMarker :: PreludeDeclaration -> Text -declarationMarker = - fromMaybe "<unmarked>" . blockMarkerText . declarationBlock - -definitionViewObject :: PreludeDefinitionView -> ObjectId -definitionViewObject (PreludeDefinitionView identity _target) = - identity - -definitionViewTarget - :: PreludeDefinitionView - -> SemanticGlobalTarget -definitionViewTarget (PreludeDefinitionView _identity target) = - target - -blockMarkerText :: Raw.Block -> Maybe Text -blockMarkerText = fmap (\(Raw.Marker marker) -> marker) . \case - Raw.BlockAxiom _location _title marker _axiom -> Just marker - Raw.BlockClaim _kind _location _title marker _claim -> Just marker - Raw.BlockDefn _location _title marker _definition -> Just marker - Raw.BlockAbbr _location _title marker _abbreviation -> Just marker - Raw.BlockData _location _title marker _datatype -> Just marker - Raw.BlockInductive _location _title marker _inductive -> Just marker - Raw.BlockSig _location _title marker _assumptions _signature -> Just marker - Raw.BlockStruct _location _title marker _structure -> Just marker - Raw.BlockProof{} -> Nothing - -expectedSuccessorBody :: CanonicalTerm ObjectId -expectedSuccessorBody = - CLam TySet - (canonicalSetInsert (CBound 0) (CBound 0)) - -expectedInductiveBody :: ObjectId -> CanonicalTerm ObjectId -expectedInductiveBody successor = - CLam TySet - (logicalAnd - (memberTerm (CIntrinsic Empty) (CBound 0)) - (CForall TySet - (CImp - (memberTerm (CBound 0) (CBound 1)) - (memberTerm - (CApp (CGlobal successor) (CBound 0)) - (CBound 1))))) - -expectedOmegaBody - :: ObjectId - -> ObjectId - -> CanonicalTerm ObjectId -expectedOmegaBody u0 inductive = - CApp - (CApp (CIntrinsic Sep) (CGlobal u0)) - (CLam TySet - (CForall TySet - (CImp - (CApp (CGlobal inductive) (CBound 0)) - (memberTerm (CBound 1) (CBound 0))))) - -expectedMinimality - :: ObjectId - -> ObjectId - -> CanonicalTerm ObjectId -expectedMinimality inductive omega = - CForall TySet - (CImp - (CApp (CGlobal inductive) (CBound 0)) - (CForall TySet - (CImp - (memberTerm (CBound 0) (CGlobal omega)) - (memberTerm (CBound 0) (CBound 1))))) - -applyIntrinsic - :: CoreIntrinsicTag - -> CanonicalTerm global - -> CanonicalTerm global -applyIntrinsic intrinsic argument = - CApp (CIntrinsic intrinsic) argument - -applyIntrinsic2 - :: CoreIntrinsicTag - -> CanonicalTerm global - -> CanonicalTerm global - -> CanonicalTerm global -applyIntrinsic2 intrinsic firstArgument secondArgument = - CApp - (CApp (CIntrinsic intrinsic) firstArgument) - secondArgument - -memberTerm - :: CanonicalTerm global - -> CanonicalTerm global - -> CanonicalTerm global -memberTerm = - applyIntrinsic2 Member - -logicalAnd - :: CanonicalTerm global - -> CanonicalTerm global - -> CanonicalTerm global -logicalAnd left right = - CImp - (CImp left (CImp right CFalsum)) - CFalsum |