[ new ] Add convenient forAlls function returning an HList (#47)

src/Hedgehog/Internal/Gen.idr

@@ -5,12 +5,14 @@ import Data.Colist
 import Data.Cotree
 import Data.Fin
 import Data.List
+import Data.List.Quantifiers
 import Data.List1
 import Data.Nat
 import Data.SOP
 import Data.String
 import Data.Tree
 import Data.Vect
+import Data.Vect.Quantifiers
 
 import Control.Monad.Maybe
 
@@ -601,6 +603,18 @@ export
 string : Range Nat -> Gen Char -> Gen String
 string range = map fastPack . list range
 
+||| Generates an heterogeneous list being provided a generator for each element
+export
+hlist : All Gen ts -> Gen (HList ts)
+hlist []      = [| [] |]
+hlist (x::xs) = [| x :: hlist xs |]
+
+||| Generates an heterogeneous vect being provided a generator for each element
+export
+hvect : All Gen ts -> Gen (HVect ts)
+hvect []      = [| [] |]
+hvect (x::xs) = [| x :: hvect xs |]
+
 --------------------------------------------------------------------------------
 --          SOP
 --------------------------------------------------------------------------------

src/Hedgehog/Internal/Property.idr

@@ -5,6 +5,7 @@ import Control.Monad.Identity
 import Control.Monad.Trans
 import Control.Monad.Writer
 import Data.Lazy
+import Data.List.Quantifiers
 import public Data.Double.Bounded
 import Data.DPair
 import Derive.Prelude
@@ -416,6 +417,13 @@ export %inline
 annotateShow : Show a => Applicative m => a -> TestT m ()
 annotateShow v = annotate $ ppShow v
 
+||| Annotates the source code with all values separately.
+export
+annotateAllShow : All Show ts => Monad m => HList ts -> TestT m ()
+annotateAllShow         []      = pure ()
+annotateAllShow @{_::_} [x]     = annotateShow x
+annotateAllShow @{_::_} (x::xs) = annotateShow x >> annotateAllShow xs
+
 ||| Logs a message to be displayed as additional information in the footer of
 ||| the failure report.
 export %inline
@@ -544,6 +552,19 @@ export %inline
 forAll : Show a => Gen a -> PropertyT a
 forAll = forAllWith ppShow
 
+||| Generates a random input provided a bunch of generators.
+|||
+||| This function is an easy way to write several foralls in a row.
+||| `[a, b, c] <- forAlls [x, y, z]` prints error message like
+||| `(a, b, c) <- [| (forAll x, forAll y, forAll z) |]` but shrinks like
+||| `(a, b, c) <- forAll [| (x, y, z) |]`.
+export
+forAlls : All Show ts => All Gen ts -> PropertyT (HList ts)
+forAlls gens = do
+  xs <- lift $ lift $ hlist gens
+  annotateAllShow xs
+  pure xs
+
 ||| Lift a test in to a property.
 export
 test : Test a -> PropertyT a

tests/Basic.idr

@@ -1,5 +1,6 @@
 module Basic
 
+import Data.List.Quantifiers
 import Hedgehog.Meta
 
 %default total
@@ -69,6 +70,49 @@ namespace NoShrinkGen
           > recheck
         """
 
+  export
+  forallsPosGeneration : Property
+  forallsPosGeneration = checkGivenOutput expected prop
+
+    where
+      prop : Property
+      prop = property $ do
+        let g = integral_ $ constant 1 999
+        [n, m] <- forAlls [g, g]
+        let _ : Integer := n
+        let _ : Integer := m
+        assert $ n >= 1 && n <= 999
+        assert $ m >= 1 && m <= 999
+      expected : String
+      expected = "✓ <interactive> passed 100 tests."
+
+  export
+  forallsNegGeneration : Property
+  forallsNegGeneration =
+    recheckGivenOutput {checkPrefixOnly=True} expected prop 7 seed
+
+    where
+      seed : StdGen
+      seed = rawStdGen 17390955263926595516 17173145979079339501
+      prop : Property
+      prop = property $ do
+        let g = integral_ $ constant 1 999
+        [n, m] <- forAlls [g, g]
+        let _ : Integer := n
+        let _ : Integer := m
+        assert $ n >= 20 && m >= 20
+      expected : String
+      expected =
+        """
+        ✗ <interactive> failed after 1 test.
+        forAll 0 =
+          5
+        forAll 1 =
+          798
+        This failure can be reproduced by running:
+          > recheck
+        """
+
 namespace ShrinkGen
 
   export
@@ -107,3 +151,54 @@ namespace ShrinkGen
         This failure can be reproduced by running:
           > recheck
         """
+
+  export
+  forallsPosGeneration : Property
+  forallsPosGeneration = checkGivenOutput expected prop
+
+    where
+      prop : Property
+      prop = property $ do
+        let g = integral $ constant 1 999
+        [n, m, k] <- forAlls [g, g, g]
+        let _ : Integer := n
+        let _ : Integer := m
+        let _ : Integer := k
+        assert $ n >= 1 && n <= 999
+        assert $ m >= 1 && m <= 999
+        assert $ k >= 1 && k <= 999
+      expected : String
+      expected = "✓ <interactive> passed 100 tests."
+
+  export
+  forallsNegGeneration : Property
+  forallsNegGeneration =
+    recheckGivenOutput {checkPrefixOnly=True} expected prop 7 seed
+
+    where
+      seed : StdGen
+      seed = rawStdGen 17390955263926595516 17173145979079339501
+
+      prop : Property
+      prop = property $ do
+        let g = integral $ constant 1 999
+        [n, m, k] <- forAlls [g, g, g]
+        let _ : Integer := n
+        let _ : Integer := m
+        let _ : Integer := k
+        assert $ n >= 20
+        assert $ m >= 20
+        assert $ k >= 20
+      expected : String
+      expected =
+        """
+        ✗ <interactive> failed after 1 test.
+        forAll 0 =
+          1
+        forAll 1 =
+          1
+        forAll 2 =
+          1
+        This failure can be reproduced by running:
+          > recheck
+        """

tests/Tests.idr

@@ -20,10 +20,14 @@ main =
     , "basic non-shrinking generation" `MkGroup`
       [ ("simplePosGeneration", Basic.NoShrinkGen.simplePosGeneration)
       , ("simpleNegGeneration", Basic.NoShrinkGen.simpleNegGeneration)
+      , ("forallsPosGeneration", Basic.NoShrinkGen.forallsPosGeneration)
+      , ("forallsNegGeneration", Basic.NoShrinkGen.forallsNegGeneration)
       ]
     , "basic shrinking generation" `MkGroup`
       [ ("simplePosGeneration", Basic.ShrinkGen.simplePosGeneration)
       , ("simpleNegGeneration", Basic.ShrinkGen.simpleNegGeneration)
+      , ("forallsPosGeneration", Basic.ShrinkGen.forallsPosGeneration)
+      , ("forallsNegGeneration", Basic.ShrinkGen.forallsNegGeneration)
       ]
     , "coverage checking" `MkGroup`
       [ ("simpleCoverage", Coverage.simpleCoverage)