Defer fixed-base conflicts to semantic ownership

2 files changed, 178 insertions, 169 deletions

diff --git a/source/Felix/Parse.hs b/source/Felix/Parse.hs
index 9510208..e8eefe8 100644
--- a/source/Felix/Parse.hs
+++ b/source/Felix/Parse.hs
@@ -477,9 +477,6 @@ data SyntaxDeclarationSite = SyntaxDeclarationSite
 type SyntaxEntryInventory =
     Map CanonicalLexicalEntry (Set SyntaxDeclarationSite)
 
-type FixedProviderInventory =
-    Map CanonicalLexicalEntry (Set SyntaxDeclarationSite)
-
 data PreparedSyntaxOccurrence = PreparedSyntaxOccurrence
     { preparedSyntaxSite :: !SyntaxDeclarationSite
     , preparedSyntaxEntry :: !CanonicalLexicalEntry
@@ -499,9 +496,7 @@ data RuntimeSyntaxModule = RuntimeSyntaxModule
     { runtimeAddress :: !ResolvedSourceAddress
     , runtimeInterface :: !ModuleSyntaxInterface
     , runtimeSyntaxDirectAddresses :: ![ResolvedSourceAddress]
-    , runtimePhysicalDirectAddresses :: ![ResolvedSourceAddress]
     , runtimeLocalEntries :: !SyntaxEntryInventory
-    , runtimeLocalFixedProviders :: !FixedProviderInventory
     , runtimeLexicon :: !Lexicon
     , runtimePreparedOccurrences :: ![[PreparedSyntaxOccurrence]]
     }
@@ -921,31 +916,22 @@ prepareRuntimeSyntaxModule
     -> Either ParseWorkspaceError RuntimeSyntaxModule
 prepareRuntimeSyntaxModule moduleIndex runtimeByAddress
         (ScannedModule node imports chunks) = do
-    physicalDirects <- traverse
+    directModules <- traverse
         (lookupRuntimeModule runtimeByAddress)
-        physicalDirectAddresses
+        directAddresses
     let syntaxDirects =
-            distinctSyntaxInterfaces physicalDirects
+            distinctSyntaxInterfaces directModules
         syntaxDirectAddresses =
             runtimeAddress <$> syntaxDirects
     importedEntries <-
         foldImportedSyntax
             runtimeByAddress
             syntaxDirectAddresses
-    importedProviders <-
-        foldImportedFixedProviders
-            runtimeByAddress
-            physicalDirectAddresses
-    validateFixedProviders importedProviders
-    ( localEntries
-      , localProviders
-      , preparedOccurrences
-      ) <-
+    (localEntries, preparedOccurrences) <-
         prepareLocalSyntax
             moduleIndex
             source
             importedEntries
-            importedProviders
             chunks
     localDelta <-
         validateSyntaxInventory localEntries
@@ -977,10 +963,7 @@ prepareRuntimeSyntaxModule moduleIndex runtimeByAddress
             , runtimeInterface = interface
             , runtimeSyntaxDirectAddresses =
                 syntaxDirectAddresses
-            , runtimePhysicalDirectAddresses =
-                physicalDirectAddresses
             , runtimeLocalEntries = localEntries
-            , runtimeLocalFixedProviders = localProviders
             , runtimeLexicon = lexicon
             , runtimePreparedOccurrences =
                 preparedOccurrences
@@ -988,7 +971,7 @@ prepareRuntimeSyntaxModule moduleIndex runtimeByAddress
   where
     source = sourceNodeResolved node
     address = resolvedSourceAddress source
-    physicalDirectAddresses =
+    directAddresses =
         nubOrd
             (parsedImportedAddress <$> imports)
 
@@ -1054,78 +1037,28 @@ foldImportedSyntax runtimeByAddress addresses =
                         (runtimeLocalEntries runtime)
                     )
 
-foldImportedFixedProviders
-    :: Map ResolvedSourceAddress RuntimeSyntaxModule
-    -> [ResolvedSourceAddress]
-    -> Either ParseWorkspaceError FixedProviderInventory
-foldImportedFixedProviders runtimeByAddress addresses =
-    snd <$> foldM visit (Set.empty, Map.empty) addresses
-  where
-    visit state address
-        | address `Set.member` fst state =
-            Right state
-        | otherwise = do
-            runtime <- lookupRuntimeModule runtimeByAddress address
-            let marked =
-                    (Set.insert address (fst state), snd state)
-            afterImports <- foldM
-                visit
-                marked
-                (runtimePhysicalDirectAddresses runtime)
-            Right
-                ( fst afterImports
-                , Map.unionWith
-                    Set.union
-                    (snd afterImports)
-                    (runtimeLocalFixedProviders runtime)
-                )
-
-validateFixedProviders
-    :: FixedProviderInventory
-    -> Either ParseWorkspaceError ()
-validateFixedProviders providers =
-    case
-        [ (entry, sites)
-        | (entry, sites) <- Map.toAscList providers
-        , Set.size sites > 1
-        ] of
-        [] ->
-            Right ()
-        (entry, sites) : _ ->
-            Left
-                (SourceLexiconCollision
-                    (fixedProviderCollision entry sites))
-
 prepareLocalSyntax
     :: Int
     -> ResolvedSource
     -> SyntaxEntryInventory
-    -> FixedProviderInventory
     -> [ScannedChunk]
     -> Either
         ParseWorkspaceError
         ( SyntaxEntryInventory
-        , FixedProviderInventory
         , [[PreparedSyntaxOccurrence]]
         )
 prepareLocalSyntax
         moduleIndex
         source
         importedEntries
-        importedProviders
         chunks = do
-    ( localEntries
-      , localProviders
-      , _allProviders
-      , reversedOccurrences
-      ) <-
+    (localEntries, reversedOccurrences) <-
         foldM
             prepareOne
-            (Map.empty, Map.empty, importedProviders, [])
+            (Map.empty, [])
             (zip [0 ..] chunks)
     pure
         ( localEntries
-        , localProviders
         , reverse reversedOccurrences
         )
   where
@@ -1133,11 +1066,7 @@ prepareLocalSyntax
         syntaxSurfaceIndex importedEntries
 
     prepareOne
-            ( localEntries
-              , localProviders
-              , allProviders
-              , reversedOccurrences
-              )
+            (localEntries, reversedOccurrences)
             (blockIndex, chunk) = do
         classified <-
             prepareSyntaxChunk
@@ -1147,28 +1076,18 @@ prepareLocalSyntax
                 importedEntries
                 importedIndex
                 chunk
-        ( localEntries'
-          , localProviders'
-          , allProviders'
-          , reversedPrepared
-          ) <-
+        (localEntries', reversedPrepared) <-
             foldM
                 insertClassified
-                ( localEntries
-                , localProviders
-                , allProviders
-                , []
-                )
+                (localEntries, [])
                 classified
         pure
             ( localEntries'
-            , localProviders'
-            , allProviders'
             , reverse reversedPrepared : reversedOccurrences
             )
 
     insertClassified
-            (entries, localProviders, allProviders, reversed)
+            (entries, reversed)
             (ClassifiedSyntaxItem site disposition _eligible) =
         case disposition of
             EmitSyntaxEntry entry ->
@@ -1178,8 +1097,6 @@ prepareLocalSyntax
                         entry
                         (Set.singleton site)
                         entries
-                    , localProviders
-                    , allProviders
                     , PreparedSyntaxOccurrence
                         site
                         entry
@@ -1188,46 +1105,19 @@ prepareLocalSyntax
             ReuseImportedSyntax entry ->
                 Right
                     ( entries
-                    , localProviders
-                    , allProviders
                     , PreparedSyntaxOccurrence
                         site
                         entry
                         : reversed
                     )
             ReuseFixedSyntax entry ->
-                let existing =
-                        Map.findWithDefault
-                            Set.empty
-                            entry
-                            allProviders
-                    combined =
-                        Set.insert site existing
-                in
-                    if Set.null existing
-                        then
-                            Right
-                                ( entries
-                                , Map.insertWith
-                                    Set.union
-                                    entry
-                                    (Set.singleton site)
-                                    localProviders
-                                , Map.insert
-                                    entry
-                                    combined
-                                    allProviders
-                                , PreparedSyntaxOccurrence
-                                    site
-                                    entry
-                                    : reversed
-                                )
-                        else
-                            Left
-                                (SourceLexiconCollision
-                                    (fixedProviderCollision
-                                        entry
-                                        combined))
+                Right
+                    ( entries
+                    , PreparedSyntaxOccurrence
+                        site
+                        entry
+                        : reversed
+                    )
 
 prepareSyntaxChunk
     :: Int
@@ -1720,17 +1610,6 @@ sourceCollisionOrigin entry site =
         (syntaxSiteSource site)
         (syntaxSiteLocation site)
 
-fixedProviderCollision
-    :: CanonicalLexicalEntry
-    -> Set SyntaxDeclarationSite
-    -> LexiconCollision
-fixedProviderCollision entry sites =
-    makeLexiconCollision
-        (entryPrimarySurface entry)
-        [ sourceCollisionOrigin entry site
-        | site <- Set.toAscList sites
-        ]
-
 makeLexiconCollision
     :: Raw.Pattern
     -> [LexiconCollisionOrigin]
diff --git a/source/Test/Unit/Source.hs b/source/Test/Unit/Source.hs
index 80c87c5..bfe230f 100644
--- a/source/Test/Unit/Source.hs
+++ b/source/Test/Unit/Source.hs
@@ -43,6 +43,7 @@ import Syntax.Token (runLexer)
 
 import Bound.Scope (toScope)
 import Control.Exception (bracket, evaluate, try)
+import Control.Monad (foldM)
 import Control.Monad.Logger (runNoLoggingT)
 import Data.ByteString qualified as ByteString
 import Data.HashMap.Strict qualified as HashMap
@@ -144,8 +145,8 @@ unitTests = testGroup "Source resolution"
         acceptsBuiltinSourceDeclaration
     , testCase "keeps the built-in marker for a prefix predicate declaration"
         acceptsBuiltinPrefixPredicateDeclaration
-    , testCase "rejects a second source declaration of a built-in pattern"
-        rejectsSecondBuiltinSourceDeclaration
+    , testCase "rejects duplicate fixed-base semantics during checking"
+        rejectsDuplicateFixedBaseSemantics
     , testCase "does not rescan repeated canonical imports"
         avoidsAliasImportLexiconCollision
     , testCase "parses loaded sources without rereading files" parsesWithoutRereading
@@ -3242,35 +3243,161 @@ acceptsBuiltinPrefixPredicateDeclaration =
                         ("unexpected built-in prefix declaration parse: "
                             <> show blocks)
 
-rejectsSecondBuiltinSourceDeclaration :: Assertion
-rejectsSecondBuiltinSourceDeclaration =
+rejectsDuplicateFixedBaseSemantics :: Assertion
+rejectsDuplicateFixedBaseSemantics =
     withTemporaryDirectory "felix-source-builtin-collision" \temp -> do
         writeBuiltinZeroDefinition
             (temp Posix.</> "a.tex")
             "source_zero_a"
-        writeBuiltinZeroDefinition
-            (temp Posix.</> "b.tex")
-            "source_zero_b"
-        writeTheory
+        writeFile
             (temp Posix.</> "entry.tex")
-            ["a.tex", "b.tex"]
-            "entry"
+            ("\\import{a.tex}\n"
+                <> builtinZeroDefinition "source_zero_b")
         graph <- buildSearchedGraph temp "entry.tex"
-        collision <- expectLexiconCollision
+        workspace <- expectRight
             =<< Parse.parseResolvedSourceGraph graph
-        assertEqual "built-in collision pattern"
-            (Raw.TokenCons (Raw.Command "zero") Raw.End)
-            (Parse.lexiconCollisionPattern collision)
-        (firstLocation, secondLocation) <-
-            expectTwoCollisionLocations collision
-        assertLocation "first source declaration"
-            "a.tex"
-            1
-            firstLocation
-        assertLocation "second source declaration"
-            "b.tex"
-            1
-            secondLocation
+        assignments <-
+            expectRight
+                (Legacy.assignLegacyModuleOrdinals workspace)
+        case toList assignments of
+            [acceptedAssignment, collidingAssignment] -> do
+                let acceptedParsed =
+                        Legacy.assignedParsedModule acceptedAssignment
+                    collidingParsed =
+                        Legacy.assignedParsedModule collidingAssignment
+                acceptedLocation <-
+                    onlySyntaxOccurrenceLocation acceptedParsed
+                collidingLocation <-
+                    onlySyntaxOccurrenceLocation collidingParsed
+                assertLocation
+                    "accepted declaration"
+                    "a.tex"
+                    1
+                    acceptedLocation
+                assertLocation
+                    "colliding declaration"
+                    "entry.tex"
+                    2
+                    collidingLocation
+                assertEqual
+                    "fixed reuses emit no syntax delta"
+                    [[], []]
+                    [ Interface.canonicalSyntaxDeltaEntries
+                        (Interface.moduleSyntaxLocalDelta
+                            (Parse.parsedModuleSyntaxInterface parsed))
+                    | parsed <- [acceptedParsed, collidingParsed]
+                    ]
+
+                checkedFoundationValue <-
+                    expectRight Foundation.checkedFoundation
+                (acceptedBlocks, glossState) <-
+                    glossParsedBlocks
+                        Meaning.initialGlossState
+                        acceptedParsed
+                acceptedBuilder <-
+                    expectRight
+                        (Transition.openTransitionModuleBuilder
+                            checkedFoundationValue
+                            Checking.initialLegacyCheckingEnvironment
+                            acceptedAssignment
+                            [])
+                acceptedState <-
+                    Checking.runCheckingBlocks
+                        acceptedBlocks
+                        (checkingState acceptedBuilder)
+                finalAcceptedBuilder <-
+                    expectJust
+                        "accepted transition builder"
+                        (Checking.checkingTransitionModuleBuilder
+                            acceptedState)
+                acceptedModule <-
+                    expectRight
+                        (Transition.sealTransitionModule
+                            (Checking.checkingStateEnvironment
+                                acceptedState)
+                            finalAcceptedBuilder)
+
+                (collidingBlocks, _finalGlossState) <-
+                    glossParsedBlocks glossState collidingParsed
+                collidingBuilder <-
+                    expectRight
+                        (Transition.openTransitionModuleBuilder
+                            checkedFoundationValue
+                            Checking.initialLegacyCheckingEnvironment
+                            collidingAssignment
+                            [acceptedModule])
+                result <-
+                    try
+                        (Checking.runCheckingBlocks
+                            collidingBlocks
+                            (checkingState collidingBuilder))
+                        :: IO
+                            (Either
+                                Checking.CheckingError
+                                Checking.CheckingState)
+                case result of
+                    Left
+                        (Checking.CheckingError
+                            message
+                            location
+                            marker) -> do
+                                assertEqual
+                                    "semantic collision location"
+                                    collidingLocation
+                                    location
+                                assertEqual
+                                    "semantic collision marker"
+                                    "source_zero_b"
+                                    marker
+                                assertBool
+                                    "accepted owner is identified"
+                                    ("already owned by abbreviation source_zero_a"
+                                        `Text.isInfixOf` message)
+                    Left err ->
+                        assertFailure
+                            ("expected located ownership collision, got "
+                                <> show err)
+                    Right _checked ->
+                        assertFailure
+                            "duplicate fixed-base semantics were accepted"
+            actual ->
+                assertFailure
+                    ("expected two module assignments, got "
+                        <> show (length actual))
+  where
+    checkingState builder =
+        Checking.initialTransitionCheckingStateWithTaskPreparation
+            Checking.WithoutDumpPremselTraining
+            id
+            builder
+            (\_batch ->
+                assertFailure
+                    "fixed-base abbreviation emitted an obligation")
+
+    glossParsedBlocks initialState parsed =
+        fmap
+            (\(reversed, finalState) ->
+                (reverse reversed, finalState))
+            (foldM
+                glossOne
+                ([], initialState)
+                (Parse.parsedModuleBlocks parsed))
+
+    glossOne (reversed, state) raw = do
+        (block, nextState) <-
+            expectRight (Meaning.glossStep state raw)
+        pure (block : reversed, nextState)
+
+    onlySyntaxOccurrenceLocation parsed =
+        case Parse.parsedModuleSyntaxOccurrences parsed of
+            [occurrence] ->
+                pure
+                    (Parse.parsedSyntaxOccurrenceLocation
+                        occurrence)
+            occurrences ->
+                assertFailure
+                    ("expected one fixed-base occurrence, got "
+                        <> show occurrences)
 
 avoidsAliasImportLexiconCollision :: Assertion
 avoidsAliasImportLexiconCollision =
@@ -3521,12 +3648,15 @@ writeNounDefinition path marker =
 
 writeBuiltinZeroDefinition :: FilePath -> String -> IO ()
 writeBuiltinZeroDefinition path marker =
-    writeFile path
-        (unlines
-            [ "\\begin{abbreviation}\\label{" <> marker <> "}"
-            , "  $\\zero = \\emptyset$."
-            , "\\end{abbreviation}"
-            ])
+    writeFile path (builtinZeroDefinition marker)
+
+builtinZeroDefinition :: String -> String
+builtinZeroDefinition marker =
+    unlines
+        [ "\\begin{abbreviation}\\label{" <> marker <> "}"
+        , "  $\\zero = \\emptyset$."
+        , "\\end{abbreviation}"
+        ]
 
 writeBuiltinCongDefinition :: FilePath -> IO ()
 writeBuiltinCongDefinition path =