Property tests: implement separate Predicate generator

kore/test/Test/ConsistentKore.hs

@@ -1,8 +1,8 @@
 module Test.ConsistentKore (
     CollectionSorts (..),
     Setup (..),
-    runTermGen,
-    termLikeGen,
+    runKoreGen,
+    patternGen,
 ) where
 
 import qualified Control.Arrow as Arrow
@@ -67,9 +67,13 @@ import qualified Kore.Internal.Alias as Internal (
 import Kore.Internal.ApplicationSorts (
     ApplicationSorts (ApplicationSorts),
  )
+import Kore.Internal.From
 import Kore.Internal.InternalMap
 import Kore.Internal.InternalSet
 import Kore.Internal.InternalString
+import Kore.Internal.Pattern (Pattern)
+import qualified Kore.Internal.Pattern as Pattern
+import Kore.Internal.Predicate (Predicate)
 import qualified Kore.Internal.Symbol as Internal (
     Symbol (Symbol),
  )
@@ -82,15 +86,11 @@ import Kore.Internal.TermLike (
     mkApplyAlias,
     mkApplySymbol,
     mkBottom,
-    mkCeil,
     mkElemVar,
-    mkEquals,
     mkExists,
-    mkFloor,
     mkForall,
     mkIff,
     mkImplies,
-    mkIn,
     mkInternalBool,
     mkInternalInt,
     mkInternalList,
@@ -186,8 +186,8 @@ data Setup = Setup
 
 type Gen = ReaderT (Setup, Context) Hedgehog.Gen
 
-runTermGen :: Setup -> Gen a -> Hedgehog.Gen a
-runTermGen
+runKoreGen :: Setup -> Gen a -> Hedgehog.Gen a
+runKoreGen
     setup@Setup{freeElementVariables, freeSetVariables}
     generator =
         Reader.runReaderT generator (setup, context)
@@ -200,6 +200,12 @@ runTermGen
                 , onlyConcrete = False
                 }
 
+patternGen :: Gen (Pattern VariableName)
+patternGen =
+    Pattern.fromTermAndPredicate
+        <$> termLikeGen
+        <*> predicateGen
+
 addQuantifiedSetVariable :: SetVariable VariableName -> Context -> Context
 addQuantifiedSetVariable
     variable
@@ -228,8 +234,11 @@ requestConcrete =
     localContext (\context -> context{onlyConcrete = True})
 
 termLikeGen :: Gen (TermLike VariableName)
-termLikeGen = do
-    topSort <- sortGen
+termLikeGen =
+    sortGen >>= termLikeGenWithSort
+
+termLikeGenWithSort :: Sort -> Gen (TermLike VariableName)
+termLikeGenWithSort topSort = do
     maybeResult <-
         Gen.scale limitTermDepth $
             Gen.sized (\size -> termLikeGenImpl size topSort)
@@ -241,6 +250,78 @@ termLikeGen = do
         | s < 10 = Range.Size s
         | otherwise = Range.Size 10
 
+predicateGen :: Gen (Predicate VariableName)
+predicateGen =
+    Gen.recursive
+        Gen.choice
+        [return fromTop_, return fromBottom_]
+        [ andPredicateGen
+        , orPredicateGen
+        , notPredicateGen
+        , impliesPredicateGen
+        , iffPredicateGen
+        , ceilGen
+        , floorGen
+        , equalsGen
+        , inGen
+        , existsPredicateGen
+        , forallPredicateGen
+        ]
+
+andPredicateGen :: Gen (Predicate VariableName)
+andPredicateGen =
+    Gen.subterm2 predicateGen predicateGen fromAnd
+
+orPredicateGen :: Gen (Predicate VariableName)
+orPredicateGen =
+    Gen.subterm2 predicateGen predicateGen fromOr
+
+impliesPredicateGen :: Gen (Predicate VariableName)
+impliesPredicateGen =
+    Gen.subterm2 predicateGen predicateGen fromImplies
+
+iffPredicateGen :: Gen (Predicate VariableName)
+iffPredicateGen =
+    Gen.subterm2 predicateGen predicateGen fromIff
+
+notPredicateGen :: Gen (Predicate VariableName)
+notPredicateGen =
+    Gen.subterm predicateGen fromNot
+
+ceilGen :: Gen (Predicate VariableName)
+ceilGen =
+    fromCeil_ <$> termLikeGen
+
+floorGen :: Gen (Predicate VariableName)
+floorGen =
+    fromFloor_ <$> termLikeGen
+
+equalsGen :: Gen (Predicate VariableName)
+equalsGen = do
+    sort' <- sortGen
+    fromEquals_
+        <$> termLikeGenWithSort sort'
+        <*> termLikeGenWithSort sort'
+
+inGen :: Gen (Predicate VariableName)
+inGen = do
+    sort' <- sortGen
+    fromIn_
+        <$> termLikeGenWithSort sort'
+        <*> termLikeGenWithSort sort'
+
+existsPredicateGen :: Gen (Predicate VariableName)
+existsPredicateGen = do
+    sort' <- sortGen
+    variable <- elementVariableGen sort'
+    Gen.subterm predicateGen (fromExists variable)
+
+forallPredicateGen :: Gen (Predicate VariableName)
+forallPredicateGen = do
+    sort' <- sortGen
+    variable <- elementVariableGen sort'
+    Gen.subterm predicateGen (fromForall variable)
+
 termLikeGenImpl :: Range.Size -> Sort -> Gen (Maybe (TermLike VariableName))
 termLikeGenImpl (Range.Size size) requestedSort = do
     allGenerators <- termGenerators
@@ -336,19 +417,15 @@ termGenerators = do
         filterGeneratorsAndGroup
             [ andGenerator
             , bottomGenerator
-            , ceilGenerator
-            , equalsGenerator
             , existsGenerator
-            , floorGenerator
             , forallGenerator
             , iffGenerator
             , impliesGenerator
-            , inGenerator
-            , muGenerator
             , notGenerator
-            , nuGenerator
             , orGenerator
             , topGenerator
+            , nuGenerator
+            , muGenerator
             ]
     literals <-
         filterGeneratorsAndGroup
@@ -425,27 +502,6 @@ unaryOperatorGenerator builder =
         return
             (builder <$> child) -- Maybe functor
 
-unaryFreeSortOperatorGenerator ::
-    (Sort -> TermLike VariableName -> TermLike VariableName) ->
-    TermGenerator
-unaryFreeSortOperatorGenerator builder =
-    TermGenerator
-        { arity = 1
-        , sort = AnySort
-        , attributes =
-            AttributeRequirements
-                { isConstructorLike = False
-                , isConcrete = True
-                }
-        , generator = worker
-        }
-  where
-    worker childGenerator resultSort = do
-        childSort <- sortGen
-        child <- childGenerator childSort
-        return
-            (builder resultSort <$> child) -- Maybe functor
-
 unaryQuantifiedElementOperatorGenerator ::
     (ElementVariable VariableName -> TermLike VariableName -> TermLike VariableName) ->
     TermGenerator
@@ -495,28 +551,6 @@ muNuOperatorGenerator builder =
             return
                 (builder quantifiedVariable <$> child) -- Maybe functor
 
-binaryFreeSortOperatorGenerator ::
-    (Sort -> TermLike VariableName -> TermLike VariableName -> TermLike VariableName) ->
-    TermGenerator
-binaryFreeSortOperatorGenerator builder =
-    TermGenerator
-        { arity = 2
-        , sort = AnySort
-        , attributes =
-            AttributeRequirements
-                { isConstructorLike = False
-                , isConcrete = True
-                }
-        , generator = worker
-        }
-  where
-    worker childGenerator resultSort = do
-        childSort <- sortGen
-        child1 <- childGenerator childSort
-        child2 <- childGenerator childSort
-        return
-            (builder resultSort <$> child1 <*> child2) -- Maybe applicative
-
 binaryOperatorGenerator ::
     (TermLike VariableName -> TermLike VariableName -> TermLike VariableName) ->
     TermGenerator
@@ -544,18 +578,9 @@ andGenerator = binaryOperatorGenerator mkAnd
 bottomGenerator :: TermGenerator
 bottomGenerator = nullaryFreeSortOperatorGenerator mkBottom
 
-ceilGenerator :: TermGenerator
-ceilGenerator = unaryFreeSortOperatorGenerator mkCeil
-
-equalsGenerator :: TermGenerator
-equalsGenerator = binaryFreeSortOperatorGenerator mkEquals
-
 existsGenerator :: TermGenerator
 existsGenerator = unaryQuantifiedElementOperatorGenerator mkExists
 
-floorGenerator :: TermGenerator
-floorGenerator = unaryFreeSortOperatorGenerator mkFloor
-
 forallGenerator :: TermGenerator
 forallGenerator = unaryQuantifiedElementOperatorGenerator mkForall
 
@@ -565,9 +590,6 @@ iffGenerator = binaryOperatorGenerator mkIff
 impliesGenerator :: TermGenerator
 impliesGenerator = binaryOperatorGenerator mkImplies
 
-inGenerator :: TermGenerator
-inGenerator = binaryFreeSortOperatorGenerator mkIn
-
 muGenerator :: TermGenerator
 muGenerator = muNuOperatorGenerator mkMu
 

kore/test/Test/Kore/Simplify/IntegrationProperty.hs

@@ -46,7 +46,7 @@ import Kore.Rewrite.Axiom.EvaluationStrategy (
  )
 import Kore.Rewrite.RewritingVariable (
     RewritingVariableName,
-    mkRewritingTerm,
+    mkRewritingPattern,
  )
 import qualified Kore.Simplify.Data as Simplification
 import qualified Kore.Simplify.Pattern as Pattern (
@@ -68,20 +68,20 @@ import Test.Tasty.HUnit.Ext
 test_simplifiesToSimplified :: TestTree
 test_simplifiesToSimplified =
     testPropertyWithoutSolver "simplify returns simplified pattern" $ do
-        term <- forAll (runTermGen Mock.generatorSetup termLikeGen)
-        let term' = mkRewritingTerm term
+        patt <- forAll (runKoreGen Mock.generatorSetup patternGen)
+        let patt' = mkRewritingPattern patt
         (annotate . unlines)
-            [" ***** unparsed input =", unparseToString term, " ***** "]
+            [" ***** unparsed input =", unparseToString patt, " ***** "]
         simplified <-
             catch
-                (evaluateT (Pattern.fromTermLike term'))
-                (exceptionHandler term)
+                (evaluateT patt')
+                (exceptionHandler patt)
         (===) True (OrPattern.isSimplified sideRepresentation simplified)
   where
     -- Discard exceptions that are normal for randomly generated patterns.
     exceptionHandler ::
         MonadThrow m =>
-        TermLike VariableName ->
+        Pattern VariableName ->
         ErrorCall ->
         PropertyT m a
     exceptionHandler term err@(ErrorCallWithLocation message _location)