
  0 | module IO.Async.Token
  1 | 
  2 | import IO.Async.MVar
  3 | import Derive.Prelude
  4 | 
  5 | %default total
  6 | %language ElabReflection
  7 | 
  8 | ||| A unique identifier for fibers.
  9 | export
 10 | record Token where
 11 |   constructor T
 12 |   value : Nat
 13 | 
 14 | %runElab derive "Token" [Show,Eq,Ord]
 15 | 
 16 | ||| A generator for unique tokens.
 17 | export
 18 | record TokenGen where
 19 |   [noHints]
 20 |   constructor TG
 21 |   var : MVar Nat
 22 | 
 23 | export
 24 | newTokenGen : IO TokenGen
 25 | newTokenGen = TG <$> newMVar 0
 26 | 
 27 | ||| Generates a new unique fiber token.
 28 | export
 29 | token : HasIO io => (g : TokenGen) => io Token
 30 | token = liftIO $ evalState g.var (\x => (S x, T x))
 31 |