0 | ||| The content of this module is based on the paper
 1 | ||| Applications of Applicative Proof Search
 2 | ||| by Liam O'Connor
 3 | ||| https://doi.org/10.1145/2976022.2976030
 4 | |||
 5 | ||| The main difference is that we use `Colist1` for the type of
 6 | ||| generators rather than `Stream`. This allows us to avoid generating
 7 | ||| many duplicates when dealing with finite types which are common in
 8 | ||| programming (Bool) but even more so in dependently typed programming
 9 | ||| (Vect 0, Fin (S n), etc.).
10 |
11 | module Search.Generator
12 |
13 | import Data.Colist
14 | import Data.Colist1
15 | import Data.Fin
16 | import Data.Stream
17 | import Data.Vect
18 |
19 | ------------------------------------------------------------------------
20 | -- Interface
21 |
22 | ||| A generator for a given type is a non-empty colist of values of that
23 | ||| type.
24 | public export
25 | interface Generator a where
26 |   generate : Colist1 a
27 |
28 | ------------------------------------------------------------------------
29 | -- Implementations
30 |
31 | -- Finite types
32 |
33 | ||| ALL of the natural numbers
34 | public export
35 | Generator Nat where
36 |   generate = fromStream nats
37 |
38 | ||| ALL of the booleans
39 | public export
40 | Generator Bool where
41 |   generate = True ::: [False]
42 |
43 | ||| ALL of the Fins
44 | public export
45 | {n : Nat} -> Generator (Fin (S n)) where
46 |   generate = fromList1 (allFins n)
47 |
48 | -- Polymorphic generators
49 |
50 | ||| We typically want to generate a generator for a unit-terminated right-nested
51 | ||| product so we have this special case that keeps the generator minimal.
52 | public export
53 | Generator a => Generator (a, ()) where
54 |   generate = map (,()) generate
55 |
56 | ||| Put two generators together by exploring the plane they define.
57 | ||| This uses Cantor's zig zag traversal
58 | public export
59 | (Generator a, Generator b) => Generator (a, b) where
60 |   generate = plane generate (\ _ => generate)
61 |
62 | ||| Put two generators together by exploring the plane they define.
63 | ||| This uses Cantor's zig zag traversal
64 | public export
65 | {0 b : a -> Type} -> (Generator a, (x : a) -> Generator (b x)) =>
66 |   Generator (x : a ** b x) where
67 |   generate = plane generate (\ x => generate)
68 |
69 | ||| Build entire vectors of values
70 | public export
71 | {n : Nat} -> Generator a => Generator (Vect n a) where
72 |   generate = case n of
73 |     Z => [] ::: []
74 |     S n => map (uncurry (::)) generate
75 |
76 | ||| Generate arbitrary lists of values
77 | ||| Departing from the paper, to avoid having infinitely many copies of
78 | ||| the empty list, we handle the case `n = 0` separately.
79 | public export
80 | Generator a => Generator (List a) where
81 |   generate = [] ::: forget (planeWith listy generate vectors) where
82 |     listy : (n : Nat) -> Vect (S n) a -> List a
83 |     listy _ = toList
84 |
85 |     vectors : (n : Nat) -> Colist1 (Vect (S n) a)
86 |     vectors n = generate
87 |