Skip to content

Commit

Permalink
[ fix ] Support dependent pairs in generators then initing coverage
Browse files Browse the repository at this point in the history
  • Loading branch information
buzden committed Sep 19, 2023
1 parent 4f8c84a commit ee694f0
Show file tree
Hide file tree
Showing 5 changed files with 70 additions and 2 deletions.
5 changes: 3 additions & 2 deletions src/Test/DepTyCheck/Gen/Coverage.idr
Original file line number Diff line number Diff line change
Expand Up @@ -92,8 +92,9 @@ genTypeName g = do
| _ => failAt (getFC lhs) "Return type must be a generator of some type"
let [_, genTy] = args
| _ => failAt (getFC lhs) "Wrong number of type arguments of a generator"
let (_, IVar _ genTy) = unDPair $ getExpr genTy
| (_, genTy) => failAt (getFC genTy) "Expected a type name"
let (_, genTy) = unDPair $ getExpr genTy
let (IVar _ genTy, _) = unApp genTy
| (genTy, _) => failAt (getFC genTy) "Expected a type name"
pure genTy

export %macro
Expand Down
38 changes: 38 additions & 0 deletions tests/lib/coverage/types-and-cons-002/PrintCoverage.idr
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
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 %hint
smallStrs : Fuel -> Gen MaybeEmpty String
smallStrs _ = elements ["", "a", "bc"]

export %hint
UsedConstructorDerivator : ConstructorDerivator
UsedConstructorDerivator = LeastEffort

data X = X1 | X2 Nat | X3 String

data Y : Nat -> Type where
Y1 : Y 0
Y2 : X -> Y 1
Y3 : X -> X -> Y 2

genY : Fuel -> (Fuel -> Gen MaybeEmpty String) => Gen MaybeEmpty (n ** Y n)
genY = deriveGen

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
15 changes: 15 additions & 0 deletions tests/lib/coverage/types-and-cons-002/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
1/1: Building PrintCoverage (PrintCoverage.idr)

Prelude.Types.Nat covered fully
- S: covered
- Z: covered

PrintCoverage.X covered fully
- X1: covered
- X2: covered
- X3: covered

PrintCoverage.Y covered fully
- Y1: covered
- Y2: covered
- Y3: covered
8 changes: 8 additions & 0 deletions tests/lib/coverage/types-and-cons-002/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-002/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 ee694f0

Please sign in to comment.