Revert "extractRules: WIP add assertion that ids are unique"

This reverts commit 4a4ce1b.

Author: ana-pantilie

kore/src/Kore/Exec.hs

@@ -103,9 +103,6 @@ import Kore.Internal.TermLike
 import Kore.Log.ErrorRewriteLoop
     ( errorRewriteLoop
     )
-import Kore.Log.ErrorRuleMergeDuplicateId
-    ( errorRuleMergeDuplicateIds
-    )
 import Kore.Log.InfoExecDepth
 import Kore.Log.KoreLogOptions
     ( KoreLogOptions (..)
@@ -573,11 +570,10 @@ 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
-    whenDuplicate errorRuleMergeDuplicateIds rulesById
-    -- whenDuplicate errorRuleMergeDuplicateLabel rulesByLabel
-    let ruleRegistry = Map.fromList (rulesById <> rulesByLabel)
+        ruleRegistry = Map.fromList (rulesById <> rulesByLabel)
     extractedRules <- traverse (extractRule ruleRegistry) names
     case extractedRules of
         [] -> throwE "Empty rule list."
@@ -609,24 +605,6 @@ 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
-    ( ErrorRuleMergeDuplicateIds
-    , errorRuleMergeDuplicateIds
+    ( ErrorRuleMergeDuplicateId
+    , errorRuleMergeDuplicateId
     ) where
 
 import Prelude.Kore
@@ -22,10 +22,6 @@ 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
     )
@@ -47,48 +43,43 @@ import Pretty
     )
 import qualified Pretty
 
-newtype ErrorRuleMergeDuplicateIds =
-    ErrorRuleMergeDuplicateIds
-        { unErrorRuleMergeDuplicateIds :: Map Text [SourceLocation]
+data ErrorRuleMergeDuplicateId =
+    ErrorRuleMergeDuplicateId
+        { locations :: [SourceLocation]
+        , ruleId :: Text
         }
     deriving (Show)
     deriving (GHC.Generic)
     deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
 
-instance Exception ErrorRuleMergeDuplicateIds where
+instance Exception ErrorRuleMergeDuplicateId where
     toException = toException . SomeEntry
     fromException exn =
         fromException exn >>= fromEntry
 
-instance Entry ErrorRuleMergeDuplicateIds where
+instance Entry ErrorRuleMergeDuplicateId where
     entrySeverity _ = Error
     helpDoc _ =
         "error thrown during rule merging when\
         \ multiple rules have the same id"
 
-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)
-                   ]
+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)
+               ]
 
-errorRuleMergeDuplicateIds :: Map Text [RewriteRule VariableName] -> a
-errorRuleMergeDuplicateIds duplicateIds =
-    throw (ErrorRuleMergeDuplicateIds idsWithlocations)
+errorRuleMergeDuplicateId :: [RewriteRule VariableName] -> Text -> a
+errorRuleMergeDuplicateId rules ruleId =
+    throw ErrorRuleMergeDuplicateId { locations, ruleId }
   where
-    idsWithlocations =
-        (fmap . fmap)
-        (
-            Lens.view
-                ( _Unwrapped
-                . field @"attributes"
-                . field @"sourceLocation"
-                )
-        )
-        duplicateIds
+    locations =
+        Lens.view
+            ( _Unwrapped
+            . field @"attributes"
+            . field @"sourceLocation"
+            )
+        <$> rules

kore/src/Kore/Log/Registry.hs

@@ -80,12 +80,6 @@ import Kore.Log.ErrorRewriteLoop
 import Kore.Log.ErrorRewritesInstantiation
     ( ErrorRewritesInstantiation
     )
-import Kore.Log.ErrorRuleMergeDuplicateId
-    ( ErrorRuleMergeDuplicateIds
-    )
-import Kore.Log.ErrorRuleMergeDuplicateLabel
-    ( ErrorRuleMergeDuplicateLabel
-    )
 import Kore.Log.InfoAttemptUnification
     ( InfoAttemptUnification
     )
@@ -161,8 +155,6 @@ 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