
   0 | module IO.Async.Loop.TimerST
   1 | 
   2 | import Data.SortedMap
   3 | import Data.Linear.Ref1
   4 | import Data.Linear.Traverse1
   5 | import IO.Async.Loop
   6 | import System.Clock
   7 | 
   8 | %default total
   9 | 
  10 | --------------------------------------------------------------------------------
  11 | -- Timer State
  12 | --------------------------------------------------------------------------------
  13 | 
  14 | record TimerST where
  15 |   constructor TST
  16 |   id  : Nat
  17 |   map : SortedMap Integer (List (Nat, IO1 ()))
  18 | 
  19 | schedule_ : Integer -> IO1 () -> TimerST -> TimerST
  20 | schedule_ ns act (TST id m) =
  21 |   case lookup ns m of
  22 |     Nothing => TST (S id) $ insert ns [(id,act)] m
  23 |     Just ps => TST (S id) $ insert ns ((id,act)::ps) m
  24 | 
  25 | drop_ : Integer -> Nat -> TimerST -> TimerST
  26 | drop_ ns x (TST id m) =
  27 |   case lookup ns m of
  28 |     Nothing => TST id m
  29 |     Just vs => case filter ((x /=) . fst) vs of
  30 |       [] => TST id $ delete ns m
  31 |       ws => TST id $ insert ns ws m
  32 | 
  33 | %inline
  34 | nanos : IO1 Integer
  35 | nanos t =
  36 |   let now # t := ioToF1 (clockTime Monotonic) t
  37 |    in toNano now # t
  38 | 
  39 | nextDue : Integer -> IORef TimerST -> IO1 (Either Integer (List (Nat,IO1 ())))
  40 | nextDue ns r t =
  41 |   let (TST id m) # t := read1 r t
  42 |    in case leftMost m of
  43 |         Nothing       => Left 0 # t
  44 |         Just (due,ps) => case ns >= due of
  45 |           True  =>
  46 |            let _ # t := write1 r (TST id $ delete due m) t
  47 |             in Right ps # t
  48 |           False => Left (due - ns) # t
  49 | 
  50 | --------------------------------------------------------------------------------
  51 | -- API
  52 | --------------------------------------------------------------------------------
  53 | 
  54 | export
  55 | record Timer where
  56 |   constructor T
  57 |   ref : IORef TimerST
  58 | 
  59 | export
  60 | timer : IO1 Timer
  61 | timer t = let st # t := ref1 (TST 0 empty) t in T st # t
  62 | 
  63 | parameters (ti : Timer)
  64 | 
  65 |   ||| Schedule an action at the given timer
  66 |   |||
  67 |   ||| This returns an action for cancelling the timer
  68 |   export
  69 |   schedule : Clock Duration -> IO1 () -> IO1 (IO1 ())
  70 |   schedule dur act t =
  71 |     let ns  # t := nanos t
  72 |         end     := ns + toNano dur
  73 |      in case end <= ns of
  74 |           True  => let _ # t := act t in unit1 # t
  75 |           False =>
  76 |             let tst # t := read1 ti.ref t
  77 |                 _   # t := write1 ti.ref (schedule_ end act tst) t
  78 |              in mod1 ti.ref (drop_ end tst.id) # t
  79 | 
  80 |   export
  81 |   runDue : Integer -> IO1 Integer
  82 |   runDue now t =
  83 |     case nextDue now ti.ref t of
  84 |       Right ps # t =>
  85 |        let _ # t := traverse1_ snd ps t
  86 |         in runDue (assert_smaller now now) t
  87 |       Left rem # t => rem # t
  88 | 
  89 |   ||| Runs all scheduled timers whose duration has exceeded
  90 |   export
  91 |   runDueTimers : IO1 Integer
  92 |   runDueTimers t =
  93 |     let st # t := read1 ti.ref t
  94 |      in case leftMost st.map of
  95 |           Nothing      => 0 # t
  96 |           Just (ns,ps) =>
  97 |             let now # t := nanos t
  98 |              in case now >= ns of
  99 |                   False => (ns - now) # t
 100 |                   True  => runDue now t
 101 |