extractRules: WIP add assertion that ids are unique

Author: ana-pantilie

kore/src/Kore/Exec.hs

@@ -103,6 +103,9 @@ import Kore.Internal.TermLike
 import Kore.Log.ErrorRewriteLoop
     ( errorRewriteLoop
     )
+import Kore.Log.ErrorRuleMergeDuplicateId
+    ( errorRuleMergeDuplicateIds
+    )
 import Kore.Log.InfoExecDepth
 import Kore.Log.KoreLogOptions
     ( KoreLogOptions (..)
@@ -570,10 +573,11 @@ extractRules
     -> [Text]
     -> ExceptT Text m (NonEmpty (RewriteRule VariableName))
 extractRules rules names = do
-    -- TODO: assert unique names
     let rulesById = mapMaybe ruleById rules
         rulesByLabel = mapMaybe ruleByLabel rules
-        ruleRegistry = Map.fromList (rulesById <> rulesByLabel)
+    whenDuplicate errorRuleMergeDuplicateIds rulesById
+    -- whenDuplicate errorRuleMergeDuplicateLabel rulesByLabel
+    let ruleRegistry = Map.fromList (rulesById <> rulesByLabel)
     extractedRules <- traverse (extractRule ruleRegistry) names
     case extractedRules of
         [] -> throwE "Empty rule list."
@@ -605,6 +609,24 @@ extractRules rules names = do
             return
             (Map.lookup ruleName registry)
 
+    whenDuplicate logError withNames = do
+        let duplicateNames = findCollisions . mkMapWithCollisions $ withNames
+        unless (null duplicateNames) (logError duplicateNames)
+
+mkMapWithCollisions
+    :: Ord key
+    => [(key, val)]
+    -> Map.Map key [val]
+mkMapWithCollisions pairs =
+    Map.fromListWith (<>)
+    $ (fmap . fmap) pure pairs
+
+findCollisions :: Map.Map key [val] -> Map.Map key [val]
+findCollisions = filter (not . isSingleton)
+  where
+    isSingleton [_] = True
+    isSingleton _ = False
+
 assertSingleClaim :: Monad m => [claim] -> m ()
 assertSingleClaim claims =
     when (length claims > 1) . error

kore/src/Kore/Log/ErrorRuleMergeDuplicateId.hs

@@ -5,8 +5,8 @@ License     : NCSA
 -}
 
 module Kore.Log.ErrorRuleMergeDuplicateId
-    ( ErrorRuleMergeDuplicateId
-    , errorRuleMergeDuplicateId
+    ( ErrorRuleMergeDuplicateIds
+    , errorRuleMergeDuplicateIds
     ) where
 
 import Prelude.Kore
@@ -22,6 +22,10 @@ import Data.Generics.Product
 import Data.Generics.Wrapped
     ( _Unwrapped
     )
+import Data.Map.Strict
+    ( Map
+    )
+import qualified Data.Map.Strict as Map
 import Data.Text
     ( Text
     )
@@ -43,43 +47,48 @@ import Pretty
     )
 import qualified Pretty
 
-data ErrorRuleMergeDuplicateId =
-    ErrorRuleMergeDuplicateId
-        { locations :: [SourceLocation]
-        , ruleId :: Text
+newtype ErrorRuleMergeDuplicateIds =
+    ErrorRuleMergeDuplicateIds
+        { unErrorRuleMergeDuplicateIds :: Map Text [SourceLocation]
         }
     deriving (Show)
     deriving (GHC.Generic)
     deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
 
-instance Exception ErrorRuleMergeDuplicateId where
+instance Exception ErrorRuleMergeDuplicateIds where
     toException = toException . SomeEntry
     fromException exn =
         fromException exn >>= fromEntry
 
-instance Entry ErrorRuleMergeDuplicateId where
+instance Entry ErrorRuleMergeDuplicateIds where
     entrySeverity _ = Error
     helpDoc _ =
         "error thrown during rule merging when\
         \ multiple rules have the same id"
 
-instance Pretty ErrorRuleMergeDuplicateId where
-    pretty ErrorRuleMergeDuplicateId { locations , ruleId } =
-        Pretty.vsep
-            $ ["The rules at the following locations:"]
-            <> fmap (Pretty.indent 4 . pretty) locations
-            <> [ Pretty.indent 2 "all have the following id:"
-               , Pretty.indent 4 (pretty ruleId)
-               ]
+instance Pretty ErrorRuleMergeDuplicateIds where
+    pretty (ErrorRuleMergeDuplicateIds duplicateIds) =
+        Map.foldMapWithKey accum duplicateIds
+      where
+        accum ruleId locations =
+            Pretty.vsep
+                $ ["The rules at the following locations:"]
+                <> fmap (Pretty.indent 4 . pretty) locations
+                <> [ Pretty.indent 2 "all have the following id:"
+                   , Pretty.indent 4 (pretty ruleId)
+                   ]
 
-errorRuleMergeDuplicateId :: [RewriteRule VariableName] -> Text -> a
-errorRuleMergeDuplicateId rules ruleId =
-    throw ErrorRuleMergeDuplicateId { locations, ruleId }
+errorRuleMergeDuplicateIds :: Map Text [RewriteRule VariableName] -> a
+errorRuleMergeDuplicateIds duplicateIds =
+    throw (ErrorRuleMergeDuplicateIds idsWithlocations)
   where
-    locations =
-        Lens.view
-            ( _Unwrapped
-            . field @"attributes"
-            . field @"sourceLocation"
-            )
-        <$> rules
+    idsWithlocations =
+        (fmap . fmap)
+        (
+            Lens.view
+                ( _Unwrapped
+                . field @"attributes"
+                . field @"sourceLocation"
+                )
+        )
+        duplicateIds

kore/src/Kore/Log/Registry.hs

@@ -80,6 +80,12 @@ import Kore.Log.ErrorRewriteLoop
 import Kore.Log.ErrorRewritesInstantiation
     ( ErrorRewritesInstantiation
     )
+import Kore.Log.ErrorRuleMergeDuplicateId
+    ( ErrorRuleMergeDuplicateIds
+    )
+import Kore.Log.ErrorRuleMergeDuplicateLabel
+    ( ErrorRuleMergeDuplicateLabel
+    )
 import Kore.Log.InfoAttemptUnification
     ( InfoAttemptUnification
     )
@@ -155,6 +161,8 @@ entryHelpDocs :: [Pretty.Doc ()]
     , mk $ Proxy @ErrorBottomTotalFunction
     , mk $ Proxy @ErrorDecidePredicateUnknown
     , mk $ Proxy @ErrorParse
+    , mk $ Proxy @ErrorRuleMergeDuplicateIds
+    , mk $ Proxy @ErrorRuleMergeDuplicateLabel
     , mk $ Proxy @WarnFunctionWithoutEvaluators
     , mk $ Proxy @WarnSymbolSMTRepresentation
     , mk $ Proxy @WarnStuckClaimState