Keep table of term replacements in SideCondition, use in term simplifier (#2315)

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,10 @@ import Data.Hashable
     ( Hashed
     , unhashed
     )
+import Data.HashMap.Strict
+    ( HashMap
+    )
+import qualified Data.HashMap.Strict as HashMap
 import Data.Int
 import Data.Map.Strict
     ( Map
@@ -332,6 +336,11 @@ 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)
@@ -592,6 +601,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

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
     (

kore/src/Kore/Equation/Simplification.hs

@@ -37,9 +37,6 @@ import Kore.Internal.Pattern
     )
 import qualified Kore.Internal.Pattern as Pattern
 import qualified Kore.Internal.Predicate as Predicate
-import qualified Kore.Internal.SideCondition as SideCondition
-    ( top
-    )
 import qualified Kore.Internal.Substitution as Substitution
 import qualified Kore.Internal.TermLike as TermLike
 import qualified Kore.Step.Simplification.Pattern as Pattern
@@ -132,6 +129,6 @@ simplifyPattern
     :: (InternalVariable variable, MonadSimplify simplifier)
     => Pattern variable
     -> simplifier (OrPattern variable)
-simplifyPattern patt =
+simplifyPattern =
     Simplifier.localSimplifierAxioms (const mempty)
-    $ Pattern.simplify SideCondition.top patt
+    . Pattern.simplify

kore/src/Kore/Exec.hs

@@ -8,6 +8,8 @@ Portability : portable
 
 Expose concrete execution as a library
 -}
+{-# LANGUAGE Strict #-}
+
 module Kore.Exec
     ( exec
     , mergeAllRules
@@ -92,8 +94,7 @@ import Kore.Internal.Predicate
     , makeMultipleOrPredicate
     )
 import qualified Kore.Internal.SideCondition as SideCondition
-    ( top
-    , topTODO
+    ( topTODO
     )
 import Kore.Internal.TermLike
 import Kore.Log.ErrorRewriteLoop
@@ -224,7 +225,7 @@ exec depthLimit breadthLimit verifiedModule strategy initialTerm =
         finals <-
             getFinalConfigsOf $ do
                 initialConfig <-
-                    Pattern.simplify SideCondition.top
+                    Pattern.simplify
                         (Pattern.fromTermLike initialTerm)
                     >>= Logic.scatter
                 let
@@ -372,7 +373,7 @@ search depthLimit breadthLimit verifiedModule termLike searchPattern searchConfi
         initialized <- initializeAndSimplify verifiedModule
         let Initialized { rewriteRules } = initialized
         simplifiedPatterns <-
-            Pattern.simplify SideCondition.top
+            Pattern.simplify
             $ Pattern.fromTermLike termLike
         let
             initialPattern =