From eebd76ccc0059845013addabaff8fe9f1829ca16 Mon Sep 17 00:00:00 2001 From: Tim Sheard Date: Thu, 16 Jan 2025 22:29:36 -0800 Subject: [PATCH] Changed the monad in Constrained.GenT to use reader instead of state. --- .../Ledger/Conformance/ExecSpecRule/Core.hs | 4 +- .../src/Constrained/Base.hs | 42 ++- .../src/Constrained/Examples/Fold.hs | 16 +- .../src/Constrained/GenT.hs | 341 +++++++++++------- .../src/Constrained/Properties.hs | 2 +- 5 files changed, 236 insertions(+), 169 deletions(-) diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs index bd371c9e72c..7250cef9cc8 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs @@ -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" diff --git a/libs/constrained-generators/src/Constrained/Base.hs b/libs/constrained-generators/src/Constrained/Base.hs index 9b6fa161d2d..35b7be534d7 100644 --- a/libs/constrained-generators/src/Constrained/Base.hs +++ b/libs/constrained-generators/src/Constrained/Base.hs @@ -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) @@ -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 @@ -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] @@ -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 $ @@ -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 :: @@ -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 @@ -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 _ _ _ = [] @@ -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 @@ -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 @@ -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`. -- @@ -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 => @@ -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 diff --git a/libs/constrained-generators/src/Constrained/Examples/Fold.hs b/libs/constrained-generators/src/Constrained/Examples/Fold.hs index 59ddbecb7e2..257903ce305 100644 --- a/libs/constrained-generators/src/Constrained/Examples/Fold.hs +++ b/libs/constrained-generators/src/Constrained/Examples/Fold.hs @@ -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) @@ -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 :: diff --git a/libs/constrained-generators/src/Constrained/GenT.hs b/libs/constrained-generators/src/Constrained/GenT.hs index fe52fa08608..e65f7f2d1d8 100644 --- a/libs/constrained-generators/src/Constrained/GenT.hs +++ b/libs/constrained-generators/src/Constrained/GenT.hs @@ -31,6 +31,7 @@ module Constrained.GenT where import Control.Monad import Data.Foldable +import Data.List.NonEmpty (NonEmpty ((:|)), (<|)) import Data.List.NonEmpty qualified as NE import GHC.Stack import System.Random @@ -38,17 +39,72 @@ import Test.QuickCheck hiding (Args, Fun) import Test.QuickCheck.Gen import Test.QuickCheck.Random +-- ============================================================== +-- The GE Monad + +-- | It distinguishes between two kinds of errors: FatalError and GenError +-- and non-fatal errors. +data GE a + = FatalError (NonEmpty (NonEmpty String)) + | GenError (NonEmpty (NonEmpty String)) + | Result a + deriving (Ord, Eq, Show, Functor) + +instance Applicative GE where + pure = Result + (<*>) = ap + +instance Monad GE where + FatalError es >>= _ = FatalError es + GenError es >>= _ = GenError es + Result a >>= k = k a + +------------------------------------------------------------------------ +-- The GenT monad +-- An environment monad on top of GE ------------------------------------------------------------------------ --- The Gen Error monad + +-- | Generation mode - how strict are we about requiring the generator to +-- succeed. This is necessary because sometimes failing to find a value means +-- there is an actual problem (a generator _should_ be satisfiable but for +-- whatever buggy reason it isn't) and sometimes failing to find a value just +-- means there are no values. The latter case is very relevant when you're +-- generating e.g. lists or sets of values that can be empty. +data GenMode + = Loose + | Strict + deriving (Ord, Eq, Show) + +newtype GenT m a = GenT {runGenT :: (GenMode, [NonEmpty String]) -> Gen (m a)} + deriving (Functor) + +instance Monad m => Applicative (GenT m) where + pure a = GenT (\_ -> pure @Gen (pure @m a)) + (<*>) = ap + +-- Honestly, I don't understand this, ask Max. +-- This might be an inlined use of the Gen monad transformer? +instance Monad m => Monad (GenT m) where + GenT m >>= k = GenT $ \mode -> MkGen $ \r n -> do + a <- unGen (m mode) (left r) n + unGen (runGenT (k a) mode) (right r) n + +instance MonadGenError m => MonadFail (GenT m) where + fail s = genError (pure s) + ------------------------------------------------------------------------ +-- The MonadGenError transformer +---------------------------------------------------------------------- -- | A class for different types of errors with a stack of `explain` calls to --- narrow down problems. The (NE.NonEmpty String) means one cannot cause an +-- narrow down problems. The (NonEmpty String) means one cannot cause an -- Error without at least 1 string to explain it. class Monad m => MonadGenError m where - genError :: HasCallStack => NE.NonEmpty String -> m a - fatalError :: HasCallStack => NE.NonEmpty String -> m a - explain :: HasCallStack => NE.NonEmpty String -> m a -> m a + genError :: HasCallStack => NonEmpty String -> m a + fatalError :: HasCallStack => NonEmpty String -> m a + genErrors :: HasCallStack => (NonEmpty (NonEmpty String)) -> m a + fatalErrors :: HasCallStack => (NonEmpty (NonEmpty String)) -> m a + explain :: HasCallStack => NonEmpty String -> m a -> m a -- | genError with one line of explanation genError1 :: MonadGenError m => String -> m a @@ -62,81 +118,115 @@ fatalError1 s = fatalError (pure s) explain1 :: MonadGenError m => String -> m a -> m a explain1 s = explain (pure s) --- | The Gen Error monad, distinguishes between fatal errors --- and non-fatal errors. -data GE a - = FatalError [NE.NonEmpty String] (NE.NonEmpty String) - | GenError [NE.NonEmpty String] (NE.NonEmpty String) - | Result [NE.NonEmpty String] a - deriving (Ord, Eq, Show, Functor) - -instance Applicative GE where - pure = Result [] - (<*>) = ap - -instance Monad GE where - FatalError es err >>= _ = FatalError es err - GenError es err >>= _ = GenError es err - Result _ a >>= k = k a +-- GE instance instance MonadGenError GE where - genError neStr = GenError [] neStr - fatalError neStr = FatalError [] neStr - 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 + genError msg = GenError (pure msg) + genErrors msgs = GenError msgs + fatalError msg = FatalError (pure msg) + fatalErrors msgs = FatalError msgs + explain m (GenError ms) = GenError (m <| ms) + explain m (FatalError ms) = FatalError (m <| ms) + explain _ (Result x) = Result x + +-- GenT instance +-- | calls to genError and fatalError, add the stacked messages in the monad. instance MonadGenError m => MonadGenError (GenT m) where - genError es = GenT $ \_ -> pure $ genError es - fatalError es = GenT $ \_ -> pure $ fatalError es - explain es gen = GenT $ \mode -> fmap (explain es) (runGenT gen mode) + genError e = GenT $ \(_, xs) -> pure $ genErrors (add e xs) + genErrors es = GenT $ \(_, xs) -> pure $ genErrors (cat es xs) -instance MonadGenError m => MonadFail (GenT m) where - fail s = genError (pure s) + -- Perhaps we want to turn genError into fatalError, if mode_ is Strict? + fatalError e = GenT $ \(_, xs) -> pure $ fatalErrors (add e xs) + fatalErrors es = GenT $ \(_, xs) -> pure $ fatalErrors (cat es xs) -catGEs :: MonadGenError m => [GE a] -> m [a] -catGEs [] = pure [] -catGEs (Result _ a : ges) = (a :) <$> catGEs ges -catGEs (GenError {} : ges) = catGEs ges -catGEs (FatalError es e : _) = - runGE $ FatalError es e - -fromGE :: (NE.NonEmpty String -> a) -> GE a -> a -fromGE _ (Result _ a) = a -fromGE a (GenError [] e) = a e -fromGE a (GenError es e) = a $ foldr1 (<>) es <> e -fromGE _ (FatalError es e) = - error . ("\n" ++) . unlines $ concat (map NE.toList es) ++ (NE.toList e) + -- Perhaps we want to turn fatalError into genError, if mode_ is Loose? + explain e (GenT f) = GenT $ \(mode, es) -> fmap (explain e) (f (mode, es)) -errorGE :: GE a -> a -errorGE mge = case mge of - (FatalError xs x) -> error $ concat (map f (reverse (x : xs))) - (GenError xs x) -> error $ concat (map f (reverse (x : xs))) - (Result _ x) -> x +-- Perhaps we want to turn fatalError into genError, if mode_ is Loose? + +-- ==================================================== +-- useful operations on NonEmpty + +add :: NonEmpty a -> [NonEmpty a] -> NonEmpty (NonEmpty a) +add a [] = pure a +add a (x : xs) = a <| (x :| xs) + +cat :: NonEmpty (NonEmpty a) -> [NonEmpty a] -> NonEmpty (NonEmpty a) +cat a [] = a +cat a (x : xs) = a <> (x :| xs) + +-- | Similar to (concat :: [[x]] -> [x]) for lists +concatNE :: NonEmpty (NonEmpty t) -> NonEmpty t +concatNE (x :| []) = x +concatNE (x :| (y : ys)) = x <> concatNE (y :| ys) + +-- | Sometimes we have a bunch of genError or fatalError +-- messages we want to combine into one big message. +-- This happens when we want to lift one of these into an input for 'error' +-- We use 'reverse' since messages are accumulated backwards. +catMessages :: (NonEmpty (NonEmpty String)) -> String +catMessages xs = unlines (reverse (NE.toList (catMessageList xs))) + +-- | Turn each inner (NonEmpty String) into a String +catMessageList :: (NonEmpty (NonEmpty String)) -> NonEmpty String +catMessageList xs = fmap sh xs where - f x = unlines (NE.toList x) ++ "\n" + sh x = unlines (NE.toList x) + +-- ======================================================== +-- Useful operations on GE + +-- If none of the GE's are FatalError, then concat together all the +-- Result's (skipping over GenError). If there is at least one +-- (FatalError xs) abort, and lift all those 'xs' as errors in the monad 'm' +catGEs :: forall m a. MonadGenError m => [GE a] -> m [a] +catGEs [] = pure [] +catGEs (g : ges) = + case g of + Result a -> (a :) <$> catGEs ges + GenError _ -> catGEs ges + FatalError xs -> fatalErrors xs + +-- | Given a function for handling GenError, +-- and handling FatalError by using 'error' +-- Turn (GE a) into 'a' +fromGE :: ((NonEmpty (NonEmpty String)) -> a) -> GE a -> a +fromGE f ge = case ge of + (Result a) -> a + (GenError xs) -> f xs + (FatalError es) -> error $ catMessages es + +-- | Turn (GE a) into a +-- both GenError and FatalErrors are handled by using 'error' +errorGE :: GE a -> a +errorGE ge = case ge of + (FatalError xs) -> error $ catMessages xs + (GenError xs) -> error $ catMessages xs + (Result x) -> x isOk :: GE a -> Bool -isOk GenError {} = False -isOk FatalError {} = False -isOk Result {} = True +isOk ge = case ge of + GenError {} -> False + FatalError {} -> False + Result {} -> True -runGE :: MonadGenError m => GE r -> m r -runGE (GenError es err) = foldr explain (genError err) es -runGE (FatalError es err) = foldr explain (fatalError err) es -runGE (Result es a) = foldr explain (pure a) es +runGE :: forall m r. MonadGenError m => GE r -> m r +runGE ge = case ge of + GenError es -> genErrors es + FatalError es -> fatalErrors es + Result a -> pure a fromGEProp :: Testable p => GE p -> Property -fromGEProp (GenError es err) = - foldr (counterexample . unlines) (counterexample (unlines (NE.toList err)) False) (map NE.toList es) -fromGEProp (FatalError es err) = - foldr (counterexample . unlines) (counterexample (unlines (NE.toList err)) False) (map NE.toList es) -fromGEProp (Result es p) = foldr (counterexample . unlines) (property p) (map NE.toList es) +fromGEProp ge = case ge of + GenError es -> counterexample (catMessages es) False + FatalError es -> counterexample (catMessages es) False + Result p -> property p fromGEDiscard :: Testable p => GE p -> Property -fromGEDiscard (Result es p) = foldr (counterexample . unlines . NE.toList) (property p) es -fromGEDiscard _ = discard +fromGEDiscard ge = case ge of + Result p -> property p + _ -> discard headGE :: Foldable t => t a -> GE a headGE t @@ -147,50 +237,24 @@ headGE t listFromGE :: GE [a] -> [a] listFromGE = fromGE (const []) . explain1 "listFromGE" ------------------------------------------------------------------------- --- GenT ------------------------------------------------------------------------- - --- | Generation mode - how strict are we about requiring the generator to --- succeed. This is necessary because sometimes failing to find a value means --- there is an actual problem (a generator _should_ be satisfiable but for --- whatever buggy reason it isn't) and sometimes failing to find a value just --- means there are no values. The latter case is very relevant when you're --- generating e.g. lists or sets of values that can be empty. -data GenMode - = Loose - | Strict - deriving (Ord, Eq, Show) - --- TODO: put a global suchThat fuel parameter in here? To avoid exponential blowup of nested such --- thats? -newtype GenT m a = GenT {runGenT :: GenMode -> Gen (m a)} - deriving (Functor) - -instance Monad m => Applicative (GenT m) where - pure x = GenT $ \_ -> pure (pure x) - (<*>) = ap - -instance Monad m => Monad (GenT m) where - GenT m >>= k = GenT $ \mode -> MkGen $ \r n -> do - a <- unGen (m mode) (left r) n - unGen (runGenT (k a) mode) (right r) n +-- ======================================================== +-- Useful operations on GenT strictGen :: GenT m a -> Gen (m a) -strictGen gen = runGenT gen Strict +strictGen genT = runGenT genT (Strict, []) genFromGenT :: GenT GE a -> Gen a -genFromGenT genT = errorGE <$> runGenT genT Strict +genFromGenT genT = errorGE <$> runGenT genT (Strict, []) resizeT :: (Int -> Int) -> GenT m a -> GenT m a -resizeT f (GenT gm) = GenT $ \mode -> sized $ \sz -> resize (f sz) (gm mode) +resizeT f (GenT gm) = GenT $ \pair -> sized $ \sz -> resize (f sz) (gm pair) pureGen :: Applicative m => Gen a -> GenT m a pureGen gen = GenT $ \_ -> pure <$> gen listOfT :: MonadGenError m => GenT GE a -> GenT m [a] listOfT gen = do - lst <- pureGen . listOf $ runGenT gen Loose + lst <- pureGen . listOf $ runGenT gen (Loose, []) catGEs lst -- | Generate a list of elements of length at most `goalLen`, but accepting failure @@ -202,16 +266,16 @@ listOfUntilLenT gen goalLen validLen = genList `suchThatT` validLen . length where genList = do - res <- pureGen . vectorOf goalLen $ runGenT gen Loose + res <- pureGen . vectorOf goalLen $ runGenT gen (Loose, []) catGEs res vectorOfT :: MonadGenError m => Int -> GenT GE a -> GenT m [a] vectorOfT i gen = GenT $ \mode -> do - res <- fmap sequence . vectorOf i $ runGenT gen Strict + res <- fmap sequence . vectorOf i $ runGenT gen (Strict, []) case mode of - Strict -> pure $ runGE res - Loose -> case res of - FatalError es e -> pure $ runGE (GenError es e) + (Strict, _) -> pure $ runGE res + (Loose, _) -> case res of + FatalError es -> pure $ genErrors es _ -> pure $ runGE res infixl 2 `suchThatT` @@ -235,25 +299,30 @@ scaleT :: (Int -> Int) -> GenT m a -> GenT m a scaleT sc (GenT gen) = GenT $ \mode -> scale sc $ gen mode getMode :: Applicative m => GenT m GenMode -getMode = GenT $ \mode -> pure (pure mode) +getMode = GenT $ \(mode, _) -> pure (pure mode) + +getMess :: Applicative m => GenT m [NonEmpty String] +getMess = GenT $ \(_, msgs) -> pure (pure msgs) withMode :: GenMode -> GenT m a -> GenT m a -withMode mode gen = GenT $ \_ -> runGenT gen mode +withMode mode gen = GenT $ \(_, msgs) -> runGenT gen (mode, msgs) oneofT :: MonadGenError m => [GenT GE a] -> GenT m a oneofT gs = do mode <- getMode + mess <- getMess r <- explain (pure "suchThatT in oneofT") $ - pureGen (oneof [runGenT g mode | g <- gs]) `suchThatT` isOk + pureGen (oneof [runGenT g (mode, mess) | g <- gs]) `suchThatT` isOk runGE r frequencyT :: MonadGenError m => [(Int, GenT GE a)] -> GenT m a frequencyT gs = do mode <- getMode + mess <- getMess r <- explain (pure "suchThatT in oneofT") $ - pureGen (frequency [(f, runGenT g mode) | (f, g) <- gs]) `suchThatT` isOk + pureGen (frequency [(f, runGenT g (mode, mess)) | (f, g) <- gs]) `suchThatT` isOk runGE r chooseT :: (Random a, Ord a, Show a, MonadGenError m) => (a, a) -> GenT m a @@ -262,7 +331,7 @@ chooseT (a, b) | otherwise = pureGen $ choose (a, b) sizeT :: Monad m => GenT m Int -sizeT = GenT $ \mode -> sized $ \n -> runGenT (pure n) mode +sizeT = GenT $ \pair -> sized $ \n -> runGenT (pure n) pair -- ================================================================== -- Reflective analysis of the internal GE structure of (GenT GE x) @@ -273,36 +342,38 @@ sizeT = GenT $ \mode -> sized $ \n -> runGenT (pure n) mode inspect :: forall m x. MonadGenError m => GenT GE x -> GenT m (GE x) inspect (GenT f) = GenT g where - g mode = do result <- f mode; pure @Gen (pure @m result) + g pair = do result <- f pair; pure @Gen (pure @m result) -- | Ignore all kinds of Errors, by squashing them into Nothing tryGenT :: MonadGenError m => GenT GE a -> GenT m (Maybe a) tryGenT g = do r <- inspect g case r of - FatalError _ _ -> pure Nothing - GenError _ _ -> pure Nothing - Result es a -> explain (foldr1 (<>) es) (pure $ Just a) + FatalError _ -> pure Nothing + GenError _ -> pure Nothing + Result a -> pure $ Just a -- Pass on the error messages of both kinds of Errors, by squashing and combining both of them into Left constructor -catchGenT :: MonadGenError m => GenT GE a -> GenT m (Either (NE.NonEmpty String) a) +catchGenT :: MonadGenError m => GenT GE a -> GenT m (Either (NonEmpty (NonEmpty String)) a) catchGenT g = do r <- inspect g case r of - FatalError es e -> pure $ Left (foldr1 (<>) es <> e) - GenError es e -> pure $ Left (foldr1 (<>) es <> e) - Result es a -> explain (foldr1 (<>) es) (pure $ Right a) + FatalError es -> pure $ Left es + GenError es -> pure $ Left es + Result a -> pure $ Right a --- Pass on the error messages of both kinds of Errors in the Gen (not the GenT) monad -catchGen :: GenT GE a -> Gen (Either (NE.NonEmpty String) a) +-- | Pass on the error messages of both kinds of Errors in the Gen (not the GenT) monad +catchGen :: GenT GE a -> Gen (Either (NonEmpty (NonEmpty String)) a) catchGen g = genFromGenT (catchGenT g) -- | Return the first successfull result from a list of computations, if they all fail -- return a list of the error messages from each one. -firstGenT :: forall m a. MonadGenError m => [GenT GE a] -> GenT m (Either [NE.NonEmpty String] a) +firstGenT :: + forall m a. MonadGenError m => [GenT GE a] -> GenT m (Either [(NonEmpty (NonEmpty String))] a) firstGenT gs = loop gs [] where - loop :: [GenT GE a] -> [NE.NonEmpty String] -> GenT m (Either [NE.NonEmpty String] a) + loop :: + [GenT GE a] -> [(NonEmpty (NonEmpty String))] -> GenT m (Either [(NonEmpty (NonEmpty String))] a) loop [] ys = pure (Left (reverse ys)) loop (x : xs) ys = do this <- catchGenT x @@ -313,15 +384,16 @@ firstGenT gs = loop gs [] liftGen :: forall x. (forall m. MonadGenError m => GenT m x) -> GenT GE x liftGen x = x --- Drop a (GenT GE) computation into a (GenT m) computation. Some error information --- is lost, as the two components of FatalError and GenError are folded into one component. +-- Drop a (GenT GE) computation into a (GenT m) computation. +-- Depending on the monad 'm' Some error information might be lost as +-- the monad m might fold FatalError's and GenError's together. dropGen :: MonadGenError m => GenT GE a -> GenT m a dropGen y = do r <- inspect y case r of - FatalError es e -> fatalError (foldr1 (<>) es <> e) - GenError es e -> genError (foldr1 (<>) es <> e) - Result es a -> explain (foldr1 (<>) es) (pure a) + FatalError es -> fatalErrors es + GenError es -> genErrors es + Result a -> pure a -- | Run one of the actions with frequency proportional to the count. If it fails, run the other. frequency2 :: forall m a. MonadGenError m => (Int, GenT GE a) -> (Int, GenT GE a) -> GenT m a @@ -338,23 +410,14 @@ frequency2 (n, g1) (m, g2) -- ====================================== --- | Temporarily extend the stack while executing 'm', and revert to the old stack if successful +-- | like explain for GenT, but uses [String] rather than (NonEmpty String) +-- if the list is null, it becomes the identity push :: forall m a. MonadGenError m => [String] -> GenT GE a -> GenT m a push [] m = dropGen m -push (x : xs) m = - case explain (x NE.:| xs) m of - GenT f -> (GenT g) - where - g :: GenMode -> Gen (m a) - g mode = do - result <- f mode - case result of - Result (_ : ys) a -> pure $ runGE (Result ys a) - other -> pure $ runGE other +push (x : xs) m = dropGen $ explain (x :| xs) m +-- | like explain for GE, but uses [String] rather than (NonEmpty String) +-- if the list is null, it becomes the identity pushGE :: forall a. [String] -> GE a -> GE a pushGE [] x = x -pushGE (x : xs) m = do - case explain (x NE.:| xs) m of - Result (_ : ys) a -> Result ys a - other -> other +pushGE (x : xs) m = explain (x :| xs) m diff --git a/libs/constrained-generators/src/Constrained/Properties.hs b/libs/constrained-generators/src/Constrained/Properties.hs index 0f78cc77c0a..00315605052 100644 --- a/libs/constrained-generators/src/Constrained/Properties.hs +++ b/libs/constrained-generators/src/Constrained/Properties.hs @@ -51,7 +51,7 @@ prop_sound :: prop_sound spec = QC.forAllBlind (strictGen $ genFromSpecT spec) $ \ma -> case ma of - Result _ a -> + Result a -> QC.cover 80 True "successful" $ QC.counterexample (show a) $ monitorSpec spec a $