
   0 | ||| Definitions and functions for working with model coverage of a bunch of generated values.
   1 | |||
   2 | ||| Model coverage means a coverage in terms of the original data structure that is being generated,
   3 | ||| e.g. involved types and their constructors.
   4 | module Test.DepTyCheck.Gen.Coverage
   5 | 
   6 | import Control.Monad.Maybe
   7 | import Control.Monad.Random
   8 | import Control.Monad.Writer
   9 | 
  10 | import Data.Alternative
  11 | import Data.Fuel
  12 | import Data.List
  13 | import Data.List.Lazy
  14 | import Data.Singleton
  15 | import Data.SortedMap
  16 | 
  17 | import public Language.Reflection.Compat.TypeInfo
  18 | import public Language.Reflection.Logging
  19 | 
  20 | import Test.DepTyCheck.Gen
  21 | 
  22 | import Text.ANSI
  23 | 
  24 | %default total
  25 | 
  26 | ||| Raw information of covered labels
  27 | public export
  28 | record ModelCoverage where
  29 |   constructor MkModelCoverage
  30 |   unModelCoverage : SortedMap Label Nat
  31 | 
  32 | export
  33 | Semigroup ModelCoverage where
  34 |   (<+>) = MkModelCoverage .: mergeWith (+) `on` unModelCoverage
  35 | 
  36 | export
  37 | Monoid ModelCoverage where
  38 |   neutral = MkModelCoverage empty
  39 | 
  40 | MonadWriter ModelCoverage m => CanManageLabels m where
  41 |   manageLabel l = tell $ MkModelCoverage $ singleton l 1
  42 | 
  43 | export
  44 | unGenD : MonadRandom m => MonadError () m => Gen em a -> m (ModelCoverage, a)
  45 | unGenD = map swap . runWriterT . unGen {m = WriterT ModelCoverage $ m}
  46 | 
  47 | export %inline
  48 | unGenD' : MonadRandom m => Gen em a -> m $ Maybe (ModelCoverage, a)
  49 | unGenD' = runMaybeT . unGenD {m = MaybeT m}
  50 | 
  51 | export
  52 | unGenTryAllD' : RandomGen g => (seed : g) -> Gen em a -> Stream (g, Maybe (ModelCoverage, a))
  53 | unGenTryAllD' seed gen = do
  54 |   let (seed, sv) = runRandom seed $ runMaybeT $ runWriterT $ unGen {m=WriterT ModelCoverage $ MaybeT Rand} gen
  55 |   (seed, map swap sv) :: unGenTryAllD' seed gen
  56 | 
  57 | export
  58 | unGenTryAllD : RandomGen g => (seed : g) -> Gen em a -> Stream $ Maybe (ModelCoverage, a)
  59 | unGenTryAllD = map snd .: unGenTryAllD'
  60 | 
  61 | export
  62 | unGenTryND : RandomGen g => (n : Nat) -> g -> Gen em a -> LazyList (ModelCoverage, a)
  63 | unGenTryND n = mapMaybe id .: take (limit n) .: unGenTryAllD
  64 | 
  65 | ||| Higher-level coverage information, in terms of types and constructors, etc.
  66 | export
  67 | record CoverageGenInfo (0 g : k) where
  68 |   constructor MkCoverageGenInfo
  69 |   types        : SortedMap String TypeInfo
  70 |   constructors : SortedMap String (TypeInfo, Con)
  71 |   coverageInfo : SortedMap TypeInfo (Nat, SortedMap Con Nat)
  72 | 
  73 | mergeCovGenInfos : CoverageGenInfo g -> CoverageGenInfo g' -> CoverageGenInfo g''
  74 | mergeCovGenInfos (MkCoverageGenInfo ts cns cis) (MkCoverageGenInfo ts' cns' cis') =
  75 |   MkCoverageGenInfo (mergeLeft ts ts') (mergeLeft cns cns') (let _ : Semigroup Nat := Additive in cis <+> cis')
  76 | 
  77 | coverageGenInfo : Name -> Elab $ CoverageGenInfo x
  78 | coverageGenInfo genTy = do
  79 |   involvedTypes <- allInvolvedTypes MW =<< getInfo' genTy
  80 |   let _    = TypeInfoOrdByName
  81 |   let _    = ConOrdByName
  82 |   let cov  = fromList $ involvedTypes <&> \ty => (ty, 0, fromList $ ty.cons <&> (, 0))
  83 |   let tys  = fromList $ involvedTypes <&> \ty => (show ty.name, ty)
  84 |   let cons = fromList $ (involvedTypes >>= \ty => (ty,) <$> ty.cons) <&> \(ty, co) => (show co.name, ty, co)
  85 |   pure $ MkCoverageGenInfo tys cons cov
  86 | 
  87 | export %macro
  88 | initCoverageInfo' : (n : Name) -> Elab $ CoverageGenInfo n
  89 | initCoverageInfo' n = coverageGenInfo n
  90 | 
  91 | export %macro
  92 | initCoverageInfo'' : (ns : List Name) -> Elab $ CoverageGenInfo ns
  93 | initCoverageInfo'' = go where
  94 |   go : (ns : List Name) -> Elab $ CoverageGenInfo ns
  95 |   go [] = fail "At least one name must be given"
  96 |   go [n] = coverageGenInfo n
  97 |   go (n::ns) = [| mergeCovGenInfos {g=n} (coverageGenInfo n) (go ns) |]
  98 | 
  99 | ||| Returns a name by the generator's type
 100 | |||
 101 | ||| Say, for the `Fuel -> Gen em (n ** Fin n)` it returns name of `Data.Fin.Fin`
 102 | genTypeName : (0 _ : Type) -> Elab Name
 103 | genTypeName g = do
 104 |   genTy <- quote g
 105 |   let (_, genTy) = unPi genTy
 106 |   let (lhs, args) = unAppAny genTy
 107 |   let IVar _ lhsName = lhs
 108 |     | _ => failAt (getFC lhs) "Generator or generator function expected"
 109 |   let True = lhsName `nameConformsTo` `{Test.DepTyCheck.Gen.Gen}
 110 |     | _ => failAt (getFC lhs) "Return type must be a generator of some type"
 111 |   let [_, genTy] = args
 112 |     | _ => failAt (getFC lhs) "Wrong number of type arguments of a generator"
 113 |   let (_, genTy) = unDPair $ getExpr genTy
 114 |   let (IVar _ genTy, _) = unAppAny genTy
 115 |     | (genTy, _) => failAt (getFC genTy) "Expected a type name, got \{show genTy}"
 116 |   pure genTy
 117 | 
 118 | export %macro
 119 | initCoverageInfo : (0 x : g) -> Elab $ CoverageGenInfo x
 120 | initCoverageInfo _ = genTypeName g >>= coverageGenInfo
 121 | 
 122 | ||| Derives function `A -> B` where `A` is determined by the given `TypeInfo`, `B` is determined by `retTy`
 123 | |||
 124 | ||| For each constructor of `A` the `matcher` function is applied and its result (of type `B`) is used as a result.
 125 | ||| Currently, `B` must be a non-dependent type.
 126 | deriveMatchingCons : (retTy : TTImp) -> (matcher : Con -> TTImp) -> (funName : Name) -> TypeInfo -> List Decl
 127 | deriveMatchingCons retTy matcher funName ti = do
 128 |   let claim = do
 129 |     let tyApplied = reAppAny (var ti.name) $ ti.args <&> \arg => appArg arg $ var $ argName' arg
 130 |     let sig = foldr
 131 |                 (pi . {count := M0, piInfo := ImplicitArg})
 132 |                 `(~tyApplied -> ~retTy)
 133 |                 ti.args
 134 |     private' funName sig
 135 |   let body = do
 136 |     let matchCon = \con => reAppAny (var con.name) $ con.args <&> flip appArg implicitTrue
 137 |     def funName $ ti.cons <&> \con =>
 138 |       patClause (var funName .$ matchCon con) $ matcher con
 139 |   [claim, body]
 140 | 
 141 | ||| Adds labelling of types and constructors to a given generator
 142 | |||
 143 | ||| Added labelling is not deep, i.e. it adds labels only for the returned type of a generator.
 144 | ||| If returned type is a dependent pair, the rightmost type is taken into the account.
 145 | export %macro
 146 | withCoverage : {em : _} -> (gen : Gen em a) -> Elab $ Gen em a
 147 | withCoverage gen = do
 148 |   tyExpr <- quote a
 149 |   let (dpairLefts, tyRExpr) = unDPair tyExpr
 150 |   let (IVar _ tyName, _) = unAppAny tyRExpr
 151 |     | (genTy, _) => failAt (getFC genTy) "Expected a normal type name"
 152 |   tyInfo <- getInfo' tyName
 153 |   let matchDPair = \expr => foldr (\_, r => var "Builtin.DPair.MkDPair" .$ implicitTrue .$ r) expr dpairLefts
 154 |   let tyLabelStr = "\{show tyName}[?]"
 155 |   let labelledValName = UN $ Basic "^val^"
 156 |   let labellingFunName = UN $ Basic "^labelling^"
 157 |   let undpairedVal = "^undpaired^"
 158 |   let consLabellingFun = deriveMatchingCons
 159 |                            `(Test.DepTyCheck.Gen.Labels.Label)
 160 |                            (\con => var "fromString" .$ primVal (Str $ "\{show con.name} (user-defined)"))
 161 |                            labellingFunName tyInfo
 162 |   labeller <- check $ lam (lambdaArg labelledValName) $
 163 |                 local consLabellingFun $
 164 |                   `(Test.DepTyCheck.Gen.label
 165 |                      ~(iCase (var labelledValName) implicitTrue $ pure $
 166 |                        patClause
 167 |                          (matchDPair $ bindVar undpairedVal)
 168 |                          (var labellingFunName .$ var undpairedVal))
 169 |                      (pure ~(var labelledValName)))
 170 |   pure $ label (fromString tyLabelStr) $ gen >>= labeller
 171 | 
 172 | c : (colourful : Bool) -> Color -> String -> String
 173 | c False _   = id
 174 | c True  col = show . colored col
 175 | 
 176 | ||| Boldens the rightmost name after the last dot, if coloured
 177 | showType : (colourful : Bool) -> TypeInfo -> String
 178 | showType False ti = show ti.name
 179 | showType True  ti = joinBy "." $ forget $ uncurry lappend $ map (singleton . show . bolden) $ unsnoc $ split (== '.') $ show ti.name
 180 | 
 181 | toString : (colourful : Bool) -> CoverageGenInfo g -> String
 182 | toString col cgi = (++ "\n") $ joinBy "\n\n" $
 183 |                      mapMaybe (\ti => lookup ti cgi.coverageInfo <&> (ti,)) (SortedMap.values cgi.types) <&> \(ti, tyCovCnt, cons) => do
 184 |   let conCovs = values cons
 185 |   let anyCons = not $ null conCovs
 186 |   let allConsCovered = all (/= 0) conCovs
 187 |   let noConsCovered  = all (== 0) conCovs
 188 | 
 189 |   let c = c col
 190 |   let cntAddition = \cnt : Nat => " (\{show cnt} time\{if cnt /= 1 then "s" else ""})"
 191 |   let tyCovStr = joinBy ", " $
 192 |                    (if tyCovCnt /= 0 && noConsCovered then [c BrightYellow "mentioned" ++ cntAddition tyCovCnt]
 193 |                     else if tyCovCnt == 0 && (not anyCons || not noConsCovered) then [c BrightYellow "not mentioned"]
 194 |                     else []) ++
 195 |                    (if not anyCons then [c Cyan "no constructors"]
 196 |                     else if allConsCovered then [c BrightGreen "covered fully" ++ cntAddition tyCovCnt]
 197 |                     else if noConsCovered then [c BrightRed "not covered"]
 198 |                     else [c BrightYellow "covered partially" ++ cntAddition tyCovCnt]
 199 |                    )
 200 |   joinBy "\n" $ (::) "\{showType col ti} \{tyCovStr}" $ whenTs anyCons $ map ("  - " ++) $
 201 |     SortedMap.toList cons <&> \(co, coCovCnt) => do
 202 |       let status : String := if coCovCnt /= 0 then c BrightGreen "covered" ++ cntAddition coCovCnt else c BrightRed "not covered"
 203 |       "\{logPosition co}: \{status}"
 204 | 
 205 | export
 206 | Show (CoverageGenInfo g) where show = toString False
 207 | 
 208 | export
 209 | [Colourful] Show (CoverageGenInfo g) where show = toString True
 210 | 
 211 | export
 212 | registerCoverage : ModelCoverage -> CoverageGenInfo g -> CoverageGenInfo g
 213 | registerCoverage mc cgi = foldr registerCoverage1 cgi $ toList mc.unModelCoverage where
 214 |   registerCoverage1 : (Label, Nat) -> CoverageGenInfo g -> CoverageGenInfo g
 215 |   registerCoverage1 (str, cnt) cgi = do
 216 |     let str = show str
 217 |     let str' = fastUnpack str
 218 |     -- Try type
 219 |     let ty = maybe str (fastPack . fst) $ fastUnpack "[" `infixOf` str'
 220 |     let tyMod = case lookup ty cgi.types of
 221 |                   Just ti => { coverageInfo $= flip updateExisting ti $ mapFst (+cnt) }
 222 |                   Nothing => id
 223 |     -- Try constructor
 224 |     let co = maybe str (fastPack . fst) $ fastUnpack " " `infixOf` str'
 225 |     let coMod : (_ -> CoverageGenInfo g) := case lookup co cgi.constructors of
 226 |                   Just (ti, co) => { coverageInfo $= flip updateExisting ti $ mapSnd $ updateExisting (+cnt) co }
 227 |                   Nothing       => id
 228 |     tyMod $ coMod $ cgi
 229 |