0 | module Test.DepTyCheck.Gen

  2 | import Control.Monad.Maybe

  3 | import public Control.Monad.Error.Interface

  4 | import Control.Monad.Random

  5 | import public Control.Monad.Random.Interface

  7 | import Data.Bool

  8 | import public Data.CheckedEmpty.List.Lazy

  9 | import Data.CheckedEmpty.List.Lazy.Elem

 10 | import Data.CheckedEmpty.List.Lazy.Quantifiers

 11 | import Data.CheckedEmpty.List.Lazy.Properties

 12 | import Data.Fuel

 13 | import public Data.Nat1

 14 | import Data.List

 15 | import Data.List.Lazy

 16 | import Data.List.Lazy.Extra

 17 | import Data.Vect

 19 | import Decidable.Equality

 21 | import public Language.Implicits.IfUnsolved

 23 | import Syntax.WithProof

 25 | import public Test.DepTyCheck.Gen.Emptiness

 26 | import public Test.DepTyCheck.Gen.Labels

 28 | %default total

 34 | randomFin : MonadRandom m => (n : Nat1) -> m $ Fin n.asNat

 35 | randomFin $ FromNat (S _) = getRandom

 37 | public export %inline

 38 | wrapLazy : (a -> b) -> Lazy a -> Lazy b

 39 | wrapLazy f = delay . f . force

 42 | wrapMaybeTaggedLazy : (a -> Maybe b) -> (tag, Lazy a) -> Maybe (tag, Lazy b)

 43 | wrapMaybeTaggedLazy f = traverse $ map delay . f . force

 45 | 0 unpackTaggedLazy : Functor f => f (tag, Lazy a) -> f a

 46 | unpackTaggedLazy = map $ force . snd

 52 | record RawGen a where

 53 |   constructor MkRawGen

 54 |   unRawGen : forall m. MonadRandom m => CanManageLabels m => m a

 57 | data Gen : Emptiness -> Type -> Type

 59 | 0 IsNonEmpty : Gen em a -> Type

 62 | record GenAlternatives (0 mustBeNotEmpty : Bool) (0 em : Emptiness) (a : Type)

 64 | 0 All : (Gen em a -> Type) -> GenAlternatives ne em a -> Type

 66 | data Gen : Emptiness -> Type -> Type where

 68 |   Empty : Gen MaybeEmpty a

 70 |   Pure  : a -> Gen em a

 72 |   Raw   : RawGen a -> Gen em a

 74 |   OneOf : (gs : GenAlternatives True alem a) ->

 75 |           (0 _ : All IsNonEmpty gs) =>

 76 |           (0 _ : alem `NoWeaker` em) =>

 77 |           Gen em a

 79 |   Bind  : (0 _ : biem `NoWeaker` em) =>

 80 |           RawGen c -> (c -> Gen biem a) -> Gen em a

 82 |   Labelled : Label -> (g : Gen em a) -> (0 _ : IsNonEmpty g) => Gen em a

 84 | isEmpty : Gen em a -> Bool

 85 | isEmpty Empty = True

 86 | isEmpty _     = False

 89 | isNonEmpty : Gen em a -> Bool

 90 | isNonEmpty = not . isEmpty

 92 | IsNonEmpty g = isEmpty g === False

 94 | record GenAlternatives (0 mustBeNotEmpty : Bool) (0 em : Emptiness) (a : Type) where

 95 |   constructor MkGenAlts

 96 |   unGenAlts : LazyLst mustBeNotEmpty (Nat1, Lazy (Gen em a))

 98 | 0 listOfAlts : GenAlternatives ne em a -> LazyLst ne $ Gen em a

 99 | listOfAlts $ MkGenAlts gs = unpackTaggedLazy gs

101 | All p = All p . listOfAlts

103 | 0 Elem : Gen em a -> GenAlternatives ne em a -> Type

104 | Elem g = Elem g . listOfAlts

106 | (.totalWeight) : GenAlternatives True em a -> Nat1

107 | (.totalWeight) = foldl1 (+) . map fst . unGenAlts

109 | public export %inline

110 | Gen1 : Type -> Type

111 | Gen1 = Gen NonEmpty

117 | public export %inline

118 | Gen0 : Type -> Type

119 | Gen0 = Gen MaybeEmpty

122 | 0 isNonEmptyGen1 : {g : Gen1 a} -> IsNonEmpty g

123 | isNonEmptyGen1 {g=Pure _}       = Refl

124 | isNonEmptyGen1 {g=Raw _}        = Refl

125 | isNonEmptyGen1 {g=OneOf _}      = Refl

126 | isNonEmptyGen1 {g=Bind _ _}     = Refl

127 | isNonEmptyGen1 {g=Labelled _ _} = Refl

134 | chooseAny : Random a => (0 _ : IfUnsolved ne NonEmpty) => Gen ne a

135 | chooseAny = Raw $ MkRawGen getRandom

137 | public export %inline

138 | chooseAnyOf : (0 a : _) -> Random a => (0 _ : IfUnsolved ne NonEmpty) => Gen ne a

139 | chooseAnyOf _ = chooseAny

142 | choose : Random a => (0 _ : IfUnsolved ne NonEmpty) => (a, a) -> Gen ne a

143 | choose bounds = Raw $ MkRawGen $ getRandomR bounds

145 | export %inline

146 | empty : Gen0 a

147 | empty = Empty

150 | label : Label -> Gen em a -> Gen em a

151 | label l g with (isEmpty g) proof 0 prf

152 |   label _ Empty | True  = Empty

153 |   label l g     | False = Labelled l g

156 | 0 labelNonEmpty : {g : Gen em a} -> IsNonEmpty g => IsNonEmpty $ label l g

157 | labelNonEmpty {g=Pure _}       = Refl

158 | labelNonEmpty {g=Raw _}        = Refl

159 | labelNonEmpty {g=OneOf _}      = Refl

160 | labelNonEmpty {g=Bind _ _}     = Refl

161 | labelNonEmpty {g=Labelled _ _} = Refl

167 | mapTaggedLazy : Functor f => (a -> b) -> f (tag, Lazy a) -> f (tag, Lazy b)

168 | mapTaggedLazy f = map $ \x => (fst x, wrapLazy f $ snd x)

170 | mapOneOf : GenAlternatives ne iem a -> (Gen iem a -> Gen em b) -> GenAlternatives ne em b

171 | mapOneOf $ MkGenAlts gs = MkGenAlts . flip mapTaggedLazy gs

173 | 0 allMapTaggedLazy : {0 f : a -> b} -> {xs : LazyLst ne (tag, Lazy a)} ->

174 |                      ({x : a} -> (0 _ : Elem x $ unpackTaggedLazy xs) -> p $ f x) ->

175 |                      All p $ unpackTaggedLazy $ mapTaggedLazy f xs

176 | allMapTaggedLazy h = allMap $ allMapForall $ \e => h $ elemMap _ e

178 | 0 allMapOneOf : {0 f : Gen iem a -> Gen em b} ->

179 |                 {gs : GenAlternatives ne iem a} ->

180 |                 ({x : Gen iem a} -> (0 _ : Elem x gs) -> p $ f x) ->

181 |                 All p $ mapOneOf gs f

182 | allMapOneOf {gs=MkGenAlts _} = allMapTaggedLazy

184 | mapElem : (xs : LazyLst ne a) -> ((x : a) -> (0 _ : Elem x xs) -> b) -> LazyLst ne b

185 | mapElem []        _ = []

186 | mapElem (x :: xs) f = f x Here :: mapElem xs (\y, e => f y $ There e)

188 | mapTaggedLazyElem : (xs : LazyLst ne (tag, Lazy a)) ->

189 |                     ((x : a) -> (0 _ : Elem x $ unpackTaggedLazy xs) -> b) ->

190 |                     LazyLst ne (tag, Lazy b)

191 | mapTaggedLazyElem xs f = mapElem xs $ \x, e => (fst x, delay $ f (snd x) $ elemMap _ e)

193 | mapOneOfElem : (gs : GenAlternatives ne iem a) ->

194 |                ((g : Gen iem a) -> (0 _ : Elem g gs) -> Gen em b) ->

195 |                GenAlternatives ne em b

196 | mapOneOfElem $ MkGenAlts gs = MkGenAlts . mapTaggedLazyElem gs

198 | 0 allMapElem : {xs : LazyLst ne a} ->

199 |                {0 f : (x : a) -> (0 _ : Elem x xs) -> b} ->

200 |                ({x : a} -> (0 e : Elem x xs) -> p $ f x e) ->

201 |                All p $ mapElem xs f

202 | allMapElem {xs=[]}      _ = []

203 | allMapElem {xs=x :: xs} h = h Here :: allMapElem (\e => h $ There e)

205 | 0 allMapTaggedLazyElem : {xs : LazyLst ne (tag, Lazy a)} ->

206 |                          {0 f : (x : a) -> (0 _ : Elem x $ unpackTaggedLazy xs) -> b} ->

207 |                          ({x : a} -> (0 e : Elem x $ unpackTaggedLazy xs) -> p $ f x e) ->

208 |                          All p $ unpackTaggedLazy $ mapTaggedLazyElem xs f

209 | allMapTaggedLazyElem h = allMap $ allMapElem $ \e => h $ elemMap _ e

211 | 0 allMapOneOfElem : {gs : GenAlternatives ne iem a} ->

212 |                     {0 f : (g : Gen iem a) -> (0 _ : Elem g gs) -> Gen em b} ->

213 |                     ({g : Gen iem a} -> (0 e : Elem g gs) -> p $ f g e) ->

214 |                     All p $ mapOneOfElem gs f

215 | allMapOneOfElem {gs=MkGenAlts _} = allMapTaggedLazyElem

222 | relax : (0 _ : iem `NoWeaker` em) => Gen iem a -> Gen em a

223 | 0 relaxNonEmpty : {g : Gen iem a} -> IsNonEmpty g => IsNonEmpty $ relax @{nw} g

225 | relax @{nw} Empty           = rewrite maybeEmptyIsMinimal nw in Empty

226 | relax $ Pure x              = Pure x

227 | relax $ Raw x               = Raw x

228 | relax $ OneOf @{ne} @{nw} x = OneOf @{ne} @{transitive' nw %search} x

229 | relax $ Bind @{nw} x f      = Bind @{transitive' nw %search} x f

230 | relax $ Labelled l x        = Labelled @{relaxNonEmpty} l $ relax x

232 | relaxNonEmpty {g=Pure _}       = Refl

233 | relaxNonEmpty {g=Raw _}        = Refl

234 | relaxNonEmpty {g=OneOf _}      = Refl

235 | relaxNonEmpty {g=Bind _ _}     = Refl

236 | relaxNonEmpty {g=Labelled _ _} = Refl

242 | nonEmpty : Gen em a -> Maybe $ Gen em a

243 | nonEmpty Empty = Nothing

244 | nonEmpty x     = Just x

246 | 0 nonEmptyNonEmpty : {g : Gen em a} -> IsJust (nonEmpty g) =>

247 |                      IsNonEmpty $ fromJust $ nonEmpty g

248 | nonEmptyNonEmpty {g=Pure _}       = Refl

249 | nonEmptyNonEmpty {g=Raw _}        = Refl

250 | nonEmptyNonEmpty {g=OneOf _}      = Refl

251 | nonEmptyNonEmpty {g=Bind _ _}     = Refl

252 | nonEmptyNonEmpty {g=Labelled _ _} = Refl

254 | mapMaybeTaggedLazy : (a -> Maybe b) -> LazyLst ne (tag, Lazy a) -> LazyLst0 (tag, Lazy b)

255 | mapMaybeTaggedLazy = mapMaybe . wrapMaybeTaggedLazy

257 | 0 allMapMaybeJustTaggedLazy : {f : a -> Maybe b} ->

258 |                               {xs : LazyLst ne (tag, Lazy a)} ->

259 |                               ((x : a) ->

260 |                                (0 _ : IsJust $ f x) ->

261 |                                p $ fromJust $ f x) ->

262 |                               All p $ unpackTaggedLazy $ mapMaybeTaggedLazy f xs

263 | allMapMaybeJustTaggedLazy h = allMap $ allMapMaybeJust helper

264 |   where

265 |     helper : (x : (tag, Lazy a)) ->

266 |              (0 _ : IsJust $ wrapMaybeTaggedLazy f x) ->

267 |              p $ force $ snd $ fromJust $ wrapMaybeTaggedLazy f x

268 |     helper (w, x) _ with (f x) proof 0 prf

269 |       _ | Just y = do

270 |         let yIsJust : IsJust (f x) = rewrite prf in ItIsJust

271 |         let Refl : y === fromJust (f x) = rewrite prf in Refl

272 |         h x yIsJust

274 | namespace OneOf

276 |   public export

277 |   data AltsNonEmpty : Bool -> Emptiness -> Type where

278 |     NT : AltsNonEmpty True   NonEmpty

279 |     Sx : AltsNonEmpty altsNe MaybeEmpty

281 |   export %defaulthint

282 |   altsNonEmptyTrue : {em : _} -> AltsNonEmpty True em

283 |   altsNonEmptyTrue {em=NonEmpty}   = NT

284 |   altsNonEmptyTrue {em=MaybeEmpty} = Sx

286 | mkOneOfMaybeEmpty : (xs : LazyLst altsNe (Nat1, Lazy (Gen alem a))) ->

287 |                     (0 _ : All IsNonEmpty $ unpackTaggedLazy xs) =>

288 |                     Gen0 a

289 | mkOneOfMaybeEmpty []                  = Empty

290 | mkOneOfMaybeEmpty (x :: xs) @{_ :: _} = OneOf $ MkGenAlts $ x :: xs

292 | mkOneOf : {em : _} ->

293 |           (0 _ : alem `NoWeaker` em) =>

294 |           (0 _ : AltsNonEmpty altsNe em) =>

295 |           LazyLst altsNe (Nat1, Lazy (Gen alem a)) ->

296 |           Gen em a

297 | mkOneOf {em=NonEmpty} @{nw} @{NT} xs with 0 (nonEmptyIsMaximal nw)

298 |   _ | Refl = OneOf @{allTrue isNonEmptyGen1} $ MkGenAlts xs

299 | mkOneOf {em=MaybeEmpty} xs =

300 |   mkOneOfMaybeEmpty (mapMaybeTaggedLazy nonEmpty xs)

301 |     @{allMapMaybeJustTaggedLazy {f=nonEmpty} $ \_, _ => nonEmptyNonEmpty}

309 | allDetermValues : Gen em a -> LazyList a

310 | allDetermValues Empty          = []

311 | allDetermValues $ Pure x       = [x]

312 | allDetermValues $ Raw {}       = [] -- here we take only determinicstic values, no raw gens

313 | allDetermValues $ OneOf gs     = toLazyList (unGenAlts gs) >>= \(_, g) => allDetermValues $ assert_smaller gs g

314 | allDetermValues $ Bind {}      = [] -- here we take only determinicstic values, no raw gens

315 | allDetermValues $ Labelled _ g = allDetermValues g

320 | unGen1 : MonadRandom m => (labels : CanManageLabels m) => Gen1 a -> m a

321 | unGen1 $ Pure x         = pure x

322 | unGen1 $ Raw sf         = sf.unRawGen

323 | unGen1 $ OneOf @{_} @{nw} oo with 0 (nonEmptyIsMaximal nw)

324 |   _ | Refl = assert_total unGen1 . force . pickWeighted oo.unGenAlts . finToNat =<< randomFin oo.totalWeight

325 | unGen1 $ Bind @{nw} x f with 0 (nonEmptyIsMaximal nw)

326 |   _ | Refl = x.unRawGen >>= unGen1 . f

327 | unGen1 $ Labelled l x   = manageLabel l >> unGen1 x

330 | unGenAll' : RandomGen g => (seed : g) -> Gen1 a -> Stream (g, a)

331 | unGenAll' seed gen = do

332 |   let sv@(seed, _) = runRandom seed $ unGen1 {m=Rand} gen

333 |   sv :: unGenAll' seed gen

336 | unGenAll : RandomGen g => (seed : g) -> Gen1 a -> Stream a

337 | unGenAll = map snd .: unGenAll'

341 | pick1 : CanInitSeed g m => Functor m => Gen1 a -> m a

342 | pick1 gen = initSeed <&> \s => evalRandom s $ unGen1 gen

347 | unGen : MonadRandom m => MonadError () m => (labels : CanManageLabels m) => Gen em a -> m a

348 | unGen $ Empty        = throwError ()

349 | unGen $ Pure x       = pure x

350 | unGen $ Raw sf       = sf.unRawGen

351 | unGen $ OneOf oo     = assert_total unGen . force . pickWeighted oo.unGenAlts . finToNat =<< randomFin oo.totalWeight

352 | unGen $ Bind x f     = x.unRawGen >>= unGen . f

353 | unGen $ Labelled l x = manageLabel l >> unGen x

355 | export %inline

356 | unGen' : MonadRandom m => (labels : CanManageLabels m) => Gen em a -> m $ Maybe a

357 | unGen' = runMaybeT . unGen {m=MaybeT m}

360 | unGenTryAll' : RandomGen g => (seed : g) -> Gen em a -> Stream (g, Maybe a)

361 | unGenTryAll' seed gen = do

362 |   let sv@(seed, _) = runRandom seed $ runMaybeT $ unGen {m=MaybeT Rand} gen

363 |   sv :: unGenTryAll' seed gen

366 | unGenTryAll : RandomGen g => (seed : g) -> Gen em a -> Stream $ Maybe a

367 | unGenTryAll = map snd .: unGenTryAll'

370 | unGenTryN : RandomGen g => (n : Nat) -> g -> Gen em a -> LazyList a

371 | unGenTryN n = mapMaybe id .: take (limit n) .: unGenTryAll

375 | pick : CanInitSeed g m => Functor m => Gen em a -> m $ Maybe a

376 | pick gen = initSeed <&> flip evalRandom (unGen' gen)

380 | pickTryN : CanInitSeed g m => Functor m => (n : Nat) -> Gen em a -> m $ Maybe (Fin n, a)

381 | pickTryN n g = initSeed <&> \s => head' (withIndex $ unGenTryN n s g) >>= \(i, x) => natToFin i n <&> (,x)

395 | Functor RawGen where

396 |   map f $ MkRawGen sf = MkRawGen $ f <$> sf

398 | Applicative RawGen where

399 |   pure x = MkRawGen $ pure x

400 |   MkRawGen x <*> MkRawGen y = MkRawGen $ x <*> y

404 | Functor (Gen em)

405 | 0 mapNonEmpty : {g : Gen iem a} -> IsNonEmpty g => IsNonEmpty $ f <$> g

407 | Functor (Gen em) where

408 |   map f $ Empty          = Empty

409 |   map f $ Pure x         = Pure $ f x

410 |   map f $ Raw sf         = Raw $ f <$> sf

411 |   map f $ OneOf @{ne} oo = OneOf @{allMapOneOf $ \e => mapNonEmpty @{indexAll e ne}} $ mapOneOf oo $ assert_total $ map f

412 |   map f $ Bind x g       = Bind x $ map f . g

413 |   map f $ Labelled l x   = Labelled @{mapNonEmpty} l $ map f x

415 | mapNonEmpty {g=Pure _}       = Refl

416 | mapNonEmpty {g=Raw _}        = Refl

417 | mapNonEmpty {g=OneOf _}      = Refl

418 | mapNonEmpty {g=Bind _ _}     = Refl

419 | mapNonEmpty {g=Labelled _ _} = Refl

421 | private infixl 3 <**>

423 | (<**>) : (g : Gen lem $ a -> b) -> (h : Gen rem a) -> Gen (min lem rem) b

424 | 0 apNonEmpty : {g, h : _} -> IsNonEmpty g => IsNonEmpty h => IsNonEmpty $ g <**> h

426 | g <**> h with (isEmpty g) proof 0 prfLeft | (isEmpty h) proof 0 prfRight

427 |   Empty <**> _ | _ | _ = rewrite minMaybeEmptyLeft rem in Empty

428 |   _ <**> Empty | _ | _ = rewrite minMaybeEmptyRight lem in Empty

430 |   Pure f <**> g | _ | _ = f <$> relax @{rightNoWeakerMin} g

431 |   g <**> Pure x | _ | _ = relax @{leftNoWeakerMin} g <&> \f => f x

433 |   Raw sfl <**> Raw sfr | _ | _ = Raw $ sfl <*> sfr

435 |   Labelled l x <**> y | _     | False = Labelled @{apNonEmpty} l $ x <**> y

436 |   x <**> Labelled l y | False | _     = Labelled @{apNonEmpty} l $ x <**> y

438 |   OneOf @{ne} @{nw} oo <**> g | _ | False =

439 |       OneOf @{allMapOneOf $ \e => apNonEmpty @{indexAll e ne}}

440 |             @{minNoWeakerLeft nw} $

441 |         mapOneOf oo $ \x => assert_total $ x <**> g

442 |   g <**> OneOf @{ne} @{nw} oo | False | _ =

443 |     OneOf @{allMapOneOf $ \e => apNonEmpty @{%search} @{indexAll e ne}}

444 |           @{minNoWeakerRight nw} $

445 |       mapOneOf oo $ \x => assert_total $ g <**> x

447 |   Bind @{nw} x f <**> Raw y | _ | _ =

448 |     Bind @{minNoWeakerLeft nw}  x $ \c => f c <**> Raw y

449 |   Raw y <**> Bind @{nw} x f | _ | _ =

450 |     Bind @{minNoWeakerRight nw} x $ \c => Raw y <**> f c

452 |   Bind @{lnw} x f <**> Bind @{rnw} y g | _ | _ =

453 |     Bind @{minNoWeaker lnw rnw} [| (x, y) |] $ \(l, r) => f l <**> g r

455 | apNonEmpty with (isEmpty g) proof 0 prfLeft | (isEmpty h) proof 0 prfRight

456 |   apNonEmpty {g=Empty}        {h}              | True  | _     impossible

457 |   apNonEmpty {g}              {h=Empty}        | _     | True  impossible

459 |   apNonEmpty {g=Pure _}       {h=Pure _}       | _     | _     = Refl

460 |   apNonEmpty {g=Pure _}       {h=Raw _}        | _     | _     = Refl

461 |   apNonEmpty {g=Pure _}       {h=OneOf _}      | _     | _     = Refl

462 |   apNonEmpty {g=Pure _}       {h=Bind _ _}     | _     | _     = Refl

463 |   apNonEmpty {g=Pure _}       {h=Labelled _ _} | _     | _     = Refl

465 |   apNonEmpty {g=Raw _}        {h=Pure _}       | _     | _     = Refl

466 |   apNonEmpty {g=OneOf _}      {h=Pure _}       | _     | _     = Refl

467 |   apNonEmpty {g=Bind _ _}     {h=Pure _}       | _     | _     = Refl

468 |   apNonEmpty {g=Labelled _ _} {h=Pure _}       | _     | _     = Refl

470 |   apNonEmpty {g=Raw _}        {h=Raw _}        | _     | _     = Refl

472 |   apNonEmpty {g=Labelled _ _} {h=Raw _}        | _     | False = Refl

473 |   apNonEmpty {g=Labelled _ _} {h=OneOf _}      | _     | False = Refl

474 |   apNonEmpty {g=Labelled _ _} {h=Bind _ _}     | _     | False = Refl

475 |   apNonEmpty {g=Labelled _ _} {h=Labelled _ _} | _     | False = Refl

477 |   apNonEmpty {g=Raw _}        {h=Labelled _ _} | False | False = Refl

478 |   apNonEmpty {g=OneOf _}      {h=Labelled _ _} | False | False = Refl

479 |   apNonEmpty {g=Bind _ _}     {h=Labelled _ _} | False | False = Refl

481 |   apNonEmpty {g=OneOf _}      {h=Raw _}        | False | False = Refl

482 |   apNonEmpty {g=OneOf _}      {h=OneOf _}      | False | False = Refl

483 |   apNonEmpty {g=OneOf _}      {h=Bind _ _}     | False | False = Refl

485 |   apNonEmpty {g=Bind _ _}     {h=OneOf _}      | False | False = Refl

486 |   apNonEmpty {g=Raw _}        {h=OneOf _}      | False | False = Refl

488 |   apNonEmpty {g=Raw _}        {h=Bind _ _}     | _     | False = Refl

489 |   apNonEmpty {g=Bind _ _}     {h=Raw _}        | _     | False = Refl

491 |   apNonEmpty {g=Bind _ _}     {h=Bind _ _}     | _     | False = Refl

494 | Applicative (Gen em) where

495 |   pure = Pure

496 |   g <*> h = rewrite sym $ minSame em in g <**> h

498 | private infixl 1 >>==

500 | (>>==) : {rem : _} -> Gen lem a -> (a -> Gen rem b) -> Gen (min lem rem) b

501 | 0 bindNonEmpty : {f : a -> Gen1 b} -> IsNonEmpty g => IsNonEmpty $ g >>== f

503 | Empty          >>== _  = rewrite minMaybeEmptyLeft rem in Empty

504 | Pure x         >>== nf = relax @{rightNoWeakerMin} $ nf x

505 | Raw g          >>== nf = Bind @{rightNoWeakerMin} g nf

506 | Bind @{nw} x f >>== nf = Bind @{minNoWeakerLeft nw} x $ (>>== nf) . f

507 | Labelled l x   >>== nf = label l $ x >>== nf

509 | (OneOf @{ne} @{nw} (MkGenAlts gs) >>== nf) {rem=NonEmpty} =

510 |   OneOf @{allMapTaggedLazy {f=assert_total (>>== nf)} $ \e => bindNonEmpty @{indexAll e ne}}

511 |         @{minNoWeakerLeft nw} $

512 |         MkGenAlts $ flip mapTaggedLazy gs $ assert_total (>>== nf)

515 | (OneOf oo >>== nf) {rem=MaybeEmpty} = do

516 |   rewrite minMaybeEmptyRight lem

517 |   mkOneOfMaybeEmpty

518 |     (mapMaybeTaggedLazy (nonEmpty . assert_total (>>== nf)) oo.unGenAlts)

519 |     @{allMapMaybeJustTaggedLazy {f=nonEmpty . assert_total (>>== nf)} $ \_, _ => nonEmptyNonEmpty}

521 | bindNonEmpty {g=Pure _}              = relaxNonEmpty @{isNonEmptyGen1}

522 | bindNonEmpty {g=Raw _}               = Refl

523 | bindNonEmpty {g=Bind _ _}            = Refl

524 | bindNonEmpty {g=Labelled _ _}        = labelNonEmpty @{bindNonEmpty}

525 | bindNonEmpty {g=OneOf $ MkGenAlts _} = Refl

528 | {em : _} -> Monad (Gen em) where

529 |   g >>= h = rewrite sym $ minSame em in g >>== h

535 | namespace GenAlternatives

537 |   export %inline

538 |   Nil : GenAlternatives False em a

539 |   Nil = MkGenAlts []

541 |   export %inline

542 |   (::) : (0 _ : lem `NoWeaker` em) =>

543 |          (0 _ : rem `NoWeaker` em) =>

544 |          (0 _ : IfUnsolved e True) =>

545 |          (0 _ : IfUnsolved em NonEmpty) =>

546 |          (0 _ : IfUnsolved lem em) =>

547 |          (0 _ : IfUnsolved rem em) =>

548 |          Lazy (Gen lem a) -> Lazy (GenAlternatives e rem a) -> GenAlternatives ne em a

549 |   x :: xs = MkGenAlts $ (1, relax x) :: mapTaggedLazy relax xs.unGenAlts

551 |   -- This concatenation breaks relative proportions in frequencies of given alternative lists

552 |   public export %inline

553 |   (++) : (0 _ : lem `NoWeaker` em) =>

554 |          (0 _ : rem `NoWeaker` em) =>

555 |          (0 _ : IfUnsolved lem em) =>

556 |          (0 _ : IfUnsolved rem em) =>

557 |          (0 _ : IfUnsolved nel False) =>

558 |          (0 _ : IfUnsolved ner False) =>

559 |          GenAlternatives nel lem a -> Lazy (GenAlternatives ner rem a) -> GenAlternatives (nel || ner) em a

560 |   xs ++ ys = MkGenAlts $ mapTaggedLazy relax xs.unGenAlts ++ mapTaggedLazy relax ys.unGenAlts

562 |   public export %inline

563 |   length : GenAlternatives ne em a -> Nat

564 |   length = length . unGenAlts

566 |   export %inline

567 |   processAlternatives : (Gen em a -> Gen em b) -> GenAlternatives ne em a -> GenAlternatives ne em b

568 |   processAlternatives = flip mapOneOf

570 |   export %inline

571 |   processAlternativesMaybe : (Gen em a -> Maybe $ Lazy (Gen em b)) -> GenAlternatives ne em a -> GenAlternatives False em b

572 |   processAlternativesMaybe f = MkGenAlts . mapMaybe (traverse $ f . force) . unGenAlts

574 |   export %inline

575 |   processAlternatives'' : (Gen em a -> GenAlternatives neb em b) -> GenAlternatives nea em a -> GenAlternatives (nea && neb) em b

576 |   processAlternatives'' f = mapGens where

578 |     mapWeight : forall a, nea. (Nat1 -> Nat1) -> GenAlternatives nea em a -> GenAlternatives nea em a

579 |     mapWeight f = MkGenAlts . map (mapFst f) . unGenAlts

581 |     mapGens : GenAlternatives nea em a -> GenAlternatives (nea && neb) em b

582 |     mapGens xs = MkGenAlts $ xs.unGenAlts `bind` \(w, x) => unGenAlts $ mapWeight (w *) $ f x

584 |   export %inline

585 |   processAlternatives' : (Gen em a -> GenAlternatives ne em b) -> GenAlternatives ne em a -> GenAlternatives ne em b

586 |   processAlternatives' f xs = rewrite sym $ andSameNeutral ne in processAlternatives'' f xs

588 |   export %inline

589 |   relax : GenAlternatives True em a -> GenAlternatives ne em a

590 |   relax = MkGenAlts . relaxT . unGenAlts

592 |   export %inline

593 |   strengthen : GenAlternatives ne em a -> Maybe $ GenAlternatives True em a

594 |   strengthen = map MkGenAlts . strengthen . unGenAlts

596 |   export

597 |   Functor (GenAlternatives ne em) where

598 |     map = processAlternatives . map

600 |   export

601 |   Applicative (GenAlternatives ne em) where

602 |     pure x = [ pure x ]

603 |     xs <*> ys = flip processAlternatives' xs $ flip processAlternatives ys . (<*>)

605 |   export

606 |   Alternative (GenAlternatives False em) where

607 |     empty = []

608 |     xs <|> ys = MkGenAlts $ xs.unGenAlts <|> ys.unGenAlts

610 |   -- implementation for `Monad` is below --

613 | Cast (LazyLst ne a) (GenAlternatives ne em a) where

614 |   cast = MkGenAlts . map (\x => (1, pure x))

616 | public export %inline

617 | altsFromList : LazyLst ne a -> GenAlternatives ne em a

618 | altsFromList = cast

629 | oneOf : {em : _} ->

630 |         (0 _ : alem `NoWeaker` em) =>

631 |         (0 _ : AltsNonEmpty altsNe em) =>

632 |         (0 _ : IfUnsolved alem em) =>

633 |         (0 _ : IfUnsolved altsNe $ em /= MaybeEmpty) =>

634 |         GenAlternatives altsNe alem a -> Gen em a

635 | oneOf = mkOneOf . unGenAlts

644 | frequency : {em : _} ->

645 |             (0 _ : alem `NoWeaker` em) =>

646 |             (0 _ : AltsNonEmpty altsNe em) =>

647 |             (0 _ : IfUnsolved alem em) =>

648 |             (0 _ : IfUnsolved altsNe $ em /= MaybeEmpty) =>

649 |             LazyLst altsNe (Nat1, Lazy (Gen alem a)) -> Gen em a

650 | frequency = oneOf . MkGenAlts

656 | elements : {em : _} ->

657 |            (0 _ : AltsNonEmpty altsNe em) =>

658 |            (0 _ : IfUnsolved em NonEmpty) =>

659 |            (0 _ : IfUnsolved altsNe $ em /= MaybeEmpty) =>

660 |            LazyLst altsNe a -> Gen em a

661 | elements = oneOf {alem=NonEmpty} . altsFromList

663 | export %inline

664 | elements' : Foldable f => (0 _ : IfUnsolved f List) => f a -> Gen0 a

665 | elements' xs = elements $ fromList $ toList xs

681 | alternativesOf : Gen em a -> GenAlternatives True em a

682 | 0 alternativesOfNonEmpty : {g : Gen em a} -> IsNonEmpty g => All IsNonEmpty $ alternativesOf g

684 | alternativesOf $ OneOf oo     = mapOneOf oo relax

685 | alternativesOf $ Labelled l x = mapOneOfElem (alternativesOf x) $ \g, e => Labelled l g @{indexAll e alternativesOfNonEmpty}

686 | alternativesOf g              = [g]

688 | alternativesOfNonEmpty {g=Pure _}        = [Refl]

689 | alternativesOfNonEmpty {g=Raw _}         = [Refl]

690 | alternativesOfNonEmpty {g=OneOf @{ne} _} = allMapOneOf $ \e => relaxNonEmpty @{indexAll e ne}

691 | alternativesOfNonEmpty {g=Bind _ _}      = [Refl]

692 | alternativesOfNonEmpty {g=Labelled _ _}  = allMapOneOfElem $ \_ => Refl

700 | deepAlternativesOf : (depth : Nat) -> Gen em a -> GenAlternatives True em a

701 | deepAlternativesOf 0     gen = [ gen ]

702 | deepAlternativesOf 1     gen = alternativesOf gen

703 | deepAlternativesOf (S k) gen = processAlternatives' alternativesOf $ deepAlternativesOf k gen

712 | forgetAlternatives : Gen em a -> Gen em a

713 | 0 forgetAlternativesNonEmpty : {g : Gen iem a} -> IsNonEmpty g => IsNonEmpty $ forgetAlternatives g

715 | forgetAlternatives g@(OneOf {})   = Labelled "forgetAlternatives" $ OneOf @{[Refl]} $ MkGenAlts [(1, g)]

716 | forgetAlternatives $ Labelled l x = Labelled @{forgetAlternativesNonEmpty} l $ forgetAlternatives x

717 | forgetAlternatives g              = g

719 | forgetAlternativesNonEmpty {g=Pure _}       = Refl

720 | forgetAlternativesNonEmpty {g=Raw _}        = Refl

721 | forgetAlternativesNonEmpty {g=OneOf _}      = Refl

722 | forgetAlternativesNonEmpty {g=Bind _ _}     = Refl

723 | forgetAlternativesNonEmpty {g=Labelled _ _} = Refl

738 | forgetStructure : {em : _} -> Gen em a -> Gen em a

739 | forgetStructure Empty             = Empty

740 | forgetStructure g@(Raw _)         = g

741 | forgetStructure g {em=NonEmpty}   = Raw $ MkRawGen $ unGen1 g

742 | forgetStructure g {em=MaybeEmpty} = MkRawGen (unGen' g) `Bind` maybe Empty Pure

744 | public export

745 | processAlternatives : (Gen em a -> Gen em b) -> Gen em a -> GenAlternatives True em b

746 | processAlternatives f = processAlternatives f . alternativesOf

748 | public export

749 | mapAlternativesOf : (a -> b) -> Gen em a -> GenAlternatives True em b

750 | mapAlternativesOf = processAlternatives . map

752 | public export %inline

753 | mapAlternativesWith : Gen em a -> (a -> b) -> GenAlternatives True em b

754 | mapAlternativesWith = flip mapAlternativesOf

759 | infix 8 `mapAlternativesOf`

760 |       , `mapAlternativesWith`

763 | {em : _} -> Monad (GenAlternatives True em) where

764 |   xs >>= f = flip processAlternatives' xs $ alternativesOf . (>>= oneOf . f)

783 | export %inline

784 | withAlts : {em : _} -> Gen em a -> Gen em a -> Gen em a

785 | a `withAlts` b = oneOf $ alternativesOf a ++ alternativesOf b

789 | infixr 2 `withAlts`

804 | export %inline

805 | withDeepAlts : {em : _} -> (depth : Nat) -> Gen em a -> Gen em a -> Gen em a

806 | withDeepAlts depth a b = oneOf $ deepAlternativesOf depth a ++ deepAlternativesOf depth b

816 | public export

817 | guard : Bool -> Gen0 ()

818 | guard True  = pure ()

819 | guard False = empty

822 | mapMaybe : (a -> Maybe b) -> Gen em a -> Gen0 b

823 | mapMaybe f g = maybe empty pure . f =<< relax g

826 | suchThat_withPrf : Gen em a -> (p : a -> Bool) -> Gen0 $ a `Subset` So . p

827 | suchThat_withPrf g p = mapMaybe lp g where

828 |   lp : a -> Maybe $ a `Subset` So . p

829 |   lp x with (p x) proof 0 prf

830 |     _ | True  = Just $ Element x $ eqToSo prf

831 |     _ | False = Nothing

833 | export infixl 4 `suchThat`

835 | public export

836 | suchThat : Gen em a -> (a -> Bool) -> Gen0 a

837 | suchThat g p = fst <$> suchThat_withPrf g p

840 | suchThat_dec : Gen em a -> ((x : a) -> Dec $ prop x) -> Gen0 $ Subset a prop

841 | suchThat_dec g f = mapMaybe d g where

842 |   d : a -> Maybe $ Subset a prop

843 |   d x = case f x of

844 |     Yes p => Just $ Element x p

845 |     No  _ => Nothing

849 | suchThat_invertedEq : DecEq b => Gen em a -> (y : b) -> (f : a -> b) -> Gen0 $ Subset a $ \x => y = f x

850 | suchThat_invertedEq g y f = g `suchThat_dec` \x => y `decEq` f x

856 | retryUntil_withPrf : (p : a -> Bool) -> (Fuel -> Gen em a) -> Fuel -> Gen0 $ a `Subset` So . p

857 | retryUntil_withPrf p f Dry           = f Dry `suchThat_withPrf` p

858 | retryUntil_withPrf p f fl'@(More fl) = do

859 |   x <- relax $ f fl'

860 |   case @@ p x of

861 |     (True ** prf) => pure $ Element x $ eqToSo prf

862 |     (False ** _)  => retryUntil_withPrf p f fl

867 | public export %inline

868 | retryUntil : (p : a -> Bool) -> (Fuel -> Gen em a) -> Fuel -> Gen0 a

869 | retryUntil p = map fst .: retryUntil_withPrf p

875 | retryUntil_dec : (p : (x : a) -> Dec $ prop x) -> (Fuel -> Gen em a) -> Fuel -> Gen0 $ Subset a prop

876 | retryUntil_dec p f Dry           = f Dry `suchThat_dec` p

877 | retryUntil_dec p f fl'@(More fl) = do

878 |   x <- relax $ f fl'

879 |   case p x of

880 |     Yes p => pure $ Element x p

881 |     No _  => retryUntil_dec p f fl

887 | iterate : Nat -> (a -> a) -> a -> a

888 | iterate Z     _ = id

889 | iterate (S n) f = iterate n f . f

893 | variant : {em : _} -> Nat -> Gen em a -> Gen em a

894 | variant _ Empty               = Empty

895 | variant Z gen                 = gen

896 | variant n gen {em=NonEmpty}   = Raw $ MkRawGen $ iterate n independent $ unGen1 gen

897 | variant n gen {em=MaybeEmpty} = MkRawGen (iterate n independent $ unGen' gen) `Bind` maybe Empty Pure

904 | listOf : {em : _} -> {default (choose (0, 10)) length : Gen em Nat} -> Gen em a -> Gen em $ List a

905 | listOf g = sequence $ List.replicate !length g

908 | vectOf : {em : _} -> {n : Nat} -> Gen em a -> Gen em $ Vect n a

909 | vectOf = sequence . replicate n