[ new ] Add a coverage labeller for hand-written generators

src/Test/DepTyCheck/Gen/Coverage.idr

@@ -101,6 +101,28 @@ export %macro
 initCoverageInfo : (0 x : g) -> Elab $ CoverageGenInfo x
 initCoverageInfo _ = genTypeName g >>= coverageGenInfo
 
+export %macro
+withCoverage : {em : _} -> (gen : Gen em a) -> Elab $ Gen em a
+withCoverage gen = do
+  tyExpr <- quote a
+  let (dpairLefts, tyExpr) = unDPair tyExpr
+  let (IVar _ tyName, _) = unApp tyExpr
+    | (genTy, _) => failAt (getFC genTy) "Expected a normal type name"
+  tyInfo <- getInfo' tyName
+  tyLabelStr <- quote "\{show tyName}[?]"
+  let matchCon = \con => reAppAny (var con.name) $ con.args <&> flip appArg implicitTrue
+  let matchDPair = \expr => foldr (\_, r => var "Builtin.DPair.MkDPair" .$ implicitTrue .$ r) expr dpairLefts
+  labeller <- check `(\val => Test.DepTyCheck.Gen.label (fromString ~tyLabelStr) ~(
+                iCase (var "val") implicitTrue $ tyInfo.cons <&> \con =>
+                  patClause
+                    (as `{x} $ matchDPair $ matchCon con)
+                    (var "Test.DepTyCheck.Gen.label"
+                      .$ (var "fromString" .$ primVal (Str "\{show con.name} (user-defined)"))
+                      .$ `(pure x)
+                    )
+              ))
+  pure $ gen >>= labeller
+
 export
 Show (CoverageGenInfo g) where
   show cgi = joinBy "\n\n" $ SortedMap.toList cgi.coverageInfo <&> \(ti, tyCov, cons) => do

tests/lib/coverage/types-and-cons-003/PrintCoverage.idr

@@ -0,0 +1,40 @@
+module PrintCoverage
+
+import Test.DepTyCheck.Gen
+import Test.DepTyCheck.Gen.Coverage
+
+import Deriving.DepTyCheck.Gen
+
+import System.Random.Pure.StdGen
+
+%default total
+
+%language ElabReflection
+
+export
+smallStrs : Fuel -> Gen NonEmpty String
+smallStrs _ = elements ["", "a", "bc"]
+
+data X = X1 | X2 Nat | X3 String
+
+genX : Fuel -> Gen NonEmpty X
+genX fl = oneOf
+  [ pure X1
+  , X3 <$> smallStrs fl
+  ]
+
+data Y = Y1 | Y2 X | Y3 X X
+
+genY : Fuel -> Gen NonEmpty Y
+genY fl = withCoverage $ oneOf
+  [ [| Y1 |]
+  , [| Y3 (genX fl) (genX fl) |]
+  ]
+
+main : IO ()
+main = do
+  let ci = initCoverageInfo genY
+  let vs = unGenTryND 100 someStdGen $ genY $ limit 10
+  let mc = concatMap fst vs
+  let ci = registerCoverage mc ci
+  putStrLn $ show ci

tests/lib/coverage/types-and-cons-003/expected

@@ -0,0 +1,15 @@
+1/1: Building PrintCoverage (PrintCoverage.idr)
+
+Prelude.Types.Nat not covered
+  - S: not covered
+  - Z: not covered
+
+PrintCoverage.X not covered
+  - X1: not covered
+  - X2: not covered
+  - X3: not covered
+
+PrintCoverage.Y covered partially
+  - Y1: covered
+  - Y2: not covered
+  - Y3: covered

tests/lib/coverage/types-and-cons-003/run

@@ -0,0 +1,8 @@
+rm -rf build
+
+flock "$1" pack -q install-deps test.ipkg && \
+idris2 --no-color --console-width 0 --no-banner --find-ipkg --check PrintCoverage.idr && \
+echo && \
+pack exec PrintCoverage.idr
+
+rm -rf build

tests/lib/coverage/types-and-cons-003/test.ipkg

@@ -0,0 +1,6 @@
+package a-test
+executable = a-test
+
+depends = deptycheck
+
+main = PrintCoverage

tests/lib/coverage/types-and-cons-004/PrintCoverage.idr

@@ -0,0 +1,40 @@
+module PrintCoverage
+
+import Test.DepTyCheck.Gen
+import Test.DepTyCheck.Gen.Coverage
+
+import Deriving.DepTyCheck.Gen
+
+import System.Random.Pure.StdGen
+
+%default total
+
+%language ElabReflection
+
+export
+smallStrs : Fuel -> Gen NonEmpty String
+smallStrs _ = elements ["", "a", "bc"]
+
+data X = X1 | X2 Nat | X3 String
+
+genX : Fuel -> Gen NonEmpty X
+genX fl = withCoverage $ oneOf
+  [ pure X1
+  , X3 <$> smallStrs fl
+  ]
+
+data Y = Y1 | Y2 X | Y3 X X
+
+genY : Fuel -> Gen NonEmpty Y
+genY fl = withCoverage $ oneOf
+  [ [| Y1 |]
+  , [| Y3 (genX fl) (genX fl) |]
+  ]
+
+main : IO ()
+main = do
+  let ci = initCoverageInfo genY
+  let vs = unGenTryND 100 someStdGen $ genY $ limit 10
+  let mc = concatMap fst vs
+  let ci = registerCoverage mc ci
+  putStrLn $ show ci

tests/lib/coverage/types-and-cons-004/expected

@@ -0,0 +1,15 @@
+1/1: Building PrintCoverage (PrintCoverage.idr)
+
+Prelude.Types.Nat not covered
+  - S: not covered
+  - Z: not covered
+
+PrintCoverage.X covered partially
+  - X1: covered
+  - X2: not covered
+  - X3: covered
+
+PrintCoverage.Y covered partially
+  - Y1: covered
+  - Y2: not covered
+  - Y3: covered

tests/lib/coverage/types-and-cons-004/run

@@ -0,0 +1,8 @@
+rm -rf build
+
+flock "$1" pack -q install-deps test.ipkg && \
+idris2 --no-color --console-width 0 --no-banner --find-ipkg --check PrintCoverage.idr && \
+echo && \
+pack exec PrintCoverage.idr
+
+rm -rf build

tests/lib/coverage/types-and-cons-004/test.ipkg

@@ -0,0 +1,6 @@
+package a-test
+executable = a-test
+
+depends = deptycheck
+
+main = PrintCoverage

tests/lib/coverage/types-and-cons-005/PrintCoverage.idr

@@ -0,0 +1,43 @@
+module PrintCoverage
+
+import Test.DepTyCheck.Gen
+import Test.DepTyCheck.Gen.Coverage
+
+import Deriving.DepTyCheck.Gen
+
+import System.Random.Pure.StdGen
+
+%default total
+
+%language ElabReflection
+
+export
+smallStrs : Fuel -> Gen NonEmpty String
+smallStrs _ = elements ["", "a", "bc"]
+
+data X = X1 | X2 Nat | X3 String
+
+genX : Fuel -> Gen NonEmpty X
+genX fl = withCoverage $ oneOf
+  [ pure X1
+  , X3 <$> smallStrs fl
+  ]
+
+data Y : Nat -> Type where
+  Y1 : Y 0
+  Y2 : X -> Y 1
+  Y3 : X -> X -> Y 2
+
+genY : Fuel -> Gen NonEmpty (n ** Y n)
+genY fl = withCoverage $ oneOf
+  [ pure (_ ** Y1)
+  , [| (\x1, x2 => (_ ** Y3 x1 x2)) (genX fl) (genX fl) |]
+  ]
+
+main : IO ()
+main = do
+  let ci = initCoverageInfo genY
+  let vs = unGenTryND 100 someStdGen $ genY $ limit 10
+  let mc = concatMap fst vs
+  let ci = registerCoverage mc ci
+  putStrLn $ show ci

tests/lib/coverage/types-and-cons-005/expected

@@ -0,0 +1,15 @@
+1/1: Building PrintCoverage (PrintCoverage.idr)
+
+Prelude.Types.Nat not covered
+  - S: not covered
+  - Z: not covered
+
+PrintCoverage.X covered partially
+  - X1: covered
+  - X2: not covered
+  - X3: covered
+
+PrintCoverage.Y covered partially
+  - Y1: covered
+  - Y2: not covered
+  - Y3: covered

tests/lib/coverage/types-and-cons-005/run

@@ -0,0 +1,8 @@
+rm -rf build
+
+flock "$1" pack -q install-deps test.ipkg && \
+idris2 --no-color --console-width 0 --no-banner --find-ipkg --check PrintCoverage.idr && \
+echo && \
+pack exec PrintCoverage.idr
+
+rm -rf build

tests/lib/coverage/types-and-cons-005/test.ipkg

@@ -0,0 +1,6 @@
+package a-test
+executable = a-test
+
+depends = deptycheck
+
+main = PrintCoverage

tests/lib/coverage/types-and-cons-006/PrintCoverage.idr

@@ -0,0 +1,53 @@
+module PrintCoverage
+
+import Test.DepTyCheck.Gen
+import Test.DepTyCheck.Gen.Coverage
+
+import Deriving.DepTyCheck.Gen
+
+import System.Random.Pure.StdGen
+
+%default total
+
+%language ElabReflection
+
+export
+smallStrs : Fuel -> Gen NonEmpty String
+smallStrs _ = elements ["", "a", "bc"]
+
+data X = X1 | X2 Nat | X3 String
+
+genX : Fuel -> Gen NonEmpty X
+genX fl = withCoverage $ oneOf
+  [ pure X1
+  , X3 <$> smallStrs fl
+  ]
+
+data Y : Nat -> Type where
+  Y1 : Y 0
+  Y2 : X -> Y 1
+  Y3 : X -> X -> Y n
+
+genY' : Fuel -> (n : _) -> Gen NonEmpty $ Y n
+genY' fl Z = oneOf
+  [ [| Y1 |]
+  , [| Y3 (genX fl) (genX fl) |]
+  ]
+genY' fl 1 = [| Y2 (genX fl) |]
+genY' fl n = [| Y3 (genX fl) (genX fl) |]
+
+genY : Fuel -> (n : _) -> Gen NonEmpty $ Y n
+genY fl n = withCoverage $ genY' fl n
+
+main : IO ()
+main = do
+  let ci = initCoverageInfo genY
+  do let vs = unGenTryND 100 someStdGen $ genY (limit 10) 0
+     let mc = concatMap fst vs
+     let ci = registerCoverage mc ci
+     putStrLn $ show ci
+  putStrLn "\n--------\n"
+  do let vs = unGenTryND 100 someStdGen $ genY (limit 10) 3
+     let mc = concatMap fst vs
+     let ci = registerCoverage mc ci
+     putStrLn $ show ci

tests/lib/coverage/types-and-cons-006/expected

@@ -0,0 +1,31 @@
+1/1: Building PrintCoverage (PrintCoverage.idr)
+
+Prelude.Types.Nat not covered
+  - S: not covered
+  - Z: not covered
+
+PrintCoverage.X covered partially
+  - X1: covered
+  - X2: not covered
+  - X3: covered
+
+PrintCoverage.Y covered partially
+  - Y1: covered
+  - Y2: not covered
+  - Y3: covered
+
+--------
+
+Prelude.Types.Nat not covered
+  - S: not covered
+  - Z: not covered
+
+PrintCoverage.X covered partially
+  - X1: covered
+  - X2: not covered
+  - X3: covered
+
+PrintCoverage.Y covered partially
+  - Y1: not covered
+  - Y2: not covered
+  - Y3: covered

tests/lib/coverage/types-and-cons-006/run

@@ -0,0 +1,8 @@
+rm -rf build
+
+flock "$1" pack -q install-deps test.ipkg && \
+idris2 --no-color --console-width 0 --no-banner --find-ipkg --check PrintCoverage.idr && \
+echo && \
+pack exec PrintCoverage.idr
+
+rm -rf build

tests/lib/coverage/types-and-cons-006/test.ipkg

@@ -0,0 +1,6 @@
+package a-test
+executable = a-test
+
+depends = deptycheck
+
+main = PrintCoverage