@@ -0,0 +1,39 @@
1+module Test.Random
2+
3+import Effects
4+import Effect.Random
5+
6+genKVPair : (genA : Eff a [RND])
7+ -> (genB : Eff b [RND])
8+ -> Eff (Pair a b) [RND]
9+genKVPair f g = pure (!f, !g)
10+
11+genRndListKVUE : (Eq a, Eq b) =>
12+ (seed : Integer)
13+ -> (len : Nat)
14+ -> (genA : Eff a [RND])
15+ -> (genB : Eff b [RND])
16+ -> Eff (List (Pair a b)) [RND]
17+genRndListKVUE s l f g = do srand s; pure !(doGen l (genKVPair f g))
18+ where
19+ genElem : (Eq a, Eq b)
20+ => (generator : Eff (Pair a b) [RND])
21+ -> (existing : List (Pair a b))
22+ -> Eff (Pair a b) [RND]
23+ genElem j xs = do
24+ x <- j
25+ if elem x xs
26+ then genElem j xs
27+ else if isJust $ lookup (fst x) xs
28+ then genElem j xs
29+ else pure x
30+
31+ doGen : (Eq a, Eq b)
32+ => (count : Nat)
33+ -> (generator : Eff (Pair a b) [RND])
34+ -> Eff (List (Pair a b)) [RND]
35+ doGen Z j = pure Nil
36+ doGen (S n) j = do
37+ xs <- doGen n j
38+ x <- genElem j xs
39+ pure (x::xs)