extractRules: refactor and add errors

Author: ana-pantilie

kore/src/Kore/Exec.hs

@@ -53,7 +53,6 @@ import Data.Generics.Wrapped
     ( _Unwrapped
     )
 import qualified Data.List as List
-import qualified Data.Map.Strict as Map
 import Data.Text
     ( Text
     )
@@ -103,6 +102,12 @@ import Kore.Internal.TermLike
 import Kore.Log.ErrorRewriteLoop
     ( errorRewriteLoop
     )
+import Kore.Log.ErrorRuleMergeDuplicateId
+    ( errorRuleMergeDuplicateId
+    )
+import Kore.Log.ErrorRuleMergeDuplicateLabel
+    ( errorRuleMergeDuplicateLabel
+    )
 import Kore.Log.InfoExecDepth
 import Kore.Log.KoreLogOptions
     ( KoreLogOptions (..)
@@ -562,48 +567,67 @@ mergeRules ruleMerger verifiedModule ruleNames =
         rules <- extractRules rewriteRules' ruleNames
         lift $ ruleMerger rules
 
--- TODO: what if a label name and an id name coincide?
 extractRules
     :: forall m
     .  Monad m
     => [RewriteRule VariableName]
     -> [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)
-    extractedRules <- traverse (extractRule ruleRegistry) names
+    extractedRules <- traverse extractRule names
     case extractedRules of
         [] -> throwE "Empty rule list."
         (r : rs) -> return (r :| rs)
-
   where
-    -- TODO: more clean-up
-    maybeRuleUniqueId :: RewriteRule VariableName -> Maybe Text
-    maybeRuleUniqueId =
+    extractRule name = do
+        let rulesWithId =
+                filter (\rule -> lensUniqueId rule == Just name) rules
+            rulesWithLabel =
+                filter (\rule -> lensLabel rule == Just name) rules
+        case getRuleExtractionResult rulesWithId rulesWithLabel of
+            ErrorRuleNotFound -> throwE ("Rule not found: '" <> name <> "'.")
+            FoundRule rule -> return rule
+            ErrorDuplicateId rules' ->
+                errorRuleMergeDuplicateId rules' name
+            ErrorDuplicateLabel rules' ->
+                errorRuleMergeDuplicateLabel rules' name
+            ErrorIdAndLabelNamesCoincide ->
+                throwE ("Rule name: '" <> name <> "' is both an id and a label.")
+
+    lensUniqueId =
         Lens.view
-            (_Unwrapped . field @"attributes" . field @"uniqueId" . _Unwrapped)
-
-    maybeRuleLabel :: RewriteRule VariableName -> Maybe Text
-    maybeRuleLabel =
+            ( _Unwrapped
+            . field @"attributes"
+            . field @"uniqueId"
+            . _Unwrapped
+            )
+    lensLabel =
         Lens.view
-            (_Unwrapped . field @"attributes" . field @"label" . _Unwrapped)
-
-    ruleById rule = do
-        name <- maybeRuleUniqueId rule
-        return (name, rule)
-
-    ruleByLabel rule = do
-        name <- maybeRuleLabel rule
-        return (name, rule)
+            ( _Unwrapped
+            . field @"attributes"
+            . field @"label"
+            . _Unwrapped
+            )
 
-    extractRule registry ruleName =
-        maybe
-            (throwE $ "Rule not found: '" <> ruleName <> "'.")
-            return
-            (Map.lookup ruleName registry)
+data RuleExtractionResult
+    = FoundRule (RewriteRule VariableName)
+    | ErrorRuleNotFound
+    | ErrorDuplicateId [RewriteRule VariableName]
+    | ErrorDuplicateLabel [RewriteRule VariableName]
+    | ErrorIdAndLabelNamesCoincide
+
+getRuleExtractionResult
+    :: [RewriteRule VariableName]
+    -> [RewriteRule VariableName]
+    -> RuleExtractionResult
+getRuleExtractionResult rulesWithId rulesWithLabel =
+    case (rulesWithId, rulesWithLabel) of
+        ([], []) -> ErrorRuleNotFound
+        ([rule], []) -> FoundRule rule
+        ([], [rule]) -> FoundRule rule
+        (rules, []) -> ErrorDuplicateId rules
+        ([], rules) -> ErrorDuplicateLabel rules
+        _ -> ErrorIdAndLabelNamesCoincide
 
 assertSingleClaim :: Monad m => [claim] -> m ()
 assertSingleClaim claims =