diff options
Diffstat (limited to 'source/Checking/Transition.hs')
| -rw-r--r-- | source/Checking/Transition.hs | 2584 |
1 files changed, 0 insertions, 2584 deletions
diff --git a/source/Checking/Transition.hs b/source/Checking/Transition.hs deleted file mode 100644 index a2e7054..0000000 --- a/source/Checking/Transition.hs +++ /dev/null @@ -1,2584 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Closed in-memory carrier used while declaration families migrate from the --- disposable legacy checker to checked typed semantics. -module Checking.Transition - ( ModuleName - , moduleName - , moduleNameNamespace - , moduleNameRelativePath - , LocalDeclarationOrdinal - , localDeclarationOrdinalValue - , LocalFactOrdinal - , localFactOrdinalValue - , LocalAssumptionOrdinal - , localAssumptionOrdinalValue - , OpaqueDeclarationRef - , opaqueDeclarationModule - , opaqueDeclarationOrdinal - , Origin - , origin - , CheckedGlobalRef - , checkedGlobalReference - , checkedGlobalType - , FactRef - , factReferenceModule - , factReferenceOrdinal - , TransitionFactRef - , transitionTypedFactReference - , TypedDirectAxiomManifestEntry - , typedDirectAssumptionFact - , typedDirectAssumptionKind - , typedDirectAssumptionStatement - , SessionTypedDeclaredAssumptionRef - , sessionTypedAssumptionFact - , sessionTypedAssumptionOrdinal - , sessionTypedAssumptionKind - , sessionTypedAssumptionStatement - , SessionTypedTrustedVampireUse - , TypedTrustDependencies - , typedDeclaredAssumptionUses - , typedTrustedVampireUses - , typedVampireLoweringUses - , typedFoundationUses - , typedKernelRuleUses - , TransitionDerivationImport - , transitionDerivationImport - , lookupTransitionTypedImport - , AdmittedFact - , admittedFactReference - , admittedFactIsKernelProof - , admittedFactIsReconstructedKernelProof - , admittedFactIsTrustedVampire - , admittedFactTypedTrustDependencies - , TransitionModuleBuilder - , openTransitionModuleBuilder - , transitionBuilderLegacyStage - , transitionBuilderImportedCheckingEnvironment - , transitionBuilderFoundation - , GlobalPremisePolicy(..) - , TransitionTypedProblemError(..) - , planTransitionTypedProblem - , beginTransitionDeclaration - , transitionCurrentDeclarationReference - , commitTransitionOpaqueGlobal - , commitTransitionTransparentGlobal - , commitTransitionKernelFact - , commitTransitionKernelFactWithImports - , commitTransitionTypedVampireFact - , commitTransitionTypedDeclaredAssumption - , transitionBuilderWithLegacyStage - , lookupTransitionGlobal - , lookupTransitionGlobalBody - , TransitionAdmittedModule - , sealTransitionModule - , transitionAdmittedName - , transitionAdmittedLegacyModule - , transitionAdmittedFacts - , transitionAdmittedKernelProofCount - , transitionAdmittedTypedTrustedVampireCount - , TransitionReplayMeasurements(..) - , transitionAdmittedReplayMeasurements - , transitionAdmittedTypedDirectAxiomManifest - , transitionAdmittedTypedTrustDependencies - , transitionAdmittedGlobals - , TransitionModuleError(..) - ) where - -import Base -import Checking.Backend.Connection qualified as BackendConnection -import Checking.Backend.Problem qualified as Backend -import Checking.Backend.Reconstruction qualified as BackendReconstruction -import Checking.Backend.Tptp qualified as BackendTptp -import Checking.Core -import Checking.Facts qualified as Facts -import Checking.Foundation - ( CheckedFoundation - , FoundationAxiomTag - , KernelRuleTag - , foundationAxiomFrozen - ) -import Checking.Kernel.Derivation -import Checking.Legacy -import Felix.Module -import Provers qualified -import Report.Location -import Syntax.Internal - -import Control.Monad (foldM, unless) -import Data.Bifunctor (first) -import Data.Map.Strict qualified as Map -import Data.Sequence qualified as Seq -import Data.Set qualified as Set -import Data.Vector (Vector) -import Data.Vector qualified as Vector -import Numeric.Natural (Natural) - - -data OpaqueDeclarationRef = OpaqueDeclarationRef - !ModuleName - !LocalDeclarationOrdinal - deriving stock (Show, Eq, Ord) - -opaqueDeclarationModule - :: OpaqueDeclarationRef - -> ModuleName -opaqueDeclarationModule - (OpaqueDeclarationRef name _ordinal) = - name - -opaqueDeclarationOrdinal - :: OpaqueDeclarationRef - -> LocalDeclarationOrdinal -opaqueDeclarationOrdinal - (OpaqueDeclarationRef _name ordinal) = - ordinal - -data Origin = Origin - !Location - !(Maybe Text) - !(Maybe Marker) - deriving stock (Show, Eq) - -origin - :: Location - -> Maybe Text - -> Maybe Marker - -> Origin -origin = - Origin - - -data CheckedGlobalRef = CheckedOpaqueGlobal - !OpaqueDeclarationRef - !CoreType - deriving stock (Show, Eq, Ord) - -checkedGlobalReference - :: CheckedGlobalRef - -> OpaqueDeclarationRef -checkedGlobalReference - (CheckedOpaqueGlobal reference _coreType) = - reference - -checkedGlobalType :: CheckedGlobalRef -> CoreType -checkedGlobalType - (CheckedOpaqueGlobal _reference coreType) = - coreType - -newtype LocalAssumptionOrdinal = - LocalAssumptionOrdinal Natural - deriving stock (Show, Eq, Ord) - -localAssumptionOrdinalValue - :: LocalAssumptionOrdinal - -> Natural -localAssumptionOrdinalValue - (LocalAssumptionOrdinal ordinal) = - ordinal - -data FactRef = FactRef - !ModuleName - !LocalFactOrdinal - deriving stock (Show, Eq, Ord) - -factReferenceModule :: FactRef -> ModuleName -factReferenceModule (FactRef name _ordinal) = - name - -factReferenceOrdinal :: FactRef -> LocalFactOrdinal -factReferenceOrdinal (FactRef _name ordinal) = - ordinal - -data TransitionFactRef - = TransitionLegacyFactRef !LegacyFactRef - | TransitionTypedFactRef !FactRef - deriving stock (Show, Eq, Ord) - -transitionTypedFactReference - :: TransitionFactRef - -> Maybe FactRef -transitionTypedFactReference = \case - TransitionLegacyFactRef{} -> - Nothing - TransitionTypedFactRef reference -> - Just reference - -data TypedSemanticFact = TypedSemanticFact - !(FrozenCheckedCore CheckedGlobalRef) - !(Backend.SupportedProposition - Void - CheckedGlobalRef) - !(Backend.FofCapability - (Backend.CheckedFofProjection - Void - CheckedGlobalRef)) - deriving stock (Eq) - -prepareTypedSemanticFact - :: TransitionModuleBuilder - -> FrozenCheckedCore CheckedGlobalRef - -> Either TransitionModuleError TypedSemanticFact -prepareTypedSemanticFact builder supplied = do - statement <- - recheckBuilderFrozenCore builder supplied - prepare statement - where - prepare statement - | frozenCoreType statement /= TyProp = - Left - (TransitionTypedFactIsNotProposition - (frozenCoreType statement)) - | otherwise = do - proposition <- - first TransitionTypedFactSupportError - (Backend.supportedProposition - Vector.empty - (embedClosedCore [] statement)) - capability <- - first TransitionTypedFactClassificationError - (Backend.classifySupportedProposition - (builderGlobalType builder) - proposition) - Right - (TypedSemanticFact - statement - proposition - capability) - -typedSemanticStatement - :: TypedSemanticFact - -> FrozenCheckedCore CheckedGlobalRef -typedSemanticStatement - (TypedSemanticFact - statement - _proposition - _capability) = - statement - -typedSemanticProposition - :: TypedSemanticFact - -> Backend.SupportedProposition - Void - CheckedGlobalRef -typedSemanticProposition - (TypedSemanticFact - _statement - proposition - _capability) = - proposition - -typedSemanticFofCapability - :: TypedSemanticFact - -> Backend.FofCapability - (Backend.CheckedFofProjection - Void - CheckedGlobalRef) -typedSemanticFofCapability - (TypedSemanticFact - _statement - _proposition - capability) = - capability - -data TypedDirectAxiomManifestEntry = - TypedDirectAxiomManifestEntry - !FactRef - !AssumptionKind - !(FrozenCheckedCore CheckedGlobalRef) - deriving stock (Show, Eq, Ord) - -typedDirectAssumptionFact - :: TypedDirectAxiomManifestEntry - -> FactRef -typedDirectAssumptionFact - (TypedDirectAxiomManifestEntry reference _kind _statement) = - reference - -typedDirectAssumptionKind - :: TypedDirectAxiomManifestEntry - -> AssumptionKind -typedDirectAssumptionKind - (TypedDirectAxiomManifestEntry _reference kind _statement) = - kind - -typedDirectAssumptionStatement - :: TypedDirectAxiomManifestEntry - -> FrozenCheckedCore CheckedGlobalRef -typedDirectAssumptionStatement - (TypedDirectAxiomManifestEntry _reference _kind statement) = - statement - -data SessionTypedDeclaredAssumptionRef = - SessionTypedDeclaredAssumptionRef - !FactRef - !LocalAssumptionOrdinal - !AssumptionKind - !(FrozenCheckedCore CheckedGlobalRef) - deriving stock (Show, Eq, Ord) - -sessionTypedAssumptionFact - :: SessionTypedDeclaredAssumptionRef - -> FactRef -sessionTypedAssumptionFact - (SessionTypedDeclaredAssumptionRef - reference - _ordinal - _kind - _statement) = - reference - -sessionTypedAssumptionOrdinal - :: SessionTypedDeclaredAssumptionRef - -> LocalAssumptionOrdinal -sessionTypedAssumptionOrdinal - (SessionTypedDeclaredAssumptionRef - _reference - ordinal - _kind - _statement) = - ordinal - -sessionTypedAssumptionKind - :: SessionTypedDeclaredAssumptionRef - -> AssumptionKind -sessionTypedAssumptionKind - (SessionTypedDeclaredAssumptionRef - _reference - _ordinal - kind - _statement) = - kind - -sessionTypedAssumptionStatement - :: SessionTypedDeclaredAssumptionRef - -> FrozenCheckedCore CheckedGlobalRef -sessionTypedAssumptionStatement - (SessionTypedDeclaredAssumptionRef - _reference - _ordinal - _kind - statement) = - statement - -newtype SessionTypedTrustedVampireUse = - SessionTypedTrustedVampireUse FactRef - deriving stock (Show, Eq, Ord) - -data TypedTrustDependencies = TypedTrustDependencies - { typedDeclaredAssumptionUses - :: !(Set SessionTypedDeclaredAssumptionRef) - , typedTrustedVampireUses - :: !(Set SessionTypedTrustedVampireUse) - , typedVampireLoweringUses - :: !(Set VampireLoweringAssumption) - , typedFoundationUses - :: !(Set FoundationAxiomTag) - , typedKernelRuleUses - :: !(Set KernelRuleTag) - } - deriving stock (Show, Eq) - -instance Semigroup TypedTrustDependencies where - left <> right = - TypedTrustDependencies - { typedDeclaredAssumptionUses = - typedDeclaredAssumptionUses left - <> typedDeclaredAssumptionUses right - , typedTrustedVampireUses = - typedTrustedVampireUses left - <> typedTrustedVampireUses right - , typedVampireLoweringUses = - typedVampireLoweringUses left - <> typedVampireLoweringUses right - , typedFoundationUses = - typedFoundationUses left - <> typedFoundationUses right - , typedKernelRuleUses = - typedKernelRuleUses left - <> typedKernelRuleUses right - } - -instance Monoid TypedTrustDependencies where - mempty = - TypedTrustDependencies - { typedDeclaredAssumptionUses = mempty - , typedTrustedVampireUses = mempty - , typedVampireLoweringUses = mempty - , typedFoundationUses = mempty - , typedKernelRuleUses = mempty - } - -data AuthorizedKernelReplay = - AuthorizedKernelReplay - !(FrozenCheckedCore CheckedGlobalRef) - !(Set FactRef) - !(Set FoundationAxiomTag) - !(Set KernelRuleTag) - !Natural - !Natural - !(Maybe SessionTypedReconstructionProvenance) - deriving stock (Eq) - -data SessionTypedReconstructionProvenance = - SessionTypedReconstructionProvenance - !BackendReconstruction.ReconstructionPolicy - !(BackendTptp.PreparedTypedTptpProblem - TransitionFactRef - Void - CheckedGlobalRef) - !Provers.AcceptedVampireRun - !BackendConnection.ConnectionTrace - !BackendConnection.ConnectionSearchStats - !Natural - !Natural - deriving stock (Eq) - -data SessionTypedReconstructionFallback = - SessionTypedReconstructionFallback - !BackendReconstruction.ReconstructionPolicy - !SessionTypedReconstructionFallbackReason - deriving stock (Eq) - -data SessionTypedReconstructionFallbackReason - = ReconstructionFallbackUnsupported - !(BackendConnection.ConnectionUnsupported - TransitionFactRef) - | ReconstructionFallbackUnavailable - !BackendConnection.ConnectionSearchStats - | ReconstructionFallbackSearchExhausted - !BackendConnection.ConnectionExhaustion - !BackendConnection.ConnectionSearchStats - | ReconstructionFallbackKernelReplayExhausted - !KernelReplayError - deriving stock (Eq) - -data SessionTypedTrustedVampireEvidence = - SessionTypedTrustedVampireEvidence - !FactRef - !(FrozenCheckedCore CheckedGlobalRef) - !(BackendTptp.PreparedTypedTptpProblem - TransitionFactRef - Void - CheckedGlobalRef) - !Provers.AcceptedVampireRun - !TypedTrustDependencies - !SessionTypedReconstructionFallback - deriving stock (Eq) - -data FactAuthorization - = KernelProof - !AuthorizedKernelReplay - !TypedTrustDependencies - | DeclaredAssumption - !SessionTypedDeclaredAssumptionRef - | TrustedVampire - !SessionTypedTrustedVampireEvidence - deriving stock (Eq) - -data TypedAdmittedFact = TypedAdmittedFact - !TypedSemanticFact - !FactAuthorization - deriving stock (Eq) - -commitTransitionKernelFact - :: NonEmpty Marker - -> Origin - -> FrozenCheckedCore CheckedGlobalRef - -> KernelDerivation CheckedGlobalRef - -> TransitionModuleBuilder - -> Either TransitionModuleError TransitionModuleBuilder -commitTransitionKernelFact aliases factOrigin target derivation builder = - commitTransitionKernelFactWithImports - aliases - factOrigin - Vector.empty - target - derivation - builder - -commitTransitionKernelFactWithImports - :: NonEmpty Marker - -> Origin - -> Vector TransitionDerivationImport - -> FrozenCheckedCore CheckedGlobalRef - -> KernelDerivation CheckedGlobalRef - -> TransitionModuleBuilder - -> Either TransitionModuleError TransitionModuleBuilder -commitTransitionKernelFactWithImports - aliases - factOrigin - imports - target - derivation - builder = do - admitted <- - authorizeTransitionKernelFactWithImports - imports - target - derivation - builder - insertTransitionTypedFact - aliases - factOrigin - admitted - builder - -data TransitionDerivationImport = - TransitionDerivationImport - !TransitionFactRef - !(DerivationImportJudgment CheckedGlobalRef) - deriving stock (Eq) - -transitionDerivationImport - :: TransitionFactRef - -> FrozenCheckedCore CheckedGlobalRef - -> Either - TransitionModuleError - TransitionDerivationImport -transitionDerivationImport reference statement = - TransitionDerivationImport reference - <$> first - TransitionDerivationImportError - (derivationImportJudgment statement) - -lookupTransitionTypedImport - :: FrozenCheckedCore CheckedGlobalRef - -> TransitionModuleBuilder - -> Either - TransitionModuleError - (Maybe TransitionDerivationImport) -lookupTransitionTypedImport statement builder = - case Vector.find - ((== Just statement) - . admittedFactStatement - . entryFact) - (builderVisibleFacts builder) of - Nothing -> - Right Nothing - Just - (TransitionFactEntry - fact@(TypedFactRow _reference admitted) - _registration) -> do - unless - (typedAdmittedStatement admitted - == statement) - (Left TransitionKernelTargetMismatch) - Just - <$> transitionDerivationImport - (admittedFactReference fact) - statement - Just (TransitionFactEntry LegacyFactRow{} _registration) -> - Right Nothing - where - entryFact - (TransitionFactEntry fact _registration) = - fact - -authorizeTransitionKernelFactWithImports - :: Vector TransitionDerivationImport - -> FrozenCheckedCore CheckedGlobalRef - -> KernelDerivation CheckedGlobalRef - -> TransitionModuleBuilder - -> Either TransitionModuleError TypedAdmittedFact -authorizeTransitionKernelFactWithImports - imports - target - derivation - builder = do - authorizeTransitionKernelFactWithImportsAndProvenance - defaultKernelReplayLimits - Nothing - imports - target - derivation - builder - -authorizeTransitionKernelFactWithImportsAndProvenance - :: KernelReplayLimits - -> Maybe SessionTypedReconstructionProvenance - -> Vector TransitionDerivationImport - -> FrozenCheckedCore CheckedGlobalRef - -> KernelDerivation CheckedGlobalRef - -> TransitionModuleBuilder - -> Either TransitionModuleError TypedAdmittedFact -authorizeTransitionKernelFactWithImportsAndProvenance - replayLimits - provenance - imports - target - derivation - builder = do - semantic <- - prepareTypedSemanticFact builder target - let checkedTarget = - typedSemanticStatement semantic - replayed <- - first TransitionKernelReplayError - (replayKernelDerivation - (builderFoundation builder) - replayLimits - (builderGlobalType builder) - (derivationImport - <$> imports) - checkedTarget - derivation) - inheritedTrust <- - foldM - (\trust index -> - (trust <>) - <$> authorizeUsedImport - imports - builder - index) - mempty - (Set.toAscList - (replayedKernelImportUses replayed)) - let foundationTrust = - mempty - { typedFoundationUses = - replayedKernelFoundationUses replayed - , typedKernelRuleUses = - replayedKernelRuleUses replayed - } - authorization = - AuthorizedKernelReplay - (replayedKernelTarget replayed) - (Set.fromList - [ reference - | index <- - Set.toAscList - (replayedKernelImportUses replayed) - , Right - (TransitionDerivationImport - (TransitionTypedFactRef reference) - _judgment) <- - [transitionImportAt imports index] - ]) - (replayedKernelFoundationUses replayed) - (replayedKernelRuleUses replayed) - (replayedKernelNodeCount replayed) - (replayedKernelMaximumDepth replayed) - provenance - unless - (typedSemanticStatement semantic - == replayedKernelTarget replayed) - (Left TransitionKernelTargetMismatch) - pure - (TypedAdmittedFact - semantic - (KernelProof - authorization - (inheritedTrust <> foundationTrust))) - -typedAdmittedStatement - :: TypedAdmittedFact - -> FrozenCheckedCore CheckedGlobalRef -typedAdmittedStatement - (TypedAdmittedFact semantic _authorization) = - typedSemanticStatement semantic - -typedAdmittedTrustDependencies - :: TypedAdmittedFact - -> TypedTrustDependencies -typedAdmittedTrustDependencies - (TypedAdmittedFact _semantic authorization) = - factAuthorizationTrust authorization - -data AdmittedFact - = LegacyFactRow - !TransitionFactRef - !H1LegacyAdmittedFact - | TypedFactRow - !TransitionFactRef - !TypedAdmittedFact - deriving stock (Eq) - -admittedFactReference - :: AdmittedFact - -> TransitionFactRef -admittedFactReference = \case - LegacyFactRow reference _admitted -> - reference - TypedFactRow reference _admitted -> - reference - -admittedFactIsKernelProof :: AdmittedFact -> Bool -admittedFactIsKernelProof = \case - LegacyFactRow{} -> - False - TypedFactRow _reference - (TypedAdmittedFact _semantic authorization) -> - case authorization of - KernelProof{} -> - True - DeclaredAssumption{} -> - False - TrustedVampire{} -> - False - -admittedFactIsReconstructedKernelProof :: AdmittedFact -> Bool -admittedFactIsReconstructedKernelProof = \case - LegacyFactRow{} -> - False - TypedFactRow _reference - (TypedAdmittedFact _semantic authorization) -> - case authorization of - KernelProof - (AuthorizedKernelReplay - _target - _imports - _foundation - _rules - _nodes - _depth - (Just _provenance)) - _trust -> - True - KernelProof{} -> - False - DeclaredAssumption{} -> - False - TrustedVampire{} -> - False - -admittedFactIsTrustedVampire :: AdmittedFact -> Bool -admittedFactIsTrustedVampire = \case - LegacyFactRow{} -> - False - TypedFactRow _reference - (TypedAdmittedFact _semantic authorization) -> - case authorization of - KernelProof{} -> - False - DeclaredAssumption{} -> - False - TrustedVampire{} -> - True - -admittedFactTypedTrustDependencies - :: AdmittedFact - -> Maybe TypedTrustDependencies -admittedFactTypedTrustDependencies = \case - LegacyFactRow{} -> - Nothing - TypedFactRow _reference admitted -> - Just (typedAdmittedTrustDependencies admitted) - -admittedFactStatement - :: AdmittedFact - -> Maybe (FrozenCheckedCore CheckedGlobalRef) -admittedFactStatement = \case - LegacyFactRow{} -> - Nothing - TypedFactRow _reference admitted -> - Just (typedAdmittedStatement admitted) - -factAuthorizationTrust - :: FactAuthorization - -> TypedTrustDependencies -factAuthorizationTrust = \case - KernelProof _replay trust -> - trust - DeclaredAssumption reference -> - mempty - { typedDeclaredAssumptionUses = - Set.singleton reference - } - TrustedVampire - (SessionTypedTrustedVampireEvidence - _reference - _target - _prepared - _accepted - trust - _fallback) -> - trust - -derivationImport - :: TransitionDerivationImport - -> DerivationImportJudgment CheckedGlobalRef -derivationImport - (TransitionDerivationImport _reference judgment) = - judgment - -transitionImportAt - :: Vector TransitionDerivationImport - -> ImportIx - -> Either - TransitionModuleError - TransitionDerivationImport -transitionImportAt imports index - | naturalIndex > - fromIntegral (maxBound :: Int) = - Left - (TransitionKernelImportIndexOutOfBounds - index) - | otherwise = - maybe - (Left - (TransitionKernelImportIndexOutOfBounds - index)) - Right - (imports Vector.!? fromIntegral naturalIndex) - where - naturalIndex = - importIxValue index - -authorizeUsedImport - :: Vector TransitionDerivationImport - -> TransitionModuleBuilder - -> ImportIx - -> Either - TransitionModuleError - TypedTrustDependencies -authorizeUsedImport imports builder index = do - TransitionDerivationImport reference judgment <- - transitionImportAt imports index - case reference of - TransitionLegacyFactRef{} -> - Left - (TransitionDependencyNotMigrated - reference) - TransitionTypedFactRef _typedReference -> do - TransitionFactEntry fact _registration <- - maybe - (Left - (TransitionKernelImportNotVisible - reference)) - Right - (lookupBuilderFact reference builder) - case fact of - LegacyFactRow{} -> - Left - (TransitionDependencyNotMigrated - reference) - TypedFactRow rowReference admitted -> do - unless - (rowReference == reference - && typedAdmittedStatement admitted - == derivationImportStatement - judgment) - (Left - (TransitionKernelImportDoesNotMatch - reference)) - pure - (typedAdmittedTrustDependencies - admitted) - -builderVisibleFacts - :: TransitionModuleBuilder - -> Vector TransitionFactEntry -builderVisibleFacts = - Vector.fromList - . toList - . inventoryFactOrder - . builderFactInventory - -lookupBuilderFact - :: TransitionFactRef - -> TransitionModuleBuilder - -> Maybe TransitionFactEntry -lookupBuilderFact reference = - Map.lookup reference - . inventoryFactsByReference - . builderFactInventory - -data TransitionFactRegistration = TransitionFactRegistration - !(NonEmpty Marker) - !Origin - deriving stock (Eq) - -data TransitionFactEntry = TransitionFactEntry - !AdmittedFact - !TransitionFactRegistration - deriving stock (Eq) - -data TransitionFactInventory = TransitionFactInventory - { inventoryFactsByReference - :: !(Map TransitionFactRef TransitionFactEntry) - , inventoryAliases - :: !(Map Marker (TransitionFactRef, Origin)) - , inventoryFactOrder :: !(Seq TransitionFactEntry) - , inventoryFofOrder :: !(Seq TransitionFactRef) - } - -emptyTransitionFactInventory :: TransitionFactInventory -emptyTransitionFactInventory = - TransitionFactInventory - { inventoryFactsByReference = Map.empty - , inventoryAliases = Map.empty - , inventoryFactOrder = Seq.empty - , inventoryFofOrder = Seq.empty - } - -insertTransitionFactEntry - :: TransitionFactEntry - -> TransitionFactInventory - -> Either TransitionModuleError TransitionFactInventory -insertTransitionFactEntry - entry@(TransitionFactEntry - fact - (TransitionFactRegistration - aliases - factOrigin)) - inventory = - case Map.lookup - reference - (inventoryFactsByReference inventory) of - Just previous - | previous == entry -> - Right inventory - | otherwise -> - Left - (TransitionFactReferenceConflict - reference) - Nothing -> do - aliases' <- - insertFactAliases - reference - factOrigin - aliases - (inventoryAliases inventory) - pure - inventory - { inventoryFactsByReference = - Map.insert - reference - entry - (inventoryFactsByReference - inventory) - , inventoryAliases = aliases' - , inventoryFactOrder = - inventoryFactOrder inventory - Seq.|> entry - , inventoryFofOrder = - case typedFofReference fact of - Nothing -> - inventoryFofOrder inventory - Just fofReference -> - inventoryFofOrder inventory - Seq.|> fofReference - } - where - reference = - admittedFactReference fact - - typedFofReference = \case - LegacyFactRow{} -> - Nothing - TypedFactRow rowReference - (TypedAdmittedFact - semantic - _authorization) -> - case typedSemanticFofCapability semantic of - Backend.FofProjectable{} -> - Just rowReference - Backend.RequiresTh0{} -> - Nothing - -data TypedGlobalBinding = TypedGlobalBinding - !Symbol - !CheckedGlobalRef - !Origin - !(Maybe (FrozenCheckedCore CheckedGlobalRef)) - deriving stock (Eq) - -instance Show TypedGlobalBinding where - show - (TypedGlobalBinding - symbol - reference - bindingOrigin - body) = - "TypedGlobalBinding " - <> show symbol - <> " " - <> show reference - <> " " - <> show bindingOrigin - <> if isJust body - then " Transparent" - else " Opaque" - -data TypedModuleEnvironmentDelta = - TypedModuleEnvironmentDelta - !ModuleName - !(Vector TypedGlobalBinding) - deriving stock (Show, Eq) - -data TransitionModuleBuilder = TransitionModuleBuilder - { builderFoundation :: !CheckedFoundation - , builderName :: !ModuleName - , builderLegacyStage :: !LegacyModuleStage - , builderEnvironmentDeltas - :: !(Vector TypedModuleEnvironmentDelta) - , builderGlobals :: !(Map Symbol TypedGlobalBinding) - , builderGlobalDeclarations - :: !(Map OpaqueDeclarationRef TypedGlobalBinding) - , builderLocalGlobalsReversed :: ![TypedGlobalBinding] - , builderFactInventory :: !TransitionFactInventory - , builderLocalFactsReversed :: ![TransitionFactEntry] - , builderTypedDirectAxiomManifestReversed - :: ![TypedDirectAxiomManifestEntry] - , builderNextTypedFact :: !Natural - , builderNextTypedAssumption :: !Natural - , builderNextDeclaration :: !Natural - , builderCurrentDeclaration - :: !(Maybe OpaqueDeclarationRef) - } - -openTransitionModuleBuilder - :: CheckedFoundation - -> LegacyCheckingEnvironment - -> LegacyModuleAssignment - -> [TransitionAdmittedModule] - -> Either TransitionModuleError TransitionModuleBuilder -openTransitionModuleBuilder - checkedFoundationValue - foundation - assignment - directImports = - checkedFoundationValue `seq` do - importedView <- - first TransitionLegacyModuleError - (legacyImportedView - foundation - (transitionAdmittedLegacyModule <$> directImports)) - (environmentDeltas, globals, globalDeclarations) <- - mergeTypedEnvironments directImports - factInventory <- - mergeTransitionFacts directImports - let address = - legacyStageSourceAddress legacyStage - name = - moduleName address - legacyStage = - openLegacyModuleStage assignment importedView - pure - TransitionModuleBuilder - { builderFoundation = - checkedFoundationValue - , builderName = name - , builderLegacyStage = legacyStage - , builderEnvironmentDeltas = - environmentDeltas - , builderGlobals = globals - , builderGlobalDeclarations = - globalDeclarations - , builderLocalGlobalsReversed = [] - , builderFactInventory = factInventory - , builderLocalFactsReversed = [] - , builderTypedDirectAxiomManifestReversed = [] - , builderNextTypedFact = 0 - , builderNextTypedAssumption = 0 - , builderNextDeclaration = 0 - , builderCurrentDeclaration = Nothing - } - -transitionBuilderLegacyStage - :: TransitionModuleBuilder - -> LegacyModuleStage -transitionBuilderLegacyStage - builder = - builderLegacyStage builder - -transitionBuilderImportedCheckingEnvironment - :: TransitionModuleBuilder - -> LegacyCheckingEnvironment -transitionBuilderImportedCheckingEnvironment = - legacyStageImportedCheckingEnvironment - . transitionBuilderLegacyStage - -transitionBuilderFoundation - :: TransitionModuleBuilder - -> CheckedFoundation -transitionBuilderFoundation = - builderFoundation - -builderGlobalType - :: TransitionModuleBuilder - -> CheckedGlobalRef - -> Maybe CoreType -builderGlobalType builder reference = - case Map.lookup - (checkedGlobalReference reference) - (builderGlobalDeclarations builder) of - Just - (TypedGlobalBinding - _symbol - authoritative - _origin - _body) - | checkedGlobalType reference - == checkedGlobalType authoritative -> - Just (checkedGlobalType authoritative) - _ -> - Nothing - -validateBuilderGlobalReference - :: TransitionModuleBuilder - -> CheckedGlobalRef - -> Either TransitionModuleError CoreType -validateBuilderGlobalReference builder reference = - case Map.lookup - (checkedGlobalReference reference) - (builderGlobalDeclarations builder) of - Nothing -> - Left - (TransitionGlobalReferenceNotVisible - reference) - Just - (TypedGlobalBinding - _symbol - authoritative - _origin - _body) - | checkedGlobalType reference - == checkedGlobalType authoritative -> - Right (checkedGlobalType authoritative) - | otherwise -> - Left - (TransitionGlobalReferenceTypeMismatch - reference - (checkedGlobalType authoritative)) - -validateBuilderCanonicalGlobals - :: TransitionModuleBuilder - -> CanonicalTerm CheckedGlobalRef - -> Either TransitionModuleError () -validateBuilderCanonicalGlobals builder = - traverse_ - (void . validateBuilderGlobalReference builder) - . Set.toAscList - . canonicalTermGlobals - -recheckBuilderFrozenCore - :: TransitionModuleBuilder - -> FrozenCheckedCore CheckedGlobalRef - -> Either - TransitionModuleError - (FrozenCheckedCore CheckedGlobalRef) -recheckBuilderFrozenCore builder supplied = do - validateBuilderCanonicalGlobals - builder - (frozenCoreTerm supplied) - first TransitionCoreCheckError - (checkCanonicalCore - (builderGlobalType builder) - (frozenCoreTerm supplied)) - -data GlobalPremisePolicy - = ImplicitFofFacts - | ExplicitFacts !(NonEmpty Marker) - | NoGlobalFacts - deriving stock (Show, Eq) - -planTransitionTypedProblem - :: Ord local - => TransitionModuleBuilder - -> Backend.SupportedProposition - local - CheckedGlobalRef - -> [ Backend.TypedLocalPremise - local - Origin - CheckedGlobalRef - ] - -> [ Backend.TypedFoundationAuxiliaryInput - CheckedGlobalRef - ] - -> GlobalPremisePolicy - -> Backend.LocalPremisePolicy - -> Either - (TransitionTypedProblemError local) - (Backend.TypedProblem - TransitionFactRef - local - Origin - CheckedGlobalRef) -planTransitionTypedProblem - builder - claim - localPremises - auxiliaries - globalPolicy - localPolicy = do - first TransitionTypedProblemGlobalValidationError - (do - validateBuilderCanonicalGlobals - builder - (Backend.supportedPropositionTerm claim) - traverse_ - ( validateBuilderCanonicalGlobals builder - . Backend.supportedPropositionTerm - . Backend.typedLocalPremiseProposition - ) - localPremises) - (selectedFacts, premiseMode) <- - selectTransitionBackendFacts - builder - globalPolicy - first TransitionTypedProblemPlanningError - (Backend.planTypedProblem - (builderGlobalType builder) - selectedFacts - claim - localPremises - auxiliaries - premiseMode - localPolicy) - -selectTransitionBackendFacts - :: TransitionModuleBuilder - -> GlobalPremisePolicy - -> Either - (TransitionTypedProblemError local) - ( Vector - (Backend.TypedBackendFact - TransitionFactRef - CheckedGlobalRef) - , Backend.GlobalPremiseMode - ) -selectTransitionBackendFacts builder policy = do - references <- - case policy of - ImplicitFofFacts -> - Right - (toList - (inventoryFofOrder inventory)) - ExplicitFacts aliases -> - stableUnique - <$> traverse resolveAlias (toList aliases) - NoGlobalFacts -> - Right [] - facts <- - Vector.fromList - <$> traverse resolveFact references - pure - ( facts - , case policy of - ImplicitFofFacts -> - Backend.ImplicitFofPremises - ExplicitFacts{} -> - Backend.ExplicitGlobalPremises - NoGlobalFacts -> - Backend.NoGlobalPremises - ) - where - inventory = - builderFactInventory builder - - resolveAlias alias = - case Map.lookup alias (inventoryAliases inventory) of - Nothing -> - Left - (TransitionTypedProblemUnknownFactAlias - alias) - Just (reference, _origin) -> - Right reference - - resolveFact reference = - case Map.lookup - reference - (inventoryFactsByReference inventory) of - Nothing -> - Left - (TransitionTypedProblemFactReferenceMissing - reference) - Just (TransitionFactEntry LegacyFactRow{} _registration) -> - Left - (TransitionTypedProblemDependencyNotMigrated - reference) - Just - (TransitionFactEntry - (TypedFactRow rowReference - (TypedAdmittedFact - semantic - _authorization)) - _registration) - | rowReference == reference -> - Right - (Backend.typedBackendFact - reference - (typedSemanticProposition semantic) - (typedSemanticFofCapability semantic)) - | otherwise -> - Left - (TransitionTypedProblemFactReferenceMissing - reference) - - stableUnique = - reverse . snd - . foldl' - (\(seen, reversed) reference -> - if reference `Set.member` seen - then (seen, reversed) - else - ( Set.insert reference seen - , reference : reversed - )) - (Set.empty, []) - -data TransitionTypedProblemError local - = TransitionTypedProblemGlobalValidationError - !TransitionModuleError - | TransitionTypedProblemUnknownFactAlias - !Marker - | TransitionTypedProblemDependencyNotMigrated - !TransitionFactRef - | TransitionTypedProblemFactReferenceMissing - !TransitionFactRef - | TransitionTypedProblemPlanningError - !(Backend.TypedProblemError - local - CheckedGlobalRef) - deriving stock (Show, Eq) - -beginTransitionDeclaration - :: TransitionModuleBuilder - -> TransitionModuleBuilder -beginTransitionDeclaration - builder = - builder - { builderNextDeclaration = - nextDeclaration + 1 - , builderCurrentDeclaration = - Just - (OpaqueDeclarationRef - (builderName builder) - (localDeclarationOrdinal - nextDeclaration)) - } - where - nextDeclaration = - builderNextDeclaration builder - -transitionCurrentDeclarationReference - :: TransitionModuleBuilder - -> Maybe OpaqueDeclarationRef -transitionCurrentDeclarationReference - builder = - builderCurrentDeclaration builder - -commitTransitionOpaqueGlobal - :: Symbol - -> CoreType - -> Origin - -> TransitionModuleBuilder - -> Either TransitionModuleError TransitionModuleBuilder -commitTransitionOpaqueGlobal - symbol - coreType - bindingOrigin - builder = - commitTransitionGlobal - symbol - coreType - bindingOrigin - Nothing - builder - -commitTransitionTransparentGlobal - :: Symbol - -> CoreType - -> FrozenCheckedCore CheckedGlobalRef - -> Origin - -> TransitionModuleBuilder - -> Either TransitionModuleError TransitionModuleBuilder -commitTransitionTransparentGlobal - symbol - coreType - body - bindingOrigin - builder = do - checkedBody <- - recheckBuilderFrozenCore builder body - unless - (frozenCoreType checkedBody == coreType) - (Left - (TransitionTransparentGlobalTypeMismatch - symbol - coreType - (frozenCoreType checkedBody))) - commitTransitionGlobal - symbol - coreType - bindingOrigin - (Just checkedBody) - builder - -commitTransitionGlobal - :: Symbol - -> CoreType - -> Origin - -> Maybe (FrozenCheckedCore CheckedGlobalRef) - -> TransitionModuleBuilder - -> Either TransitionModuleError TransitionModuleBuilder -commitTransitionGlobal - symbol - coreType - bindingOrigin - body - builder = - case transitionCurrentDeclarationReference builder of - Nothing -> - Left TransitionDeclarationNotOpen - Just reference -> do - let binding = - TypedGlobalBinding - symbol - (CheckedOpaqueGlobal - reference - coreType) - bindingOrigin - body - case Map.lookup symbol - (builderGlobals builder) of - Just previous -> - Left - (globalSymbolConflict - previous - binding) - Nothing -> - pure () - case Map.lookup reference - (builderGlobalDeclarations builder) of - Just previous -> - Left - (globalReferenceConflict - previous - binding) - Nothing -> - pure () - (globals, declarations) <- - insertVisibleGlobalBinding - ( builderGlobals builder - , builderGlobalDeclarations builder - ) - binding - Right - builder - { builderGlobals = globals - , builderGlobalDeclarations = - declarations - , builderLocalGlobalsReversed = - binding - : builderLocalGlobalsReversed - builder - } - -insertTransitionTypedFact - :: NonEmpty Marker - -> Origin - -> TypedAdmittedFact - -> TransitionModuleBuilder - -> Either TransitionModuleError TransitionModuleBuilder -insertTransitionTypedFact aliases factOrigin admitted builder = do - factReference <- - nextTransitionTypedFactReference builder - let ordinal = - builderNextTypedFact builder - reference = - TransitionTypedFactRef - factReference - registration = - TransitionFactRegistration - aliases - factOrigin - entry = - TransitionFactEntry - (TypedFactRow reference admitted) - registration - inventory' <- - insertTransitionFactEntry - entry - (builderFactInventory builder) - Right - builder - { builderLocalFactsReversed = - entry - : builderLocalFactsReversed - builder - , builderFactInventory = inventory' - , builderNextTypedFact = ordinal + 1 - } - -commitTransitionTypedVampireFact - :: BackendReconstruction.ReconstructionPolicy - -> NonEmpty Marker - -> Origin - -> FrozenCheckedCore CheckedGlobalRef - -> Provers.PreparedTypedProverTask - TransitionFactRef - Void - inputOrigin - CheckedGlobalRef - -> Provers.AcceptedVampireRun - -> TransitionModuleBuilder - -> Either TransitionModuleError TransitionModuleBuilder -commitTransitionTypedVampireFact - reconstructionPolicy - aliases - factOrigin - target - preparedTask - accepted - builder = do - semantic <- - prepareTypedSemanticFact builder target - let checkedTarget = - typedSemanticStatement semantic - let problem = - Provers.preparedTypedProverLogicalProblem - preparedTask - claim = - Backend.typedProblemClaim problem - unless - ( Vector.null - (Backend.supportedPropositionSupport - claim) - && Backend.supportedPropositionTerm claim - == frozenCoreTerm checkedTarget - ) - (Left TransitionTypedVampireTargetMismatch) - unless - (Provers.acceptedVampireRequest accepted - == Provers.preparedTypedProverRequest - preparedTask) - (Left TransitionTypedVampireRequestMismatch) - unless - (Vector.null - (Backend.typedProblemLocalPremises - problem)) - (Left TransitionTypedVampireHasOpenLocalPremises) - traverse_ - validateGlobalType - (Map.toList - (Backend.typedProblemGlobalTypes - problem)) - validatedPremises <- - traverse - validateSelectedFact - (Backend.typedProblemGlobalPremises - problem) - foundationTrust <- - foldM - (\tags auxiliary -> - (tags <>) - <$> validateFoundationAuxiliary - auxiliary) - mempty - (Backend.typedProblemAuxiliaries - problem) - let imports = - fst <$> validatedPremises - premiseTrust = - foldMap snd validatedPremises - case BackendReconstruction.attemptVampireReconstruction - reconstructionPolicy - preparedTask - accepted of - BackendReconstruction.ReconstructionSucceeded - reconstructed -> - commitReconstructed - reconstructionPolicy - semantic - premiseTrust - foundationTrust - imports - checkedTarget - reconstructed - BackendReconstruction.ReconstructionUnsupported - unsupported -> - commitTrusted - semantic - premiseTrust - foundationTrust - (ReconstructionFallbackUnsupported - unsupported) - BackendReconstruction.ReconstructionUnavailable - searchStats -> - commitTrusted - semantic - premiseTrust - foundationTrust - (ReconstructionFallbackUnavailable - searchStats) - BackendReconstruction.ReconstructionExhausted - exhaustion - searchStats -> - commitTrusted - semantic - premiseTrust - foundationTrust - (ReconstructionFallbackSearchExhausted - exhaustion - searchStats) - BackendReconstruction.ReconstructionDefinitiveMismatch - mismatch -> - Left - (TransitionTypedReconstructionMismatch - mismatch) - where - commitReconstructed - policy - semantic - premiseTrust - foundationTrust - imports - checkedTarget - reconstructed = do - let connectionReplay = - BackendReconstruction.reconstructedConnectionReplay - reconstructed - provenance = - SessionTypedReconstructionProvenance - policy - (Provers.preparedTypedProverTptpProblem - (BackendReconstruction.reconstructedPreparedTask - reconstructed)) - (BackendReconstruction.reconstructedAcceptedRun - reconstructed) - (BackendReconstruction.reconstructedConnectionTrace - reconstructed) - (BackendReconstruction.reconstructedSearchStats - reconstructed) - (BackendConnection.replayedConnectionNodeCount - connectionReplay) - (BackendConnection.replayedConnectionMaximumDepth - connectionReplay) - case authorizeTransitionKernelFactWithImportsAndProvenance - (BackendReconstruction.reconstructionPolicyKernelReplayLimits - policy) - (Just provenance) - imports - checkedTarget - (BackendConnection.replayedConnectionDerivation - connectionReplay) - builder of - Left - (TransitionKernelReplayError replayError) - | isKernelReplayExhaustion replayError -> - commitTrusted - semantic - premiseTrust - foundationTrust - (ReconstructionFallbackKernelReplayExhausted - replayError) - Left transitionError -> - Left transitionError - Right admitted -> - insertTransitionTypedFact - aliases - factOrigin - admitted - builder - - commitTrusted - semantic - premiseTrust - foundationTrust - fallbackReason = do - factReference <- - nextTransitionTypedFactReference builder - let trust = - premiseTrust - <> mempty - { typedTrustedVampireUses = - Set.singleton - (SessionTypedTrustedVampireUse - factReference) - , typedVampireLoweringUses = - mandatoryVampireLoweringAssumptions - , typedFoundationUses = - foundationTrust - } - admitted = - TypedAdmittedFact - semantic - (TrustedVampire - (SessionTypedTrustedVampireEvidence - factReference - (typedSemanticStatement semantic) - (Provers.preparedTypedProverTptpProblem - preparedTask) - accepted - trust - (SessionTypedReconstructionFallback - reconstructionPolicy - fallbackReason))) - insertTransitionTypedFact - aliases - factOrigin - admitted - builder - - isKernelReplayExhaustion = \case - KernelReplayNodeLimitExceeded{} -> - True - KernelReplayDepthLimitExceeded{} -> - True - _ -> - False - - validateGlobalType (global, reportedType) = do - authoritativeType <- - validateBuilderGlobalReference - builder - global - unless - (authoritativeType == reportedType) - (Left - (TransitionTypedVampireGlobalTypeMismatch - global - reportedType)) - - validateSelectedFact selected = - case lookupBuilderFact reference builder of - Nothing -> - Left - (TransitionTypedVampireFactNotVisible - reference) - Just - (TransitionFactEntry - LegacyFactRow{} - _registration) -> - Left - (TransitionDependencyNotMigrated - reference) - Just - (TransitionFactEntry - (TypedFactRow - rowReference - admitted) - _registration) -> do - semantic <- - prepareTypedSemanticFact - builder - (typedAdmittedStatement - admitted) - let selectedProposition = - Backend.typedBackendFactProposition - selected - selectedCapability = - Backend.typedBackendFactCapability - selected - unless - ( rowReference == reference - && frozenCoreTerm - (typedSemanticStatement - semantic) - == Backend.supportedPropositionTerm - selectedProposition - && typedSemanticFofCapability - semantic - == selectedCapability - ) - (Left - (TransitionTypedVampireFactMismatch - reference)) - typedImport <- - transitionDerivationImport - reference - (typedSemanticStatement - semantic) - pure - ( typedImport - , typedAdmittedTrustDependencies - admitted - ) - where - reference = - Backend.typedBackendFactReference - selected - - validateFoundationAuxiliary auxiliary = do - let tag = - Backend.typedProblemAuxiliaryTag - auxiliary - actual = - Backend.supportedPropositionTerm - (Backend.typedProblemAuxiliaryProposition - auxiliary) - expected = - frozenCoreTerm - (mapFrozenGlobals - absurd - (foundationAxiomFrozen - (builderFoundation builder) - tag)) - unless - (actual == expected) - (Left - (TransitionTypedVampireFoundationMismatch - tag)) - pure (Set.singleton tag) - -nextTransitionTypedFactReference - :: TransitionModuleBuilder - -> Either TransitionModuleError FactRef -nextTransitionTypedFactReference builder = do - void - (maybe - (Left TransitionDeclarationNotOpen) - Right - (transitionCurrentDeclarationReference builder)) - let ordinal = - builderNextTypedFact builder - pure - (FactRef - (builderName builder) - (localFactOrdinal ordinal)) - -commitTransitionTypedDeclaredAssumption - :: NonEmpty Marker - -> Origin - -> AssumptionKind - -> FrozenCheckedCore CheckedGlobalRef - -> TransitionModuleBuilder - -> Either TransitionModuleError TransitionModuleBuilder -commitTransitionTypedDeclaredAssumption - aliases - factOrigin - kind - statement - builder = do - semantic <- - prepareTypedSemanticFact builder statement - factReference <- - nextTransitionTypedFactReference builder - let checkedStatement = - typedSemanticStatement semantic - assumptionOrdinal = - LocalAssumptionOrdinal - (builderNextTypedAssumption builder) - manifestEntry = - TypedDirectAxiomManifestEntry - factReference - kind - checkedStatement - sessionReference = - SessionTypedDeclaredAssumptionRef - factReference - assumptionOrdinal - kind - checkedStatement - admitted = - TypedAdmittedFact - semantic - (DeclaredAssumption - sessionReference) - builder' <- - insertTransitionTypedFact - aliases - factOrigin - admitted - builder - pure - builder' - { builderTypedDirectAxiomManifestReversed = - manifestEntry - : builderTypedDirectAxiomManifestReversed - builder' - , builderNextTypedAssumption = - builderNextTypedAssumption builder + 1 - } - -transitionBuilderWithLegacyStage - :: LegacyModuleStage - -> TransitionModuleBuilder - -> Either TransitionModuleError TransitionModuleBuilder -transitionBuilderWithLegacyStage newStage builder - | legacyStageSourceAddress newStage - /= legacyStageSourceAddress - (builderLegacyStage builder) = - Left TransitionLegacyStageAddressMismatch - | Vector.take oldCount newFacts /= oldFacts = - Left TransitionLegacyStageIsNotAnExtension - | otherwise = do - (reversedFacts, inventory) <- - foldM - appendLegacyEntry - ( builderLocalFactsReversed builder - , builderFactInventory builder - ) - (Vector.toList - (Vector.drop oldCount newFacts)) - Right - builder - { builderLegacyStage = newStage - , builderLocalFactsReversed = - reversedFacts - , builderFactInventory = inventory - } - where - oldFacts = - legacyStageLocalFacts - (builderLegacyStage builder) - oldCount = - Vector.length oldFacts - newFacts = - legacyStageLocalFacts newStage - - appendLegacyEntry (reversedFacts, inventory) legacyEntry = do - let staged = - legacyFactEntryStagedFact legacyEntry - reference = - TransitionLegacyFactRef - (legacyFactEntryReference - legacyEntry) - factOrigin = - originFromLegacyStagedFact staged - entry = - TransitionFactEntry - (LegacyFactRow - reference - (legacyFactEntryAdmittedFact - legacyEntry)) - (TransitionFactRegistration - (Facts.stagedFactAliases staged) - factOrigin) - inventory' <- - insertTransitionFactEntry - entry - inventory - pure (entry : reversedFacts, inventory') - -lookupTransitionGlobal - :: Symbol - -> TransitionModuleBuilder - -> Maybe CheckedGlobalRef -lookupTransitionGlobal symbol builder = - bindingReference - <$> Map.lookup symbol (builderGlobals builder) - where - bindingReference - (TypedGlobalBinding - _symbol - reference - _origin - _body) = - reference - -lookupTransitionGlobalBody - :: Symbol - -> TransitionModuleBuilder - -> Maybe (FrozenCheckedCore CheckedGlobalRef) -lookupTransitionGlobalBody symbol builder = do - TypedGlobalBinding - _bindingSymbol - _reference - _origin - body <- - Map.lookup symbol (builderGlobals builder) - body - - -data TransitionAdmittedModule = TransitionAdmittedModule - { admittedName :: !ModuleName - , admittedLegacyModule :: !LegacyAdmittedModule - , admittedEnvironmentDeltas - :: !(Vector TypedModuleEnvironmentDelta) - , admittedLocalGlobals :: !(Vector TypedGlobalBinding) - , admittedVisibleFacts :: !(Vector TransitionFactEntry) - , admittedTypedDirectAxiomManifest - :: !(Vector TypedDirectAxiomManifestEntry) - } - -sealTransitionModule - :: LegacyCheckingEnvironment - -> TransitionModuleBuilder - -> Either TransitionModuleError TransitionAdmittedModule -sealTransitionModule finalEnvironment builder = do - legacyAdmitted <- - first TransitionLegacyModuleError - (sealLegacyModuleStage - finalEnvironment - (builderLegacyStage builder)) - let localBindings = - Vector.fromList - (reverse - (builderLocalGlobalsReversed - builder)) - localDelta = - TypedModuleEnvironmentDelta - (builderName builder) - localBindings - localFacts = - Vector.fromList - (reverse - (builderLocalFactsReversed - builder)) - visibleFacts = - builderVisibleFacts builder - typedManifest = - Vector.fromList - (reverse - (builderTypedDirectAxiomManifestReversed - builder)) - actualLegacyReferences = - [ reference - | TransitionFactEntry - (LegacyFactRow - (TransitionLegacyFactRef reference) - _admitted) - _registration <- - Vector.toList localFacts - ] - expectedLegacyReferences = - legacyFactEntryReference - <$> Vector.toList - (legacyAdmittedLocalFacts - legacyAdmitted) - unless - (actualLegacyReferences - == expectedLegacyReferences) - (Left TransitionLegacyFactOrderMismatch) - validateTypedDirectAxiomManifest - localFacts - typedManifest - pure - TransitionAdmittedModule - { admittedName = builderName builder - , admittedLegacyModule = legacyAdmitted - , admittedEnvironmentDeltas = - Vector.snoc - (builderEnvironmentDeltas builder) - localDelta - , admittedLocalGlobals = localBindings - , admittedVisibleFacts = visibleFacts - , admittedTypedDirectAxiomManifest = - typedManifest - } - -transitionAdmittedName - :: TransitionAdmittedModule - -> ModuleName -transitionAdmittedName = - admittedName - -transitionAdmittedLegacyModule - :: TransitionAdmittedModule - -> LegacyAdmittedModule -transitionAdmittedLegacyModule = - admittedLegacyModule - -transitionAdmittedFacts - :: TransitionAdmittedModule - -> Vector AdmittedFact -transitionAdmittedFacts = - fmap entryFact . admittedVisibleFacts - where - entryFact - (TransitionFactEntry fact _registration) = - fact - -transitionAdmittedKernelProofCount - :: TransitionAdmittedModule - -> Int -transitionAdmittedKernelProofCount = - Vector.length - . Vector.filter admittedFactIsKernelProof - . transitionAdmittedFacts - -transitionAdmittedTypedTrustedVampireCount - :: TransitionAdmittedModule - -> Int -transitionAdmittedTypedTrustedVampireCount = - Vector.length - . Vector.filter admittedFactIsTrustedVampire - . transitionAdmittedFacts - --- | Replay work retained by the admitted root module's visible fact closure. -data TransitionReplayMeasurements = - TransitionReplayMeasurements - { transitionKernelReplayCount :: !Int - , transitionKernelReplayNodeCount :: !Natural - , transitionKernelReplayMaximumDepth :: !Natural - , transitionReconstructionCount :: !Int - , transitionReconstructionSearchWork :: !Natural - , transitionReconstructionDerivedAtomCount :: !Natural - , transitionReconstructionMaximumCandidateDepth :: !Natural - , transitionConnectionReplayNodeCount :: !Natural - , transitionConnectionReplayMaximumDepth :: !Natural - } - deriving stock (Show, Eq) - -transitionAdmittedReplayMeasurements - :: TransitionAdmittedModule - -> TransitionReplayMeasurements -transitionAdmittedReplayMeasurements = - Vector.foldl' - combineReplayMeasurements - emptyReplayMeasurements - . transitionAdmittedFacts - -emptyReplayMeasurements :: TransitionReplayMeasurements -emptyReplayMeasurements = - TransitionReplayMeasurements - { transitionKernelReplayCount = 0 - , transitionKernelReplayNodeCount = 0 - , transitionKernelReplayMaximumDepth = 0 - , transitionReconstructionCount = 0 - , transitionReconstructionSearchWork = 0 - , transitionReconstructionDerivedAtomCount = 0 - , transitionReconstructionMaximumCandidateDepth = 0 - , transitionConnectionReplayNodeCount = 0 - , transitionConnectionReplayMaximumDepth = 0 - } - -combineReplayMeasurements - :: TransitionReplayMeasurements - -> AdmittedFact - -> TransitionReplayMeasurements -combineReplayMeasurements measurements = \case - LegacyFactRow{} -> - measurements - TypedFactRow _reference - (TypedAdmittedFact _semantic authorization) -> - case authorization of - KernelProof - (AuthorizedKernelReplay - _target - _imports - _foundation - _rules - nodes - depth - provenance) - _trust -> - combineReconstructionMeasurements - provenance - measurements - { transitionKernelReplayCount = - transitionKernelReplayCount measurements - + 1 - , transitionKernelReplayNodeCount = - transitionKernelReplayNodeCount measurements - + nodes - , transitionKernelReplayMaximumDepth = - max - (transitionKernelReplayMaximumDepth - measurements) - depth - } - DeclaredAssumption{} -> - measurements - TrustedVampire{} -> - measurements - -combineReconstructionMeasurements - :: Maybe SessionTypedReconstructionProvenance - -> TransitionReplayMeasurements - -> TransitionReplayMeasurements -combineReconstructionMeasurements Nothing measurements = - measurements -combineReconstructionMeasurements - (Just - (SessionTypedReconstructionProvenance - _policy - _prepared - _accepted - _trace - searchStats - replayNodes - replayDepth)) - measurements = - measurements - { transitionReconstructionCount = - transitionReconstructionCount measurements - + 1 - , transitionReconstructionSearchWork = - transitionReconstructionSearchWork measurements - + BackendConnection.connectionSearchWork searchStats - , transitionReconstructionDerivedAtomCount = - transitionReconstructionDerivedAtomCount measurements - + BackendConnection.connectionSearchDerivedAtomCount - searchStats - , transitionReconstructionMaximumCandidateDepth = - max - (transitionReconstructionMaximumCandidateDepth - measurements) - (BackendConnection.connectionSearchMaximumCandidateDepth - searchStats) - , transitionConnectionReplayNodeCount = - transitionConnectionReplayNodeCount measurements - + replayNodes - , transitionConnectionReplayMaximumDepth = - max - (transitionConnectionReplayMaximumDepth - measurements) - replayDepth - } - -transitionAdmittedTypedDirectAxiomManifest - :: TransitionAdmittedModule - -> Vector TypedDirectAxiomManifestEntry -transitionAdmittedTypedDirectAxiomManifest = - admittedTypedDirectAxiomManifest - -transitionAdmittedTypedTrustDependencies - :: TransitionAdmittedModule - -> TypedTrustDependencies -transitionAdmittedTypedTrustDependencies = - foldMap - (fromMaybe mempty - . admittedFactTypedTrustDependencies) - . transitionAdmittedFacts - -transitionAdmittedGlobals - :: TransitionAdmittedModule - -> Vector (Symbol, CheckedGlobalRef, Origin) -transitionAdmittedGlobals admitted = - fmap - (\(TypedGlobalBinding - symbol - reference - bindingOrigin - _body) -> - (symbol, reference, bindingOrigin)) - (admittedLocalGlobals admitted) - -validateTypedDirectAxiomManifest - :: Vector TransitionFactEntry - -> Vector TypedDirectAxiomManifestEntry - -> Either TransitionModuleError () -validateTypedDirectAxiomManifest localFacts manifest = - unless - (actual == expected) - (Left TransitionTypedDirectAxiomManifestMismatch) - where - actual = - [ ( reference - , ordinal - , kind - , statement - ) - | TransitionFactEntry - (TypedFactRow - (TransitionTypedFactRef reference) - (TypedAdmittedFact - semantic - (DeclaredAssumption - sessionReference))) - _registration <- - Vector.toList localFacts - , let ordinal = - sessionTypedAssumptionOrdinal - sessionReference - kind = - sessionTypedAssumptionKind - sessionReference - statement = - typedSemanticStatement semantic - , sessionTypedAssumptionFact sessionReference - == reference - , sessionTypedAssumptionStatement sessionReference - == statement - ] - expected = - [ ( typedDirectAssumptionFact entry - , LocalAssumptionOrdinal ordinal - , typedDirectAssumptionKind entry - , typedDirectAssumptionStatement entry - ) - | (ordinal, entry) <- - zip [0 ..] (Vector.toList manifest) - ] - -insertVisibleGlobalBinding - :: ( Map Symbol TypedGlobalBinding - , Map OpaqueDeclarationRef TypedGlobalBinding - ) - -> TypedGlobalBinding - -> Either - TransitionModuleError - ( Map Symbol TypedGlobalBinding - , Map OpaqueDeclarationRef TypedGlobalBinding - ) -insertVisibleGlobalBinding - (globals, declarations) - binding@(TypedGlobalBinding - symbol - reference - _bindingOrigin - _body) = do - globals' <- - case Map.lookup symbol globals of - Nothing -> - Right (Map.insert symbol binding globals) - Just previous@(TypedGlobalBinding - _previousSymbol - _previousReference - _previousOrigin - _previousBody) - | previous == binding -> - Right globals - | otherwise -> - Left - (globalSymbolConflict - previous - binding) - declarations' <- - case Map.lookup declaration declarations of - Nothing -> - Right - (Map.insert - declaration - binding - declarations) - Just previous - | previous == binding -> - Right declarations - | otherwise -> - Left - (globalReferenceConflict - previous - binding) - pure (globals', declarations') - where - declaration = - checkedGlobalReference reference - -globalSymbolConflict - :: TypedGlobalBinding - -> TypedGlobalBinding - -> TransitionModuleError -globalSymbolConflict - (TypedGlobalBinding - previousSymbol - previousReference - previousOrigin - _previousBody) - (TypedGlobalBinding - _incomingSymbol - incomingReference - incomingOrigin - _incomingBody) = - TransitionGlobalConflict - previousSymbol - previousReference - previousOrigin - incomingReference - incomingOrigin - -globalReferenceConflict - :: TypedGlobalBinding - -> TypedGlobalBinding - -> TransitionModuleError -globalReferenceConflict - (TypedGlobalBinding - previousSymbol - previousReference - previousOrigin - _previousBody) - (TypedGlobalBinding - incomingSymbol - incomingReference - incomingOrigin - _incomingBody) = - TransitionGlobalReferenceConflict - (checkedGlobalReference incomingReference) - previousSymbol - (checkedGlobalType previousReference) - previousOrigin - incomingSymbol - (checkedGlobalType incomingReference) - incomingOrigin - - -mergeTypedEnvironments - :: [TransitionAdmittedModule] - -> Either - TransitionModuleError - ( Vector TypedModuleEnvironmentDelta - , Map Symbol TypedGlobalBinding - , Map OpaqueDeclarationRef TypedGlobalBinding - ) -mergeTypedEnvironments directImports = do - (_deltasByModule, reversedDeltas) <- - foldM - importModule - (Map.empty, []) - directImports - (globals, globalDeclarations) <- - foldM - applyDelta - (Map.empty, Map.empty) - (reverse reversedDeltas) - pure - ( Vector.fromList (reverse reversedDeltas) - , globals - , globalDeclarations - ) - where - importModule imported admitted = - foldM - importDelta - imported - (moduleEnvironmentDeltas admitted) - - moduleEnvironmentDeltas - admitted = - toList (admittedEnvironmentDeltas admitted) - - importDelta - current@(byModule, reversedDeltas) - delta@(TypedModuleEnvironmentDelta name _bindings) = - case Map.lookup name byModule of - Nothing -> - Right - ( Map.insert name delta byModule - , delta : reversedDeltas - ) - Just previous - | previous == delta -> - Right current - | otherwise -> - Left - (TransitionImportedModuleConflict - name) - - applyDelta environment - (TypedModuleEnvironmentDelta _name bindings) = - foldM insertVisibleGlobalBinding environment bindings - -mergeTransitionFacts - :: [TransitionAdmittedModule] - -> Either - TransitionModuleError - TransitionFactInventory -mergeTransitionFacts = - foldM importModule emptyTransitionFactInventory - where - importModule inventory admitted = - foldM - (flip insertTransitionFactEntry) - inventory - (Vector.toList - (admittedVisibleFacts admitted)) - -insertFactAliases - :: TransitionFactRef - -> Origin - -> NonEmpty Marker - -> Map Marker (TransitionFactRef, Origin) - -> Either - TransitionModuleError - (Map Marker (TransitionFactRef, Origin)) -insertFactAliases reference factOrigin aliases initial = - foldM insertAlias initial aliases - where - insertAlias current alias = - case Map.lookup alias current of - Nothing -> - Right - (Map.insert - alias - (reference, factOrigin) - current) - Just (previousReference, previousOrigin) - | previousReference == reference -> - Right current - | otherwise -> - Left - (TransitionFactAliasConflict - alias - previousReference - previousOrigin - reference - factOrigin) - -originFromLegacyStagedFact - :: Facts.StagedFact - -> Origin -originFromLegacyStagedFact staged = - Origin - (Facts.factOriginLocation factOrigin) - Nothing - (Just (Facts.factOriginBlock factOrigin)) - where - factOrigin = - Facts.stagedFactOrigin staged - - -data TransitionModuleError - = TransitionLegacyModuleError - !LegacyModuleStageError - | TransitionLegacyStageAddressMismatch - | TransitionLegacyStageIsNotAnExtension - | TransitionLegacyFactOrderMismatch - | TransitionDeclarationNotOpen - | TransitionImportedModuleConflict - !ModuleName - | TransitionGlobalConflict - !Symbol - !CheckedGlobalRef - !Origin - !CheckedGlobalRef - !Origin - | TransitionGlobalReferenceConflict - !OpaqueDeclarationRef - !Symbol - !CoreType - !Origin - !Symbol - !CoreType - !Origin - | TransitionGlobalReferenceNotVisible - !CheckedGlobalRef - | TransitionGlobalReferenceTypeMismatch - !CheckedGlobalRef - !CoreType - | TransitionCoreCheckError - !CoreCheckError - | TransitionTransparentGlobalTypeMismatch - !Symbol - !CoreType - !CoreType - | TransitionTypedFactIsNotProposition - !CoreType - | TransitionTypedFactSupportError - !(Backend.SupportedPropositionError Void) - | TransitionTypedFactClassificationError - !(Backend.BackendClassificationError - CheckedGlobalRef) - | TransitionTypedVampireTargetMismatch - | TransitionTypedVampireRequestMismatch - | TransitionTypedVampireHasOpenLocalPremises - | TransitionTypedVampireGlobalTypeMismatch - !CheckedGlobalRef - !CoreType - | TransitionTypedVampireFactNotVisible - !TransitionFactRef - | TransitionTypedVampireFactMismatch - !TransitionFactRef - | TransitionTypedVampireFoundationMismatch - !FoundationAxiomTag - | TransitionTypedReconstructionMismatch - !BackendReconstruction.ReconstructionMismatch - | TransitionKernelTargetMismatch - | TransitionKernelReplayError - !KernelReplayError - | TransitionDerivationImportError - !DerivationImportError - | TransitionKernelImportIndexOutOfBounds - !ImportIx - | TransitionKernelImportNotVisible - !TransitionFactRef - | TransitionKernelImportDoesNotMatch - !TransitionFactRef - | TransitionDependencyNotMigrated - !TransitionFactRef - | TransitionTypedDirectAxiomManifestMismatch - | TransitionFactReferenceConflict - !TransitionFactRef - | TransitionFactAliasConflict - !Marker - !TransitionFactRef - !Origin - !TransitionFactRef - !Origin - deriving stock (Show, Eq) |