0 | module System.Posix.Errno
  1 |
  2 | import Data.C.Integer
  3 | import Data.C.Ptr
  4 | import Data.Finite
  5 | import Data.Maybe
  6 | import Data.SortedMap
  7 | import public System.Posix.Errno.Type
  8 | import public Data.Linear.ELift1
  9 |
 10 | --------------------------------------------------------------------------------
 11 | -- Interface
 12 | --------------------------------------------------------------------------------
 13 |
 14 | ||| Prints the error text and name of a system error.
 15 | export %inline
 16 | Interpolation Errno where
 17 |   interpolate x = "\{errorText x} (\{errorName x})"
 18 |
 19 | public export
 20 | 0 EPrim : Type -> Type
 21 | EPrim a = {0 es : List Type} -> Has Errno es => E1 World es a
 22 |
 23 | --------------------------------------------------------------------------------
 24 | -- Utilities
 25 | --------------------------------------------------------------------------------
 26 |
 27 | ||| Converts 0 to `False`, everything else to `True`
 28 | public export %inline
 29 | toBool : Bits8 -> Bool
 30 | toBool 0 = False
 31 | toBool _ = True
 32 |
 33 | ||| Converts a negative number to a system error.
 34 | export %inline
 35 | fromNeg : Neg n => Cast n Bits32 => n -> Errno
 36 | fromNeg = EN . cast . negate
 37 |
 38 | export %inline
 39 | primMap : (a -> b) -> PrimIO a -> PrimIO b
 40 | primMap f act w =
 41 |   let MkIORes v w := act w
 42 |    in MkIORes (f v) w
 43 |
 44 | export %inline
 45 | elinMap : (a -> b) -> E1 s es a -> E1 s es b
 46 | elinMap f act w =
 47 |   let R v w := act w | E x w => E x w
 48 |    in R (f v) w
 49 |
 50 | export %inline
 51 | toVal : (CInt -> a) -> PrimIO CInt -> EPrim a
 52 | toVal f act t =
 53 |   let r # t := toF1 act t
 54 |    in if r < 0 then E (inject $ fromNeg r) t else R (f r) t
 55 |
 56 | export %inline
 57 | toSize : PrimIO SsizeT -> EPrim Bits32
 58 | toSize act t =
 59 |   let r # t := toF1 act t
 60 |    in if r < 0 then E (inject $ fromNeg r) t else R (cast r) t
 61 |
 62 | export %inline
 63 | toUnit : PrimIO CInt -> EPrim ()
 64 | toUnit act t =
 65 |   let r # t := toF1 act t
 66 |    in if r < 0 then E (inject $ fromNeg r) t else R () t
 67 |
 68 | export %inline
 69 | toPidT : PrimIO PidT -> EPrim PidT
 70 | toPidT act t =
 71 |   let r # t := toF1 act t
 72 |    in if r < 0 then E (inject $ fromNeg r) t else R r t
 73 |
 74 | export %inline
 75 | posToUnit : PrimIO Bits32 -> EPrim ()
 76 | posToUnit act t =
 77 |   case toF1 act t of
 78 |     0 # t => R () t
 79 |     x # t => E (inject $ EN x) t
 80 |
 81 | export %inline
 82 | posNotErr : Errno -> PrimIO Bits32 -> EPrim Bool
 83 | posNotErr err act t =
 84 |   case toF1 act t of
 85 |     0 # t => R True t
 86 |     x # t => case EN x == err of
 87 |       True  => R False t
 88 |       False => E (inject $ EN x) t
 89 |
 90 | export %inline
 91 | toRes : PrimIO a -> PrimIO CInt -> EPrim a
 92 | toRes wrap act t =
 93 |   let R _ t := toUnit act t | E x t => E x t
 94 |       r # t := toF1 wrap t
 95 |    in R r t
 96 |
 97 | export %inline
 98 | ignore : E1 World es a -> PrimIO ()
 99 | ignore act =
100 |   primRun $ \t => case act t of
101 |     R _ t => () # t
102 |     E _ t => () # t
103 |
104 | --------------------------------------------------------------------------------
105 | -- General PrimIO Utilities
106 | --------------------------------------------------------------------------------
107 |
108 | export %inline
109 | freeFail : Struct f => f World -> Errno -> EPrim b
110 | freeFail s err t =
111 |   let _ # t := freeStruct1 s t
112 |    in E (inject err) t
113 |
114 | export %inline
115 | finally : PrimIO () -> EPrim a -> EPrim a
116 | finally cleanup act t =
117 |   case act t of
118 |     R r t => let _ # t := toF1 cleanup t in R r t
119 |     E x t => let _ # t := toF1 cleanup t in E x t
120 |
121 | export %inline
122 | primStruct : (0 f : _) -> Struct f => SizeOf (f World) => F1 World (f World)
123 | primStruct f = allocStruct1 f
124 |
125 | export %inline
126 | withStruct : (0 f : _) -> Struct f => SizeOf (f World) => (f World -> EPrim b) -> EPrim b
127 | withStruct a f t =
128 |   let str # t := primStruct a t
129 |    in finally (prim__free (sunwrap str)) (f str) t
130 |
131 | export %inline
132 | withBox : (0 a : Type) -> SizeOf a => Deref a => (IOBox a -> EPrim b) -> EPrim b
133 | withBox a f t =
134 |   let box # t := ioToF1 (malloc a 1) t
135 |    in finally (toPrim $ free box) (f box) t
136 |
137 | export %inline
138 | withPtr :  Bits32 -> (AnyPtr -> EPrim b) -> EPrim b
139 | withPtr sz f t =
140 |   let ptr         := prim__malloc sz
141 |    in finally (prim__free ptr) (f ptr) t
142 |
143 | export %inline
144 | withCArray :
145 |      (0 a : Type)
146 |   -> {auto sz : SizeOf a}
147 |   -> (n   : Nat)
148 |   -> (CArrayIO n a -> EPrim b)
149 |   -> EPrim b
150 | withCArray a n f t =
151 |   let arr # t := malloc1 a n t
152 |    in finally (prim__free (unsafeUnwrap arr)) (f arr) t
153 |
154 | export
155 | primTraverse_ : (a -> PrimIO ()) -> List a -> PrimIO ()
156 | primTraverse_ f []        w = MkIORes () w
157 | primTraverse_ f (x :: xs) w =
158 |   let MkIORes _ w := f x w
159 |    in primTraverse_ f xs w
160 |
161 | export
162 | filterM : SnocList a -> (a -> F1 rs Bool) -> List a -> F1 rs (List a)
163 | filterM sa f []      t = (sa <>> []) # t
164 | filterM sa f (v::vs) t =
165 |   let True # t := f v t | _ # t => filterM sa f vs t
166 |    in filterM (sa :< v) f vs t
167 |
168 | export
169 | values :
170 |      {auto der : Deref b}
171 |   -> {auto sof : SizeOf b}
172 |   -> List c
173 |   -> CArray s n b
174 |   -> (b -> F1 s c)
175 |   -> (k : Nat)
176 |   -> {auto 0 prf : LTE k n}
177 |   -> F1 s (List c)
178 | values cs arr f 0     t = cs # t
179 | values cs arr f (S k) t =
180 |   let vb # t := getNat arr k t
181 |       vc # t := f vb t
182 |    in values (vc::cs) arr f k t
183 |
184 | export
185 | structs :
186 |      {auto str : Struct f}
187 |   -> {auto sof : SizeOf (f s)}
188 |   -> List c
189 |   -> CArray s n (f s)
190 |   -> (f s -> F1 s c)
191 |   -> (k : Nat)
192 |   -> {auto 0 prf : LTE k n}
193 |   -> F1 s (List c)
194 | structs cs arr f 0     t = cs # t
195 | structs cs arr f (S k) t =
196 |   let vb # t := getStructNat arr k t
197 |       vc # t := f vb t
198 |    in structs (vc::cs) arr f k t
199 |