handwritten.txt

https://github.com/nick8325/quickcheck/blob/master/examples/Heap.hs

Heap:
instance (Ord a, Arbitrary a) => Arbitrary (Heap a) where
  arbitrary = sized (arbHeap Nothing)
   where
    arbHeap mx n =
      frequency $
        [ (1, return Empty) ] ++
        [ (7, do my <- arbitrary `suchThatMaybe` ((>= mx) . Just)
                 case my of
                   Nothing -> return Empty
                   Just y  -> liftM2 (Node y) arbHeap2 arbHeap2
                    where arbHeap2 = arbHeap (Just y) (n `div` 2))
        | n > 0
        ]


Set:
https://github.com/nick8325/quickcheck/blob/master/examples/Set.hs

instance (Ord a, Arbitrary a) => Arbitrary (Set a) where
  arbitrary = sized (arbSet Nothing Nothing)
   where
    arbSet mx my n =
      frequency $
        [ (1, return Empty) ] ++
        [ (7, do mz <- arbitrary `suchThatMaybe` (isOK mx my)
                 case mz of
                   Nothing -> return Empty
                   Just z  -> liftM2 (Node z) (arbSet mx mz n2)
                                              (arbSet mz my n2)
                    where n2 = n `div` 2)
        | n > 0
        ]

    isOK mx my z =
      maybe True (<z) mx && maybe True (z<) my

RBtree:
https://github.com/QuickChick/QuickChick/blob/master/examples/RedBlack/testing.v
Program Fixpoint genRBTree_height (hc : nat*color) {wf wf_hc hc} : G tree :=
  match hc with
  | (0, Red) => returnGen Leaf
  | (0, Black) => oneOf [returnGen Leaf;
                    (do! n <- arbitrary; returnGen (Node Red Leaf n Leaf))]
  | (S h, Red) => liftGen4 Node (returnGen Black) (genRBTree_height (h, Black))
                                        arbitrary (genRBTree_height (h, Black))
  | (S h, Black) => do! c' <- genColor;
                    let h' := match c' with Red => S h | Black => h end in
                    liftGen4 Node (returnGen c') (genRBTree_height (h', c'))
                                       arbitrary (genRBTree_height (h', c')) end.

https://softwarefoundations.cis.upenn.edu/qc-current/QC.html

Fixpoint genSortedList (low high : nat) (size : nat)
             : G (list nat) :=
  match size with
  | O ⇒ ret []
  | S size' ⇒
    if high <? low then
      ret []
    else
      freq [ (1, ret []) ;
             (size, x <- choose (low, high);;
                    xs <- genSortedList x high size';;
                    ret (x :: xs)) ] end.


Fixpoint genTreeSized' {A} (sz : nat) (g : G A) : G (Tree A) :=
  match sz with
    | O ⇒ ret Leaf
    | S sz' ⇒
        freq [ (1, ret Leaf) ;
               (sz, liftM3 Node g (genTreeSized' sz' g)
                                  (genTreeSized' sz' g))
             ]
  end.


https://lemonidas.github.io/pdf/GeneratingGoodGenerators.pdf
Complete Tree:
Fixpoint gen_complete (in1 : nat) : G (option Tree) :=
match in1 with
| O => ret (Some Leaf)
| S n => doM! l <- gen_complete n;
doM! r <- gen_complete n;
do! x <- arbitrary;
ret (Some (Node x l r))
end.

Sized BST:
Definition gen_bst in1 in2 : nat -> G (option Tree) :=
let fix aux_arb size (in1 in2 : nat) : G (option (Tree)) :=
match size with
| O => ret (Some Leaf)
| S size' =>
backtrack [(1, ret (Some Leaf))
;(1, doM! x <- arbitraryST (fun x => in1 < x);
if (x < in2)? then
doM! l <- aux_arb size' in1 x;
doM! r <- aux_arb size' x in2;
ret (Some (Node x l r))
else ret None)]
end in
fun size => aux_arb size in1 in2.

BST:...



Compliate example: stack machine.
genInstrMem
https://github.com/QuickChick/TestingNoninterference/blob/master/stack/Generation.hs

Elrond:
...