hotfix with new test

IntersectMBO · Apr 25, 2024 · 8613227 · 8613227
1 parent 2f0ad36
commit 8613227
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 1 deletion.
diff --git a/libs/constrained-generators/src/Constrained/Base.hs b/libs/constrained-generators/src/Constrained/Base.hs
@@ -3783,7 +3783,11 @@ reify t f body =
     ]
 
 assertReified :: HasSpec fn a => Term fn a -> (a -> Bool) -> Pred fn
-assertReified = reifies (lit True)
+-- Note, it is necessary to introduce the extra variable from the `exists` here
+-- to make things like `assertRealMultiple` work, if you don't have it then the
+-- `reifies` isn't a defining constraint for anything any more.
+assertReified t f =
+  reify t f assert
 
 reifies :: (HasSpec fn a, HasSpec fn b) => Term fn b -> Term fn a -> (a -> b) -> Pred fn
 reifies = Reifies

diff --git a/libs/constrained-generators/src/Constrained/Examples/Basic.hs b/libs/constrained-generators/src/Constrained/Examples/Basic.hs
@@ -156,3 +156,10 @@ assertReal = constrained $ \x ->
   [ assert $ x <=. 10
   , assertReified x (<= 10)
   ]
+
+assertRealMultiple :: Specification BaseFn (Int, Int)
+assertRealMultiple = constrained' $ \x y ->
+  [ assert $ x <=. 10
+  , assert $ 11 <=. y
+  , assertReified (pair_ x y) $ uncurry (/=)
+  ]
diff --git a/libs/constrained-generators/test/Constrained/Test.hs b/libs/constrained-generators/test/Constrained/Test.hs
@@ -45,6 +45,7 @@ tests :: Spec
 tests =
   describe "constrained" $ do
     testSpec "assertReal" assertReal
+    testSpec "assertRealMultiple" assertRealMultiple
     testSpec "setSpec" setSpec
     testSpec "leqPair" leqPair
     testSpec "setPair" setPair