
  0 | module Control.Monad.Coop.Sync
  1 | 
  2 | import Data.SortedMap
  3 | 
  4 | %default total
  5 | 
  6 | --- Stuff for runtime syncronisation between discrete events ---
  7 | 
  8 | export
  9 | record Sync (0 t : k) where
 10 |   constructor Sy
 11 |   unSy : Nat
 12 | 
 13 | export %inline
 14 | Eq (Sync sk) where
 15 |   (==) = (==) `on` unSy
 16 | 
 17 | export %inline
 18 | Ord (Sync sk) where
 19 |   compare = compare `on` unSy
 20 | 
 21 | export
 22 | newUniqueSync : SortedMap (Sync sk) whatever -> Sync sk
 23 | newUniqueSync syncs = Sy $ case unSy . fst <$> leftMost syncs of
 24 |   Nothing    => Z
 25 |   Just (S x) => x                                              -- either minimal minus 1
 26 |   Just Z     => maybe Z (S . unSy . fst) $ rightMost syncs     -- or maximal plus 1
 27 |