Clean up built-in types

kore/kore.cabal

@@ -174,7 +174,10 @@ library
       Kore.Internal.Condition
       Kore.Internal.Conditional
       Kore.Internal.Inj
+      Kore.Internal.InternalBool
       Kore.Internal.InternalBytes
+      Kore.Internal.InternalInt
+      Kore.Internal.InternalString
       Kore.Internal.MultiAnd
       Kore.Internal.MultiOr
       Kore.Internal.OrCondition
@@ -287,7 +290,10 @@ library
       Kore.Step.Simplification.Inhabitant
       Kore.Step.Simplification.Inj
       Kore.Step.Simplification.InjSimplifier
+      Kore.Step.Simplification.InternalBool
       Kore.Step.Simplification.InternalBytes
+      Kore.Step.Simplification.InternalInt
+      Kore.Step.Simplification.InternalString
       Kore.Step.Simplification.Mu
       Kore.Step.Simplification.Next
       Kore.Step.Simplification.NoConfusion

kore/src/Kore/Attribute/Pattern/ConstructorLike.hs

@@ -186,9 +186,6 @@ instance HasConstructorLike key => Synthetic ConstructorLike (Builtin key)
   where
     synthetic =
         \case
-            BuiltinInt _    -> ConstructorLike . Just $ ConstructorLikeHead
-            BuiltinBool _   -> ConstructorLike . Just $ ConstructorLikeHead
-            BuiltinString _ -> ConstructorLike . Just $ ConstructorLikeHead
             (BuiltinMap InternalAc
                     {builtinAcChild = NormalizedMap builtinMapChild}
                 ) -> normalizedAcConstructorLike builtinMapChild

kore/src/Kore/Attribute/Pattern/Defined.hs

@@ -6,6 +6,7 @@ License     : NCSA
 
 module Kore.Attribute.Pattern.Defined
     ( Defined (..)
+    , alwaysDefined
     ) where
 
 import Prelude.Kore
@@ -25,9 +26,6 @@ import Kore.Internal.Inj
     ( Inj
     )
 import qualified Kore.Internal.Inj as Inj
-import Kore.Internal.InternalBytes
-    ( InternalBytes
-    )
 import qualified Kore.Internal.Symbol as Internal
 import Kore.Syntax
 
@@ -41,6 +39,9 @@ newtype Defined = Defined { isDefined :: Bool }
     deriving anyclass (Debug, Diff)
     deriving (Semigroup, Monoid) via All
 
+alwaysDefined :: a -> Defined
+alwaysDefined = const (Defined True)
+
 instance Synthetic Defined (And sort) where
     synthetic = const (Defined False)
     {-# INLINE synthetic #-}
@@ -166,31 +167,26 @@ normalizedAcDefined ac@(NormalizedAc _ _ _) =
   where
     sameAsChildren = fold ac
 
-
 -- | A 'Top' pattern is always 'Defined'.
 instance Synthetic Defined (Top sort) where
-    synthetic = const (Defined True)
+    synthetic = alwaysDefined
     {-# INLINE synthetic #-}
 
 -- | A 'StringLiteral' pattern is always 'Defined'.
 instance Synthetic Defined (Const StringLiteral) where
-    synthetic = const (Defined True)
-    {-# INLINE synthetic #-}
-
--- | A 'Bytes' pattern is always 'Defined'.
-instance Synthetic Defined (Const InternalBytes) where
-    synthetic = const (Defined True)
+    synthetic = alwaysDefined
     {-# INLINE synthetic #-}
 
 -- | An 'Inhabitant' pattern is always 'Defined'.
 instance Synthetic Defined Inhabitant where
-    synthetic = const (Defined True)
+    synthetic = alwaysDefined
     {-# INLINE synthetic #-}
 
 -- | An element variable pattern is always 'Defined'.
 --   A set variable is not.
 instance Synthetic Defined (Const (SomeVariable variable)) where
-    synthetic (Const unifiedVariable)= Defined (isElementVariable unifiedVariable)
+    synthetic (Const unifiedVariable) =
+        Defined (isElementVariable unifiedVariable)
     {-# INLINE synthetic #-}
 
 instance Synthetic Defined Inj where

kore/src/Kore/Attribute/Pattern/Function.hs

@@ -6,6 +6,7 @@ License     : NCSA
 
 module Kore.Attribute.Pattern.Function
     ( Function (..)
+    , alwaysFunction
     ) where
 
 import Prelude.Kore
@@ -24,9 +25,6 @@ import Kore.Internal.Inj
     ( Inj
     )
 import qualified Kore.Internal.Inj as Inj
-import Kore.Internal.InternalBytes
-    ( InternalBytes
-    )
 import qualified Kore.Internal.Symbol as Internal
 import Kore.Syntax
 
@@ -40,6 +38,10 @@ newtype Function = Function { isFunction :: Bool }
     deriving anyclass (Debug, Diff)
     deriving (Semigroup, Monoid) via All
 
+alwaysFunction :: a -> Function
+alwaysFunction = const (Function True)
+{-# INLINE alwaysFunction #-}
+
 instance Synthetic Function (And sort) where
     -- TODO (thomas.tuegel):
     -- synthetic = getAny . Foldable.foldMap (Any . isFunction)
@@ -139,11 +141,6 @@ instance Synthetic Function (Const StringLiteral) where
     synthetic = const (Function True)
     {-# INLINE synthetic #-}
 
--- | A 'Bytes' pattern is always 'Function'.
-instance Synthetic Function (Const InternalBytes) where
-    synthetic = const (Function True)
-    {-# INLINE synthetic #-}
-
 -- | An 'Inhabitant' pattern is never 'Function'.
 instance Synthetic Function Inhabitant where
     synthetic = const (Function False)

kore/src/Kore/Attribute/Pattern/Functional.hs

@@ -6,6 +6,7 @@ License     : NCSA
 
 module Kore.Attribute.Pattern.Functional
     ( Functional (..)
+    , alwaysFunctional
     ) where
 
 import Prelude.Kore
@@ -25,9 +26,6 @@ import Kore.Internal.Inj
     ( Inj
     )
 import qualified Kore.Internal.Inj as Inj
-import Kore.Internal.InternalBytes
-    ( InternalBytes
-    )
 import qualified Kore.Internal.Symbol as Internal
 import Kore.Syntax
 
@@ -36,18 +34,13 @@ import Kore.Syntax
 newtype Functional = Functional { isFunctional :: Bool }
     deriving (Eq, GHC.Generic, Ord, Show)
     deriving (Semigroup, Monoid) via All
+    deriving anyclass (Hashable, NFData)
+    deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
+    deriving anyclass (Debug, Diff)
 
-instance SOP.Generic Functional
-
-instance SOP.HasDatatypeInfo Functional
-
-instance Debug Functional
-
-instance Diff Functional
-
-instance NFData Functional
-
-instance Hashable Functional
+alwaysFunctional :: a -> Functional
+alwaysFunctional = const (Functional True)
+{-# INLINE alwaysFunctional #-}
 
 instance Synthetic Functional (And sort) where
     synthetic = const (Functional False)
@@ -185,11 +178,6 @@ instance Synthetic Functional (Const StringLiteral) where
     synthetic = const (Functional True)
     {-# INLINE synthetic #-}
 
--- | A 'Bytes' pattern is always 'Functional'.
-instance Synthetic Functional (Const InternalBytes) where
-    synthetic = const (Functional True)
-    {-# INLINE synthetic #-}
-
 -- | An 'Inhabitant' pattern is never 'Functional'.
 instance Synthetic Functional Inhabitant where
     synthetic = const (Functional False)

kore/src/Kore/Attribute/Pattern/Simplified.hs

@@ -13,6 +13,7 @@ module Kore.Attribute.Pattern.Simplified
     , isFullySimplified
     , simplifiedTo
     , fullySimplified
+    , alwaysSimplified
     , simplifiedConditionally
     , simplifiableConditionally
     , unparseTag
@@ -367,9 +368,6 @@ instance Synthetic Simplified (Rewrites sort) where
     {-# INLINE synthetic #-}
 
 instance Synthetic Simplified (Builtin key) where
-    synthetic (BuiltinInt    _) = fullySimplified
-    synthetic (BuiltinBool   _) = fullySimplified
-    synthetic (BuiltinString _) = fullySimplified
     synthetic b@(BuiltinMap    _) = notSimplified b
     synthetic b@(BuiltinList   _) = notSimplified b
     synthetic b@(BuiltinSet    _) = notSimplified b

kore/src/Kore/Builtin/Bool.hs

@@ -13,7 +13,7 @@ module Kore.Builtin.Bool
     , asPattern
     , extractBoolDomainValue
     , parse
-    , unifyBoolValues
+    , unifyBool
     , unifyBoolAnd
     , unifyBoolOr
     , unifyBoolNot
@@ -36,6 +36,7 @@ import Control.Error
     ( MaybeT
     )
 import qualified Control.Monad as Monad
+import Data.Functor.Const
 import qualified Data.HashMap.Strict as HashMap
 import Data.Map.Strict
     ( Map
@@ -44,7 +45,6 @@ import qualified Data.Map.Strict as Map
 import Data.Text
     ( Text
     )
-import qualified Data.Text as Text
 import qualified Text.Megaparsec as Parsec
 import qualified Text.Megaparsec.Char as Parsec
 
@@ -53,8 +53,8 @@ import Kore.Attribute.Hook
     )
 import Kore.Builtin.Bool.Bool
 import qualified Kore.Builtin.Builtin as Builtin
-import qualified Kore.Domain.Builtin as Domain
 import qualified Kore.Error
+import Kore.Internal.InternalBool
 import Kore.Internal.Pattern
     ( Pattern
     )
@@ -122,11 +122,11 @@ patternVerifierHook =
     patternVerifierWorker domainValue =
         case externalChild of
             StringLiteral_ lit -> do
-                builtinBoolValue <- Builtin.parseString parse lit
-                (return . BuiltinF . Domain.BuiltinBool)
-                    Domain.InternalBool
-                        { builtinBoolSort = domainValueSort
-                        , builtinBoolValue
+                internalBoolValue <- Builtin.parseString parse lit
+                (return . InternalBoolF . Const)
+                    InternalBool
+                        { internalBoolSort = domainValueSort
+                        , internalBoolValue
                         }
             _ -> Kore.Error.koreFail "Expected literal string"
       where
@@ -136,15 +136,9 @@ patternVerifierHook =
 -- | get the value from a (possibly encoded) domain value
 extractBoolDomainValue
     :: Text -- ^ error message Context
-    -> Builtin child
-    -> Bool
-extractBoolDomainValue ctx =
-    \case
-        Domain.BuiltinBool Domain.InternalBool { builtinBoolValue } ->
-            builtinBoolValue
-        _ ->
-            Builtin.verifierBug
-            $ Text.unpack ctx ++ ": Bool builtin should be internal"
+    -> TermLike variable
+    -> Maybe Bool
+extractBoolDomainValue _ = matchBool
 
 {- | Parse an integer string literal.
  -}
@@ -171,20 +165,22 @@ builtinFunctions =
     ]
   where
     unaryOperator =
-        Builtin.unaryOperator extractBoolDomainValue asPattern
+        Builtin.unaryOperator' extractBoolDomainValue asPattern
     binaryOperator =
-        Builtin.binaryOperator extractBoolDomainValue asPattern
+        Builtin.binaryOperator' extractBoolDomainValue asPattern
     xor a b = (a && not b) || (not a && b)
     implies a b = not a || b
 
-unifyBoolValues
+{- | Unification of @BOOL.Bool@ values.
+ -}
+unifyBool
     :: forall variable unifier
     .  InternalVariable variable
     => MonadUnify unifier
     => TermLike variable
     -> TermLike variable
     -> MaybeT unifier (Pattern variable)
-unifyBoolValues a b =
+unifyBool a b =
     worker a b <|> worker b a
   where
     worker termLike1 termLike2
@@ -285,8 +281,8 @@ unifyBoolNot unifyChildren a b =
 {- | Match a @BOOL.Bool@ builtin value.
  -}
 matchBool :: TermLike variable -> Maybe Bool
-matchBool (BuiltinBool_ Domain.InternalBool { builtinBoolValue }) =
-    Just builtinBoolValue
+matchBool (InternalBool_ InternalBool { internalBoolValue }) =
+    Just internalBoolValue
 matchBool _ = Nothing
 
 {- | The @BOOL.and@ hooked symbol applied to @term@-type arguments.

kore/src/Kore/Builtin/Bool/Bool.hs

@@ -30,21 +30,20 @@ import Data.Text
     ( Text
     )
 
-import qualified Kore.Domain.Builtin as Domain
+import Kore.Internal.InternalBool
 import Kore.Internal.Pattern
     ( Pattern
     )
 import qualified Kore.Internal.Pattern as Pattern
     ( fromTermLike
     )
 import Kore.Internal.TermLike
-    ( Concrete
-    , DomainValue (DomainValue)
+    ( DomainValue (DomainValue)
     , InternalVariable
     , Sort
     , TermLike
-    , mkBuiltin
     , mkDomainValue
+    , mkInternalBool
     , mkStringLiteral
     )
 import qualified Kore.Internal.TermLike as TermLike
@@ -71,18 +70,14 @@ asInternal
     -> Bool  -- ^ builtin value to render
     -> TermLike variable
 asInternal builtinBoolSort builtinBoolValue =
-    TermLike.markSimplified . mkBuiltin
+    TermLike.markSimplified . mkInternalBool
     $ asBuiltin builtinBoolSort builtinBoolValue
 
 asBuiltin
     :: Sort  -- ^ resulting sort
     -> Bool  -- ^ builtin value to render
-    -> Domain.Builtin (TermLike Concrete) (TermLike variable)
-asBuiltin builtinBoolSort builtinBoolValue =
-    Domain.BuiltinBool Domain.InternalBool
-        { builtinBoolSort
-        , builtinBoolValue
-        }
+    -> InternalBool
+asBuiltin = InternalBool
 
 {- | Render a 'Bool' as a domain value pattern of the given sort.
 
@@ -94,16 +89,16 @@ asBuiltin builtinBoolSort builtinBoolValue =
  -}
 asTermLike
     :: InternalVariable variable
-    => Domain.InternalBool  -- ^ builtin value to render
+    => InternalBool  -- ^ builtin value to render
     -> TermLike variable
 asTermLike builtin =
     mkDomainValue DomainValue
-        { domainValueSort = builtinBoolSort
+        { domainValueSort = internalBoolSort
         , domainValueChild = mkStringLiteral literal
         }
   where
-    Domain.InternalBool { builtinBoolSort } = builtin
-    Domain.InternalBool { builtinBoolValue = bool } = builtin
+    InternalBool { internalBoolSort } = builtin
+    InternalBool { internalBoolValue = bool } = builtin
     literal
       | bool      = "true"
       | otherwise = "false"