Removes sort checks for Map and Set during internalization (#2440)

* removing sort checks for Map and Set

* removing unneeded arg from internalize functions

Co-authored-by: Octavian Mircea Sebe <[email protected]>

Author: emarzion

kore/src/Kore/Builtin.hs

@@ -198,6 +198,6 @@ internalize tools =
   where
     internalize1 =
             List.internalize tools
-        .   Map.internalize tools
-        .   Set.internalize tools
+        .   Map.internalize
+        .   Set.internalize
         .   InternalBytes.internalize

kore/src/Kore/Builtin/Map.hs

@@ -52,7 +52,6 @@ import Data.Text
 import Kore.Attribute.Hook
     ( Hook (..)
     )
-import qualified Kore.Attribute.Symbol as Attribute
 import qualified Kore.Builtin.AssociativeCommutative as Ac
 import Kore.Builtin.Attributes
     ( isConstructorModulo_
@@ -485,18 +484,14 @@ internalize subterms.
 
 internalize
     :: InternalVariable variable
-    => SmtMetadataTools Attribute.Symbol
-    -> TermLike variable
+    => TermLike variable
     -> TermLike variable
-internalize tools termLike
-  | fromMaybe False (isMapSort tools sort')
+internalize termLike
   -- Ac.toNormalized is greedy about 'normalizing' opaque terms, we should only
   -- apply it if we know the term head is a constructor-like symbol.
-  , App_ symbol _ <- termLike
+  | App_ symbol _ <- termLike
   , isConstructorModulo_ symbol = Ac.toNormalizedInternalMap termLike
   | otherwise = termLike
-  where
-    sort' = termLikeSort termLike
 
 {- | Simplify the conjunction or equality of two concrete Map domain values.
 

kore/src/Kore/Builtin/Set.hs

@@ -52,9 +52,6 @@ import qualified Data.Set as Set
 import Data.Text
     ( Text
     )
-import qualified Kore.Attribute.Symbol as Attribute
-    ( Symbol
-    )
 import qualified Kore.Builtin.AssociativeCommutative as Ac
 import Kore.Builtin.Attributes
     ( isConstructorModulo_
@@ -482,18 +479,14 @@ internalize subterms.
  -}
 internalize
     :: InternalVariable variable
-    => SmtMetadataTools Attribute.Symbol
-    -> TermLike variable
+    => TermLike variable
     -> TermLike variable
-internalize tools termLike
-  | fromMaybe False (isSetSort tools sort')
+internalize termLike
   -- Ac.toNormalized is greedy about 'normalizing' opaque terms, we should only
   -- apply it if we know the term head is a constructor-like symbol.
-  , App_ symbol _ <- termLike
+  | App_ symbol _ <- termLike
   , isConstructorModulo_ symbol = Ac.toNormalizedInternalSet termLike
   | otherwise = termLike
-  where
-    sort' = termLikeSort termLike
 
 {- | Simplify the conjunction or equality of two concrete Set domain values.