0 | ||| The content of this module is based on the paper
  1 | ||| A Completely Unique Account of Enumeration
  2 | ||| by Cas van der Rest, and Wouter Swierstra
  3 | ||| https://doi.org/10.1145/3547636
  4 |
  5 | module Data.Enumerate
  6 |
  7 | import Data.List
  8 | import Data.Description.Regular
  9 | import Data.Stream
 10 |
 11 | import Data.Enumerate.Common
 12 |
 13 | %default total
 14 |
 15 | ------------------------------------------------------------------------------
 16 | -- Definition of enumerators
 17 | ------------------------------------------------------------------------------
 18 |
 19 | ||| An (a,b)-enumerator is an enumerator for values of type b provided
 20 | ||| that we already know how to enumerate subterms of type a
 21 | export
 22 | record Enumerator (a, b : Type) where
 23 |   constructor MkEnumerator
 24 |   runEnumerator : List a -> List b
 25 |
 26 | ------------------------------------------------------------------------------
 27 | -- Combinators to build enumerators
 28 | ------------------------------------------------------------------------------
 29 |
 30 | export
 31 | Functor (Enumerator a) where
 32 |   map f (MkEnumerator enum) = MkEnumerator (\ as => f <$> enum as)
 33 |
 34 | ||| This interleaving is fair, unlike one defined using concatMap.
 35 | ||| Cf. paper for definition of fairness
 36 | export
 37 | pairWith : (b -> c -> d) -> Enumerator a b -> Enumerator a c -> Enumerator a d
 38 | pairWith f (MkEnumerator e1) (MkEnumerator e2)
 39 |   = MkEnumerator (\ as => prodWith f (e1 as) (e2 as)) where
 40 |
 41 | export
 42 | pair : Enumerator a b -> Enumerator a c -> Enumerator a (b, c)
 43 | pair = pairWith (,)
 44 |
 45 | export
 46 | Applicative (Enumerator a) where
 47 |   pure = MkEnumerator . const . pure
 48 |   (<*>) = pairWith ($)
 49 |
 50 | export
 51 | Monad (Enumerator a) where
 52 |   xs >>= ks = MkEnumerator $ \ as =>
 53 |     foldr (\ x => interleave (runEnumerator (ks x) as)) []
 54 |       (runEnumerator xs as)
 55 |
 56 | export
 57 | Alternative (Enumerator a) where
 58 |   empty = MkEnumerator (const [])
 59 |   MkEnumerator e1 <|> MkEnumerator e2 = MkEnumerator (\ as => interleave (e1 as) (e2 as))
 60 |
 61 | ||| Like `pure` but returns more than one result
 62 | export
 63 | const : List b -> Enumerator a b
 64 | const = MkEnumerator . const
 65 |
 66 | ||| The construction of recursive substructures is memoised by
 67 | ||| simply passing the result of the recursive call
 68 | export
 69 | rec : Enumerator a a
 70 | rec = MkEnumerator id
 71 |
 72 | namespace Example
 73 |
 74 |   data Tree : Type where
 75 |     Leaf : Tree
 76 |     Node : Tree -> Tree -> Tree
 77 |
 78 |   tree : Enumerator Tree Tree
 79 |   tree = pure Leaf <|> Node <$> rec <*> rec
 80 |
 81 | ------------------------------------------------------------------------------
 82 | -- Extracting values by running an enumerator
 83 | ------------------------------------------------------------------------------
 84 |
 85 | ||| Assuming that the enumerator is building one layer of term,
 86 | ||| sized e n will produce a list of values of depth n
 87 | export
 88 | sized : Enumerator a a -> Nat -> List a
 89 | sized (MkEnumerator enum) = go where
 90 |
 91 |   go : Nat -> List a
 92 |   go Z = []
 93 |   go (S n) = enum (go n)
 94 |
 95 | ||| Assuming that the enumerator is building one layer of term,
 96 | ||| stream e will produce a list of increasingly deep values
 97 | export
 98 | stream : Enumerator a a -> Stream (List a)
 99 | stream (MkEnumerator enum) = iterate enum []
100 |
101 | ------------------------------------------------------------------------------
102 | -- Defining generic enumerators for regular types
103 | ------------------------------------------------------------------------------
104 |
105 | export
106 | regular : (d : Desc List) -> Enumerator (Fix d) (Fix d)
107 | regular d = MkFix <$> go d where
108 |
109 |   go : (e : Desc List) -> Enumerator (Fix d) (Elem e (Fix d))
110 |   go Zero = empty
111 |   go One = pure ()
112 |   go Id = rec
113 |   go (Const s prop) = const prop
114 |   go (d1 * d2) = pair (go d1) (go d2)
115 |   go (d1 + d2) = Left <$> go d1 <|> Right <$> go d2
116 |
117 | namespace Example
118 |
119 |   ListD : List a -> Desc List
120 |   ListD as = One + (Const a as * Id)
121 |
122 |   lists : (xs : List a) -> Nat -> List (Fix (ListD xs))
123 |   lists xs = sized (regular (ListD xs))
124 |
125 |   encode : {0 xs : List a} -> List a -> Fix (ListD xs)
126 |   encode = foldr (\x, xs => MkFix (Right (x, xs))) (MkFix (Left ()))
127 |
128 |   decode : {xs : List a} -> Fix (ListD xs) -> List a
129 |   decode = fold (either (const []) (uncurry (::)))
130 |
131 |   -- [[], ['a'], ['a', 'a'], ['b'], ['a', 'b'], ['b', 'a'], ['b', 'b']]
132 |   abs : List (List Char)
133 |   abs = decode <$> lists ['a', 'b'] 3
134 |