
  0 | module IO.Async.Loop.SignalST
  1 | 
  2 | import Data.Linear.Ref1
  3 | import Data.Linear.Traverse1
  4 | import Data.SortedMap
  5 | import IO.Async.Loop
  6 | import System.Posix.Signal.Prim
  7 | 
  8 | %default total
  9 | 
 10 | 0 SigMap : Type
 11 | SigMap = SortedMap Signal (List (Nat, Siginfo -> IO1 ())) 
 12 | 
 13 | record SignalST where
 14 |   constructor SST
 15 |   id  : Nat
 16 |   map : SigMap
 17 | 
 18 | 
 19 | await_ : IORef SignalST -> List Signal -> (Siginfo -> IO1 ()) -> IO1 Nat
 20 | await_ r sigs act t = 
 21 |   let SST id m # t := read1 r t
 22 |       _        # t := write1 r (SST (S id) (go id sigs m)) t
 23 |    in id # t
 24 |   where
 25 |     go : Nat -> List Signal -> SigMap -> SigMap
 26 |     go id []     m = m
 27 |     go id (s::ss) m =
 28 |       case lookup s m of
 29 |         Nothing => go id ss $ insert s [(id,act)] m
 30 |         Just ps => go id ss $ insert s ((id,act)::ps) m
 31 | 
 32 | drop_ : List Signal -> Nat -> SignalST -> SignalST
 33 | drop_ []      x st         = st
 34 | drop_ (s::ss) x (SST id m) =
 35 |   case lookup s m of
 36 |     Nothing => drop_ ss x (SST id m)
 37 |     Just vs => case filter ((x /=) . fst) vs of
 38 |       [] => drop_ ss x $ (SST id $ delete s m)
 39 |       ws => drop_ ss x $ (SST id $ insert s ws m)
 40 | 
 41 | dropRef : IORef SignalST -> List Signal -> Nat -> IO1 ()
 42 | dropRef r ss n t = let st # t := read1 r t in write1 r (drop_ ss n st) t
 43 | 
 44 | %inline
 45 | hasHandle : SignalST -> Signal -> Bool
 46 | hasHandle s sig =
 47 |   case lookup sig s.map of
 48 |     Just (_::_) => True
 49 |     _           => False
 50 | 
 51 | --------------------------------------------------------------------------------
 52 | -- API
 53 | --------------------------------------------------------------------------------
 54 | 
 55 | export
 56 | record Sighandler where
 57 |   constructor S
 58 |   ref  : IORef SignalST
 59 | 
 60 | export
 61 | sighandler : IO1 Sighandler
 62 | sighandler t =
 63 |   let st # t := ref1 (SST 0 empty) t
 64 |    in S st # t
 65 | 
 66 | parameters (si : Sighandler)
 67 | 
 68 |   ||| Await a signal and carry out the given action once it is
 69 |   ||| fired.
 70 |   |||
 71 |   ||| This returns an action for cancelling the signal handler
 72 |   export
 73 |   await : List Signal -> (Siginfo -> IO1 ()) -> IO1 (IO1 ())
 74 |   await sigs act t =
 75 |     let ix # t := await_ si.ref sigs act t
 76 |      in dropRef si.ref sigs ix # t
 77 | 
 78 |   ||| Checks for pending signals and runs the corresponding
 79 |   ||| signal handlers (if any).
 80 |   export
 81 |   checkSignals : IO1 ()
 82 |   checkSignals t =
 83 |     let st # t := read1 si.ref t
 84 |      in case null st.map of
 85 |           True  => () # t -- don't do anything if there are no signal handlers
 86 |           False => case toF1 sigpending t of -- check pending signals
 87 |             [] # t => () # t -- no pending signals. abort.
 88 |             ss # t => case filter (hasHandle st) ss of -- check handled signals
 89 |               [] => () # t -- we don't handle any pending signals. abort.
 90 |               ss => case sigwaitinfo {es = [Errno]} ss t of
 91 |                 E _   t => () # t
 92 |                 R inf t => case lookup inf.signal st.map of
 93 |                   Nothing => () # t
 94 |                   Just hs =>
 95 |                     let _ # t := write1 si.ref ({map $= delete inf.signal} st) t
 96 |                      in traverse1_ (\h => snd h inf) hs t 
 97 |