
  0 | module Control.Cont.Out
  1 | 
  2 | import Control.HigherOrder
  3 | 
  4 | import Control.Monad.Free
  5 | 
  6 | public export
  7 | data Out cnt = MkOut String cnt
  8 | 
  9 | public export
 10 | Functor Out where
 11 |   map f (MkOut x y) = MkOut x (f y)
 12 | 
 13 | public export
 14 | HOut : (Type -> Type) -> (Type -> Type)
 15 | HOut = Lift Out
 16 | 
 17 | public export
 18 | runOut : Free HOut a -> IO a
 19 | runOut (Return x) = pure x
 20 | runOut (Op (MkLift (MkOut s p))) =
 21 |   putStrLn s `io_bind` \_ => runOut p
 22 | 
 23 | public export
 24 | out : Inj HOut sig => String -> Free sig ()
 25 | out x = inject {sub = HOut} $ MkLift $ MkOut x (return ())
 26 | 
 27 |