diff options
Diffstat (limited to 'source/Checking/Legacy.hs')
| -rw-r--r-- | source/Checking/Legacy.hs | 1788 |
1 files changed, 0 insertions, 1788 deletions
diff --git a/source/Checking/Legacy.hs b/source/Checking/Legacy.hs deleted file mode 100644 index 7c7bbb4..0000000 --- a/source/Checking/Legacy.hs +++ /dev/null @@ -1,1788 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Disposable H1 vocabulary for the legacy checker. --- --- These values exist only for one checking invocation. They are neither final --- typed identities nor persistent authorization. -module Checking.Legacy - ( LegacyModuleOrdinal - , legacyModuleOrdinal - , legacyModuleOrdinalValue - , LegacyLocalFactOrdinal - , legacyLocalFactOrdinal - , legacyLocalFactOrdinalValue - , LegacyFactRef - , legacyFactRef - , legacyFactModule - , legacyFactLocalOrdinal - , LegacyModuleAssignment - , assignLegacyModuleOrdinals - , assignedLegacyModuleOrdinal - , assignedParsedModule - , LegacyLocalAssumptionOrdinal - , legacyLocalAssumptionOrdinal - , legacyLocalAssumptionOrdinalValue - , LegacyObligationOrdinal - , legacyObligationOrdinal - , legacyObligationOrdinalValue - , SessionLegacyObligationRef - , sessionLegacyObligationRef - , AssumptionKind(..) - , LegacyPreparedProposition - , prepareLegacyProposition - , legacyPreparedFormula - , LegacyDirectAxiomManifestEntry - , SessionLegacyDeclaredAssumptionRef - , LegacySemanticFact - , legacySemanticFact - , legacySemanticProposition - , LegacyTheoremFinalizationRole(..) - , LegacyDefinitionFactRole(..) - , LegacyDatatypeFactRole(..) - , LegacyStructureFactRole(..) - , LegacyInductiveFactRole(..) - , LegacyRuleTag(..) - , LegacyFactProducer(..) - , LegacyRulePredecessor - , legacyRuleFactPredecessor - , legacyRuleObligationPredecessor - , CheckedLegacyRuleApplication - , VampireLoweringAssumption(..) - , mandatoryVampireLoweringAssumptions - , SessionLegacyTrustedVampireUse - , SessionLegacyGapUse - , SessionLegacyRuleUse - , LegacyTrustDependencies - , emptyLegacyTrustDependencies - , legacyTrustedVampireTrust - , legacyGapTrust - , legacyDeclaredAssumptionUses - , legacyTrustedVampireUses - , legacyExplicitGaps - , legacyGapLocations - , trustedLegacyRuleUses - , legacyVampireLoweringUses - , SessionLegacyTrustedVampireEvidence - , SessionLegacyGapEvidence - , LegacyFactAuthorization - , legacyAuthorizationTrustDependencies - , H1LegacyFactAuthorization - , LegacyAdmittedFact - , H1LegacyAdmittedFact - , SymbolOwnerKind(..) - , SymbolOwner(..) - , LegacyCheckingEnvironment - , legacyCheckingEnvironment - , legacyEnvironmentAbbreviations - , legacyEnvironmentPredicateDefinitions - , legacyEnvironmentDependencies - , legacyEnvironmentOwnedSymbols - , legacyEnvironmentOwnedSymbolMarkers - , legacyEnvironmentFrozenSymbols - , legacyEnvironmentStructs - , legacyEnvironmentDefinedMarkers - , LegacyImportedView - , emptyLegacyImportedView - , legacyImportedView - , legacyImportedModuleOrdinals - , legacyImportedCheckingEnvironment - , LegacyModuleStage - , openLegacyModuleStage - , legacyStageModuleOrdinal - , legacyStageSourceAddress - , legacyStageVisibleFacts - , legacyStageLocalFacts - , legacyStageFactRegistry - , legacyStageDirectAxiomManifest - , legacyStageImportedCheckingEnvironment - , lookupLegacyStageFact - , LegacyFactEntry - , legacyFactEntryReference - , legacyFactEntryStagedFact - , legacyFactEntryAdmittedFact - , legacyFactEntryTrustDependencies - , LegacyReservedFact - , legacyReservedFactReference - , legacyReservedStagedFact - , LegacyDeclarationReservation - , reserveLegacyDeclaration - , legacyReservedFacts - , appendEstablishedLegacyDeclaration - , authorizeLegacyDeclaredAssumption - , authorizeLegacyTrustedVampire - , authorizeLegacyGap - , authorizeLegacyRule - , LegacyAdmittedModule - , sealLegacyModuleStage - , legacyAdmittedModuleOrdinal - , legacyAdmittedSourceAddress - , legacyAdmittedDirectImports - , legacyAdmittedVisibleFacts - , legacyAdmittedLocalFacts - , legacyAdmittedFactRegistry - , legacyAdmittedDirectAxiomManifest - , legacyAdmittedTrustDependencies - , legacyAdmittedCheckingEnvironment - , LegacyModuleStageError(..) - ) where - -import Base -import Checking.Facts qualified as Facts -import Checking.Legacy.Environment -import Felix.Parse - ( ParsedModule - , ParsedSourceWorkspace - , parsedModuleAddress - , parsedWorkspaceImportedBeforeImporter - ) -import Felix.Source (ResolvedSourceAddress) -import Provers (AcceptedVampireRun) -import Report.Location -import Syntax.Internal - -import Control.Monad (foldM, unless) -import Data.Bifunctor (first) -import Data.List.NonEmpty qualified as NonEmpty -import Data.Map.Strict qualified as Map -import Data.Set qualified as Set -import Data.Vector (Vector) -import Data.Vector qualified as Vector -import Data.Word (Word32) -import Numeric.Natural (Natural) - - --- | Dense invocation-local module position. -newtype LegacyModuleOrdinal = LegacyModuleOrdinal Word32 - deriving stock (Show, Eq, Ord) - -legacyModuleOrdinal :: Word32 -> LegacyModuleOrdinal -legacyModuleOrdinal = LegacyModuleOrdinal - -legacyModuleOrdinalValue :: LegacyModuleOrdinal -> Word32 -legacyModuleOrdinalValue (LegacyModuleOrdinal ordinal) = - ordinal - - --- | Dense invocation-local fact position within one module. -newtype LegacyLocalFactOrdinal = LegacyLocalFactOrdinal Word32 - deriving stock (Show, Eq, Ord) - -legacyLocalFactOrdinal :: Word32 -> LegacyLocalFactOrdinal -legacyLocalFactOrdinal = LegacyLocalFactOrdinal - -legacyLocalFactOrdinalValue :: LegacyLocalFactOrdinal -> Word32 -legacyLocalFactOrdinalValue (LegacyLocalFactOrdinal ordinal) = - ordinal - - -data LegacyFactRef = LegacyFactRef - !LegacyModuleOrdinal - !LegacyLocalFactOrdinal - deriving stock (Show, Eq, Ord) - -legacyFactRef - :: LegacyModuleOrdinal - -> LegacyLocalFactOrdinal - -> LegacyFactRef -legacyFactRef = LegacyFactRef - -legacyFactModule :: LegacyFactRef -> LegacyModuleOrdinal -legacyFactModule (LegacyFactRef moduleOrdinal _factOrdinal) = - moduleOrdinal - -legacyFactLocalOrdinal :: LegacyFactRef -> LegacyLocalFactOrdinal -legacyFactLocalOrdinal (LegacyFactRef _moduleOrdinal factOrdinal) = - factOrdinal - - --- | One parsed module paired with its dense invocation-local position. -data LegacyModuleAssignment = LegacyModuleAssignment - !LegacyModuleOrdinal - !ParsedModule - -assignedLegacyModuleOrdinal - :: LegacyModuleAssignment - -> LegacyModuleOrdinal -assignedLegacyModuleOrdinal - (LegacyModuleAssignment ordinal _parsedModule) = - ordinal - -assignedParsedModule :: LegacyModuleAssignment -> ParsedModule -assignedParsedModule - (LegacyModuleAssignment _ordinal parsedModule) = - parsedModule - --- | Assign module ordinals in imported-before-importer source order. -assignLegacyModuleOrdinals - :: ParsedSourceWorkspace - -> Either LegacyModuleStageError (NonEmpty LegacyModuleAssignment) -assignLegacyModuleOrdinals workspace - | moduleCountInteger > legacyModuleCapacity = - Left - (LegacyModuleOrdinalSpaceExhausted - (fromIntegral moduleCount)) - | otherwise = - Right - (NonEmpty.zipWith - (\ordinal parsedModule -> - LegacyModuleAssignment - (legacyModuleOrdinal - (fromIntegral ordinal)) - parsedModule) - ((0 :| [1 ..]) :: NonEmpty Integer) - modules) - where - modules = - parsedWorkspaceImportedBeforeImporter workspace - parsedModules = - NonEmpty.toList modules - moduleCount = - length parsedModules - moduleCountInteger = - toInteger moduleCount - legacyModuleCapacity = - toInteger (maxBound :: Word32) + 1 - - -newtype LegacyLocalAssumptionOrdinal = - LegacyLocalAssumptionOrdinal Natural - deriving stock (Show, Eq, Ord) - -legacyLocalAssumptionOrdinal - :: Natural - -> LegacyLocalAssumptionOrdinal -legacyLocalAssumptionOrdinal = LegacyLocalAssumptionOrdinal - -legacyLocalAssumptionOrdinalValue - :: LegacyLocalAssumptionOrdinal - -> Natural -legacyLocalAssumptionOrdinalValue - (LegacyLocalAssumptionOrdinal ordinal) = - ordinal - - --- | Position of one goal among all batches emitted by one declaration. -newtype LegacyObligationOrdinal = LegacyObligationOrdinal Natural - deriving stock (Show, Eq, Ord) - -legacyObligationOrdinal :: Natural -> LegacyObligationOrdinal -legacyObligationOrdinal = LegacyObligationOrdinal - -legacyObligationOrdinalValue :: LegacyObligationOrdinal -> Natural -legacyObligationOrdinalValue (LegacyObligationOrdinal ordinal) = - ordinal - - --- | Session identity assigned after M3a supplies the owning module. -data SessionLegacyObligationRef = SessionLegacyObligationRef - !LegacyModuleOrdinal - !Marker - !LegacyObligationOrdinal - deriving stock (Show, Eq, Ord) - -sessionLegacyObligationRef - :: LegacyModuleOrdinal - -> Marker - -> LegacyObligationOrdinal - -> SessionLegacyObligationRef -sessionLegacyObligationRef = - SessionLegacyObligationRef - - -data AssumptionKind - = DeclaredUserAxiom - | OpaqueAssumption - deriving stock (Show, Eq, Ord) - - --- | Canonical H0 proposition. This makes no typed-core claim. -newtype LegacyPreparedProposition = - LegacyPreparedProposition Formula - deriving stock (Show, Eq, Ord) - -prepareLegacyProposition - :: Facts.PreparedSemanticFact - -> LegacyPreparedProposition -prepareLegacyProposition = - LegacyPreparedProposition . Facts.preparedSemanticStatement - -legacyPreparedFormula :: LegacyPreparedProposition -> Formula -legacyPreparedFormula (LegacyPreparedProposition formula) = - formula - - -data LegacyDirectAxiomManifestEntry = LegacyDirectAxiomManifestEntry - { legacyDirectAssumptionFact :: !LegacyFactRef - , legacyDirectAssumptionKind :: !AssumptionKind - , legacyDirectAssumptionStatement :: !LegacyPreparedProposition - } - deriving stock (Show, Eq, Ord) - - -data SessionLegacyDeclaredAssumptionRef = - SessionLegacyDeclaredAssumptionRef - !LegacyFactRef - !LegacyLocalAssumptionOrdinal - !AssumptionKind - !LegacyPreparedProposition - deriving stock (Show, Eq, Ord) - - -newtype LegacySemanticFact = - LegacySemanticFact LegacyPreparedProposition - deriving stock (Show, Eq, Ord) - -legacySemanticFact :: LegacyPreparedProposition -> LegacySemanticFact -legacySemanticFact = LegacySemanticFact - -legacySemanticProposition - :: LegacySemanticFact - -> LegacyPreparedProposition -legacySemanticProposition (LegacySemanticFact proposition) = - proposition - - -data LegacyTheoremFinalizationRole - = LegacyOrdinaryTheoremFinalization - deriving stock (Show, Eq, Ord) - -data LegacyDefinitionFactRole - = LegacyDefinitionEquation - deriving stock (Show, Eq, Ord) - -data LegacyDatatypeFactRole - = LegacyDatatypeIntroduction - | LegacyDatatypeDistinctness - | LegacyDatatypeInjectivity - | LegacyDatatypeCases - | LegacyDatatypeInduction - deriving stock (Show, Eq, Ord) - -data LegacyStructureFactRole - = LegacyStructureIntroduction - | LegacyStructureInheritance - | LegacyStructureAssumption - deriving stock (Show, Eq, Ord) - -data LegacyInductiveFactRole - = LegacyInductiveIntroduction - | LegacyInductiveDomainSubset - | LegacyInductiveCases - | LegacyInductiveInduction - deriving stock (Show, Eq, Ord) - -data LegacyRuleTag - = LegacyTheoremRule !LegacyTheoremFinalizationRole - | LegacyDefinitionRule !LegacyDefinitionFactRole - | LegacyDatatypeRule !LegacyDatatypeFactRole - | LegacyStructureRule !LegacyStructureFactRole - | LegacyInductiveRule !LegacyInductiveFactRole - deriving stock (Show, Eq, Ord) - --- | Complete authorization choice for every current legacy fact publisher. -data LegacyFactProducer - = LegacyDeclaredAssumptionProducer !AssumptionKind - | LegacyDirectObligationProducer - | LegacyDeclarationRuleProducer !LegacyRuleTag - deriving stock (Show, Eq, Ord) - - -data LegacyRulePredecessor ref - = LegacyRuleFactPredecessor !ref - | LegacyRuleObligationPredecessor !SessionLegacyObligationRef - deriving stock (Show, Eq, Ord) - -legacyRuleFactPredecessor - :: ref - -> LegacyRulePredecessor ref -legacyRuleFactPredecessor = - LegacyRuleFactPredecessor - -legacyRuleObligationPredecessor - :: SessionLegacyObligationRef - -> LegacyRulePredecessor ref -legacyRuleObligationPredecessor = - LegacyRuleObligationPredecessor - -data CheckedLegacyRuleApplication ref trust = - CheckedLegacyRuleApplication - { checkedLegacyRuleTag :: !LegacyRuleTag - , checkedLegacyRuleTarget :: !LegacyPreparedProposition - , checkedLegacyPredecessors - :: !(Vector (LegacyRulePredecessor ref)) - , checkedLegacyTrustSummary :: !trust - } - deriving stock (Show, Eq) - - -data VampireLoweringAssumption - = VampireUsesDoubleNegationElim - | VampireUsesPropositionalExtensionality - deriving stock (Show, Eq, Ord) - -mandatoryVampireLoweringAssumptions - :: Set VampireLoweringAssumption -mandatoryVampireLoweringAssumptions = - Set.fromList - [ VampireUsesDoubleNegationElim - , VampireUsesPropositionalExtensionality - ] - - -newtype SessionLegacyTrustedVampireUse = - SessionLegacyTrustedVampireUse SessionLegacyObligationRef - deriving stock (Show, Eq, Ord) - -data SessionLegacyGapUse = SessionLegacyGapUse - !SessionLegacyObligationRef - !Location - !Marker - deriving stock (Show, Eq, Ord) - -data SessionLegacyRuleUse = SessionLegacyRuleUse - !LegacyFactRef - !LegacyRuleTag - deriving stock (Show, Eq, Ord) - - -data LegacyTrustDependencies = LegacyTrustDependencies - { legacyDeclaredAssumptionUses - :: !(Set SessionLegacyDeclaredAssumptionRef) - , legacyTrustedVampireUses - :: !(Set SessionLegacyTrustedVampireUse) - , legacyExplicitGaps - :: !(Set SessionLegacyGapUse) - , trustedLegacyRuleUses - :: !(Set SessionLegacyRuleUse) - , legacyVampireLoweringUses - :: !(Set VampireLoweringAssumption) - } - deriving stock (Show, Eq) - -emptyLegacyTrustDependencies :: LegacyTrustDependencies -emptyLegacyTrustDependencies = - LegacyTrustDependencies - { legacyDeclaredAssumptionUses = mempty - , legacyTrustedVampireUses = mempty - , legacyExplicitGaps = mempty - , trustedLegacyRuleUses = mempty - , legacyVampireLoweringUses = mempty - } - -legacyTrustedVampireTrust - :: SessionLegacyObligationRef - -> LegacyTrustDependencies - -> LegacyTrustDependencies -legacyTrustedVampireTrust obligation predecessorTrust = - predecessorTrust - <> mempty - { legacyTrustedVampireUses = - Set.singleton - (SessionLegacyTrustedVampireUse obligation) - , legacyVampireLoweringUses = - mandatoryVampireLoweringAssumptions - } - -legacyGapTrust - :: SessionLegacyObligationRef - -> Location - -> Marker - -> LegacyTrustDependencies - -> LegacyTrustDependencies -legacyGapTrust obligation location marker predecessorTrust = - predecessorTrust - <> mempty - { legacyExplicitGaps = - Set.singleton - (SessionLegacyGapUse - obligation - location - marker) - } - -legacyGapLocations - :: LegacyTrustDependencies - -> [Location] -legacyGapLocations trust = - [ location - | SessionLegacyGapUse - _obligation - location - _marker <- - Set.toList (legacyExplicitGaps trust) - ] - -instance Semigroup LegacyTrustDependencies where - left <> right = - LegacyTrustDependencies - { legacyDeclaredAssumptionUses = - legacyDeclaredAssumptionUses left - <> legacyDeclaredAssumptionUses right - , legacyTrustedVampireUses = - legacyTrustedVampireUses left - <> legacyTrustedVampireUses right - , legacyExplicitGaps = - legacyExplicitGaps left - <> legacyExplicitGaps right - , trustedLegacyRuleUses = - trustedLegacyRuleUses left - <> trustedLegacyRuleUses right - , legacyVampireLoweringUses = - legacyVampireLoweringUses left - <> legacyVampireLoweringUses right - } - -instance Monoid LegacyTrustDependencies where - mempty = emptyLegacyTrustDependencies - - -data SessionLegacyTrustedVampireEvidence trust = - SessionLegacyTrustedVampireEvidence - !SessionLegacyObligationRef - !LegacyPreparedProposition - !AcceptedVampireRun - !trust - deriving stock (Eq) - -data SessionLegacyGapEvidence trust = SessionLegacyGapEvidence - !SessionLegacyObligationRef - !LegacyPreparedProposition - !Location - !Marker - !trust - deriving stock (Show, Eq) - - -data LegacyFactAuthorization ref trust - = LegacyDeclaredAssumption !SessionLegacyDeclaredAssumptionRef - | LegacyTrustedVampire - !(SessionLegacyTrustedVampireEvidence trust) - | LegacyGap !(SessionLegacyGapEvidence trust) - | TrustedLegacyDeclarationRule - !(CheckedLegacyRuleApplication ref trust) - deriving stock (Eq) - -type H1LegacyFactAuthorization = - LegacyFactAuthorization LegacyFactRef LegacyTrustDependencies - -legacyAuthorizationTrustDependencies - :: H1LegacyFactAuthorization - -> LegacyTrustDependencies -legacyAuthorizationTrustDependencies = \case - LegacyDeclaredAssumption reference -> - mempty - { legacyDeclaredAssumptionUses = - Set.singleton reference - } - LegacyTrustedVampire - (SessionLegacyTrustedVampireEvidence - _obligation - _proposition - _run - trust) -> - trust - LegacyGap - (SessionLegacyGapEvidence - _obligation - _proposition - _location - _marker - trust) -> - trust - TrustedLegacyDeclarationRule application -> - checkedLegacyTrustSummary application - - -data LegacyAdmittedFact ref trust = LegacyAdmittedFact - !LegacySemanticFact - !(LegacyFactAuthorization ref trust) - deriving stock (Eq) - -type H1LegacyAdmittedFact = - LegacyAdmittedFact LegacyFactRef LegacyTrustDependencies - - --- | One established fact and its invocation-local registration sidecar. -data LegacyFactEntry = LegacyFactEntry - !LegacyFactRef - !Facts.StagedFact - !H1LegacyAdmittedFact - deriving stock (Eq) - -legacyFactEntryReference :: LegacyFactEntry -> LegacyFactRef -legacyFactEntryReference - (LegacyFactEntry reference _staged _admitted) = - reference - -legacyFactEntryStagedFact :: LegacyFactEntry -> Facts.StagedFact -legacyFactEntryStagedFact - (LegacyFactEntry _reference staged _admitted) = - staged - -legacyFactEntryAdmittedFact - :: LegacyFactEntry - -> H1LegacyAdmittedFact -legacyFactEntryAdmittedFact - (LegacyFactEntry _reference _staged admitted) = - admitted - -legacyFactEntryTrustDependencies - :: LegacyFactEntry - -> LegacyTrustDependencies -legacyFactEntryTrustDependencies = - legacyAuthorizationTrustDependencies - . admittedAuthorization - . legacyFactEntryAdmittedFact - where - admittedAuthorization - (LegacyAdmittedFact _semantic authorization) = - authorization - - --- M3b is the only producer of a nonempty imported view. -data LegacyImportedView = LegacyImportedView - !(Vector LegacyModuleOrdinal) - !(Vector LegacyFactEntry) - !(Map Marker LegacyFactRef) - !Facts.FactRegistry - !(Vector LegacyModuleEnvironmentDelta) - !LegacyCheckingEnvironment - -emptyLegacyImportedView - :: LegacyCheckingEnvironment - -> LegacyImportedView -emptyLegacyImportedView foundation = - LegacyImportedView - Vector.empty - Vector.empty - Map.empty - Facts.emptyFactRegistry - Vector.empty - foundation - -legacyImportedModuleOrdinals - :: LegacyImportedView - -> Vector LegacyModuleOrdinal -legacyImportedModuleOrdinals - (LegacyImportedView - moduleOrdinals - _facts - _aliases - _registry - _environmentDeltas - _environment) = - moduleOrdinals - -legacyImportedCheckingEnvironment - :: LegacyImportedView - -> LegacyCheckingEnvironment -legacyImportedCheckingEnvironment - (LegacyImportedView - _moduleOrdinals - _facts - _aliases - _registry - _environmentDeltas - environment) = - environment - - --- | Private builder for one legacy module in the current invocation. -data LegacyModuleStage = LegacyModuleStage - !LegacyModuleOrdinal - !ResolvedSourceAddress - !LegacyImportedView - !(Vector LegacyFactEntry) - !(Map Marker LegacyFactRef) - !Facts.FactRegistry - !(Vector LegacyDirectAxiomManifestEntry) - -openLegacyModuleStage - :: LegacyModuleAssignment - -> LegacyImportedView - -> LegacyModuleStage -openLegacyModuleStage assignment imported = - LegacyModuleStage - (assignedLegacyModuleOrdinal assignment) - (parsedModuleAddress - (assignedParsedModule assignment)) - imported - Vector.empty - Map.empty - importedRegistry - Vector.empty - where - LegacyImportedView - _moduleOrdinals - _importedFacts - _importedAliases - importedRegistry - _environmentDeltas - _environment = - imported - -legacyStageModuleOrdinal - :: LegacyModuleStage - -> LegacyModuleOrdinal -legacyStageModuleOrdinal - (LegacyModuleStage - ordinal - _address - _imported - _localFacts - _localAliases - _registry - _manifest) = - ordinal - -legacyStageSourceAddress - :: LegacyModuleStage - -> ResolvedSourceAddress -legacyStageSourceAddress - (LegacyModuleStage - _ordinal - address - _imported - _localFacts - _localAliases - _registry - _manifest) = - address - -legacyStageVisibleFacts - :: LegacyModuleStage - -> Vector LegacyFactEntry -legacyStageVisibleFacts stage = - importedFacts <> legacyStageLocalFacts stage - where - LegacyModuleStage - _ordinal - _address - (LegacyImportedView - _moduleOrdinals - importedFacts - _importedAliases - _importedRegistry - _environmentDeltas - _environment) - _localFacts - _localAliases - _stageRegistry - _manifest = - stage - -legacyStageLocalFacts - :: LegacyModuleStage - -> Vector LegacyFactEntry -legacyStageLocalFacts - (LegacyModuleStage - _ordinal - _address - _imported - localFacts - _localAliases - _registry - _manifest) = - localFacts - -legacyStageFactRegistry :: LegacyModuleStage -> Facts.FactRegistry -legacyStageFactRegistry - (LegacyModuleStage - _ordinal - _address - _imported - _localFacts - _localAliases - registry - _manifest) = - registry - -legacyStageDirectAxiomManifest - :: LegacyModuleStage - -> Vector LegacyDirectAxiomManifestEntry -legacyStageDirectAxiomManifest - (LegacyModuleStage - _ordinal - _address - _imported - _localFacts - _localAliases - _registry - manifest) = - manifest - -legacyStageImportedCheckingEnvironment - :: LegacyModuleStage - -> LegacyCheckingEnvironment -legacyStageImportedCheckingEnvironment - (LegacyModuleStage - _ordinal - _address - imported - _localFacts - _localAliases - _registry - _manifest) = - legacyImportedCheckingEnvironment imported - -lookupLegacyStageFact - :: Marker - -> LegacyModuleStage - -> Maybe LegacyFactEntry -lookupLegacyStageFact alias stage = do - reference <- Map.lookup alias (visibleAliasBindings stage) - find - ((== reference) . legacyFactEntryReference) - (Vector.toList (legacyStageVisibleFacts stage)) - - -data LegacyReservedFact = LegacyReservedFact - !LegacyFactRef - !Facts.StagedFact - deriving stock (Show, Eq) - -legacyReservedFactReference - :: LegacyReservedFact - -> LegacyFactRef -legacyReservedFactReference - (LegacyReservedFact reference _staged) = - reference - -legacyReservedStagedFact - :: LegacyReservedFact - -> Facts.StagedFact -legacyReservedStagedFact - (LegacyReservedFact _reference staged) = - staged - -data LegacyDeclarationReservation = LegacyDeclarationReservation - !LegacyModuleOrdinal - !(NonEmpty LegacyReservedFact) - deriving stock (Show, Eq) - -legacyReservedFacts - :: LegacyDeclarationReservation - -> NonEmpty LegacyReservedFact -legacyReservedFacts - (LegacyDeclarationReservation _moduleOrdinal facts) = - facts - -reserveLegacyDeclaration - :: NonEmpty Facts.StagedFact - -> LegacyModuleStage - -> Either LegacyModuleStageError LegacyDeclarationReservation -reserveLegacyDeclaration stagedFacts stage - | finalOrdinal > toInteger (maxBound :: Word32) = - Left - (LegacyLocalFactOrdinalSpaceExhausted - (legacyStageModuleOrdinal stage)) - | otherwise = do - void - (foldM - reserveAlias - (visibleAliasBindings stage) - [ ( alias - , legacyReservedFactReference reserved - ) - | reserved <- reservedFactsList - , alias <- - NonEmpty.toList - (Facts.stagedFactAliases - (legacyReservedStagedFact reserved)) - ]) - pure - (LegacyDeclarationReservation - moduleOrdinal - reservedFacts) - where - moduleOrdinal = - legacyStageModuleOrdinal stage - firstOrdinal = - Vector.length (legacyStageLocalFacts stage) - stagedFactsList = - NonEmpty.toList stagedFacts - finalOrdinal = - toInteger firstOrdinal - + toInteger (length stagedFactsList) - - 1 - reservedFacts = - NonEmpty.zipWith - (\ordinal staged -> - LegacyReservedFact - (legacyFactRef - moduleOrdinal - (legacyLocalFactOrdinal - (fromIntegral ordinal))) - staged) - (firstOrdinal :| [firstOrdinal + 1 ..]) - stagedFacts - reservedFactsList = - NonEmpty.toList reservedFacts - - reserveAlias aliases (alias, reference) = - case Map.lookup alias aliases of - Nothing -> - Right (Map.insert alias reference aliases) - Just previous -> - Left - (LegacyAliasAlreadyBound - alias - previous - reference) - -visibleAliasBindings - :: LegacyModuleStage - -> Map Marker LegacyFactRef -visibleAliasBindings - (LegacyModuleStage - _ordinal - _address - (LegacyImportedView - _moduleOrdinals - _facts - importedAliases - _importedRegistry - _environmentDeltas - _environment) - _localFacts - localAliases - _stageRegistry - _manifest) = - Map.union localAliases importedAliases - -appendEstablishedLegacyDeclaration - :: LegacyDeclarationReservation - -> NonEmpty H1LegacyAdmittedFact - -> LegacyModuleStage - -> Either LegacyModuleStageError LegacyModuleStage -appendEstablishedLegacyDeclaration reservation admittedFacts stage = do - expectedReservation <- - reserveLegacyDeclaration - (fmap legacyReservedStagedFact - (legacyReservedFacts reservation)) - stage - unless - (reservation == expectedReservation) - (Left LegacyReservationDoesNotMatchStage) - let reserved = - NonEmpty.toList (legacyReservedFacts reservation) - admitted = - NonEmpty.toList admittedFacts - unless - (length reserved == length admitted) - (Left - (LegacyEstablishedFactCountMismatch - (length reserved) - (length admitted))) - entries <- - traverse - prepareEntry - (zip reserved admitted) - (manifestEntries, _nextAssumptionOrdinal) <- - foldM - prepareManifestEntry - ([], fromIntegral (Vector.length manifest)) - entries - registry' <- - first - LegacyFactRegistryRejectedAlias - (Facts.registerStagedFacts - (fmap legacyReservedStagedFact - (legacyReservedFacts reservation)) - registry) - let localAliases' = - foldl' - insertEntryAliases - localAliases - entries - pure - (LegacyModuleStage - moduleOrdinal - address - imported - (localFacts <> Vector.fromList entries) - localAliases' - registry' - (manifest - <> Vector.fromList (reverse manifestEntries))) - where - LegacyModuleStage - moduleOrdinal - address - imported - localFacts - localAliases - registry - manifest = - stage - - prepareEntry (reservedFact, admitted) = - let reference = - legacyReservedFactReference reservedFact - staged = - legacyReservedStagedFact reservedFact - expected = - prepareLegacyProposition - (Facts.stagedFactSemantic staged) - LegacyAdmittedFact semantic authorization = - admitted - in - do - unless - (legacySemanticProposition semantic == expected) - (Left - (LegacyEstablishedFactStatementMismatch - reference)) - unless - (legacyAuthorizationTarget authorization - == expected) - (Left - (LegacyEstablishedAuthorizationMismatch - reference)) - traverse_ - (validateObligationModule moduleOrdinal) - (legacyAuthorizationObligations authorization) - let availableReferences = - Set.fromList - ( (legacyFactEntryReference - <$> Vector.toList - (legacyStageVisibleFacts stage)) - <> (legacyReservedFactReference - <$> NonEmpty.toList - (legacyReservedFacts - reservation)) - ) - traverse_ - (\predecessor -> - unless - (predecessor - `Set.member` availableReferences) - (Left - (LegacyAuthorizationReferencesUnknownFact - reference - predecessor))) - (legacyAuthorizationFactPredecessors - authorization) - pure - (LegacyFactEntry - reference - staged - admitted) - - prepareManifestEntry - (entries, nextOrdinal) - (LegacyFactEntry - reference - _staged - (LegacyAdmittedFact - semantic - authorization)) = - case authorization of - LegacyDeclaredAssumption - (SessionLegacyDeclaredAssumptionRef - authorizedReference - assumptionOrdinal - kind - proposition) - | authorizedReference == reference - && legacyLocalAssumptionOrdinalValue - assumptionOrdinal - == nextOrdinal - && proposition - == legacySemanticProposition semantic -> - Right - ( LegacyDirectAxiomManifestEntry - reference - kind - proposition - : entries - , nextOrdinal + 1 - ) - | otherwise -> - Left - (LegacyDeclaredAssumptionDoesNotMatch - reference) - _ -> - Right (entries, nextOrdinal) - - insertEntryAliases aliases entry = - foldl' - (\current alias -> - Map.insert - alias - (legacyFactEntryReference entry) - current) - aliases - (NonEmpty.toList - (Facts.stagedFactAliases - (legacyFactEntryStagedFact entry))) - - -authorizeLegacyDeclaredAssumption - :: LegacyModuleStage - -> AssumptionKind - -> LegacyReservedFact - -> H1LegacyAdmittedFact -authorizeLegacyDeclaredAssumption stage kind reserved = - LegacyAdmittedFact - semantic - (LegacyDeclaredAssumption - (SessionLegacyDeclaredAssumptionRef - reference - assumptionOrdinal - kind - proposition)) - where - reference = - legacyReservedFactReference reserved - proposition = - reservedProposition reserved - semantic = - legacySemanticFact proposition - assumptionOrdinal = - legacyLocalAssumptionOrdinal - (fromIntegral - (Vector.length - (legacyStageDirectAxiomManifest stage))) - -authorizeLegacyTrustedVampire - :: SessionLegacyObligationRef - -> AcceptedVampireRun - -> LegacyTrustDependencies - -> LegacyReservedFact - -> H1LegacyAdmittedFact -authorizeLegacyTrustedVampire - obligation - accepted - predecessorTrust - reserved = - LegacyAdmittedFact - semantic - (LegacyTrustedVampire - (SessionLegacyTrustedVampireEvidence - obligation - proposition - accepted - trust)) - where - proposition = - reservedProposition reserved - semantic = - legacySemanticFact proposition - trust = - legacyTrustedVampireTrust - obligation - predecessorTrust - -authorizeLegacyGap - :: SessionLegacyObligationRef - -> Location - -> Marker - -> LegacyTrustDependencies - -> LegacyReservedFact - -> H1LegacyAdmittedFact -authorizeLegacyGap - obligation - location - marker - predecessorTrust - reserved = - LegacyAdmittedFact - semantic - (LegacyGap - (SessionLegacyGapEvidence - obligation - proposition - location - marker - trust)) - where - proposition = - reservedProposition reserved - semantic = - legacySemanticFact proposition - trust = - legacyGapTrust - obligation - location - marker - predecessorTrust - -authorizeLegacyRule - :: LegacyRuleTag - -> Vector (LegacyRulePredecessor LegacyFactRef) - -> LegacyTrustDependencies - -> LegacyReservedFact - -> H1LegacyAdmittedFact -authorizeLegacyRule tag predecessors predecessorTrust reserved = - LegacyAdmittedFact - semantic - (TrustedLegacyDeclarationRule - CheckedLegacyRuleApplication - { checkedLegacyRuleTag = tag - , checkedLegacyRuleTarget = proposition - , checkedLegacyPredecessors = predecessors - , checkedLegacyTrustSummary = trust - }) - where - reference = - legacyReservedFactReference reserved - proposition = - reservedProposition reserved - semantic = - legacySemanticFact proposition - trust = - predecessorTrust - <> mempty - { trustedLegacyRuleUses = - Set.singleton - (SessionLegacyRuleUse reference tag) - } - -reservedProposition - :: LegacyReservedFact - -> LegacyPreparedProposition -reservedProposition = - prepareLegacyProposition - . Facts.stagedFactSemantic - . legacyReservedStagedFact - -legacyAuthorizationTarget - :: H1LegacyFactAuthorization - -> LegacyPreparedProposition -legacyAuthorizationTarget = \case - LegacyDeclaredAssumption - (SessionLegacyDeclaredAssumptionRef - _reference - _ordinal - _kind - proposition) -> - proposition - LegacyTrustedVampire - (SessionLegacyTrustedVampireEvidence - _obligation - proposition - _run - _trust) -> - proposition - LegacyGap - (SessionLegacyGapEvidence - _obligation - proposition - _location - _marker - _trust) -> - proposition - TrustedLegacyDeclarationRule application -> - checkedLegacyRuleTarget application - -legacyAuthorizationObligations - :: H1LegacyFactAuthorization - -> [SessionLegacyObligationRef] -legacyAuthorizationObligations = \case - LegacyDeclaredAssumption{} -> - [] - LegacyTrustedVampire - (SessionLegacyTrustedVampireEvidence - obligation - _proposition - _run - _trust) -> - [obligation] - LegacyGap - (SessionLegacyGapEvidence - obligation - _proposition - _location - _marker - _trust) -> - [obligation] - TrustedLegacyDeclarationRule application -> - [ obligation - | LegacyRuleObligationPredecessor obligation <- - Vector.toList - (checkedLegacyPredecessors application) - ] - -legacyAuthorizationFactPredecessors - :: H1LegacyFactAuthorization - -> [LegacyFactRef] -legacyAuthorizationFactPredecessors = \case - TrustedLegacyDeclarationRule application -> - [ reference - | LegacyRuleFactPredecessor reference <- - Vector.toList - (checkedLegacyPredecessors application) - ] - _ -> - [] - -validateObligationModule - :: LegacyModuleOrdinal - -> SessionLegacyObligationRef - -> Either LegacyModuleStageError () -validateObligationModule - expected - (SessionLegacyObligationRef actual _marker _ordinal) = - unless - (actual == expected) - (Left - (LegacyAuthorizationReferencesAnotherModule - expected - actual)) - - --- | Completed H1 module. Only 'sealLegacyModuleStage' constructs this value. -data LegacyAdmittedModule = LegacyAdmittedModule - { legacyAdmittedModuleOrdinal :: !LegacyModuleOrdinal - , legacyAdmittedSourceAddress :: !ResolvedSourceAddress - , legacyAdmittedDirectImports :: !(Vector LegacyModuleOrdinal) - , legacyAdmittedVisibleFacts :: !(Vector LegacyFactEntry) - , legacyAdmittedLocalFacts :: !(Vector LegacyFactEntry) - , legacyAdmittedAliasBindings :: !(Map Marker LegacyFactRef) - , legacyAdmittedFactRegistry :: !Facts.FactRegistry - , legacyAdmittedDirectAxiomManifest - :: !(Vector LegacyDirectAxiomManifestEntry) - , legacyAdmittedTrustDependencies :: !LegacyTrustDependencies - , legacyAdmittedEnvironmentDeltas - :: !(Vector LegacyModuleEnvironmentDelta) - , legacyAdmittedCheckingEnvironment - :: !LegacyCheckingEnvironment - } - -sealLegacyModuleStage - :: LegacyCheckingEnvironment - -> LegacyModuleStage - -> Either LegacyModuleStageError LegacyAdmittedModule -sealLegacyModuleStage finalEnvironment stage = do - unless - (actualReferences == expectedReferences) - (Left LegacyStageLocalFactOrderMismatch) - expectedVisibleAliases <- - aliasesForEntries - importedAliases - (Vector.toList localFacts) - unless - (Map.union localAliases importedAliases - == expectedVisibleAliases) - (Left LegacyStageAliasMapMismatch) - expectedManifest <- - manifestForEntries localFacts - unless - (manifest == expectedManifest) - (Left LegacyStageDirectAxiomManifestMismatch) - validateStageRegistry visibleFacts registry - localEnvironmentDelta <- - first - LegacyStageEnvironmentMismatch - (legacyCheckingEnvironmentExtension - importedEnvironment - finalEnvironment) - let moduleEnvironmentDelta = - LegacyModuleEnvironmentDelta - moduleOrdinal - address - localEnvironmentDelta - pure - LegacyAdmittedModule - { legacyAdmittedModuleOrdinal = moduleOrdinal - , legacyAdmittedSourceAddress = address - , legacyAdmittedDirectImports = - legacyImportedModuleOrdinals imported - , legacyAdmittedVisibleFacts = visibleFacts - , legacyAdmittedLocalFacts = localFacts - , legacyAdmittedAliasBindings = - Map.union localAliases importedAliases - , legacyAdmittedFactRegistry = registry - , legacyAdmittedDirectAxiomManifest = manifest - , legacyAdmittedTrustDependencies = - foldMap - legacyFactEntryTrustDependencies - visibleFacts - , legacyAdmittedEnvironmentDeltas = - Vector.snoc - importedEnvironmentDeltas - moduleEnvironmentDelta - , legacyAdmittedCheckingEnvironment = - finalEnvironment - } - where - LegacyModuleStage - moduleOrdinal - address - imported@(LegacyImportedView - _directImports - importedFacts - importedAliases - _importedRegistry - importedEnvironmentDeltas - importedEnvironment) - localFacts - localAliases - registry - manifest = - stage - visibleFacts = - importedFacts <> localFacts - actualReferences = - legacyFactEntryReference <$> Vector.toList localFacts - expectedReferences = - [ legacyFactRef - moduleOrdinal - (legacyLocalFactOrdinal - (fromIntegral ordinal)) - | ordinal <- [0 .. Vector.length localFacts - 1] - ] - -legacyImportedView - :: LegacyCheckingEnvironment - -> [LegacyAdmittedModule] - -> Either LegacyModuleStageError LegacyImportedView -legacyImportedView foundation admittedModules = do - imported <- - foldM - importModule - emptyImportedViewBuild - admittedModules - registry <- - registryForEntries - (reverse (importedFactsReversed imported)) - (environmentDeltas, environment) <- - mergeModuleEnvironments foundation admittedModules - pure - (LegacyImportedView - (Vector.fromList - (legacyAdmittedModuleOrdinal <$> admittedModules)) - (Vector.fromList - (reverse (importedFactsReversed imported))) - (fst <$> importedAliasBindings imported) - registry - environmentDeltas - environment) - where - importModule imported admitted = - foldM - importEntry - imported - (Vector.toList - (legacyAdmittedVisibleFacts admitted)) - -data ImportedViewBuild = ImportedViewBuild - !(Map LegacyFactRef LegacyFactEntry) - ![LegacyFactEntry] - !(Map Marker (LegacyFactRef, Facts.FactOrigin)) - -emptyImportedViewBuild :: ImportedViewBuild -emptyImportedViewBuild = - ImportedViewBuild Map.empty [] Map.empty - -importedFactsReversed :: ImportedViewBuild -> [LegacyFactEntry] -importedFactsReversed - (ImportedViewBuild _entriesByReference entries _aliases) = - entries - -importedAliasBindings - :: ImportedViewBuild - -> Map Marker (LegacyFactRef, Facts.FactOrigin) -importedAliasBindings - (ImportedViewBuild _entriesByReference _entries aliases) = - aliases - -data LegacyModuleEnvironmentDelta = LegacyModuleEnvironmentDelta - !LegacyModuleOrdinal - !ResolvedSourceAddress - !LegacyCheckingEnvironmentDelta - deriving stock (Show, Eq) - -data ImportedEnvironmentBuild = ImportedEnvironmentBuild - !(Map LegacyModuleOrdinal LegacyModuleEnvironmentDelta) - ![LegacyModuleEnvironmentDelta] - -mergeModuleEnvironments - :: LegacyCheckingEnvironment - -> [LegacyAdmittedModule] - -> Either - LegacyModuleStageError - ( Vector LegacyModuleEnvironmentDelta - , LegacyCheckingEnvironment - ) -mergeModuleEnvironments foundation admittedModules = do - imported <- - foldM - importModuleEnvironment - (ImportedEnvironmentBuild Map.empty []) - admittedModules - let ImportedEnvironmentBuild _byOrdinal reversedDeltas = - imported - deltas = - reverse reversedDeltas - environment <- - foldM - applyModuleEnvironmentDelta - foundation - deltas - pure (Vector.fromList deltas, environment) - where - importModuleEnvironment imported admitted = - foldM - importEnvironmentDelta - imported - (Vector.toList - (legacyAdmittedEnvironmentDeltas admitted)) - - importEnvironmentDelta - imported@(ImportedEnvironmentBuild - byOrdinal - reversedDeltas) - delta@(LegacyModuleEnvironmentDelta - ordinal - _address - _environmentDelta) = - case Map.lookup ordinal byOrdinal of - Nothing -> - Right - (ImportedEnvironmentBuild - (Map.insert ordinal delta byOrdinal) - (delta : reversedDeltas)) - Just previous - | previous == delta -> - Right imported - | otherwise -> - Left - (LegacyImportedModuleEnvironmentConflict - ordinal) - - applyModuleEnvironmentDelta - environment - (LegacyModuleEnvironmentDelta - _ordinal - address - delta) = - first - (LegacyImportedEnvironmentConflict address) - (applyLegacyCheckingEnvironmentDelta - delta - environment) - -importEntry - :: ImportedViewBuild - -> LegacyFactEntry - -> Either LegacyModuleStageError ImportedViewBuild -importEntry imported entry = - case Map.lookup reference entriesByReference of - Just previous - | previous == entry -> - Right imported - | otherwise -> - Left - (LegacyImportedFactReferenceConflict - reference) - Nothing -> do - aliases' <- - foldM - insertImportedAlias - aliases - (NonEmpty.toList - (Facts.stagedFactAliases staged)) - pure - (ImportedViewBuild - (Map.insert - reference - entry - entriesByReference) - (entry : entries) - aliases') - where - ImportedViewBuild - entriesByReference - entries - aliases = - imported - reference = - legacyFactEntryReference entry - staged = - legacyFactEntryStagedFact entry - origin = - Facts.stagedFactOrigin staged - - insertImportedAlias current alias = - case Map.lookup alias current of - Nothing -> - Right - (Map.insert - alias - (reference, origin) - current) - Just (previousReference, previousOrigin) - | previousReference == reference -> - Right current - | otherwise -> - Left - (LegacyImportedAliasConflict - alias - previousReference - previousOrigin - reference - origin) - -aliasesForEntries - :: Map Marker LegacyFactRef - -> [LegacyFactEntry] - -> Either LegacyModuleStageError (Map Marker LegacyFactRef) -aliasesForEntries = - foldM insertEntry - where - insertEntry aliases entry = - foldM - (insertAlias - (legacyFactEntryReference entry)) - aliases - (NonEmpty.toList - (Facts.stagedFactAliases - (legacyFactEntryStagedFact entry))) - - insertAlias reference aliases alias = - case Map.lookup alias aliases of - Nothing -> - Right (Map.insert alias reference aliases) - Just previous - | previous == reference -> - Right aliases - | otherwise -> - Left - (LegacyAliasAlreadyBound - alias - previous - reference) - -manifestForEntries - :: Vector LegacyFactEntry - -> Either - LegacyModuleStageError - (Vector LegacyDirectAxiomManifestEntry) -manifestForEntries entries = - Vector.fromList . reverse . fst - <$> foldM - step - ([], 0) - (Vector.toList entries) - where - step (manifest, nextOrdinal) entry = - case legacyFactEntryAdmittedFact entry of - LegacyAdmittedFact - semantic - (LegacyDeclaredAssumption - (SessionLegacyDeclaredAssumptionRef - authorizedReference - assumptionOrdinal - kind - proposition)) - | authorizedReference == reference - && legacyLocalAssumptionOrdinalValue - assumptionOrdinal - == nextOrdinal - && proposition - == legacySemanticProposition semantic -> - Right - ( LegacyDirectAxiomManifestEntry - reference - kind - proposition - : manifest - , nextOrdinal + 1 - ) - | otherwise -> - Left - LegacyStageDirectAxiomManifestMismatch - _ -> - Right (manifest, nextOrdinal) - where - reference = - legacyFactEntryReference entry - -validateStageRegistry - :: Vector LegacyFactEntry - -> Facts.FactRegistry - -> Either LegacyModuleStageError () -validateStageRegistry entries registry = do - unless - (Facts.factRegistryInvariant registry) - (Left LegacyStageFactRegistryMismatch) - unless - (length (Facts.registeredFacts registry) - == Vector.length entries) - (Left LegacyStageFactRegistryMismatch) - traverse_ validateEntry entries - where - validateEntry entry = - traverse_ - (validateAlias - (legacyFactEntryStagedFact entry)) - (Facts.stagedFactAliases - (legacyFactEntryStagedFact entry)) - - validateAlias staged alias = do - unless - (Facts.lookupPreparedFact alias registry - == Just (Facts.stagedFactSemantic staged)) - (Left LegacyStageFactRegistryMismatch) - unless - (Facts.lookupFactOrigin alias registry - == Just (Facts.stagedFactOrigin staged)) - (Left LegacyStageFactRegistryMismatch) - -registryForEntries - :: [LegacyFactEntry] - -> Either LegacyModuleStageError Facts.FactRegistry -registryForEntries = \case - [] -> - Right Facts.emptyFactRegistry - firstEntry : remainingEntries -> - first - LegacyFactRegistryRejectedAlias - (Facts.registerStagedFacts - ( legacyFactEntryStagedFact firstEntry - :| (legacyFactEntryStagedFact - <$> remainingEntries) - ) - Facts.emptyFactRegistry) - - -data LegacyModuleStageError - = LegacyModuleOrdinalSpaceExhausted !Natural - | LegacyLocalFactOrdinalSpaceExhausted !LegacyModuleOrdinal - | LegacyAliasAlreadyBound - !Marker - !LegacyFactRef - !LegacyFactRef - | LegacyReservationDoesNotMatchStage - | LegacyEstablishedFactCountMismatch !Int !Int - | LegacyEstablishedFactStatementMismatch !LegacyFactRef - | LegacyEstablishedAuthorizationMismatch !LegacyFactRef - | LegacyAuthorizationReferencesUnknownFact - !LegacyFactRef - !LegacyFactRef - | LegacyAuthorizationReferencesAnotherModule - !LegacyModuleOrdinal - !LegacyModuleOrdinal - | LegacyDeclaredAssumptionDoesNotMatch !LegacyFactRef - | LegacyFactRegistryRejectedAlias !Marker - | LegacyImportedFactReferenceConflict !LegacyFactRef - | LegacyImportedAliasConflict - !Marker - !LegacyFactRef - !Facts.FactOrigin - !LegacyFactRef - !Facts.FactOrigin - | LegacyStageLocalFactOrderMismatch - | LegacyStageAliasMapMismatch - | LegacyStageFactRegistryMismatch - | LegacyStageDirectAxiomManifestMismatch - | LegacyStageEnvironmentMismatch !Text - | LegacyImportedModuleEnvironmentConflict - !LegacyModuleOrdinal - | LegacyImportedEnvironmentConflict - !ResolvedSourceAddress - !Text - deriving stock (Show, Eq) |