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

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

module Test.Unit.Source (unitTests) where

import Base
import Checking.Foundation qualified as Foundation
import Checking.Identity qualified as Identity
import Checking.Semantic qualified as Semantic
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.Prelude qualified as Prelude
import Felix.Source
import Felix.Source.Content qualified as Content
import Felix.Source.Graph
import Felix.Store qualified as Store
import Report.Location
    ( FileId(..)
    , FileIdAllocator(..)
    , Location(..)
    , LocationRegistrationError(..)
    , 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.Token (runLexer)

import Control.Exception (bracket, evaluate)
import Data.ByteString qualified as ByteString
import Data.IORef
import Data.List qualified as List
import Data.List.NonEmpty qualified as NonEmpty
import Data.Text qualified as Text
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 "rejects the packaged prelude as ordinary source"
        rejectsPackagedPreludeAsOrdinarySource
    , 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 "invalidates exact parsed inputs transitively"
        invalidatesExactParsedInputs
    , testCase "rebinds relocated parsed artifacts"
        rebindsRelocatedParsedArtifacts
    , testCase "rejects a corrupted cached declaration anchor"
        rejectsCorruptedCachedDeclarationAnchor
    , testCase "parses source-local blocks in graph order" parsesSourceGraph
    , 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 scanner errors before importer tokenizer errors"
        reportsImportedScannerErrorFirst
    , testCase "returns malformed lexical declarations as typed errors"
        reportsMalformedLexicalDeclaration
    , testCase "validates inductive function patterns during scanning"
        rejectsMalformedInductivePattern
    , testCase "scans and parses adjective signatures"
        acceptsAdjectiveSignature
    , 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 "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))

rejectsPackagedPreludeAsOrdinarySource :: Assertion
rejectsPackagedPreludeAsOrdinarySource = do
    packaged <- expectRight =<< Prelude.loadReservedPreludeSourceInput
    canonical <- expectJust "packaged canonical path"
        (Prelude.reservedPreludeSourceCanonicalPath packaged)
    let path = canonicalPathFilePath canonical
    mounts <- oneMount "packaged" (Posix.takeDirectory path)
    request <- expectRight (searchedRoot (Posix.takeFileName path))
    let validate = Prelude.rejectOrdinaryPreludeSourceGraph packaged
        syntaxInputs = const []
    Parse.parseSourceWorkspaceMeasuredWithSyntaxInputsAndGraphValidation
        mounts request syntaxInputs validate >>= \case
            Left
                (Parse.SourceWorkspaceError
                    (PackagedPreludeSelectedAsOrdinarySource source)) ->
                        assertEqual "authority-free rejected path"
                            canonical
                            (resolvedSourceCanonicalPath source)
            other ->
                assertFailure
                    ("unexpected authority-free result: " <> show other)

    withTemporaryDirectory "felix-reserved-parse-store" \temp -> do
        foundation <- expectRight Foundation.checkedFoundation
        store <- openTestStore
            (temp Posix.</> "store.sqlite")
            (Identity.theoryId foundation)
        Parse.parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndGraphValidation
            store mounts request syntaxInputs validate >>= \case
                Left
                    (Parse.ParseExecutionWorkspaceError
                        (Parse.SourceWorkspaceError
                            (PackagedPreludeSelectedAsOrdinarySource source))) ->
                                assertEqual "typed rejected path"
                                    canonical
                                    (resolvedSourceCanonicalPath source)
                other ->
                    assertFailure
                        ("unexpected typed result: " <> show other)
        Store.closeStore store

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)))))

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)
        let expectedChunkCount =
                length (Parse.parsedModuleBlocks warmRoot)
        assertBool "fixture has source chunks" (expectedChunkCount > 0)
        assertEqual "cold structural chunks" expectedChunkCount
            (Parse.parseMeasurementChunkCount coldMeasurements)
        assertEqual "warm structural chunks" expectedChunkCount
            (Parse.parseMeasurementChunkCount 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

invalidatesExactParsedInputs :: Assertion
invalidatesExactParsedInputs =
    withTemporaryDirectory "felix-parsed-invalidation" \temp -> do
        let notationPath = temp Posix.</> "notation.tex"
            entryPath = temp Posix.</> "entry.tex"
            notation associativity level =
                syntaxFunctionDefinition
                    "join"
                    "join"
                    (Just
                        ("%! " <> associativity <> " " <> show level))
            entry suffix =
                "\\import{notation.tex}\n"
                    <> axiomBlock
                        "imported_syntax_use"
                        "a\\join b\\join c = a"
                    <> suffix
        writeFile notationPath (notation "infixl" (1 :: Int))
        writeFile entryPath (entry "")
        mounts <- oneMount "project" temp
        request <- expectRight (searchedRoot "entry.tex")
        foundation <- expectRight Foundation.checkedFoundation
        store <- openTestStore
            (temp Posix.</> "store.sqlite")
            (Identity.theoryId foundation)
        let parse =
                expectParseExecution
                    =<< Parse.parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputs
                        store mounts request (const [])
        (coldWorkspace, coldMeasurements) <- parse
        (warmWorkspace, warmMeasurements) <- parse
        assertEqual "cold graph misses" 2
            (Parse.parseMeasurementParsedMissCount coldMeasurements)
        assertEqual "unchanged graph hits" 2
            (Parse.parseMeasurementParsedHitCount warmMeasurements)
        assertEqual "unchanged graph builds no parser table" 0
            (Parse.parseMeasurementParserTableMaterializationCount
                warmMeasurements)
        coldNotation <- findParsedModule "notation.tex" coldWorkspace
        warmNotation <- findParsedModule "notation.tex" warmWorkspace
        let coldRoot = Parse.parsedWorkspaceRootModule coldWorkspace
            warmRoot = Parse.parsedWorkspaceRootModule warmWorkspace
        assertEqual "unchanged import identity"
            (Parse.parsedModuleId coldNotation)
            (Parse.parsedModuleId warmNotation)
        assertEqual "unchanged importer identity"
            (Parse.parsedModuleId coldRoot)
            (Parse.parsedModuleId warmRoot)

        writeFile entryPath (entry "% formatting-only edit\n")
        (editedWorkspace, editedMeasurements) <- parse
        editedNotation <- findParsedModule "notation.tex" editedWorkspace
        let editedRoot = Parse.parsedWorkspaceRootModule editedWorkspace
        assertEqual "unchanged import hits" 1
            (Parse.parseMeasurementParsedHitCount editedMeasurements)
        assertEqual "edited importer misses" 1
            (Parse.parseMeasurementParsedMissCount editedMeasurements)
        assertEqual "edited importer builds one parser table" 1
            (Parse.parseMeasurementParserTableMaterializationCount
                editedMeasurements)
        assertEqual "cached import retains identity"
            (Parse.parsedModuleId warmNotation)
            (Parse.parsedModuleId editedNotation)
        assertBool "exact source edit changes importer key"
            (Parse.parsedModuleKey warmRoot
                /= Parse.parsedModuleKey editedRoot)
        assertEqual "formatting retains parsed projection"
            (Parse.parsedModulePayload warmRoot)
            (Parse.parsedModulePayload editedRoot)

        writeFile notationPath (notation "infixr" (2 :: Int))
        (syntaxWorkspace, syntaxMeasurements) <- parse
        syntaxNotation <- findParsedModule "notation.tex" syntaxWorkspace
        let syntaxRoot = Parse.parsedWorkspaceRootModule syntaxWorkspace
        assertEqual "syntax edit invalidates both modules" 0
            (Parse.parseMeasurementParsedHitCount syntaxMeasurements)
        assertEqual "syntax edit reparses both modules" 2
            (Parse.parseMeasurementParsedMissCount syntaxMeasurements)
        assertEqual "syntax edit builds both parser tables" 2
            (Parse.parseMeasurementParserTableMaterializationCount
                syntaxMeasurements)
        assertBool "local syntax identity changes"
            ( Interface.moduleSyntaxAssertedId
                (Parse.parsedModuleSyntaxInterface editedNotation)
                /= Interface.moduleSyntaxAssertedId
                    (Parse.parsedModuleSyntaxInterface syntaxNotation)
            )
        assertEqual "importer source is unchanged"
            (Parse.parsedModuleSourceContentId editedRoot)
            (Parse.parsedModuleSourceContentId syntaxRoot)
        assertBool "direct syntax invalidates importer key"
            (Parse.parsedModuleKey editedRoot
                /= Parse.parsedModuleKey syntaxRoot)
        Store.closeStore store

rebindsRelocatedParsedArtifacts :: Assertion
rebindsRelocatedParsedArtifacts =
    withTemporaryDirectory "felix-parsed-relocation" \temp -> do
        let firstRoot = temp Posix.</> "first"
            secondRoot = temp Posix.</> "second"
            sourceBytes = axiomBlock "same" "x = x"
        Directory.createDirectory firstRoot
        Directory.createDirectory secondRoot
        writeFile (firstRoot Posix.</> "entry.tex") sourceBytes
        writeFile (secondRoot Posix.</> "entry.tex") sourceBytes
        firstMounts <- oneMount "first" firstRoot
        secondMounts <- oneMount "second" secondRoot
        request <- expectRight (searchedRoot "entry.tex")
        foundation <- expectRight Foundation.checkedFoundation
        let theory = Identity.theoryId foundation
        store <- openTestStore (temp Posix.</> "store.sqlite") theory
        (firstWorkspace, firstMeasurements) <- expectParseExecution
            =<< Parse.parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputs
                store firstMounts request (const [])
        (secondWorkspace, secondMeasurements) <- expectParseExecution
            =<< Parse.parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputs
                store secondMounts request (const [])
        let first = Parse.parsedWorkspaceRootModule firstWorkspace
            second = Parse.parsedWorkspaceRootModule secondWorkspace
            firstSource = Parse.parsedModuleResolved first
            secondSource = Parse.parsedModuleResolved second
        assertEqual "first owner misses" 1
            (Parse.parseMeasurementParsedMissCount firstMeasurements)
        assertEqual "relocated owner hits" 1
            (Parse.parseMeasurementParsedHitCount secondMeasurements)
        assertEqual "relocated owner builds no parser table" 0
            (Parse.parseMeasurementParserTableMaterializationCount
                secondMeasurements)
        assertEqual "relocation retains parsed identity"
            (Parse.parsedModuleId first)
            (Parse.parsedModuleId second)
        assertEqual "relocation retains canonical payload"
            (Parse.parsedModulePayload first)
            (Parse.parsedModulePayload second)
        assertBool "relocation rebinds the physical source"
            (resolvedSourceCanonicalPath firstSource
                /= resolvedSourceCanonicalPath secondSource)
        assertBool "relocation rebinds the logical owner"
            (Parse.parsedModuleAddress first
                /= Parse.parsedModuleAddress second)
        firstFileId <- expectJust "first location file id"
            (locFileId (onlyAxiomLocation first))
        secondFileId <- expectJust "second location file id"
            (locFileId (onlyAxiomLocation second))
        assertBool "relocation rebinds locations"
            (firstFileId /= secondFileId)
        firstArtifactKey <- expectRight
            (Semantic.moduleArtifactKey
                (Module.moduleName (Parse.parsedModuleAddress first))
                (Parse.parsedModuleId first)
                []
                theory)
        secondArtifactKey <- expectRight
            (Semantic.moduleArtifactKey
                (Module.moduleName (Parse.parsedModuleAddress second))
                (Parse.parsedModuleId second)
                []
                theory)
        assertBool "module artifact remains owner-dependent"
            (Semantic.moduleArtifactId firstArtifactKey
                /= Semantic.moduleArtifactId secondArtifactKey)
        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

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)

reportsImportedScannerErrorFirst :: Assertion
reportsImportedScannerErrorFirst =
    withTemporaryDirectory "felix-source-lexer-error-order" \temp -> do
        let scannerFailure = unlines
                [ "\\begin{abbreviation}\\label{malformed_function}"
                , "  $x = \\emptyset$."
                , "\\end{abbreviation}"
                ]
            tokenizerFailure = unlines
                [ "\\begin{axiom}"
                , "#"
                , "\\end{axiom}"
                ]
        writeFile
            (temp Posix.</> "imported.tex")
            scannerFailure
        writeFile
            (temp Posix.</> "entry.tex")
            ("\\import{imported.tex}\n" <> tokenizerFailure)
        graph <- buildSearchedGraph temp "entry.tex"
        result <- Parse.parseResolvedSourceGraph graph
        case result of
            Left
                (Parse.SourceParseError
                    source
                    (Parse.LexicalScanFailure
                        Adapt.InvalidFunctionPattern{})) ->
                            assertEqual
                                "dependency scanner error"
                                "imported.tex"
                                (safeRelativePathFilePath
                                    (resolvedSourceRelativePath source))
            Left err ->
                assertFailure
                    ("expected imported scanner error, got " <> show err)
            Right workspace ->
                assertFailure
                    ("expected imported scanner 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)

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)

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