constrained-generators: Fix looping issue

IntersectMBO · Nov 8, 2024 · f5cffc3 · f5cffc3
1 parent aed1dc2
commit f5cffc3
Show file tree

Hide file tree

Showing 5 changed files with 34 additions and 9 deletions.
diff --git a/libs/constrained-generators/src/Constrained/Base.hs b/libs/constrained-generators/src/Constrained/Base.hs
@@ -1317,7 +1317,6 @@ flattenPred pIn = go (freeVarNames pIn) [pIn]
 
 computeDependencies :: Pred fn -> DependGraph fn
 computeDependencies = \case
-  x@(Exists _ (_v :-> Block [Reifies (V a) _b _, _c])) -> deleteNode (Name a) (computeDependencies x)
   Monitor {} -> mempty
   Subst x t p -> computeDependencies (substitutePred x t p)
   Assert _ t -> computeTermDependencies t
@@ -1388,7 +1387,15 @@ prepareLinearization p = do
   let preds = concatMap saturatePred $ flattenPred p
       hints = computeHints preds
       graph = transitiveClosure $ hints <> respecting hints (foldMap computeDependencies preds)
-  plan <- linearize preds graph
+  plan <-
+    explain
+      ( NE.fromList
+          [ "Linearizing"
+          , show $ "  preds: " <> pretty preds
+          , show $ "  graph: " <> pretty graph
+          ]
+      )
+      $ linearize preds graph
   pure $ backPropagation $ SolverPlan plan graph
 
 -- TODO: generalize this to make it more flexible and extensible
@@ -2339,7 +2346,9 @@ simplifyPred = \case
     t' -> GenHint h t'
   Subst x t p -> simplifyPred $ substitutePred x t p
   Assert es t -> assertExplain es (simplifyTerm t)
-  Reifies t' t f -> Reifies (simplifyTerm t') (simplifyTerm t) f
+  Reifies t' t f -> case simplifyTerm t of
+    Lit a -> assert $ simplifyTerm t' ==. Lit (f a)
+    t'' -> Reifies (simplifyTerm t') t'' f
   ForAll set b -> case simplifyTerm set of
     Lit as -> foldMap (`unBind` b) (forAllToList as)
     App (extractFn @(SetFn fn) @fn -> Just Union) (xs :> ys :> Nil) ->

diff --git a/libs/constrained-generators/src/Constrained/Examples/Basic.hs b/libs/constrained-generators/src/Constrained/Examples/Basic.hs
@@ -312,3 +312,14 @@ whenTrueExists = constrained $ \x ->
       [ not_ [var| b |]
       , not_ (not_ b)
       ]
+
+wtfSpec :: Specification BaseFn ([Int], Maybe ((), [Int]))
+wtfSpec = constrained' $ \ [var| options |] [var| mpair |] ->
+  caseOn
+    mpair
+    (branch $ \_ -> False)
+    ( branch $ \pair -> match pair $ \unit ints ->
+        [ forAll ints $ \int -> reify options id $ \xs -> int `elem_` xs
+        , assert $ unit ==. lit ()
+        ]
+    )
diff --git a/libs/constrained-generators/src/Constrained/GenT.hs b/libs/constrained-generators/src/Constrained/GenT.hs
@@ -82,9 +82,10 @@ instance Monad GE where
 instance MonadGenError GE where
   genError neStr = GenError [] neStr
   fatalError neStr = FatalError [] neStr
-  explain nes (GenError es' err) = GenError (nes : es') err
-  explain nes (FatalError es' err) = FatalError (nes : es') err
-  explain nes (Result es' a) = Result (nes : es') a
+  explain nes ge = case ge of
+    GenError es' err -> GenError (nes : es') err
+    FatalError es' err -> FatalError (nes : es') err
+    Result es' a -> Result (nes : es') a
 
 instance MonadGenError m => MonadGenError (GenT m) where
   genError es = GenT $ \_ -> pure $ genError es

diff --git a/libs/constrained-generators/src/Constrained/Properties.hs b/libs/constrained-generators/src/Constrained/Properties.hs
@@ -61,6 +61,11 @@ prop_sound spec =
 prop_constrained_satisfies_sound :: HasSpec fn a => Specification fn a -> QC.Property
 prop_constrained_satisfies_sound spec = prop_sound (constrained $ \a -> satisfies a spec)
 
+prop_constrained_explained :: HasSpec fn a => Specification fn a -> QC.Property
+prop_constrained_explained spec =
+  QC.forAll QC.arbitrary $ \es ->
+    prop_sound $ constrained $ \x -> explanation es $ x `satisfies` spec
+
 -- | `prop_complete ps` assumes that `ps` is satisfiable
 prop_complete :: HasSpec fn a => Specification fn a -> QC.Property
 prop_complete s =

diff --git a/libs/constrained-generators/test/Constrained/Test.hs b/libs/constrained-generators/test/Constrained/Test.hs
@@ -25,7 +25,6 @@ import GHC.Natural
 import Test.Hspec
 import Test.Hspec.QuickCheck
 import Test.QuickCheck hiding (Args, Fun, forAll)
-import Test.QuickCheck qualified as QC
 
 import Constrained.Examples
 import Constrained.Internals
@@ -151,6 +150,7 @@ tests nightly =
     testSpecNoShrink "powersetPickOne" powersetPickOne
     testSpecNoShrink "appendSuffix" appendSuffix
     testSpecNoShrink "appendForAll" appendForAll
+    testSpec "wtfSpec" wtfSpec
     numberyTests
     sizeTests
     numNumSpecTree
@@ -295,8 +295,7 @@ testSpec' withShrink n s = do
     prop "prop_constrained_explained" $
       within 10_000_0000 $
         checkCoverage' $
-          QC.forAll arbitrary $ \es ->
-            prop_sound $ constrained $ \x -> explanation es $ x `satisfies` s
+          prop_constrained_explained s
     when withShrink $
       prop "prop_shrink_sound" $
         discardAfter 100_000 $