{-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternSynonyms #-} module Felix.Test.Unit.Source (unitTests) where import Base import Felix.Checking.Foundation qualified as Foundation import Felix.Checking.Identity qualified as Identity import Felix.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 Felix.Report.Location ( FileId(..) , FileIdAllocator(..) , Location(..) , LocationRegistrationError(..) , allocateFileId , locColumn , locFile , locFileId , locLine , lookupFileIdentityPath ) import Felix.Syntax.Abstract qualified as Raw import Felix.Syntax.Adapt qualified as Adapt import Felix.Syntax.Interface qualified as Interface import Felix.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 , testCase "rejects guarded symbolic declarations before publication" rejectsGuardedSymbolicDeclarations ] 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.parseSourceWorkspaceWithSyntaxInputsAndGraphValidation 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.parseSourceWorkspaceWithStoreAndSyntaxInputsAndGraphValidation 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.parseSourceWorkspaceWithStoreAndSyntaxInputsAndCallback store mounts request (const []) (\_source _block -> modifyIORef' coldCallbacks (+ 1)) warmCallbacks <- newIORef (0 :: Int) warm <- expectParseExecution =<< Parse.parseSourceWorkspaceWithStoreAndSyntaxInputsAndCallback store mounts request (const []) (\_source _block -> modifyIORef' warmCallbacks (+ 1)) let coldRoot = Parse.parsedWorkspaceRootModule cold warmRoot = Parse.parsedWorkspaceRootModule warm let expectedChunkCount = length (Parse.parsedModuleBlocks warmRoot) assertBool "fixture has source chunks" (expectedChunkCount > 0) assertEqual "cold callbacks" expectedChunkCount =<< readIORef coldCallbacks assertEqual "warm callbacks" expectedChunkCount =<< readIORef warmCallbacks 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.parseSourceWorkspaceWithStoreAndSyntaxInputs store mounts request (const []) coldWorkspace <- parse warmWorkspace <- parse 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 <- parse editedNotation <- findParsedModule "notation.tex" editedWorkspace let editedRoot = Parse.parsedWorkspaceRootModule editedWorkspace 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 <- parse syntaxNotation <- findParsedModule "notation.tex" syntaxWorkspace let syntaxRoot = Parse.parsedWorkspaceRootModule syntaxWorkspace 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 <- expectParseExecution =<< Parse.parseSourceWorkspaceWithStoreAndSyntaxInputs store firstMounts request (const []) secondWorkspace <- expectParseExecution =<< Parse.parseSourceWorkspaceWithStoreAndSyntaxInputs store secondMounts request (const []) let first = Parse.parsedWorkspaceRootModule firstWorkspace second = Parse.parsedWorkspaceRootModule secondWorkspace firstSource = Parse.parsedModuleResolved first secondSource = Parse.parsedModuleResolved second 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 <- expectParseExecution =<< Parse.parseSourceWorkspaceWithStoreAndSyntaxInputs 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.parseSourceWorkspaceWithStoreAndSyntaxInputsAndCallback 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) rejectsGuardedSymbolicDeclarations :: Assertion rejectsGuardedSymbolicDeclarations = for_ [("definition", 3 :: Int), ("abbreviation", 2)] \(kind, failureLine) -> withTemporaryDirectory ("felix-guarded-symbolic-" <> kind) \temp -> do let relative = "entry.tex" source = unlines [ "\\begin{" <> kind <> "}\\label{guarded_symbolic}" , " Suppose $\\top$." , " $\\guardedsymbolic{X} = X$." , "\\end{" <> kind <> "}" ] writeFile (temp Posix. relative) source graph <- buildSearchedGraph temp relative emittedRef <- newIORef ([] :: [Raw.Block]) result <- Parse.parseResolvedSourceGraphWith graph (\_source block -> modifyIORef' emittedRef (block :)) case result of Left (Parse.SourceParseError failed parseFailure) -> do assertEqual (kind <> " source") relative (safeRelativePathFilePath (resolvedSourceRelativePath failed)) assertBool (kind <> " parse failure retains a located source position: " <> show parseFailure) (("entry.tex " <> show failureLine <> ":") `List.isInfixOf` show parseFailure) assertEqual (kind <> " publishes no completed source block") [] =<< readIORef emittedRef Left failure -> assertFailure ("expected guarded-symbolic parse failure, got " <> show failure) Right workspace -> assertFailure ("guarded symbolic " <> kind <> " was silently accepted: " <> 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