0 | module System.Posix.Signal.Struct
  1 |
  2 | import public Control.Monad.Resource
  3 | import Data.C.Ptr
  4 | import Data.Finite
  5 | import Data.Linear.Traverse1
  6 | import Derive.Prelude
  7 | import System.Posix.Errno
  8 | import System.Posix.File.ReadRes
  9 | import System.Posix.Signal.Types
 10 |
 11 | %default total
 12 | %language ElabReflection
 13 |
 14 | signals : List Signal
 15 | signals =
 16 |   map Signal.Types.S $
 17 |     if SIGRTMAX > 31 then [1..sig SIGRTMAX] else [1..31]
 18 |
 19 | export %inline
 20 | Finite Signal where
 21 |   values = signals
 22 |
 23 | --------------------------------------------------------------------------------
 24 | -- FFI
 25 | --------------------------------------------------------------------------------
 26 |
 27 | %foreign "C:li_emptysigset, posix-idris"
 28 | prim__emptysigset : PrimIO AnyPtr
 29 |
 30 | %foreign "C:li_fullsigset, posix-idris"
 31 | prim__fullsigset : PrimIO AnyPtr
 32 |
 33 | %foreign "C:sigaddset, posix-idris"
 34 | prim__sigaddset : AnyPtr -> Bits32 -> PrimIO ()
 35 |
 36 | %foreign "C:sigdelset, posix-idris"
 37 | prim__sigdelset : AnyPtr -> Bits32 -> PrimIO ()
 38 |
 39 | %foreign "C:sigismember, posix-idris"
 40 | prim__sigismember : AnyPtr -> Bits32 -> PrimIO CInt
 41 |
 42 | export %foreign "C:get_siginfo_t_si_signo, posix-idris"
 43 | get_siginfo_t_si_signo: AnyPtr -> PrimIO Bits32
 44 |
 45 | export %foreign "C:get_siginfo_t_si_code, posix-idris"
 46 | get_siginfo_t_si_code: AnyPtr -> PrimIO CInt
 47 |
 48 | export %foreign "C:get_siginfo_t_si_pid, posix-idris"
 49 | get_siginfo_t_si_pid: AnyPtr -> PrimIO PidT
 50 |
 51 | export %foreign "C:get_siginfo_t_si_uid, posix-idris"
 52 | get_siginfo_t_si_uid: AnyPtr -> PrimIO UidT
 53 |
 54 | export %foreign "C:get_siginfo_t_si_status, posix-idris"
 55 | get_siginfo_t_si_status: AnyPtr -> PrimIO CInt
 56 |
 57 | export %foreign "C:get_siginfo_t_si_value, posix-idris"
 58 | get_siginfo_t_si_value: AnyPtr -> PrimIO CInt
 59 |
 60 | --------------------------------------------------------------------------------
 61 | -- SigsetT
 62 | --------------------------------------------------------------------------------
 63 |
 64 | ||| Wrapper around a pointer of a signal set (`sigset_t`).
 65 | export
 66 | record SigsetT where
 67 |   constructor S
 68 |   ptr : AnyPtr
 69 |
 70 | export %inline
 71 | WrappedPtr SigsetT where
 72 |   wrap   = S
 73 |   unwrap = ptr
 74 |
 75 | export %inline
 76 | freeSigset1 : SigsetT -> F1' World
 77 | freeSigset1 (S p) = ffi $ prim__free p
 78 |
 79 | export %inline
 80 | freeSigset : Lift1 World f => SigsetT -> f ()
 81 | freeSigset p = lift1 (freeSigset1 p)
 82 |
 83 | export %inline
 84 | ELift1 World f => Resource f SigsetT where
 85 |   cleanup = freeSigset
 86 |
 87 | ||| Allocates a `sigset_t` with all signals cleared.
 88 | |||
 89 | ||| This must be freed with `freeSigset`.
 90 | export %inline
 91 | emptySigset : PrimIO SigsetT
 92 | emptySigset = primMap S prim__emptysigset
 93 |
 94 | ||| Allocates a `sigset_t` with all signals set.
 95 | |||
 96 | ||| This must be freed with `freeSigset`.
 97 | export %inline
 98 | fullSigset : PrimIO SigsetT
 99 | fullSigset = primMap S prim__fullsigset
100 |
101 | ||| Adds a signal to a `sigset_t`
102 | export %inline
103 | sigaddset : (r : SigsetT) -> Signal -> F1 World ()
104 | sigaddset (S p) s = ffi $ prim__sigaddset p s.sig
105 |
106 | ||| Removes a signal from a `sigset_t`
107 | export %inline
108 | sigdelset : (r : SigsetT) -> Signal -> F1 World ()
109 | sigdelset (S p) s = ffi $ prim__sigdelset p s.sig
110 |
111 | ||| Tests if a signal is a member of a `sigset_t`.
112 | export %inline
113 | sigismember : (r : SigsetT) -> Signal -> F1 World Bool
114 | sigismember (S p) s t =
115 |   case ffi (prim__sigismember p s.sig) t of
116 |     0 # t => False # t
117 |     _ # t => True # t
118 |
119 | ||| Extracts the set signals from a `SigsetT`.
120 | export %inline
121 | getSignals : (r : SigsetT) -> F1 World (List Signal)
122 | getSignals set = filterM [<] (sigismember set) values
123 |
124 | export
125 | withSignals : List Signal -> (SigsetT -> EPrim a) -> EPrim a
126 | withSignals ss f t =
127 |   let sigs # t := toF1 emptySigset t
128 |       _    # t := traverse1_ (\s => sigaddset sigs s) ss t
129 |       R res  t := f sigs t
130 |         | E x t =>
131 |             let _ # t := freeSigset1 sigs t
132 |              in E x t
133 |       _# t := freeSigset1 sigs t
134 |    in R res t
135 |
136 | export
137 | withoutSignals : List Signal -> (SigsetT -> EPrim a) -> EPrim a
138 | withoutSignals ss f t =
139 |   let sigs # t := toF1 fullSigset t
140 |       _    # t := traverse1_ (\s => sigdelset sigs s) ss t
141 |       R res  t := f sigs t
142 |         | E x t =>
143 |             let _ # t := freeSigset1 sigs t
144 |              in E x t
145 |       _ # t := freeSigset1 sigs t
146 |    in R res t
147 |
148 | --------------------------------------------------------------------------------
149 | -- Siginfo
150 | --------------------------------------------------------------------------------
151 |
152 | export
153 | record SSiginfoT (s : Type) where
154 |   constructor ST
155 |   ptr : AnyPtr
156 |
157 | public export
158 | 0 SiginfoT : Type
159 | SiginfoT = SSiginfoT World
160 |
161 | export %inline
162 | Struct SSiginfoT where
163 |   swrap   = ST
164 |   sunwrap = ptr
165 |
166 | export %inline
167 | SizeOf (SSiginfoT s) where
168 |   sizeof_ = siginfo_t_size
169 |
170 | public export
171 | record Siginfo where
172 |   constructor SI
173 |   signal : Signal
174 |   code   : CInt
175 |   pid    : PidT
176 |   uid    : UidT
177 |   status : CInt
178 |   value  : CInt
179 |
180 | %runElab derive "Siginfo" [Show,Eq]
181 |
182 | export
183 | siginfo : SSiginfoT s -> F1 s Siginfo
184 | siginfo (ST p) t =
185 |   let sig # t := ffi (get_siginfo_t_si_signo p) t
186 |       cod # t := ffi (get_siginfo_t_si_code p) t
187 |       pid # t := ffi (get_siginfo_t_si_pid p) t
188 |       uid # t := ffi (get_siginfo_t_si_uid p) t
189 |       stt # t := ffi (get_siginfo_t_si_status p) t
190 |       val # t := ffi (get_siginfo_t_si_value p) t
191 |    in SI (S sig) cod pid uid stt val # t
192 |
193 | export %inline %hint
194 | convertSiginfo : Convert Siginfo
195 | convertSiginfo = convStruct SSiginfoT siginfo
196 |