Fix Strict performance (#2447)

* WIP: make evaluation of side condition representation lazy

* WIP fix: best results so far

* Replace undefined

* WIP fix: best performance yet

* Remove useless lazy bindings

* Remove useless lazy bindings

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

Co-authored-by: Thomas Tuegel <[email protected]>

* TermLike.setSimplified: make attributes lazy

* TermLike.TermLike: make call to Attribute.traverseVariables lazy

* Review: make Representation lazy

* Make Attribute.Simplified lazy

* Review: remove redundant

Co-authored-by: Thomas Tuegel <[email protected]>

* Review: make TypeRep strict

Co-authored-by: Thomas Tuegel <[email protected]>

* Make Simplified and SideCondition.SideCondition NoStrict

* Remove redundant lazy bindings

Co-authored-by: Thomas Tuegel <[email protected]>

Author: ana-pantilie

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

@@ -4,7 +4,7 @@ License     : NCSA
 
  -}
 
-{-# LANGUAGE Strict #-}
+{-# LANGUAGE NoStrict #-}
 
 module Kore.Attribute.Pattern.Simplified
     ( Simplified (..)
@@ -100,7 +100,7 @@ data Condition
     = Any
     -- ^ The term and all its subterms are simplified the same regardless
     -- of the side condition.
-    | Condition !SideCondition.Representation
+    | Condition SideCondition.Representation
     -- ^ The term is in its current simplified state only when using the
     -- given side condition. When the side condition changes, e.g. by
     -- adding extra conditions, then we may be able to further simplify the
@@ -134,8 +134,8 @@ instance Monoid Condition where
 
 data SimplifiedData =
     SimplifiedData
-        { sType :: !Type
-        , condition :: !Condition
+        { sType :: Type
+        , condition :: Condition
         }
     deriving (Eq, Ord, Show)
     deriving (GHC.Generic)
@@ -156,7 +156,7 @@ Most patterns are assumed un-simplified until marked otherwise, so the
 simplified status is reset by any substitution under the pattern.
 -}
 data Simplified
-    = Simplified !SimplifiedData
+    = Simplified SimplifiedData
     | NotSimplified
     deriving (Eq, Ord, Show)
     deriving (GHC.Generic)

kore/src/Kore/Internal/Predicate.hs

@@ -1045,8 +1045,24 @@ mapVariables
     => AdjSomeVariableName (variable1 -> variable2)
     -> Predicate variable1
     -> Predicate variable2
-mapVariables adj =
-    either undefined id . makePredicate . TermLike.mapVariables adj . fromPredicate_
+mapVariables adj predicate =
+    let termPredicate =
+            TermLike.mapVariables adj
+            . fromPredicate_
+            $ predicate
+    in
+        either
+            errorMappingVariables
+            id
+            (makePredicate termPredicate)
+  where
+    errorMappingVariables termPredicate =
+        error . show . Pretty.vsep $
+            [ "Error when mapping the variables of predicate:"
+            , Pretty.pretty predicate
+            , "The resulting term is not a predicate:"
+            , Pretty.pretty termPredicate
+            ]
 
 -- |Is the predicate free of the given variables?
 isFreeOf

kore/src/Kore/Internal/SideCondition/SideCondition.hs

@@ -3,6 +3,8 @@ Copyright   : (c) Runtime Verification, 2020
 License     : NCSA
 -}
 
+{-# LANGUAGE NoStrict #-}
+
 module Kore.Internal.SideCondition.SideCondition
     ( Representation
     , mkRepresentation
@@ -34,7 +36,9 @@ import Type.Reflection
     )
 
 data Representation where
-    Representation :: (Ord a, Pretty a) => !(TypeRep a) -> !(Hashed a) -> Representation
+    Representation
+        :: (Ord a, Pretty a)
+        => !(TypeRep a) -> Hashed a -> Representation
 
 instance Eq Representation where
     (==) (Representation typeRep1 hashed1) (Representation typeRep2 hashed2) =

kore/src/Kore/Internal/TermLike/TermLike.hs

@@ -909,8 +909,8 @@ traverseVariables adj termLike =
                 (RenamingT variable1 variable2 m (TermLike variable2))
         ->  RenamingT variable1 variable2 m (TermLike variable2)
     worker (attrs :< termLikeF) = do
-        attrs' <- Attribute.traverseVariables askSomeVariableName attrs
-        let avoiding = freeVariables attrs'
+        ~attrs' <- Attribute.traverseVariables askSomeVariableName attrs
+        let ~avoiding = freeVariables attrs'
         termLikeF' <- case termLikeF of
             VariableF (Const unifiedVariable) -> do
                 unifiedVariable' <- askSomeVariable unifiedVariable