Activate base relation typed root

2 files changed, 65 insertions, 17 deletions

diff --git a/source/Test/Unit/Migration.hs b/source/Test/Unit/Migration.hs
index 8c01b93..155dce7 100644
--- a/source/Test/Unit/Migration.hs
+++ b/source/Test/Unit/Migration.hs
@@ -36,7 +36,7 @@ resolvesManifestReferences = do
     forM_
         (toList activeMigrationRoots
             <> toList protectedMigrationModules
-            <> toList elementarySetMigrationModules)
+            <> toList phase53LibraryMigrationModules)
         \reference -> do
             assertEqual
                 "manifest role"
@@ -56,7 +56,7 @@ resolvesManifestReferences = do
             "typed module mount role"
             (if reference `elem`
                     (toList protectedMigrationModules
-                        <> toList elementarySetMigrationModules)
+                        <> toList phase53LibraryMigrationModules)
                 then MigrationLibrary
                 else MigrationProject)
             (migrationModuleRefRole reference)
@@ -112,14 +112,17 @@ selectsCompleteGraphDriver = do
           )
         , ("set/product.tex", ["set.tex"])
         , ("set/filter.tex", ["set.tex", "set/powerset.tex"])
+        , ( "relation.tex"
+          , ["set.tex", "set/powerset.tex", "set/product.tex"]
+          )
         ]
         \(path, expectedImports) -> do
-            (elementary, _elementaryMeasurements) <-
+            (phase53, _phase53Measurements) <-
                 expectRight =<< parseRoot path
             assertEqual
                 (path <> " closure uses the typed driver")
                 TypedMigrationGraph
-                (classifyMigrationGraph selection elementary)
+                (classifyMigrationGraph selection phase53)
             assertEqual
                 (path <> " direct imports")
                 expectedImports
@@ -127,7 +130,7 @@ selectsCompleteGraphDriver = do
                     (sourceAddressRelativePath
                         (Parse.parsedImportedAddress imported))
                 | imported <- Parse.parsedModuleImports
-                    (Parse.parsedWorkspaceRootModule elementary)
+                    (Parse.parsedWorkspaceRootModule phase53)
                 ]
 
 expectRight :: Show err => Either err value -> IO value
diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index e840dba..d3295c1 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -76,8 +76,8 @@ unitTests =
             publishesFinalPreludeRoot
         , testCase "checks the protected nat closure with the final prelude"
             checksProtectedNatClosure
-        , testCase "checks the elementary set closure with the final prelude"
-            checksElementarySetClosure
+        , testCase "checks Phase 5.3 library closures with the final prelude"
+            checksPhase53LibraryClosures
         , testCase "retains exact omitted-proof locations"
             retainsExactOmittedProofLocation
         , testCase "coalesces syntax without collapsing semantic imports"
@@ -645,18 +645,18 @@ checksProtectedNatClosure = do
                 . (> 0)
                 =<< readIORef runs
 
-checksElementarySetClosure :: Assertion
-checksElementarySetClosure = do
+checksPhase53LibraryClosures :: Assertion
+checksPhase53LibraryClosures = do
     foundation <- expectRight Foundation.checkedFoundation
     repository <- getCurrentDirectory
-    Temp.withSystemTempDirectory "felix-elementary-set" \directory -> do
+    Temp.withSystemTempDirectory "felix-phase53-library" \directory -> do
         let storePath = directory Posix.</> "store.sqlite"
             executable = directory Posix.</> "vampire"
         writeFile executable
             (unlines
                 [ "#!/bin/sh"
                 , "cat >/dev/null"
-                , "printf '%s\\n' '% SZS status Theorem for elementary-set'"
+                , "printf '%s\\n' '% SZS status Theorem for phase53-library'"
                 ])
         permissions <- getPermissions executable
         setPermissions executable
@@ -781,6 +781,34 @@ checksElementarySetClosure = do
                             (Semantic.semanticInterfaceDirectInputs
                                 (Module.sealedTypedModuleSemantic filterModule))
                         assertAllLocalFactsClean filterModule
+                checkRoot "relation.tex"
+                    \moduleAt -> do
+                        (_setParsed, setModule) <- moduleAt "set.tex"
+                        (_powersetParsed, powersetModule) <-
+                            moduleAt "set/powerset.tex"
+                        (_productParsed, productModule) <-
+                            moduleAt "set/product.tex"
+                        (_relationParsed, relationModule) <-
+                            moduleAt "relation.tex"
+                        assertEqual "relation semantic imports"
+                            [ preludeSemanticId
+                            , semanticId setModule
+                            , semanticId powersetModule
+                            , semanticId productModule
+                            ]
+                            (Semantic.semanticInterfaceDirectInputs
+                                (Module.sealedTypedModuleSemantic
+                                    relationModule))
+                        assertCleanFactAlias
+                            relationModule
+                            "union_relations_is_relation"
+                        assertFactAliasEscapeKind
+                            relationModule
+                            "id_iff"
+                            Authority.SourceAxiom
+                        assertNoLocalFactEscapeKind
+                            relationModule
+                            Authority.Omitted
   where
     semanticId =
         Semantic.semanticInterfaceAssertedId
@@ -942,6 +970,27 @@ assertAllLocalFactsClean sealed =
             (Semantic.semanticFactAuthority fact)
             == Authority.cleanAuthoritySafety
 
+assertNoLocalFactEscapeKind
+    :: Module.SealedTypedModule
+    -> Authority.EscapeKind
+    -> Assertion
+assertNoLocalFactEscapeKind sealed unexpected =
+    assertBool
+        ("no local fact has " <> show unexpected <> " authority")
+        (all lacksEscapeKind localFacts)
+  where
+    localFacts =
+        [ fact
+        | delta <- localSemanticDeltas sealed
+        , fact <- Semantic.declarationDeltaFacts delta
+        ]
+    lacksEscapeKind fact =
+        unexpected
+            `notElem` Authority.escapeKindsToList
+                (Authority.authoritySafetyEscapeKinds
+                    (Authority.factAuthoritySafety
+                        (Semantic.semanticFactAuthority fact)))
+
 assertSourceAxiomAlias
     :: Module.SealedTypedModule
     -> Text
@@ -4211,12 +4260,8 @@ routesProductionVerification =
             Api.TypedVerificationRoute
             natRoot
         forM_
-            [ ("symmetric difference", "set/symdiff.tex")
-            , ("powerset", "set/powerset.tex")
-            , ("partition", "set/partition.tex")
-            , ("bipartition", "set/bipartition.tex")
-            , ("product", "set/product.tex")
-            , ("filter", "set/filter.tex")
+            [ ("bipartition", "set/bipartition.tex")
+            , ("relation", "relation.tex")
             ]
             \(label, path) ->
                 assertRoute ("typed " <> label)