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}

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

311 | unGen1 $ Pure x         = pure x

312 | unGen1 $ Raw sf         = sf.unRawGen

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

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

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

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

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

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

321 | unGenAll' seed gen = do

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

323 |   sv :: unGenAll' seed gen

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

327 | unGenAll = map snd .: unGenAll'

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

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

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

338 | unGen $ Empty        = throwError ()

339 | unGen $ Pure x       = pure x

340 | unGen $ Raw sf       = sf.unRawGen

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

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

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

345 | export %inline

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

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

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

351 | unGenTryAll' seed gen = do

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

353 |   sv :: unGenTryAll' seed gen

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

357 | unGenTryAll = map snd .: unGenTryAll'

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

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

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

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

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

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

385 | Functor RawGen where

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

388 | Applicative RawGen where

389 |   pure x = MkRawGen $ pure x

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

394 | Functor (Gen em)

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

397 | Functor (Gen em) where

398 |   map f $ Empty          = Empty

399 |   map f $ Pure x         = Pure $ f x

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

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

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

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

405 | mapNonEmpty {g=Pure _}       = Refl

406 | mapNonEmpty {g=Raw _}        = Refl

407 | mapNonEmpty {g=OneOf _}      = Refl

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

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

411 | private infixl 3 <**>

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

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

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

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

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

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

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

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

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

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

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

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

430 |             @{minNoWeakerLeft nw} $

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

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

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

434 |           @{minNoWeakerRight nw} $

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

484 | Applicative (Gen em) where

485 |   pure = Pure

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

488 | private infixl 1 >>==

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

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

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

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

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

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

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

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

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

501 |         @{minNoWeakerLeft nw} $

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

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

506 |   rewrite minMaybeEmptyRight lem

507 |   mkOneOfMaybeEmpty

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

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

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

512 | bindNonEmpty {g=Raw _}               = Refl

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

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

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

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

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

525 | namespace GenAlternatives

527 |   export %inline

528 |   Nil : GenAlternatives False em a

529 |   Nil = MkGenAlts []

531 |   export %inline

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

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

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

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

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

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

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

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

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

542 |   public export %inline

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

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

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

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

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

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

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

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

552 |   public export %inline

553 |   length : GenAlternatives ne em a -> Nat

554 |   length = length . unGenAlts

556 |   export %inline

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

558 |   processAlternatives = flip mapOneOf

560 |   export %inline

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

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

564 |   export %inline

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

566 |   processAlternatives'' f = mapGens where

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

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

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

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

574 |   export %inline

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

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

578 |   export %inline

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

580 |   relax = MkGenAlts . relaxT . unGenAlts

582 |   export %inline

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

584 |   strengthen = map MkGenAlts . strengthen . unGenAlts

586 |   export

587 |   Functor (GenAlternatives ne em) where

588 |     map = processAlternatives . map

590 |   export

591 |   Applicative (GenAlternatives ne em) where

592 |     pure x = [ pure x ]

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

595 |   export

596 |   Alternative (GenAlternatives False em) where

597 |     empty = []

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

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

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

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

606 | public export %inline

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

608 | altsFromList = cast

619 | oneOf : {em : _} ->

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

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

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

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

624 |         GenAlternatives altsNe alem a -> Gen em a

625 | oneOf = mkOneOf . unGenAlts

634 | frequency : {em : _} ->

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

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

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

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

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

640 | frequency = oneOf . MkGenAlts

646 | elements : {em : _} ->

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

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

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

650 |            LazyLst altsNe a -> Gen em a

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

653 | export %inline

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

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

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

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

674 | alternativesOf $ OneOf oo     = mapOneOf oo relax

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

676 | alternativesOf g              = [g]

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

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

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

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

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

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

691 | deepAlternativesOf 0     gen = [ gen ]

692 | deepAlternativesOf 1     gen = alternativesOf gen

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

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

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

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

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

707 | forgetAlternatives g              = g

709 | forgetAlternativesNonEmpty {g=Pure _}       = Refl

710 | forgetAlternativesNonEmpty {g=Raw _}        = Refl

711 | forgetAlternativesNonEmpty {g=OneOf _}      = Refl

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

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

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

729 | forgetStructure Empty             = Empty

730 | forgetStructure g@(Raw _)         = g

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

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

734 | public export

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

736 | processAlternatives f = processAlternatives f . alternativesOf

738 | public export

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

740 | mapAlternativesOf = processAlternatives . map

742 | public export %inline

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

744 | mapAlternativesWith = flip mapAlternativesOf

749 | infix 8 `mapAlternativesOf`

750 |       , `mapAlternativesWith`

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

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

773 | export %inline

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

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

779 | infixr 2 `withAlts`

794 | export %inline

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

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

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

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

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

808 | suchThat_withPrf g p = mapMaybe lp g where

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

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

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

812 |     _ | False = Nothing

814 | export infixl 4 `suchThat`

816 | public export

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

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

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

822 | suchThat_dec g f = mapMaybe d g where

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

824 |   d x = case f x of

825 |     Yes p => Just $ Element x p

826 |     No  _ => Nothing

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

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

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

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

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

840 |   x <- relax $ f fl'

841 |   case @@ p x of

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

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

848 | public export %inline

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

850 | retryUntil p = map fst .: retryUntil_withPrf p

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

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

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

859 |   x <- relax $ f fl'

860 |   case p x of

861 |     Yes p => pure $ Element x p

862 |     No _  => retryUntil_dec p f fl

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

869 | iterate Z     _ = id

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

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

875 | variant _ Empty               = Empty

876 | variant Z gen                 = gen

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

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

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

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

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

890 | vectOf = sequence . replicate n