path: root/source/Test/Unit/Source.hs

{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}

module Test.Unit.Source (unitTests) where

import Base
import Checking qualified
import Checking.Backend.Problem qualified as Backend
import Checking.Backend.Reconstruction qualified as Reconstruction
import Checking.Core qualified as Core
import Checking.Facts qualified as Facts
import Checking.Foundation qualified as Foundation
import Checking.Identity qualified as Identity
import Checking.Kernel.Derivation qualified as Derivation
import Checking.Legacy qualified as Legacy
import Checking.Obligation qualified as Obligation
import Checking.Transition qualified as Transition
import Felix.Cache.Codec qualified as Cache
import Felix.Module qualified as Module
import Felix.Parse qualified as Parse
import Felix.Parsed.Identity qualified as ParsedIdentity
import Felix.Parsed.Payload qualified as Parsed
import Felix.Source
import Felix.Source.Content qualified as Content
import Felix.Source.Graph
import Felix.Store qualified as Store
import Meaning qualified
import Provers qualified
import Report.Location
    ( FileId(..)
    , FileIdAllocator(..)
    , Location(..)
    , LocationRegistrationError(..)
    , pattern Nowhere
    , allocateFileId
    , locColumn
    , locFile
    , locFileId
    , locLine
    , lookupFileIdentityPath
    )
import Syntax.Abstract qualified as Raw
import Syntax.Adapt qualified as Adapt
import Syntax.Interface qualified as Interface
import Syntax.Internal
import Syntax.Token (runLexer)

import Bound.Scope (toScope)
import Control.Exception (bracket, evaluate, try)
import Control.Monad (foldM)
import Control.Monad.Logger (runNoLoggingT)
import Data.ByteString qualified as ByteString
import Data.HashMap.Strict qualified as HashMap
import Data.IORef
import Data.List qualified as List
import Data.List.NonEmpty qualified as NonEmpty
import Data.Set qualified as Set
import Data.Text qualified as Text
import Data.Vector qualified as Vector
import Data.Word (Word8, Word16)
import Database.SQLite.Simple qualified as SQLite
import System.Directory qualified as Directory
import System.FilePath.Posix qualified as Posix
import System.Posix.Files qualified as PosixFiles
import Test.Tasty
import Test.Tasty.HUnit


unitTests :: TestTree
unitTests = testGroup "Source resolution"
    [ testCase "validates mount-root-relative POSIX paths" validatesRelativePaths
    , testCase "rejects duplicate source mount ids" rejectsDuplicateMountIds
    , testCase "rejects duplicate canonical mount roots" rejectsDuplicateMountRoots
    , testCase "permits missing and rejects non-directory mounts"
        validatesMountRootTypes
    , testCase "rejects relative exact roots" rejectsRelativeExactRoots
    , testCase "retains exact root spelling as diagnostic trivia" retainsRootSpelling
    , testCase "searched and exact roots share canonical identity" rootFormsShareIdentity
    , testCase "attributes nested sources to the most specific mount" attributesNestedSources
    , testCase "configured order selects searched candidates" candidateOrderSelectsWinner
    , testCase "rejects a higher-priority special source"
        rejectsHigherPrioritySpecialSource
    , testCase "rejects exact roots outside configured mounts" rejectsOutsideExactRoot
    , testCase "loads source text as strict UTF-8" loadsStrictUtf8
    , testCase "reports malformed UTF-8 sequence starts"
        reportsInvalidUtf8Offsets
    , testCase "reserves the all-ones file identifier"
        preservesReservedFileId
    , testCase "builds an imported-before-importer source graph" buildsSourceGraph
    , testCase "orders sibling imports by textual occurrence"
        ordersSiblingImports
    , testCase "orders shared dependencies before their importers"
        ordersSharedDependencies
    , testCase "retains repeated import-edge occurrences" retainsRepeatedImports
    , testCase "deduplicates canonical source nodes" deduplicatesCanonicalNodes
    , testCase "reports missing imports at their source location" reportsMissingImports
    , testCase "rejects unsafe imports at their source location" rejectsUnsafeImports
    , testCase "reports the located import cycle chain" reportsImportCycles
    , testCase "rejects malformed imported source before discovery" rejectsMalformedImportedSource
    , testCase "builds empty modules through the ordinary pipeline"
        buildsEmptyModules
    , testCase "identifies owner-independent parsed modules"
        identifiesOwnerIndependentParsedModules
    , testCase "keys effective direct syntax inputs"
        keysEffectiveDirectSyntaxInputs
    , testCase "reuses exact parsed syntax on a warm pass"
        reusesExactParsedSyntax
    , testCase "rejects a corrupted cached declaration anchor"
        rejectsCorruptedCachedDeclarationAnchor
    , testCase "parses source-local blocks in graph order" parsesSourceGraph
    , testCase "assigns and reserves dense legacy module positions"
        reservesLegacyModulePositions
    , testCase "admits complete legacy declaration batches"
        admitsLegacyDeclarations
    , testCase "publishes deterministic legacy import views"
        publishesLegacyImportViews
    , testCase "publishes typed signatures and facts through transition modules"
        publishesTransitionSignatures
    , testCase "rejects cached global types from another builder"
        rejectsForeignCachedGlobalType
    , testCase "authorizes exact typed Vampire requests"
        authorizesTypedVampireRequests
    , testCase "enforces and replays direct inductive guards"
        publishesTypedInductive
    , testCase "does not leak syntax between sibling imports"
        rejectsSiblingSyntaxLeakage
    , testCase "parses source fixity levels and grouping"
        parsesSourceFixities
    , testCase "parses cdot and symdiff fixities"
        parsesLibraryFixities
    , testCase "validates source pragma associations"
        validatesSourcePragmaAssociations
    , testCase "rejects fixed-base category mismatches"
        rejectsFixedBaseCategoryMismatch
    , testCase "retains multi-item syntax occurrence order"
        retainsMultiItemSyntaxOccurrences
    , testCase "propagates and coalesces imported syntax"
        propagatesImportedSyntax
    , testCase "rejects unequal imported syntax"
        rejectsUnequalImportedSyntax
    , testCase "qualifies same-display cross-mount collisions"
        distinguishesPhysicalSourceLocations
    , testCase "retains each workspace location display path"
        retainsWorkspaceLocationDisplayPath
    , testCase "reports imported lexer errors before importer errors"
        reportsImportedLexerErrorFirst
    , testCase "returns malformed lexical declarations as typed errors"
        reportsMalformedLexicalDeclaration
    , testCase "validates inductive function patterns during scanning"
        rejectsMalformedInductivePattern
    , testCase "scans, parses, and checks adjective signatures"
        acceptsAdjectiveSignature
    , testCase "rejects unresolved quantified symbolic-signature terms"
        rejectsQuantifiedSymbolicSignatureTerm
    , testCase "rejects malformed math-led signature heads"
        rejectsMalformedSignatureHead
    , testCase "locates conflicting declarations within one environment"
        reportsSameSourceLexiconCollision
    , testCase "accepts the first source declaration of a built-in pattern"
        acceptsBuiltinSourceDeclaration
    , testCase "keeps the built-in marker for a prefix predicate declaration"
        acceptsBuiltinPrefixPredicateDeclaration
    , testCase "rejects duplicate fixed-base semantics during checking"
        rejectsDuplicateFixedBaseSemantics
    , testCase "does not rescan repeated canonical imports"
        avoidsAliasImportLexiconCollision
    , testCase "parses loaded sources without rereading files" parsesWithoutRereading
    , testCase "returns source-local failures after prior chunk callbacks"
        returnsSourceParseFailures
    ]

validatesRelativePaths :: Assertion
validatesRelativePaths = do
    assertRight (safeRelativePath "theory/set.tex")
    assertRight (safeRelativePath "theory\\set.tex")
    assertLeft EmptyRelativePath (safeRelativePath "")
    assertLeft AbsoluteRelativePath (safeRelativePath "/theory.tex")
    assertLeft CurrentDirectoryComponent (safeRelativePath "./theory.tex")
    assertLeft ParentDirectoryComponent (safeRelativePath "a/../theory.tex")
    assertLeft EmptyPathComponent (safeRelativePath "a//theory.tex")
    assertLeft EmptyPathComponent (safeRelativePath "a/")
    assertLeft NullPathCharacter (safeRelativePath "a\0b")

rejectsDuplicateMountIds :: Assertion
rejectsDuplicateMountIds =
    withTemporaryDirectory "felix-source-duplicate-id" \temp -> do
        result <- prepareSourceMounts
            [ (sourceMountId "same", temp Posix.</> "one")
            , (sourceMountId "same", temp Posix.</> "two")
            ]
        assertEqual
            "duplicate id"
            (Left (DuplicateSourceMountId (sourceMountId "same")))
            result

rejectsDuplicateMountRoots :: Assertion
rejectsDuplicateMountRoots =
    withTemporaryDirectory "felix-source-duplicate-root" \temp -> do
        result <- prepareSourceMounts
            [ (sourceMountId "one", temp)
            , (sourceMountId "two", temp Posix.</> ".")
            ]
        canonical <- Directory.canonicalizePath temp
        case result of
            Left (DuplicateCanonicalMountRoot root firstId secondId) -> do
                assertEqual "canonical root" canonical (canonicalPathFilePath root)
                assertEqual "first mount id" (sourceMountId "one") firstId
                assertEqual "second mount id" (sourceMountId "two") secondId
            Left err ->
                assertFailure ("expected DuplicateCanonicalMountRoot, got " <> show err)
            Right mounts ->
                assertFailure ("expected duplicate-root rejection, got " <> show mounts)

validatesMountRootTypes :: Assertion
validatesMountRootTypes =
    withTemporaryDirectory "felix-source-mount-type" \temp -> do
        let ident = sourceMountId "project"
            missing = temp Posix.</> "missing"
            regularFile = temp Posix.</> "file"
        assertRight =<< prepareSourceMounts [(ident, missing)]

        writeFile regularFile ""
        result <- prepareSourceMounts [(ident, regularFile)]
        case result of
            Left SourceMountNotDirectory{} ->
                pure ()
            Left err ->
                assertFailure
                    ("expected SourceMountNotDirectory, got " <> show err)
            Right mounts ->
                assertFailure
                    ("expected non-directory rejection, got " <> show mounts)

rejectsRelativeExactRoots :: Assertion
rejectsRelativeExactRoots =
    assertEqual
        "relative exact roots are rejected"
        (Left (ExistingRootNotAbsolute "entry.tex"))
        =<< existingRoot "entry.tex"

retainsRootSpelling :: Assertion
retainsRootSpelling =
    withTemporaryDirectory "felix-source-root-spelling" \temp -> do
        let source = temp Posix.</> "entry.tex"
            alias = temp Posix.</> "entry-alias.tex"
        writeFile source ""
        Directory.createFileLink source alias
        direct <- expectRight =<< existingRoot source
        throughAlias <- expectRight =<< existingRoot alias
        assertEqual "canonical request identity" direct throughAlias
        assertEqual "diagnostic spelling" alias
            (rootRequestSpelling throughAlias)

rootFormsShareIdentity :: Assertion
rootFormsShareIdentity =
    withTemporaryDirectory "felix-source-root-identity" \temp -> do
        let source = temp Posix.</> "entry.tex"
        writeFile source "source"
        mounts <- oneMount "project" temp
        searched <- expectRight (searchedRoot "entry.tex")
        exact <- expectRight =<< existingRoot source
        searchedLoaded <- expectRight =<< resolveAndLoadRoot mounts searched
        exactLoaded <- expectRight =<< resolveAndLoadRoot mounts exact
        assertEqual "loaded source" searchedLoaded exactLoaded
        assertEqual "source mount"
            (resolvedSourceMount (loadedSource searchedLoaded))
            (resolvedSourceMount (loadedSource exactLoaded))
        assertEqual "mount-relative source path"
            (resolvedSourceRelativePath (loadedSource searchedLoaded))
            (resolvedSourceRelativePath (loadedSource exactLoaded))

attributesNestedSources :: Assertion
attributesNestedSources =
    withTemporaryDirectory "felix-source-nested-mount" \temp -> do
        let nested = temp Posix.</> "library"
            source = nested Posix.</> "entry.tex"
        Directory.createDirectory nested
        writeFile source "source"
        exact <- expectRight =<< existingRoot source
        outerFirst <- expectRight =<< prepareSourceMounts
            [ (sourceMountId "project", temp)
            , (sourceMountId "library", nested)
            ]
        innerFirst <- expectRight =<< prepareSourceMounts
            [ (sourceMountId "library", nested)
            , (sourceMountId "project", temp)
            ]
        searched <- expectRight (searchedRoot "library/entry.tex")
        outerFirstSource <- loadedSource <$> (expectRight =<< resolveAndLoadRoot outerFirst exact)
        innerFirstSource <- loadedSource <$> (expectRight =<< resolveAndLoadRoot innerFirst exact)
        searchedSource <- loadedSource <$> (expectRight =<< resolveAndLoadRoot outerFirst searched)
        assertEqual "order-independent attribution" outerFirstSource innerFirstSource
        assertEqual "root-form-independent attribution" outerFirstSource searchedSource
        assertEqual "most specific mount" (sourceMountId "library") (resolvedSourceMount outerFirstSource)
        assertEqual "mount-relative identity" "entry.tex"
            (safeRelativePathFilePath (resolvedSourceRelativePath outerFirstSource))

candidateOrderSelectsWinner :: Assertion
candidateOrderSelectsWinner =
    withTemporaryDirectory "felix-source-precedence" \temp -> do
        let firstRoot = temp Posix.</> "first"
            secondRoot = temp Posix.</> "second"
            firstSource = firstRoot Posix.</> "entry.tex"
            secondSource = secondRoot Posix.</> "entry.tex"
        Directory.createDirectory firstRoot
        Directory.createDirectory secondRoot
        writeFile firstSource "first"
        writeFile secondSource "second"
        request <- expectRight (searchedRoot "entry.tex")
        firstMounts <- expectRight =<< prepareSourceMounts
            [ (sourceMountId "first", firstRoot)
            , (sourceMountId "second", secondRoot)
            ]
        secondMounts <- expectRight =<< prepareSourceMounts
            [ (sourceMountId "second", secondRoot)
            , (sourceMountId "first", firstRoot)
            ]
        firstWinner <- expectRight =<< resolveAndLoadRoot firstMounts request
        secondWinner <- expectRight =<< resolveAndLoadRoot secondMounts request
        assertEqual "first configured source" "first" (loadedText firstWinner)
        assertEqual "reversed configured source" "second" (loadedText secondWinner)

rejectsHigherPrioritySpecialSource :: Assertion
rejectsHigherPrioritySpecialSource =
    withTemporaryDirectory "felix-source-special-precedence" \temp -> do
        let higherRoot = temp Posix.</> "higher"
            lowerRoot = temp Posix.</> "lower"
            higherSource = higherRoot Posix.</> "entry.tex"
            lowerSource = lowerRoot Posix.</> "entry.tex"
        Directory.createDirectory higherRoot
        Directory.createDirectory lowerRoot
        PosixFiles.createNamedPipe higherSource PosixFiles.ownerModes
        writeFile lowerSource "ordinary source"
        mounts <- expectRight =<< prepareSourceMounts
            [ (sourceMountId "higher", higherRoot)
            , (sourceMountId "lower", lowerRoot)
            ]
        request <- expectRight (searchedRoot "entry.tex")
        result <- resolveRoot mounts request
        case result of
            Left
                (SelectedSourceNotRegular
                    (SearchedRootLookup relative)
                    selectedPath
                    canonical) -> do
                        assertEqual "searched path"
                            "entry.tex"
                            (safeRelativePathFilePath relative)
                        assertEqual "selected higher candidate"
                            higherSource
                            selectedPath
                        canonicalHigher <-
                            Directory.canonicalizePath higherSource
                        assertEqual "selected canonical target"
                            canonicalHigher
                            (canonicalPathFilePath canonical)
            Left err ->
                assertFailure
                    ("expected SelectedSourceNotRegular, got " <> show err)
            Right source ->
                assertFailure
                    ("expected special-source rejection, got " <> show source)

rejectsOutsideExactRoot :: Assertion
rejectsOutsideExactRoot =
    withTemporaryDirectory "felix-source-outside-root" \temp -> do
        let mountRoot = temp Posix.</> "mount"
            outsideRoot = temp Posix.</> "outside"
            source = outsideRoot Posix.</> "entry.tex"
        Directory.createDirectory mountRoot
        Directory.createDirectory outsideRoot
        writeFile source "source"
        mounts <- oneMount "project" mountRoot
        exact <- expectRight =<< existingRoot source
        result <- resolveAndLoadRoot mounts exact
        case result of
            Left (RootOutsideConfiguredMount spelling _canonical) ->
                assertEqual "exact-root diagnostic spelling" source spelling
            Left err ->
                assertFailure ("expected RootOutsideConfiguredMount, got " <> show err)
            Right loaded ->
                assertFailure ("expected outside-root rejection, got " <> show loaded)

loadsStrictUtf8 :: Assertion
loadsStrictUtf8 =
    withTemporaryDirectory "felix-source-utf8" \temp -> do
        let source = temp Posix.</> "unicode.tex"
            bytes =
                ByteString.pack
                    [ 0xCE, 0xB1, 0x20, 0xE2
                    , 0x88, 0x88, 0x20, 0x41
                    ]
        ByteString.writeFile source bytes
        mounts <- oneMount "project" temp
        request <- expectRight (searchedRoot "unicode.tex")
        loaded <- expectRight =<< resolveAndLoadRoot mounts request
        assertEqual "exact bytes" bytes (loadedBytes loaded)
        assertEqual "decoded text" ("α ∈ A" :: Text) (loadedText loaded)
        assertEqual
            "byte count"
            (fromIntegral (ByteString.length bytes))
            (loadedByteCount loaded)
        let identifier =
                Content.sourceContentId loaded
        assertEqual
            "content identity cache round trip"
            (Right identifier)
            (Cache.decodeCache
                Content.getSourceContentIdCache
                (Cache.encodeCache
                    (Content.putSourceContentIdCache
                        identifier)))
        ByteString.writeFile source (bytes <> "\n")
        changed <- expectRight
            =<< loadResolvedSource (loadedSource loaded)
        assertBool
            "exact byte edits change source identity"
            (identifier /= Content.sourceContentId changed)

reportsInvalidUtf8Offsets :: Assertion
reportsInvalidUtf8Offsets =
    withTemporaryDirectory "felix-source-invalid-utf8" \temp -> do
        let source = temp Posix.</> "invalid.tex"
        mounts <- oneMount "project" temp
        request <- expectRight (searchedRoot "invalid.tex")
        let assertOffset label bytes expected = do
                ByteString.writeFile source (ByteString.pack bytes)
                result <- resolveAndLoadRoot mounts request
                case result of
                    Left (SourceDecodeError _source offset) ->
                        assertEqual label expected offset
                    Left err ->
                        assertFailure
                            ("expected SourceDecodeError, got " <> show err)
                    Right loaded ->
                        assertFailure
                            ("expected malformed UTF-8 rejection, got "
                                <> show loaded)
        assertOffset "malformed sequence start" [0x61, 0xC3, 0x28] 1
        assertOffset "incomplete sequence start" [0x61, 0xC3] 1

preservesReservedFileId :: Assertion
preservesReservedFileId =
    case allocateFileId boundaryAllocator of
        Left err ->
            assertFailure
                ("could not allocate last available file id: " <> show err)
        Right (fileId, exhaustedAllocator) -> do
            assertEqual "last available file id"
                (maxBound - 1)
                (unFileId fileId)
            assertBool "allocator returned reserved file id"
                (unFileId fileId /= maxBound)
            assertEqual "allocator reports exhaustion"
                (Left FileIdSpaceExhausted)
                (allocateFileId exhaustedAllocator)
  where
    boundaryAllocator =
        FileIdAllocator
            (fromIntegral (maxBound :: Word16) - 1)

buildsSourceGraph :: Assertion
buildsSourceGraph =
    withTemporaryDirectory "felix-source-graph" \temp -> do
        writeTheory (temp Posix.</> "shared.tex") [] "shared"
        writeTheory (temp Posix.</> "entry.tex") ["shared.tex"] "entry"
        mounts <- oneMount "project" temp
        request <- expectRight (searchedRoot "entry.tex")
        graph <- expectRight =<< buildResolvedSourceGraph mounts request
        assertEqual "two source nodes" 2 (length (sourceGraphNodes graph))
        case sourceGraphImportEdges graph of
            [edge] -> do
                assertEqual "root imports" (sourceGraphRoot graph) (sourceImportingNode edge)
                assertEqual
                    "imported-before-importer order"
                    [sourceImportedNode edge, sourceGraphRoot graph]
                    ( sourceNodeCanonicalPathForTest
                        <$> toList
                            (sourceGraphImportedBeforeImporter graph)
                    )
                assertEqual "import location line" 1
                    (locLine (importLocation (sourceImportReference edge)))
                assertEqual "selected location path" "entry.tex"
                    (locFile (importLocation (sourceImportReference edge)))
            edges ->
                assertFailure ("expected one import edge, got " <> show edges)

ordersSiblingImports :: Assertion
ordersSiblingImports =
    withTemporaryDirectory "felix-source-sibling-order" \temp -> do
        writeTheory (temp Posix.</> "a.tex") [] "a"
        writeTheory (temp Posix.</> "b.tex") [] "b"
        writeTheory
            (temp Posix.</> "entry.tex")
            ["a.tex", "b.tex"]
            "entry"
        graph <- buildSearchedGraph temp "entry.tex"
        order <- sourceGraphOrderPaths graph
        assertEqual "DFS completion order"
            ["a.tex", "b.tex", "entry.tex"]
            order

ordersSharedDependencies :: Assertion
ordersSharedDependencies =
    withTemporaryDirectory "felix-source-shared-order" \temp -> do
        writeTheory (temp Posix.</> "shared.tex") [] "shared"
        writeTheory (temp Posix.</> "a.tex") ["shared.tex"] "a"
        writeTheory (temp Posix.</> "b.tex") ["shared.tex"] "b"
        writeTheory
            (temp Posix.</> "entry.tex")
            ["a.tex", "b.tex"]
            "entry"
        graph <- buildSearchedGraph temp "entry.tex"
        order <- sourceGraphOrderPaths graph
        assertEqual "shared dependency occurs once before both importers"
            ["shared.tex", "a.tex", "b.tex", "entry.tex"]
            order

retainsRepeatedImports :: Assertion
retainsRepeatedImports =
    withTemporaryDirectory "felix-source-repeated-import" \temp -> do
        writeTheory (temp Posix.</> "shared.tex") [] "shared"
        writeTheory
            (temp Posix.</> "entry.tex")
            ["shared.tex", "shared.tex"]
            "entry"
        graph <- buildSearchedGraph temp "entry.tex"
        assertEqual "canonical node count" 2 (length (sourceGraphNodes graph))
        assertEqual "repeated edge count" 2 (length (sourceGraphImportEdges graph))

deduplicatesCanonicalNodes :: Assertion
deduplicatesCanonicalNodes =
    withTemporaryDirectory "felix-source-canonical-dedup" \temp -> do
        let shared = temp Posix.</> "shared.tex"
            alias = temp Posix.</> "alias.tex"
        writeTheory shared [] "shared"
        Directory.createFileLink shared alias
        writeTheory
            (temp Posix.</> "entry.tex")
            ["shared.tex", "alias.tex"]
            "entry"
        graph <- buildSearchedGraph temp "entry.tex"
        assertEqual "one node for symlink aliases" 2 (length (sourceGraphNodes graph))
        case sourceGraphImportEdges graph of
            [firstEdge, secondEdge] ->
                assertEqual
                    "both occurrences reach one node"
                    (sourceImportedNode firstEdge)
                    (sourceImportedNode secondEdge)
            edges ->
                assertFailure ("expected two import edges, got " <> show edges)

reportsMissingImports :: Assertion
reportsMissingImports =
    withTemporaryDirectory "felix-source-missing-import" \temp -> do
        writeFile
            (temp Posix.</> "entry.tex")
            (unlines
                [ "% heading"
                , "\\import{missing.tex}"
                , theoryBlock "entry"
                ])
        mounts <- oneMount "project" temp
        request <- expectRight (searchedRoot "entry.tex")
        result <- buildResolvedSourceGraph mounts request
        case result of
            Left (SourceNotFound (ImportedSourceLookup _ reference) _candidates) -> do
                assertEqual "missing import line" 2 (locLine (importLocation reference))
                assertEqual "missing import source" "entry.tex"
                    (locFile (importLocation reference))
            Left err ->
                assertFailure ("expected located SourceNotFound, got " <> show err)
            Right graph ->
                assertFailure ("expected missing-import rejection, got " <> show graph)

rejectsUnsafeImports :: Assertion
rejectsUnsafeImports =
    withTemporaryDirectory "felix-source-unsafe-import" \temp -> do
        writeTheory (temp Posix.</> "entry.tex") ["./shared.tex"] "entry"
        mounts <- oneMount "project" temp
        request <- expectRight (searchedRoot "entry.tex")
        result <- buildResolvedSourceGraph mounts request
        case result of
            Left (InvalidImportPath _source location raw CurrentDirectoryComponent) -> do
                assertEqual "raw import" "./shared.tex" raw
                assertEqual "unsafe import line" 1 (locLine location)
                assertEqual "unsafe import source" "entry.tex" (locFile location)
            Left err ->
                assertFailure ("expected InvalidImportPath, got " <> show err)
            Right graph ->
                assertFailure ("expected unsafe-import rejection, got " <> show graph)

reportsImportCycles :: Assertion
reportsImportCycles =
    withTemporaryDirectory "felix-source-cycle" \temp -> do
        writeTheory (temp Posix.</> "a.tex") ["b.tex"] "a"
        writeTheory (temp Posix.</> "b.tex") ["a.tex"] "b"
        mounts <- oneMount "project" temp
        request <- expectRight (searchedRoot "a.tex")
        result <- buildResolvedSourceGraph mounts request
        case result of
            Left (SourceImportCycle steps) -> do
                assertEqual "cycle length" 2 (length steps)
                assertEqual
                    "cycle importer sequence"
                    ["a.tex", "b.tex"]
                    [ safeRelativePathFilePath
                        (resolvedSourceRelativePath (cycleImporter step))
                    | step <- toList steps
                    ]
                assertEqual
                    "cycle import locations"
                    ["a.tex", "b.tex"]
                    [ locFile (importLocation (cycleImport step))
                    | step <- toList steps
                    ]
            Left err ->
                assertFailure ("expected SourceImportCycle, got " <> show err)
            Right graph ->
                assertFailure ("expected cycle rejection, got " <> show graph)

rejectsMalformedImportedSource :: Assertion
rejectsMalformedImportedSource =
    withTemporaryDirectory "felix-source-import-utf8" \temp -> do
        writeTheory (temp Posix.</> "entry.tex") ["bad.tex"] "entry"
        ByteString.writeFile
            (temp Posix.</> "bad.tex")
            (ByteString.pack [0x61, 0xFF])
        mounts <- oneMount "project" temp
        request <- expectRight (searchedRoot "entry.tex")
        result <- buildResolvedSourceGraph mounts request
        case result of
            Left (SourceDecodeError source offset) -> do
                assertEqual "bad source" "bad.tex"
                    (safeRelativePathFilePath (resolvedSourceRelativePath source))
                assertEqual "bad byte offset" 1 offset
            Left err ->
                assertFailure ("expected SourceDecodeError, got " <> show err)
            Right graph ->
                assertFailure ("expected malformed-source rejection, got " <> show graph)

buildsEmptyModules :: Assertion
buildsEmptyModules =
    withTemporaryDirectory "felix-source-empty" \temp ->
        forM_
            [ ("empty.tex", "")
            , ("comments.tex", "% heading\n% body")
            ]
            \(relative, contents) -> do
                writeFile (temp Posix.</> relative) contents
                graph <- buildSearchedGraph temp relative
                assertEqual
                    "one ordinary graph node"
                    1
                    (length (sourceGraphNodes graph))
                emittedRef <- newIORef (0 :: Int)
                workspace <-
                    expectRight
                        =<< Parse.parseResolvedSourceGraphWith
                            graph
                            (\_source _block ->
                                modifyIORef' emittedRef (+ 1))
                assertEqual
                    "no block callbacks"
                    0
                    =<< readIORef emittedRef
                assertEqual
                    "empty parsed projection"
                    []
                    (Parse.importedBeforeImporterBlocks workspace)
                assertBool
                    "empty syntax declarations"
                    (null
                        (Interface.canonicalSyntaxDeltaEntries
                            (Interface.moduleSyntaxLocalDelta
                                (Parse.parsedModuleSyntaxInterface
                                    (Parse.parsedWorkspaceRootModule
                                        workspace)))))
                assignments <-
                    expectRight
                        (Legacy.assignLegacyModuleOrdinals workspace)
                assignment <-
                    case toList assignments of
                        [only] ->
                            pure only
                        actual ->
                            assertFailure
                                ("expected one empty module assignment, got "
                                    <> show (length actual))
                                >> fail "unreachable"
                checkedFoundationValue <-
                    expectRight Foundation.checkedFoundation
                builder <-
                    expectRight
                        (Transition.openTransitionModuleBuilder
                            checkedFoundationValue
                            Checking.initialLegacyCheckingEnvironment
                            assignment
                            [])
                checked <-
                    Checking.runCheckingBlocks
                        []
                        (Checking.initialTransitionCheckingStateWithTaskPreparation
                                Checking.WithoutDumpPremselTraining
                                id
                                builder
                                (\_batch ->
                                    assertFailure
                                        "empty module emitted an obligation"))
                finalBuilder <-
                    expectJust
                        "empty transition builder"
                        (Checking.checkingTransitionModuleBuilder checked)
                void
                    (expectRight
                        (Transition.sealTransitionModule
                            (Checking.checkingStateEnvironment checked)
                            finalBuilder))

identifiesOwnerIndependentParsedModules :: Assertion
identifiesOwnerIndependentParsedModules =
    withTemporaryDirectory "felix-parsed-identity" \temp -> do
        let firstRoot = temp Posix.</> "first"
            secondRoot = temp Posix.</> "second"
            bytes = axiomBlock "same" "x = x"
        Directory.createDirectory firstRoot
        Directory.createDirectory secondRoot
        writeFile (firstRoot Posix.</> "entry.tex") bytes
        writeFile (secondRoot Posix.</> "entry.tex") bytes
        firstWorkspace <- expectRight
            =<< Parse.parseResolvedSourceGraph
            =<< buildSearchedGraph firstRoot "entry.tex"
        secondWorkspace <- expectRight
            =<< Parse.parseResolvedSourceGraph
            =<< buildSearchedGraph secondRoot "entry.tex"
        let first = Parse.parsedWorkspaceRootModule firstWorkspace
            second = Parse.parsedWorkspaceRootModule secondWorkspace
        assertBool
            "logical owners remain distinct"
            ( Module.moduleName (Parse.parsedModuleAddress first)
                /= Module.moduleName (Parse.parsedModuleAddress second)
            )
        assertEqual
            "equal bytes retain one content identity"
            (Parse.parsedModuleSourceContentId first)
            (Parse.parsedModuleSourceContentId second)
        assertEqual
            "physical source registration is outside parsed identity"
            (Parse.parsedModuleId first)
            (Parse.parsedModuleId second)
        assertEqual
            "canonical payload is owner-independent"
            (Parse.parsedModulePayload first)
            (Parse.parsedModulePayload second)
        let payload = Parse.parsedModulePayload first
        assertEqual
            "canonical parsed payload cache round trip"
            (Right payload)
            (Cache.decodeCache
                Parsed.getCanonicalParsedPayloadCache
                (Cache.encodeCache
                    (Parsed.putCanonicalParsedPayloadCache payload)))
        rebound <- expectRight
            (Parsed.decodeCanonicalParsedPayload
                (FileId 123)
                payload)
        case Parsed.decodedParsedBlocks rebound of
            Raw.BlockAxiom location _title _marker _axiom : _ ->
                assertEqual
                    "decoded locations bind only to the current live file"
                    (Just (FileId 123))
                    (locFileId location)
            blocks ->
                assertFailure
                    ("expected decoded axiom, got " <> show blocks)
        writeFile
            (secondRoot Posix.</> "entry.tex")
            (bytes <> "% content identity change\n")
        changedWorkspace <- expectRight
            =<< Parse.parseResolvedSourceGraph
            =<< buildSearchedGraph secondRoot "entry.tex"
        assertBool
            "exact source changes parsed identity"
            ( Parse.parsedModuleId first
                /= Parse.parsedModuleId
                    (Parse.parsedWorkspaceRootModule changedWorkspace)
            )

keysEffectiveDirectSyntaxInputs :: Assertion
keysEffectiveDirectSyntaxInputs =
    withTemporaryDirectory "felix-parsed-syntax-input" \temp -> do
        let firstRoot = temp Posix.</> "first"
            secondRoot = temp Posix.</> "second"
            rootBytes = "\\import{notation.tex}\n"
        Directory.createDirectory firstRoot
        Directory.createDirectory secondRoot
        writeFile (firstRoot Posix.</> "entry.tex") rootBytes
        writeFile (secondRoot Posix.</> "entry.tex") rootBytes
        writeFile
            (firstRoot Posix.</> "notation.tex")
            (syntaxFunctionDefinition
                "first_notation"
                "firstop"
                (Just "%! infixl 1"))
        writeFile
            (secondRoot Posix.</> "notation.tex")
            (syntaxFunctionDefinition
                "second_notation"
                "secondop"
                (Just "%! infixl 1"))
        firstWorkspace <- expectRight
            =<< Parse.parseResolvedSourceGraph
            =<< buildSearchedGraph firstRoot "entry.tex"
        secondWorkspace <- expectRight
            =<< Parse.parseResolvedSourceGraph
            =<< buildSearchedGraph secondRoot "entry.tex"
        let first = Parse.parsedWorkspaceRootModule firstWorkspace
            second = Parse.parsedWorkspaceRootModule secondWorkspace
        assertEqual
            "root source bytes are unchanged"
            (Parse.parsedModuleSourceContentId first)
            (Parse.parsedModuleSourceContentId second)
        assertBool
            "effective syntax changes the parsed key"
            (Parse.parsedModuleKey first /= Parse.parsedModuleKey second)
        assertBool
            "effective syntax changes parsed identity"
            (Parse.parsedModuleId first /= Parse.parsedModuleId second)

reusesExactParsedSyntax :: Assertion
reusesExactParsedSyntax =
    withTemporaryDirectory "felix-parsed-warm" \temp -> do
        let datatype = unlines
                [ "\\begin{datatype}\\label{multi_item}"
                , "  Define $\\itemkind$ inductively as follows."
                , "  \\begin{enumerate}"
                , "    \\item $\\itemzero \\in \\itemkind$."
                , "    \\item $\\itemsucc{x} \\in \\itemkind$ for $x \\in \\itemkind$."
                , "  \\end{enumerate}"
                , "\\end{datatype}"
                ]
        writeFile
            (temp Posix.</> "entry.tex")
            (builtinZeroDefinition "source_zero" <> datatype)
        mounts <- oneMount "project" temp
        request <- expectRight (searchedRoot "entry.tex")
        foundation <- expectRight Foundation.checkedFoundation
        store <- openTestStore
            (temp Posix.</> "store.sqlite")
            (Identity.theoryId foundation)
        coldCallbacks <- newIORef (0 :: Int)
        cold <- expectParseExecution
            =<< Parse.parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndCallback
                store mounts request (const [])
                (\_source _block -> modifyIORef' coldCallbacks (+ 1))
        warmCallbacks <- newIORef (0 :: Int)
        warm <- expectParseExecution
            =<< Parse.parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndCallback
                store mounts request (const [])
                (\_source _block -> modifyIORef' warmCallbacks (+ 1))
        let coldRoot = Parse.parsedWorkspaceRootModule (fst cold)
            warmRoot = Parse.parsedWorkspaceRootModule (fst warm)
            coldMeasurements = snd cold
            warmMeasurements = snd warm
        assertEqual "cold parsed misses" 1
            (Parse.parseMeasurementParsedMissCount coldMeasurements)
        assertEqual "cold parser tables" 1
            (Parse.parseMeasurementParserTableMaterializationCount
                coldMeasurements)
        assertEqual "warm parsed hits" 1
            (Parse.parseMeasurementParsedHitCount warmMeasurements)
        assertEqual "warm parsed misses" 0
            (Parse.parseMeasurementParsedMissCount warmMeasurements)
        assertEqual "warm tokenization" 0
            (Parse.parseMeasurementTokenizationNanoseconds warmMeasurements)
        assertEqual "warm scanning" 0
            (Parse.parseMeasurementScanningNanoseconds warmMeasurements)
        assertEqual "warm parsing" 0
            (Parse.parseMeasurementParsingNanoseconds warmMeasurements)
        assertEqual "warm parser tables" 0
            (Parse.parseMeasurementParserTableMaterializationCount
                warmMeasurements)
        assertEqual "warm blocks" (Parse.parsedModuleBlocks coldRoot)
            (Parse.parsedModuleBlocks warmRoot)
        assertEqual "warm occurrences"
            (Parse.parsedModuleSyntaxOccurrences coldRoot)
            (Parse.parsedModuleSyntaxOccurrences warmRoot)
        assertEqual "warm syntax interface"
            (Parse.parsedModuleSyntaxInterface coldRoot)
            (Parse.parsedModuleSyntaxInterface warmRoot)
        assertEqual "warm parsed identity"
            (Parse.parsedModuleId coldRoot)
            (Parse.parsedModuleId warmRoot)
        case Parse.parsedModuleSyntaxOccurrences warmRoot of
            first : second : third : fourth : [] -> do
                assertEqual "fixed source marker" "source_zero"
                    (Parse.parsedSyntaxOccurrenceMarker first)
                case Parse.parsedSyntaxOccurrenceEntry first of
                    Interface.CanonicalExpressionFunction
                            _pattern marker _fixity ->
                        assertEqual "fixed authoritative marker" "zero" marker
                    entry ->
                        assertFailure
                            ("unexpected fixed cached entry: " <> show entry)
                assertEqual "multi-item block order" [1, 1, 1]
                    (Parse.parsedSyntaxOccurrenceBlockIndex
                        <$> [second, third, fourth])
                assertEqual "multi-item scanner order"
                    ["multi_item", "itemzero", "itemsucc"]
                    (Parse.parsedSyntaxOccurrenceMarker
                        <$> [second, third, fourth])
                case drop 1 (Parse.parsedModuleBlocks warmRoot) of
                    block : _ ->
                        case block of
                            Raw.BlockData _location _title marker _datatype ->
                                assertEqual "cached declaration-head anchor"
                                    marker
                                    (Parse.parsedSyntaxOccurrenceMarker second)
                            other ->
                                assertFailure
                                    ("expected cached datatype block, got "
                                        <> show other)
                    [] ->
                        assertFailure "cached datatype block is absent"
            occurrences ->
                assertFailure
                    ("unexpected cached syntax occurrences: "
                        <> show occurrences)
        assertEqual "cold callback projection" 2
            =<< readIORef coldCallbacks
        assertEqual "warm callback projection" 2
            =<< readIORef warmCallbacks
        Store.closeStore store

rejectsCorruptedCachedDeclarationAnchor :: Assertion
rejectsCorruptedCachedDeclarationAnchor =
    withTemporaryDirectory "felix-parsed-corrupt-anchor" \temp -> do
        writeBuiltinZeroDefinition
            (temp Posix.</> "entry.tex")
            "source_zero"
        mounts <- oneMount "project" temp
        request <- expectRight (searchedRoot "entry.tex")
        foundation <- expectRight Foundation.checkedFoundation
        let storePath = temp Posix.</> "store.sqlite"
            theory = Identity.theoryId foundation
        store <- openTestStore storePath theory
        (cold, _measurements) <- expectParseExecution
            =<< Parse.parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputs
                store mounts request (const [])
        let parsed = Parse.parsedWorkspaceRootModule cold
            key = Parse.parsedModuleKey parsed
        fileId <- case Parse.parsedModuleSyntaxOccurrences parsed of
            occurrence : _ ->
                expectJust
                    "parsed occurrence file id"
                    (locFileId
                        (Parse.parsedSyntaxOccurrenceLocation occurrence))
            [] ->
                assertFailure "parsed fixed occurrence is absent"
                    >> fail "unreachable"
        decoded <- expectRight
            (Parsed.decodeCanonicalParsedPayload
                fileId
                (Parse.parsedModulePayload parsed))
        Store.closeStore store
        let corruptedOccurrences = case Parsed.decodedParsedOccurrences decoded of
                (blockIndex, location, _marker, entry) : rest ->
                    (blockIndex, location, "corrupted_anchor", entry) : rest
                [] ->
                    []
            corruptedPayload =
                Parsed.canonicalParsedPayload
                    (Parsed.decodedParsedImports decoded)
                    (Parsed.decodedParsedBlocks decoded)
                    corruptedOccurrences
                    (Parsed.decodedParsedSyntaxInterface decoded)
            corruptedId =
                ParsedIdentity.parsedModuleId
                    key
                    (Parsed.canonicalParsedPayloadBytes corruptedPayload)
        connection <- SQLite.open storePath
        SQLite.execute connection
            "UPDATE parsed_artifacts \
            \SET parsed_module_id = ?, payload = ? \
            \WHERE parsed_module_key = ?"
            ( Cache.cacheDigestBytes
                (ParsedIdentity.parsedModuleIdDigest corruptedId)
            , Parsed.canonicalParsedPayloadBytes corruptedPayload
            , Cache.cacheDigestBytes
                (ParsedIdentity.parsedModuleKeyDigest key)
            )
        SQLite.close connection
        current <- openTestStore storePath theory
        callbacks <- newIORef (0 :: Int)
        Parse.parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndCallback
            current mounts request (const [])
            (\_source _block -> modifyIORef' callbacks (+ 1)) >>= \case
                Left
                    (Parse.ParseExecutionArtifactIntegrityFailure
                        _source
                        (Parse.ParsedArtifactAssociationFailure
                            Parse.SyntaxOccurrenceMarkerMismatch{})) ->
                            pure ()
                other ->
                    assertFailure
                        ("unexpected corrupted parsed result: " <> show other)
        assertEqual "corrupt hit invokes no parse callback" 0
            =<< readIORef callbacks
        Store.closeStore current

openTestStore :: FilePath -> Identity.TheoryId -> IO Store.Store
openTestStore path theory =
    Store.openStore path theory >>= \case
        Left failure ->
            assertFailure (show failure) >> fail "unreachable"
        Right (_startup, store) ->
            pure store

expectParseExecution
    :: Either Parse.ParseExecutionError value
    -> IO value
expectParseExecution = \case
    Left failure ->
        assertFailure (show failure) >> fail "unreachable"
    Right value ->
        pure value

parsesSourceGraph :: Assertion
parsesSourceGraph =
    withTemporaryDirectory "felix-source-parse" \temp -> do
        writeTheory (temp Posix.</> "shared.tex") [] "shared"
        writeTheory (temp Posix.</> "entry.tex") ["shared.tex"] "entry"
        graph <- buildSearchedGraph temp "entry.tex"
        emittedRef <- newIORef []
        workspace <- expectRight =<<
            Parse.parseResolvedSourceGraphWith graph
                (\source _block ->
                    modifyIORef'
                        emittedRef
                        (safeRelativePathFilePath
                            (resolvedSourceRelativePath source) :))
        assertEqual "two parsed source nodes" 2
            (length (Parse.parsedWorkspaceModules workspace))
        assertEqual "one source-local block per node" [1, 1]
            (toList
                (length . Parse.parsedModuleBlocks
                    <$> Parse.parsedWorkspaceImportedBeforeImporter workspace))
        assertEqual "imported-before-importer source order"
            ["shared.tex", "entry.tex"]
            (toList
                (safeRelativePathFilePath
                    . resolvedSourceRelativePath
                    . Parse.parsedModuleResolved
                    <$> Parse.parsedWorkspaceImportedBeforeImporter workspace))
        assertEqual "flattened block view" 2
            (length (Parse.importedBeforeImporterBlocks workspace))
        emitted <- reverse <$> readIORef emittedRef
        assertEqual "streamed block order"
            ["shared.tex", "entry.tex"]
            emitted

reservesLegacyModulePositions :: Assertion
reservesLegacyModulePositions =
    withTemporaryDirectory "felix-legacy-module-stage" \temp -> do
        writeTheory (temp Posix.</> "shared.tex") [] "shared"
        writeTheory
            (temp Posix.</> "entry.tex")
            ["shared.tex"]
            "entry"
        graph <- buildSearchedGraph temp "entry.tex"
        workspace <-
            expectRight
                =<< Parse.parseResolvedSourceGraph graph
        assignments <-
            expectRight
                (Legacy.assignLegacyModuleOrdinals workspace)
        assertEqual "dense imported-first module ordinals"
            [0, 1]
            ( Legacy.legacyModuleOrdinalValue
                . Legacy.assignedLegacyModuleOrdinal
                <$> toList assignments
            )
        assertEqual "assigned source order"
            ["shared.tex", "entry.tex"]
            ( safeRelativePathFilePath
                . sourceAddressRelativePath
                . Parse.parsedModuleAddress
                . Legacy.assignedParsedModule
                <$> toList assignments
            )

        let firstAssignment :| _remainingAssignments =
                assignments
            stage =
                Legacy.openLegacyModuleStage
                    firstAssignment
                    (Legacy.emptyLegacyImportedView
                        Checking.initialLegacyCheckingEnvironment)
            origin = Facts.factOrigin (Location 0) "declaration"
            firstFact =
                Facts.stageFact
                    ("first" :| ["first_alias"])
                    origin
                    (Facts.prepareSemanticFact Top)
            secondFact =
                Facts.stageFact
                    ("second" :| [])
                    origin
                    (Facts.prepareSemanticFact Bottom)
        reservation <-
            expectRight
                (Legacy.reserveLegacyDeclaration
                    (firstFact :| [secondFact])
                    stage)
        assertEqual "dense local fact ordinals"
            [0, 1]
            ( Legacy.legacyLocalFactOrdinalValue
                . Legacy.legacyFactLocalOrdinal
                . Legacy.legacyReservedFactReference
                <$> toList (Legacy.legacyReservedFacts reservation)
            )

        let duplicateAliasFact =
                Facts.stageFact
                    ("first_alias" :| [])
                    origin
                    (Facts.prepareSemanticFact Bottom)
        case Legacy.reserveLegacyDeclaration
                (firstFact :| [duplicateAliasFact])
                stage of
            Left Legacy.LegacyAliasAlreadyBound{} ->
                pure ()
            Left err ->
                assertFailure
                    ("expected alias rejection, got " <> show err)
            Right _ ->
                assertFailure "expected duplicate legacy alias rejection"

admitsLegacyDeclarations :: Assertion
admitsLegacyDeclarations =
    withTemporaryDirectory "felix-legacy-admission" \temp -> do
        writeTheory (temp Posix.</> "entry.tex") [] "entry"
        graph <- buildSearchedGraph temp "entry.tex"
        workspace <-
            expectRight
                =<< Parse.parseResolvedSourceGraph graph
        assignment :| _ <-
            expectRight
                (Legacy.assignLegacyModuleOrdinals workspace)
        let stage =
                Legacy.openLegacyModuleStage
                    assignment
                    (Legacy.emptyLegacyImportedView
                        Checking.initialLegacyCheckingEnvironment)
            blocks =
                [ BlockAxiom
                    Nowhere
                    "declared"
                    (Axiom [] Top)
                , BlockLemma
                    Nowhere
                    "omitted"
                    (Lemma [] Bottom)
                , BlockProof
                    Nowhere
                    Nowhere
                    (Omitted Nowhere)
                ]
            resolveGapBatch batch = do
                resolved <-
                    traverse
                        (either
                            (ioError . userError . show)
                            pure
                            . Obligation.resolveObligationAsGap)
                        (Obligation.preparedBatchObligations batch)
                either
                    (ioError . userError . show)
                    pure
                    (Obligation.resolveObligationBatch
                        batch
                        resolved)
            initial =
                Checking.initialLegacyCheckingStateWithTaskPreparation
                    Checking.WithoutDumpPremselTraining
                    id
                    stage
                    resolveGapBatch
        checked <-
            Checking.runCheckingBlocks blocks initial
        admittedStage <-
            maybe
                (assertFailure
                    "authoritative checking lost the legacy stage"
                    >> pure stage)
                pure
                (Checking.checkingLegacyModuleStage checked)
        admittedModule <-
            expectRight
                (Legacy.sealLegacyModuleStage
                    (Checking.checkingStateEnvironment checked)
                    admittedStage)
        assertEqual "two sealed local facts"
            2
            (Vector.length
                (Legacy.legacyAdmittedLocalFacts admittedModule))
        assertEqual "one sealed declared assumption"
            1
            (Vector.length
                (Legacy.legacyAdmittedDirectAxiomManifest
                    admittedModule))
        let finalTrust =
                Legacy.legacyFactEntryTrustDependencies
                    (Vector.last
                        (Legacy.legacyAdmittedLocalFacts
                            admittedModule))
        assertEqual "one explicit gap"
            1
            (Set.size
                (Legacy.legacyExplicitGaps finalTrust))
        assertEqual "direct gap needs no legacy finalization rule"
            0
            (Set.size
                (Legacy.trustedLegacyRuleUses finalTrust))

publishesTransitionSignatures :: Assertion
publishesTransitionSignatures =
    withTemporaryDirectory "felix-transition-signatures" \temp -> do
        writeTheory (temp Posix.</> "shared.tex") [] "shared"
        writeTheory
            (temp Posix.</> "entry.tex")
            ["shared.tex"]
            "entry"
        graph <- buildSearchedGraph temp "entry.tex"
        workspace <-
            expectRight
                =<< Parse.parseResolvedSourceGraph graph
        assignments <-
            expectRight
                (Legacy.assignLegacyModuleOrdinals workspace)
        checkedFoundationValue <-
            expectRight Foundation.checkedFoundation
        case toList assignments of
            [sharedAssignment, entryAssignment] -> do
                shared <-
                    admit
                        checkedFoundationValue
                        sharedAssignment
                        []
                        [ BlockSig
                            Nowhere
                            "shared_signature"
                            []
                            (SignaturePredicate
                                sharedPredicate
                                ("x" :| []))
                        , BlockAxiom
                            Nowhere
                            "shared_atomic_axiom"
                            (Axiom [] sharedAtomicFormula)
                        ]
                let sharedGlobals =
                        Transition.transitionAdmittedGlobals
                            shared
                assertEqual
                    "one shared typed declaration"
                    1
                    (Vector.length sharedGlobals)
                case Vector.toList sharedGlobals of
                    [(symbol, reference, _origin)] -> do
                        assertEqual
                            "shared symbol"
                            (SymbolPredicate sharedPredicate)
                            symbol
                        assertEqual
                            "shared declaration ordinal"
                            0
                            (Transition.localDeclarationOrdinalValue
                                (Transition.opaqueDeclarationOrdinal
                                    (Transition.checkedGlobalReference
                                        reference)))
                        assertEqual
                            "shared predicate type"
                            (Core.TySet
                                `Core.TyArrow`
                                    Core.TyProp)
                            (Transition.checkedGlobalType reference)
                    _ ->
                        assertFailure
                            "expected one shared typed declaration"
                let sharedFacts =
                        Vector.toList
                            (Transition.transitionAdmittedFacts
                                shared)
                    sharedManifest =
                        Vector.toList
                            (Transition.transitionAdmittedTypedDirectAxiomManifest
                                shared)
                (sharedReference, sharedStatement) <-
                    case (sharedFacts, sharedManifest) of
                    ([assumption], [manifestEntry]) -> do
                        assertBool
                            "typed axiom is not a kernel proof"
                            (not
                                (Transition.admittedFactIsKernelProof
                                    assumption))
                        assertEqual
                            "manifest kind"
                            Legacy.DeclaredUserAxiom
                            (Transition.typedDirectAssumptionKind
                                manifestEntry)
                        assertEqual
                            "manifest fact reference"
                            (Just
                                (Transition.typedDirectAssumptionFact
                                    manifestEntry))
                            (Transition.transitionTypedFactReference
                                (Transition.admittedFactReference
                                    assumption))
                        pure
                            ( Transition.admittedFactReference
                                assumption
                            , Transition.typedDirectAssumptionStatement
                                manifestEntry
                            )
                    _ ->
                        fail
                            "expected one manifest-backed typed axiom"

                hiddenBuilder <-
                    expectRight
                        (Transition.openTransitionModuleBuilder
                            checkedFoundationValue
                            Checking.initialLegacyCheckingEnvironment
                            entryAssignment
                            [])
                hiddenTarget <-
                    expectRight
                        (Core.checkCanonicalCore
                            (const Nothing)
                            (Core.CImp
                                Core.CFalsum
                                Core.CFalsum))
                hiddenImport <-
                    expectRight
                        (Transition.transitionDerivationImport
                            sharedReference
                            hiddenTarget)
                case Transition.commitTransitionKernelFactWithImports
                        ("hidden_import" :| [])
                        (Transition.origin
                            Nowhere
                            Nothing
                            (Just "hidden_import"))
                        (Vector.singleton hiddenImport)
                        hiddenTarget
                        (Derivation.importedFactDerivation
                            (Derivation.importIx 0))
                        hiddenBuilder of
                    Left
                        (Transition.TransitionKernelImportNotVisible
                            actualReference) ->
                                assertEqual
                                    "unimported fact reference"
                                    sharedReference
                                    actualReference
                    Left err ->
                        assertFailure
                            ("expected hidden typed import failure, got "
                                <> show err)
                    Right _ ->
                        assertFailure
                            "an unimported typed row authorized replay"

                entryBuilder <-
                    expectRight
                        (Transition.openTransitionModuleBuilder
                            checkedFoundationValue
                            Checking.initialLegacyCheckingEnvironment
                            entryAssignment
                            [shared])
                assertBool
                    "direct import exposes the typed global"
                    (isJust
                        (Transition.lookupTransitionGlobal
                            (SymbolPredicate sharedPredicate)
                            entryBuilder))
                entry <-
                    admitWithBuilder
                        entryBuilder
                        [ BlockAxiom
                            Nowhere
                            "legacy_axiom"
                            (Axiom [] Top)
                        , BlockSig
                            Nowhere
                            "entry_signature"
                            []
                            (SignaturePredicate
                                entryPredicate
                                ("z" :| []))
                        , BlockLemma
                            Nowhere
                            "typed_import_reuse"
                            (Lemma [] sharedAtomicFormula)
                        , BlockLemma
                            Nowhere
                            "typed_reflexivity"
                            (Lemma
                                []
                                (Equals
                                    Nowhere
                                    (EmptySet Nowhere)
                                    (EmptySet Nowhere)))
                        ]
                case Vector.toList
                        (Transition.transitionAdmittedGlobals
                            entry) of
                    [(_symbol, reference, _origin)] ->
                        assertEqual
                            "legacy declaration occupies its source ordinal"
                            1
                            (Transition.localDeclarationOrdinalValue
                                (Transition.opaqueDeclarationOrdinal
                                    (Transition.checkedGlobalReference
                                        reference)))
                    _ ->
                        assertFailure
                            "expected one local entry declaration"
                let facts =
                        Vector.toList
                            (Transition.transitionAdmittedFacts
                                entry)
                assertEqual
                    "imported and local rows retain declaration order"
                    [False, False, True, True]
                    (Transition.admittedFactIsKernelProof
                        <$> facts)
                case facts of
                    [_assumption, _legacy, reused, reflexivity] -> do
                        case Transition.transitionTypedFactReference
                                (Transition.admittedFactReference
                                    reused) of
                            Nothing ->
                                assertFailure
                                    "expected a typed fact reference"
                            Just reference ->
                                assertEqual
                                    "first typed fact ordinal"
                                    0
                                    (Transition.localFactOrdinalValue
                                        (Transition.factReferenceOrdinal
                                            reference))
                        case Transition.transitionTypedFactReference
                                (Transition.admittedFactReference
                                    reflexivity) of
                            Nothing ->
                                assertFailure
                                    "expected a typed reflexivity reference"
                            Just reference ->
                                assertEqual
                                    "second typed fact ordinal"
                                    1
                                    (Transition.localFactOrdinalValue
                                        (Transition.factReferenceOrdinal
                                            reference))
                    _ ->
                        assertFailure
                            "expected imported assumption and three local facts"
                let inheritedAssumptions =
                        Set.toList
                            (Transition.typedDeclaredAssumptionUses
                                (Transition.transitionAdmittedTypedTrustDependencies
                                    entry))
                case inheritedAssumptions of
                    [assumption] -> do
                        assertEqual
                            "the importer retains the owner fact"
                            (Transition.transitionTypedFactReference
                                sharedReference)
                            (Just
                                (Transition.sessionTypedAssumptionFact
                                    assumption))
                        assertEqual
                            "the owner assumption ordinal"
                            0
                            (Transition.localAssumptionOrdinalValue
                                (Transition.sessionTypedAssumptionOrdinal
                                    assumption))
                        assertEqual
                            "the imported assumption statement"
                            sharedStatement
                            (Transition.sessionTypedAssumptionStatement
                                assumption)
                    _ ->
                        assertFailure
                            "expected one inherited typed declared assumption"
                assertEqual
                    "two local replayed kernel proofs"
                    2
                    (Transition.transitionAdmittedKernelProofCount
                        entry)
            actual ->
                assertFailure
                    ("expected two module assignments, got "
                        <> show (length actual))
  where
    sharedPredicate =
        PredicateSymbol "typed_shared_predicate"
    entryPredicate =
        PredicateSymbol "typed_entry_predicate"
    sharedAtomicFormula =
        Atomic
            Nowhere
            sharedPredicate
            [EmptySet Nowhere]

    admit checkedFoundationValue assignment imports blocks = do
        builder <-
            expectRight
                (Transition.openTransitionModuleBuilder
                    checkedFoundationValue
                    Checking.initialLegacyCheckingEnvironment
                    assignment
                    imports)
        admitWithBuilder builder blocks

    admitWithBuilder builder blocks = do
        checked <-
            Checking.runCheckingBlocks
                blocks
                (Checking.initialTransitionCheckingStateWithTaskPreparation
                    Checking.WithoutDumpPremselTraining
                    id
                    builder
                    (\_batch ->
                        assertFailure
                            "typed transition emitted an obligation"))
        finalBuilder <-
            maybe
                (assertFailure
                    "checking lost its transition builder")
                pure
                (Checking.checkingTransitionModuleBuilder
                    checked)
        expectRight
            (Transition.sealTransitionModule
                (Checking.checkingStateEnvironment checked)
                finalBuilder)

rejectsForeignCachedGlobalType :: Assertion
rejectsForeignCachedGlobalType =
    withTemporaryDirectory "felix-transition-global-types" \temp -> do
        writeTheory
            (temp Posix.</> "entry.tex")
            []
            "entry"
        graph <-
            buildSearchedGraph temp "entry.tex"
        workspace <-
            expectRight
                =<< Parse.parseResolvedSourceGraph graph
        assignments <-
            expectRight
                (Legacy.assignLegacyModuleOrdinals workspace)
        assignment <-
            case toList assignments of
                [only] ->
                    pure only
                actual ->
                    assertFailure
                        ("expected one module assignment, got "
                            <> show (length actual))
                        >> fail "unreachable"
        checkedFoundationValue <-
            expectRight Foundation.checkedFoundation
        builderA0 <-
            expectRight
                (Transition.openTransitionModuleBuilder
                    checkedFoundationValue
                    Checking.initialLegacyCheckingEnvironment
                    assignment
                    [])
        builderB0 <-
            expectRight
                (Transition.openTransitionModuleBuilder
                    checkedFoundationValue
                    Checking.initialLegacyCheckingEnvironment
                    assignment
                    [])
        let symbol =
                SymbolPredicate
                    (PredicateSymbol
                        "same_nominal_global")
            declarationOrigin =
                Transition.origin
                    Nowhere
                    Nothing
                    (Just "same_nominal_global")
        builderA <-
            expectRight
                (Transition.commitTransitionOpaqueGlobal
                    symbol
                    Core.TySet
                    declarationOrigin
                    (Transition.beginTransitionDeclaration
                        builderA0))
        builderB <-
            expectRight
                (Transition.commitTransitionOpaqueGlobal
                    symbol
                    Core.TyProp
                    declarationOrigin
                    (Transition.beginTransitionDeclaration
                        builderB0))
        globalA <-
            maybe
                (assertFailure "builder A lost its global"
                    >> fail "unreachable")
                pure
                (Transition.lookupTransitionGlobal
                    symbol
                    builderA)
        globalB <-
            maybe
                (assertFailure "builder B lost its global"
                    >> fail "unreachable")
                pure
                (Transition.lookupTransitionGlobal
                    symbol
                    builderB)
        operand <-
            expectRight
                (Core.checkCanonicalCore
                    (Just . Transition.checkedGlobalType)
                    (Core.CGlobal globalA))
        statement <-
            expectRight
                (Core.checkCanonicalCore
                    (Just . Transition.checkedGlobalType)
                    (Core.CEq
                        Core.TySet
                        (Core.CGlobal globalA)
                        (Core.CGlobal globalA)))
        case Transition.commitTransitionKernelFact
                ("foreign_global_type" :| [])
                (Transition.origin
                    Nowhere
                    Nothing
                    (Just "foreign_global_type"))
                statement
                (Derivation.equalityReflexivityDerivation
                    operand)
                (Transition.beginTransitionDeclaration
                    builderB) of
            Left
                (Transition.TransitionGlobalReferenceTypeMismatch
                    actual
                    authoritativeType) -> do
                        assertEqual
                            "cached global reference"
                            globalA
                            actual
                        assertEqual
                            "builder B authoritative type"
                            Core.TyProp
                            authoritativeType
            Left err ->
                assertFailure
                    ("expected cached global type rejection, got "
                        <> show err)
            Right _ ->
                assertFailure
                    "builder B admitted builder A's cached type"
        let remappedOperand =
                Core.mapFrozenGlobals
                    (const globalB)
                    operand
            remappedStatement =
                Core.mapFrozenGlobals
                    (const globalB)
                    statement
        case Transition.commitTransitionKernelFact
                ("stale_term_annotation" :| [])
                (Transition.origin
                    Nowhere
                    Nothing
                    (Just "stale_term_annotation"))
                remappedStatement
                (Derivation.equalityReflexivityDerivation
                    remappedOperand)
                (Transition.beginTransitionDeclaration
                    builderB) of
            Left
                (Transition.TransitionCoreCheckError
                    (Core.EqualityOperandTypeMismatch
                        Core.TySet
                        Core.TyProp)) ->
                pure ()
            Left err ->
                assertFailure
                    ("expected fresh builder-relative core check, got "
                        <> show err)
            Right _ ->
                assertFailure
                    "builder B admitted a stale term annotation"

authorizesTypedVampireRequests :: Assertion
authorizesTypedVampireRequests =
    withTemporaryDirectory "felix-typed-vampire" \temp -> do
        let sourcePath =
                temp Posix.</> "entry.tex"
            executablePath =
                temp Posix.</> "vampire"
        writeTheory sourcePath [] "entry"
        graph <-
            buildSearchedGraph temp "entry.tex"
        workspace <-
            expectRight
                =<< Parse.parseResolvedSourceGraph graph
        assignments <-
            expectRight
                (Legacy.assignLegacyModuleOrdinals
                    workspace)
        assignment <-
            case toList assignments of
                [only] ->
                    pure only
                actual ->
                    assertFailure
                        ("expected one module assignment, got "
                            <> show (length actual))
                        >> fail "unreachable"
        checkedFoundationValue <-
            expectRight Foundation.checkedFoundation
        baseBuilder <-
            expectRight
                (Transition.openTransitionModuleBuilder
                    checkedFoundationValue
                    Checking.initialLegacyCheckingEnvironment
                    assignment
                    [])
        let legacyStage =
                Transition.transitionBuilderLegacyStage
                    baseBuilder
            legacyStaged =
                Facts.stageFact
                    ("legacy_input" :| [])
                    (Facts.factOrigin
                        (Location 0)
                        "legacy_input")
                    (Facts.prepareSemanticFact Top)
        legacyReservation <-
            expectRight
                (Legacy.reserveLegacyDeclaration
                    (legacyStaged :| [])
                    legacyStage)
        let legacyReserved =
                NonEmpty.head
                    (Legacy.legacyReservedFacts
                        legacyReservation)
            legacyAdmitted =
                Legacy.authorizeLegacyDeclaredAssumption
                    legacyStage
                    Legacy.DeclaredUserAxiom
                    legacyReserved
        legacyStage' <-
            expectRight
                (Legacy.appendEstablishedLegacyDeclaration
                    legacyReservation
                    (legacyAdmitted :| [])
                    legacyStage)
        builderWithLegacy <-
            expectRight
                (Transition.transitionBuilderWithLegacyStage
                    legacyStage'
                    baseBuilder)
        target <-
            expectRight
                (Core.checkCanonicalCore
                    (Just . Transition.checkedGlobalType)
                    (Core.CImp
                        Core.CFalsum
                        Core.CFalsum))
        claim <-
            expectRight
                (Backend.supportedProposition
                    (Vector.empty
                        :: Vector.Vector
                            (Void, Core.CoreType))
                    (Core.embedClosedCore [] target))
        builderWithFof <-
            expectRight
                (Transition.commitTransitionTypedDeclaredAssumption
                    ("fof_input" :| [])
                    (Transition.origin
                        Nowhere
                        Nothing
                        (Just "fof_input"))
                    Legacy.DeclaredUserAxiom
                    target
                    (Transition.beginTransitionDeclaration
                        builderWithLegacy))
        let higherOrderTarget =
                Core.mapFrozenGlobals
                    absurd
                    (Foundation.foundationAxiomFrozen
                        checkedFoundationValue
                        Foundation.DoubleNegationElim)
        builderWithTh0 <-
            expectRight
                (Transition.commitTransitionTypedDeclaredAssumption
                    ("th0_input" :| [])
                    (Transition.origin
                        Nowhere
                        Nothing
                        (Just "th0_input"))
                    Legacy.DeclaredUserAxiom
                    higherOrderTarget
                    (Transition.beginTransitionDeclaration
                        builderWithFof))
        builder <-
            expectRight
                (Transition.commitTransitionTypedDeclaredAssumption
                    ("second_fof_input" :| [])
                    (Transition.origin
                        Nowhere
                        Nothing
                        (Just "second_fof_input"))
                    Legacy.DeclaredUserAxiom
                    target
                    (Transition.beginTransitionDeclaration
                        builderWithTh0))
        implicitProblem <-
            expectRight
                (Transition.planTransitionTypedProblem
                    builder
                    claim
                    []
                    []
                    Transition.ImplicitFofFacts
                    Backend.FirstOrderLocals)
        let selected =
                Vector.toList
                    (Backend.typedProblemGlobalPremises
                        implicitProblem)
        references <-
            traverse
                ( maybe
                    (assertFailure
                        "implicit planning selected a legacy row"
                        >> fail "unreachable")
                    pure
                    . Transition.transitionTypedFactReference
                    . Backend.typedBackendFactReference
                )
                selected
        assertEqual
            "implicit planning preserves FOF admission order"
            [0, 2]
            ( Transition.localFactOrdinalValue
                . Transition.factReferenceOrdinal
                <$> references
            )
        assertEqual
            "implicit admitted-fact route"
            Backend.RouteFof
            (Backend.typedProblemRoute
                implicitProblem)
        explicitHigherOrder <-
            expectRight
                (Transition.planTransitionTypedProblem
                    builder
                    claim
                    []
                    []
                    (Transition.ExplicitFacts
                        ("th0_input" :| ["th0_input"]))
                    Backend.FirstOrderLocals)
        assertEqual
            "explicit higher-order admitted fact selects TH0"
            Backend.RouteTh0
            (Backend.typedProblemRoute
                explicitHigherOrder)
        assertEqual
            "repeated explicit aliases select one fact"
            1
            (Vector.length
                (Backend.typedProblemGlobalPremises
                    explicitHigherOrder))
        case Transition.planTransitionTypedProblem
                builder
                claim
                []
                []
                (Transition.ExplicitFacts
                    ("legacy_input" :| []))
                Backend.FirstOrderLocals of
            Left
                (Transition.TransitionTypedProblemDependencyNotMigrated
                    reference) ->
                        assertEqual
                            "legacy dependency stays legacy"
                            Nothing
                            (Transition.transitionTypedFactReference
                                reference)
            result' ->
                assertFailure
                    ("expected legacy dependency rejection, got "
                        <> case result' of
                            Left err ->
                                "Left " <> show err
                            Right _problem ->
                                "Right problem")
        problem <-
            expectRight
                (Transition.planTransitionTypedProblem
                    builder
                    claim
                    []
                    [Backend.typedFoundationAuxiliaryInput
                        checkedFoundationValue
                        Foundation.DoubleNegationElim]
                    Transition.NoGlobalFacts
                    Backend.AllLocals)
        prepared <-
            expectRight
                (Provers.prepareTypedProverTask
                    Provers.DirectTask
                    problem)
        mismatched <-
            expectRight
                (Provers.prepareTypedProverTask
                    Provers.IndirectTask
                    problem)
        assertEqual
            "higher-order foundation input selects TH0"
            Provers.VerificationTh0
            (Provers.preparedVerificationDialect
                (Provers.preparedTypedProverRequest
                    prepared))
        writeFile executablePath
            (unlines
                [ "#!/bin/sh"
                , "cat >/dev/null"
                , "printf '%s\\n' '% SZS status Theorem for typed'"
                ])
        permissions <-
            Directory.getPermissions executablePath
        Directory.setPermissions executablePath
            (Directory.setOwnerExecutable
                True
                permissions)
        result <-
            runNoLoggingT
                (Provers.runPreparedTypedProver
                    (Provers.vampire
                        executablePath
                        Provers.defaultTimeLimit
                        Provers.defaultMemoryLimit)
                    prepared)
        accepted <-
            case result of
                Right answer
                    | Just run <-
                        Provers.provedVampireRun answer ->
                            pure run
                _ ->
                    assertFailure
                        ("expected accepted typed Vampire run, got "
                            <> show result)
                        >> fail "unreachable"
        let factOrigin =
                Transition.origin
                    Nowhere
                    Nothing
                    (Just "typed_vampire")
            commit task =
                Transition.commitTransitionTypedVampireFact
                    Reconstruction.defaultReconstructionPolicy
                    ("typed_vampire" :| [])
                    factOrigin
                    target
                    task
                    accepted
                    builder
        case commit mismatched of
            Left Transition.TransitionTypedVampireRequestMismatch ->
                pure ()
            result' ->
                assertFailure
                    ("expected exact-request mismatch, got "
                        <> showResult result')
        committed <-
            expectRight (commit prepared)
        admitted <-
            expectRight
                (Transition.sealTransitionModule
                    Checking.initialLegacyCheckingEnvironment
                    committed)
        let trust =
                Transition.transitionAdmittedTypedTrustDependencies
                    admitted
        assertEqual
            "one typed trusted Vampire row"
            1
            (Transition.transitionAdmittedTypedTrustedVampireCount
                admitted)
        assertEqual
            "one typed Vampire trust occurrence"
            1
            (Set.size
                (Transition.typedTrustedVampireUses
                    trust))
        assertEqual
            "mandatory lowering assumptions"
            Legacy.mandatoryVampireLoweringAssumptions
            (Transition.typedVampireLoweringUses
                trust)
        assertEqual
            "exact foundation input"
            (Set.singleton
                Foundation.DoubleNegationElim)
            (Transition.typedFoundationUses
                trust)
        let atom argument =
                Core.CApp
                    (Core.CApp
                        (Core.CIntrinsic Core.Member)
                        (Core.CIntrinsic Core.Empty))
                    argument
            atomP =
                atom (Core.CIntrinsic Core.Empty)
            atomQ =
                atom (Core.COpaqueInteger 1)
            atomR =
                atom (Core.COpaqueInteger 2)
            declareTyped alias statement current =
                expectRight
                    (Transition.commitTransitionTypedDeclaredAssumption
                        (alias :| [])
                        (Transition.origin
                            Nowhere
                            Nothing
                            (Just alias))
                        Legacy.DeclaredUserAxiom
                        statement
                        (Transition.beginTransitionDeclaration
                            current))
        premiseP <-
            expectRight
                (Core.checkCanonicalCore
                    (Just . Transition.checkedGlobalType)
                    atomP)
        premisePtoQ <-
            expectRight
                (Core.checkCanonicalCore
                    (Just . Transition.checkedGlobalType)
                    (Core.CImp atomP atomQ))
        premiseQtoR <-
            expectRight
                (Core.checkCanonicalCore
                    (Just . Transition.checkedGlobalType)
                    (Core.CImp atomQ atomR))
        reconstructedTarget <-
            expectRight
                (Core.checkCanonicalCore
                    (Just . Transition.checkedGlobalType)
                    atomR)
        builderWithP <-
            declareTyped
                "horn_p"
                premiseP
                builder
        builderWithPtoQ <-
            declareTyped
                "horn_p_to_q"
                premisePtoQ
                builderWithP
        builderWithHornInputs <-
            declareTyped
                "horn_q_to_r"
                premiseQtoR
                builderWithPtoQ
        reconstructedClaim <-
            expectRight
                (Backend.supportedProposition
                    (Vector.empty
                        :: Vector.Vector
                            (Void, Core.CoreType))
                    (Core.embedClosedCore
                        []
                        reconstructedTarget))
        reconstructedProblem <-
            expectRight
                (Transition.planTransitionTypedProblem
                    builderWithHornInputs
                    reconstructedClaim
                    []
                    []
                    (Transition.ExplicitFacts
                        ("horn_p"
                            :| [ "horn_p_to_q"
                               , "horn_q_to_r"
                               ]))
                    Backend.FirstOrderLocals)
        reconstructedPrepared <-
            expectRight
                (Provers.prepareTypedProverTask
                    Provers.DirectTask
                    reconstructedProblem)
        reconstructedResult <-
            runNoLoggingT
                (Provers.runPreparedTypedProver
                    (Provers.vampire
                        executablePath
                        Provers.defaultTimeLimit
                        Provers.defaultMemoryLimit)
                    reconstructedPrepared)
        reconstructedAccepted <-
            case reconstructedResult of
                Right answer
                    | Just run <-
                        Provers.provedVampireRun answer ->
                            pure run
                _ ->
                    assertFailure
                        ("expected accepted Horn Vampire run, got "
                            <> show reconstructedResult)
                        >> fail "unreachable"
        reconstructedBuilder <-
            expectRight
                (Transition.commitTransitionTypedVampireFact
                    Reconstruction.defaultReconstructionPolicy
                    ("horn_result" :| [])
                    (Transition.origin
                        Nowhere
                        Nothing
                        (Just "horn_result"))
                    reconstructedTarget
                    reconstructedPrepared
                    reconstructedAccepted
                    builderWithHornInputs)
        reconstructedModule <-
            expectRight
                (Transition.sealTransitionModule
                    Checking.initialLegacyCheckingEnvironment
                    reconstructedBuilder)
        reconstructedFact <-
            case Vector.unsnoc
                    (Transition.transitionAdmittedFacts
                        reconstructedModule) of
                Just (_earlier, finalFact) ->
                    pure finalFact
                Nothing ->
                    assertFailure
                        "expected a reconstructed admitted fact"
                        >> fail "unreachable"
        assertBool
            "supported accepted task becomes a reconstructed kernel proof"
            (Transition.admittedFactIsReconstructedKernelProof
                reconstructedFact)
        reconstructedTrust <-
            maybe
                (assertFailure
                    "expected typed reconstructed trust")
                pure
                (Transition.admittedFactTypedTrustDependencies
                    reconstructedFact)
        assertEqual
            "reconstruction inherits its three exact assumptions"
            3
            (Set.size
                (Transition.typedDeclaredAssumptionUses
                    reconstructedTrust))
        assertEqual
            "reconstructed run adds no trusted Vampire leaf"
            Set.empty
            (Transition.typedTrustedVampireUses
                reconstructedTrust)
        assertEqual
            "reconstructed run adds no Vampire lowering trust"
            Set.empty
            (Transition.typedVampireLoweringUses
                reconstructedTrust)
        tinyKernelLimits <-
            expectRight
                (Derivation.kernelReplayLimits 1 10)
        let tinyKernelPolicy =
                Reconstruction.reconstructionPolicy
                    (Reconstruction.reconstructionPolicyConnectionLimits
                        Reconstruction.defaultReconstructionPolicy)
                    tinyKernelLimits
        fallbackBuilder <-
            expectRight
                (Transition.commitTransitionTypedVampireFact
                    tinyKernelPolicy
                    ("horn_fallback" :| [])
                    (Transition.origin
                        Nowhere
                        Nothing
                        (Just "horn_fallback"))
                    reconstructedTarget
                    reconstructedPrepared
                    reconstructedAccepted
                    builderWithHornInputs)
        fallbackModule <-
            expectRight
                (Transition.sealTransitionModule
                    Checking.initialLegacyCheckingEnvironment
                    fallbackBuilder)
        fallbackFact <-
            case Vector.unsnoc
                    (Transition.transitionAdmittedFacts
                        fallbackModule) of
                Just (_earlier, finalFact) ->
                    pure finalFact
                Nothing ->
                    assertFailure
                        "expected a kernel-exhaustion fallback fact"
                        >> fail "unreachable"
        assertBool
            "kernel exhaustion retains accepted Vampire authority"
            (Transition.admittedFactIsTrustedVampire
                fallbackFact)
  where
    showResult = \case
        Left err ->
            "Left " <> show err
        Right _builder ->
            "Right builder"

publishesTypedInductive :: Assertion
publishesTypedInductive =
    withTemporaryDirectory "felix-transition-inductive" \temp -> do
        writeTheory
            (temp Posix.</> "entry.tex")
            []
            "entry"
        graph <- buildSearchedGraph temp "entry.tex"
        workspace <-
            expectRight
                =<< Parse.parseResolvedSourceGraph graph
        assignments <-
            expectRight
                (Legacy.assignLegacyModuleOrdinals
                    workspace)
        assignment <-
            case toList assignments of
                [only] ->
                    pure only
                actual ->
                    assertFailure
                        ("expected one module assignment, got "
                            <> show (length actual))
                        >> fail "unreachable"
        checkedFoundationValue <-
            expectRight Foundation.checkedFoundation
        builder <-
            expectRight
                (Transition.openTransitionModuleBuilder
                    checkedFoundationValue
                    Checking.initialLegacyCheckingEnvironment
                    assignment
                    [])
        let unprovedCarrier =
                TermOp Nowhere unprovedInductiveSymbol []
            unprovedBlocks =
                [ BlockInductive
                    Nowhere
                    "unproved_inductive"
                    Inductive
                        { inductiveSymbol =
                            unprovedInductiveSymbol
                        , inductiveParams = []
                        , inductiveDomain =
                            EmptySet Nowhere
                        , inductiveIntros =
                            IntroRule
                                []
                                ( EmptySet Nowhere
                                    `isElementOf`
                                        unprovedCarrier
                                )
                                :| []
                        }
                ]
        unproved <-
            try
                (Checking.runCheckingBlocks
                    unprovedBlocks
                    (Checking.initialTransitionCheckingStateWithTaskPreparation
                        Checking.WithoutDumpPremselTraining
                        id
                        builder
                        (\_batch ->
                            assertFailure
                                "unproved inductive emitted a legacy obligation")))
                :: IO
                    (Either
                        Checking.CheckingError
                        Checking.CheckingState)
        case unproved of
            Left checkingError ->
                assertBool
                    "missing exact guard is reported"
                    ("has no authorized typed fact"
                        `Text.isInfixOf`
                            Text.pack (show checkingError))
            Right _checked ->
                assertFailure
                    "inductive with an unproved domain guard was admitted"
        unchanged <-
            expectRight
                (Transition.sealTransitionModule
                    Checking.initialLegacyCheckingEnvironment
                    builder)
        assertEqual
            "failed inductive publishes no global"
            0
            (Vector.length
                (Transition.transitionAdmittedGlobals
                    unchanged))
        assertEqual
            "failed inductive publishes no fact"
            0
            (Vector.length
                (Transition.transitionAdmittedFacts
                    unchanged))
        let parameter =
                NamedVar "domain"
            domain =
                TermOp
                    Nowhere
                    cumulSymbol
                    [TermVar parameter]
            carrier =
                TermOp
                    Nowhere
                    typedInductiveSymbol
                    [TermVar parameter]
            blocks =
                [ BlockInductive
                    Nowhere
                    "typed_inductive"
                    Inductive
                        { inductiveSymbol =
                            typedInductiveSymbol
                        , inductiveParams = [parameter]
                        , inductiveDomain = domain
                        , inductiveIntros =
                            IntroRule
                                []
                                (TermVar parameter
                                    `isElementOf`
                                        carrier)
                                :| []
                        }
                ]
        checked <-
            Checking.runCheckingBlocks
                blocks
                (Checking.initialTransitionCheckingStateWithTaskPreparation
                    Checking.WithoutDumpPremselTraining
                    id
                    builder
                    (\_batch ->
                        assertFailure
                            "typed inductive emitted a legacy obligation"))
        finalBuilder <-
            maybe
                (assertFailure
                    "checking lost its transition builder"
                    >> fail "unreachable")
                pure
                (Checking.checkingTransitionModuleBuilder
                    checked)
        admitted <-
            expectRight
                (Transition.sealTransitionModule
                    (Checking.checkingStateEnvironment
                        checked)
                    finalBuilder)
        assertEqual
            "one transparent carrier"
            1
            (Vector.length
                (Transition.transitionAdmittedGlobals
                    admitted))
        assertEqual
            "four derived facts"
            [True, True, True, True]
            ( Transition.admittedFactIsKernelProof
                <$> Vector.toList
                    (Transition.transitionAdmittedFacts
                        admitted)
            )
        assertEqual
            "four replayed inductive facts"
            4
            (Transition.transitionAdmittedKernelProofCount
                admitted)
        assertBool
            "foundation guard dependency is retained"
            (Foundation.UnivOfContains
                `Set.member`
                    Transition.typedFoundationUses
                        (Transition.transitionAdmittedTypedTrustDependencies
                            admitted))
  where
    typedInductiveSymbol =
        mkMixfixItem
            [ Just (Command "typedfin")
            , Just InvisibleBraceL
            , Nothing
            , Just InvisibleBraceR
            ]
            "typed_inductive"
            NonAssoc

    cumulSymbol =
        mkMixfixItem
            [ Just (Command "cumul")
            , Just InvisibleBraceL
            , Nothing
            , Just InvisibleBraceR
            ]
            "cumul"
            NonAssoc

    unprovedInductiveSymbol =
        mkMixfixItem
            [Just (Command "unprovedfin")]
            "unproved_inductive"
            NonAssoc

publishesLegacyImportViews :: Assertion
publishesLegacyImportViews =
    withTemporaryDirectory "felix-legacy-import-view" \temp -> do
        writeTheory (temp Posix.</> "shared.tex") [] "shared"
        writeTheory
            (temp Posix.</> "a.tex")
            ["shared.tex"]
            "a"
        writeTheory
            (temp Posix.</> "b.tex")
            ["shared.tex"]
            "b"
        writeTheory
            (temp Posix.</> "entry.tex")
            ["a.tex", "b.tex"]
            "entry"
        graph <- buildSearchedGraph temp "entry.tex"
        workspace <-
            expectRight
                =<< Parse.parseResolvedSourceGraph graph
        assignments <-
            expectRight
                (Legacy.assignLegacyModuleOrdinals workspace)
        case toList assignments of
            [ sharedAssignment
                , aAssignment
                , bAssignment
                , entryAssignment
                ] -> do
                    shared <-
                        admitOne
                            sharedAssignment
                            (Legacy.emptyLegacyImportedView
                                Checking.initialLegacyCheckingEnvironment)
                            "shared_fact"
                            Bottom
                            (Location 1)
                    sharedView <-
                        expectRight
                            (Legacy.legacyImportedView
                                Checking.initialLegacyCheckingEnvironment
                                [shared])
                    a <-
                        admitOne
                            aAssignment
                            sharedView
                            "a_fact"
                            Top
                            (Location 2)
                    b <-
                        admitOne
                            bAssignment
                            sharedView
                            "b_fact"
                            Top
                            (Location 3)
                    diamondView <-
                        expectRight
                            (Legacy.legacyImportedView
                                Checking.initialLegacyCheckingEnvironment
                                [a, b])
                    entry <-
                        expectRight
                            (Legacy.sealLegacyModuleStage
                                (Legacy.legacyImportedCheckingEnvironment
                                    diamondView)
                                (Legacy.openLegacyModuleStage
                                    entryAssignment
                                    diamondView))
                    assertEqual
                        "direct imports retain textual order"
                        [1, 2]
                        ( Legacy.legacyModuleOrdinalValue
                            <$> Vector.toList
                                (Legacy.legacyAdmittedDirectImports
                                    entry)
                        )
                    assertEqual
                        "diamond facts retain imported source order"
                        [0, 1, 2]
                        ( Legacy.legacyModuleOrdinalValue
                            . Legacy.legacyFactModule
                            . Legacy.legacyFactEntryReference
                            <$> Vector.toList
                                (Legacy.legacyAdmittedVisibleFacts
                                    entry)
                        )
                    assertEqual
                        "equal statements at different references remain"
                        3
                        (Vector.length
                            (Legacy.legacyAdmittedVisibleFacts entry))
                    let environmentSymbol =
                            SymbolMixfix
                                (mkMixfixItem
                                    [Just
                                        (Command
                                            "module_environment")]
                                    "module_environment"
                                    NonAssoc)
                        environmentWith body =
                            Legacy.legacyCheckingEnvironment
                                (HashMap.insert
                                    environmentSymbol
                                    (toScope body)
                                    (Legacy.legacyEnvironmentAbbreviations
                                        Checking.initialLegacyCheckingEnvironment))
                                (Legacy.legacyEnvironmentPredicateDefinitions
                                    Checking.initialLegacyCheckingEnvironment)
                                (Legacy.legacyEnvironmentDependencies
                                    Checking.initialLegacyCheckingEnvironment)
                                (Legacy.legacyEnvironmentOwnedSymbols
                                    Checking.initialLegacyCheckingEnvironment)
                                (Legacy.legacyEnvironmentOwnedSymbolMarkers
                                    Checking.initialLegacyCheckingEnvironment)
                                (Legacy.legacyEnvironmentFrozenSymbols
                                    Checking.initialLegacyCheckingEnvironment)
                                (Legacy.legacyEnvironmentStructs
                                    Checking.initialLegacyCheckingEnvironment)
                                (Legacy.legacyEnvironmentDefinedMarkers
                                    Checking.initialLegacyCheckingEnvironment)
                    environmentA <-
                        admitEnvironment
                            aAssignment
                            (Legacy.emptyLegacyImportedView
                                Checking.initialLegacyCheckingEnvironment)
                            (environmentWith Top)
                    environmentView <-
                        expectRight
                            (Legacy.legacyImportedView
                                Checking.initialLegacyCheckingEnvironment
                                [environmentA])
                    assertEqual
                        "admitted semantic environment is imported"
                        (Just (toScope Top))
                        (HashMap.lookup
                            environmentSymbol
                            (Legacy.legacyEnvironmentAbbreviations
                                (Legacy.legacyImportedCheckingEnvironment
                                    environmentView)))
                    environmentB <-
                        admitEnvironment
                            bAssignment
                            (Legacy.emptyLegacyImportedView
                                Checking.initialLegacyCheckingEnvironment)
                            (environmentWith Bottom)
                    case Legacy.legacyImportedView
                            Checking.initialLegacyCheckingEnvironment
                            [environmentA, environmentB] of
                        Left Legacy.LegacyImportedEnvironmentConflict{} ->
                            pure ()
                        Left err ->
                            assertFailure
                                ("expected imported environment conflict, got "
                                    <> show err)
                        Right _ ->
                            assertFailure
                                "expected imported environment conflict"

                    conflictingA <-
                        admitOne
                            aAssignment
                            (Legacy.emptyLegacyImportedView
                                Checking.initialLegacyCheckingEnvironment)
                            "conflicting"
                            Top
                            (Location 4)
                    conflictingB <-
                        admitOne
                            bAssignment
                            (Legacy.emptyLegacyImportedView
                                Checking.initialLegacyCheckingEnvironment)
                            "conflicting"
                            Bottom
                            (Location 5)
                    case Legacy.legacyImportedView
                            Checking.initialLegacyCheckingEnvironment
                            [conflictingA, conflictingB] of
                        Left Legacy.LegacyImportedAliasConflict{} ->
                            pure ()
                        Left err ->
                            assertFailure
                                ("expected imported alias conflict, got "
                                    <> show err)
                        Right _ ->
                            assertFailure
                                "expected imported alias conflict"
            actual ->
                assertFailure
                    ("expected four module assignments, got "
                        <> show (length actual))
  where
    admitOne assignment imported alias statement location = do
        let stage =
                Legacy.openLegacyModuleStage
                    assignment
                    imported
            staged =
                Facts.stageFact
                    (alias :| [])
                    (Facts.factOrigin location alias)
                    (Facts.prepareSemanticFact statement)
        reservation <-
            expectRight
                (Legacy.reserveLegacyDeclaration
                    (staged :| [])
                    stage)
        let reserved =
                NonEmpty.head
                    (Legacy.legacyReservedFacts reservation)
            admitted =
                Legacy.authorizeLegacyDeclaredAssumption
                    stage
                    Legacy.DeclaredUserAxiom
                    reserved
        stage' <-
            expectRight
                (Legacy.appendEstablishedLegacyDeclaration
                    reservation
                    (admitted :| [])
                    stage)
        expectRight
            (Legacy.sealLegacyModuleStage
                (Legacy.legacyImportedCheckingEnvironment imported)
                stage')

    admitEnvironment assignment imported finalEnvironment =
        expectRight
            (Legacy.sealLegacyModuleStage
                finalEnvironment
                (Legacy.openLegacyModuleStage assignment imported))

rejectsSiblingSyntaxLeakage :: Assertion
rejectsSiblingSyntaxLeakage =
    withTemporaryDirectory "felix-source-syntax-world" \temp -> do
        writeFile
            (temp Posix.</> "use.tex")
            (unlines
                [ "\\begin{axiom}\\label{use}"
                , "  $x$ is special."
                , "\\end{axiom}"
                ])
        writeAdjectiveDefinition
            (temp Posix.</> "declare.tex")
            "shared_special"
        writeTheory
            (temp Posix.</> "entry.tex")
            ["use.tex", "declare.tex"]
            "entry"
        graph <- buildSearchedGraph temp "entry.tex"
        result <- Parse.parseResolvedSourceGraph graph
        case result of
            Left (Parse.SourceParseError source _parseError) ->
                assertEqual
                    "syntax consumer fails in its own module"
                    "use.tex"
                    (safeRelativePathFilePath
                        (resolvedSourceRelativePath source))
            Left err ->
                assertFailure
                    ("expected a source-local parse error, got "
                        <> show err)
            Right workspace ->
                assertFailure
                    ("sibling syntax leaked into use.tex: "
                        <> show workspace)

parsesSourceFixities :: Assertion
parsesSourceFixities =
    withTemporaryDirectory "felix-source-fixity" \temp -> do
        writeFile
            (temp Posix.</> "entry.tex")
            ( syntaxFunctionDefinition
                "loose"
                "loose"
                (Just "%! infixl 0")
              <> syntaxFunctionDefinition
                "tight"
                "tight"
                (Just "%! infixr 7")
              <> axiomBlock
                "loose_associativity"
                "a\\loose b\\loose c = a"
              <> axiomBlock
                "tight_associativity"
                "a\\tight b\\tight c = a"
              <> axiomBlock
                "mixed_precedence"
                "a\\loose b\\tight c = a"
              <> axiomBlock
                "parenthesized_precedence"
                "(a\\loose b)\\tight c = a"
            )
        graph <- buildSearchedGraph temp "entry.tex"
        workspace <- expectRight
            =<< Parse.parseResolvedSourceGraph graph
        let root =
                Parse.parsedWorkspaceRootModule workspace
            localEntries =
                Interface.canonicalSyntaxDeltaEntries
                    (Interface.moduleSyntaxLocalDelta
                        (Parse.parsedModuleSyntaxInterface root))
        assertExpressionFixity
            "loose"
            Raw.LeftAssoc
            0
            localEntries
        assertExpressionFixity
            "tight"
            Raw.RightAssoc
            7
            localEntries
        assertEqual
            "source declaration occurrences"
            [0, 1]
            (Parse.parsedSyntaxOccurrenceBlockIndex
                <$> Parse.parsedModuleSyntaxOccurrences root)
        case drop 2 (Parse.parsedModuleBlocks root) of
            [ looseAssociativity
              , tightAssociativity
              , mixedPrecedence
              , parenthesizedPrecedence
              ] -> do
                    assertAxiomLeftShape
                        "left associativity"
                        "loose(loose(a,b),c)"
                        looseAssociativity
                    assertAxiomLeftShape
                        "right associativity"
                        "tight(a,tight(b,c))"
                        tightAssociativity
                    assertAxiomLeftShape
                        "mixed precedence"
                        "loose(a,tight(b,c))"
                        mixedPrecedence
                    assertAxiomLeftShape
                        "parentheses override precedence"
                        "tight(loose(a,b),c)"
                        parenthesizedPrecedence
            blocks ->
                assertFailure
                    ("expected four fixity axioms, got "
                        <> show blocks)

parsesLibraryFixities :: Assertion
parsesLibraryFixities =
    withTemporaryDirectory "felix-source-library-fixity" \temp -> do
        writeFile
            (temp Posix.</> "entry.tex")
            ( syntaxFunctionDefinition
                "cdot"
                "cdot"
                (Just "%! infixl 4")
              <> syntaxFunctionDefinition
                "symdiff"
                "symdiff"
                (Just "%! infixl 1")
              <> axiomBlock
                "cdot_associativity"
                "a\\cdot b\\cdot c = a"
              <> axiomBlock
                "symdiff_associativity"
                "a\\symdiff b\\symdiff c = a"
              <> axiomBlock
                "library_mixed_precedence"
                "a\\symdiff b\\cdot c = a"
              <> axiomBlock
                "library_parentheses"
                "(a\\symdiff b)\\cdot c = a"
            )
        graph <- buildSearchedGraph temp "entry.tex"
        workspace <- expectRight
            =<< Parse.parseResolvedSourceGraph graph
        case drop 2
                (Parse.parsedModuleBlocks
                    (Parse.parsedWorkspaceRootModule workspace)) of
            [ cdotAssociativity
              , symdiffAssociativity
              , mixedPrecedence
              , parenthesizedPrecedence
              ] -> do
                    assertAxiomLeftShape
                        "cdot left associativity"
                        "cdot(cdot(a,b),c)"
                        cdotAssociativity
                    assertAxiomLeftShape
                        "symdiff left associativity"
                        "symdiff(symdiff(a,b),c)"
                        symdiffAssociativity
                    assertAxiomLeftShape
                        "cdot binds tighter than symdiff"
                        "symdiff(a,cdot(b,c))"
                        mixedPrecedence
                    assertAxiomLeftShape
                        "library parentheses override precedence"
                        "cdot(symdiff(a,b),c)"
                        parenthesizedPrecedence
            blocks ->
                assertFailure
                    ("expected four library-fixity axioms, got "
                        <> show blocks)

validatesSourcePragmaAssociations :: Assertion
validatesSourcePragmaAssociations =
    forM_ cases \(description, contents, checkProblem) ->
        withTemporaryDirectory
            ("felix-source-pragma-" <> description)
            \temp -> do
                writeFile
                    (temp Posix.</> "entry.tex")
                    contents
                graph <- buildSearchedGraph temp "entry.tex"
                result <- Parse.parseResolvedSourceGraph graph
                case result of
                    Left
                        (Parse.SourceSyntaxDeclarationError
                            source
                            problem) -> do
                                assertEqual
                                    "pragma source"
                                    "entry.tex"
                                    (safeRelativePathFilePath
                                        (resolvedSourceRelativePath source))
                                checkProblem problem
                    Left err ->
                        assertFailure
                            ("expected source pragma error, got "
                                <> show err)
                    Right workspace ->
                        assertFailure
                            ("expected source pragma rejection, got "
                                <> show workspace)
  where
    cases
        :: [ ( String
             , String
             , Parse.SyntaxDeclarationError -> Assertion
             )
           ]
    cases =
        [ ( "outside"
          , "%! infixl 1\n" <> theoryBlock "outside"
          , \case
                Parse.SyntaxPragmaOutsideDeclaration{} ->
                    pure ()
                problem ->
                    unexpected "outside-declaration pragma" problem
          )
        , ( "inside-nonsyntax"
          , unlines
                [ "\\begin{axiom}\\label{inside_nonsyntax}"
                , "  %! infixl 1"
                , "  $x = x$."
                , "\\end{axiom}"
                ]
          , \case
                Parse.SyntaxPragmaOutsideDeclaration location ->
                    assertEqual
                        "pragma in non-syntax chunk"
                        2
                        (locLine location)
                problem ->
                    unexpected "non-syntax declaration pragma" problem
          )
        , ( "missing"
          , syntaxFunctionDefinition
                "missing"
                "missing"
                Nothing
          , \case
                Parse.MissingSyntaxPragma{} ->
                    pure ()
                problem ->
                    unexpected "missing pragma" problem
          )
        , ( "duplicate"
          , unlines
                [ "\\begin{abbreviation}\\label{duplicate}"
                , "  %! infixl 1"
                , "  %! infixl 1"
                , "  $x\\duplicate y = x$."
                , "\\end{abbreviation}"
                ]
          , \case
                Parse.DuplicateSyntaxPragma{} ->
                    pure ()
                problem ->
                    unexpected "duplicate pragma" problem
          )
        , ( "irrelevant"
          , unlines
                [ "\\begin{definition}\\label{irrelevant}"
                , "  %! infixl 1"
                , "  $x$ is irrelevant iff $x = x$."
                , "\\end{definition}"
                ]
          , \case
                Parse.IrrelevantSyntaxPragma{} ->
                    pure ()
                problem ->
                    unexpected "irrelevant pragma" problem
          )
        , ( "multiple-without-pragma"
          , unlines
                [ "\\begin{datatype}\\label{multiple_patterns}"
                , "  Define $\\patternkind$ inductively as follows."
                , "  \\begin{enumerate}"
                , "    \\item $(x \\firstpattern y) \\in \\patternkind$."
                , "    \\item $(x \\secondpattern y) \\in \\patternkind$."
                , "  \\end{enumerate}"
                , "\\end{datatype}"
                ]
          , \case
                problem@(Parse.MultipleNewSyntaxPatternsWithoutPragma
                        location
                        patterns) -> do
                            assertEqual
                                "first new pattern location"
                                4
                                (locLine location)
                            assertEqual
                                "new pattern count"
                                2
                                (NonEmpty.length patterns)
                            assertBool
                                "accurate multiple-pattern message"
                                ("several new eligible patterns that V1 cannot select between"
                                    `List.isInfixOf` show problem)
                            assertBool
                                "message requires an unambiguous declaration"
                                ("make the declaration unambiguous"
                                    `List.isInfixOf` show problem)
                problem ->
                    unexpected "multiple unannotated patterns" problem
          )
        , ( "fixed"
          , unlines
                [ "\\begin{abbreviation}\\label{local_addition}"
                , "  %! infixl 1"
                , "  $x + y = x$."
                , "\\end{abbreviation}"
                ]
          , \case
                Parse.SyntaxPragmaOnFixedReuse{} ->
                    pure ()
                problem ->
                    unexpected "fixed-base pragma" problem
          )
        ]

    unexpected expected problem =
        assertFailure
            ("expected " <> expected <> ", got " <> show problem)

rejectsFixedBaseCategoryMismatch :: Assertion
rejectsFixedBaseCategoryMismatch =
    withTemporaryDirectory "felix-source-fixed-category" \temp -> do
        writeFile
            (temp Posix.</> "entry.tex")
            (unlines
                [ "\\begin{definition}\\label{local_add_relation}"
                , "  $x + y$ iff $x = y$."
                , "\\end{definition}"
                ])
        graph <- buildSearchedGraph temp "entry.tex"
        collision <- expectLexiconCollision
            =<< Parse.parseResolvedSourceGraph graph
        assertEqual
            "fixed collision pattern"
            (Raw.HoleCons
                (Raw.TokenCons
                    (Raw.Symbol "+")
                    (Raw.HoleCons Raw.End)))
            (Parse.lexiconCollisionPattern collision)
        case toList (Parse.lexiconCollisionOrigins collision) of
            [ Parse.FixedLexiconOrigin
                    Interface.CanonicalExpressionFunction{}
              , Parse.SourceLexiconOrigin
                    Interface.CanonicalRelation{}
                    source
                    location
              ] -> do
                    assertEqual
                        "local collision source"
                        "entry.tex"
                        (safeRelativePathFilePath
                            (resolvedSourceRelativePath source))
                    assertLocation
                        "local collision declaration"
                        "entry.tex"
                        1
                        location
            origins ->
                assertFailure
                    ("expected fixed/source category origins, got "
                        <> show origins)

retainsMultiItemSyntaxOccurrences :: Assertion
retainsMultiItemSyntaxOccurrences =
    withTemporaryDirectory "felix-source-multi-item-syntax" \temp -> do
        writeFile
            (temp Posix.</> "entry.tex")
            (unlines
                [ "\\begin{datatype}\\label{multi_item}"
                , "  Define $\\itemkind$ inductively as follows."
                , "  \\begin{enumerate}"
                , "    \\item $\\itemzero \\in \\itemkind$."
                , "    \\item $\\itemsucc{x} \\in \\itemkind$ for $x \\in \\itemkind$."
                , "  \\end{enumerate}"
                , "\\end{datatype}"
                ])
        graph <- buildSearchedGraph temp "entry.tex"
        workspace <- expectRight
            =<< Parse.parseResolvedSourceGraph graph
        let root =
                Parse.parsedWorkspaceRootModule workspace
            occurrences =
                Parse.parsedModuleSyntaxOccurrences root
            summarize occurrence =
                case Parse.parsedSyntaxOccurrenceEntry occurrence of
                    Interface.CanonicalExpressionFunction
                            _pattern
                            marker
                            _fixity ->
                        Right
                            ( Parse.parsedSyntaxOccurrenceBlockIndex
                                occurrence
                            , locLine
                                (Parse.parsedSyntaxOccurrenceLocation
                                    occurrence)
                            , Parse.parsedSyntaxOccurrenceMarker occurrence
                            , marker
                            )
                    entry ->
                        Left entry
        case traverse summarize occurrences of
            Right summaries ->
                assertEqual
                    "block association and scanner order"
                    [ (0, 2, "multi_item", "multi_item")
                    , (0, 4, "itemzero", "itemzero")
                    , (0, 5, "itemsucc", "itemsucc")
                    ]
                    summaries
            Left entry ->
                assertFailure
                    ("expected an expression occurrence, got "
                        <> show entry)
        case (Parse.parsedModuleBlocks root, occurrences) of
            ( Raw.BlockData _location _title blockMarker _datatype : _
              , firstOccurrence : _
              ) ->
                assertEqual
                    "first occurrence is the declaration-head anchor"
                    blockMarker
                    (Parse.parsedSyntaxOccurrenceMarker firstOccurrence)
            _ ->
                assertFailure "expected a datatype block and its occurrences"

propagatesImportedSyntax :: Assertion
propagatesImportedSyntax =
    withTemporaryDirectory "felix-source-syntax-diamond" \temp -> do
        writeFile
            (temp Posix.</> "base.tex")
            (syntaxFunctionDefinition
                "star"
                "star"
                (Just "%! infixl 3"))
        writeFile
            (temp Posix.</> "left.tex")
            ("\\import{base.tex}\n"
                <> syntaxFunctionDefinition
                    "star"
                    "star"
                    Nothing)
        writeTheory
            (temp Posix.</> "right.tex")
            ["base.tex"]
            "right"
        writeFile
            (temp Posix.</> "entry.tex")
            (unlines
                [ "\\import{left.tex}"
                , "\\import{right.tex}"
                ]
                <> axiomBlock
                    "imported_use"
                    "a\\star b\\star c = a")
        graph <- buildSearchedGraph temp "entry.tex"
        workspace <- expectRight
            =<< Parse.parseResolvedSourceGraph graph
        baseModule <- findParsedModule "base.tex" workspace
        leftModule <- findParsedModule "left.tex" workspace
        rightModule <- findParsedModule "right.tex" workspace
        let root =
                Parse.parsedWorkspaceRootModule workspace
            interface =
                Parse.parsedModuleSyntaxInterface
            localEntries parsed =
                Interface.canonicalSyntaxDeltaEntries
                    (Interface.moduleSyntaxLocalDelta
                        (interface parsed))
        assertEqual "base exports one syntax entry"
            1
            (length (localEntries baseModule))
        assertEqual "imported reuse emits no local entry"
            []
            (localEntries leftModule)
        assertEqual "imported reuse retains its occurrence"
            1
            (length
                (Parse.parsedModuleSyntaxOccurrences leftModule))
        assertEqual "empty diamond branch has no occurrence"
            []
            (Parse.parsedModuleSyntaxOccurrences rightModule)
        assertEqual "equal diamond interfaces"
            (Interface.moduleSyntaxAssertedId
                (interface leftModule))
            (Interface.moduleSyntaxAssertedId
                (interface rightModule))
        assertEqual "root coalesces equal direct interfaces"
            1
            (length
                (Interface.moduleSyntaxDirectInputs
                    (interface root)))
        case Parse.parsedModuleBlocks root of
            [block] ->
                assertAxiomLeftShape
                    "imported left associativity"
                    "star(star(a,b),c)"
                    block
            blocks ->
                assertFailure
                    ("expected one imported-syntax axiom, got "
                        <> show blocks)
        writeFile
            (temp Posix.</> "left.tex")
            ("\\import{base.tex}\n"
                <> syntaxFunctionDefinition
                    "star"
                    "star"
                    (Just "%! infixl 3"))
        reuseGraph <- buildSearchedGraph temp "left.tex"
        reuseResult <-
            Parse.parseResolvedSourceGraph reuseGraph
        case reuseResult of
            Left
                (Parse.SourceSyntaxDeclarationError
                    _source
                    Parse.SyntaxPragmaOnImportedReuse{}) ->
                        pure ()
            Left err ->
                assertFailure
                    ("expected imported-reuse pragma rejection, got "
                        <> show err)
            Right reused ->
                assertFailure
                    ("expected imported-reuse pragma rejection, got "
                        <> show reused)

rejectsUnequalImportedSyntax :: Assertion
rejectsUnequalImportedSyntax =
    forM_ cases \(description, leftDefinition, rightDefinition) ->
        withTemporaryDirectory
            ("felix-source-imported-collision-" <> description)
            \temp -> do
                writeFile
                    (temp Posix.</> "a.tex")
                    leftDefinition
                writeFile
                    (temp Posix.</> "b.tex")
                    rightDefinition
                writeTheory
                    (temp Posix.</> "entry.tex")
                    ["a.tex", "b.tex"]
                    "entry"
                graph <- buildSearchedGraph temp "entry.tex"
                collision <- expectLexiconCollision
                    =<< Parse.parseResolvedSourceGraph graph
                (firstLocation, secondLocation) <-
                    expectTwoCollisionLocations collision
                assertLocation
                    "first imported declaration"
                    "a.tex"
                    1
                    firstLocation
                assertLocation
                    "second imported declaration"
                    "b.tex"
                    1
                    secondLocation
  where
    cases =
        [ ( "marker"
          , syntaxFunctionDefinition
                "clash_left"
                "clash"
                (Just "%! infixl 2")
          , syntaxFunctionDefinition
                "clash_right"
                "clash"
                (Just "%! infixl 2")
          )
        , ( "fixity"
          , syntaxFunctionDefinition
                "clash"
                "clash"
                (Just "%! infixl 2")
          , syntaxFunctionDefinition
                "clash"
                "clash"
                (Just "%! infixr 2")
          )
        ]

distinguishesPhysicalSourceLocations :: Assertion
distinguishesPhysicalSourceLocations =
    withTemporaryDirectory "felix-source-location-identity" \temp -> do
        let projectRoot = temp Posix.</> "project"
            libraryRoot = temp Posix.</> "library"
            projectEntry = projectRoot Posix.</> "entry.tex"
            libraryEntry = libraryRoot Posix.</> "entry.tex"
        Directory.createDirectory projectRoot
        Directory.createDirectory libraryRoot
        writeFile projectEntry
            ("\\import{entry.tex}\n"
                <> adjectiveDefinition "project_adjective")
        writeNounDefinition libraryEntry "library_noun"
        mounts <- expectRight =<< prepareSourceMounts
            [ (sourceMountId "library", libraryRoot)
            , (sourceMountId "project", projectRoot)
            ]
        request <- expectRight =<< existingRoot projectEntry
        graph <- expectRight =<< buildResolvedSourceGraph mounts request
        collision <- expectLexiconCollision
            =<< Parse.parseResolvedSourceGraph graph
        assertEqual "normalized cross-category pattern"
            (Raw.TokenCons (Raw.Word "special") Raw.End)
            (Parse.lexiconCollisionPattern collision)
        (libraryLocation, projectLocation) <-
            expectTwoCollisionLocations collision
        assertEqual "accepted display path"
            "entry.tex"
            (locFile libraryLocation)
        assertEqual "accepted declaration line"
            1
            (locLine libraryLocation)
        assertEqual "colliding display path"
            "entry.tex"
            (locFile projectLocation)
        assertEqual "colliding declaration line"
            2
            (locLine projectLocation)
        canonicalProject <- Directory.canonicalizePath projectEntry
        canonicalLibrary <- Directory.canonicalizePath libraryEntry
        let rendered = show collision
            quotedLibrary = show canonicalLibrary
            quotedProject = show canonicalProject
        assertBool "rendered error includes accepted canonical path"
            (quotedLibrary `List.isInfixOf` rendered)
        assertBool "rendered error includes colliding canonical path"
            (quotedProject `List.isInfixOf` rendered)
        assertBool "canonical locations render in declaration order"
            (substringIndex quotedLibrary rendered
                < substringIndex quotedProject rendered)

retainsWorkspaceLocationDisplayPath :: Assertion
retainsWorkspaceLocationDisplayPath =
    withTemporaryDirectory "felix-source-location-display" \temp -> do
        let nested = temp Posix.</> "nested"
            entry = nested Posix.</> "entry.tex"
        Directory.createDirectory nested
        writeTheory entry [] "entry"
        outerMounts <- oneMount "project" temp
        outerRequest <- expectRight (searchedRoot "nested/entry.tex")
        outerGraph <- expectRight =<<
            buildResolvedSourceGraph outerMounts outerRequest
        outerWorkspace <- expectRight =<<
            Parse.parseResolvedSourceGraph outerGraph
        innerMounts <- oneMount "library" nested
        innerRequest <- expectRight (searchedRoot "entry.tex")
        innerGraph <- expectRight =<<
            buildResolvedSourceGraph innerMounts innerRequest
        innerWorkspace <- expectRight =<<
            Parse.parseResolvedSourceGraph innerGraph
        let outerLocation =
                onlyAxiomLocation
                    (Parse.parsedWorkspaceRootModule outerWorkspace)
            innerLocation =
                onlyAxiomLocation
                    (Parse.parsedWorkspaceRootModule innerWorkspace)
        assertEqual "outer-mount display path"
            "nested/entry.tex"
            (locFile outerLocation)
        assertEqual "more-specific-mount display path"
            "entry.tex"
            (locFile innerLocation)
        outerFileId <- expectJust "outer workspace file id"
            (locFileId outerLocation)
        innerFileId <- expectJust "inner workspace file id"
            (locFileId innerLocation)
        assertBool "distinct display registrations use distinct file ids"
            (outerFileId /= innerFileId)
        canonicalEntry <- Directory.canonicalizePath entry
        assertEqual "outer physical location key"
            (Just canonicalEntry)
            (lookupFileIdentityPath outerFileId)
        assertEqual "inner physical location key"
            (Just canonicalEntry)
            (lookupFileIdentityPath innerFileId)

reportsImportedLexerErrorFirst :: Assertion
reportsImportedLexerErrorFirst =
    withTemporaryDirectory "felix-source-lexer-error-order" \temp -> do
        let malformedSource = unlines
                [ "\\begin{axiom}"
                , "#"
                , "\\end{axiom}"
                ]
        writeFile
            (temp Posix.</> "imported.tex")
            malformedSource
        writeFile
            (temp Posix.</> "entry.tex")
            ("\\import{imported.tex}\n" <> malformedSource)
        graph <- buildSearchedGraph temp "entry.tex"
        result <- Parse.parseResolvedSourceGraph graph
        case result of
            Left (Parse.SourceParseError source (Parse.TokenError _err)) ->
                assertEqual "first lexer error" "imported.tex"
                    (safeRelativePathFilePath
                        (resolvedSourceRelativePath source))
            Left err ->
                assertFailure ("expected lexer error, got " <> show err)
            Right workspace ->
                assertFailure ("expected lexer error, got " <> show workspace)

reportsMalformedLexicalDeclaration :: Assertion
reportsMalformedLexicalDeclaration =
    withTemporaryDirectory "felix-source-malformed-lexical" \temp -> do
        writeFile
            (temp Posix.</> "entry.tex")
            (unlines
                [ "\\begin{abbreviation}\\label{malformed_function}"
                , "  $x = \\emptyset$."
                , "\\end{abbreviation}"
                ])
        graph <- buildSearchedGraph temp "entry.tex"
        result <- Parse.parseResolvedSourceGraph graph
        void (evaluate (length (show result)))
        case result of
            Left
                (Parse.SourceParseError
                    source
                    (Parse.LexicalScanFailure
                        (Adapt.InvalidFunctionPattern
                            location
                            Adapt.FunctionPatternBareVariable))) -> do
                                assertEqual "malformed source"
                                    "entry.tex"
                                    (safeRelativePathFilePath
                                        (resolvedSourceRelativePath source))
                                assertLocation
                                    "malformed declaration"
                                    "entry.tex"
                                    1
                                    location
            Left err ->
                assertFailure
                    ("expected typed lexical scan failure, got " <> show err)
            Right workspace ->
                assertFailure
                    ("expected typed lexical scan failure, got "
                        <> show workspace)

rejectsMalformedInductivePattern :: Assertion
rejectsMalformedInductivePattern =
    case runLexer (FileId 0) "inductive.tex" source of
        Left err ->
            assertFailure ("could not tokenize fixture: " <> show err)
        Right (_imports, [chunk]) ->
            case Adapt.scanChunk chunk of
                Left
                    (Adapt.InvalidFunctionPattern
                        _location
                        Adapt.FunctionPatternBareVariable) ->
                            pure ()
                Left err ->
                    assertFailure
                        ("expected bare-variable scan failure, got "
                            <> show err)
                Right scans ->
                    assertFailure
                        ("expected bare-variable scan failure, got "
                            <> show scans)
        Right (_imports, chunks) ->
            assertFailure
                ("expected one lexical chunk, got " <> show (length chunks))
  where
    source =
        Text.pack
            (unlines
            [ "\\begin{inductive}\\label{malformed_inductive}"
            , "  Define $x\\subseteq\\pow{x}$ inductively."
            , "\\end{inductive}"
            ])

acceptsAdjectiveSignature :: Assertion
acceptsAdjectiveSignature =
    withTemporaryDirectory "felix-source-signature-adjective" \temp -> do
        writeFile
            (temp Posix.</> "entry.tex")
            (unlines
                [ "\\begin{signature}\\label{reflexive_signature}"
                , "  Suppose $A$ is a set."
                , "  Then $x$ can be reflexive."
                , "\\end{signature}"
                , "\\begin{axiom}\\label{reflexive_use}"
                , "  $x$ is reflexive."
                , "\\end{axiom}"
                ])
        graph <- buildSearchedGraph temp "entry.tex"
        workspace <- expectRight
            =<< Parse.parseResolvedSourceGraph graph
        let blocks = Parse.importedBeforeImporterBlocks workspace
        case blocks of
            [ Raw.BlockSig
                    _signatureLocation
                    _signatureTitle
                    _signatureMarker
                    [_signatureAssumption]
                    (Raw.SignatureAdj
                        _variable
                        (Raw.Adj _adjectiveLocation declaredAdjective []))
              , Raw.BlockAxiom{}
              ] -> do
                    assertEqual
                        "signature marker enters the lexicon"
                        "reflexive_signature"
                        (Raw.lexicalItemMarker declaredAdjective)
            _ ->
                assertFailure
                    ("unexpected adjective-signature blocks: " <> show blocks)
        semanticBlocks <- expectRight (Meaning.meaning blocks)
        void
            (Checking.check
                Checking.WithoutDumpPremselTraining
                semanticBlocks)

rejectsQuantifiedSymbolicSignatureTerm :: Assertion
rejectsQuantifiedSymbolicSignatureTerm =
    withTemporaryDirectory "felix-source-signature-quantified-term" \temp -> do
        writeFile
            (temp Posix.</> "entry.tex")
            (unlines
                [ "\\begin{definition}\\label{bridge}"
                , "  $z$ is a bridge from $A$ to $B$ iff $z = z$ and $A = A$ and $B = B$."
                , "\\end{definition}"
                , "\\begin{signature}\\label{bridge_signature}"
                , "  $\\foo{A}$ is a bridge from every set $x$ to $x$."
                , "\\end{signature}"
                ])
        graph <- buildSearchedGraph temp "entry.tex"
        workspace <- expectRight
            =<< Parse.parseResolvedSourceGraph graph
        case Meaning.meaning
                (Parse.importedBeforeImporterBlocks workspace) of
            Left (Meaning.QuantifiedTermRequiresResolvedContext location) -> do
                assertEqual "quantified term file"
                    "entry.tex"
                    (locFile location)
                assertEqual "quantified term line"
                    5
                    (locLine location)
                assertEqual "quantified term column"
                    30
                    (locColumn location)
            Left err ->
                assertFailure
                    ("expected quantified-term context error, got "
                        <> show err)
            Right blocks ->
                assertFailure
                    ("expected quantified-term context rejection, got "
                        <> show blocks)

rejectsMalformedSignatureHead :: Assertion
rejectsMalformedSignatureHead = do
    case runLexer
        (FileId 49)
        "malformed-signature.tex"
        (Text.unlines
            [ "\\begin{signature}\\label{bad_signature}"
            , "  $x$ can be."
            , "\\end{signature}"
            ]) of
        Left err ->
            assertFailure ("unexpected token error: " <> show err)
        Right (_imports, [chunk]) ->
            case Adapt.scanChunk chunk of
                Left
                    (Adapt.InvalidFunctionPattern
                        location
                        Adapt.FunctionPatternBareVariable) -> do
                            assertEqual "error line" 1 (locLine location)
                            assertEqual "error column" 1 (locColumn location)
                Left err ->
                    assertFailure
                        ("expected malformed signature error, got " <> show err)
                Right scans ->
                    assertFailure
                        ("expected malformed signature rejection, got "
                            <> show scans)
        Right (_imports, chunks) ->
            assertFailure
                ("expected one malformed signature chunk, got "
                    <> show (length chunks))

reportsSameSourceLexiconCollision :: Assertion
reportsSameSourceLexiconCollision =
    withTemporaryDirectory "felix-source-local-lexicon-collision" \temp -> do
        writeFile
            (temp Posix.</> "entry.tex")
            (unlines
                [ "\\begin{struct}\\label{duplicate_operations}"
                , "  A \\duplicateop $X$ is equipped with"
                , "  \\begin{enumerate}"
                , "    \\item $\\duplicateop$"
                , "  \\end{enumerate}"
                , "\\end{struct}"
                ])
        graph <- buildSearchedGraph temp "entry.tex"
        collision <- expectLexiconCollision
            =<< Parse.parseResolvedSourceGraph graph
        (firstLocation, secondLocation) <-
            expectTwoCollisionLocations collision
        assertEqual "first declaration file"
            "entry.tex"
            (locFile firstLocation)
        assertEqual "first declaration line" 1 (locLine firstLocation)
        assertEqual "colliding declaration file"
            "entry.tex"
            (locFile secondLocation)
        assertEqual "colliding declaration line" 4 (locLine secondLocation)
        assertBool "declarations have distinct locations"
            (firstLocation /= secondLocation)

acceptsBuiltinSourceDeclaration :: Assertion
acceptsBuiltinSourceDeclaration =
    withTemporaryDirectory "felix-source-builtin-declaration" \temp -> do
        writeBuiltinZeroDefinition
            (temp Posix.</> "entry.tex")
            "source_zero"
        graph <- buildSearchedGraph temp "entry.tex"
        workspace <- expectRight
            =<< Parse.parseResolvedSourceGraph graph
        let root =
                Parse.parsedWorkspaceRootModule workspace
        assertEqual
            "fixed reuse emits no local syntax"
            []
            (Interface.canonicalSyntaxDeltaEntries
                (Interface.moduleSyntaxLocalDelta
                    (Parse.parsedModuleSyntaxInterface root)))
        case Parse.parsedModuleBlocks root of
            [Raw.BlockAbbr
                    _location
                    _title
                    blockMarker
                    (Raw.AbbreviationEq
                        (Raw.SymbolPattern
                            (Raw.MixfixItem
                                _pattern
                                symbolMarker
                                _associativity)
                            [])
                        _expression)] -> do
                assertEqual
                    "declaration label remains independent"
                    "source_zero"
                    blockMarker
                assertEqual
                    "built-in marker remains authoritative"
                    "zero"
                    symbolMarker
                case Parse.parsedModuleSyntaxOccurrences root of
                    [occurrence] ->
                        case Parse.parsedSyntaxOccurrenceEntry occurrence of
                            Interface.CanonicalExpressionFunction
                                    _pattern
                                    occurrenceMarker
                                    _fixity -> do
                                        assertEqual
                                            "occurrence retains source marker"
                                            "source_zero"
                                            (Parse.parsedSyntaxOccurrenceMarker
                                                occurrence)
                                        assertEqual
                                            "occurrence uses fixed marker"
                                            "zero"
                                            occurrenceMarker
                                        fileId <- expectJust
                                            "fixed occurrence file id"
                                            (locFileId
                                                (Parse.parsedSyntaxOccurrenceLocation
                                                    occurrence))
                                        decoded <- expectRight
                                            (Parsed.decodeCanonicalParsedPayload
                                                fileId
                                                (Parse.parsedModulePayload root))
                                        case Parsed.decodedParsedOccurrences decoded of
                                            [ ( _blockIndex
                                              , _location
                                              , storedMarker
                                              , Interface.CanonicalExpressionFunction
                                                    _storedPattern
                                                    storedEntryMarker
                                                    _storedFixity
                                              )
                                              ] -> do
                                                    assertEqual
                                                        "payload source marker"
                                                        "source_zero"
                                                        storedMarker
                                                    assertEqual
                                                        "payload authoritative marker"
                                                        "zero"
                                                        storedEntryMarker
                                            stored ->
                                                assertFailure
                                                    ("unexpected decoded fixed occurrence: "
                                                        <> show stored)
                            entry ->
                                assertFailure
                                    ("unexpected fixed occurrence: "
                                        <> show entry)
                    occurrences ->
                        assertFailure
                            ("unexpected fixed occurrences: "
                                <> show occurrences)
            blocks ->
                assertFailure
                    ("unexpected built-in declaration parse: "
                        <> show blocks)

acceptsBuiltinPrefixPredicateDeclaration :: Assertion
acceptsBuiltinPrefixPredicateDeclaration =
    withTemporaryDirectory "felix-source-builtin-prefix" \temp -> do
        writeBuiltinCongDefinition
            (temp Posix.</> "entry.tex")
        graph <- buildSearchedGraph temp "entry.tex"
        workspace <- expectRight
            =<< Parse.parseResolvedSourceGraph graph
        case Parse.parsedModuleBlocks
            (Parse.parsedWorkspaceRootModule workspace) of
                [Raw.BlockDefn
                    _location
                    _title
                    _blockMarker
                    (Raw.Defn
                        _assumptions
                        (Raw.DefnSymbolicPredicate
                            predicate
                            predicateMarker
                            _variables)
                        _statement)] -> do
                            assertEqual "built-in prefix predicate"
                                (Raw.PrefixPredicate "Cong" 4)
                                predicate
                            assertEqual
                                "built-in prefix marker remains authoritative"
                                "cong"
                                predicateMarker
                blocks ->
                    assertFailure
                        ("unexpected built-in prefix declaration parse: "
                            <> show blocks)

rejectsDuplicateFixedBaseSemantics :: Assertion
rejectsDuplicateFixedBaseSemantics =
    withTemporaryDirectory "felix-source-builtin-collision" \temp -> do
        writeBuiltinZeroDefinition
            (temp Posix.</> "a.tex")
            "source_zero_a"
        writeFile
            (temp Posix.</> "entry.tex")
            ("\\import{a.tex}\n"
                <> builtinZeroDefinition "source_zero_b")
        graph <- buildSearchedGraph temp "entry.tex"
        workspace <- expectRight
            =<< Parse.parseResolvedSourceGraph graph
        assignments <-
            expectRight
                (Legacy.assignLegacyModuleOrdinals workspace)
        case toList assignments of
            [acceptedAssignment, collidingAssignment] -> do
                let acceptedParsed =
                        Legacy.assignedParsedModule acceptedAssignment
                    collidingParsed =
                        Legacy.assignedParsedModule collidingAssignment
                acceptedLocation <-
                    onlySyntaxOccurrenceLocation acceptedParsed
                collidingLocation <-
                    onlySyntaxOccurrenceLocation collidingParsed
                assertLocation
                    "accepted declaration"
                    "a.tex"
                    1
                    acceptedLocation
                assertLocation
                    "colliding declaration"
                    "entry.tex"
                    2
                    collidingLocation
                assertEqual
                    "fixed reuses emit no syntax delta"
                    [[], []]
                    [ Interface.canonicalSyntaxDeltaEntries
                        (Interface.moduleSyntaxLocalDelta
                            (Parse.parsedModuleSyntaxInterface parsed))
                    | parsed <- [acceptedParsed, collidingParsed]
                    ]

                checkedFoundationValue <-
                    expectRight Foundation.checkedFoundation
                (acceptedBlocks, glossState) <-
                    glossParsedBlocks
                        Meaning.initialGlossState
                        acceptedParsed
                acceptedBuilder <-
                    expectRight
                        (Transition.openTransitionModuleBuilder
                            checkedFoundationValue
                            Checking.initialLegacyCheckingEnvironment
                            acceptedAssignment
                            [])
                acceptedState <-
                    Checking.runCheckingBlocks
                        acceptedBlocks
                        (checkingState acceptedBuilder)
                finalAcceptedBuilder <-
                    expectJust
                        "accepted transition builder"
                        (Checking.checkingTransitionModuleBuilder
                            acceptedState)
                acceptedModule <-
                    expectRight
                        (Transition.sealTransitionModule
                            (Checking.checkingStateEnvironment
                                acceptedState)
                            finalAcceptedBuilder)

                (collidingBlocks, _finalGlossState) <-
                    glossParsedBlocks glossState collidingParsed
                collidingBuilder <-
                    expectRight
                        (Transition.openTransitionModuleBuilder
                            checkedFoundationValue
                            Checking.initialLegacyCheckingEnvironment
                            collidingAssignment
                            [acceptedModule])
                result <-
                    try
                        (Checking.runCheckingBlocks
                            collidingBlocks
                            (checkingState collidingBuilder))
                        :: IO
                            (Either
                                Checking.CheckingError
                                Checking.CheckingState)
                case result of
                    Left
                        (Checking.CheckingError
                            message
                            location
                            marker) -> do
                                assertEqual
                                    "semantic collision location"
                                    collidingLocation
                                    location
                                assertEqual
                                    "semantic collision marker"
                                    "source_zero_b"
                                    marker
                                assertBool
                                    "accepted owner is identified"
                                    ("already owned by abbreviation source_zero_a"
                                        `Text.isInfixOf` message)
                    Left err ->
                        assertFailure
                            ("expected located ownership collision, got "
                                <> show err)
                    Right _checked ->
                        assertFailure
                            "duplicate fixed-base semantics were accepted"
            actual ->
                assertFailure
                    ("expected two module assignments, got "
                        <> show (length actual))
  where
    checkingState builder =
        Checking.initialTransitionCheckingStateWithTaskPreparation
            Checking.WithoutDumpPremselTraining
            id
            builder
            (\_batch ->
                assertFailure
                    "fixed-base abbreviation emitted an obligation")

    glossParsedBlocks initialState parsed =
        fmap
            (\(reversed, finalState) ->
                (reverse reversed, finalState))
            (foldM
                glossOne
                ([], initialState)
                (Parse.parsedModuleBlocks parsed))

    glossOne (reversed, state) raw = do
        (block, nextState) <-
            expectRight (Meaning.glossStep state raw)
        pure (block : reversed, nextState)

    onlySyntaxOccurrenceLocation parsed =
        case Parse.parsedModuleSyntaxOccurrences parsed of
            [occurrence] ->
                pure
                    (Parse.parsedSyntaxOccurrenceLocation
                        occurrence)
            occurrences ->
                assertFailure
                    ("expected one fixed-base occurrence, got "
                        <> show occurrences)

avoidsAliasImportLexiconCollision :: Assertion
avoidsAliasImportLexiconCollision =
    withTemporaryDirectory "felix-source-alias-lexicon" \temp -> do
        let shared = temp Posix.</> "shared.tex"
            alias = temp Posix.</> "alias.tex"
        writeAdjectiveDefinition shared "shared_special"
        Directory.createFileLink shared alias
        writeFile
            (temp Posix.</> "entry.tex")
            (unlines
                [ "\\import{shared.tex}"
                , "\\import{shared.tex}"
                , "\\import{alias.tex}"
                , "\\begin{axiom}\\label{root}"
                , "  $x$ is special."
                , "\\end{axiom}"
                ])
        graph <- buildSearchedGraph temp "entry.tex"
        workspace <- expectRight
            =<< Parse.parseResolvedSourceGraph graph
        assertEqual "canonical source is parsed once"
            ["shared.tex", "entry.tex"]
            (toList
                ( safeRelativePathFilePath
                    . resolvedSourceRelativePath
                    . Parse.parsedModuleResolved
                    <$> Parse.parsedWorkspaceImportedBeforeImporter workspace
                ))

parsesWithoutRereading :: Assertion
parsesWithoutRereading =
    withTemporaryDirectory "felix-source-no-reread" \temp -> do
        let shared = temp Posix.</> "shared.tex"
            entry = temp Posix.</> "entry.tex"
        writeTheory shared [] "shared"
        writeTheory entry ["shared.tex"] "entry"
        graph <- buildSearchedGraph temp "entry.tex"
        Directory.removeFile entry
        Directory.removeFile shared
        firstWorkspace <- expectRight =<< Parse.parseResolvedSourceGraph graph
        secondWorkspace <- expectRight =<< Parse.parseResolvedSourceGraph graph
        assertEqual "first flat projection" 2
            (length (Parse.importedBeforeImporterBlocks firstWorkspace))
        assertEqual "repeated downstream projection" 2
            (length (Parse.importedBeforeImporterBlocks secondWorkspace))

returnsSourceParseFailures :: Assertion
returnsSourceParseFailures =
    withTemporaryDirectory "felix-source-parse-error" \temp -> do
        writeFile
            (temp Posix.</> "entry.tex")
            (theoryBlock "accepted"
                <> "\\begin{axiom}\\label{late_failure}\n")
        graph <- buildSearchedGraph temp "entry.tex"
        emittedRef <- newIORef []
        result <-
            Parse.parseResolvedSourceGraphWith graph
                (\_source block ->
                    case block of
                        Raw.BlockAxiom _location _title marker _axiom ->
                            modifyIORef' emittedRef (marker :)
                        _ ->
                            assertFailure
                                ("unexpected emitted block: " <> show block))
        case result of
            Left (Parse.SourceParseError source _err) -> do
                assertEqual "failed source" "entry.tex"
                    (safeRelativePathFilePath
                        (resolvedSourceRelativePath source))
                emitted <- reverse <$> readIORef emittedRef
                assertEqual "completed callbacks before later failure"
                    ["accepted"]
                    emitted
            Left err ->
                assertFailure ("expected SourceParseError, got " <> show err)
            Right workspace ->
                assertFailure ("expected parse failure, got " <> show workspace)

buildSearchedGraph :: FilePath -> FilePath -> IO ResolvedSourceGraph
buildSearchedGraph root path = do
    mounts <- oneMount "project" root
    request <- expectRight (searchedRoot path)
    expectRight =<< buildResolvedSourceGraph mounts request

sourceGraphOrderPaths :: ResolvedSourceGraph -> IO [FilePath]
sourceGraphOrderPaths graph =
    pure
        [ safeRelativePathFilePath
            (resolvedSourceRelativePath (sourceNodeResolved node))
        | node <- toList (sourceGraphImportedBeforeImporter graph)
        ]

sourceNodeCanonicalPathForTest :: SourceNode -> CanonicalPath
sourceNodeCanonicalPathForTest =
    resolvedSourceCanonicalPath . sourceNodeResolved

onlyAxiomLocation :: Parse.ParsedModule -> Location
onlyAxiomLocation node =
    case Parse.parsedModuleBlocks node of
        [Raw.BlockAxiom location _title _marker _axiom] ->
            location
        blocks ->
            error ("expected one axiom block, got " <> show blocks)

syntaxFunctionDefinition
    :: String
    -> String
    -> Maybe String
    -> String
syntaxFunctionDefinition marker command pragma =
    unlines
        ( [ "\\begin{abbreviation}\\label{" <> marker <> "}"
          ]
          <> maybe [] (\line -> ["  " <> line]) pragma
          <> [ "  $x\\" <> command <> " y = x$."
             , "\\end{abbreviation}"
             ]
        )

axiomBlock :: String -> String -> String
axiomBlock marker statement =
    unlines
        [ "\\begin{axiom}\\label{" <> marker <> "}"
        , "  $" <> statement <> "$."
        , "\\end{axiom}"
        ]

assertExpressionFixity
    :: Text
    -> Raw.Associativity
    -> Word8
    -> [Interface.CanonicalLexicalEntry]
    -> Assertion
assertExpressionFixity marker associativity level entries =
    case
        [ fixity
        | Interface.CanonicalExpressionFunction
                _pattern
                (Raw.Marker candidate)
                fixity <-
            entries
        , candidate == marker
        ] of
        [Interface.Fixity actualAssociativity actualLevel] -> do
            assertEqual
                (Text.unpack marker <> " associativity")
                associativity
                actualAssociativity
            assertEqual
                (Text.unpack marker <> " level")
                level
                (Interface.mixfixLevelValue actualLevel)
        actual ->
            assertFailure
                ("expected one fixity for "
                    <> Text.unpack marker
                    <> ", got "
                    <> show actual)

assertAxiomLeftShape
    :: String
    -> String
    -> Raw.Block
    -> Assertion
assertAxiomLeftShape description expected block =
    case block of
        Raw.BlockAxiom
            _location
            _title
            _marker
            (Raw.Axiom
                _assumptions
                (Raw.StmtFormula
                    (Raw.FormulaChain
                        (Raw.ChainBase
                            (expression :| [])
                            _sign
                            _relation
                            _right)))) ->
                                assertEqual
                                    description
                                    expected
                                    (expressionShape expression)
        _ ->
            assertFailure
                ("expected an axiom with one left expression, got "
                    <> show block)

expressionShape :: Raw.Expr -> String
expressionShape = \case
    Raw.ExprVar (Raw.NamedVarAt _location name) ->
        Text.unpack name
    Raw.ExprOp
            _location
            symbol
            arguments ->
        let Raw.Marker marker =
                Raw.mixfixMarker symbol
        in
            Text.unpack marker
                <> "("
                <> List.intercalate ","
                    (expressionShape <$> arguments)
                <> ")"
    expression ->
        show expression

findParsedModule
    :: FilePath
    -> Parse.ParsedSourceWorkspace
    -> IO Parse.ParsedModule
findParsedModule relative workspace =
    case List.find hasPath
            (Parse.parsedWorkspaceModules workspace) of
        Just parsed ->
            pure parsed
        Nothing ->
            assertFailure
                ("could not find parsed module " <> relative)
  where
    hasPath parsed =
        safeRelativePathFilePath
            (resolvedSourceRelativePath
                (Parse.parsedModuleResolved parsed))
            == relative

writeAdjectiveDefinition :: FilePath -> String -> IO ()
writeAdjectiveDefinition path marker =
    writeFile path (adjectiveDefinition marker)

adjectiveDefinition :: String -> String
adjectiveDefinition marker =
    unlines
        [ "\\begin{definition}\\label{" <> marker <> "}"
        , "  $x$ is special iff $x = x$."
        , "\\end{definition}"
        ]

writeNounDefinition :: FilePath -> String -> IO ()
writeNounDefinition path marker =
    writeFile path
        (unlines
            [ "\\begin{definition}\\label{" <> marker <> "}"
            , "  $x$ is a special iff $x = x$."
            , "\\end{definition}"
            ])

writeBuiltinZeroDefinition :: FilePath -> String -> IO ()
writeBuiltinZeroDefinition path marker =
    writeFile path (builtinZeroDefinition marker)

builtinZeroDefinition :: String -> String
builtinZeroDefinition marker =
    unlines
        [ "\\begin{abbreviation}\\label{" <> marker <> "}"
        , "  $\\zero = \\emptyset$."
        , "\\end{abbreviation}"
        ]

writeBuiltinCongDefinition :: FilePath -> IO ()
writeBuiltinCongDefinition path =
    writeFile path
        (unlines
            [ "\\begin{definition}\\label{source_cong}"
            , "  $\\Cong{x}{y}{z}{w}$ iff $x = x$."
            , "\\end{definition}"
            ])

writeTheory :: FilePath -> [FilePath] -> String -> IO ()
writeTheory path imports label =
    writeFile path
        (unlines
            (["\\import{" <> imported <> "}" | imported <- imports]
                <> [theoryBlock label]))

theoryBlock :: String -> String
theoryBlock label =
    unlines
        [ "\\begin{axiom}\\label{" <> label <> "}"
        , "  $x = x$."
        , "\\end{axiom}"
        ]

oneMount :: Text -> FilePath -> IO SourceMounts
oneMount ident root =
    expectRight =<< prepareSourceMounts [(sourceMountId ident, root)]

withTemporaryDirectory :: String -> (FilePath -> IO a) -> IO a
withTemporaryDirectory template =
    bracket create Directory.removePathForcibly
  where
    create = do
        systemTemp <- Directory.getTemporaryDirectory
        (path, handle) <- openTempFile systemTemp template
        hClose handle
        Directory.removeFile path
        Directory.createDirectory path
        pure path

assertRight :: (Show e, HasCallStack) => Either e a -> Assertion
assertRight = void . expectRight

expectRight :: (Show e, HasCallStack) => Either e a -> IO a
expectRight = \case
    Left err ->
        assertFailure ("expected Right, got Left " <> show err)
    Right value ->
        pure value

expectJust :: HasCallStack => String -> Maybe a -> IO a
expectJust description = \case
    Nothing ->
        assertFailure ("expected " <> description)
    Just value ->
        pure value

expectLexiconCollision
    :: Either Parse.ParseWorkspaceError a
    -> IO Parse.LexiconCollision
expectLexiconCollision = \case
    Left (Parse.SourceLexiconCollision collision) ->
        pure collision
    Left err ->
        assertFailure
            ("expected SourceLexiconCollision, got " <> show err)
    Right _value ->
        assertFailure "expected SourceLexiconCollision, got Right"

expectTwoCollisionLocations
    :: Parse.LexiconCollision
    -> IO (Location, Location)
expectTwoCollisionLocations collision =
    case Parse.lexiconCollisionDeclarations collision of
        firstLocation : secondLocation : _ ->
            pure (firstLocation, secondLocation)
        locations ->
            assertFailure
                ("expected two source collision locations, got "
                    <> show locations)

assertLocation :: String -> FilePath -> Int -> Location -> Assertion
assertLocation description expectedFile expectedLine location = do
    assertEqual (description <> " file")
        expectedFile
        (locFile location)
    assertEqual (description <> " line")
        expectedLine
        (locLine location)
    assertEqual (description <> " column")
        1
        (locColumn location)

substringIndex :: String -> String -> Int
substringIndex needle haystack =
    fromMaybe maxBound
        (List.findIndex
            (List.isPrefixOf needle)
            (List.tails haystack))

assertLeft :: (Eq e, Eq a, Show e, Show a, HasCallStack) => e -> Either e a -> Assertion
assertLeft expected actual =
    assertEqual "expected Left value" (Left expected) actual