diff options
Diffstat (limited to 'source/Test/Unit/Source.hs')
| -rw-r--r-- | source/Test/Unit/Source.hs | 2581 |
1 files changed, 0 insertions, 2581 deletions
diff --git a/source/Test/Unit/Source.hs b/source/Test/Unit/Source.hs deleted file mode 100644 index a8e4506..0000000 --- a/source/Test/Unit/Source.hs +++ /dev/null @@ -1,2581 +0,0 @@ -{-# 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 - , 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 |