Threads.idr

module Threads

import Control.ST
import System.Concurrency.Channels
import System

public export
interface Conc (m : Type -> Type) where
  -- 'Fork' sends some resources to the spawned thread, and keeps the rest
  -- for the parent
  -- TODO: Note that there is nothing here yet about how the threads
  -- communicate with each other...
  fork : (thread : STrans m () thread_res (const [])) ->
         {auto tprf : SubRes thread_res all} ->
         STrans m () all (const (kept tprf)) 

export
implementation Conc IO where
  fork thread
      = do threadEnv <- dropSub
           lift $ spawn (do runWith threadEnv thread
                            pure ()) 
           pure ()