[ mcov ] Support the colouring of the resulting printed model coverage

src/Test/DepTyCheck/Gen/Coverage.idr

@@ -4,6 +4,8 @@
 ||| e.g. involved types and their constructors.
 module Test.DepTyCheck.Gen.Coverage
 
+import Control.ANSI
+
 import Control.Monad.Maybe
 import Control.Monad.Random
 import Control.Monad.Writer
@@ -134,27 +136,42 @@ withCoverage gen = do
               ))
   pure $ gen >>= labeller
 
-toString : CoverageGenInfo g -> String
-toString cgi = joinBy "\n\n" $ SortedMap.toList cgi.coverageInfo <&> \(ti, tyCov, cons) => do
+c : (colourful : Bool) -> Color -> String -> String
+c False _   = id
+c True  col = show . colored col
+
+||| Boldens the rightmost name after the last dot, if coloured
+showType : (colourful : Bool) -> TypeInfo -> String
+showType False ti = show ti.name
+showType True  ti = joinBy "." $ forget $ uncurry lappend $ map (singleton . show . bolden) $ unsnoc $ split (== '.') $ show ti.name
+
+toString : (colourful : Bool) -> CoverageGenInfo g -> String
+toString col cgi = joinBy "\n\n" $ SortedMap.toList cgi.coverageInfo <&> \(ti, tyCov, cons) => do
   let conCovs = values cons
   let anyCons = not $ null conCovs
   let allConsCovered = all (== True)  conCovs
   let noConsCovered  = all (== False) conCovs
 
+  let c = c col
   let tyCovStr = joinBy ", " $
-                   (if tyCov && noConsCovered then ["mentioned"]
-                    else if not tyCov && (not anyCons || not noConsCovered) then ["not menioned"]
+                   (if tyCov && noConsCovered then [c BrightYellow "mentioned"]
+                    else if not tyCov && (not anyCons || not noConsCovered) then [c BrightYellow "not menioned"]
                     else []) ++
-                   (if not anyCons then ["no constructors"]
-                    else if allConsCovered then ["covered fully"]
-                    else if noConsCovered then ["not covered"]
-                    else ["covered partially"]
+                   (if not anyCons then [c Cyan "no constructors"]
+                    else if allConsCovered then [c BrightGreen "covered fully"]
+                    else if noConsCovered then [c BrightRed "not covered"]
+                    else [c BrightYellow "covered partially"]
                    )
-  joinBy "\n" $ (::) "\{show ti.name} \{tyCovStr}" $ whenTs anyCons $ map ("  - " ++) $
-    SortedMap.toList cons <&> \(co, coCov) => "\{logPosition co}: \{the String $ if coCov then "" else "not "}covered"
+  joinBy "\n" $ (::) "\{showType col ti} \{tyCovStr}" $ whenTs anyCons $ map ("  - " ++) $
+    SortedMap.toList cons <&> \(co, coCov) => do
+      let status : String := if coCov then c BrightGreen "covered" else c BrightRed "not covered"
+      "\{logPosition co}: \{status}"
+
+export
+Show (CoverageGenInfo g) where show = toString False
 
 export
-Show (CoverageGenInfo g) where show = toString
+[Colourful] Show (CoverageGenInfo g) where show = toString True
 
 infixOf : Eq a => List a -> List a -> Maybe (List a, List a)
 infixOf = map (map snd) .: infixOfBy (\x, y => if x == y then Just () else Nothing)

tests/lib/coverage/types-and-cons-008/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 @{Colourful} 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 @{Colourful} ci

tests/lib/coverage/types-and-cons-008/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-008/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-008/test.ipkg

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