[ gen ] Add an associative binary composition fun merging alternatives

src/Test/DepTyCheck/Gen.idr

@@ -507,6 +507,15 @@ elements' xs = elements $ relaxF $ fromList $ toList xs
 --- Analysis of generators ---
 ------------------------------
 
+||| Shallow alternatives of a generator.
+|||
+||| If the given generator is made by one of `oneOf`, `frequency` or `elements`,
+||| this function returns alternatives which this generators contains.
+||| Otherwise it retuns a single-element alternative list containing given generator.
+|||
+||| In a sense, this function is a reverse function of `oneOf`, i.g.
+||| `oneOf $ alternativesOf g` must be equivalent to `g` and
+||| `alternativesof $ oneOf gs` must be equivalent to `gs`.
 export
 alternativesOf : {em : _} -> Gen em a -> GenAlternatives True em a
 alternativesOf $ OneOf oo     = MkGenAlts $ unGenAlts $ mapOneOf oo relax
@@ -585,6 +594,48 @@ export
 {em : _} -> Monad (GenAlternatives True em) where
   xs >>= f = flip processAlternatives' xs $ alternativesOf . (>>= oneOf . f)
 
+----------------------------------------
+--- Additional composition functions ---
+----------------------------------------
+
+||| Associative composition of two generators, merging shallow alternatives of given two generators
+|||
+||| This operation being applied to arguments `a` and `b` is *not* the same as `oneOf [a, b]`.
+||| Generator ``a `withAlts` b`` has equal probabilities of all shallow alternatives of generators `a` and `b`.
+||| For example, when there are generators
+||| ```idris
+||| g1 = oneOf [elems [0, 1, 2, 3], elems [4, 5]]
+||| g2 = oneOf elemts [10, 11, 12, 13, 14, 15]
+||| ```
+||| generator ``g1 `withAlts` g2`` would be equivalent to
+||| `oneOf [elems [0, 1, 2, 3], elems [4, 5], pure 10, pure 11, pure 12, pure 13, pure 14, pure 15]`.
+|||
+||| In other words, ``a `withAlts` b`` must be equivalent to `oneOf $ alternativesOf a ++ alternativesOf b`.
+export %inline
+withAlts : {em : _} -> Gen em a -> Gen em a -> Gen em a
+a `withAlts` b = oneOf $ alternativesOf a ++ alternativesOf b
+
+-- As of `<|>`
+export
+infixr 2 `withAlts`
+
+||| Associative composition of two generators, merging deep alternatives of given two generators
+|||
+||| This operation being applied to arguments `a` and `b` is *not* the same as `oneOf [a, b]`.
+||| Generator ``a `withDeepAlts` b`` has equal probabilities of all deep alternatives of generators `a` and `b`.
+||| For example, when there are generators
+||| ```idris
+||| g1 = oneOf [elems [0, 1, 2, 3], elems [4, 5]]
+||| g2 = oneOf elemts [10, 11, 12, 13, 14, 15]
+||| ```
+||| generator ``withDeepAlts n g1 g2`` with `n >= 2` would be equivalent to
+||| `oneOf elements [0, 1, 2, 3, 4, 5, 10, 11, 12, 13, 14, 15]`.
+|||
+||| In other words, ``withDeepAlts d a b`` must be equivalent to `oneOf $ deepAlternativesOf d a ++ deepAlternativesOf d b`.
+export %inline
+withDeepAlts : {em : _} -> (depth : Nat) -> Gen em a -> Gen em a -> Gen em a
+withDeepAlts depth a b = oneOf $ deepAlternativesOf depth a ++ deepAlternativesOf depth b
+
 -----------------
 --- Filtering ---
 -----------------

tests/lib/distribution/_common/DistrCheckCommon.idr

@@ -17,12 +17,12 @@ find (x::xs) = case force xs of
                  [] => Just x
                  xs => if all isOk x then Just x else assert_total $ find xs
 
-verdict : Vect n (CoverageTest a) -> Gen MaybeEmpty a -> Maybe $ Vect n SignificantBounds
+verdict : Vect n (CoverageTest a) -> Gen em a -> Maybe $ Vect n SignificantBounds
 verdict conds = find . mapMaybe sequence .
                   checkCoverageConditions conds . unGenTryN 10000000 someStdGen
 
 Show SignificantBounds where show = interpolate
 
 export
-printVerdict : HasIO m => Gen MaybeEmpty a -> Vect n (CoverageTest a) -> m ()
+printVerdict : HasIO m => Gen em a -> Vect n (CoverageTest a) -> m ()
 printVerdict = putStrLn .: show .: flip verdict

tests/lib/distribution/with-alts-deep-001/CheckDistribution.idr

@@ -0,0 +1,35 @@
+module CheckDistribution
+
+import Data.Either
+
+import DistrCheckCommon
+
+%default total
+
+g1 : Gen NonEmpty Nat
+g1 = oneOf
+       [ elements [0, 1, 2, 3]
+       , elements [4, 5]
+       ]
+
+g2 : Gen NonEmpty Nat
+g2 = elements [10, 11, 12, 13, 14, 15]
+
+g12 : Gen NonEmpty Nat
+g12 = withDeepAlts 2 g1 g2
+
+main : IO ()
+main = printVerdict g12
+         [ coverWith 8.3.percent (== 0)
+         , coverWith 8.3.percent (== 1)
+         , coverWith 8.3.percent (== 2)
+         , coverWith 8.3.percent (== 3)
+         , coverWith 8.3.percent (== 4)
+         , coverWith 8.3.percent (== 5)
+         , coverWith 8.3.percent (== 10)
+         , coverWith 8.3.percent (== 11)
+         , coverWith 8.3.percent (== 12)
+         , coverWith 8.3.percent (== 13)
+         , coverWith 8.3.percent (== 14)
+         , coverWith 8.3.percent (== 15)
+         ]

tests/lib/distribution/with-alts-deep-001/DistrCheckCommon.idr

@@ -0,0 +1 @@
+../_common/DistrCheckCommon.idr

tests/lib/distribution/with-alts-deep-001/expected

@@ -0,0 +1 @@
+Just [ok, ok, ok, ok, ok, ok, ok, ok, ok, ok, ok, ok]

tests/lib/distribution/with-alts-deep-001/run

@@ -0,0 +1 @@
+../_common/run

tests/lib/distribution/with-alts-deep-001/test.ipkg

@@ -0,0 +1 @@
+../_common/test.ipkg

tests/lib/distribution/with-alts-shallow-001/CheckDistribution.idr

@@ -0,0 +1,37 @@
+module CheckDistribution
+
+import Data.Either
+
+import DistrCheckCommon
+
+%default total
+
+g1 : Gen NonEmpty Nat
+g1 = oneOf
+       [ elements [0, 1, 2, 3]
+       , elements [4, 5]
+       ]
+
+g2 : Gen NonEmpty Nat
+g2 = elements [10, 11, 12, 13, 14, 15]
+
+g12 : Gen NonEmpty Nat
+g12 = g1 `withAlts` g2
+
+main : IO ()
+main = printVerdict g12
+         [ coverWith 3.125.percent (== 0)
+         , coverWith 3.125.percent (== 1)
+         , coverWith 3.125.percent (== 2)
+         , coverWith 3.125.percent (== 3)
+
+         , coverWith 6.25.percent (== 4)
+         , coverWith 6.25.percent (== 5)
+
+         , coverWith 12.5.percent (== 10)
+         , coverWith 12.5.percent (== 11)
+         , coverWith 12.5.percent (== 12)
+         , coverWith 12.5.percent (== 13)
+         , coverWith 12.5.percent (== 14)
+         , coverWith 12.5.percent (== 15)
+         ]

tests/lib/distribution/with-alts-shallow-001/DistrCheckCommon.idr

@@ -0,0 +1 @@
+../_common/DistrCheckCommon.idr

tests/lib/distribution/with-alts-shallow-001/expected

@@ -0,0 +1 @@
+Just [ok, ok, ok, ok, ok, ok, ok, ok, ok, ok, ok, ok]

tests/lib/distribution/with-alts-shallow-001/run

@@ -0,0 +1 @@
+../_common/run

tests/lib/distribution/with-alts-shallow-001/test.ipkg

@@ -0,0 +1 @@
+../_common/test.ipkg