mkDefined: Descend into elements of collections

kore/src/Kore/Internal/TermLike.hs

@@ -181,6 +181,7 @@ module Kore.Internal.TermLike
 
 import Prelude.Kore
 
+import qualified Control.Lens as Lens
 import Data.Align
     ( alignWith
     )
@@ -196,6 +197,9 @@ import Data.Functor.Foldable
     ( Base
     )
 import qualified Data.Functor.Foldable as Recursive
+import Data.Generics.Product
+    ( field
+    )
 import qualified Data.Map.Strict as Map
 import Data.Monoid
     ( Endo (..)
@@ -1450,6 +1454,10 @@ mkDefined
     -> TermLike variable
 mkDefined = updateCallStack . worker
   where
+    mkDefined1 term
+      | isDefinedPattern term = term
+      | otherwise = mkDefinedAtTop term
+
     worker
         :: TermLike variable
         -> TermLike variable
@@ -1469,14 +1477,9 @@ mkDefined = updateCallStack . worker
                         { applicationSymbolOrAlias
                         , applicationChildren
                         } ->
-                    (if isFunctional applicationSymbolOrAlias
-                        then id
-                        else mkDefinedAtTop
-                    )
-                        (mkApplySymbol
-                                    applicationSymbolOrAlias
-                                    (fmap worker applicationChildren)
-                        )
+                    mkDefined1
+                    $ mkApplySymbol applicationSymbolOrAlias
+                    $ fmap worker applicationChildren
                 ApplyAliasF _ ->
                     mkDefinedAtTop term
                 BottomF _ ->
@@ -1488,9 +1491,16 @@ mkDefined = updateCallStack . worker
                 BuiltinF (Domain.BuiltinBool _) -> term
                 BuiltinF (Domain.BuiltinInt _) -> term
                 BuiltinF (Domain.BuiltinString _) -> term
-                BuiltinF (Domain.BuiltinList _) -> mkDefinedAtTop term
-                BuiltinF (Domain.BuiltinMap _) -> mkDefinedAtTop term
-                BuiltinF (Domain.BuiltinSet _) -> mkDefinedAtTop term
+                BuiltinF (Domain.BuiltinList internalList) ->
+                    -- mkDefinedAtTop is not needed because the list is always
+                    -- defined if its elements are all defined.
+                    mkBuiltinList $ mkDefined <$> internalList
+                BuiltinF (Domain.BuiltinMap internalMap) ->
+                    mkDefined1 . mkBuiltinMap
+                    $ mkDefinedInternalAc internalMap
+                BuiltinF (Domain.BuiltinSet internalSet) ->
+                    mkDefined1 . mkBuiltinSet
+                    $ mkDefinedInternalAc internalSet
                 EqualsF _ -> term
                 ExistsF _ -> mkDefinedAtTop term
                 FloorF _ -> term
@@ -1523,6 +1533,21 @@ mkDefined = updateCallStack . worker
                 InhabitantF _ -> mkDefinedAtTop term
                 InternalBytesF _ -> term
 
+    mkDefinedInternalAc internalAc =
+        Lens.over (field @"builtinAcChild") mkDefinedNormalized internalAc
+      where
+        mkDefinedNormalized =
+            Domain.unwrapAc
+            >>> Lens.over (field @"concreteElements") mkDefinedConcrete
+            >>> Lens.over (field @"elementsWithVariables") mkDefinedAbstract
+            >>> Lens.over (field @"opaque") mkDefinedOpaque
+            >>> Domain.wrapAc
+        mkDefinedConcrete =
+            (fmap . fmap) mkDefined
+            . Map.mapKeys mkDefined
+        mkDefinedAbstract = (fmap . fmap) mkDefined
+        mkDefinedOpaque = map mkDefined
+
 -- | Apply the 'Defined' wrapper to the top of any 'TermLike'.
 mkDefinedAtTop :: Ord variable => TermLike variable -> TermLike variable
 mkDefinedAtTop = synthesize . DefinedF . Defined

kore/test/Test/Kore/Attribute/Pattern/ConstructorLike.hs

@@ -25,18 +25,11 @@ test_TermLike =
         Mock.builtinSet [] `shouldBeConstructorLike` True
     , testCase "Simplifiable constructor-like BuiltinSet" $
         Mock.builtinSet [Mock.a, Mock.b] `shouldBeConstructorLike` True
-    , testCase "Simplifiable non-constructor-like BuiltinSet" $
-        assertErrorIO (assertSubstring "" "Expecting constructor-like object") $
-        Mock.builtinSet [Mock.a, Mock.f Mock.b] `shouldBeConstructorLike` False
     , testCase "Simplifiable empty BuiltinMap" $
         Mock.builtinMap [] `shouldBeConstructorLike` True
     , testCase "Simplifiable constructor-like BuiltinMap" $
         Mock.builtinMap [(Mock.a, Mock.c), (Mock.b, Mock.c)]
         `shouldBeConstructorLike` True
-    , testCase "Simplifiable non-constructor-like key BuiltinMap" $
-        assertErrorIO (assertSubstring "" "Expecting constructor-like object") $
-        Mock.builtinMap [(Mock.a, Mock.c), (Mock.f Mock.b, Mock.c)]
-        `shouldBeConstructorLike` False
     , testCase "Simplifiable non-constructor-like BuiltinMap" $
         Mock.builtinMap [(Mock.a, Mock.c), (Mock.b, Mock.f Mock.c)]
         `shouldBeConstructorLike` False

kore/test/Test/Kore/Internal/TermLike.hs

@@ -532,6 +532,98 @@ test_mkDefined =
                 )
             actual = mkDefined term
         assertEqual "" expected actual
+    , testCase "List" $ do
+        let fx = Mock.f (mkElemVar Mock.x)
+            fy = Mock.f (mkElemVar Mock.y)
+            actual = mkDefined (Mock.builtinList [fx, fy])
+            expect = Mock.builtinList [defined fx, defined fy]
+        assertEqual "" expect actual
+    , testGroup "Set" $
+        let fx = Mock.f (mkElemVar Mock.x)
+            fa = Mock.f Mock.a
+            opaque = Mock.opaqueSet Mock.a
+            defx = defined fx
+            defa = defined fa
+            defOpaque = defined opaque
+        in
+            [ testCase "SetItem(a) SetItem(x)" $ do
+                let actual =
+                        Mock.builtinSet [Mock.a, mkElemVar Mock.x]
+                        & mkDefined
+                    expect :: TermLike VariableName
+                    expect =
+                        Mock.builtinSet [Mock.a, mkElemVar Mock.x]
+                        & defined
+                assertEqual "" expect actual
+            , testCase "SetItem( f(a) )" $ do
+                let actual = mkDefined (Mock.builtinSet [fa])
+                    expect = Mock.builtinSet [defa]
+                assertEqual "" expect actual
+            , testCase "SetItem( f(x) )" $ do
+                let actual = mkDefined (Mock.builtinSet [fx])
+                    expect = Mock.builtinSet [defx]
+                assertEqual "" expect actual
+            , testCase "SetItem(a) SetItem( opaque(a) )" $ do
+                let actual = mkDefined (Mock.framedSet [Mock.a] [opaque])
+                    expect = defined (Mock.framedSet [Mock.a] [defOpaque])
+                assertEqual "" expect actual
+            , testCase "same result inside and outside" $ do
+                let defInside = Mock.builtinSet [mkDefined fx]
+                    defOutside = mkDefined $ Mock.builtinSet [fx]
+                assertEqual "" defInside defOutside
+            ]
+    , testGroup "Map" $
+        let fx = Mock.f (mkElemVar Mock.x)
+            fy = Mock.f (mkElemVar Mock.y)
+            fa = Mock.f Mock.a
+            opaque = Mock.opaqueMap Mock.a
+            defx = defined fx
+            defy = defined fy
+            defa = defined fa
+            defOpaque = defined opaque
+        in
+            [ testCase "a |-> a  x |-> b" $ do
+                let actual =
+                        Mock.builtinMap
+                            [ (Mock.a, Mock.a)
+                            , (mkElemVar Mock.x, Mock.b)
+                            ]
+                        & mkDefined
+                    expect :: TermLike VariableName
+                    expect =
+                        Mock.builtinMap
+                            [ (Mock.a, Mock.a)
+                            , (mkElemVar Mock.x, Mock.b)
+                            ]
+                        & defined
+                assertEqual "" expect actual
+            , testCase "f(a) |-> a" $ do
+                let actual = mkDefined (Mock.builtinMap [(fa, Mock.a)])
+                    expect = Mock.builtinMap [(defa, Mock.a)]
+                assertEqual "" expect actual
+            , testCase "f(x) |-> a" $ do
+                let actual = mkDefined (Mock.builtinMap [(fx, Mock.a)])
+                    expect = Mock.builtinMap [(defx, Mock.a)]
+                assertEqual "" expect actual
+            , testCase "a |-> f(a)" $ do
+                let actual = mkDefined (Mock.builtinMap [(Mock.a, fa)])
+                    expect = Mock.builtinMap [(Mock.a, defa)]
+                assertEqual "" expect actual
+            , testCase "a |-> f(y)" $ do
+                let actual = mkDefined (Mock.builtinMap [(Mock.a, fy)])
+                    expect = Mock.builtinMap [(Mock.a, defy)]
+                assertEqual "" expect actual
+            , testCase "a |-> a  opaque(a)" $ do
+                let actual =
+                        mkDefined (Mock.framedMap [(Mock.a, Mock.a)] [opaque])
+                    expect =
+                        defined (Mock.framedMap [(Mock.a, Mock.a)] [defOpaque])
+                assertEqual "" expect actual
+            , testCase "same result inside and outside" $ do
+                let defInside = Mock.builtinMap [(defx, defa)]
+                    defOutside = mkDefined $ Mock.builtinMap [(fx, fa)]
+                assertEqual "" defInside defOutside
+            ]
     ]
   where
     defined :: TermLike VariableName -> TermLike VariableName

kore/test/Test/Kore/Step/MockSymbols.hs

@@ -25,7 +25,10 @@ module Test.Kore.Step.MockSymbols where
 
 import Prelude.Kore
 
+import Test.Tasty
+
 import qualified Control.Lens as Lens
+import qualified Control.Monad as Monad
 import qualified Data.Bifunctor as Bifunctor
 import qualified Data.Default as Default
 import Data.Generics.Product
@@ -41,6 +44,9 @@ import Data.Sup
 import Kore.Attribute.Hook
     ( Hook (..)
     )
+import Kore.Attribute.Pattern.ConstructorLike
+    ( isConstructorLike
+    )
 import qualified Kore.Attribute.Sort as Attribute
 import qualified Kore.Attribute.Sort.Concat as Attribute
 import qualified Kore.Attribute.Sort.Constructors as Attribute
@@ -67,7 +73,8 @@ import Kore.IndexedModule.MetadataTools
 import qualified Kore.IndexedModule.OverloadGraph as OverloadGraph
 import qualified Kore.IndexedModule.SortGraph as SortGraph
 import Kore.Internal.Symbol hiding
-    ( sortInjection
+    ( isConstructorLike
+    , sortInjection
     )
 import Kore.Internal.TermLike
     ( InternalVariable
@@ -112,6 +119,7 @@ import Test.Kore
     ( testId
     )
 import qualified Test.Kore.IndexedModule.MockMetadataTools as Mock
+import Test.Tasty.HUnit.Ext
 
 aId :: Id
 aId = testId "a"
@@ -1718,6 +1726,16 @@ builtinMap
     -> TermLike variable
 builtinMap elements = framedMap elements []
 
+test_builtinMap :: [TestTree]
+test_builtinMap =
+    [ testCase "constructor-like keys" $ do
+        let input = builtinMap [(a, a), (b, b)] :: TermLike VariableName
+        assertBool "" (isConstructorLike input)
+    , testCase "symbolic keys" $ do
+        let input = builtinMap [(f a, a), (f b, b)] :: TermLike VariableName
+        assertBool "" (not $ isConstructorLike input)
+    ]
+
 framedMap
     :: InternalVariable variable
     => [(TermLike variable, TermLike variable)]
@@ -1737,7 +1755,9 @@ framedMap elements opaque =
         }
   where
     asConcrete element@(key, value) =
-        (,) <$> Internal.asConcrete key <*> pure value
+        do
+            Monad.guard (isConstructorLike key)
+            (,) <$> Internal.asConcrete key <*> pure value
         & maybe (Left element) Right
     (abstractElements, Map.fromList -> concreteElements) =
         asConcrete . Bifunctor.second Domain.MapValue <$> elements
@@ -1762,6 +1782,16 @@ builtinSet
     -> TermLike variable
 builtinSet elements = framedSet elements []
 
+test_builtinSet :: [TestTree]
+test_builtinSet =
+    [ testCase "constructor-like keys" $ do
+        let input = builtinSet [a, b] :: TermLike VariableName
+        assertBool "" (isConstructorLike input)
+    , testCase "symbolic keys" $ do
+        let input = builtinSet [f a, f b] :: TermLike VariableName
+        assertBool "" (not $ isConstructorLike input)
+    ]
+
 framedSet
     :: InternalVariable variable
     => [TermLike variable]
@@ -1781,7 +1811,9 @@ framedSet elements opaque =
         }
   where
     asConcrete key =
-        (,) <$> Internal.asConcrete key <*> pure Domain.SetValue
+        do
+            Monad.guard (isConstructorLike key)
+            (,) <$> Internal.asConcrete key <*> pure Domain.SetValue
         & maybe (Left (key, Domain.SetValue)) Right
     (abstractElements, Map.fromList -> concreteElements) =
         asConcrete <$> elements