
  0 | module Control.Cont.Thread
  1 | 
  2 | import Data.List
  3 | 
  4 | import Control.HigherOrder
  5 | 
  6 | import Control.Monad.Free
  7 | 
  8 | public export
  9 | data Thread : (Type -> Type) -> (Type -> Type) where
 10 |   Yield : m a -> Thread m a
 11 |   Fork : forall t. m t -> m a -> Thread m a
 12 | 
 13 | public export
 14 | HThread : (Type -> Type) -> (Type -> Type)
 15 | HThread = Thread
 16 | 
 17 | public export
 18 | yield : Inj Thread sig => Free sig ()
 19 | yield = inject $ Yield $ return ()
 20 | 
 21 | public export
 22 | fork : Inj Thread sig => Free sig a -> Free sig ()
 23 | fork d = inject $ Fork d $ return ()
 24 | 
 25 | public export
 26 | HFunctor Thread where
 27 |   hmap f (Yield x) = Yield (f x)
 28 |   hmap f (Fork x y) = Fork (f x) (f y)
 29 | 
 30 | public export
 31 | Syntax Thread where
 32 |   emap f (Yield p) = Yield (f p)
 33 |   emap f (Fork d p) = Fork d (f p)
 34 | 
 35 |   weave s hdl (Yield p) = Yield (hdl (map (const p) s))
 36 |   weave s hdl (Fork d p) = Fork (hdl (map (const d) s))
 37 |                                 (hdl (map (const p) s))
 38 | 
 39 | public export
 40 | data Daemon : ((Type -> Type) -> (Type -> Type)) -> Type where
 41 |   MkDaemon : forall t. Free (Thread :+: sig) t -> Daemon sig
 42 | 
 43 | public export
 44 | data SThread : (f : (Type -> Type) -> (Type -> Type))
 45 |             -> Type
 46 |             -> Type where
 47 |   SYield : Free (Thread :+: sig) r -> SThread sig r
 48 |   SFork : Daemon sig -> Free (Thread :+: sig) r -> SThread sig r
 49 |   SActive : r -> SThread sig r
 50 | 
 51 | public export
 52 | Syntax sig => Functor (SThread sig) where
 53 |   map f (SActive x) = SActive (f x)
 54 |   map f (SYield p) = SYield (map f p)
 55 |   map f (SFork d p) = SFork d (map f p)
 56 | 
 57 | mutual
 58 |   public export
 59 |   thread : Syntax sig
 60 |         => Handler (SThread sig) (Free (Thread :+: sig)) (Free sig)
 61 |   thread (SActive p) = runThread p
 62 |   thread (SYield p) = return (SYield (join p))
 63 |   thread (SFork d p) = return (SFork d (join p))
 64 | 
 65 |   public export
 66 |   runThread : Syntax sig
 67 |            => Free (Thread :+: sig) a -> Free sig (SThread sig a)
 68 |   runThread (Return x) = return (SActive x)
 69 |   runThread (Op (Inl (Yield q))) = return (SYield q)
 70 |   runThread (Op (Inl (Fork d q))) = return (SFork (MkDaemon d) q)
 71 |   runThread (Op (Inr op)) = Op (weave {s = SThread sig} (SActive ()) thread op)
 72 | 
 73 | public export
 74 | schedule : Syntax sig => Free (Thread :+: sig) a -> Free sig a
 75 | schedule p = master p [] where
 76 |   mutual
 77 |     daemons : List (Daemon sig) -> List (Daemon sig) -> Free (Thread :+: sig) a -> Free sig a
 78 |     daemons [] ds' p = master p (reverse ds')
 79 |     daemons (MkDaemon q :: ds) ds' p = do
 80 |       r <- runThread q
 81 |       case r of
 82 |         SActive _ => daemons ds ds' p
 83 |         SYield q' => daemons ds (MkDaemon q' :: ds') p
 84 |         SFork d' q' => daemons (d' :: ds) (MkDaemon q' :: ds') p
 85 | 
 86 |     master : Free (Thread :+: sig) a -> List (Daemon sig) -> Free sig a
 87 |     master p ds = do
 88 |       r <- runThread p
 89 |       case r of
 90 |         SActive x => return x
 91 |         SYield p => daemons ds [] p
 92 |         SFork d p => daemons (d :: ds) [] p
 93 |