From de78a487c6c99ff45b18d39754fa63cf03e384a6 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Sun, 26 Jul 2020 13:59:08 -0500 Subject: [PATCH 1/8] mkDefined: Define Set elements --- kore/src/Kore/Internal/TermLike.hs | 3 ++- kore/test/Test/Kore/Internal/TermLike.hs | 6 ++++++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs index fd641f1992..813867ddcb 100644 --- a/kore/src/Kore/Internal/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike.hs @@ -1490,7 +1490,8 @@ mkDefined = updateCallStack . worker BuiltinF (Domain.BuiltinString _) -> term BuiltinF (Domain.BuiltinList _) -> mkDefinedAtTop term BuiltinF (Domain.BuiltinMap _) -> mkDefinedAtTop term - BuiltinF (Domain.BuiltinSet _) -> mkDefinedAtTop term + BuiltinF (Domain.BuiltinSet internalSet) -> + mkDefinedAtTop . mkBuiltinSet $ mkDefined <$> internalSet EqualsF _ -> term ExistsF _ -> mkDefinedAtTop term FloorF _ -> term diff --git a/kore/test/Test/Kore/Internal/TermLike.hs b/kore/test/Test/Kore/Internal/TermLike.hs index 3087ef0aa2..963caae5fa 100644 --- a/kore/test/Test/Kore/Internal/TermLike.hs +++ b/kore/test/Test/Kore/Internal/TermLike.hs @@ -532,6 +532,12 @@ test_mkDefined = ) actual = mkDefined term assertEqual "" expected actual + , testCase "Set" $ do + let fx = Mock.f (mkElemVar Mock.x) + fy = Mock.f (mkElemVar Mock.y) + actual = mkDefined (Mock.builtinSet [fx, fy]) + expect = defined (Mock.builtinSet [defined fx, defined fy]) + assertEqual "" expect actual ] where defined :: TermLike VariableName -> TermLike VariableName From 23ac7141feb168c703b2e2bd270fb9639b5dad19 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Sun, 26 Jul 2020 14:00:30 -0500 Subject: [PATCH 2/8] mkDefined: Define List elements --- kore/src/Kore/Internal/TermLike.hs | 3 ++- kore/test/Test/Kore/Internal/TermLike.hs | 6 ++++++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs index 813867ddcb..ae76a4e5d7 100644 --- a/kore/src/Kore/Internal/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike.hs @@ -1488,7 +1488,8 @@ mkDefined = updateCallStack . worker BuiltinF (Domain.BuiltinBool _) -> term BuiltinF (Domain.BuiltinInt _) -> term BuiltinF (Domain.BuiltinString _) -> term - BuiltinF (Domain.BuiltinList _) -> mkDefinedAtTop term + BuiltinF (Domain.BuiltinList internalList) -> + mkDefinedAtTop . mkBuiltinList $ mkDefined <$> internalList BuiltinF (Domain.BuiltinMap _) -> mkDefinedAtTop term BuiltinF (Domain.BuiltinSet internalSet) -> mkDefinedAtTop . mkBuiltinSet $ mkDefined <$> internalSet diff --git a/kore/test/Test/Kore/Internal/TermLike.hs b/kore/test/Test/Kore/Internal/TermLike.hs index 963caae5fa..a8838c63d9 100644 --- a/kore/test/Test/Kore/Internal/TermLike.hs +++ b/kore/test/Test/Kore/Internal/TermLike.hs @@ -532,6 +532,12 @@ 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 = defined (Mock.builtinList [defined fx, defined fy]) + assertEqual "" expect actual , testCase "Set" $ do let fx = Mock.f (mkElemVar Mock.x) fy = Mock.f (mkElemVar Mock.y) From 61c1e03110ab09bc7e8645c4e0cc86c4050c161f Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Sun, 26 Jul 2020 14:13:48 -0500 Subject: [PATCH 3/8] mkDefined: Define Map elements --- kore/src/Kore/Internal/TermLike.hs | 3 ++- kore/test/Test/Kore/Internal/TermLike.hs | 10 ++++++++++ 2 files changed, 12 insertions(+), 1 deletion(-) diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs index ae76a4e5d7..8f9cd5ddd6 100644 --- a/kore/src/Kore/Internal/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike.hs @@ -1490,7 +1490,8 @@ mkDefined = updateCallStack . worker BuiltinF (Domain.BuiltinString _) -> term BuiltinF (Domain.BuiltinList internalList) -> mkDefinedAtTop . mkBuiltinList $ mkDefined <$> internalList - BuiltinF (Domain.BuiltinMap _) -> mkDefinedAtTop term + BuiltinF (Domain.BuiltinMap internalMap) -> + mkDefinedAtTop . mkBuiltinMap $ mkDefined <$> internalMap BuiltinF (Domain.BuiltinSet internalSet) -> mkDefinedAtTop . mkBuiltinSet $ mkDefined <$> internalSet EqualsF _ -> term diff --git a/kore/test/Test/Kore/Internal/TermLike.hs b/kore/test/Test/Kore/Internal/TermLike.hs index a8838c63d9..3acf1093b8 100644 --- a/kore/test/Test/Kore/Internal/TermLike.hs +++ b/kore/test/Test/Kore/Internal/TermLike.hs @@ -544,6 +544,16 @@ test_mkDefined = actual = mkDefined (Mock.builtinSet [fx, fy]) expect = defined (Mock.builtinSet [defined fx, defined fy]) assertEqual "" expect actual + , testCase "Map" $ do + let fx = Mock.f (mkElemVar Mock.x) + fy = Mock.f (mkElemVar Mock.y) + fa = Mock.f Mock.a + defx = defined fx + defy = defined fy + defa = defined fa + actual = mkDefined (Mock.builtinMap [(fx, fx), (fa, fy)]) + expect = defined (Mock.builtinMap [(defx, defx), (defa, defy)]) + assertEqual "" expect actual ] where defined :: TermLike VariableName -> TermLike VariableName From 33d6505e5ccba2f9227c357aed463ec9d71b8e9d Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Sat, 25 Jul 2020 20:21:13 -0500 Subject: [PATCH 4/8] framedMap and framedSet only create valid test inputs --- .../Kore/Attribute/Pattern/ConstructorLike.hs | 7 ---- kore/test/Test/Kore/Step/MockSymbols.hs | 38 +++++++++++++++++-- 2 files changed, 35 insertions(+), 10 deletions(-) diff --git a/kore/test/Test/Kore/Attribute/Pattern/ConstructorLike.hs b/kore/test/Test/Kore/Attribute/Pattern/ConstructorLike.hs index 55289888ec..0d3389ec99 100644 --- a/kore/test/Test/Kore/Attribute/Pattern/ConstructorLike.hs +++ b/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 diff --git a/kore/test/Test/Kore/Step/MockSymbols.hs b/kore/test/Test/Kore/Step/MockSymbols.hs index 0781aec137..cb14a21034 100644 --- a/kore/test/Test/Kore/Step/MockSymbols.hs +++ b/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 From 6fcecd31466ecfab4c6364851989b7d866d274c3 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 27 Jul 2020 10:32:27 -0500 Subject: [PATCH 5/8] mkDefined: Define opaque Map and Set terms --- kore/src/Kore/Internal/TermLike.hs | 25 +++++++- kore/test/Test/Kore/Internal/TermLike.hs | 82 +++++++++++++++++++++--- 2 files changed, 95 insertions(+), 12 deletions(-) diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs index 8f9cd5ddd6..57c230d627 100644 --- a/kore/src/Kore/Internal/TermLike.hs +++ b/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 (..) @@ -1491,9 +1495,11 @@ mkDefined = updateCallStack . worker BuiltinF (Domain.BuiltinList internalList) -> mkDefinedAtTop . mkBuiltinList $ mkDefined <$> internalList BuiltinF (Domain.BuiltinMap internalMap) -> - mkDefinedAtTop . mkBuiltinMap $ mkDefined <$> internalMap + mkDefinedAtTop . mkBuiltinMap + $ mkDefinedInternalAc internalMap BuiltinF (Domain.BuiltinSet internalSet) -> - mkDefinedAtTop . mkBuiltinSet $ mkDefined <$> internalSet + mkDefinedAtTop . mkBuiltinSet + $ mkDefinedInternalAc internalSet EqualsF _ -> term ExistsF _ -> mkDefinedAtTop term FloorF _ -> term @@ -1526,6 +1532,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 = + Map.map (fmap mkDefined) + . Map.mapKeys mkDefined + mkDefinedAbstract = map (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 diff --git a/kore/test/Test/Kore/Internal/TermLike.hs b/kore/test/Test/Kore/Internal/TermLike.hs index 3acf1093b8..f9fb27a788 100644 --- a/kore/test/Test/Kore/Internal/TermLike.hs +++ b/kore/test/Test/Kore/Internal/TermLike.hs @@ -536,24 +536,86 @@ test_mkDefined = let fx = Mock.f (mkElemVar Mock.x) fy = Mock.f (mkElemVar Mock.y) actual = mkDefined (Mock.builtinList [fx, fy]) - expect = defined (Mock.builtinList [defined fx, defined fy]) + expect = Mock.builtinList [defined fx, defined fy] assertEqual "" expect actual - , testCase "Set" $ do + , testGroup "Set" $ let fx = Mock.f (mkElemVar Mock.x) - fy = Mock.f (mkElemVar Mock.y) - actual = mkDefined (Mock.builtinSet [fx, fy]) - expect = defined (Mock.builtinSet [defined fx, defined fy]) - assertEqual "" expect actual - , testCase "Map" $ do + fa = Mock.f Mock.a + opaque = Mock.opaqueSet Mock.a + defx = defined fx + defa = defined fa + defOpaque = defined opaque + in + [ testCase "a 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 "f(a)" $ do + let actual = mkDefined (Mock.builtinSet [fa]) + expect = defined (Mock.builtinSet [defa]) + assertEqual "" expect actual + , testCase "f(x)" $ do + let actual = mkDefined (Mock.builtinSet [fx]) + expect = defined (Mock.builtinSet [defx]) + assertEqual "" expect actual + , testCase "a opaque(a)" $ do + let actual = mkDefined (Mock.framedSet [Mock.a] [opaque]) + expect = defined (Mock.framedSet [Mock.a] [defOpaque]) + assertEqual "" expect actual + ] + , 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 - actual = mkDefined (Mock.builtinMap [(fx, fx), (fa, fy)]) - expect = defined (Mock.builtinMap [(defx, defx), (defa, defy)]) - assertEqual "" expect actual + 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 = defined (Mock.builtinMap [(defa, Mock.a)]) + assertEqual "" expect actual + , testCase "f(x) |-> a" $ do + let actual = mkDefined (Mock.builtinMap [(fx, Mock.a)]) + expect = defined (Mock.builtinMap [(defx, Mock.a)]) + assertEqual "" expect actual + , testCase "a |-> f(a)" $ do + let actual = mkDefined (Mock.builtinMap [(Mock.a, fa)]) + expect = defined (Mock.builtinMap [(Mock.a, defa)]) + assertEqual "" expect actual + , testCase "a |-> f(y)" $ do + let actual = mkDefined (Mock.builtinMap [(Mock.a, fy)]) + expect = defined (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 + ] ] where defined :: TermLike VariableName -> TermLike VariableName From 705e4bea8243c819d26b366f84f3900323b0e456 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 27 Jul 2020 10:38:04 -0500 Subject: [PATCH 6/8] mkDefined: No need to define List at the top --- kore/src/Kore/Internal/TermLike.hs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs index 57c230d627..8181936d08 100644 --- a/kore/src/Kore/Internal/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike.hs @@ -1493,7 +1493,9 @@ mkDefined = updateCallStack . worker BuiltinF (Domain.BuiltinInt _) -> term BuiltinF (Domain.BuiltinString _) -> term BuiltinF (Domain.BuiltinList internalList) -> - mkDefinedAtTop . mkBuiltinList $ mkDefined <$> internalList + -- mkDefinedAtTop is not needed because the list is always + -- defined if its elements are all defined. + mkBuiltinList $ mkDefined <$> internalList BuiltinF (Domain.BuiltinMap internalMap) -> mkDefinedAtTop . mkBuiltinMap $ mkDefinedInternalAc internalMap From 7c9b31b35973840e4caacd4368e1f9284b14d722 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Mon, 27 Jul 2020 12:03:05 -0500 Subject: [PATCH 7/8] mkDefined: Omit redundant markers on Map and Set --- kore/src/Kore/Internal/TermLike.hs | 19 +++++++++---------- kore/test/Test/Kore/Internal/TermLike.hs | 20 ++++++++++++++------ 2 files changed, 23 insertions(+), 16 deletions(-) diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs index 8181936d08..54fdab3d8a 100644 --- a/kore/src/Kore/Internal/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike.hs @@ -1454,6 +1454,10 @@ mkDefined -> TermLike variable mkDefined = updateCallStack . worker where + mkDefined1 term + | isDefinedPattern term = term + | otherwise = mkDefinedAtTop term + worker :: TermLike variable -> TermLike variable @@ -1473,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 _ -> @@ -1497,10 +1496,10 @@ mkDefined = updateCallStack . worker -- defined if its elements are all defined. mkBuiltinList $ mkDefined <$> internalList BuiltinF (Domain.BuiltinMap internalMap) -> - mkDefinedAtTop . mkBuiltinMap + mkDefined1 . mkBuiltinMap $ mkDefinedInternalAc internalMap BuiltinF (Domain.BuiltinSet internalSet) -> - mkDefinedAtTop . mkBuiltinSet + mkDefined1 . mkBuiltinSet $ mkDefinedInternalAc internalSet EqualsF _ -> term ExistsF _ -> mkDefinedAtTop term diff --git a/kore/test/Test/Kore/Internal/TermLike.hs b/kore/test/Test/Kore/Internal/TermLike.hs index f9fb27a788..7eedf52370 100644 --- a/kore/test/Test/Kore/Internal/TermLike.hs +++ b/kore/test/Test/Kore/Internal/TermLike.hs @@ -557,16 +557,20 @@ test_mkDefined = assertEqual "" expect actual , testCase "f(a)" $ do let actual = mkDefined (Mock.builtinSet [fa]) - expect = defined (Mock.builtinSet [defa]) + expect = Mock.builtinSet [defa] assertEqual "" expect actual , testCase "f(x)" $ do let actual = mkDefined (Mock.builtinSet [fx]) - expect = defined (Mock.builtinSet [defx]) + expect = Mock.builtinSet [defx] assertEqual "" expect actual , testCase "a 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) @@ -595,19 +599,19 @@ test_mkDefined = assertEqual "" expect actual , testCase "f(a) |-> a" $ do let actual = mkDefined (Mock.builtinMap [(fa, Mock.a)]) - expect = defined (Mock.builtinMap [(defa, 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 = defined (Mock.builtinMap [(defx, 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 = defined (Mock.builtinMap [(Mock.a, defa)]) + expect = Mock.builtinMap [(Mock.a, defa)] assertEqual "" expect actual , testCase "a |-> f(y)" $ do let actual = mkDefined (Mock.builtinMap [(Mock.a, fy)]) - expect = defined (Mock.builtinMap [(Mock.a, defy)]) + expect = Mock.builtinMap [(Mock.a, defy)] assertEqual "" expect actual , testCase "a |-> a opaque(a)" $ do let actual = @@ -615,6 +619,10 @@ test_mkDefined = 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 From 36e529298e01934668377879088cb2e2326a111d Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Tue, 28 Jul 2020 11:12:21 +0300 Subject: [PATCH 8/8] Refactoring: subsequent fmaps + test descriptions --- kore/src/Kore/Internal/TermLike.hs | 4 ++-- kore/test/Test/Kore/Internal/TermLike.hs | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs index 54fdab3d8a..963e8ff5da 100644 --- a/kore/src/Kore/Internal/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike.hs @@ -1543,9 +1543,9 @@ mkDefined = updateCallStack . worker >>> Lens.over (field @"opaque") mkDefinedOpaque >>> Domain.wrapAc mkDefinedConcrete = - Map.map (fmap mkDefined) + (fmap . fmap) mkDefined . Map.mapKeys mkDefined - mkDefinedAbstract = map (fmap mkDefined) + mkDefinedAbstract = (fmap . fmap) mkDefined mkDefinedOpaque = map mkDefined -- | Apply the 'Defined' wrapper to the top of any 'TermLike'. diff --git a/kore/test/Test/Kore/Internal/TermLike.hs b/kore/test/Test/Kore/Internal/TermLike.hs index 7eedf52370..76423cbafa 100644 --- a/kore/test/Test/Kore/Internal/TermLike.hs +++ b/kore/test/Test/Kore/Internal/TermLike.hs @@ -546,7 +546,7 @@ test_mkDefined = defa = defined fa defOpaque = defined opaque in - [ testCase "a x" $ do + [ testCase "SetItem(a) SetItem(x)" $ do let actual = Mock.builtinSet [Mock.a, mkElemVar Mock.x] & mkDefined @@ -555,15 +555,15 @@ test_mkDefined = Mock.builtinSet [Mock.a, mkElemVar Mock.x] & defined assertEqual "" expect actual - , testCase "f(a)" $ do + , testCase "SetItem( f(a) )" $ do let actual = mkDefined (Mock.builtinSet [fa]) expect = Mock.builtinSet [defa] assertEqual "" expect actual - , testCase "f(x)" $ do + , testCase "SetItem( f(x) )" $ do let actual = mkDefined (Mock.builtinSet [fx]) expect = Mock.builtinSet [defx] assertEqual "" expect actual - , testCase "a opaque(a)" $ do + , 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