0 | module Text.WebIDL.Types.Type
  1 |
  2 | import Data.Bitraversable
  3 | import Data.Traversable
  4 | import Derive.Prelude
  5 | import Text.WebIDL.Types.Attribute
  6 | import Text.WebIDL.Types.Identifier
  7 |
  8 | %language ElabReflection
  9 |
 10 | ||| BufferRelatedType ::
 11 | |||     ArrayBuffer
 12 | |||     DataView
 13 | |||     Int8Array
 14 | |||     Int16Array
 15 | |||     Int32Array
 16 | |||     Uint8Array
 17 | |||     Uint16Array
 18 | |||     Uint32Array
 19 | |||     Uint8ClampedArray
 20 | |||     Float32Array
 21 | |||     Float64Array
 22 | public export
 23 | data BufferRelatedType =
 24 |     ArrayBuffer
 25 |   | DataView
 26 |   | Int8Array
 27 |   | Int16Array
 28 |   | Int32Array
 29 |   | Uint8Array
 30 |   | Uint16Array
 31 |   | Uint32Array
 32 |   | Uint8ClampedArray
 33 |   | Float32Array
 34 |   | Float64Array
 35 |
 36 | %runElab derive "BufferRelatedType" [Eq,Show,HasAttributes]
 37 |
 38 | ||| StringType ::
 39 | |||     ByteString
 40 | |||     DOMString
 41 | |||     USVString
 42 | public export
 43 | data StringType = ByteString | DOMString | USVString
 44 |
 45 | %runElab derive "Type.StringType" [Eq,Show,HasAttributes]
 46 |
 47 | public export
 48 | data IntType = Short | Long | LongLong
 49 |
 50 | %runElab derive "Type.IntType" [Eq,Show,HasAttributes]
 51 |
 52 | public export
 53 | data FloatType = Float | Dbl
 54 |
 55 | %runElab derive "Type.FloatType" [Eq,Show,HasAttributes]
 56 |
 57 | ||| PrimitiveType ::
 58 | |||     UnsignedIntegerType
 59 | |||     UnrestrictedFloatType
 60 | |||     undefined
 61 | |||     boolean
 62 | |||     byte
 63 | |||     octet
 64 | |||     bigint
 65 | ||| UnrestrictedFloatType ::
 66 | |||     unrestricted FloatType
 67 | |||     FloatType
 68 | |||
 69 | ||| FloatType ::
 70 | |||     float
 71 | |||     double
 72 | |||
 73 | ||| UnsignedIntegerType ::
 74 | |||     unsigned IntegerType
 75 | |||     IntegerType
 76 | |||
 77 | ||| IntegerType ::
 78 | |||     short
 79 | |||     long OptionalLong
 80 | |||
 81 | ||| OptionalLong ::
 82 | |||     long
 83 | |||     ε
 84 | public export
 85 | data PrimitiveType : Type where
 86 |   Unsigned     : IntType -> PrimitiveType
 87 |   Signed       : IntType -> PrimitiveType
 88 |   Unrestricted : FloatType -> PrimitiveType
 89 |   Restricted   : FloatType -> PrimitiveType
 90 |   Undefined    : PrimitiveType
 91 |   Boolean      : PrimitiveType
 92 |   Byte         : PrimitiveType
 93 |   Octet        : PrimitiveType
 94 |   BigInt       : PrimitiveType
 95 |
 96 | %runElab derive "PrimitiveType" [Eq,Show,HasAttributes]
 97 |
 98 | public export
 99 | data ConstTypeF a = CP PrimitiveType | CI a
100 |
101 | %runElab derive "ConstTypeF" [Eq,Show,HasAttributes]
102 |
103 | ||| Null ::
104 | |||     ?
105 | |||     ε
106 | public export
107 | data Nullable a = MaybeNull a | NotNull a
108 |
109 | %runElab derive "Nullable" [Eq,Show,HasAttributes]
110 |
111 | public export
112 | val : Nullable a -> a
113 | val (MaybeNull x) = x
114 | val (NotNull x)   = x
115 |
116 | public export
117 | zipWith : (a -> b -> c) -> Nullable a -> Nullable b -> Nullable c
118 | zipWith f (NotNull x) (NotNull y) = NotNull $ f x y
119 | zipWith f x y                     = MaybeNull $ f (val x) (val y)
120 |
121 | public export
122 | Functor Nullable where
123 |   map f (MaybeNull x) = MaybeNull $ f x
124 |   map f (NotNull x)   = NotNull $ f x
125 |
126 | public export
127 | Foldable Nullable where
128 |   foldr f acc v = f (val v) acc
129 |
130 | public export
131 | Traversable Nullable where
132 |   traverse f (MaybeNull x) = MaybeNull <$> f x
133 |   traverse f (NotNull x)   = NotNull <$> f x
134 |
135 | export
136 | nullVal : Nullable a -> a
137 | nullVal (MaybeNull x) = x
138 | nullVal (NotNull x)   = x
139 |
140 | export
141 | nullable : Nullable a -> Nullable a
142 | nullable = MaybeNull . nullVal
143 |
144 | export
145 | notNullable : Nullable a -> Nullable a
146 | notNullable = NotNull . nullVal
147 |
148 | export
149 | isNullable : Nullable a -> Bool
150 | isNullable (MaybeNull _) = True
151 | isNullable (NotNull _)   = False
152 |
153 | mutual
154 |   ||| Type ::
155 |   |||     SingleType
156 |   |||     UnionType Null
157 |   |||
158 |   ||| SingleType ::
159 |   |||     DistinguishableType
160 |   |||     any
161 |   |||     PromiseType
162 |   |||
163 |   ||| PromiseType ::
164 |   |||     Promise < Type >
165 |   public export
166 |   data IdlTypeF : (a : Type) -> (b : Type) -> Type where
167 |     Any     : IdlTypeF a b
168 |     D       : Nullable (DistinguishableF a b) -> IdlTypeF a b
169 |     U       : Nullable (UnionTypeF a b) -> IdlTypeF a b
170 |     Promise : IdlTypeF a b -> IdlTypeF a b
171 |
172 |   ||| UnionType ::
173 |   |||     ( UnionMemberType or UnionMemberType UnionMemberTypes )
174 |   |||
175 |   ||| UnionMemberTypes ::
176 |   |||     or UnionMemberType UnionMemberTypes
177 |   |||     ε
178 |   public export
179 |   record UnionTypeF (a : Type) (b : Type) where
180 |     constructor UT
181 |     fst  : UnionMemberTypeF a b
182 |     snd  : UnionMemberTypeF a b
183 |     rest : List (UnionMemberTypeF a b)
184 |
185 |   ||| UnionMemberType ::
186 |   |||     ExtendedAttributeList DistinguishableType
187 |   |||     UnionType Null
188 |   public export
189 |   record UnionMemberTypeF (a : Type) (b : Type) where
190 |     constructor MkUnionMember
191 |     attr : a
192 |     type : DistinguishableF a b
193 |
194 |   ||| DistinguishableType ::
195 |   |||     PrimitiveType Null
196 |   |||     StringType Null
197 |   |||     identifier Null
198 |   |||     sequence < TypeWithExtendedAttributes > Null
199 |   |||     object Null
200 |   |||     symbol Null
201 |   |||     BufferRelatedType Null
202 |   |||     FrozenArray < TypeWithExtendedAttributes > Null
203 |   |||     ObservableArray < TypeWithExtendedAttributes > Null
204 |   |||     RecordType Null
205 |   |||
206 |   ||| RecordType ::
207 |   |||     record < StringType , TypeWithExtendedAttributes >
208 |   public export
209 |   data DistinguishableF : (a : Type) -> (b : Type) -> Type where
210 |     P : PrimitiveType -> DistinguishableF a b
211 |     S : StringType -> DistinguishableF a b
212 |     I : b -> DistinguishableF a b
213 |     B : BufferRelatedType -> DistinguishableF a b
214 |     Sequence : a -> IdlTypeF a b -> DistinguishableF a b
215 |     FrozenArray : a -> IdlTypeF a b -> DistinguishableF a b
216 |     ObservableArray : a -> IdlTypeF a b -> DistinguishableF a b
217 |     Record : StringType -> a -> IdlTypeF a b -> DistinguishableF a b
218 |     Object : DistinguishableF a b
219 |     Symbol : DistinguishableF a b
220 |
221 | %runElab deriveMutual
222 |   [ "DistinguishableF"
223 |   , "UnionMemberTypeF"
224 |   , "UnionTypeF"
225 |   , "IdlTypeF"
226 |   ] [Show, Eq]
227 |
228 | public export
229 | IdlType : Type
230 | IdlType = IdlTypeF ExtAttributeList Identifier
231 |
232 | public export
233 | UnionType : Type
234 | UnionType = UnionTypeF ExtAttributeList Identifier
235 |
236 | public export
237 | UnionMemberType : Type
238 | UnionMemberType = UnionMemberTypeF ExtAttributeList Identifier
239 |
240 | public export
241 | Distinguishable : Type
242 | Distinguishable = DistinguishableF ExtAttributeList Identifier
243 |
244 | public export
245 | ConstType : Type
246 | ConstType = ConstTypeF Identifier
247 |
248 | ||| OptionalType ::
249 | |||     , TypeWithExtendedAttributes
250 | |||     ε
251 | public export
252 | 0 OptionalType : Type
253 | OptionalType = Maybe (Attributed IdlType)
254 |
255 | ||| Wraps and `Indentifier` as a non-nullable type.
256 | export
257 | identToType : b -> IdlTypeF a b
258 | identToType = D . NotNull . I
259 |
260 | ||| The `Undefined` type
261 | export
262 | undefined : IdlTypeF a b
263 | undefined = D $ NotNull $ P Undefined
264 |
265 | export
266 | isUndefined : IdlTypeF a b -> Bool
267 | isUndefined (D $ NotNull $ P Undefined) = True
268 | isUndefined _                           = False
269 |
270 | export
271 | domString : IdlTypeF a b
272 | domString = D $ NotNull $ S DOMString
273 |
274 | export
275 | ulong : IdlTypeF a b
276 | ulong = D $ NotNull $ P $ Unsigned Long
277 |
278 | export
279 | isIndex : IdlTypeF a b -> Bool
280 | isIndex (D $ NotNull $ S DOMString)       = True
281 | isIndex (D $ NotNull $ P $ Unsigned Long) = True
282 | isIndex _                                 = False
283 |
284 | --------------------------------------------------------------------------------
285 | --          Implementations
286 | --------------------------------------------------------------------------------
287 |
288 | mutual
289 |   export
290 |   Functor ConstTypeF where map = mapDefault
291 |
292 |   export
293 |   Foldable ConstTypeF where foldr = foldrDefault
294 |
295 |   export
296 |   Traversable ConstTypeF where
297 |     traverse _ (CP x) = pure (CP x)
298 |     traverse f (CI x) = CI <$> f x
299 |
300 | mutual
301 |   export
302 |   Bifunctor DistinguishableF where bimap = assert_total bimapDefault
303 |
304 |   export
305 |   Bifoldable DistinguishableF where bifoldr = bifoldrDefault
306 |
307 |   export
308 |   Bitraversable DistinguishableF where
309 |     bitraverse _ _ (P x) = pure (P x)
310 |     bitraverse _ _ (S x) = pure (S x)
311 |     bitraverse _ g (I x) = I <$> g x
312 |     bitraverse _ _ (B x) = pure (B x)
313 |     bitraverse f g (Sequence x y) = [| Sequence (f x) (bitraverse f g y) |]
314 |     bitraverse f g (FrozenArray x y) = [| FrozenArray (f x) (bitraverse f g y) |]
315 |     bitraverse f g (ObservableArray x y) = [| ObservableArray (f x) (bitraverse f g y) |]
316 |     bitraverse f g (Record x y z) = [| Record (pure x) (f y) (bitraverse f g z) |]
317 |     bitraverse _ _ Object = pure Object
318 |     bitraverse _ _ Symbol = pure Symbol
319 |
320 |   export
321 |   Functor (DistinguishableF a) where map = bimap id
322 |
323 |   export
324 |   Foldable (DistinguishableF a) where foldr = bifoldr (const id)
325 |
326 |   export
327 |   Traversable (DistinguishableF a) where traverse = bitraverse pure
328 |
329 |   export
330 |   Bifunctor UnionMemberTypeF where bimap = assert_total bimapDefault
331 |
332 |   export
333 |   Bifoldable UnionMemberTypeF where bifoldr = bifoldrDefault
334 |
335 |   export
336 |   Bitraversable UnionMemberTypeF where
337 |     bitraverse f g (MkUnionMember a t) =
338 |       [| MkUnionMember (f a) (bitraverse f g t) |]
339 |
340 |   export
341 |   Functor (UnionMemberTypeF a) where map = bimap id
342 |
343 |   export
344 |   Foldable (UnionMemberTypeF a) where foldr = bifoldr (const id)
345 |
346 |   export
347 |   Traversable (UnionMemberTypeF a) where traverse = bitraverse pure
348 |
349 |   export
350 |   Bifunctor UnionTypeF where bimap = assert_total bimapDefault
351 |
352 |   export
353 |   Bifoldable UnionTypeF where bifoldr = bifoldrDefault
354 |
355 |   export
356 |   Bitraversable UnionTypeF where
357 |     bitraverse f g (UT a b ts) =
358 |       [| UT (bitraverse f g a) (bitraverse f g b)
359 |             (traverse (bitraverse f g) ts) |]
360 |
361 |   export
362 |   Functor (UnionTypeF a) where map = bimap id
363 |
364 |   export
365 |   Foldable (UnionTypeF a) where foldr = bifoldr (const id)
366 |
367 |   export
368 |   Traversable (UnionTypeF a) where traverse = bitraverse pure
369 |
370 |   export
371 |   Bifunctor IdlTypeF where bimap = assert_total bimapDefault
372 |
373 |   export
374 |   Bifoldable IdlTypeF where bifoldr = bifoldrDefault
375 |
376 |   export
377 |   Bitraversable IdlTypeF where
378 |     bitraverse f g Any = pure Any
379 |     bitraverse f g (D x) = D <$> traverse (bitraverse f g) x
380 |     bitraverse f g (U x) = U <$> traverse (bitraverse f g) x
381 |     bitraverse f g (Promise x) = Promise <$> bitraverse f g x
382 |
383 |   export
384 |   Functor (IdlTypeF a) where map = bimap id
385 |
386 |   export
387 |   Foldable (IdlTypeF a) where foldr = bifoldr (const id)
388 |
389 |   export
390 |   Traversable (IdlTypeF a) where traverse = bitraverse pure
391 |
392 |   export
393 |   HasAttributes a => HasAttributes (IdlTypeF a b) where
394 |     attributes = bifoldMap attributes (const Nil)
395 |