Merge pull request #4298 from IntersectMBO/PR-assertReified

`constrained-generators`: utility function for asserting over a reified value
IntersectMBO · Apr 25, 2024 · 2f0ad36 · 2f0ad36
2 parents 53cd7f9 + 914143b
commit 2f0ad36
Show file tree

Hide file tree

Showing 4 changed files with 16 additions and 0 deletions.
diff --git a/libs/constrained-generators/src/Constrained.hs b/libs/constrained-generators/src/Constrained.hs
@@ -65,6 +65,8 @@ module Constrained (
   isJust,
   reify,
   reify',
+  reifies,
+  assertReified,
   genHint,
   dependsOn,
   forAll,

diff --git a/libs/constrained-generators/src/Constrained/Base.hs b/libs/constrained-generators/src/Constrained/Base.hs
@@ -1034,8 +1034,12 @@ computeSpecSimplified x p = fromGE ErrorSpec $ case p of
   Case t branches ->
     let branchSpecs = mapList computeSpecBinderSimplified branches
      in propagateSpec (caseSpec branchSpecs) <$> toCtx x t
+  Reifies (Lit a) (Lit val) f
+    | f val == a -> pure TrueSpec
+    | otherwise -> genError ["Value does not reify to literal: " ++ show val ++ " -/> " ++ show a]
   Reifies t' (Lit val) f ->
     propagateSpec (equalSpec (f val)) <$> toCtx x t'
+  Reifies Lit {} _ _ -> pure TrueSpec
   -- Impossible cases that should be ruled out by the dependency analysis and linearizer
   DependsOn {} -> fatalError ["The impossible happened in computeSpec: DependsOn"]
   Reifies {} -> fatalError ["The impossible happened in computeSpec: Reifies", show x, show p]
@@ -3778,6 +3782,9 @@ reify t f body =
     , toPred $ body x
     ]
 
+assertReified :: HasSpec fn a => Term fn a -> (a -> Bool) -> Pred fn
+assertReified = reifies (lit True)
+
 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
@@ -150,3 +150,9 @@ basicSpec = constrained $ \x ->
   unsafeExists $ \y ->
     satisfies x $ constrained $ \x' ->
       x' <=. 1 + y
+
+assertReal :: Specification BaseFn Int
+assertReal = constrained $ \x ->
+  [ assert $ x <=. 10
+  , assertReified x (<= 10)
+  ]
diff --git a/libs/constrained-generators/test/Constrained/Test.hs b/libs/constrained-generators/test/Constrained/Test.hs
@@ -44,6 +44,7 @@ testAll = hspec tests
 tests :: Spec
 tests =
   describe "constrained" $ do
+    testSpec "assertReal" assertReal
     testSpec "setSpec" setSpec
     testSpec "leqPair" leqPair
     testSpec "setPair" setPair