
  0 | module Control.Cont.IO
  1 | 
  2 | import Control.HigherOrder
  3 | 
  4 | import Control.Monad.Free
  5 | 
  6 | public export
  7 | data HIO : (Type -> Type) -> (Type -> Type) where
  8 |   MkHIO : forall t. IO t -> (t -> m a) -> HIO m a
  9 | 
 10 | public export
 11 | HFunctor HIO where
 12 |   hmap f (MkHIO x k) = MkHIO x (f . k)
 13 | 
 14 | public export
 15 | Syntax HIO where
 16 |   emap f (MkHIO x k) = MkHIO x (f . k)
 17 | 
 18 |   weave f hdl (MkHIO x k) =
 19 |     MkHIO (map (\x => map (const x) f) x)
 20 |             (hdl . map k)
 21 | 
 22 | public export
 23 | runIO : Free HIO a -> IO a
 24 | runIO (Return x) = pure x
 25 | runIO (Op (MkHIO x k)) = x `io_bind` runIO . k
 26 | 
 27 | public export
 28 | io : Syntax sig => Inj HIO sig => IO a -> Free sig a
 29 | io x = inject {sub = HIO} (MkHIO x Return)
 30 |