Change the structure of the GenT monad, to better track explanations. (#4838)

* Added Constrained.SumList.hs to repo
Defined pickAll the basis of sums with fixed length.
Added getSizedList as a method of the Foldy class
getSizeList cost is metered at 1000 calls. Typical calls are less than 10.
Gave HasSpec (optional) method 'typeSpecHasError' a better default value

* Changed the monad in Constrained.GenT to use reader instead of state.

Author: TimSheard

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs

@@ -428,13 +428,13 @@ conformsToImpl = property @(ImpTestM era Property) . (`runContT` pure) $ do
     forAllSpec spec = do
       let
         simplifiedSpec = simplifySpec spec
-        generator = CV2.runGenT (CV2.genFromSpecT simplifiedSpec) Loose
-        shrinker (Result _ x) = pure <$> shrinkWithSpec simplifiedSpec x
+        generator = CV2.runGenT (CV2.genFromSpecT simplifiedSpec) Loose []
+        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"

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]
@@ -1167,8 +1167,7 @@ genFromSpecT (simplifySpec -> spec) = case spec of
           [ "genFromSpecT on (TypeSpec tspec cant) at type " ++ showType @a
           , "tspec = "
           , show s
-          , "cant = "
-          , unlines (map (\x -> "  " ++ show x) cant)
+          , "cant = " ++ show (short cant)
           , "with mode " ++ show mode
           ]
       )
@@ -1196,7 +1195,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 +1291,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 +1308,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 +1518,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 +1607,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 +1760,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 +1885,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`.
 --
@@ -5636,7 +5637,7 @@ showType :: forall t. Typeable t => String
 showType = show (typeRep (Proxy @t))
 
 prettyType :: forall t x. Typeable t => Doc x
-prettyType = fromString $ showType @t
+prettyType = fromString $ show (typeRep (Proxy @t))
 
 instance HasSpec fn a => Pretty (Term fn a) where
   pretty = prettyPrec 0
@@ -6236,11 +6237,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 =>
@@ -6249,7 +6252,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

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)
@@ -141,14 +140,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 ::