Activate typed function module

2 files changed, 65 insertions, 4 deletions

diff --git a/source/Test/Unit/Migration.hs b/source/Test/Unit/Migration.hs
index 965a3dc..41bc1f9 100644
--- a/source/Test/Unit/Migration.hs
+++ b/source/Test/Unit/Migration.hs
@@ -121,6 +121,9 @@ selectsCompleteGraphDriver = do
         , ( "relation/uniqueness.tex"
           , ["set.tex", "relation.tex"]
           )
+        , ( "function.tex"
+          , ["set.tex", "relation.tex", "relation/uniqueness.tex"]
+          )
         ]
         \(path, expectedImports) -> do
             (phase53, _phase53Measurements) <-
@@ -139,8 +142,8 @@ selectsCompleteGraphDriver = do
                     (Parse.parsedWorkspaceRootModule phase53)
                 ]
     (functionImporter, _functionMeasurements) <-
-        expectRight =<< parseRoot "function.tex"
-    assertEqual "unselected function graph remains legacy"
+        expectRight =<< parseRoot "set/cantor.tex"
+    assertEqual "unselected function importer remains legacy"
         LegacyMigrationGraph
         (classifyMigrationGraph selection functionImporter)
 
diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index 0448395..579a6b0 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -733,6 +733,12 @@ checksPhase53LibraryClosures = do
                                         (Module.sealedTypedModuleSemantic
                                             checked)))
                         inspect moduleAt
+                unselectedImporter <- parseFinalExactWorkspace
+                    prelude mounts "set/cantor.tex"
+                assertEqual "unselected function importer graph route"
+                    Migration.LegacyMigrationGraph
+                    (Migration.classifyMigrationGraph
+                        selection unselectedImporter)
                 checkRoot "set/bipartition.tex"
                     \moduleAt -> do
                         (_setParsed, setModule) <- moduleAt "set.tex"
@@ -861,6 +867,40 @@ checksPhase53LibraryClosures = do
                             uniquenessModule
                             Authority.Omitted
                         assertNoLocalSourceAxiom uniquenessModule
+                checkRoot "function.tex"
+                    \moduleAt -> do
+                        (_setParsed, setModule) <- moduleAt "set.tex"
+                        (_relationParsed, relationModule) <-
+                            moduleAt "relation.tex"
+                        (_uniquenessParsed, uniquenessModule) <-
+                            moduleAt "relation/uniqueness.tex"
+                        (_functionParsed, functionModule) <-
+                            moduleAt "function.tex"
+                        assertEqual "function semantic imports"
+                            [ preludeSemanticId
+                            , semanticId setModule
+                            , semanticId relationModule
+                            , semanticId uniquenessModule
+                            ]
+                            (Semantic.semanticInterfaceDirectInputs
+                                (Module.sealedTypedModuleSemantic
+                                    functionModule))
+                        assertCleanFactAlias
+                            functionModule
+                            "function_on_weaken_codom"
+                        assertFactAliasEscapeKind
+                            functionModule
+                            "function_apply_intro"
+                            Authority.SourceAxiom
+                        assertFactAliasEscapeKind
+                            functionModule
+                            "funs_circ"
+                            Authority.Omitted
+                        assertLocalDirectAuthorizationCount
+                            functionModule
+                            Authority.OmittedAuthorization
+                            6
+                        assertNoLocalSourceAxiom functionModule
   where
     semanticId =
         Semantic.semanticInterfaceAssertedId
@@ -1074,6 +1114,25 @@ assertNoLocalSourceAxiom sealed =
             Semantic.declarationValidationRecordCertificates validation
         ]
 
+assertLocalDirectAuthorizationCount
+    :: Module.SealedTypedModule
+    -> Authority.DirectAuthorization
+    -> Int
+    -> Assertion
+assertLocalDirectAuthorizationCount sealed expected expectedCount =
+    assertEqual
+        ("local " <> show expected <> " authorization count")
+        expectedCount
+        (length
+            [ ()
+            | batch <- Declaration.pendingModulePrefixBatches
+                (Module.sealedTypedModulePrefix sealed)
+            , validation <- Declaration.committedBatchProofValidations batch
+            , Authority.validationDirectAuthorization
+                (Semantic.proofValidationRecordCertificate validation)
+                == expected
+            ])
+
 assertSourceAxiomAlias
     :: Module.SealedTypedModule
     -> Text
@@ -4503,8 +4562,7 @@ routesProductionVerification =
             natRoot
         forM_
             [ ("bipartition", "set/bipartition.tex")
-            , ("relation properties", "relation/properties.tex")
-            , ("relation uniqueness", "relation/uniqueness.tex")
+            , ("function", "function.tex")
             ]
             \(label, path) ->
                 assertRoute ("typed " <> label)