Test.DepTyCheck.Gen.Coverage

Definitions and functions for working with model coverage of a bunch of generated values.

Model coverage means a coverage in terms of the original data structure that is being generated,
e.g. involved types and their constructors.

Reexports

Definitions

record ModelCoverage : Type

  Raw information of covered labels

Totality: total
Visibility: public export
Constructor: 

MkModelCoverage : SortedMap Label Nat -> ModelCoverage

Projection: 

.unModelCoverage : ModelCoverage -> SortedMap Label Nat

Hints:

MonadWriter ModelCoverage m => CanManageLabels m

Monoid ModelCoverage

Semigroup ModelCoverage

.unModelCoverage : ModelCoverage -> SortedMap Label Nat

Totality: total
Visibility: public export

unModelCoverage : ModelCoverage -> SortedMap Label Nat

Totality: total
Visibility: public export

unGenD : MonadRandom m => MonadError () m => Gen em a -> m (ModelCoverage, a)

Totality: total
Visibility: export

unGenD' : MonadRandom m => Gen em a -> m (Maybe (ModelCoverage, a))

Totality: total
Visibility: export

unGenTryAllD' : RandomGen g => g -> Gen em a -> Stream (g, Maybe (ModelCoverage, a))

Totality: total
Visibility: export

unGenTryAllD : RandomGen g => g -> Gen em a -> Stream (Maybe (ModelCoverage, a))

Totality: total
Visibility: export

unGenTryND : RandomGen g => Nat -> g -> Gen em a -> LazyList (ModelCoverage, a)

Totality: total
Visibility: export

record CoverageGenInfo : (0 _ : k) -> Type

  Higher-level coverage information, in terms of types and constructors, etc.

Totality: total
Visibility: export
Constructor: 

MkCoverageGenInfo : SortedMap String TypeInfo -> SortedMap String (TypeInfo, Con) -> SortedMap TypeInfo (Nat, SortedMap Con Nat) -> CoverageGenInfo g

Projections:

.constructors : CoverageGenInfo g -> SortedMap String (TypeInfo, Con)

.coverageInfo : CoverageGenInfo g -> SortedMap TypeInfo (Nat, SortedMap Con Nat)

.types : CoverageGenInfo g -> SortedMap String TypeInfo

Hint: 

Show (CoverageGenInfo g)

initCoverageInfo' : (n : Name) -> Elab (CoverageGenInfo n)

Totality: total
Visibility: export

initCoverageInfo'' : (ns : List Name) -> Elab (CoverageGenInfo ns)

Totality: total
Visibility: export

initCoverageInfo : (0 x : g) -> Elab (CoverageGenInfo x)

Totality: total
Visibility: export

withCoverage : Gen em a -> Elab (Gen em a)

  Adds labelling of types and constructors to a given generator
  
  Added labelling is not deep, i.e. it adds labels only for the returned type of a generator.
  If returned type is a dependent pair, the rightmost type is taken into the account.

Totality: total
Visibility: export

registerCoverage : ModelCoverage -> CoverageGenInfo g -> CoverageGenInfo g

Totality: total
Visibility: export