Use unit and element symbol attributes

kore/kore.cabal

@@ -4,7 +4,7 @@ cabal-version: 2.2
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 2702a5d875e9f185a4aedc5fdcafa951249ccd4ef5edab6f1e96689991c8f13f
+-- hash: 80d27d36f0343e3b6779aa37ed5fccc747fd7c1b66c7b9bd2fb27c1f6a2d6403
 
 name:           kore
 version:        0.41.0.0
@@ -70,7 +70,9 @@ 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
@@ -101,12 +103,9 @@ 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
@@ -120,6 +119,7 @@ library
       Kore.Attribute.Synthetic
       Kore.Attribute.Trusted
       Kore.Attribute.UniqueId
+      Kore.Attribute.Unit
       Kore.BugReport
       Kore.Builtin
       Kore.Builtin.AssocComm.AssocComm
@@ -916,7 +916,6 @@ 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
@@ -927,6 +926,7 @@ 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

@@ -0,0 +1,95 @@
+{-|
+Copyright   : (c) Runtime Verification, 2021
+License     : NCSA
+-}
+
+{-# LANGUAGE Strict #-}
+
+module Kore.Attribute.Concat
+    ( Concat (..)
+    , mergeConcat, toConcat, fromConcat
+    , concatId, concatSymbol, concatAttribute
+    ) where
+
+import Prelude.Kore
+
+import Data.Default
+import qualified Generics.SOP as SOP
+import qualified Pretty
+
+import Kore.Attribute.Parser
+import Kore.Debug
+import Kore.Unparser
+
+-- | @Concat@ represents the @concat@ attribute.
+newtype Concat symbol = Concat { getConcat :: Maybe symbol }
+    deriving (Generic, Eq, Ord, Show)
+    deriving (Foldable, Functor, Traversable)
+    deriving anyclass (Hashable)
+    deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
+    deriving anyclass (Debug, Diff)
+
+mergeConcat
+    :: (Eq symbol , Unparse symbol)
+    => Concat symbol
+    -> Concat symbol
+    -> Concat symbol
+mergeConcat (Concat Nothing) b = b
+mergeConcat a (Concat Nothing) = a
+mergeConcat a@(Concat (Just aSymbol)) (Concat (Just bSymbol))
+      | aSymbol == bSymbol = a
+      | otherwise = (error . show . Pretty.vsep)
+          [ "Concat symbol mismatch error! Found both"
+          , Pretty.indent 4 (unparse aSymbol)
+          , "and"
+          , Pretty.indent 4 (unparse bSymbol)
+          , "inside term. This is a bug."
+          ]
+
+instance Default (Concat symbol) where
+    def = Concat { getConcat = Nothing }
+
+instance NFData symbol => NFData (Concat symbol)
+
+instance ParseAttributes (Concat SymbolOrAlias) 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 SymbolOrAlias) Attributes where
+    from =
+        maybe def toAttribute . getConcat
+      where
+        toAttribute = from @AttributePattern . concatAttribute
+
+toConcat :: symbol -> Concat symbol
+toConcat sym = Concat { getConcat = Just sym }
+
+fromConcat :: HasCallStack => Concat symbol -> symbol
+fromConcat Concat {getConcat = Just sym} = sym
+fromConcat _ = error "There is no concat symbol to extract"
+
+-- | 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]

kore/src/Kore/Attribute/Element.hs

@@ -0,0 +1,95 @@
+{-|
+Copyright   : (c) Runtime Verification, 2021
+License     : NCSA
+-}
+
+{-# LANGUAGE Strict #-}
+
+module Kore.Attribute.Element
+    ( Element (..)
+    , mergeElement, toElement, fromElement
+    , elementId, elementSymbol, elementAttribute
+    ) where
+
+import Prelude.Kore
+
+import Data.Default
+import qualified Generics.SOP as SOP
+import qualified Pretty
+
+import Kore.Attribute.Parser
+import Kore.Debug
+import Kore.Unparser
+
+-- | @Element@ represents the @element@ attribute.
+newtype Element symbol = Element { getElement :: Maybe symbol }
+    deriving (Generic, Eq, Ord, Show)
+    deriving (Foldable, Functor, Traversable)
+    deriving anyclass (Hashable)
+    deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
+    deriving anyclass (Debug, Diff)
+
+mergeElement
+    :: (Eq symbol , Unparse symbol)
+    => Element symbol
+    -> Element symbol
+    -> Element symbol
+mergeElement (Element Nothing) b = b
+mergeElement a (Element Nothing) = a
+mergeElement a@(Element (Just aSymbol)) (Element (Just bSymbol))
+      | aSymbol == bSymbol = a
+      | otherwise = (error . show . Pretty.vsep)
+          [ "Element symbol mismatch error! Found both"
+          , Pretty.indent 4 (unparse aSymbol)
+          , "and"
+          , Pretty.indent 4 (unparse bSymbol)
+          , "inside term. This is a bug."
+          ]
+
+instance Default (Element symbol) where
+    def = Element { getElement = Nothing }
+
+instance NFData symbol => NFData (Element symbol)
+
+-- | Kore identifier representing the @element@ attribute symbol.
+elementId :: Id
+elementId = "element"
+
+-- | Kore symbol representing the @element@ attribute.
+elementSymbol :: SymbolOrAlias
+elementSymbol =
+    SymbolOrAlias
+        { symbolOrAliasConstructor = elementId
+        , symbolOrAliasParams = []
+        }
+
+-- | Kore pattern representing the @element@ attribute.
+elementAttribute :: SymbolOrAlias -> AttributePattern
+elementAttribute symbol =
+    attributePattern elementSymbol [attributePattern_ symbol]
+
+instance ParseAttributes (Element SymbolOrAlias) where
+    parseAttribute = withApplication' parseApplication
+      where
+        parseApplication params args Element { getElement }
+          | Just _ <- getElement = failDuplicate'
+          | otherwise = do
+            getZeroParams params
+            arg <- getOneArgument args
+            symbol <- getSymbolOrAlias arg
+            return Element { getElement = Just symbol }
+        withApplication' = withApplication elementId
+        failDuplicate' = failDuplicate elementId
+
+instance From (Element SymbolOrAlias) Attributes where
+    from =
+        maybe def toAttribute . getElement
+      where
+        toAttribute = from @AttributePattern . elementAttribute
+
+toElement :: symbol -> Element symbol
+toElement sym = Element { getElement = Just sym }
+
+fromElement :: HasCallStack => Element symbol -> symbol
+fromElement Element {getElement = Just sym} = sym
+fromElement _ = error "There is no element symbol to extract"

kore/src/Kore/Attribute/Sort.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.Sort.Unit
+import Kore.Attribute.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
+        , unit            :: !(Unit SymbolOrAlias)
         -- ^ The unit symbol associated with the sort.
-        , element         :: !Element
+        , element         :: !(Element SymbolOrAlias)
         -- ^ The element symbol associated with the sort.
-        , concat          :: !Concat
+        , concat          :: !(Concat SymbolOrAlias)
         -- ^ 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 (parseAttribute attr)
-        Monad.>=> typed @Element (parseAttribute attr)
-        Monad.>=> typed @Concat (parseAttribute attr)
+        Monad.>=> typed @(Unit SymbolOrAlias) (parseAttribute attr)
+        Monad.>=> typed @(Element SymbolOrAlias) (parseAttribute attr)
+        Monad.>=> typed @(Concat SymbolOrAlias) (parseAttribute attr)
         Monad.>=> typed @HasDomainValues (parseAttribute attr)
 
 instance From Sort Attributes where