0 | module Hedgehog.Internal.Gen

  2 | import Data.Bounded

  3 | import Data.Colist

  4 | import Data.Cotree

  5 | import Data.Fin

  6 | import Data.List

  7 | import Data.List.Quantifiers

  8 | import Data.List1

  9 | import Data.Nat

 10 | import Data.SOP

 11 | import Data.String

 12 | import Data.Tree

 13 | import Data.Vect

 14 | import Data.Vect.Quantifiers

 16 | import Control.Monad.Maybe

 18 | import Hedgehog.Internal.Range

 19 | import Hedgehog.Internal.Shrink

 20 | import Hedgehog.Internal.Util

 22 | import System.Random.Pure.StdGen

 24 | %hide Prelude.Range

 26 | %default total

 33 | public export

 34 | record Gen (a : Type) where

 35 |   constructor MkGen

 36 |   unGen   : Size -> StdGen -> Cotree a

 38 | public export %inline

 39 | runGen : Size -> StdGen -> Gen a -> Cotree a

 40 | runGen si se g = unGen g si se

 42 | public export

 43 | mapGen :  (f : Cotree a -> Cotree b) -> Gen a -> Gen b

 44 | mapGen f (MkGen run) = MkGen $ \si,se => f (run si se)

 48 | public export

 49 | fromTree : Cotree a -> Gen a

 50 | fromTree ct = MkGen $ \_,_ => ct

 53 | public export

 54 | toTree : Gen a -> Gen (Cotree a)

 55 | toTree (MkGen unGen) = MkGen $ \si,se => pure (unGen si se)

 61 | public export

 62 | Functor Gen where

 63 |   map f (MkGen g) = MkGen $ \si,se => map f (g si se)

 65 | public export

 66 | Applicative Gen where

 67 |   pure a = MkGen $ \_,_ => pure a

 69 |   MkGen ff <*> MkGen fa =

 70 |     MkGen $ \si,se =>

 71 |       let (se1,se2) := split se

 72 |        in interleave (ff si se1) (fa si se2)

 74 | public export

 75 | Monad Gen where

 76 |   MkGen run >>= f =

 77 |     MkGen $ \si,se =>

 78 |       let (se1,se2) := split se

 79 |           ta        := run si se1

 80 |        in bind ta (runGen si se2 . f)

 86 | public export

 87 | generate : (Size -> StdGen -> a) -> Gen a

 88 | generate  f = MkGen $ \si,se => pure (f si se)

 94 | public export

 95 | shrink : (a -> Colist a) -> Gen a -> Gen a

 96 | shrink f = mapGen (expand f)

 98 | public export %inline

 99 | prune : Gen a -> Gen a

100 | prune = mapGen prune

107 | public export

108 | sized : (Size -> Gen a) -> Gen a

109 | sized f = generate (\si,_ => si) >>= f

112 | public export

113 | scale : (Size -> Size) -> Gen a -> Gen a

114 | scale f (MkGen run) = MkGen $ \si,se => run (f si) se

118 | public export %inline

119 | resize : Size -> Gen a -> Gen a

120 | resize size = scale (const size)

126 | public export

127 | golden : Size -> Size

128 | golden = resize $ \n => round (0.61803398875 * cast n)

131 | public export %inline

132 | small : Gen a -> Gen a

133 | small = scale golden

142 | public export

143 | integral_ : ToInteger a => Range a -> Gen a

144 | integral_ range = generate $ \si,se =>

145 |   let (x, y) := bounds si range

146 |    in fromInteger . snd $ randomR (toInteger x, toInteger y) se

181 | public export

182 | integral : ToInteger a => Range a -> Gen a

183 | integral range = shrink (towards $ origin range) (integral_ range)

188 | public export %inline

189 | int : Range Int -> Gen Int

190 | int = integral

195 | public export %inline

196 | int8 : Range Int8 -> Gen Int8

197 | int8 = integral

202 | public export %inline

203 | anyInt8 : Gen Int8

204 | anyInt8 = int8 (exponentialFrom 0 minBound maxBound)

209 | public export %inline

210 | int16 : Range Int16 -> Gen Int16

211 | int16 = integral

216 | public export %inline

217 | anyInt16 : Gen Int16

218 | anyInt16 = int16 (exponentialFrom 0 minBound maxBound)

223 | public export %inline

224 | int32 : Range Int32 -> Gen Int32

225 | int32 = integral

230 | public export %inline

231 | anyInt32 : Gen Int32

232 | anyInt32 = int32 (exponentialFrom 0 minBound maxBound)

237 | public export %inline

238 | int64 : Range Int64 -> Gen Int64

239 | int64 = integral

244 | public export %inline

245 | anyInt64 : Gen Int64

246 | anyInt64 = int64 (exponentialFrom 0 minBound maxBound)

251 | public export %inline

252 | bits8 : Range Bits8 -> Gen Bits8

253 | bits8 = integral

258 | public export %inline

259 | anyBits8 : Gen Bits8

260 | anyBits8 = bits8 (exponential 0 maxBound)

265 | public export %inline

266 | bits16 : Range Bits16 -> Gen Bits16

267 | bits16 = integral

272 | public export %inline

273 | anyBits16 : Gen Bits16

274 | anyBits16 = bits16 (exponential 0 maxBound)

279 | public export %inline

280 | bits32 : Range Bits32 -> Gen Bits32

281 | bits32 = integral

286 | public export %inline

287 | anyBits32 : Gen Bits32

288 | anyBits32 = bits32 (exponential 0 maxBound)

293 | public export %inline

294 | bits64 : Range Bits64 -> Gen Bits64

295 | bits64 = integral

300 | public export %inline

301 | anyBits64 : Gen Bits64

302 | anyBits64 = bits64 (exponential 0 maxBound)

307 | public export %inline

308 | integer : Range Integer -> Gen Integer

309 | integer = integral

314 | public export %inline

315 | nat : Range Nat -> Gen Nat

316 | nat = integral

321 | public export %inline

322 | size : Range Size -> Gen Size

323 | size = integral

326 | public export

327 | fin : {n : _} -> Range (Fin n) -> Gen (Fin n)

328 | fin range =

329 |   let rangeInt := map finToInteger range

330 |    in map toFin (integer rangeInt)

332 |   where

333 |     toFin : Integer -> Fin n

334 |     toFin k = fromMaybe range.origin (integerToFin k n)

344 | double_ : Range Double -> Gen Double

345 | double_ range =

346 |   generate $ \si,se =>

347 |     let (x, y) := bounds si range

348 |      in snd $ randomR (x, y) se

354 | export %inline

355 | double : Range Double -> Gen Double

356 | double range = shrink (towardsDouble $ origin range) (double_ range)

365 | public export %inline

366 | constant : a -> Gen a

367 | constant = pure

372 | public export

373 | element : {k : _} -> Vect (S k) a -> Gen a

374 | element vs = map (`index` vs) (fin $ constant FZ last)

379 | public export %inline

380 | element_ : {k : _} -> Vect (S k) a -> Gen a

381 | element_ = prune . element

386 | public export %inline

387 | choice : {k : _} -> Vect (S k) (Gen a) -> Gen a

388 | choice vs = element vs >>= id

394 | public export %inline

395 | choice_ : {k : _} -> Vect (S k) (Gen a) -> Gen a

396 | choice_ vs = element_ vs >>= id

405 | public export

406 | frequency : Vect (S k) (Nat, Gen a) -> Gen a

407 | frequency ps =

408 |   let acc   := scanl1 addFst $ map (mapFst toInteger) ps

409 |       gen   := integral_ . constant 0 . fst $ last acc

410 |       lower := \n => takeWhile (< n) (fromFoldable $ map fst acc)

412 |   in shrink lower gen >>= choose acc

414 |   where

415 |     addFst : (Integer,x) -> (Integer,x) -> (Integer,x)

416 |     addFst (x,_) (y,v) = (x + y,v)

418 |     choose : Vect n (Integer, Gen a) -> Integer -> Gen a

419 |     choose []             _ = snd $ head ps

420 |     choose ((i, v) :: ps) k = if i >= k then v else choose ps k

425 | public export %inline

426 | bool : Gen Bool

427 | bool = element [False,True]

430 | export %inline

431 | unit : Gen ()

432 | unit = pure ()

442 | char : Range Char -> Gen Char

443 | char = map chr . int . map ord

448 | export %inline

449 | charc : (lower : Char) -> (upper : Char) -> Gen Char

450 | charc l u = char $ constant l u

454 | export %inline

455 | binit : Gen Char

456 | binit = charc '0' '1'

459 | export %inline

460 | octit : Gen Char

461 | octit = charc '0' '7'

464 | export %inline

465 | digit : Gen Char

466 | digit = charc '0' '9'

470 | hexit : Gen Char

471 | hexit = frequency [(10, digit),(6, charc 'a' 'f'),(6, charc 'A' 'F')]

474 | export %inline

475 | lower : Gen Char

476 | lower = charc 'a' 'z'

479 | export %inline

480 | upper : Gen Char

481 | upper = charc 'A' 'Z'

484 | export %inline

485 | alpha : Gen Char

486 | alpha = choice [lower,upper]

490 | alphaNum : Gen Char

491 | alphaNum = frequency [(10,digit),(24,lower),(24,upper)]

494 | export %inline

495 | ascii : Gen Char

496 | ascii = charc '\0' '\127'

501 | export %inline

502 | printableAscii : Gen Char

503 | printableAscii = charc '\32' '\126'

506 | export %inline

507 | latin : Gen Char

508 | latin = charc '\0' '\255'

512 | printableLatin : Gen Char

513 | printableLatin = frequency [ (95, printableAscii), (96, charc '\160' '\255') ]

519 | unicode : Gen Char

520 | unicode =

521 |   frequency

522 |     [ (55296, charc '\0' '\55295')

523 |     , (8190, charc '\57344' '\65533')

524 |     , (1048576, charc '\65536' '\1114111')

525 |     ]

532 | printableUnicode : Gen Char

533 | printableUnicode =

534 |   frequency

535 |     [ (95, printableAscii)

536 |     , (55136, charc '\160' '\55295')

537 |     , (8190, charc '\57344' '\65533')

538 |     , (1048576, charc '\65536' '\1114111')

539 |     ]

544 | export %inline

545 | unicodeAll : Gen Char

546 | unicodeAll =

547 |   frequency

548 |     [ (55296, charc '\0' '\55295')

549 |     , (1056768, charc '\57344' '\1114111')

550 |     ]

558 | maybe : Gen a -> Gen (Maybe a)

559 | maybe gen =

560 |   sized $ \s =>

561 |     frequency

562 |       [ (2, constant Nothing)

563 |       , (S s.size, Just <$> gen)

564 |       ]

570 | either : Gen a -> Gen b -> Gen (Either a b)

571 | either genA genB =

572 |   sized $ \s =>

573 |     frequency

574 |       [ (2, Left <$> genA)

575 |       , (S s.size, Right <$> genB)

576 |       ]

581 | export %inline

582 | either_ : Gen a -> Gen b -> Gen (Either a b)

583 | either_ genA genB = choice [Left <$> genA, Right <$> genB]

587 | vect : (n : Nat) -> Gen a -> Gen (Vect n a)

588 | vect 0     _ = pure []

589 | vect (S k) g = [| g :: vect k g |]

593 | list : Range Nat -> Gen a -> Gen (List a)

594 | list range gen =

595 |   sized $ \si =>

596 |     let minLength := lowerBound si range

597 |      in mapGen (interleave minLength . value) $

598 |         integral_ range >>= (\n => map toList (vect n (toTree gen)))

602 | list1 : Range Nat -> Gen a -> Gen (List1 a)

603 | list1 range gen = [| gen ::: list (map pred range) gen |]

607 | string : Range Nat -> Gen Char -> Gen String

608 | string range = map fastPack . list range

612 | hlist : All Gen ts -> Gen (HList ts)

613 | hlist []      = [| [] |]

614 | hlist (x::xs) = [| x :: hlist xs |]

618 | hvect : All Gen ts -> Gen (HVect ts)

619 | hvect []      = [| [] |]

620 | hvect (x::xs) = [| x :: hvect xs |]

626 | collapseNPV : NP (K a) ks -> {auto 0 _ : NonEmpty ks} -> (k ** Vect (S k) a)

627 | collapseNPV {ks = _} [] impossible

628 | collapseNPV {ks = _} (v::[]) = (0 ** [v])

629 | collapseNPV {ks = t::t2::ts}(v::v2::vs) =

630 |   let (k ** vs2) := collapseNPV {ks = t2 :: ts} (v2 :: vs)

631 |    in (S k ** (v :: vs2))

636 | np : NP Gen ts -> Gen (NP I ts)

637 | np = sequenceNP

644 | ns : NP Gen ts -> {auto 0 prf : NonEmpty ts} -> Gen (NS I ts)

645 | ns np =

646 |   let (_ ** vs) := collapseNPV (apInjsNP_ np)

647 |    in choice (map sequenceNS vs)

654 | ns_ : NP Gen ts -> {auto 0 prf : NonEmpty ts} -> Gen (NS I ts)

655 | ns_ np =

656 |   let (_ ** vs) := collapseNPV (apInjsNP_ np)

657 |    in choice_ (map sequenceNS vs)

660 | sop : POP Gen tss -> {auto 0 prf : NonEmpty tss} -> Gen (SOP I tss)

661 | sop p =

662 |   let (_ ** vs) := collapseNPV {a = SOP Gen tss} (apInjsPOP_ p)

663 |    in choice (map sequenceSOP vs)

674 | printWith : (HasIO io, Show a) => Size -> StdGen -> Gen a -> io ()

675 | printWith si se gen =

676 |   let (MkCotree v fo) := runGen si se gen

677 |       shrinks         := value <$> take 1000 fo

678 |    in do

679 |      putStrLn "=== Outcome ==="

680 |      putStrLn (show v)

681 |      putStrLn "=== Shrinks ==="

682 |      traverse_ printLn shrinks

698 | print : Show a => HasIO io => Gen a -> io ()

699 | print gen = initSeed >>= \se => printWith 100 se gen

703 | sample : HasIO io => Gen a -> io a

704 | sample gen = (value . gen.unGen 100) <$> initSeed

709 | renderTree :

710 |      {auto _ : Show a}

711 |   -> (maxDepth : Nat)

712 |   -> (maxWidth : Nat)

713 |   -> Size

714 |   -> StdGen

715 |   -> Gen a

716 |   -> String

717 | renderTree md mw si se = drawTree

718 |                        . map show

719 |                        . toTree md mw

720 |                        . runGen si se

727 | printTreeWith :

728 |      {auto _ : Show a}

729 |   -> {auto _ : HasIO io}

730 |   -> (maxDepth : Nat)

731 |   -> (maxWidth : Nat)

732 |   -> Size

733 |   -> StdGen

734 |   -> Gen a

735 |   -> io ()

736 | printTreeWith md mw si se = putStrLn . renderTree md mw si se

756 | printTree :

757 |      {auto _ : Show a}

758 |   -> {auto _ : HasIO io}

759 |   -> (maxDepth : Nat)

760 |   -> (maxWidth : Nat)

761 |   -> Gen a

762 |   -> io ()

763 | printTree md mw gen = initSeed >>= \se => printTreeWith md mw 100 se gen