Reuse exact parsed module artifacts

1 files changed, 206 insertions, 0 deletions

diff --git a/source/Test/Unit/Source.hs b/source/Test/Unit/Source.hs
index f2bdd22..862ff87 100644
--- a/source/Test/Unit/Source.hs
+++ b/source/Test/Unit/Source.hs
@@ -11,6 +11,7 @@ import Checking.Backend.Reconstruction qualified as Reconstruction
 import Checking.Core qualified as Core
 import Checking.Facts qualified as Facts
 import Checking.Foundation qualified as Foundation
+import Checking.Identity qualified as Identity
 import Checking.Kernel.Derivation qualified as Derivation
 import Checking.Legacy qualified as Legacy
 import Checking.Obligation qualified as Obligation
@@ -18,10 +19,12 @@ import Checking.Transition qualified as Transition
 import Felix.Cache.Codec qualified as Cache
 import Felix.Module qualified as Module
 import Felix.Parse qualified as Parse
+import Felix.Parsed.Identity qualified as ParsedIdentity
 import Felix.Parsed.Payload qualified as Parsed
 import Felix.Source
 import Felix.Source.Content qualified as Content
 import Felix.Source.Graph
+import Felix.Store qualified as Store
 import Meaning qualified
 import Provers qualified
 import Report.Location
@@ -56,6 +59,7 @@ import Data.Set qualified as Set
 import Data.Text qualified as Text
 import Data.Vector qualified as Vector
 import Data.Word (Word8, Word16)
+import Database.SQLite.Simple qualified as SQLite
 import System.Directory qualified as Directory
 import System.FilePath.Posix qualified as Posix
 import System.Posix.Files qualified as PosixFiles
@@ -100,6 +104,10 @@ unitTests = testGroup "Source resolution"
         identifiesOwnerIndependentParsedModules
     , testCase "keys effective direct syntax inputs"
         keysEffectiveDirectSyntaxInputs
+    , testCase "reuses exact parsed syntax on a warm pass"
+        reusesExactParsedSyntax
+    , testCase "rejects a corrupted cached declaration anchor"
+        rejectsCorruptedCachedDeclarationAnchor
     , testCase "parses source-local blocks in graph order" parsesSourceGraph
     , testCase "assigns and reserves dense legacy module positions"
         reservesLegacyModulePositions
@@ -820,6 +828,204 @@ keysEffectiveDirectSyntaxInputs =
             "effective syntax changes parsed identity"
             (Parse.parsedModuleId first /= Parse.parsedModuleId second)
 
+reusesExactParsedSyntax :: Assertion
+reusesExactParsedSyntax =
+    withTemporaryDirectory "felix-parsed-warm" \temp -> do
+        let datatype = unlines
+                [ "\\begin{datatype}\\label{multi_item}"
+                , "  Define $\\itemkind$ inductively as follows."
+                , "  \\begin{enumerate}"
+                , "    \\item $\\itemzero \\in \\itemkind$."
+                , "    \\item $\\itemsucc{x} \\in \\itemkind$ for $x \\in \\itemkind$."
+                , "  \\end{enumerate}"
+                , "\\end{datatype}"
+                ]
+        writeFile
+            (temp Posix.</> "entry.tex")
+            (builtinZeroDefinition "source_zero" <> datatype)
+        mounts <- oneMount "project" temp
+        request <- expectRight (searchedRoot "entry.tex")
+        foundation <- expectRight Foundation.checkedFoundation
+        store <- openTestStore
+            (temp Posix.</> "store.sqlite")
+            (Identity.theoryId foundation)
+        coldCallbacks <- newIORef (0 :: Int)
+        cold <- expectParseExecution
+            =<< Parse.parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndCallback
+                store mounts request (const [])
+                (\_source _block -> modifyIORef' coldCallbacks (+ 1))
+        warmCallbacks <- newIORef (0 :: Int)
+        warm <- expectParseExecution
+            =<< Parse.parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndCallback
+                store mounts request (const [])
+                (\_source _block -> modifyIORef' warmCallbacks (+ 1))
+        let coldRoot = Parse.parsedWorkspaceRootModule (fst cold)
+            warmRoot = Parse.parsedWorkspaceRootModule (fst warm)
+            coldMeasurements = snd cold
+            warmMeasurements = snd warm
+        assertEqual "cold parsed misses" 1
+            (Parse.parseMeasurementParsedMissCount coldMeasurements)
+        assertEqual "cold parser tables" 1
+            (Parse.parseMeasurementParserTableMaterializationCount
+                coldMeasurements)
+        assertEqual "warm parsed hits" 1
+            (Parse.parseMeasurementParsedHitCount warmMeasurements)
+        assertEqual "warm parsed misses" 0
+            (Parse.parseMeasurementParsedMissCount warmMeasurements)
+        assertEqual "warm tokenization" 0
+            (Parse.parseMeasurementTokenizationNanoseconds warmMeasurements)
+        assertEqual "warm scanning" 0
+            (Parse.parseMeasurementScanningNanoseconds warmMeasurements)
+        assertEqual "warm parsing" 0
+            (Parse.parseMeasurementParsingNanoseconds warmMeasurements)
+        assertEqual "warm parser tables" 0
+            (Parse.parseMeasurementParserTableMaterializationCount
+                warmMeasurements)
+        assertEqual "warm blocks" (Parse.parsedModuleBlocks coldRoot)
+            (Parse.parsedModuleBlocks warmRoot)
+        assertEqual "warm occurrences"
+            (Parse.parsedModuleSyntaxOccurrences coldRoot)
+            (Parse.parsedModuleSyntaxOccurrences warmRoot)
+        assertEqual "warm syntax interface"
+            (Parse.parsedModuleSyntaxInterface coldRoot)
+            (Parse.parsedModuleSyntaxInterface warmRoot)
+        assertEqual "warm parsed identity"
+            (Parse.parsedModuleId coldRoot)
+            (Parse.parsedModuleId warmRoot)
+        case Parse.parsedModuleSyntaxOccurrences warmRoot of
+            first : second : third : fourth : [] -> do
+                assertEqual "fixed source marker" "source_zero"
+                    (Parse.parsedSyntaxOccurrenceMarker first)
+                case Parse.parsedSyntaxOccurrenceEntry first of
+                    Interface.CanonicalExpressionFunction
+                            _pattern marker _fixity ->
+                        assertEqual "fixed authoritative marker" "zero" marker
+                    entry ->
+                        assertFailure
+                            ("unexpected fixed cached entry: " <> show entry)
+                assertEqual "multi-item block order" [1, 1, 1]
+                    (Parse.parsedSyntaxOccurrenceBlockIndex
+                        <$> [second, third, fourth])
+                assertEqual "multi-item scanner order"
+                    ["multi_item", "itemzero", "itemsucc"]
+                    (Parse.parsedSyntaxOccurrenceMarker
+                        <$> [second, third, fourth])
+                case drop 1 (Parse.parsedModuleBlocks warmRoot) of
+                    block : _ ->
+                        case block of
+                            Raw.BlockData _location _title marker _datatype ->
+                                assertEqual "cached declaration-head anchor"
+                                    marker
+                                    (Parse.parsedSyntaxOccurrenceMarker second)
+                            other ->
+                                assertFailure
+                                    ("expected cached datatype block, got "
+                                        <> show other)
+                    [] ->
+                        assertFailure "cached datatype block is absent"
+            occurrences ->
+                assertFailure
+                    ("unexpected cached syntax occurrences: "
+                        <> show occurrences)
+        assertEqual "cold callback projection" 2
+            =<< readIORef coldCallbacks
+        assertEqual "warm callback projection" 2
+            =<< readIORef warmCallbacks
+        Store.closeStore store
+
+rejectsCorruptedCachedDeclarationAnchor :: Assertion
+rejectsCorruptedCachedDeclarationAnchor =
+    withTemporaryDirectory "felix-parsed-corrupt-anchor" \temp -> do
+        writeBuiltinZeroDefinition
+            (temp Posix.</> "entry.tex")
+            "source_zero"
+        mounts <- oneMount "project" temp
+        request <- expectRight (searchedRoot "entry.tex")
+        foundation <- expectRight Foundation.checkedFoundation
+        let storePath = temp Posix.</> "store.sqlite"
+            theory = Identity.theoryId foundation
+        store <- openTestStore storePath theory
+        (cold, _measurements) <- expectParseExecution
+            =<< Parse.parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputs
+                store mounts request (const [])
+        let parsed = Parse.parsedWorkspaceRootModule cold
+            key = Parse.parsedModuleKey parsed
+        fileId <- case Parse.parsedModuleSyntaxOccurrences parsed of
+            occurrence : _ ->
+                expectJust
+                    "parsed occurrence file id"
+                    (locFileId
+                        (Parse.parsedSyntaxOccurrenceLocation occurrence))
+            [] ->
+                assertFailure "parsed fixed occurrence is absent"
+                    >> fail "unreachable"
+        decoded <- expectRight
+            (Parsed.decodeCanonicalParsedPayload
+                fileId
+                (Parse.parsedModulePayload parsed))
+        Store.closeStore store
+        let corruptedOccurrences = case Parsed.decodedParsedOccurrences decoded of
+                (blockIndex, location, _marker, entry) : rest ->
+                    (blockIndex, location, "corrupted_anchor", entry) : rest
+                [] ->
+                    []
+            corruptedPayload =
+                Parsed.canonicalParsedPayload
+                    (Parsed.decodedParsedImports decoded)
+                    (Parsed.decodedParsedBlocks decoded)
+                    corruptedOccurrences
+                    (Parsed.decodedParsedSyntaxInterface decoded)
+            corruptedId =
+                ParsedIdentity.parsedModuleId
+                    key
+                    (Parsed.canonicalParsedPayloadBytes corruptedPayload)
+        connection <- SQLite.open storePath
+        SQLite.execute connection
+            "UPDATE parsed_artifacts \
+            \SET parsed_module_id = ?, payload = ? \
+            \WHERE parsed_module_key = ?"
+            ( Cache.cacheDigestBytes
+                (ParsedIdentity.parsedModuleIdDigest corruptedId)
+            , Parsed.canonicalParsedPayloadBytes corruptedPayload
+            , Cache.cacheDigestBytes
+                (ParsedIdentity.parsedModuleKeyDigest key)
+            )
+        SQLite.close connection
+        current <- openTestStore storePath theory
+        callbacks <- newIORef (0 :: Int)
+        Parse.parseSourceWorkspaceMeasuredWithStoreAndSyntaxInputsAndCallback
+            current mounts request (const [])
+            (\_source _block -> modifyIORef' callbacks (+ 1)) >>= \case
+                Left
+                    (Parse.ParseExecutionArtifactIntegrityFailure
+                        _source
+                        (Parse.ParsedArtifactAssociationFailure
+                            Parse.SyntaxOccurrenceMarkerMismatch{})) ->
+                            pure ()
+                other ->
+                    assertFailure
+                        ("unexpected corrupted parsed result: " <> show other)
+        assertEqual "corrupt hit invokes no parse callback" 0
+            =<< readIORef callbacks
+        Store.closeStore current
+
+openTestStore :: FilePath -> Identity.TheoryId -> IO Store.Store
+openTestStore path theory =
+    Store.openStore path theory >>= \case
+        Left failure ->
+            assertFailure (show failure) >> fail "unreachable"
+        Right (_startup, store) ->
+            pure store
+
+expectParseExecution
+    :: Either Parse.ParseExecutionError value
+    -> IO value
+expectParseExecution = \case
+    Left failure ->
+        assertFailure (show failure) >> fail "unreachable"
+    Right value ->
+        pure value
+
 parsesSourceGraph :: Assertion
 parsesSourceGraph =
     withTemporaryDirectory "felix-source-parse" \temp -> do