Revert PRs related to InternalAc, Unit, Element & Concat symbols changes (#2463)

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

This reverts commit 4195d94.

* Revert "Use unit and element symbol attributes"

This reverts commit abf0292.

* Materialize Nix expressions

* removed issue-2095 tests

Co-authored-by: MirceaS <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>

Author: MirceaS

kore/kore.cabal

@@ -4,7 +4,7 @@ cabal-version: 2.2
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: e1fb37a3896c7ce0fd031723af0b1589be0df0d9b5f958befbe74dbbfdee231f
+-- hash: 2efec6a0024031e0d72609be302ec5298405ab977cfd1fac26ad002a0327ef18
 
 name:           kore
 version:        0.41.0.0
@@ -70,9 +70,7 @@ library
       Kore.Attribute.Axiom.Symbolic
       Kore.Attribute.Axiom.Unit
       Kore.Attribute.Comm
-      Kore.Attribute.Concat
       Kore.Attribute.Constructor
-      Kore.Attribute.Element
       Kore.Attribute.Function
       Kore.Attribute.Functional
       Kore.Attribute.Hook
@@ -103,9 +101,12 @@ library
       Kore.Attribute.Smtlib.Smthook
       Kore.Attribute.Smtlib.Smtlib
       Kore.Attribute.Sort
+      Kore.Attribute.Sort.Concat
       Kore.Attribute.Sort.Constructors
       Kore.Attribute.Sort.ConstructorsBuilder
+      Kore.Attribute.Sort.Element
       Kore.Attribute.Sort.HasDomainValues
+      Kore.Attribute.Sort.Unit
       Kore.Attribute.SortInjection
       Kore.Attribute.Source
       Kore.Attribute.SourceLocation
@@ -119,7 +120,6 @@ library
       Kore.Attribute.Synthetic
       Kore.Attribute.Trusted
       Kore.Attribute.UniqueId
-      Kore.Attribute.Unit
       Kore.BugReport
       Kore.Builtin
       Kore.Builtin.AssocComm.AssocComm
@@ -915,6 +915,7 @@ test-suite kore-test
       Test.Kore.Attribute.Smtlib
       Test.Kore.Attribute.Sort.ConstructorsBuilder
       Test.Kore.Attribute.Sort.HasDomainValues
+      Test.Kore.Attribute.Sort.Unit
       Test.Kore.Attribute.SortInjection
       Test.Kore.Attribute.Subsort
       Test.Kore.Attribute.Symbol
@@ -925,7 +926,6 @@ test-suite kore-test
       Test.Kore.Attribute.Symbol.SymbolKywd
       Test.Kore.Attribute.Trusted
       Test.Kore.Attribute.UniqueId
-      Test.Kore.Attribute.Unit
       Test.Kore.BugReport
       Test.Kore.Builtin
       Test.Kore.Builtin.AssocComm.CeilSimplifier

kore/src/Kore/Attribute/Concat.hs

@@ -18,29 +18,29 @@ import Prelude.Kore hiding
 import qualified Control.Monad as Monad
 import Data.Generics.Product
 
-import Kore.Attribute.Concat
-import Kore.Attribute.Element
 import Kore.Attribute.Hook
 import Kore.Attribute.Parser hiding
     ( Sort
     )
 import Kore.Attribute.Smtlib.Smtlib
+import Kore.Attribute.Sort.Concat
+import Kore.Attribute.Sort.Element
 import Kore.Attribute.Sort.HasDomainValues
     ( HasDomainValues
     )
-import Kore.Attribute.Unit
+import Kore.Attribute.Sort.Unit
 
 data Sort =
     Sort
         { hook            :: !Hook
         -- ^ The builtin sort hooked to the sort.
         , smtlib          :: !Smtlib
         -- ^ The user-defined translation of the sort for SMT.
-        , unit            :: !(Unit SymbolOrAlias)
+        , unit            :: !Unit
         -- ^ The unit symbol associated with the sort.
-        , element         :: !(Element SymbolOrAlias)
+        , element         :: !Element
         -- ^ The element symbol associated with the sort.
-        , concat          :: !(Concat SymbolOrAlias)
+        , concat          :: !Concat
         -- ^ The concat symbol associated with the sort.
         , hasDomainValues :: !HasDomainValues
         -- ^ whether the sort has domain values
@@ -68,9 +68,9 @@ instance ParseAttributes Sort where
     parseAttribute attr =
         typed @Hook (parseAttribute attr)
         Monad.>=> typed @Smtlib (parseAttribute attr)
-        Monad.>=> typed @(Unit SymbolOrAlias) (parseAttribute attr)
-        Monad.>=> typed @(Element SymbolOrAlias) (parseAttribute attr)
-        Monad.>=> typed @(Concat SymbolOrAlias) (parseAttribute attr)
+        Monad.>=> typed @Unit (parseAttribute attr)
+        Monad.>=> typed @Element (parseAttribute attr)
+        Monad.>=> typed @Concat (parseAttribute attr)
         Monad.>=> typed @HasDomainValues (parseAttribute attr)
 
 instance From Sort Attributes where

kore/src/Kore/Attribute/Element.hs

@@ -0,0 +1,70 @@
+{-|
+Module      : Kore.Attribute.Sort.Concat
+Description : Concat sort attribute
+Copyright   : (c) Runtime Verification, 2019
+License     : NCSA
+Maintainer  : [email protected]
+
+-}
+module Kore.Attribute.Sort.Concat
+    ( Concat (..)
+    , concatId, concatSymbol, concatAttribute
+    ) where
+
+import Prelude.Kore
+
+import Data.Default
+
+import Kore.Attribute.Parser
+
+-- | @Concat@ represents the @concat@ attribute for sorts.
+newtype Concat = Concat { getConcat :: Maybe SymbolOrAlias }
+    deriving (Generic, Eq, Ord, Show)
+
+instance Semigroup Concat where
+    (<>) a@(Concat (Just _)) _ = a
+    (<>) _                     b = b
+
+instance Monoid Concat where
+    mempty = Concat { getConcat = Nothing }
+
+instance Default Concat where
+    def = mempty
+
+instance NFData Concat
+
+instance ParseAttributes Concat where
+    parseAttribute = withApplication' parseApplication
+      where
+        parseApplication params args Concat { getConcat }
+          | Just _ <- getConcat = failDuplicate'
+          | otherwise = do
+            getZeroParams params
+            arg <- getOneArgument args
+            symbol <- getSymbolOrAlias arg
+            return Concat { getConcat = Just symbol }
+        withApplication' = withApplication concatId
+        failDuplicate' = failDuplicate concatId
+
+instance From Concat Attributes where
+    from =
+        maybe def toAttribute . getConcat
+      where
+        toAttribute = from @AttributePattern . concatAttribute
+
+-- | Kore identifier representing the @concat@ attribute symbol.
+concatId :: Id
+concatId = "concat"
+
+-- | Kore symbol representing the @concat@ attribute.
+concatSymbol :: SymbolOrAlias
+concatSymbol =
+    SymbolOrAlias
+        { symbolOrAliasConstructor = concatId
+        , symbolOrAliasParams = []
+        }
+
+-- | Kore pattern representing the @concat@ attribute.
+concatAttribute :: SymbolOrAlias -> AttributePattern
+concatAttribute symbol =
+    attributePattern concatSymbol [attributePattern_ symbol]