
  0 | module Data.Iterable
  1 | 
  2 | import Data.List1
  3 | import Data.SnocList
  4 | 
  5 | import public Control.MonadRec
  6 | 
  7 | --------------------------------------------------------------------------------
  8 | --          Iterable
  9 | --------------------------------------------------------------------------------
 10 | 
 11 | refl : {k : Nat} -> LTE k k
 12 | refl = reflexive {x = k}
 13 | 
 14 | public export
 15 | interface Iterable container element | container where
 16 |   iterM :
 17 |        {auto rec : MonadRec m}
 18 |     -> (accum : element -> st -> m st)
 19 |     -> (done  : st -> res)
 20 |     -> (ini   : st)
 21 |     -> (seed  : container)
 22 |     -> m res
 23 | 
 24 | export
 25 | forM_ :
 26 |      {auto _ : Iterable container element}
 27 |   -> {auto _ : MonadRec m}
 28 |   -> (run  : element -> m ())
 29 |   -> (seed : container)
 30 |   -> m ()
 31 | forM_ run = iterM (\e,_ => run e) (const ()) ()
 32 | 
 33 | export
 34 | foldM :
 35 |      {auto _ : Iterable container element}
 36 |   -> {auto _ : MonadRec m}
 37 |   -> {auto _ : Monoid mo}
 38 |   -> (calc : element -> m mo)
 39 |   -> (seed : container)
 40 |   -> m mo
 41 | foldM calc = iterM (\e,acc => (<+> acc) <$> calc e) id neutral
 42 | 
 43 | --------------------------------------------------------------------------------
 44 | --          Iterable Implementations
 45 | --------------------------------------------------------------------------------
 46 | 
 47 | export
 48 | Iterable Nat Nat where
 49 |   iterM accum done ini seed =
 50 |     trSized seed ini $
 51 |       \case Z       => pure . Done . done
 52 |             v@(S k) => map (Cont k refl) . accum v
 53 | 
 54 | export
 55 | Iterable (List a) a where
 56 |   iterM accum done ini seed =
 57 |     trSized seed ini $
 58 |       \case Nil    => pure . Done . done
 59 |             h :: t => map (Cont t refl) . accum h
 60 | 
 61 | export
 62 | Iterable (List1 a) a where
 63 |   iterM accum done ini = iterM accum done ini . forget
 64 | 
 65 | export
 66 | Iterable Fuel () where
 67 |   iterM accum done ini seed =
 68 |     trSized seed ini $
 69 |       \case Dry    => pure . Done . done
 70 |             More f => map (Cont f refl) . accum ()
 71 | 
 72 | export
 73 | Iterable (SnocList a) a where
 74 |   iterM accum done ini seed =
 75 |     trSized seed ini $
 76 |       \case [<]     => pure . Done . done
 77 |             sx :< x => map (Cont sx refl) . accum x
 78 |