Skip to content

Commit

Permalink
Changed the monad in Constrained.GenT to use reader instead of state.
Browse files Browse the repository at this point in the history
  • Loading branch information
TimSheard committed Jan 17, 2025
1 parent c11c6ae commit eebd76c
Show file tree
Hide file tree
Showing 5 changed files with 236 additions and 169 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -429,12 +429,12 @@ conformsToImpl = property @(ImpTestM era Property) . (`runContT` pure) $ do
let
simplifiedSpec = simplifySpec spec
generator = CV2.runGenT (CV2.genFromSpecT simplifiedSpec) Loose
shrinker (Result _ x) = pure <$> shrinkWithSpec simplifiedSpec x
shrinker (Result x) = pure <$> shrinkWithSpec simplifiedSpec x
shrinker _ = []
res :: GE a <- ContT $ \c ->
pure $ forAllShrinkBlind generator shrinker c
case res of
Result _ x -> pure x
Result x -> pure x
_ -> ContT . const . pure $ property Discard
env <- forAllSpec $ environmentSpec @fn @rule @era ctx
deepEval env "environment"
Expand Down
42 changes: 23 additions & 19 deletions libs/constrained-generators/src/Constrained/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@ import GHC.Natural
import GHC.Real
import GHC.Stack
import GHC.TypeLits
import Prettyprinter
import Prettyprinter hiding (cat)
import System.Random
import System.Random.Stateful
import Test.QuickCheck hiding (Args, Fun, forAll)
Expand Down Expand Up @@ -532,7 +532,7 @@ monitorPred env = \case
monitorPred (extendEnv x val env) p
Exists k (x :-> p) -> do
case k (errorGE . explain1 "monitorPred: Exists" . runTerm env) of
Result _ a -> monitorPred (extendEnv x a env) p
Result a -> monitorPred (extendEnv x a env) p
_ -> pure id
Explain es p -> explain es $ monitorPred env p

Expand Down Expand Up @@ -787,7 +787,7 @@ instance (HasSpec fn a, Arbitrary (TypeSpec fn a)) => Arbitrary (Specification f
shrink (SuspendedSpec x p) =
[TrueSpec, ErrorSpec (pure "From shrinking SuspendedSpec")]
++ [ s
| Result _ s <- [computeSpec x p]
| Result s <- [computeSpec x p]
, not $ isSuspendedSpec s
]
++ [SuspendedSpec x p' | p' <- shrinkPred p]
Expand Down Expand Up @@ -1196,7 +1196,7 @@ shrinkWithSpec (simplifySpec -> spec) a = filter (`conformsToSpec` spec) $ case

shrinkFromPreds :: HasSpec fn a => Pred fn -> Var a -> a -> [a]
shrinkFromPreds p
| Result _ plan <- prepareLinearization p = \x a -> listFromGE $ do
| Result plan <- prepareLinearization p = \x a -> listFromGE $ do
-- NOTE: we do this to e.g. guard against bad construction functions in Exists
xaGood <- checkPred (singletonEnv x a) p
unless xaGood $
Expand Down Expand Up @@ -1292,7 +1292,7 @@ envFromPred env p = case p of
genFromSpec :: forall fn a. (HasCallStack, HasSpec fn a) => Specification fn a -> Gen a
genFromSpec spec = do
res <- catchGen $ genFromSpecT @fn @a @GE spec
either (error . show . NE.toList) pure res
either (error . show . catMessages) pure res

-- | A version of `genFromSpecT` that takes a seed and a size and gives you a result
genFromSpecWithSeed ::
Expand All @@ -1309,9 +1309,9 @@ debugSpec spec = do
then putStrLn "True"
else putStrLn "False, perhaps there is an unsafeExists in the spec?"
case ans of
FatalError xs x -> mapM f xs >> f x
GenError xs x -> mapM f xs >> f x
Result _ x -> print spec >> print x >> ok x
FatalError xs -> mapM_ f xs
GenError xs -> mapM_ f xs
Result x -> print spec >> print x >> ok x

genInverse ::
( MonadGenError m
Expand Down Expand Up @@ -1519,7 +1519,7 @@ backPropagation (SolverPlan plan graph) = SolverPlan (go [] (reverse plan)) grap
termVarEqCases spec x' t
| Just Refl <- eqVar x x'
, [Name y] <- Set.toList $ freeVarSet t
, Result _ ctx <- toCtx y t =
, Result ctx <- toCtx y t =
[SolverStage y [] (propagateSpec spec ctx)]
termVarEqCases _ _ _ = []

Expand Down Expand Up @@ -1608,7 +1608,7 @@ short xs = "([" <+> viaShow (length xs) <+> "elements ...] @" <> prettyType @a <
prettyPlan :: HasSpec fn a => Specification fn a -> Doc ann
prettyPlan (simplifySpec -> spec)
| SuspendedSpec _ p <- spec
, Result _ plan <- prepareLinearization p =
, Result plan <- prepareLinearization p =
vsep'
[ "Simplified spec:" /> pretty spec
, pretty plan
Expand Down Expand Up @@ -1761,9 +1761,9 @@ normalizeSolverStage (SolverStage x ps spec) = SolverStage x ps'' (spec <> spec'

fromGESpec :: HasCallStack => GE (Specification fn a) -> Specification fn a
fromGESpec ge = case ge of
Result [] s -> s
Result es s -> addToErrorSpec (foldr1 (<>) es) s
_ -> fromGE ErrorSpec ge
Result s -> s
GenError xs -> ErrorSpec (catMessageList xs)
FatalError es -> error $ catMessages es

-- | Add the explanations, if it's an ErrorSpec, else drop them
addToErrorSpec :: NE.NonEmpty String -> Specification fn a -> Specification fn a
Expand Down Expand Up @@ -1886,8 +1886,10 @@ computeSpecSimplified x p = localGESpec $ case p of
["The impossible happened in computeSpec: Reifies", " " ++ show x, show $ indent 2 (pretty p)]
where
-- We want `genError` to turn into `ErrorSpec` and we want `FatalError` to turn into `FatalError`
localGESpec ge@FatalError {} = ge
localGESpec ge = pure $ fromGESpec ge
localGESpec ge = case ge of
(GenError xs) -> Result $ ErrorSpec (catMessageList xs)
(FatalError es) -> FatalError es
(Result x) -> Result x

-- | Precondition: the `Pred fn` defines the `Var a`.
--
Expand Down Expand Up @@ -6242,11 +6244,13 @@ checkPredE env msgs = \case
Right v -> v
Left es -> error $ unlines $ NE.toList (msgs <> es)
in case k eval of
Result _ a -> checkPredE (extendEnv x a env) msgs p
FatalError ess es -> Just (msgs <> foldr1 (<>) ess <> es)
GenError ess es -> Just (msgs <> foldr1 (<>) ess <> es)
Result a -> checkPredE (extendEnv x a env) msgs p
FatalError es -> Just (msgs <> catMessageList es)
GenError es -> Just (msgs <> catMessageList es)
Explain es p -> checkPredE env (msgs <> es) p

-- | conformsToSpec with explanation. Nothing if (conformsToSpec a spec),
-- but (Just explanations) if not(conformsToSpec a spec).
conformsToSpecE ::
forall fn a.
HasSpec fn a =>
Expand All @@ -6255,7 +6259,7 @@ conformsToSpecE ::
NE.NonEmpty String ->
Maybe (NE.NonEmpty String)
conformsToSpecE a (ExplainSpec [] s) msgs = conformsToSpecE a s msgs
conformsToSpecE a (ExplainSpec (x : xs) s) msgs = conformsToSpecE a s (msgs <> (x NE.:| xs))
conformsToSpecE a (ExplainSpec (x : xs) s) msgs = conformsToSpecE a s ((x :| xs) <> msgs)
conformsToSpecE _ TrueSpec _ = Nothing
conformsToSpecE a (MemberSpec as) msgs =
if elem a as
Expand Down
16 changes: 8 additions & 8 deletions libs/constrained-generators/src/Constrained/Examples/Fold.hs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,6 @@ import Constrained.Base (Pred (..), genListWithSize, predSpecPair)
import Constrained.Examples.List (Numbery)
import Constrained.SumList
import Data.List.NonEmpty (NonEmpty ((:|)))
import qualified Data.List.NonEmpty as NE
import Data.String (fromString)
import Prettyprinter (fillSep, punctuate, space)
import System.Random (Random)
Expand Down Expand Up @@ -140,14 +139,15 @@ testFoldSpec size elemSpec total outcome = do
ans <- genFromGenT $ inspect $ genListWithSize size elemSpec total
let callString = parensList ["GenListWithSize", show size, fst (predSpecPair elemSpec), show total]
fails xs = unlines [callString, "Should fail, but it succeeds with", show xs]
succeeds xs = unlines (callString : "Should succeed, but it fails with" : NE.toList xs)
succeeds xs =
unlines [callString, "Should succeed, but it fails with", catMessages xs]
case (ans, outcome) of
(Result _ _, Succeed) -> pure $ property True
(Result _ xs, Fail) -> pure $ counterexample (fails xs) False
(FatalError _ _, Fail) -> pure $ property True
(FatalError _ xs, Succeed) -> pure $ counterexample (succeeds xs) False
(GenError _ _, Fail) -> pure $ property True
(GenError _ xs, Succeed) -> pure $ counterexample (succeeds xs) False
(Result _, Succeed) -> pure $ property True
(Result xs, Fail) -> pure $ counterexample (fails xs) False
(FatalError _, Fail) -> pure $ property True
(FatalError xs, Succeed) -> pure $ counterexample (succeeds xs) False
(GenError _, Fail) -> pure $ property True
(GenError xs, Succeed) -> pure $ counterexample (succeeds xs) False

-- | Generate a property from a call to 'pickAll'. We can test for success or failure using 'outcome'
sumProp ::
Expand Down
Loading

0 comments on commit eebd76c

Please sign in to comment.