0 | module Test.Data.Graph.Generators
 1 |
 2 | import public Chem
 3 | import public Hedgehog
 4 |
 5 | import Data.List
 6 | import Data.Refined.Bits32
 7 | import Data.Vect
 8 |
 9 | --------------------------------------------------------------------------------
10 | --          Generators
11 | --------------------------------------------------------------------------------
12 |
13 | export
14 | edge : {k : _} -> Gen e -> Gen (Edge (S $ S k) e)
15 | edge lbl =
16 |   let gnode = fin {n = S (S k)} (constant FZ last)
17 |    in [| toEdge gnode gnode lbl |]
18 |   where
19 |     toEdge : Fin (S $ S k) -> Fin (S $ S k) -> e -> Edge (S $ S k) e
20 |     toEdge k j l = fromMaybe (E 0 1 l) (mkEdge k j l)
21 |
22 | export
23 | edges :
24 |      {k : _}
25 |   -> (nrEdges    : Hedgehog.Range Nat)
26 |   -> (label      : Gen e)
27 |   -> Gen (List $ Edge k e)
28 | edges {k = S (S m)} nr lbl = list nr (edge lbl)
29 | edges               _  _   = pure []
30 |
31 | export
32 | lgraph :
33 |      (nrNodes   : Hedgehog.Range Nat)
34 |   -> (nrEdges   : Hedgehog.Range Nat)
35 |   -> (edgeLabel : Gen e)
36 |   -> (nodeLabel : Gen n)
37 |   -> Gen (Graph e n)
38 | lgraph nrn nre el nl = do
39 |   ns <- list nrn nl
40 |   es <- edges nre el
41 |   pure $ (G (length ns) $ mkGraphL ns es)
42 |