Fix uninterpreted functions in keys of Maps and Sets (#2323)

* Prelude.Kore: Export NFData

* Kore.Step.Function.Memo: Rename Key to CacheKey

* From: Add into

* Add instance From [a] (Seq a)

* Add Kore.Internal.Key

* InternalBytes: Rename fields for uniformity

* test: make golden

Co-authored-by: ttuegel <[email protected]>
Co-authored-by: ana-pantilie <[email protected]>

Author: ttuegel

kore/kore.cabal

@@ -4,7 +4,7 @@ cabal-version: 2.2
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 3a3209955e7db4f112e2b2c2ab073b1d479448d68f21f84c4a14ce8f5f2293d9
+-- hash: 1eb807e1a58c0a657f51fd08934c8a7e171988a07bcd9e0e4c098055595b6ac4
 
 name:           kore
 version:        0.38.0.0
@@ -183,6 +183,7 @@ library
       Kore.Internal.InternalMap
       Kore.Internal.InternalSet
       Kore.Internal.InternalString
+      Kore.Internal.Key
       Kore.Internal.MultiAnd
       Kore.Internal.MultiOr
       Kore.Internal.NormalizedAc
@@ -962,6 +963,7 @@ test-suite kore-test
       Test.Kore.IndexedModule.SortGraph
       Test.Kore.Internal.ApplicationSorts
       Test.Kore.Internal.Condition
+      Test.Kore.Internal.Key
       Test.Kore.Internal.MultiAnd
       Test.Kore.Internal.OrCondition
       Test.Kore.Internal.OrPattern

kore/src/Data/Sup.hs

@@ -13,9 +13,6 @@ module Data.Sup
 
 import Prelude.Kore
 
-import Control.DeepSeq
-    ( NFData
-    )
 import Data.Data
     ( Data
     )

kore/src/From.hs

@@ -6,8 +6,13 @@ License     : NCSA
 
 module From
     ( From (..)
+    , into
     ) where
 
+import Data.Sequence
+    ( Seq
+    )
+import qualified Data.Sequence as Seq
 import Data.Void
 
 {- | Convert type @from@ into @to@.
@@ -43,8 +48,17 @@ let b = let a :: A = _ in from @_ @B a
 class From from to where
     from :: from -> to
 
+{- | @into@ is 'from' with the type parameters in reverse order.
+ -}
+into :: forall to from. From from to => from -> to
+into = from @from @to
+
 {- | This instance implements the principle /ex falso quodlibet/.
  -}
 instance From Void any where
     from = absurd
     {-# INLINE from #-}
+
+instance From [a] (Seq a) where
+    from = Seq.fromList
+    {-# INLINE from #-}

kore/src/Kore/Attribute/Attributes.hs

@@ -17,9 +17,6 @@ module Kore.Attribute.Attributes
 
 import Prelude.Kore
 
-import Control.DeepSeq
-    ( NFData
-    )
 import Data.Default
     ( Default (..)
     )

kore/src/Kore/Attribute/Axiom.hs

@@ -37,9 +37,6 @@ module Kore.Attribute.Axiom
 
 import Prelude.Kore
 
-import Control.DeepSeq
-    ( NFData
-    )
 import qualified Control.Lens as Lens
 import qualified Control.Monad as Monad
 import Data.Default

kore/src/Kore/Attribute/Null.hs

@@ -21,9 +21,6 @@ module Kore.Attribute.Null
 
 import Prelude.Kore
 
-import Control.DeepSeq
-    ( NFData
-    )
 import Data.Default
 import qualified Generics.SOP as SOP
 import qualified GHC.Generics as GHC

kore/src/Kore/Attribute/Parser.hs

@@ -68,9 +68,6 @@ module Kore.Attribute.Parser
 
 import Prelude.Kore
 
-import Control.DeepSeq
-    ( NFData
-    )
 import Control.Lens
     ( Getter
     , Iso'

kore/src/Kore/Attribute/Pattern.hs

@@ -28,9 +28,6 @@ module Kore.Attribute.Pattern
 
 import Prelude.Kore
 
-import Control.DeepSeq
-    ( NFData
-    )
 import qualified Control.Lens as Lens
 import Data.Generics.Product
 import qualified Generics.SOP as SOP

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

@@ -15,7 +15,6 @@ module Kore.Attribute.Pattern.ConstructorLike
 
 import Prelude.Kore
 
-import Control.DeepSeq
 import qualified Generics.SOP as SOP
 import qualified GHC.Generics as GHC
 

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

@@ -11,7 +11,6 @@ module Kore.Attribute.Pattern.Created
 
 import Prelude.Kore
 
-import Control.DeepSeq
 import qualified Generics.SOP as SOP
 import qualified GHC.Generics as GHC
 import GHC.Stack

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

@@ -13,7 +13,6 @@ module Kore.Attribute.Pattern.Defined
 
 import Prelude.Kore
 
-import Control.DeepSeq
 import Data.Functor.Const
 import Data.Monoid
 import qualified Generics.SOP as SOP

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

@@ -25,7 +25,6 @@ import Prelude.Kore hiding
     ( toList
     )
 
-import Control.DeepSeq
 import Data.Functor.Const
 import Data.Map.Strict
     ( Map

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

@@ -13,7 +13,6 @@ module Kore.Attribute.Pattern.Function
 
 import Prelude.Kore
 
-import Control.DeepSeq
 import Data.Functor.Const
 import Data.Monoid
 import qualified Generics.SOP as SOP

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

@@ -13,7 +13,6 @@ module Kore.Attribute.Pattern.Functional
 
 import Prelude.Kore
 
-import Control.DeepSeq
 import Data.Functor.Const
 import Data.Monoid
 import qualified Generics.SOP as SOP

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

@@ -24,7 +24,6 @@ module Kore.Attribute.Pattern.Simplified
 
 import Prelude.Kore
 
-import Control.DeepSeq
 import Data.Text
     ( Text
     )

kore/src/Kore/Attribute/PredicatePattern.hs

@@ -23,9 +23,6 @@ module Kore.Attribute.PredicatePattern
 
 import Prelude.Kore
 
-import Control.DeepSeq
-    ( NFData
-    )
 import qualified Control.Lens as Lens
 import Data.Generics.Product
 import qualified Generics.SOP as SOP

kore/src/Kore/Attribute/RuleIndex.hs

@@ -11,9 +11,6 @@ module Kore.Attribute.RuleIndex
 
 import Prelude.Kore
 
-import Control.DeepSeq
-    ( NFData
-    )
 import Data.Default
 import qualified Generics.SOP as SOP
 import qualified GHC.Generics as GHC

kore/src/Kore/Attribute/Smtlib/Smtlib.hs

@@ -15,9 +15,6 @@ module Kore.Attribute.Smtlib.Smtlib
 
 import Prelude.Kore
 
-import Control.DeepSeq
-    ( NFData
-    )
 import Data.Default
     ( Default (..)
     )

kore/src/Kore/Attribute/SourceLocation.hs

@@ -15,9 +15,6 @@ module Kore.Attribute.SourceLocation
 
 import Prelude.Kore
 
-import Control.DeepSeq
-    ( NFData
-    )
 import Control.Monad
     ( (>=>)
     )

kore/src/Kore/Attribute/Symbol.hs

@@ -62,9 +62,6 @@ module Kore.Attribute.Symbol
 
 import Prelude.Kore
 
-import Control.DeepSeq
-    ( NFData
-    )
 import qualified Control.Lens as Lens
 import Control.Monad
     ( (>=>)

kore/src/Kore/Builtin/AssocComm/CeilSimplifier.hs

@@ -32,7 +32,6 @@ import Kore.Attribute.Pattern.FreeVariables
     ( FreeVariables
     )
 import qualified Kore.Attribute.Pattern.FreeVariables as FreeVariables
-import qualified Kore.Builtin.Builtin as Builtin
 import Kore.Internal.InternalMap
 import Kore.Internal.InternalSet
 import Kore.Internal.MultiAnd
@@ -54,12 +53,13 @@ import Kore.Internal.SideCondition
     )
 import Kore.Internal.TermLike
     ( Ceil (..)
-    , Concrete
     , ElementVariable
     , InternalVariable
+    , Key
     , TermLike
     , fromVariableName
     , generatedId
+    , retractKey
     , termLikeSort
     )
 import qualified Kore.Internal.TermLike as TermLike
@@ -76,7 +76,7 @@ import Kore.Variables.Fresh
     )
 
 type BuiltinAssocComm normalized variable =
-    InternalAc (TermLike Concrete) normalized (TermLike variable)
+    InternalAc Key normalized (TermLike variable)
 
 type MkBuiltinAssocComm normalized variable =
     BuiltinAssocComm normalized variable -> TermLike variable
@@ -188,7 +188,8 @@ newBuiltinAssocCommCeilSimplifier mkBuiltin mkNotMember =
     CeilSimplifier $ \Ceil { ceilChild } -> do
         let internalAc@InternalAc { builtinAcChild } = ceilChild
         sideCondition <- Reader.ask
-        let normalizedAc = unwrapAc builtinAcChild
+        let normalizedAc :: NormalizedAc normalized Key (TermLike variable)
+            normalizedAc = unwrapAc builtinAcChild
             NormalizedAc
                 { elementsWithVariables = abstractElements
                 , concreteElements
@@ -234,7 +235,7 @@ newBuiltinAssocCommCeilSimplifier mkBuiltin mkNotMember =
                 :: [Value normalized (TermLike variable)]
             (abstractKeys, abstractValues) =
                 unzip (unwrapElement <$> abstractElements)
-            concreteKeys = TermLike.fromConcrete <$> Map.keys concreteElements
+            concreteKeys = from @Key <$> Map.keys concreteElements
             concreteValues = Map.elems concreteElements
             allValues = concreteValues <> abstractValues
 
@@ -310,7 +311,7 @@ newBuiltinAssocCommCeilSimplifier mkBuiltin mkNotMember =
         & MultiAnd.singleton
 
     notMembers
-        :: NormalizedAc normalized (TermLike Concrete) (TermLike variable)
+        :: NormalizedAc normalized Key (TermLike variable)
         -> TermLike variable
         -> MultiAnd (OrCondition variable)
     notMembers normalizedAc termLike =
@@ -320,7 +321,7 @@ foldElements
     ::  AcWrapper collection
     =>  InternalVariable variable
     =>  Lens.Fold
-            (NormalizedAc collection (TermLike Concrete) (TermLike variable))
+            (NormalizedAc collection Key (TermLike variable))
             (Element collection (TermLike variable))
 foldElements =
     Lens.folding $ \normalizedAc ->
@@ -335,11 +336,10 @@ foldElements =
 
 fromElement
     :: AcWrapper normalized
-    => InternalVariable variable
     => Element normalized (TermLike variable)
-    -> NormalizedAc normalized (TermLike Concrete) (TermLike variable)
+    -> NormalizedAc normalized Key (TermLike variable)
 fromElement element
-  | Just concreteKey <- Builtin.toKey symbolicKey
+  | Just concreteKey <- retractKey symbolicKey
   = emptyNormalizedAc { concreteElements = Map.singleton concreteKey value }
   | otherwise
   = emptyNormalizedAc { elementsWithVariables = [element] }