Skip to content

Commit

Permalink
[ fix ] Support dependent types in withCoverage macro
Browse files Browse the repository at this point in the history
  • Loading branch information
buzden committed Sep 19, 2023
1 parent 6d3f23a commit ec70d2f
Show file tree
Hide file tree
Showing 5 changed files with 108 additions and 3 deletions.
16 changes: 13 additions & 3 deletions src/Test/DepTyCheck/Gen/Coverage.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
50 changes: 50 additions & 0 deletions tests/lib/coverage/types-and-cons-007/PrintCoverage.idr
Original file line number Diff line number Diff line change
@@ -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
31 changes: 31 additions & 0 deletions tests/lib/coverage/types-and-cons-007/expected
Original file line number Diff line number Diff line change
@@ -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
8 changes: 8 additions & 0 deletions tests/lib/coverage/types-and-cons-007/run
Original file line number Diff line number Diff line change
@@ -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
6 changes: 6 additions & 0 deletions tests/lib/coverage/types-and-cons-007/test.ipkg
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
package a-test
executable = a-test

depends = deptycheck

main = PrintCoverage

0 comments on commit ec70d2f

Please sign in to comment.