From eed186886ab8e0a3fa57bc9f4e88e5fb9a5be8aa Mon Sep 17 00:00:00 2001 From: adelon <22380201+adelon@users.noreply.github.com> Date: Sun, 2 Aug 2026 22:46:18 +0200 Subject: Activate product and filter typed roots --- source/Test/Unit/Migration.hs | 38 +++++---- source/Test/Unit/Module.hs | 174 ++++++++++++++++++++++++++++-------------- 2 files changed, 140 insertions(+), 72 deletions(-) (limited to 'source/Test/Unit') diff --git a/source/Test/Unit/Migration.hs b/source/Test/Unit/Migration.hs index b9e9bd1..8c01b93 100644 --- a/source/Test/Unit/Migration.hs +++ b/source/Test/Unit/Migration.hs @@ -106,23 +106,29 @@ selectsCompleteGraphDriver = do assertEqual "unselected importer keeps the complete graph legacy" LegacyMigrationGraph (classifyMigrationGraph selection importer) - (elementary, _elementaryMeasurements) <- - expectRight - =<< parseRoot "set/bipartition.tex" - assertEqual "elementary set closure uses the typed driver" - TypedMigrationGraph - (classifyMigrationGraph selection elementary) - assertEqual "bipartition direct imports" - [ "set.tex" - , "set/cons.tex" - , "set/powerset.tex" - ] - [ safeRelativePathFilePath - (sourceAddressRelativePath - (Parse.parsedImportedAddress imported)) - | imported <- Parse.parsedModuleImports - (Parse.parsedWorkspaceRootModule elementary) + forM_ + [ ( "set/bipartition.tex" + , ["set.tex", "set/cons.tex", "set/powerset.tex"] + ) + , ("set/product.tex", ["set.tex"]) + , ("set/filter.tex", ["set.tex", "set/powerset.tex"]) ] + \(path, expectedImports) -> do + (elementary, _elementaryMeasurements) <- + expectRight =<< parseRoot path + assertEqual + (path <> " closure uses the typed driver") + TypedMigrationGraph + (classifyMigrationGraph selection elementary) + assertEqual + (path <> " direct imports") + expectedImports + [ safeRelativePathFilePath + (sourceAddressRelativePath + (Parse.parsedImportedAddress imported)) + | imported <- Parse.parsedModuleImports + (Parse.parsedWorkspaceRootModule elementary) + ] expectRight :: Show err => Either err value -> IO value expectRight = \case diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs index bd6772b..f7e8fed 100644 --- a/source/Test/Unit/Module.hs +++ b/source/Test/Unit/Module.hs @@ -671,72 +671,114 @@ checksElementarySetClosure = do =<< Module.buildFinalPreludeSession store foundation resolver mounts <- exactFixtureMounts repository - workspace <- parseFinalExactWorkspace - prelude mounts "set/bipartition.tex" selection <- expectRight (Migration.resolveMigrationSelection mounts Migration.typedMigrationModules) - assertEqual "elementary graph route" - Migration.TypedMigrationGraph - (Migration.classifyMigrationGraph selection workspace) - sealed <- compileFinalParsedWorkspaceWithResolver - foundation prelude resolver workspace - let parsed = toList - (Parse.parsedWorkspaceImportedBeforeImporter workspace) - modules = Map.fromList - [ ( safeRelativePathFilePath - (resolvedSourceRelativePath - (Parse.parsedModuleResolved source)) - , (source, checked) - ) - | (source, checked) <- zip parsed sealed - ] - moduleAt path = maybe - (assertFailure ("missing typed module " <> path) - >> fail "unreachable") - pure - (Map.lookup path modules) - preludeSyntaxId = Syntax.moduleSyntaxAssertedId + let preludeSyntaxId = Syntax.moduleSyntaxAssertedId (Module.sealedTypedModuleSyntax (Module.migrationPreludeModule prelude)) preludeSemanticId = Semantic.semanticInterfaceAssertedId (Module.sealedTypedModuleSemantic (Module.migrationPreludeModule prelude)) - assertEqual "elementary module count" - (length parsed) - (length sealed) - forM_ parsed \source -> - assertEqual "final prelude is the first syntax input" - (Just preludeSyntaxId) - (listToMaybe - (Syntax.moduleSyntaxDirectInputs - (Parse.parsedModuleSyntaxInterface source))) - forM_ sealed \checked -> - assertEqual "final prelude is the first semantic input" - (Just preludeSemanticId) - (listToMaybe + checkRoot path inspect = do + workspace <- parseFinalExactWorkspace + prelude mounts path + assertEqual (path <> " graph route") + Migration.TypedMigrationGraph + (Migration.classifyMigrationGraph + selection workspace) + sealed <- compileFinalParsedWorkspaceWithResolver + foundation prelude resolver workspace + let parsed = toList + (Parse.parsedWorkspaceImportedBeforeImporter + workspace) + modules = Map.fromList + [ ( safeRelativePathFilePath + (resolvedSourceRelativePath + (Parse.parsedModuleResolved source)) + , (source, checked) + ) + | (source, checked) <- zip parsed sealed + ] + moduleAt modulePath = maybe + (assertFailure + ("missing typed module " <> modulePath) + >> fail "unreachable") + pure + (Map.lookup modulePath modules) + assertEqual (path <> " module count") + (length parsed) + (length sealed) + forM_ parsed \source -> + assertEqual + (path <> " final-prelude syntax input") + (Just preludeSyntaxId) + (listToMaybe + (Syntax.moduleSyntaxDirectInputs + (Parse.parsedModuleSyntaxInterface + source))) + forM_ sealed \checked -> + assertEqual + (path <> " final-prelude semantic input") + (Just preludeSemanticId) + (listToMaybe + (Semantic.semanticInterfaceDirectInputs + (Module.sealedTypedModuleSemantic + checked))) + inspect moduleAt + checkRoot "set/bipartition.tex" + \moduleAt -> do + (_setParsed, setModule) <- moduleAt "set.tex" + (_consParsed, consModule) <- + moduleAt "set/cons.tex" + (_powersetParsed, powersetModule) <- + moduleAt "set/powerset.tex" + (_bipartitionParsed, bipartitionModule) <- + moduleAt "set/bipartition.tex" + assertLocalAliasesAbsent powersetModule ["pow_iff"] + assertEqual "bipartition semantic imports" + [ preludeSemanticId + , semanticId setModule + , semanticId consModule + , semanticId powersetModule + ] (Semantic.semanticInterfaceDirectInputs - (Module.sealedTypedModuleSemantic checked))) - (_setParsed, setModule) <- moduleAt "set.tex" - (_consParsed, consModule) <- moduleAt "set/cons.tex" - (_powersetParsed, powersetModule) <- - moduleAt "set/powerset.tex" - (_bipartitionParsed, bipartitionModule) <- - moduleAt "set/bipartition.tex" - assertLocalAliasesAbsent powersetModule ["pow_iff"] - assertEqual "bipartition semantic imports" - [ preludeSemanticId - , semanticId setModule - , semanticId consModule - , semanticId powersetModule - ] - (Semantic.semanticInterfaceDirectInputs - (Module.sealedTypedModuleSemantic bipartitionModule)) - assertFactAliasEscapeKind - bipartitionModule - "bipartition_elim" - Authority.SourceAxiom + (Module.sealedTypedModuleSemantic + bipartitionModule)) + assertFactAliasEscapeKind + bipartitionModule + "bipartition_elim" + Authority.SourceAxiom + checkRoot "set/product.tex" + \moduleAt -> do + (_setParsed, setModule) <- moduleAt "set.tex" + (_productParsed, productModule) <- + moduleAt "set/product.tex" + assertEqual "product semantic imports" + [preludeSemanticId, semanticId setModule] + (Semantic.semanticInterfaceDirectInputs + (Module.sealedTypedModuleSemantic + productModule)) + assertFactAliasEscapeKind + productModule + "inter_times_intro" + Authority.SourceAxiom + checkRoot "set/filter.tex" + \moduleAt -> do + (_setParsed, setModule) <- moduleAt "set.tex" + (_powersetParsed, powersetModule) <- + moduleAt "set/powerset.tex" + (_filterParsed, filterModule) <- + moduleAt "set/filter.tex" + assertEqual "filter semantic imports" + [ preludeSemanticId + , semanticId setModule + , semanticId powersetModule + ] + (Semantic.semanticInterfaceDirectInputs + (Module.sealedTypedModuleSemantic filterModule)) + assertAllLocalFactsClean filterModule where semanticId = Semantic.semanticInterfaceAssertedId @@ -880,6 +922,24 @@ assertCleanFactAlias sealed name = do (Authority.factAuthoritySafety (Semantic.semanticFactAuthority fact)) +assertAllLocalFactsClean + :: Module.SealedTypedModule + -> Assertion +assertAllLocalFactsClean sealed = + assertBool + "all locally published facts have clean authority" + (all hasCleanAuthority localFacts) + where + localFacts = + [ fact + | delta <- localSemanticDeltas sealed + , fact <- Semantic.declarationDeltaFacts delta + ] + hasCleanAuthority fact = + Authority.factAuthoritySafety + (Semantic.semanticFactAuthority fact) + == Authority.cleanAuthoritySafety + assertSourceAxiomAlias :: Module.SealedTypedModule -> Text @@ -4107,6 +4167,8 @@ routesProductionVerification = , ("powerset", "set/powerset.tex") , ("partition", "set/partition.tex") , ("bipartition", "set/bipartition.tex") + , ("product", "set/product.tex") + , ("filter", "set/filter.tex") ] \(label, path) -> assertRoute ("typed " <> label) -- cgit v1.2.3