diff options
Diffstat (limited to 'source/Felix/Migration.hs')
| -rw-r--r-- | source/Felix/Migration.hs | 284 |
1 files changed, 0 insertions, 284 deletions
diff --git a/source/Felix/Migration.hs b/source/Felix/Migration.hs deleted file mode 100644 index 0fcb05d..0000000 --- a/source/Felix/Migration.hs +++ /dev/null @@ -1,284 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Temporary routing data for the content-addressed migration. --- --- These values select current physical sources. They are not durable module --- names and must be deleted with the legacy driver. -module Felix.Migration - ( MigrationMountRole(..) - , migrationMountId - , MigrationModuleRef - , migrationModuleRefRole - , migrationModuleRefPath - , MigrationManifestError(..) - , migrationModuleCandidatePath - , ResolvedMigrationSelection - , resolveMigrationSelection - , migrationSelectionContains - , MigrationGraphRoute(..) - , classifyMigrationGraph - , activeMigrationRoots - , protectedMigrationModules - , phase53LibraryMigrationModules - , typedMigrationModules - , PreludeSourceFamily(..) - , finalPreludeSourceFamilies - , PreludePublicRole(..) - , expectedFinalPreludePublicRoles - ) where - -import Base -import Felix.Parse -import Felix.Source - -import Data.List qualified as List -import Data.Set qualified as Set - - -data MigrationMountRole - = MigrationProject - | MigrationLibrary - | MigrationDebug - deriving stock (Show, Eq, Ord, Enum, Bounded) - -migrationMountId :: MigrationMountRole -> SourceMountId -migrationMountId = \case - MigrationProject -> - sourceMountId "project" - MigrationLibrary -> - sourceMountId "library" - MigrationDebug -> - sourceMountId "debug" - - -data MigrationModuleRef = MigrationModuleRef - !MigrationMountRole - !SafeRelativePath - deriving stock (Show, Eq, Ord) - -migrationModuleRefRole - :: MigrationModuleRef - -> MigrationMountRole -migrationModuleRefRole (MigrationModuleRef role _path) = - role - -migrationModuleRefPath - :: MigrationModuleRef - -> SafeRelativePath -migrationModuleRefPath (MigrationModuleRef _role path) = - path - -data MigrationManifestError - = MissingMigrationMountRole !MigrationMountRole - deriving stock (Show, Eq) - -newtype ResolvedMigrationSelection = ResolvedMigrationSelection - (Set (SourceMountId, CanonicalPath, SafeRelativePath)) - -resolveMigrationSelection - :: Foldable references - => SourceMounts - -> references MigrationModuleRef - -> Either MigrationManifestError ResolvedMigrationSelection -resolveMigrationSelection mounts references = - ResolvedMigrationSelection . Set.fromList - <$> traverse resolveOne (toList references) - where - resolveOne reference = - case List.find - ((== migrationMountId role) . sourceMountIdentifier) - (sourceMountList mounts) of - Nothing -> - Left (MissingMigrationMountRole role) - Just mount -> - Right - ( sourceMountIdentifier mount - , sourceMountRoot mount - , migrationModuleRefPath reference - ) - where - role = migrationModuleRefRole reference - -migrationSelectionContains - :: ResolvedMigrationSelection - -> ResolvedSource - -> Bool -migrationSelectionContains - (ResolvedMigrationSelection selected) source = - ( resolvedSourceMount source - , resolvedSourceMountRoot source - , resolvedSourceRelativePath source - ) `Set.member` selected - -data MigrationGraphRoute - = TypedMigrationGraph - | LegacyMigrationGraph - deriving stock (Show, Eq) - -classifyMigrationGraph - :: ResolvedMigrationSelection - -> ParsedSourceWorkspace - -> MigrationGraphRoute -classifyMigrationGraph selected workspace - | all - (migrationSelectionContains selected . parsedModuleResolved) - (parsedWorkspaceModules workspace) = - TypedMigrationGraph - | otherwise = - LegacyMigrationGraph - --- | Resolve one routing reference against the current prepared mount table. --- --- This deliberately returns a physical candidate path, not a logical owner. -migrationModuleCandidatePath - :: SourceMounts - -> MigrationModuleRef - -> Either MigrationManifestError FilePath -migrationModuleCandidatePath mounts reference = - case List.find matchesRole candidates of - Nothing -> - Left (MissingMigrationMountRole role) - Just candidate -> - Right (sourceCandidatePath candidate) - where - role = migrationModuleRefRole reference - expectedMount = migrationMountId role - candidates = - sourceCandidates - mounts - (migrationModuleRefPath reference) - matchesRole candidate = - sourceCandidateMount candidate == expectedMount - - --- | Current supported verification root. -activeMigrationRoots :: NonEmpty MigrationModuleRef -activeMigrationRoots = - migrationLibraryModule "everything.tex" :| [] - --- | Dependency-closed set/naturals migration boundary. -protectedMigrationModules :: NonEmpty MigrationModuleRef -protectedMigrationModules = - migrationLibraryModule "set.tex" :| - [ migrationLibraryModule "set/cons.tex" - , migrationLibraryModule "set/regularity.tex" - , migrationLibraryModule "set/suc.tex" - , migrationLibraryModule "nat.tex" - ] - --- | Phase 5.3 ordinary library modules admitted by the typed driver. -phase53LibraryMigrationModules :: NonEmpty MigrationModuleRef -phase53LibraryMigrationModules = - migrationLibraryModule "set/symdiff.tex" :| - [ migrationLibraryModule "set/powerset.tex" - , migrationLibraryModule "set/partition.tex" - , migrationLibraryModule "set/bipartition.tex" - , migrationLibraryModule "set/product.tex" - , migrationLibraryModule "set/filter.tex" - , migrationLibraryModule "relation.tex" - , migrationLibraryModule "relation/properties.tex" - , migrationLibraryModule "relation/uniqueness.tex" - , migrationLibraryModule "function.tex" - , migrationLibraryModule "set/cantor.tex" - , migrationLibraryModule "set/fixpoint.tex" - ] - --- | Sources whose complete graphs may enter the typed driver. -typedMigrationModules :: NonEmpty MigrationModuleRef -typedMigrationModules = - protectedMigrationModules - <> phase53LibraryMigrationModules - <> (migrationProjectModule "test/phase3/typed-producer.tex" :| - [ migrationProjectModule "test/phase3/typed-unsupported.tex" - , migrationProjectModule "test/phase3/typed-shared-a.tex" - , migrationProjectModule "test/phase3/typed-shared-b.tex" - , migrationProjectModule "test/phase3/typed-shared-root.tex" - , migrationProjectModule "test/phase5/exact-producer.tex" - , migrationProjectModule "test/phase5/exact-importer.tex" - , migrationProjectModule "test/phase5/exact-failure.tex" - , migrationProjectModule "test/phase5/exact-proofs.tex" - , migrationProjectModule "test/phase5/exact-local-definition.tex" - , migrationProjectModule "test/phase5/exact-local-definition-failure.tex" - , migrationProjectModule "test/phase5/exact-contradiction.tex" - , migrationProjectModule "test/phase5/exact-contradiction-goal.tex" - , migrationProjectModule "test/phase5/exact-relation-expression.tex" - , migrationProjectModule "test/phase5/exact-relation-expression-missing-pair.tex" - , migrationProjectModule "test/phase5/exact-application.tex" - , migrationProjectModule "test/phase5/exact-application-missing.tex" - , migrationProjectModule "test/phase5/exact-quantified-subject.tex" - , migrationProjectModule "test/phase5/exact-quantified-subject-nested.tex" - , migrationProjectModule "test/phase5/exact-proof-failure.tex" - , migrationProjectModule "test/phase5/exact-induction-nested.tex" - , migrationProjectModule "test/phase5/exact-runtime-failure.tex" - , migrationProjectModule "test/phase5/exact-source-axiom.tex" - , migrationProjectModule "test/phase5/exact-source-axiom-assumptions.tex" - , migrationProjectModule "test/phase5/exact-omitted.tex" - , migrationProjectModule "test/phase5/exact-escape-producer.tex" - , migrationProjectModule "test/phase5/exact-escape-consumer.tex" - , migrationProjectModule "test/phase5/exact-separation.tex" - , migrationProjectModule "test/phase5/exact-replacement.tex" - , migrationProjectModule "test/phase5/exact-finite-set.tex" - , migrationProjectModule "test/phase5/exact-datatype.tex" - , migrationProjectModule "test/phase5/exact-datatype-nested.tex" - , migrationProjectModule "test/phase5/exact-inductive.tex" - , migrationProjectModule "test/phase5/exact-inductive-recursive.tex" - , migrationProjectModule "test/phase5/exact-inductive-nested.tex" - , migrationProjectModule "test/phase5/unmatched-proof.tex" - ]) - - --- | Source constructs required by the non-authoritative prelude skeleton. -data PreludeSourceFamily - = PreludeDefinition - | PreludeAbbreviation - | PreludeProposition - | PreludeProof - deriving stock (Show, Eq, Ord, Enum, Bounded) - -finalPreludeSourceFamilies :: Set PreludeSourceFamily -finalPreludeSourceFamilies = - Set.fromList - [ PreludeDefinition - , PreludeAbbreviation - , PreludeProposition - , PreludeProof - ] - --- | Stable public roles required at final-prelude cutover. --- --- Helper declarations used to derive these roles are intentionally not --- frozen by Phase 0. -data PreludePublicRole - = PreludeInfinityTheorem - | PreludeOmegaObject - | PreludeOmegaDefiningEquation - | PreludeNaturalsAlias - | PreludeNaturalsInductiveTheorem - | PreludeNaturalsMinimalTheorem - deriving stock (Show, Eq, Ord, Enum, Bounded) - -expectedFinalPreludePublicRoles :: Set PreludePublicRole -expectedFinalPreludePublicRoles = - Set.fromList [minBound .. maxBound] - - -migrationLibraryModule :: FilePath -> MigrationModuleRef -migrationLibraryModule = - MigrationModuleRef MigrationLibrary . checkedRelativePath - -migrationProjectModule :: FilePath -> MigrationModuleRef -migrationProjectModule = - MigrationModuleRef MigrationProject . checkedRelativePath - -checkedRelativePath :: FilePath -> SafeRelativePath -checkedRelativePath path = - case safeRelativePath path of - Left err -> - impossible - ("invalid migration path literal " - <> show path - <> ": " - <> show err) - Right relative -> - relative |