Reject Object-Symbol Marker Collisions

4 files changed, 158 insertions, 62 deletions

diff --git a/source/Checking.hs b/source/Checking.hs
index f6402f6..a5f8baa 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -66,6 +66,7 @@ initialCheckingState dumpPremselTraining emitTask = CheckingState
     , checkingPredicateDefinitions = mempty
     , checkingDefinitionDependencies = mempty
     , checkingOwnedSymbols = builtinOwnedSymbols
+    , checkingOwnedSymbolMarkers = builtinOwnedSymbolMarkers
     , checkingFrozenSymbols = mempty
     , checkingStructs = initCheckingStructs
     , checkingStructContext = mempty
@@ -127,6 +128,10 @@ data CheckingState = CheckingState
     , checkingOwnedSymbols :: HashMap Symbol SymbolOwner
     -- ^ Top-level symbols with an established introducing owner in this document.
     --
+    , checkingOwnedSymbolMarkers :: HashSet Marker
+    -- ^ Object-language markers claimed by top-level symbols.
+    -- INVARIANT: contains the marker of every key in 'checkingOwnedSymbols'.
+    --
     , checkingFrozenSymbols :: HashMap Symbol Marker
     -- ^ Symbols mentioned in an inductive specification may not be defined later.
     --
@@ -213,6 +218,14 @@ builtinOwnedSymbols =
         | symbol <- builtinSymbols
         ]
 
+builtinOwnedSymbolMarkers :: HashSet Marker
+builtinOwnedSymbolMarkers =
+    HS.fromList
+        [ marker
+        | symbol <- builtinSymbols
+        , Just marker <- [objectSymbolMarker symbol]
+        ]
+
 builtinReservedMixfixMarkers :: Set Marker
 builtinReservedMixfixMarkers =
     Set.fromList
@@ -468,9 +481,8 @@ formatSymbols symbols =
     Text.intercalate ", " (symbolText <$> Set.toList symbols)
 
 ownableSymbol :: Symbol -> Bool
-ownableSymbol = \case
-    SymbolInteger{} -> False
-    _ -> True
+ownableSymbol =
+    isJust . objectSymbolMarker
 
 markerTextOf :: Marker -> Text
 markerTextOf (Marker text) = text
@@ -487,19 +499,8 @@ symbolText = \case
         predicateText predicate
 
 predicateText :: Predicate -> Text
-predicateText = \case
-    PredicateAdj item ->
-        markerTextOf (lexicalItemMarker item)
-    PredicateVerb item ->
-        markerTextOf (lexicalItemSgPlMarker item)
-    PredicateNoun item ->
-        markerTextOf (lexicalItemSgPlMarker item)
-    PredicateRelation relation ->
-        markerTextOf (relationSymbolMarker relation)
-    PredicateSymbol text ->
-        text
-    PredicateNounStruct item ->
-        markerTextOf (lexicalItemSgPlMarker item)
+predicateText =
+    markerTextOf . predicateObjectMarker
 
 symbolOwnerKindText :: SymbolOwnerKind -> Text
 symbolOwnerKindText = \case
@@ -526,6 +527,17 @@ symbolOwnerKindText = \case
     OwnedByStructureDefinition ->
         "structure definition"
 
+symbolOwnerText :: SymbolOwner -> Text
+symbolOwnerText SymbolOwner{symbolOwnerKind, symbolOwnerMarker} =
+    symbolOwnerKindText symbolOwnerKind
+        <> " "
+        <> markerTextOf symbolOwnerMarker
+
+-- Multiple matches can only be builtin aliases, which all have 'builtinOwner'.
+symbolOwnerByMarker :: Marker -> HashMap Symbol SymbolOwner -> Maybe SymbolOwner
+symbolOwnerByMarker marker owners =
+    snd <$> List.find ((== Just marker) . objectSymbolMarker . fst) (HM.toList owners)
+
 assertOwnedSymbolsInFormula :: Formula -> Checking
 assertOwnedSymbolsInFormula phi = do
     owners <- gets checkingOwnedSymbols
@@ -537,39 +549,48 @@ assertOwnedSymbolsInFormula phi = do
         throwCheckingError ("top-level fact mentions symbol(s) without prior ownership: " <> formatSymbols unknown)
 
 claimSymbolOwnership :: SymbolOwnerKind -> Symbol -> Checking
-claimSymbolOwnership ownerKind symbol
-    | not (ownableSymbol symbol) =
-        skip
-    | otherwise = do
-        owners <- gets checkingOwnedSymbols
-        case HM.lookup symbol owners of
-            Just SymbolOwner{symbolOwnerKind, symbolOwnerMarker} ->
+claimSymbolOwnership ownerKind symbol =
+    case objectSymbolMarker symbol of
+        Nothing ->
+            skip
+        Just marker -> do
+            owners <- gets checkingOwnedSymbols
+            for_ (HM.lookup symbol owners) \owner ->
                 throwCheckingError
                     ( "symbol "
                         <> symbolText symbol
                         <> " is already owned by "
-                        <> symbolOwnerKindText symbolOwnerKind
-                        <> " "
-                        <> markerTextOf symbolOwnerMarker
+                        <> symbolOwnerText owner
+                    )
+
+            ownedMarkers <- gets checkingOwnedSymbolMarkers
+            when (marker `HS.member` ownedMarkers) do
+                throwCheckingError
+                    ( "object-symbol marker "
+                        <> markerTextOf marker
+                        <> " is already owned"
+                        <> maybe "" ((" by " <>) . symbolOwnerText) (symbolOwnerByMarker marker owners)
                     )
-            Nothing -> do
-                frozen <- gets checkingFrozenSymbols
-                currentMarker <- gets blockLabel
-                case HM.lookup symbol frozen of
-                    Just frozenBy | frozenBy /= currentMarker ->
-                        throwCheckingError
-                            ( "symbol "
-                                <> symbolText symbol
-                                <> " is frozen by inductive block "
-                                <> markerTextOf frozenBy
-                                <> " and cannot be defined here"
-                            )
-                    _ ->
-                        modify \st ->
-                            st
-                                { checkingOwnedSymbols =
-                                    HM.insert symbol (SymbolOwner ownerKind currentMarker) (checkingOwnedSymbols st)
-                                }
+
+            frozen <- gets checkingFrozenSymbols
+            currentMarker <- gets blockLabel
+            case HM.lookup symbol frozen of
+                Just frozenBy | frozenBy /= currentMarker ->
+                    throwCheckingError
+                        ( "symbol "
+                            <> symbolText symbol
+                            <> " is frozen by inductive block "
+                            <> markerTextOf frozenBy
+                            <> " and cannot be defined here"
+                        )
+                _ ->
+                    modify \st ->
+                        st
+                            { checkingOwnedSymbols =
+                                HM.insert symbol (SymbolOwner ownerKind currentMarker) (checkingOwnedSymbols st)
+                            , checkingOwnedSymbolMarkers =
+                                HS.insert marker (checkingOwnedSymbolMarkers st)
+                            }
 
 freezeSymbols :: Set Symbol -> Checking
 freezeSymbols symbols = do
diff --git a/source/Encoding.hs b/source/Encoding.hs
index 9f5e447..5239c3c 100644
--- a/source/Encoding.hs
+++ b/source/Encoding.hs
@@ -221,19 +221,8 @@ encodeSymbol = \case
 
 
 encodePredicate :: Predicate -> Tptp.AtomicWord
-encodePredicate = \case
-    PredicateAdj adj ->
-        unMarker (lexicalItemMarker adj)
-    PredicateVerb verb ->
-        unMarker (lexicalItemSgPlMarker verb)
-    PredicateNoun noun ->
-        unMarker (lexicalItemSgPlMarker noun)
-    PredicateRelation rel ->
-        unMarker (relationSymbolMarker rel)
-    PredicateNounStruct noun ->
-        unMarker (lexicalItemSgPlMarker noun)
-    PredicateSymbol symb ->
-        unMarker (Marker symb)
+encodePredicate =
+    unMarker . predicateObjectMarker
 
 unMarker :: Marker -> Tptp.AtomicWord
 unMarker (Marker m) = Tptp.AtomicWord m
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs
index 9ba6921..5037e14 100644
--- a/source/Syntax/Internal.hs
+++ b/source/Syntax/Internal.hs
@@ -83,6 +83,35 @@ data Predicate
     deriving (Show, Eq, Ord, Generic, Hashable)
 
 
+-- | The object-language marker of an ownable symbol.
+objectSymbolMarker :: Symbol -> Maybe Marker
+objectSymbolMarker = \case
+    SymbolMixfix symbol ->
+        Just (mixfixMarker symbol)
+    SymbolFun symbol ->
+        Just (lexicalItemSgPlMarker symbol)
+    SymbolInteger{} ->
+        Nothing
+    SymbolPredicate predicate ->
+        Just (predicateObjectMarker predicate)
+
+-- | The object-language marker of a predicate.
+predicateObjectMarker :: Predicate -> Marker
+predicateObjectMarker = \case
+    PredicateAdj item ->
+        lexicalItemMarker item
+    PredicateVerb item ->
+        lexicalItemSgPlMarker item
+    PredicateNoun item ->
+        lexicalItemSgPlMarker item
+    PredicateRelation relation ->
+        relationSymbolMarker relation
+    PredicateSymbol text ->
+        Marker text
+    PredicateNounStruct item ->
+        lexicalItemSgPlMarker item
+
+
 data Quantifier
     = Universally
     | Existentially
diff --git a/source/Test/Unit/Checking.hs b/source/Test/Unit/Checking.hs
index cea5873..352ec4e 100644
--- a/source/Test/Unit/Checking.hs
+++ b/source/Test/Unit/Checking.hs
@@ -57,6 +57,16 @@ unitTests = testGroup "Checking"
         expectCheckingError "self-referential" directSelfReferentialAbbrBlocks
     , testCase "abbreviations reject indirect self-reference after expansion" do
         expectCheckingError "self-referential" indirectSelfReferentialAbbrBlocks
+    , testCase "definitions reject builtin mixfix marker collisions" do
+        expectCheckingError "object-symbol marker pow is already owned by builtin" [builtinMixfixMarkerCollisionBlock]
+    , testCase "definitions reject builtin predicate marker collisions" do
+        expectCheckingError "object-symbol marker elem is already owned by builtin" [builtinPredicateMarkerCollisionBlock]
+    , testCase "abbreviations reject builtin marker collisions" do
+        expectCheckingError "object-symbol marker pow is already owned by builtin" [builtinAbbreviationMarkerCollisionBlock]
+    , testCase "builtin object markers do not reserve proof labels" do
+        expectChecks [builtinMarkerProofLabelBlock]
+    , testCase "subseteq remains user-definable" do
+        expectChecks [subseteqDefinitionBlock]
     , testCase "datatype accepts bootstrap propositional fragment" do
         expectChecks [goodDatatypeBlock]
     , testCase "datatype rejects nested recursive premise" do
@@ -81,8 +91,8 @@ unitTests = testGroup "Checking"
         expectChecks datatypeInjectiveReferenceBlocks
     , testCase "datatype generated fact markers cannot be reused by later blocks" do
         expectDuplicateMarker "propform_cases" datatypeGeneratedMarkerReuseBlocks
-    , testCase "datatype rejects synthetic fact marker collisions within one datatype" do
-        expectDuplicateMarker "propform_dup_intro" [badDuplicateGeneratedMarkerDatatypeBlock]
+    , testCase "datatype rejects duplicate constructor markers" do
+        expectCheckingError "object-symbol marker dup is already owned by datatype constructor" [badDuplicateConstructorMarkerDatatypeBlock]
     , testCase "signature predicate declares symbols for later facts" do
         expectChecks signaturePredicateUsageBlocks
     , testCase "signature formula declares symbolic operators for later facts" do
@@ -352,6 +362,49 @@ indirectSelfReferentialAbbrBlocks =
     , BlockAbbr Nowhere "bad_abbr_indirect_b" (Abbreviation abbrSymbolB (toScope (TermSymbol Nowhere abbrSymbolA [])))
     ]
 
+builtinMixfixMarkerCollisionBlock :: Block
+builtinMixfixMarkerCollisionBlock =
+    BlockDefn Nowhere "pow" (DefnOp powHijackSym ["A"] emptySet)
+
+powHijackSym :: FunctionSymbol
+powHijackSym =
+    mkMixfixItem
+        [Just (Command "powhijack"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR]
+        "pow"
+        NonAssoc
+
+builtinPredicateMarkerCollisionBlock :: Block
+builtinPredicateMarkerCollisionBlock =
+    BlockDefn Nowhere "elem"
+        ( DefnPredicate
+            []
+            (PredicateRelation (RelationSymbol (Command "elemhijack") "elem"))
+            ("A" :| ["B"])
+            (var "A" `eq` var "B")
+        )
+
+builtinAbbreviationMarkerCollisionBlock :: Block
+builtinAbbreviationMarkerCollisionBlock =
+    BlockAbbr Nowhere "pow"
+        ( Abbreviation
+            (SymbolMixfix (constSymbolWithMarker "powabbr" "pow"))
+            (toScope (TermSymbol Nowhere (SymbolInteger 0) []))
+        )
+
+builtinMarkerProofLabelBlock :: Block
+builtinMarkerProofLabelBlock =
+    BlockAxiom Nowhere "pow" (Axiom [] (emptySet `eq` emptySet))
+
+subseteqDefinitionBlock :: Block
+subseteqDefinitionBlock =
+    BlockDefn Nowhere "subseteq"
+        ( DefnPredicate
+            []
+            (PredicateRelation SubseteqSymbol)
+            ("A" :| ["B"])
+            (var "A" `eq` var "B")
+        )
+
 goodDatatypeBlock :: Block
 goodDatatypeBlock =
     datatypeBlock "good_datatype" goodDatatypeClauses
@@ -411,9 +464,9 @@ datatypeGeneratedMarkerReuseBlocks =
     , BlockLemma Nowhere "propform_cases" (Lemma [] Top)
     ]
 
-badDuplicateGeneratedMarkerDatatypeBlock :: Block
-badDuplicateGeneratedMarkerDatatypeBlock =
-    datatypeBlock "bad_duplicate_generated_marker_datatype"
+badDuplicateConstructorMarkerDatatypeBlock :: Block
+badDuplicateConstructorMarkerDatatypeBlock =
+    datatypeBlock "propform"
         ( DatatypeClause (SymbolPattern (unarySymbol "dup") ["n"]) [("n", naturalsTerm)] :|
             [ DatatypeClause (SymbolPattern (infixSymbol "dup") ["p", "q"]) [("p", propformTerm), ("q", propformTerm)]
             ]
@@ -989,6 +1042,10 @@ constSymbol :: Text -> FunctionSymbol
 constSymbol name =
     mkMixfixItem [Just (Command name)] (Marker name) NonAssoc
 
+constSymbolWithMarker :: Text -> Marker -> FunctionSymbol
+constSymbolWithMarker name marker =
+    mkMixfixItem [Just (Command name)] marker NonAssoc
+
 unarySymbol :: Text -> FunctionSymbol
 unarySymbol name =
     mkMixfixItem [Just (Command name), Just InvisibleBraceL, Nothing, Just InvisibleBraceR] (Marker name) NonAssoc