[ label ] Simplify labels management + add a simple printer of labels

Author: buzden

src/Test/DepTyCheck/Gen.idr

@@ -308,14 +308,14 @@ mkOneOf {em=MaybeEmpty} xs =
 --- Non-empty generators ---
 
 export
-unGen1 : MonadRandom m => CanManageLabels m => Gen1 a -> m a
+unGen1 : MonadRandom m => (labels : CanManageLabels m) => Gen1 a -> m a
 unGen1 $ Pure x         = pure x
 unGen1 $ Raw sf         = sf.unRawGen
 unGen1 $ OneOf @{_} @{nw} oo with 0 (nonEmptyIsMaximal nw)
   _ | Refl = assert_total unGen1 . force . pickWeighted oo.unGenAlts . finToNat =<< randomFin oo.totalWeight
 unGen1 $ Bind @{nw} x f with 0 (nonEmptyIsMaximal nw)
   _ | Refl = x.unRawGen >>= unGen1 . f
-unGen1 $ Labelled l x   = manageLabel l $ unGen1 x
+unGen1 $ Labelled l x   = manageLabel l >> unGen1 x
 
 export
 unGenAll' : RandomGen g => (seed : g) -> Gen1 a -> Stream (g, a)
@@ -335,16 +335,16 @@ pick1 gen = initSeed <&> \s => evalRandom s $ unGen1 gen
 --- Possibly empty generators ---
 
 export
-unGen : MonadRandom m => MonadError () m => CanManageLabels m => Gen em a -> m a
+unGen : MonadRandom m => MonadError () m => (labels : CanManageLabels m) => Gen em a -> m a
 unGen $ Empty        = throwError ()
 unGen $ Pure x       = pure x
 unGen $ Raw sf       = sf.unRawGen
 unGen $ OneOf oo     = assert_total unGen . force . pickWeighted oo.unGenAlts . finToNat =<< randomFin oo.totalWeight
 unGen $ Bind x f     = x.unRawGen >>= unGen . f
-unGen $ Labelled l x = manageLabel l $ unGen x
+unGen $ Labelled l x = manageLabel l >> unGen x
 
 export %inline
-unGen' : MonadRandom m => CanManageLabels m => Gen em a -> m $ Maybe a
+unGen' : MonadRandom m => (labels : CanManageLabels m) => Gen em a -> m $ Maybe a
 unGen' = runMaybeT . unGen {m=MaybeT m}
 
 export

src/Test/DepTyCheck/Gen/Coverage.idr

@@ -38,7 +38,7 @@ Monoid ModelCoverage where
   neutral = MkModelCoverage empty
 
 MonadWriter ModelCoverage m => CanManageLabels m where
-  manageLabel l x = tell (MkModelCoverage $ singleton l 1) >> x
+  manageLabel l = tell $ MkModelCoverage $ singleton l 1
 
 export
 unGenD : MonadRandom m => MonadError () m => Gen em a -> m (ModelCoverage, a)

src/Test/DepTyCheck/Gen/Labels.idr

@@ -1,5 +1,10 @@
 module Test.DepTyCheck.Gen.Labels
 
+import Control.Monad.State.Interface
+import public Control.Monad.Trans
+
+import Data.String
+
 %default total
 
 -----------------
@@ -26,12 +31,22 @@ export
 Ord Label where
   compare = comparing $ \(StringLabel x) => x
 
+--- Labels management interface ---
+
 public export
-interface CanManageLabels (0 m : Type -> Type) where
-  manageLabel : Label -> m a -> m a
+interface Monad m => CanManageLabels (0 m : Type -> Type) where
+  manageLabel : Label -> m ()
+
+public export
+CanManageLabels m => MonadTrans t => Monad (t m) => CanManageLabels (t m) where
+  manageLabel = lift . manageLabel
 
 export %defaulthint
-IgnoreLabels : CanManageLabels m
+IgnoreLabels : Monad m => CanManageLabels m
 IgnoreLabels = I where
   [I] CanManageLabels m where
-    manageLabel _ = id
+    manageLabel _ = pure ()
+
+export
+[PrintAllLabels] HasIO io => CanManageLabels io where
+  manageLabel = putStrLn . show

tests/lib/coverage/ty-and-con-withCov-012/PrintCoverage.idr

@@ -0,0 +1,51 @@
+module PrintCoverage
+
+import Test.DepTyCheck.Gen
+import Test.DepTyCheck.Gen.Coverage
+
+import Deriving.DepTyCheck.Gen
+import Deriving.Show
+
+import Control.Monad.Maybe
+import Control.Monad.Random
+import System.Random.Pure.StdGen
+
+%default total
+
+%language ElabReflection
+
+data X = X2 Nat | X3 String
+
+genX : Fuel -> Gen MaybeEmpty X
+genX fl = withCoverage $ oneOf
+  [ [| X2 $ elements [0 .. 9] |]
+  , [| X3 $ elements ["", "a", "bc"] |]
+  ]
+
+data Y : Nat -> Type where
+  Y1 : Y 0
+  Y2 : X -> Y 1
+  Y3 : X -> X -> Y n
+
+genY : Fuel -> (n : _) -> Gen MaybeEmpty $ Y n
+genY fl n = withCoverage $ oneOf [ [| Y3 (genX fl) (genX fl) |], add n ] where
+  add : (n : _) -> Gen MaybeEmpty $ Y n
+  add 0 = [| Y1 |]
+  add 1 = [| Y2 $ genX fl |]
+  add _ = empty
+
+%hint ShowX : Show X; ShowX = %runElab derive
+%hint ShowY : Show (Y n); ShowY = %runElab derive
+
+try : (n : Nat) -> IO ()
+try n = do
+  v : Maybe (Y n) <- runMaybeT {m=IO} $ evalRandomT someStdGen $ evalStateT Z $ unGen {labels = PrintAllLabels} $ genY (limit 5) n
+  let Just v = v
+    | Nothing => putStrLn "couldn't produce a value"
+  putStrLn "value: \{show v}"
+
+main : IO ()
+main = do
+  Lazy.for_ [Z, 1, 3] $ \n => do
+    putStrLn "--------\n"
+    try n

tests/lib/coverage/ty-and-con-withCov-012/expected

@@ -0,0 +1,23 @@
+1/1: Building PrintCoverage (PrintCoverage.idr)
+
+--------
+
+PrintCoverage.Y[?]
+PrintCoverage.Y1 (user-defined)
+value: Y1
+--------
+
+PrintCoverage.Y[?]
+PrintCoverage.X[?]
+PrintCoverage.X2 (user-defined)
+PrintCoverage.Y2 (user-defined)
+value: Y2 (X2 4)
+--------
+
+PrintCoverage.Y[?]
+PrintCoverage.X[?]
+PrintCoverage.X[?]
+PrintCoverage.X2 (user-defined)
+PrintCoverage.X2 (user-defined)
+PrintCoverage.Y3 (user-defined)
+value: Y3 (X2 4) (X2 8)

tests/lib/coverage/ty-and-con-withCov-012/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

tests/lib/coverage/ty-and-con-withCov-012/test.ipkg

@@ -0,0 +1,6 @@
+package a-test
+executable = a-test
+
+depends = deptycheck
+
+main = PrintCoverage

tests/lib/coverage/ty-and-con-withCov-013/PrintCoverage.idr

@@ -0,0 +1,51 @@
+module PrintCoverage
+
+import Test.DepTyCheck.Gen
+import Test.DepTyCheck.Gen.Coverage
+
+import Deriving.DepTyCheck.Gen
+import Deriving.Show
+
+import Control.Monad.Maybe
+import Control.Monad.Random
+import System.Random.Pure.StdGen
+
+%default total
+
+%language ElabReflection
+
+data X = X2 Nat | X3 String
+
+genX : Fuel -> Gen MaybeEmpty X
+genX fl = withCoverage $ oneOf
+  [ [| X2 $ elements [0 .. 9] |]
+  , [| X3 $ elements ["", "a", "bc"] |]
+  ]
+
+data Y : Nat -> Type where
+  Y1 : Y 0
+  Y2 : X -> Y 1
+  Y3 : X -> X -> Y n
+
+genY : Fuel -> (n : _) -> Gen MaybeEmpty $ Y n
+genY fl n = withCoverage $ oneOf [ [| Y3 (genX fl) (genX fl) |], add n ] where
+  add : (n : _) -> Gen MaybeEmpty $ Y n
+  add 0 = [| Y1 |]
+  add 1 = [| Y2 $ genX fl |]
+  add _ = empty
+
+%hint ShowX : Show X; ShowX = %runElab derive
+%hint ShowY : Show (Y n); ShowY = %runElab derive
+
+try : (n : Nat) -> IO ()
+try n = do
+  v : Maybe (Y n) <- evalRandomT someStdGen $ evalStateT Z $ unGen' {labels = PrintAllLabels} $ genY (limit 5) n
+  let Just v = v
+    | Nothing => putStrLn "couldn't produce a value"
+  putStrLn "value: \{show v}"
+
+main : IO ()
+main = do
+  Lazy.for_ [Z, 1, 3] $ \n => do
+    putStrLn "--------\n"
+    try n

tests/lib/coverage/ty-and-con-withCov-013/expected

@@ -0,0 +1,23 @@
+1/1: Building PrintCoverage (PrintCoverage.idr)
+
+--------
+
+PrintCoverage.Y[?]
+PrintCoverage.Y1 (user-defined)
+value: Y1
+--------
+
+PrintCoverage.Y[?]
+PrintCoverage.X[?]
+PrintCoverage.X2 (user-defined)
+PrintCoverage.Y2 (user-defined)
+value: Y2 (X2 4)
+--------
+
+PrintCoverage.Y[?]
+PrintCoverage.X[?]
+PrintCoverage.X[?]
+PrintCoverage.X2 (user-defined)
+PrintCoverage.X2 (user-defined)
+PrintCoverage.Y3 (user-defined)
+value: Y3 (X2 4) (X2 8)

tests/lib/coverage/ty-and-con-withCov-013/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

tests/lib/coverage/ty-and-con-withCov-013/test.ipkg

@@ -0,0 +1,6 @@
+package a-test
+executable = a-test
+
+depends = deptycheck
+
+main = PrintCoverage