diff --git a/src/Test/DepTyCheck/Gen/Coverage.idr b/src/Test/DepTyCheck/Gen/Coverage.idr index 82e729f1b..1f1a45be3 100644 --- a/src/Test/DepTyCheck/Gen/Coverage.idr +++ b/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) diff --git a/tests/lib/coverage/types-and-cons-008/PrintCoverage.idr b/tests/lib/coverage/types-and-cons-008/PrintCoverage.idr new file mode 100644 index 000000000..43c10da5e --- /dev/null +++ b/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 diff --git a/tests/lib/coverage/types-and-cons-008/expected b/tests/lib/coverage/types-and-cons-008/expected new file mode 100644 index 000000000..82adbc9b9 --- /dev/null +++ b/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 diff --git a/tests/lib/coverage/types-and-cons-008/run b/tests/lib/coverage/types-and-cons-008/run new file mode 100755 index 000000000..9706b3375 --- /dev/null +++ b/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 diff --git a/tests/lib/coverage/types-and-cons-008/test.ipkg b/tests/lib/coverage/types-and-cons-008/test.ipkg new file mode 100644 index 000000000..879278361 --- /dev/null +++ b/tests/lib/coverage/types-and-cons-008/test.ipkg @@ -0,0 +1,6 @@ +package a-test +executable = a-test + +depends = deptycheck + +main = PrintCoverage