
  0 | module Evince.Synchronized
  1 | 
  2 | %default total
  3 | 
  4 | ||| A lock: a function that runs an action while holding mutual exclusion, for
  5 | ||| any result type. `Synchronized.newLock` allocates one.
  6 | public export
  7 | record Lock (m : Type -> Type) where
  8 |   constructor MkLock
  9 |   withLock : {0 a : Type} -> m a -> m a
 10 | 
 11 | ||| A monad whose actions can run under mutual exclusion. Sequential `IO` runs
 12 | ||| can't race, so its lock is a no-op; a concurrent driver provides a real lock.
 13 | public export
 14 | interface Synchronized (m : Type -> Type) where
 15 |   newLock : IO (Lock m)
 16 | 
 17 | public export
 18 | Synchronized IO where
 19 |   newLock = pure (MkLock id)
 20 |