
   0 | module Data.MSF.Running
   1 | 
   2 | import Control.Monad.Identity
   3 | import Data.Contravariant
   4 | import Data.IORef
   5 | import Data.MSF.Core
   6 | 
   7 | %default total
   8 | 
   9 | --------------------------------------------------------------------------------
  10 | --          Single step evaluation
  11 | --------------------------------------------------------------------------------
  12 | 
  13 | ||| Single step evaluation of monadic stream functions.
  14 | ||| This is used to drive a typical application using
  15 | ||| MSFs for processing input.
  16 | export
  17 | step : Monad m => MSF m i o -> i -> m (o, MSF m i o)
  18 | 
  19 | par : Monad m => ParList m is os -> HList is -> m (HList os, ParList m is os)
  20 | par []          []          = pure ([],[])
  21 | par (sf :: sfs) (vi :: vis) = do
  22 |   (vo, sf2)   <- step    sf  vi
  23 |   (vos, sfs2) <- par sfs vis
  24 |   pure (vo :: vos, sf2 :: sfs2)
  25 | 
  26 | fan : Monad m => FanList m i os -> i -> m (HList os, FanList m i os)
  27 | fan []          _  = pure ([],[])
  28 | fan (sf :: sfs) vi = do
  29 |   (vo, sf2)   <- step    sf  vi
  30 |   (vos, sfs2) <- fan sfs vi
  31 |   pure (vo :: vos, sf2 :: sfs2)
  32 | 
  33 | choice : Monad m => ParList m is os -> HSum is -> m (HSum os, ParList m is os)
  34 | choice (sf :: sfs) (Here vi) = do
  35 |   (vo, sf2) <- step sf vi
  36 |   pure (Here vo, sf2 :: sfs)
  37 | 
  38 | choice (sf :: sfs) (There y) = do
  39 |   (vo, sfs2) <- choice sfs y
  40 |   pure (There vo, sf :: sfs2)
  41 | 
  42 | collect : Monad m => CollectList m is o -> HSum is -> m (o, CollectList m is o)
  43 | collect (sf :: sfs) (Here vi) = do
  44 |   (vo, sf2) <- step sf vi
  45 |   pure (vo, sf2 :: sfs)
  46 | 
  47 | collect (sf :: sfs) (There y) = do
  48 |   (vo, sfs2) <- collect sfs y
  49 |   pure (vo, sf :: sfs2)
  50 | 
  51 | step c@(Const x)  _ = pure (x, c)
  52 | step Id           v = pure (v, Id)
  53 | step c@(Arr f)    v = pure (f v, c)
  54 | step c@(Lifted f) v = (,c) <$> f v
  55 | 
  56 | step (Seq sf1 sf2) v = do
  57 |   (vx,sf1') <- step sf1 v
  58 |   (vo,sf2') <- step sf2 vx
  59 |   pure (vo, Seq sf1' sf2')
  60 | 
  61 | step (Par sfs) v = mapSnd Par <$> par sfs v
  62 | 
  63 | step (Fan sfs) v = mapSnd Fan <$> fan sfs v
  64 | 
  65 | step (Choice sfs) v = mapSnd Choice <$> choice sfs v
  66 | 
  67 | step (Collect sfs) v = mapSnd Collect <$> collect sfs v
  68 | 
  69 | step (Loop s sf) v = do
  70 |   ([s2,o], sf2) <- step sf [s,v]
  71 |   pure (o, Loop s2 sf2)
  72 | 
  73 | step (Switch sf f) i = do
  74 |   (Left e,_) <- step sf i
  75 |     | (Right o,sf2) => pure (o, Switch sf2 f)
  76 |   step (f e) i
  77 | 
  78 | --------------------------------------------------------------------------------
  79 | --          Testing MSFs
  80 | --------------------------------------------------------------------------------
  81 | 
  82 | ||| Uses the given MSF to process a list of input
  83 | ||| values. This is useful for testing MSFs.
  84 | export
  85 | embed : Monad m => List i -> MSF m i o -> m (List o)
  86 | embed [] _          = pure []
  87 | embed (vi :: is) sf = do
  88 |   (vo,sf2) <- step sf vi
  89 |   os       <- embed is sf2
  90 |   pure $ vo :: os
  91 | 
  92 | ||| `embed` using the `Identity` monad.
  93 | export
  94 | embedI : List i -> MSF Identity i o -> List o
  95 | embedI is = runIdentity . embed is
  96 | 
  97 | ||| Calculates the size (number of constructors)
  98 | ||| of a MSF. This is useful for testing and
  99 | ||| possibly optimizing applications.
 100 | export
 101 | size : MSF m i o -> Nat
 102 | 
 103 | sizePar : ParList m is os -> Nat
 104 | sizePar [] = 0
 105 | sizePar (sf :: sfs) = size sf + sizePar sfs
 106 | 
 107 | sizeFan : FanList m i os -> Nat
 108 | sizeFan [] = 0
 109 | sizeFan (sf :: sfs) = size sf + sizeFan sfs
 110 | 
 111 | sizeCol : CollectList m is o -> Nat
 112 | sizeCol [] = 0
 113 | sizeCol (sf :: sfs) = size sf + sizeCol sfs
 114 | 
 115 | size Id            = 1
 116 | size (Const x)     = 1
 117 | size (Arr f)       = 1
 118 | size (Lifted f)    = 1
 119 | size (Seq x y)     = 1 + size x + size y
 120 | size (Par x)       = 1 + sizePar x
 121 | size (Fan x)       = 1 + sizeFan x
 122 | size (Choice x)    = 1 + sizePar x
 123 | size (Collect x)   = 1 + sizeCol x
 124 | size (Loop x y)    = 1 + size y
 125 | size (Switch x f)  = 1 + size x
 126 | 
 127 | --------------------------------------------------------------------------------
 128 | --          Handler
 129 | --------------------------------------------------------------------------------
 130 | 
 131 | ||| An event handler typically used as an auto-implicit argument
 132 | public export
 133 | record Handler (m : Type -> Type) (e : Type) where
 134 |   [noHints]
 135 |   constructor H
 136 |   handle_ : e -> m ()
 137 | 
 138 | public export
 139 | Contravariant (Handler m) where
 140 |   contramap f (H g) = H $ g . f
 141 | 
 142 | export %inline
 143 | handle : {auto h : Handler m e} -> e -> m ()
 144 | handle = h.handle_
 145 | 
 146 | --------------------------------------------------------------------------------
 147 | --          Running MSFs
 148 | --------------------------------------------------------------------------------
 149 | 
 150 | -- initialEvent: If `Just e`, evaluate the given `MSF` once with `e` to
 151 | -- properly initialize all components.
 152 | -- idPrefix: prefix for uniqe ids
 153 | reactimate_ :
 154 |      {auto _ : HasIO m}
 155 |   -> (initialEvent : Maybe e)
 156 |   -> (mkMSF        : Handler m e -> m (MSF m e (), m ()))
 157 |   -> m (m ())
 158 | reactimate_ ie mkMSF = do
 159 |   -- Here we will put the proper event handler once everyting
 160 |   -- is ready. This is not Haskell, so we can't define
 161 |   -- the handler lazily and satisfy the totality checker at
 162 |   -- the same time. We therefore initialize the mutable reference
 163 |   -- with a dummy.
 164 |   hRef    <- newIORef {a = e -> m ()} (const $ pure ())
 165 | 
 166 |   -- our event handler
 167 |   let h := H (\ve => readIORef hRef >>= \h => h ve)
 168 | 
 169 |   (sf,cl) <- mkMSF h
 170 | 
 171 |   -- the current application state consists of the current
 172 |   -- monadic stream function, which will be stored in a
 173 |   -- mutable ref
 174 |   sfRef   <- newIORef sf
 175 | 
 176 |   -- we can now implement the *real* event handler:
 177 |   -- when an event is being fired, we evaluate the current
 178 |   -- MSF and put the resulting continuation in the mutable ref
 179 |   -- to be used when the next event occurs.
 180 |   let realHandler : e -> m ()
 181 |       realHandler = \ev => do
 182 |         sf1      <- readIORef sfRef
 183 |         (_, sf2) <- step sf1 ev
 184 |         writeIORef sfRef sf2
 185 | 
 186 |   -- we need to register the correct event handler, otherwise
 187 |   -- nothing will run
 188 |   writeIORef hRef realHandler
 189 | 
 190 |   -- finally, fire the initial event (if any)
 191 |   traverse_ h.handle_ ie
 192 | 
 193 |   pure cl
 194 | 
 195 | ||| Create a monadic stream function (the reactive behavior
 196 | ||| of an UI, for instance)
 197 | ||| by passing the given generation function `sf` an event handler
 198 | ||| that can be registered at reactive components.
 199 | ||| The MSF will then be invoked and
 200 | ||| evaluated whenever an event is fired.
 201 | export %inline
 202 | reactimate : HasIO m => (Handler m e -> m (MSF m e (), m ())) -> m (m ())
 203 | reactimate = reactimate_ Nothing
 204 | 
 205 | ||| Like `reactimate`, but evaluates the `MSF` once at the beginning by
 206 | ||| passing it the given initial event.
 207 | export
 208 | reactimateIni : HasIO m => e -> (Handler m e -> m (MSF m e (), m ())) -> m (m ())
 209 | reactimateIni = reactimate_ . Just
 210 |