summaryrefslogtreecommitdiff
path: root/source/Test/Unit
diff options
context:
space:
mode:
Diffstat (limited to 'source/Test/Unit')
-rw-r--r--source/Test/Unit/Migration.hs38
-rw-r--r--source/Test/Unit/Module.hs174
2 files changed, 140 insertions, 72 deletions
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)
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 20:44:03 +0000