From ec70d2fc816597de7fb95578dabad7f3c831cf8c Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Tue, 19 Sep 2023 17:40:04 +0300
Subject: [PATCH] [ fix ] Support dependent types in `withCoverage` macro

---
 src/Test/DepTyCheck/Gen/Coverage.idr          | 16 ++++--
 .../types-and-cons-007/PrintCoverage.idr      | 50 +++++++++++++++++++
 .../lib/coverage/types-and-cons-007/expected  | 31 ++++++++++++
 tests/lib/coverage/types-and-cons-007/run     |  8 +++
 .../lib/coverage/types-and-cons-007/test.ipkg |  6 +++
 5 files changed, 108 insertions(+), 3 deletions(-)
 create mode 100644 tests/lib/coverage/types-and-cons-007/PrintCoverage.idr
 create mode 100644 tests/lib/coverage/types-and-cons-007/expected
 create mode 100755 tests/lib/coverage/types-and-cons-007/run
 create mode 100644 tests/lib/coverage/types-and-cons-007/test.ipkg

diff --git a/src/Test/DepTyCheck/Gen/Coverage.idr b/src/Test/DepTyCheck/Gen/Coverage.idr
index 1b3eb6475..3ae7e2cf0 100644
--- a/src/Test/DepTyCheck/Gen/Coverage.idr
+++ b/src/Test/DepTyCheck/Gen/Coverage.idr
@@ -105,22 +105,32 @@ 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
+  let (dpairLefts, tyRExpr) = unDPair tyExpr
+  let (IVar _ tyName, _) = unApp tyRExpr
     | (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
   let asName = UN $ Basic "^x^"
+  let unitConClause = \con => patClause (matchDPair $ matchCon con) `(Builtin.MkUnit)
   let conClause = \con => patClause
                     (as asName $ matchDPair $ matchCon con)
                     (var "Test.DepTyCheck.Gen.label"
                       .$ (var "fromString" .$ primVal (Str "\{show con.name} (user-defined)"))
                       .$ `(pure ~(var asName))
                     )
+  goodClauses <- for tyInfo.cons $ \con => do
+    let funName = `{conCheckingFun}
+    res <- catch $ check {expected=Unit} $ flip local (var "Builtin.MkUnit")
+             [ claim M0 Private [Totality PartialOK] funName `(~tyExpr -> Builtin.Unit)
+             , def funName $ pure $ patClause (var funName .$ bindVar "var") $
+                 iCase (var "var") implicitTrue [ unitConClause con ]
+             ]
+    pure $ res $> conClause con
+  let goodClauses = mapMaybe id goodClauses
   labeller <- check `(\val => Test.DepTyCheck.Gen.label (fromString ~tyLabelStr) ~(
-                iCase (var "val") implicitTrue $ tyInfo.cons <&> conClause
+                iCase (var "val") implicitTrue goodClauses
               ))
   pure $ gen >>= labeller
 
diff --git a/tests/lib/coverage/types-and-cons-007/PrintCoverage.idr b/tests/lib/coverage/types-and-cons-007/PrintCoverage.idr
new file mode 100644
index 000000000..a9f02ab39
--- /dev/null
+++ b/tests/lib/coverage/types-and-cons-007/PrintCoverage.idr
@@ -0,0 +1,50 @@
+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 = withCoverage $ oneOf
+  [ [| Y1 |]
+  , [| Y3 (genX fl) (genX fl) |]
+  ]
+genY fl 1 = withCoverage [| Y2 (genX fl) |]
+genY fl n = withCoverage [| Y3 (genX fl) (genX fl) |]
+
+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
diff --git a/tests/lib/coverage/types-and-cons-007/expected b/tests/lib/coverage/types-and-cons-007/expected
new file mode 100644
index 000000000..e7ba804c1
--- /dev/null
+++ b/tests/lib/coverage/types-and-cons-007/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
diff --git a/tests/lib/coverage/types-and-cons-007/run b/tests/lib/coverage/types-and-cons-007/run
new file mode 100755
index 000000000..9706b3375
--- /dev/null
+++ b/tests/lib/coverage/types-and-cons-007/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
diff --git a/tests/lib/coverage/types-and-cons-007/test.ipkg b/tests/lib/coverage/types-and-cons-007/test.ipkg
new file mode 100644
index 000000000..879278361
--- /dev/null
+++ b/tests/lib/coverage/types-and-cons-007/test.ipkg
@@ -0,0 +1,6 @@
+package a-test
+executable = a-test
+
+depends = deptycheck
+
+main = PrintCoverage