runtimeverification · ttuegel · Jan 14, 2021 · Aug 27, 2020 · Aug 27, 2020 · Aug 27, 2020
diff --git a/default.nix b/default.nix
@@ -46,6 +46,7 @@ let
         "/*"
         "!/stack.yaml"
         "!/kore"
+        "*.cabal"
       ];
     };
     inherit checkMaterialization;

diff --git a/kore/kore.cabal b/kore/kore.cabal
@@ -4,7 +4,7 @@ cabal-version: 2.2
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 3120f5e24384393d150b1db1b680ac8a0c5d310317b293ba3f29f6848b8c6af7
+-- hash: 14a9c3fb13f5926dbd7132316a785e05c02d496c072bab9f8bd7533b1cbc8d41
 
 name:           kore
 version:        0.37.0.0
@@ -90,6 +90,7 @@ library
       Kore.Attribute.Pattern.Function
       Kore.Attribute.Pattern.Functional
       Kore.Attribute.Pattern.Simplified
+      Kore.Attribute.PredicatePattern
       Kore.Attribute.Priority
       Kore.Attribute.ProductionID
       Kore.Attribute.RuleIndex

diff --git a/kore/src/Kore/Attribute/Pattern.hs b/kore/src/Kore/Attribute/Pattern.hs
@@ -38,9 +38,27 @@ import qualified GHC.Generics as GHC
 
 import Kore.Attribute.Pattern.ConstructorLike
 import Kore.Attribute.Pattern.Created
+    ( Created (..)
+    , hasKnownCreator
+    )
 import Kore.Attribute.Pattern.Defined
-import Kore.Attribute.Pattern.FreeVariables hiding
-    ( freeVariables
+    ( Defined (..)
+    )
+import Kore.Attribute.Pattern.FreeVariables
+    ( FreeVariables
+    , HasFreeVariables
+    , bindVariable
+    , bindVariables
+    , emptyFreeVariables
+    , freeVariable
+    , getFreeElementVariables
+    , isFreeVariable
+    , mapFreeVariables
+    , nullFreeVariables
+    , toList
+    , toNames
+    , toSet
+    , traverseFreeVariables
     )
 import qualified Kore.Attribute.Pattern.FreeVariables as FreeVariables
     ( freeVariables

diff --git a/kore/src/Kore/Attribute/PredicatePattern.hs b/kore/src/Kore/Attribute/PredicatePattern.hs
@@ -0,0 +1,153 @@
+{- |
+Copyright   : (c) Runtime Verification, 2020
+License     : NCSA
+
+ -}
+
+{-# LANGUAGE UndecidableInstances #-}
+
+module Kore.Attribute.PredicatePattern
+    ( PredicatePattern (PredicatePattern, freeVariables)
+    -- simplified is excluded on purpose
+    , simplifiedAttribute
+    , isSimplified
+    , isFullySimplified
+    , setSimplified
+    , mapVariables
+    , traverseVariables
+    , deleteFreeVariable
+    , fromPattern
+    -- * Re-exports
+    , module Kore.Attribute.Pattern.FreeVariables
+    ) where
+
+import Prelude.Kore
+
+import Control.DeepSeq
+    ( NFData
+    )
+import qualified Control.Lens as Lens
+import Data.Generics.Product
+import qualified Generics.SOP as SOP
+import qualified GHC.Generics as GHC
+
+import Kore.Attribute.Pattern
+    ( Pattern
+    )
+import qualified Kore.Attribute.Pattern as Pattern
+import Kore.Attribute.Pattern.FreeVariables hiding
+    ( freeVariables
+    )
+import qualified Kore.Attribute.Pattern.FreeVariables as FreeVariables
+    ( freeVariables
+    )
+import Kore.Attribute.Pattern.Simplified hiding
+    ( isFullySimplified
+    , isSimplified
+    )
+import qualified Kore.Attribute.Pattern.Simplified as Simplified
+    ( isFullySimplified
+    , isSimplified
+    )
+import Kore.Attribute.Synthetic
+import Kore.Debug
+import qualified Kore.Internal.SideCondition.SideCondition as SideCondition
+    ( Representation
+    )
+import Kore.Syntax.Variable
+
+{- | @Pattern@ are the attributes of a pattern collected during verification.
+ -}
+data PredicatePattern variable =
+    PredicatePattern
+        { freeVariables :: !(FreeVariables variable)
+        , simplified :: !Simplified
+        }
+    deriving (Eq, GHC.Generic, Show)
+
+instance NFData variable => NFData (PredicatePattern variable)
+
+instance Hashable variable => Hashable (PredicatePattern variable)
+
+instance SOP.Generic (PredicatePattern variable)
+
+instance SOP.HasDatatypeInfo (PredicatePattern variable)
+
+instance Debug variable => Debug (PredicatePattern variable) where
+    debugPrecBrief _ _ = "_"
+
+instance (Debug variable, Diff variable) => Diff (PredicatePattern variable)
+
+instance
+    ( Functor base
+    , Synthetic (FreeVariables variable) base
+    , Synthetic Simplified base
+    ) => Synthetic (PredicatePattern variable) base
+  where
+    synthetic base = PredicatePattern
+        { freeVariables = synthetic (freeVariables <$> base)
+        , simplified = synthetic (simplified <$> base)
+        }
+
+
+simplifiedAttribute :: PredicatePattern variable -> Simplified
+simplifiedAttribute PredicatePattern {simplified} = simplified
+
+{- Checks whether the pattern is simplified relative to the given side
+condition.
+-}
+isSimplified
+    :: SideCondition.Representation -> PredicatePattern variable -> Bool
+isSimplified sideCondition = Simplified.isSimplified sideCondition . simplifiedAttribute
+
+{- Checks whether the pattern is simplified relative to any side condition.
+-}
+isFullySimplified :: PredicatePattern variable -> Bool
+isFullySimplified PredicatePattern {simplified} = Simplified.isFullySimplified simplified
+
+setSimplified :: Simplified -> PredicatePattern variable -> PredicatePattern variable
+setSimplified simplified patt = patt { simplified }
+
+{- | Use the provided mapping to replace all variables in a 'Pattern'.
+
+See also: 'traverseVariables'
+
+ -}
+mapVariables
+    :: Ord variable2
+    => AdjSomeVariableName (variable1 -> variable2)
+    -> PredicatePattern variable1
+    -> PredicatePattern variable2
+mapVariables adj = Lens.over (field @"freeVariables") (mapFreeVariables adj)
+
+{- | Use the provided traversal to replace the free variables in a 'Pattern'.
+
+See also: 'mapVariables'
+
+ -}
+traverseVariables
+    :: forall m variable1 variable2
+    .  Monad m
+    => Ord variable2
+    => AdjSomeVariableName (variable1 -> m variable2)
+    -> PredicatePattern variable1
+    -> m (PredicatePattern variable2)
+traverseVariables adj = field @"freeVariables" (traverseFreeVariables adj)
+
+{- | Delete the given variable from the set of free variables.
+ -}
+deleteFreeVariable
+    :: Ord variable
+    => SomeVariable variable
+    -> PredicatePattern variable
+    -> PredicatePattern variable
+deleteFreeVariable variable =
+    Lens.over (field @"freeVariables") (bindVariable variable)
+
+
+instance HasFreeVariables (PredicatePattern variable) variable where
+    freeVariables = freeVariables
+
+fromPattern :: Pattern variable -> PredicatePattern variable
+fromPattern p =
+    PredicatePattern (Pattern.freeVariables p) (Pattern.simplifiedAttribute p)
diff --git a/kore/src/Kore/Builtin/AssocComm/CeilSimplifier.hs b/kore/src/Kore/Builtin/AssocComm/CeilSimplifier.hs
@@ -95,13 +95,13 @@ newSetCeilSimplifier
             (BuiltinAssocComm NormalizedSet variable)
             (OrCondition variable)
 newSetCeilSimplifier =
-    CeilSimplifier $ \ceil@Ceil { ceilResultSort, ceilChild } -> do
+    CeilSimplifier $ \ceil@Ceil { ceilChild } -> do
         let mkInternalAc normalizedAc =
                 ceilChild { builtinAcChild = wrapAc normalizedAc }
             mkNotMember element termLike =
                 mkInternalAc (fromElement element) { opaque = [termLike] }
                 & TermLike.mkInternalSet
-                & makeCeilPredicate ceilResultSort
+                & 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.
@@ -122,13 +122,13 @@ newMapCeilSimplifier
             (BuiltinAssocComm NormalizedMap variable)
             (OrCondition variable)
 newMapCeilSimplifier =
-    CeilSimplifier $ \ceil@Ceil { ceilResultSort, ceilChild } -> do
+    CeilSimplifier $ \ceil@Ceil { ceilChild } -> do
         let mkInternalAc normalizedAc =
                 ceilChild { builtinAcChild = wrapAc normalizedAc }
             mkNotMember element termLike =
                 mkInternalAc (fromElement element') { opaque = [termLike] }
                 & TermLike.mkInternalMap
-                & makeCeilPredicate ceilResultSort
+                & 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.
@@ -185,7 +185,7 @@ newBuiltinAssocCommCeilSimplifier
             (BuiltinAssocComm normalized variable)
             (OrCondition variable)
 newBuiltinAssocCommCeilSimplifier mkBuiltin mkNotMember =
-    CeilSimplifier $ \Ceil { ceilResultSort, ceilChild } -> do
+    CeilSimplifier $ \Ceil { ceilChild } -> do
         let internalAc@InternalAc { builtinAcChild } = ceilChild
         sideCondition <- Reader.ask
         let normalizedAc = unwrapAc builtinAcChild
@@ -207,7 +207,7 @@ newBuiltinAssocCommCeilSimplifier mkBuiltin mkNotMember =
                         emptyNormalizedAc { opaque = [opaque1, opaque2] }
                     }
                 & mkBuiltin
-                & makeCeilPredicate ceilResultSort
+                & 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.
@@ -240,7 +240,7 @@ newBuiltinAssocCommCeilSimplifier mkBuiltin mkNotMember =
 
         let makeEvaluateTerm, defineAbstractKey, defineOpaque
                 :: TermLike variable -> MaybeT simplifier (OrCondition variable)
-            makeEvaluateTerm = makeEvaluateTermCeil sideCondition ceilResultSort
+            makeEvaluateTerm = makeEvaluateTermCeil sideCondition
             defineAbstractKey = makeEvaluateTerm
             defineOpaque = makeEvaluateTerm
 

diff --git a/kore/src/Kore/Builtin/Builtin.hs b/kore/src/Kore/Builtin/Builtin.hs
@@ -93,7 +93,7 @@ import Kore.Internal.Pattern as Pattern
     , withCondition
     )
 import Kore.Internal.Predicate
-    ( makeEqualsPredicate_
+    ( makeEqualsPredicate
     )
 import qualified Kore.Internal.Predicate as Predicate
 import qualified Kore.Internal.SideCondition as SideCondition
@@ -511,13 +511,12 @@ unifyEqualsUnsolved SimplificationType.And a b = do
     orCondition <-
         makeEvaluateTermCeil
             SideCondition.topTODO
-            predicateSort
             unified
     predicate <- Monad.Unify.scatter orCondition
     return (unified `Pattern.withCondition` predicate)
 unifyEqualsUnsolved SimplificationType.Equals a b =
     return Pattern.top
-        {predicate = Predicate.markSimplified $ makeEqualsPredicate_ a b}
+        {predicate = Predicate.markSimplified $ makeEqualsPredicate a b}
 
 makeDomainValueTerm
     :: InternalVariable variable

diff --git a/kore/src/Kore/Builtin/Int.hs b/kore/src/Kore/Builtin/Int.hs
@@ -385,9 +385,9 @@ evalEq resultSort arguments@[_intLeft, _intRight] =
             empty
 
     mkCeilUnlessDefined termLike
-      | TermLike.isDefinedPattern termLike = Condition.topOf resultSort
+      | TermLike.isDefinedPattern termLike = Condition.top
       | otherwise =
-        Condition.fromPredicate (makeCeilPredicate resultSort termLike)
+        Condition.fromPredicate (makeCeilPredicate termLike)
     returnPattern = return . flip Pattern.andCondition conditions
     conditions = foldMap mkCeilUnlessDefined arguments
 

diff --git a/kore/src/Kore/Builtin/KEqual.hs b/kore/src/Kore/Builtin/KEqual.hs
@@ -61,7 +61,7 @@ import Kore.Internal.Pattern
     )
 import qualified Kore.Internal.Pattern as Pattern
 import Kore.Internal.Predicate
-    ( makeCeilPredicate_
+    ( makeCeilPredicate
     )
 import qualified Kore.Internal.SideCondition as SideCondition
 import Kore.Internal.Symbol
@@ -258,7 +258,7 @@ unifyIfThenElse unifyChildren a b =
     worker a b <|> worker b a
   where
     takeCondition value condition' =
-        makeCeilPredicate_ (mkAnd (Bool.asInternal sort value) condition')
+        makeCeilPredicate (mkAnd (Bool.asInternal sort value) condition')
         & Condition.fromPredicate
       where
         sort = termLikeSort condition'

diff --git a/kore/src/Kore/Builtin/Map.hs b/kore/src/Kore/Builtin/Map.hs
@@ -98,7 +98,6 @@ import qualified Kore.Internal.TermLike as TermLike
 import Kore.Sort
     ( Sort
     )
-import qualified Kore.Sort as Sort
 import Kore.Step.Simplification.NotSimplifier
 import Kore.Step.Simplification.Simplify as Simplifier
 import Kore.Syntax.Sentence
@@ -340,9 +339,9 @@ evalInKeys resultSort arguments@[_key, _map] =
     emptyMap <|> concreteMap <|> symbolicMap
   where
     mkCeilUnlessDefined termLike
-      | TermLike.isDefinedPattern termLike = Condition.topOf resultSort
+      | TermLike.isDefinedPattern termLike = Condition.top
       | otherwise =
-        Condition.fromPredicate (makeCeilPredicate resultSort termLike)
+        Condition.fromPredicate (makeCeilPredicate termLike)
 
     returnPattern = return . flip Pattern.andCondition conditions
     conditions = foldMap mkCeilUnlessDefined arguments
@@ -616,7 +615,7 @@ unifyNotInKeys unifyChildren (NotSimplifier notSimplifier) a b =
 
     defineTerm :: TermLike variable -> MaybeT unifier (Condition variable)
     defineTerm termLike =
-        makeEvaluateTermCeil SideCondition.topTODO Sort.predicateSort termLike
+        makeEvaluateTermCeil SideCondition.topTODO termLike
         >>= Unify.scatter
         & lift
 

diff --git a/kore/src/Kore/Builtin/Set.hs b/kore/src/Kore/Builtin/Set.hs
@@ -298,7 +298,7 @@ evalIn resultSort [_elem, _set] = do
     returnIfTrueAndDefined result setTerm
       | result = do
         let condition =
-                Conditional.fromPredicate $ makeCeilPredicate resultSort setTerm
+                Conditional.fromPredicate $ makeCeilPredicate setTerm
             trueWithCondition =
                 Pattern.andCondition
                     (asExpandedBoolPattern result)
@@ -347,7 +347,7 @@ evalDifference
             _set2 <- expectBuiltinSet ctx _set2
             let definedArgs =
                     filter (not . TermLike.isDefinedPattern) args
-                    & map (makeCeilPredicate resultSort)
+                    & map makeCeilPredicate
                     & makeMultipleAndPredicate
                     & Conditional.fromPredicate
             let NormalizedAc

diff --git a/kore/src/Kore/Equation/Application.hs b/kore/src/Kore/Equation/Application.hs
@@ -651,11 +651,11 @@ instance InternalVariable variable => Pretty (CheckRequiresError variable) where
     pretty checkRequiresError =
         Pretty.vsep
         [ "could not infer the equation requirement:"
-        , Pretty.indent 4 (unparse equationRequires)
+        , Pretty.indent 4 (pretty equationRequires)
         , "and the matching requirement:"
-        , Pretty.indent 4 (unparse matchPredicate)
+        , Pretty.indent 4 (pretty matchPredicate)
         , "from the side condition:"
-        , Pretty.indent 4 (unparse sideCondition)
+        , Pretty.indent 4 (pretty sideCondition)
         ]
       where
         CheckRequiresError { matchPredicate, equationRequires, sideCondition } =