Cut verification over to the typed driver

1 files changed, 35 insertions, 98 deletions

diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs
index 1874a98..35993cb 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -21,7 +21,6 @@ import Checking.Typed.Inductive qualified as TypedInductive
 import CommandLine qualified
 import Felix.Module
 import Felix.Math.Codec
-import Felix.Migration qualified as Migration
 import Felix.Parse qualified as Parse
 import Felix.Prelude qualified as Prelude
 import Felix.Source
@@ -35,8 +34,6 @@ import Syntax.Internal qualified as Internal
 import Syntax.Interface qualified as Syntax
 import Syntax.Pragma qualified as Pragma
 
-import Bound.Scope (fromScope)
-import Bound.Var (Var(..))
 import Control.Exception (bracket)
 import Control.Monad (foldM)
 import Data.ByteString qualified as ByteString
@@ -83,8 +80,6 @@ unitTests =
             retainsExactOmittedProofLocation
         , testCase "coalesces syntax without collapsing semantic imports"
             coalescesSharedDirectSyntax
-        , testCase "resets gloss state between modules"
-            resetsGlossStatePerModule
         , testCase "makes selected source errors terminal"
             rejectsUnsupportedTypedSource
         , testCase "compiles exact declarations across an import"
@@ -161,7 +156,7 @@ unitTests =
             classifiesTypedVampireFailures
         , testCase "retains the exact prefix before a later failure"
             retainsExactPrefixBeforeFailure
-        , testCase "routes production verification by complete graph"
+        , testCase "routes every production root through exact checking"
             routesProductionVerification
         , testCase "installs nonempty implicit prelude evidence"
             installsNonemptyImplicitPreludeEvidence
@@ -480,13 +475,13 @@ buildsConfinedFinalPrelude = do
                         pure
                         (FinalPrelude.finalPreludePublicRole
                             candidate roleName)
-            omega <- role Migration.PreludeOmegaObject
-            naturals <- role Migration.PreludeNaturalsAlias
+            omega <- role FinalPrelude.PreludeOmegaObject
+            naturals <- role FinalPrelude.PreludeNaturalsAlias
             assertEqual "naturals expands to Omega"
                 omega naturals
             traverse_
                 (void . role)
-                (Set.toList Migration.expectedFinalPreludePublicRoles)
+                (Set.toList FinalPrelude.expectedFinalPreludePublicRoles)
             let foundationTags = Set.fromList
                     [ tag
                     | batch <-
@@ -547,15 +542,15 @@ publishesFinalPreludeRoot = do
             freshMemo <- Store.newStoreMemo store
             session <-
                 expectRight
-                    =<< Module.buildFinalPreludeSession
+                    =<< Module.acquireFinalPreludeSession
                         freshMemo store foundation finalPreludeResolver
-            let input = Module.migrationPreludeInput session
-                sealed = Module.migrationPreludeModule session
+            let input = Module.finalPreludeInput session
+                sealed = Module.finalPreludeModule session
                 syntax = Module.sealedTypedModuleSyntax sealed
                 semantic = Module.sealedTypedModuleSemantic sealed
             assertEqual "empty store constructs the final-prelude root"
                 Module.ModuleRootMiss
-                (Module.migrationPreludeAcquisition session)
+                (Module.finalPreludeAcquisition session)
             assertEqual "final prelude owner"
                 preludeModuleName
                 (Module.identifiedModuleOwner input)
@@ -564,12 +559,12 @@ publishesFinalPreludeRoot = do
                 (Semantic.semanticInterfaceDirectInputs semantic)
             warmMemo <- Store.newStoreMemo store
             warmSession <- expectRight
-                =<< Module.buildFinalPreludeSession
+                =<< Module.acquireFinalPreludeSession
                     warmMemo store foundation unusedResolver
-            let cached = Module.migrationPreludeModule warmSession
+            let cached = Module.finalPreludeModule warmSession
             assertEqual "persisted final-prelude root is a cache hit"
                 Module.ModuleRootHit
-                (Module.migrationPreludeAcquisition warmSession)
+                (Module.finalPreludeAcquisition warmSession)
             assertEqual "generic root syntax"
                 syntax
                 (Module.sealedTypedModuleSyntax cached)
@@ -655,11 +650,11 @@ checksProtectedNatClosure = do
             let preludeSyntaxId =
                     Syntax.moduleSyntaxAssertedId
                         (Module.sealedTypedModuleSyntax
-                            (Module.migrationPreludeModule prelude))
+                            (Module.finalPreludeModule prelude))
                 preludeSemanticId =
                     Semantic.semanticInterfaceAssertedId
                         (Module.sealedTypedModuleSemantic
-                            (Module.migrationPreludeModule prelude))
+                            (Module.finalPreludeModule prelude))
             forM_
                 (toList
                     (Parse.parsedWorkspaceImportedBeforeImporter workspace))
@@ -710,7 +705,7 @@ checksProtectedNatClosure = do
                 ( pairIdentity
                     `Set.notMember` Core.canonicalTermGlobals consBody
                 )
-            let preludeModule = Module.migrationPreludeModule prelude
+            let preludeModule = Module.finalPreludeModule prelude
             preludeSuccessor <-
                 localObjectAliasTarget preludeModule "prelude_successor"
             sourceSuccessor <- localObjectAliasTarget sucModule "suc"
@@ -1065,18 +1060,10 @@ coalescesSharedDirectSyntax = do
                 , (sourceMountId "library", root Posix.</> "library")
                 , (sourceMountId "debug", root Posix.</> "debug")
                 ]
-    selection <-
-        expectRight
-            (Migration.resolveMigrationSelection
-                mounts
-                Migration.typedMigrationModules)
     let bootstrapSyntax =
             Module.sealedTypedModuleSyntax
                 (Module.bootstrapPreludeModule session)
-        syntaxInputs source
-            | Migration.migrationSelectionContains selection source =
-                [bootstrapSyntax]
-            | otherwise = []
+        syntaxInputs _source = [bootstrapSyntax]
     request <-
         expectRight
             (searchedRoot "test/phase3/typed-shared-root.tex")
@@ -1086,9 +1073,6 @@ coalescesSharedDirectSyntax = do
                 mounts
                 request
                 syntaxInputs
-    assertEqual "selected shared-syntax graph"
-        Migration.TypedMigrationGraph
-        (Migration.classifyMigrationGraph selection workspace)
     case Parse.parsedWorkspaceModules workspace of
         [firstParsed, secondParsed, rootParsed] -> do
             first <- seal foundation session firstParsed []
@@ -1151,31 +1135,6 @@ coalescesSharedDirectSyntax = do
                 assertFailure "empty typed module did not seal"
                     >> fail "unreachable"
 
-resetsGlossStatePerModule :: Assertion
-resetsGlossStatePerModule = do
-    blocks <- Api.gloss "test/phase3/gloss-root.tex"
-    binders <- traverse signatureBinder blocks
-    assertEqual "fresh variables restart at each module boundary"
-        [Internal.FreshVar 0, Internal.FreshVar 0, Internal.FreshVar 1]
-        binders
-  where
-    signatureBinder = \case
-        Internal.BlockSig
-                _location
-                _marker
-                _assumptions
-                (Internal.SignatureFormula
-                    (Internal.Quantified Internal.Universally scope)) ->
-            case nubOrd [binder | B binder <- toList (fromScope scope)] of
-                [binder] -> pure binder
-                binders ->
-                    assertFailure
-                        ("unexpected signature binders: " <> show binders)
-                        >> fail "unreachable"
-        block ->
-            assertFailure ("unexpected glossed block: " <> show block)
-                >> fail "unreachable"
-
 rejectsUnsupportedTypedSource :: Assertion
 rejectsUnsupportedTypedSource = do
     result <-
@@ -1410,7 +1369,7 @@ compilesExactStructures = do
                 [ operation
                 | descriptor <- semanticStructureDescriptors
                     (Module.sealedTypedModuleSemantic
-                        (Module.migrationPreludeModule prelude))
+                        (Module.finalPreludeModule prelude))
                 , operation <-
                     Semantic.semanticStructureDescriptorOperations descriptor
                 ]
@@ -1584,7 +1543,7 @@ compilesExactStructures = do
                         <> " checked modules")
                     >> fail "unreachable"
       where
-        preludeModule = Module.migrationPreludeModule prelude
+        preludeModule = Module.finalPreludeModule prelude
 
         persistAndLoad memo parents parsed sealedModule = do
             let input = Module.identifiedPhysicalModule parsed
@@ -1750,7 +1709,7 @@ compilesContextualAbbreviations = do
             cached <- expectRight
                 (Module.cachedSealedTypedModule
                     foundation
-                    [Module.migrationPreludeModule prelude]
+                    [Module.finalPreludeModule prelude]
                     installation)
             assertEqual "cached contextual semantic target"
                 semantic
@@ -5044,7 +5003,7 @@ loadsCachedExactProducerForFreshImporter = do
         memo <- Store.newStoreMemo store
         prelude <-
             expectRight
-                =<< Module.buildFinalPreludeSession
+                =<< Module.acquireFinalPreludeSession
                     memo store foundation unusedResolver
         preludeVisits <- Store.storeMemoVisits memo
         repository <- getCurrentDirectory
@@ -5056,7 +5015,7 @@ loadsCachedExactProducerForFreshImporter = do
                     (Parse.parsedWorkspaceImportedBeforeImporter workspace)
             preludeSemantic =
                 Module.sealedTypedModuleSemantic
-                    (Module.migrationPreludeModule prelude)
+                    (Module.finalPreludeModule prelude)
             preludeId =
                 Semantic.semanticInterfaceAssertedId preludeSemantic
             theory = Identity.theoryId foundation
@@ -5331,9 +5290,6 @@ classifiesTypedVampireFailures = do
                         verify "test/phase5/exact-runtime-failure.tex"
                     case result of
                         Api.VerificationFailure report failed -> do
-                            assertEqual "typed failure retains typed report"
-                                Api.TypedVerificationRoute
-                                (Api.verificationRoute report)
                             assertEqual "typed failure has no direct escapes"
                                 []
                                 (Api.verificationDirectEscapes report)
@@ -5608,18 +5564,14 @@ routesProductionVerification =
         setPermissions executable
             (setOwnerExecutable True permissions)
         producer <- verifyFixture executable "test/phase3/typed-producer.tex"
-        assertRoute "selected producer"
-            Api.TypedVerificationRoute
-            producer
+        assertTypedSuccess "exact producer" producer
         selectedRuns <- runCount counter
-        assertBool "selected roots constructed the final prelude"
+        assertBool "ordinary roots construct the final prelude"
             (selectedRuns > 0)
-        importer <- verifyFixture executable "test/phase3/legacy-importer.tex"
-        assertRoute "unselected importer"
-            Api.LegacyVerificationRoute
-            importer
-        assertEqual "legacy root did not construct the final prelude"
-            selectedRuns
+        importer <- verifyFixture executable "test/phase3/typed-importer.tex"
+        assertTypedSuccess "ordinary importer" importer
+        assertBool "every root constructs the final prelude"
+            . (> selectedRuns)
             =<< runCount counter
   where
     verifyFixture executable path =
@@ -5636,18 +5588,6 @@ routesProductionVerification =
     runCount path =
         length . StrictText.lines . StrictText.pack <$> readFile path
 
-    assertRoute label expected = \case
-        Api.VerificationCompleted report ->
-            assertEqual label expected (Api.verificationRoute report)
-        Api.CompletedWithExplicitGaps report ->
-            assertFailure
-                (label <> " completed with gaps via "
-                    <> show (Api.verificationRoute report))
-        Api.VerificationFailure _report failure ->
-            assertFailure (label <> " failed: " <> show failure)
-        Api.VerificationCheckingFailure _report failure ->
-            assertFailure (label <> " failed: " <> show failure)
-
 installsNonemptyImplicitPreludeEvidence :: Assertion
 installsNonemptyImplicitPreludeEvidence = do
     foundation <- expectRight Foundation.checkedFoundation
@@ -6069,13 +6009,13 @@ parseExactWorkspace bootstrap mounts relative =
         relative
 
 parseFinalExactWorkspace
-    :: Module.MigrationPreludeSession
+    :: Module.FinalPreludeSession
     -> SourceMounts
     -> FilePath
     -> IO Parse.ParsedSourceWorkspace
 parseFinalExactWorkspace prelude mounts relative =
     parseExactWorkspaceWithPrelude
-        (Module.migrationPreludeModule prelude)
+        (Module.finalPreludeModule prelude)
         mounts
         relative
 
@@ -6140,7 +6080,7 @@ compileParsedWorkspaceWithValidation
 
 compileFinalParsedWorkspaceWithResolver
     :: Foundation.CheckedFoundation
-    -> Module.MigrationPreludeSession
+    -> Module.FinalPreludeSession
     -> Declaration.VampireResolver
     -> Parse.ParsedSourceWorkspace
     -> IO [Module.SealedTypedModule]
@@ -6207,13 +6147,10 @@ compileParsedWorkspaceWithReadiness
 
 assertTypedSuccess :: String -> Api.VerificationResult -> Assertion
 assertTypedSuccess label = \case
-    Api.VerificationCompleted report ->
-        assertEqual label Api.TypedVerificationRoute
-            (Api.verificationRoute report)
-    Api.CompletedWithExplicitGaps report ->
-        assertFailure
-            (label <> " completed with gaps via "
-                <> show (Api.verificationRoute report))
+    Api.VerificationCompleted _report ->
+        pure ()
+    Api.CompletedWithExplicitGaps _report ->
+        assertFailure (label <> " completed with gaps")
     Api.VerificationFailure _report failure ->
         assertFailure (label <> " failed: " <> show failure)
     Api.VerificationCheckingFailure _report failure ->
@@ -6243,8 +6180,8 @@ acquireFinalPreludeSession
     -> IO
         (Either
             Module.FinalPreludeReadinessError
-            Module.MigrationPreludeSession)
+            Module.FinalPreludeSession)
 acquireFinalPreludeSession store foundation resolver = do
     memo <- Store.newStoreMemo store
-    Module.buildFinalPreludeSession
+    Module.acquireFinalPreludeSession
         memo store foundation resolver