Route complete graphs through one checker

3 files changed, 188 insertions, 2 deletions

diff --git a/source/Test/Unit/CommandLine.hs b/source/Test/Unit/CommandLine.hs
index 11b3a02..9d6c71d 100644
--- a/source/Test/Unit/CommandLine.hs
+++ b/source/Test/Unit/CommandLine.hs
@@ -3,7 +3,7 @@
 module Test.Unit.CommandLine (unitTests) where
 
 import Base
-import Api (VerificationReport(..))
+import Api (VerificationReport(..), VerificationRoute(..))
 import CommandLine
 import Report.Location (pattern Nowhere)
 
@@ -92,7 +92,8 @@ outcomeCases =
 emptyReport :: VerificationReport
 emptyReport =
     VerificationReport
-        { verificationLegacyDeclaredAssumptionCount = 0
+        { verificationRoute = LegacyVerificationRoute
+        , verificationLegacyDeclaredAssumptionCount = 0
         , verificationTypedDeclaredAssumptionCount = 0
         , verificationTrustedVampireCount = 0
         , verificationExplicitGapLocations = []
diff --git a/source/Test/Unit/Migration.hs b/source/Test/Unit/Migration.hs
index e53a076..49f05f1 100644
--- a/source/Test/Unit/Migration.hs
+++ b/source/Test/Unit/Migration.hs
@@ -4,8 +4,12 @@ module Test.Unit.Migration (unitTests) where
 
 import Base
 import Felix.Migration
+import Felix.Parse qualified as Parse
+import Felix.Prelude qualified as Prelude
 import Felix.Source
+import Syntax.Interface qualified as Syntax
 
+import System.Directory (getCurrentDirectory)
 import System.FilePath.Posix qualified as Posix
 import Test.Tasty
 import Test.Tasty.HUnit
@@ -16,6 +20,8 @@ unitTests =
     testGroup "Migration manifest"
         [ testCase "resolves references from prepared mount roots"
             resolvesManifestReferences
+        , testCase "selects one driver for the complete graph"
+            selectsCompleteGraphDriver
         ]
 
 resolvesManifestReferences :: Assertion
@@ -44,6 +50,57 @@ resolvesManifestReferences = do
                     Posix.</> safeRelativePathFilePath
                         (migrationModuleRefPath reference))
                 candidate
+    forM_ (toList typedMigrationModules) \reference ->
+        assertEqual
+            "typed fixture mount role"
+            MigrationProject
+            (migrationModuleRefRole reference)
+
+selectsCompleteGraphDriver :: Assertion
+selectsCompleteGraphDriver = do
+    root <- getCurrentDirectory
+    mounts <-
+        expectRight
+            =<< prepareSourceMounts
+                [ (sourceMountId "project", root)
+                , (sourceMountId "library", root Posix.</> "library")
+                , (sourceMountId "debug", root Posix.</> "debug")
+                ]
+    selection <-
+        expectRight
+            (resolveMigrationSelection mounts typedMigrationModules)
+    reserved <-
+        expectRight
+            =<< Prelude.parseReservedPreludeSource
+                Prelude.emptyBootstrapSourceInput
+    let bootstrapSyntax =
+            Parse.freshParsedModuleSyntaxInterface
+                (Prelude.reservedParsedPreludeModule reserved)
+        syntaxInputs source
+            | migrationSelectionContains selection source =
+                [bootstrapSyntax]
+            | otherwise = []
+        parseRoot path = do
+            request <- expectRight (searchedRoot path)
+            Parse.parseSourceWorkspaceMeasuredWithSyntaxInputs
+                mounts request syntaxInputs
+    (producer, _producerMeasurements) <-
+        expectRight
+            =<< parseRoot "test/phase3/typed-producer.tex"
+    assertEqual "selected root uses typed driver"
+        TypedMigrationGraph
+        (classifyMigrationGraph selection producer)
+    assertEqual "selected parse receives the bootstrap syntax input"
+        [Syntax.moduleSyntaxAssertedId bootstrapSyntax]
+        (Syntax.moduleSyntaxDirectInputs
+            (Parse.parsedModuleSyntaxInterface
+                (Parse.parsedWorkspaceRootModule producer)))
+    (importer, _importerMeasurements) <-
+        expectRight
+            =<< parseRoot "test/phase3/legacy-importer.tex"
+    assertEqual "unselected importer keeps the complete graph legacy"
+        LegacyMigrationGraph
+        (classifyMigrationGraph selection importer)
 
 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 37af621..d0c4489 100644
--- a/source/Test/Unit/Module.hs
+++ b/source/Test/Unit/Module.hs
@@ -3,20 +3,28 @@
 module Test.Unit.Module (unitTests) where
 
 import Base
+import Api qualified
 import Checking.Declaration qualified as Declaration
 import Checking.Foundation qualified as Foundation
 import Checking.Identity qualified as Identity
 import Checking.Module qualified as Module
 import Checking.Semantic qualified as Semantic
 import Felix.Module
+import Felix.Migration qualified as Migration
 import Felix.Parse qualified as Parse
 import Felix.Prelude qualified as Prelude
+import Felix.Source
 import Felix.Source.Content qualified as Content
 import Report.Location
+import Provers qualified
 import Syntax.Interface qualified as Syntax
 
 import Data.ByteString qualified as ByteString
 import Data.Text.Encoding qualified as Text
+import Control.Monad.Logger (runNoLoggingT)
+import Control.Monad.Reader (runReaderT)
+import System.Directory (getCurrentDirectory)
+import System.FilePath.Posix qualified as Posix
 import Test.Tasty
 import Test.Tasty.HUnit
 
@@ -28,6 +36,10 @@ unitTests =
             constructsEmptyBootstrap
         , testCase "identifies comment-only reserved input"
             identifiesCommentOnlyInput
+        , testCase "makes selected unsupported syntax terminal"
+            rejectsUnsupportedTypedSource
+        , testCase "routes production verification by complete graph"
+            routesProductionVerification
         ]
 
 constructsEmptyBootstrap :: Assertion
@@ -127,6 +139,122 @@ identifiesCommentOnlyInput = do
         (Syntax.moduleSyntaxAssertedId
             (Parse.freshParsedModuleSyntaxInterface firstParsed))
 
+rejectsUnsupportedTypedSource :: Assertion
+rejectsUnsupportedTypedSource = do
+    foundation <- expectRight Foundation.checkedFoundation
+    session <-
+        expectRight
+            =<< Module.buildBootstrapPreludeSession
+                foundation
+                unusedResolver
+    root <- getCurrentDirectory
+    mounts <-
+        expectRight
+            =<< prepareSourceMounts
+                [ (sourceMountId "project", root)
+                , (sourceMountId "library", root Posix.</> "library")
+                , (sourceMountId "debug", root Posix.</> "debug")
+                ]
+    selection <-
+        expectRight
+            (Migration.resolveMigrationSelection
+                mounts
+                Migration.typedMigrationModules)
+    let bootstrapSyntax =
+            Module.sealedTypedModuleSyntax
+                (Module.migrationPreludeModule session)
+        syntaxInputs source
+            | Migration.migrationSelectionContains selection source =
+                [bootstrapSyntax]
+            | otherwise = []
+    request <-
+        expectRight
+            (searchedRoot "test/phase3/typed-unsupported.tex")
+    (workspace, _measurements) <-
+        expectRight
+            =<< Parse.parseSourceWorkspaceMeasuredWithSyntaxInputs
+                mounts
+                request
+                syntaxInputs
+    assertEqual "selected graph classification"
+        Migration.TypedMigrationGraph
+        (Migration.classifyMigrationGraph selection workspace)
+    let parsed = Parse.parsedWorkspaceRootModule workspace
+    input <-
+        expectRight
+            (Module.typedModuleInput
+                foundation
+                session
+                unusedResolver
+                parsed
+                [])
+    Module.runTypedModule input >>= \case
+        Module.TypedModuleFailed
+                (Module.TypedActionFailed
+                    (Module.TypedUnsupportedBlock location))
+                prefix -> do
+            assertEqual "unsupported block location line"
+                1
+                (locLine location)
+            assertEqual "failure retains the initial module prefix"
+                0
+                (length
+                    (Declaration.pendingModulePrefixBatches prefix))
+        Module.TypedModuleOpenFailed err ->
+            assertFailure ("typed module did not open: " <> show err)
+        Module.TypedModuleFailed err _prefix ->
+            assertFailure ("unexpected typed failure: " <> show err)
+        Module.TypedModuleSucceeded{} ->
+            assertFailure "unsupported typed source was admitted"
+
+routesProductionVerification :: Assertion
+routesProductionVerification = do
+    producer <- verifyFixture "test/phase3/typed-producer.tex"
+    assertRoute "selected producer"
+        Api.TypedVerificationRoute
+        producer
+    importer <- verifyFixture "test/phase3/legacy-importer.tex"
+    assertRoute "unselected importer"
+        Api.LegacyVerificationRoute
+        importer
+  where
+    verifyFixture path =
+        runNoLoggingT
+            (runReaderT
+                (fst
+                    <$> Api.verifyMeasured
+                        (Provers.vampire
+                            "vampire"
+                            Provers.defaultTimeLimit
+                            Provers.defaultMemoryLimit)
+                        path)
+                testOptions)
+
+    assertRoute label expected = \case
+        Api.VerifiedWithTrustedVampire report ->
+            assertEqual label expected (Api.verificationRoute report)
+        Api.CompletedWithExplicitGaps report ->
+            assertFailure
+                (label <> " completed with gaps via "
+                    <> show (Api.verificationRoute report))
+        Api.VerificationFailure failure ->
+            assertFailure (label <> " failed: " <> show failure)
+
+testOptions :: Api.Options
+testOptions = Api.Options
+    { Api.inputPath = ""
+    , Api.withDump = Api.WithoutDump
+    , Api.withFilter = Api.WithoutFilter
+    , Api.withLogging = Api.WithoutLogging
+    , Api.withMemoryLimit = Provers.defaultMemoryLimit
+    , Api.withOmissions = Api.WithOmissions
+    , Api.withParseOnly = Api.WithoutParseOnly
+    , Api.withTimeLimit = Provers.defaultTimeLimit
+    , Api.withVersion = Api.WithoutVersion
+    , Api.withHtml = Api.WithoutHtml
+    , Api.withDumpPremselTraining = Api.WithoutDumpPremselTraining
+    }
+
 unusedResolver :: Declaration.VampireResolver
 unusedResolver =
     Declaration.vampireResolver \_prepared ->