From 3da632196db8e49a0340be38ddba37c9074c5f54 Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Mon, 2 Sep 2024 18:29:57 +0300 Subject: [PATCH] [ gen ] Add an associative binary composition fun merging alternatives --- src/Test/DepTyCheck/Gen.idr | 51 +++++++++++++++++++ .../distribution/_common/DistrCheckCommon.idr | 4 +- .../with-alts-deep-001/CheckDistribution.idr | 35 +++++++++++++ .../with-alts-deep-001/DistrCheckCommon.idr | 1 + .../distribution/with-alts-deep-001/expected | 1 + tests/lib/distribution/with-alts-deep-001/run | 1 + .../distribution/with-alts-deep-001/test.ipkg | 1 + .../CheckDistribution.idr | 37 ++++++++++++++ .../DistrCheckCommon.idr | 1 + .../with-alts-shallow-001/expected | 1 + .../distribution/with-alts-shallow-001/run | 1 + .../with-alts-shallow-001/test.ipkg | 1 + 12 files changed, 133 insertions(+), 2 deletions(-) create mode 100644 tests/lib/distribution/with-alts-deep-001/CheckDistribution.idr create mode 120000 tests/lib/distribution/with-alts-deep-001/DistrCheckCommon.idr create mode 100644 tests/lib/distribution/with-alts-deep-001/expected create mode 120000 tests/lib/distribution/with-alts-deep-001/run create mode 120000 tests/lib/distribution/with-alts-deep-001/test.ipkg create mode 100644 tests/lib/distribution/with-alts-shallow-001/CheckDistribution.idr create mode 120000 tests/lib/distribution/with-alts-shallow-001/DistrCheckCommon.idr create mode 100644 tests/lib/distribution/with-alts-shallow-001/expected create mode 120000 tests/lib/distribution/with-alts-shallow-001/run create mode 120000 tests/lib/distribution/with-alts-shallow-001/test.ipkg diff --git a/src/Test/DepTyCheck/Gen.idr b/src/Test/DepTyCheck/Gen.idr index 56e8a5d50..d14f37071 100644 --- a/src/Test/DepTyCheck/Gen.idr +++ b/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 --- ----------------- diff --git a/tests/lib/distribution/_common/DistrCheckCommon.idr b/tests/lib/distribution/_common/DistrCheckCommon.idr index 6029809f3..b66f524ca 100644 --- a/tests/lib/distribution/_common/DistrCheckCommon.idr +++ b/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 diff --git a/tests/lib/distribution/with-alts-deep-001/CheckDistribution.idr b/tests/lib/distribution/with-alts-deep-001/CheckDistribution.idr new file mode 100644 index 000000000..5dec965ee --- /dev/null +++ b/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) + ] diff --git a/tests/lib/distribution/with-alts-deep-001/DistrCheckCommon.idr b/tests/lib/distribution/with-alts-deep-001/DistrCheckCommon.idr new file mode 120000 index 000000000..97b34ad55 --- /dev/null +++ b/tests/lib/distribution/with-alts-deep-001/DistrCheckCommon.idr @@ -0,0 +1 @@ +../_common/DistrCheckCommon.idr \ No newline at end of file diff --git a/tests/lib/distribution/with-alts-deep-001/expected b/tests/lib/distribution/with-alts-deep-001/expected new file mode 100644 index 000000000..672c4e48d --- /dev/null +++ b/tests/lib/distribution/with-alts-deep-001/expected @@ -0,0 +1 @@ +Just [ok, ok, ok, ok, ok, ok, ok, ok, ok, ok, ok, ok] diff --git a/tests/lib/distribution/with-alts-deep-001/run b/tests/lib/distribution/with-alts-deep-001/run new file mode 120000 index 000000000..805165988 --- /dev/null +++ b/tests/lib/distribution/with-alts-deep-001/run @@ -0,0 +1 @@ +../_common/run \ No newline at end of file diff --git a/tests/lib/distribution/with-alts-deep-001/test.ipkg b/tests/lib/distribution/with-alts-deep-001/test.ipkg new file mode 120000 index 000000000..7297aae9f --- /dev/null +++ b/tests/lib/distribution/with-alts-deep-001/test.ipkg @@ -0,0 +1 @@ +../_common/test.ipkg \ No newline at end of file diff --git a/tests/lib/distribution/with-alts-shallow-001/CheckDistribution.idr b/tests/lib/distribution/with-alts-shallow-001/CheckDistribution.idr new file mode 100644 index 000000000..d19c4605e --- /dev/null +++ b/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) + ] diff --git a/tests/lib/distribution/with-alts-shallow-001/DistrCheckCommon.idr b/tests/lib/distribution/with-alts-shallow-001/DistrCheckCommon.idr new file mode 120000 index 000000000..97b34ad55 --- /dev/null +++ b/tests/lib/distribution/with-alts-shallow-001/DistrCheckCommon.idr @@ -0,0 +1 @@ +../_common/DistrCheckCommon.idr \ No newline at end of file diff --git a/tests/lib/distribution/with-alts-shallow-001/expected b/tests/lib/distribution/with-alts-shallow-001/expected new file mode 100644 index 000000000..672c4e48d --- /dev/null +++ b/tests/lib/distribution/with-alts-shallow-001/expected @@ -0,0 +1 @@ +Just [ok, ok, ok, ok, ok, ok, ok, ok, ok, ok, ok, ok] diff --git a/tests/lib/distribution/with-alts-shallow-001/run b/tests/lib/distribution/with-alts-shallow-001/run new file mode 120000 index 000000000..805165988 --- /dev/null +++ b/tests/lib/distribution/with-alts-shallow-001/run @@ -0,0 +1 @@ +../_common/run \ No newline at end of file diff --git a/tests/lib/distribution/with-alts-shallow-001/test.ipkg b/tests/lib/distribution/with-alts-shallow-001/test.ipkg new file mode 120000 index 000000000..7297aae9f --- /dev/null +++ b/tests/lib/distribution/with-alts-shallow-001/test.ipkg @@ -0,0 +1 @@ +../_common/test.ipkg \ No newline at end of file