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.Indexed
  6 |
  7 | import Data.List
  8 | import Data.Description.Regular
  9 | import Data.Description.Indexed
 10 |
 11 | import Data.Enumerate.Common
 12 |
 13 | %default total
 14 |
 15 | ------------------------------------------------------------------------------
 16 | -- Definition of indexed 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 IEnumerator {i : Type} (a : i -> Type) (b : Type) where
 23 |   constructor MkIEnumerator
 24 |   runIEnumerator : ((v : i) -> List (a v)) -> List b
 25 |
 26 | ------------------------------------------------------------------------------
 27 | -- Combinators to build enumerators
 28 | ------------------------------------------------------------------------------
 29 |
 30 | export
 31 | Functor (IEnumerator a) where
 32 |   map f (MkIEnumerator enum) = MkIEnumerator (map f . enum)
 33 |
 34 | export
 35 | Applicative (IEnumerator a) where
 36 |   pure = MkIEnumerator . const . pure
 37 |   MkIEnumerator e1 <*> MkIEnumerator e2
 38 |     = MkIEnumerator (\ as => prodWith ($) (e1 as) (e2 as))
 39 |
 40 | export
 41 | Alternative (IEnumerator a) where
 42 |   empty = MkIEnumerator (const [])
 43 |   MkIEnumerator e1 <|> MkIEnumerator e2
 44 |     = MkIEnumerator (\ as => interleave (e1 as) (e2 as))
 45 |
 46 | export
 47 | Monad (IEnumerator a) where
 48 |   xs >>= ks = MkIEnumerator $ \ as =>
 49 |     foldr (\ x => interleave (runIEnumerator (ks x) as)) []
 50 |       (runIEnumerator xs as)
 51 |
 52 | export
 53 | rec : (v : i) -> IEnumerator a (a v)
 54 | rec v = MkIEnumerator ($ v)
 55 |
 56 | export
 57 | pairWith : (b -> c -> d) -> IEnumerator a b -> IEnumerator a c -> IEnumerator a d
 58 | pairWith f (MkIEnumerator e1) (MkIEnumerator e2)
 59 |   = MkIEnumerator (\ as => prodWith f (e1 as) (e2 as))
 60 |
 61 | export
 62 | pair : IEnumerator a b -> IEnumerator a c -> IEnumerator a (b, c)
 63 | pair = pairWith (,)
 64 |
 65 | export
 66 | sig : {b : a -> Type} ->
 67 |       IEnumerator f a -> ((x : a) -> IEnumerator f (b x)) ->
 68 |       IEnumerator f (x : a ** b x)
 69 | sig as bs = as >>= \ a => bs a >>= \ b => pure (a ** b)
 70 |
 71 | export
 72 | const : List b -> IEnumerator a b
 73 | const bs = MkIEnumerator (const bs)
 74 |
 75 | ------------------------------------------------------------------------------
 76 | -- Extracting values by running an enumerator
 77 | ------------------------------------------------------------------------------
 78 |
 79 | export
 80 | isized : ((v : i) -> IEnumerator a (a v)) -> Nat -> (v : i) -> List (a v)
 81 | isized f 0 v = []
 82 | isized f (S n) v = runIEnumerator (f v) (isized f n)
 83 |
 84 | ------------------------------------------------------------------------------
 85 | -- Defining  generic enumerators for indexed datatypes
 86 | ------------------------------------------------------------------------------
 87 |
 88 | export
 89 | indexed : (d : i -> IDesc List i) -> (v : i) -> IEnumerator (Fix d) (Fix d v)
 90 | indexed d v = MkFix <$> go (d v) where
 91 |
 92 |   go : (e : IDesc List i) -> IEnumerator (Fix d) (Elem e (Fix d))
 93 |   go Zero = empty
 94 |   go One = pure ()
 95 |   go (Id v) = rec v
 96 |   go (d1 * d2) = pair (go d1) (go d2)
 97 |   go (d1 + d2) = Left <$> go d1 <|> Right <$> go d2
 98 |   go (Sig s vs f) = sig (const vs) (\ x => go (f x))
 99 |
100 | export
101 | 0 Memorator : (d : Desc p) -> (Fix d -> Type) -> Type -> Type
102 | Memorator d a b = (d ~> (List . a)) -> List b
103 |
104 | export
105 | memorate : {d : Desc p} ->
106 |            {0 b : Fix d -> Type} ->
107 |            ((x : Fix d) -> Memorator d b (b x)) ->
108 |            Nat -> (x : Fix d) -> List (b x)
109 | memorate f 0 x = []
110 | memorate f (S n) x = f x (trie $ memorate f n)
111 |