diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2026-08-06 17:54:00 +0200 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2026-08-06 17:54:00 +0200 |
| commit | 82328890108bae64b372b8d58620ebc62699de76 (patch) | |
| tree | 575404c6b425c19259c0ded296f1c8ffb7ff0e2b /source/Felix/Test/Unit/Source.hs | |
| parent | 1a25421c2a168d420581358c8733fcd8f36f379b (diff) | |
Diffstat (limited to 'source/Felix/Test/Unit/Source.hs')
| -rw-r--r-- | source/Felix/Test/Unit/Source.hs | 2581 |
1 files changed, 2581 insertions, 0 deletions
diff --git a/source/Felix/Test/Unit/Source.hs b/source/Felix/Test/Unit/Source.hs new file mode 100644 index 0000000..6216381 --- /dev/null +++ b/source/Felix/Test/Unit/Source.hs @@ -0,0 +1,2581 @@ +{-# 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 |