Revert "Revert #2315 (#2385)" (#2389)

This reverts commit 266597e.

Author: ana-pantilie

kore/src/Debug.hs

@@ -1,10 +1,10 @@
-{-# LANGUAGE UndecidableInstances #-}
-
 {- |
 Copyright   : (c) Runtime Verification, 2019
 License     : NCSA
 
  -}
+{-# LANGUAGE Strict               #-}
+{-# LANGUAGE UndecidableInstances #-}
 
 module Debug
     (
@@ -37,6 +37,14 @@ import Data.Hashable
     ( Hashed
     , unhashed
     )
+import Data.HashMap.Strict
+    ( HashMap
+    )
+import qualified Data.HashMap.Strict as HashMap
+import Data.HashSet
+    ( HashSet
+    )
+import qualified Data.HashSet as HashSet
 import Data.Int
 import Data.Map.Strict
     ( Map
@@ -332,11 +340,21 @@ instance (Debug k, Debug a) => Debug (Map.Map k a) where
         (parens (precOut >= 10) . Pretty.sep)
         ["Data.Map.Strict.fromList", debug (Map.toList as)]
 
+instance (Debug k, Debug a) => Debug (HashMap k a) where
+    debugPrec as precOut =
+        (parens (precOut >= 10) . Pretty.sep)
+        ["Data.HashMap.Strict.fromList", debug (HashMap.toList as)]
+
 instance Debug a => Debug (Set a) where
     debugPrec as precOut =
         (parens (precOut >= 10) . Pretty.sep)
         ["Data.Set.fromList", debug (Set.toList as)]
 
+instance Debug a => Debug (HashSet a) where
+    debugPrec as precOut =
+        (parens (precOut >= 10) . Pretty.sep)
+        ["Data.HashSet.fromList", debug (HashSet.toList as)]
+
 instance Debug a => Debug (Seq a) where
     debugPrec as precOut =
         (parens (precOut >= 10) . Pretty.sep)
@@ -592,6 +610,16 @@ instance
         wrapFromList diff' precOut =
             parens (precOut >= 10) $ "Data.Map.Strict.fromList" <+> diff' 10
 
+instance
+    ( Debug key, Debug value, Diff key, Diff value )
+    => Diff (HashMap key value)
+  where
+    diffPrec as bs =
+        fmap wrapFromList $ diffPrec (HashMap.toList as) (HashMap.toList bs)
+      where
+        wrapFromList diff' precOut =
+            parens (precOut >= 10) $ "Data.HashMap.Strict.fromList" <+> diff' 10
+
 instance (Debug a, Debug b, Diff a, Diff b) => Diff (a, b)
 
 instance (Debug a, Diff a) => Diff (Set a) where
@@ -601,6 +629,13 @@ instance (Debug a, Diff a) => Diff (Set a) where
         wrapFromList diff' precOut =
             parens (precOut >= 10) $ "Data.Set.fromList" <+> diff' 10
 
+instance (Debug a, Diff a) => Diff (HashSet a) where
+    diffPrec as bs =
+        fmap wrapFromList $ diffPrec (HashSet.toList as) (HashSet.toList bs)
+      where
+        wrapFromList diff' precOut =
+            parens (precOut >= 10) $ "Data.HashSet.fromList" <+> diff' 10
+
 instance Diff ExitCode
 
 instance (Debug a, Debug b, Diff a, Diff b) => Diff (Either a b)

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

@@ -17,15 +17,11 @@ import Prelude.Kore
 import Control.Error
     ( MaybeT
     )
-import qualified Control.Lens as Lens
-import Control.Monad
-    ( zipWithM
-    )
 import Control.Monad.Reader
     ( MonadReader
     )
 import qualified Control.Monad.Reader as Reader
-import qualified Data.List as List
+import qualified Data.Bifunctor as Bifunctor
 import qualified Data.Map.Strict as Map
 
 import Kore.Attribute.Pattern.FreeVariables
@@ -176,6 +172,8 @@ generalizeMapElement freeVariables' element =
 newBuiltinAssocCommCeilSimplifier
     :: forall normalized simplifier
     .   MonadReader (SideCondition RewritingVariableName) simplifier
+    =>  Ord (Element normalized (TermLike RewritingVariableName))
+    =>  Ord (Value normalized (TermLike RewritingVariableName ))
     =>  MonadSimplify simplifier
     =>  Traversable (Value normalized)
     =>  AcWrapper normalized
@@ -188,116 +186,98 @@ newBuiltinAssocCommCeilSimplifier mkBuiltin mkNotMember =
     CeilSimplifier $ \Ceil { ceilChild } -> do
         let internalAc@InternalAc { builtinAcChild } = ceilChild
         sideCondition <- Reader.ask
-        let normalizedAc
-                :: NormalizedAc normalized Key (TermLike RewritingVariableName)
-            normalizedAc = unwrapAc builtinAcChild
-            NormalizedAc
-                { elementsWithVariables = abstractElements
-                , concreteElements
-                , opaque
-                }
-              = normalizedAc
-
-        let defineOpaquePair
-                :: TermLike RewritingVariableName
-                -> TermLike RewritingVariableName
-                -> MultiAnd (OrCondition RewritingVariableName)
-            defineOpaquePair opaque1 opaque2 =
-                internalAc
-                    { builtinAcChild =
-                        wrapAc
-                        emptyNormalizedAc { opaque = [opaque1, opaque2] }
-                    }
-                & mkBuiltin
-                & makeCeilPredicate
-                -- TODO (thomas.tuegel): Do not mark this simplified.
-                -- Marking here may prevent user-defined axioms from applying.
-                -- At present, we wouldn't apply such an axiom, anyway.
-                & Predicate.markSimplifiedMaybeConditional Nothing
-                & OrCondition.fromPredicate
-                & MultiAnd.singleton
-
-            defineOpaquePairs
-                :: TermLike RewritingVariableName
-                -> [TermLike RewritingVariableName]
-                -> MultiAnd (OrCondition RewritingVariableName)
-            defineOpaquePairs this others =
-                foldMap (defineOpaquePair this) others
-
-            definedOpaquePairs :: MultiAnd (OrCondition RewritingVariableName)
-            definedOpaquePairs =
-                mconcat
-                $ zipWith defineOpaquePairs opaque
-                $ tail $ List.tails opaque
-
-        let abstractKeys, concreteKeys
-                :: [TermLike RewritingVariableName]
-            abstractValues, concreteValues, allValues
-                :: [Value normalized (TermLike RewritingVariableName)]
-            (abstractKeys, abstractValues) =
-                unzip (unwrapElement <$> abstractElements)
-            concreteKeys = from @Key <$> Map.keys concreteElements
-            concreteValues = Map.elems concreteElements
-            allValues = concreteValues <> abstractValues
-
-        let makeEvaluateTerm, defineAbstractKey, defineOpaque
-                :: TermLike RewritingVariableName
-                -> MaybeT simplifier (OrCondition RewritingVariableName)
-            makeEvaluateTerm = makeEvaluateTermCeil sideCondition
-            defineAbstractKey = makeEvaluateTerm
-            defineOpaque = makeEvaluateTerm
-
-            defineValue
-                :: Value normalized (TermLike RewritingVariableName)
-                -> MaybeT
-                    simplifier
-                    (MultiAnd (OrCondition RewritingVariableName))
-            defineValue = foldlM worker mempty
-              where
-                worker multiAnd termLike = do
-                    evaluated <- makeEvaluateTerm termLike
-                    return (multiAnd <> MultiAnd.singleton evaluated)
-
-        TermLike.assertConstructorLikeKeys concreteKeys $ return ()
-
-        -- concreteKeys are defined by assumption
-        definedKeys <- traverse defineAbstractKey abstractKeys
-        definedOpaque <- traverse defineOpaque opaque
-        definedValues <- traverse defineValue allValues
-        -- concreteKeys are distinct by assumption
-        distinctConcreteKeys <-
-            traverse (flip distinctKey concreteKeys) abstractKeys
-        distinctAbstractKeys <-
-            zipWithM distinctKey
-                abstractKeys
-                (tail $ List.tails abstractKeys)
-        let conditions :: MultiAnd (OrCondition RewritingVariableName)
-            conditions =
-                mconcat
-                    [ MultiAnd.make definedKeys
-                    , MultiAnd.make definedOpaque
-                    , mconcat definedValues
-                    , mconcat distinctConcreteKeys
-                    , mconcat distinctAbstractKeys
-                    , foldMap (notMembers normalizedAc) opaque
-                    , definedOpaquePairs
-                    ]
-
+        let symbolicKeys = getSymbolicKeysOfAc builtinAcChild
+            symbolicValues = getSymbolicValuesOfAc builtinAcChild
+            concreteValues = getConcreteValuesOfAc builtinAcChild
+            opaqueElements = opaque . unwrapAc $ builtinAcChild
+        definedKeysAndOpaque <-
+            traverse
+                (makeEvaluateTermCeil sideCondition)
+                (symbolicKeys <> opaqueElements)
+            & fmap MultiAnd.make
+        definedValues <-
+            traverse
+                (defineValue sideCondition)
+                (symbolicValues <> concreteValues)
+            & fmap mconcat
+        definedSubCollections <-
+            definePairWiseElements mkBuiltin mkNotMember internalAc
+            . generatePairWiseElements
+            $ builtinAcChild
+        let conditions =
+                definedKeysAndOpaque
+                <> definedValues
+                <> definedSubCollections
         And.simplifyEvaluatedMultiPredicate sideCondition conditions
   where
+    defineValue
+        :: SideCondition RewritingVariableName
+        -> Value normalized (TermLike RewritingVariableName)
+        -> MaybeT
+            simplifier
+            (MultiAnd (OrCondition RewritingVariableName))
+    defineValue sideCondition = foldlM worker mempty
+      where
+        worker multiAnd termLike = do
+            evaluated <- makeEvaluateTermCeil sideCondition termLike
+            return (multiAnd <> MultiAnd.singleton evaluated)
 
-    distinctKey
-        :: TermLike RewritingVariableName
-        -> [TermLike RewritingVariableName]
-        -> MaybeT simplifier (MultiAnd (OrCondition RewritingVariableName))
-    distinctKey thisKey otherKeys =
-        MultiAnd.make <$> traverse (notEquals thisKey) otherKeys
+definePairWiseElements
+    :: forall normalized simplifier
+    .  MonadSimplify simplifier
+    => MonadReader (SideCondition RewritingVariableName) simplifier
+    => AcWrapper normalized
+    => MkBuiltinAssocComm normalized RewritingVariableName
+    -> MkNotMember normalized RewritingVariableName
+    -> InternalAc Key normalized (TermLike RewritingVariableName)
+    -> PairWiseElements normalized Key (TermLike RewritingVariableName)
+    -> MaybeT simplifier (MultiAnd (OrCondition RewritingVariableName))
+definePairWiseElements mkBuiltin mkNotMember internalAc pairWiseElements = do
+    definedKeyPairs <-
+        traverse
+            distinctKey
+            (symbolicKeyPairs <> symbolicConcreteKeyPairs)
+            & fmap MultiAnd.make
+    let definedElementOpaquePairs =
+            foldMap
+                notMember
+                (symbolicOpaquePairs <> concreteOpaquePairs')
+        definedOpaquePairs =
+            foldMap defineOpaquePair opaquePairs
+    return . fold $
+        [ definedKeyPairs
+        , definedElementOpaquePairs
+        , definedOpaquePairs
+        ]
+  where
+    PairWiseElements
+        { symbolicPairs
+        , opaquePairs
+        , symbolicConcretePairs
+        , symbolicOpaquePairs
+        , concreteOpaquePairs
+        } = pairWiseElements
+    symbolicKeyPairs =
+        Bifunctor.bimap
+            (fst . unwrapElement)
+            (fst . unwrapElement)
+        <$> symbolicPairs
+    symbolicConcreteKeyPairs =
+        Bifunctor.bimap
+            (fst . unwrapElement)
+            (from @Key @(TermLike _) . fst)
+        <$> symbolicConcretePairs
+    concreteOpaquePairs' =
+        Bifunctor.first
+            wrapConcreteElement
+        <$> concreteOpaquePairs
 
-    notEquals
-        :: TermLike RewritingVariableName
-        -> TermLike RewritingVariableName
+    distinctKey
+        :: ( TermLike RewritingVariableName
+           , TermLike RewritingVariableName
+           )
         -> MaybeT simplifier (OrCondition RewritingVariableName)
-    notEquals t1 t2 = do
+    distinctKey (t1, t2) = do
         sideCondition <- Reader.ask
         Equals.makeEvaluateTermsToPredicate tMin tMax sideCondition
             >>= Not.simplifyEvaluatedPredicate
@@ -306,42 +286,39 @@ newBuiltinAssocCommCeilSimplifier mkBuiltin mkNotMember =
         (tMin, tMax) = minMax t1 t2
 
     notMember
-        :: TermLike RewritingVariableName
-        -> Element normalized (TermLike RewritingVariableName)
+        :: ( Element normalized (TermLike RewritingVariableName)
+           , TermLike RewritingVariableName
+           )
         -> MultiAnd (OrCondition RewritingVariableName)
-    notMember termLike element =
+    notMember (element, termLike) =
         mkNotMember element termLike
         & OrCondition.fromPredicate
         & MultiAnd.singleton
 
-    notMembers
-        :: NormalizedAc normalized Key (TermLike RewritingVariableName)
-        -> TermLike RewritingVariableName
+    defineOpaquePair
+        :: ( TermLike RewritingVariableName
+           , TermLike RewritingVariableName
+           )
         -> MultiAnd (OrCondition RewritingVariableName)
-    notMembers normalizedAc termLike =
-        Lens.foldMapOf foldElements (notMember termLike) normalizedAc
-
-foldElements
-    ::  AcWrapper collection
-    =>  InternalVariable variable
-    =>  Lens.Fold
-            (NormalizedAc collection Key (TermLike variable))
-            (Element collection (TermLike variable))
-foldElements =
-    Lens.folding $ \normalizedAc ->
-        let
-            concreteElements' =
-                concreteElements normalizedAc
-                & Map.toList
-                & map wrapConcreteElement
-            symbolicElements' = elementsWithVariables normalizedAc
-        in
-            concreteElements' <> symbolicElements'
+    defineOpaquePair (opaque1, opaque2) =
+        internalAc
+            { builtinAcChild =
+                wrapAc
+                emptyNormalizedAc { opaque = [opaque1, opaque2] }
+            }
+        & mkBuiltin
+        & makeCeilPredicate
+        -- TODO (thomas.tuegel): Do not mark this simplified.
+        -- Marking here may prevent user-defined axioms from applying.
+        -- At present, we wouldn't apply such an axiom, anyway.
+        & Predicate.markSimplifiedMaybeConditional Nothing
+        & OrCondition.fromPredicate
+        & MultiAnd.singleton
 
 fromElement
     :: AcWrapper normalized
-    => Element normalized (TermLike variable)
-    -> NormalizedAc normalized Key (TermLike variable)
+    => Element normalized (TermLike RewritingVariableName)
+    -> NormalizedAc normalized Key (TermLike RewritingVariableName)
 fromElement element
   | Just concreteKey <- retractKey symbolicKey
   = emptyNormalizedAc { concreteElements = Map.singleton concreteKey value }

kore/src/Kore/Debug.hs

@@ -1,5 +1,3 @@
-{-# OPTIONS_GHC -Wno-unused-top-binds    #-}
-
 {- |
 Copyright   : (c) Runtime Verification, 2018
 License     : NCSA
@@ -41,6 +39,8 @@ It also works for test error messages:
 
 Enjoy.
 -}
+{-# OPTIONS_GHC -Wno-unused-top-binds    #-}
+{-# LANGUAGE Strict #-}
 
 module Kore.Debug
     (