0 | module Text.WebIDL.Types.Member
  1 |
  2 | import Data.SOP
  3 | import Derive.Prelude
  4 | import Text.WebIDL.Types.Argument
  5 | import Text.WebIDL.Types.Attribute
  6 | import Text.WebIDL.Types.Identifier
  7 | import Text.WebIDL.Types.StringLit
  8 | import Text.WebIDL.Types.Type
  9 |
 10 | %language ElabReflection
 11 |
 12 | ||| Const ::
 13 | |||     const ConstType identifier = ConstValue ;
 14 | |||
 15 | ||| ConstValue ::
 16 | |||     BooleanLiteral
 17 | |||     FloatLiteral
 18 | |||     integer
 19 | public export
 20 | record Const where
 21 |   constructor MkConst
 22 |   type  : ConstType
 23 |   name  : Identifier
 24 |   value : ConstValue
 25 |
 26 | %runElab derive "Const" [Eq,Show,HasAttributes]
 27 |
 28 | --------------------------------------------------------------------------------
 29 | --          Operation
 30 | --------------------------------------------------------------------------------
 31 |
 32 | ||| OperationName ::
 33 | |||     OperationNameKeyword
 34 | |||     identifier
 35 | |||
 36 | ||| OperationNameKeyword ::
 37 | |||     includes
 38 | public export
 39 | record OperationName where
 40 |   constructor MkOpName
 41 |   value : String
 42 |
 43 | %runElab derive "OperationName" [Eq,Show,HasAttributes]
 44 |
 45 | ||| Special ::
 46 | |||     getter
 47 | |||     setter
 48 | |||     deleter
 49 | public export
 50 | data Special = Getter | Setter | Deleter
 51 |
 52 | %runElab derive "Special" [Eq,Show,HasAttributes]
 53 |
 54 | ||| RegularOperation ::
 55 | |||     Type OperationRest
 56 | |||
 57 | ||| OperationRest ::
 58 | |||     OptionalOperationName ( ArgumentList ) ;
 59 | |||
 60 | ||| OptionalOperationName ::
 61 | |||     OperationName
 62 | |||     ε
 63 | |||
 64 | ||| SpecialOperation ::
 65 | |||     Special RegularOperation
 66 | |||
 67 | ||| Operation ::
 68 | |||     RegularOperation
 69 | |||     SpecialOperation
 70 | public export
 71 | record Op a where
 72 |   constructor MkOp
 73 |   special : a
 74 |   type    : IdlType
 75 |   name    : Maybe OperationName
 76 |   args    : ArgumentList
 77 |
 78 | %runElab derive "Op" [Eq,Show,HasAttributes]
 79 |
 80 | public export
 81 | 0 RegularOperation : Type
 82 | RegularOperation = Op ()
 83 |
 84 | public export
 85 | 0 SpecialOperation : Type
 86 | SpecialOperation = Op Special
 87 |
 88 | public export
 89 | 0 Operation : Type
 90 | Operation = Op (Maybe Special)
 91 |
 92 | public export
 93 | regToOp : RegularOperation -> Operation
 94 | regToOp = { special := Nothing }
 95 |
 96 | public export
 97 | specToOp : SpecialOperation -> Operation
 98 | specToOp = { special $= Just }
 99 |
100 | --------------------------------------------------------------------------------
101 | --          Callbacks
102 | --------------------------------------------------------------------------------
103 |
104 |
105 | ||| CallbackInterfaceMember ::
106 | |||     Const
107 | |||     RegularOperation
108 | public export
109 | 0 CallbackInterfaceMember : Type
110 | CallbackInterfaceMember = NS I [Const,RegularOperation]
111 |
112 | ||| CallbackInterfaceMembers ::
113 | |||     ExtendedAttributeList CallbackInterfaceMember CallbackInterfaceMembers
114 | |||     ε
115 | public export
116 | 0 CallbackInterfaceMembers : Type
117 | CallbackInterfaceMembers = List (Attributed CallbackInterfaceMember)
118 |
119 | --------------------------------------------------------------------------------
120 | --          Dictionary
121 | --------------------------------------------------------------------------------
122 |
123 | ||| Inheritance ::
124 | |||     : identifier
125 | |||     ε
126 | public export
127 | 0 Inheritance : Type
128 | Inheritance = Maybe Identifier
129 |
130 | ||| DictionaryMemberRest ::
131 | |||     required TypeWithExtendedAttributes identifier ;
132 | |||     Type identifier Default ;
133 | public export
134 | data DictionaryMemberRest : Type where
135 |   Required :  (attrs : ExtAttributeList)
136 |            -> (type : IdlType)
137 |            -> (name : Identifier)
138 |            -> DictionaryMemberRest
139 |
140 |   Optional :  (type  : IdlType)
141 |            -> (name  : Identifier)
142 |            -> (deflt : Default)
143 |            -> DictionaryMemberRest
144 |
145 | %runElab derive "DictionaryMemberRest" [Eq,Show,HasAttributes]
146 |
147 | ||| DictionaryMember ::
148 | |||     ExtendedAttributeList DictionaryMemberRest
149 | public export
150 | 0 DictionaryMember : Type
151 | DictionaryMember = Attributed DictionaryMemberRest
152 |
153 | ||| DictionaryMembers ::
154 | |||     DictionaryMember DictionaryMembers
155 | |||     ε
156 | public export
157 | 0 DictionaryMembers : Type
158 | DictionaryMembers = List DictionaryMember
159 |
160 | --------------------------------------------------------------------------------
161 | --          Attributes
162 | --------------------------------------------------------------------------------
163 |
164 | public export
165 | record Readonly a where
166 |   constructor MkRO
167 |   value : a
168 |
169 | %runElab derive "Readonly" [Eq,Show,HasAttributes]
170 |
171 | public export
172 | record Inherit a where
173 |   constructor MkI
174 |   value : a
175 |
176 | %runElab derive "Inherit" [Eq,Show,HasAttributes]
177 |
178 | ||| AttributeName ::
179 | |||     AttributeNameKeyword
180 | |||     identifier
181 | |||
182 | ||| AttributeNameKeyword ::
183 | |||     async
184 | |||     required
185 | public export
186 | record AttributeName where
187 |   constructor MkAttributeName
188 |   value : String
189 |
190 | %runElab derive "AttributeName" [Eq,Ord,Show,HasAttributes]
191 |
192 | ||| AttributeRest ::
193 | |||     attribute TypeWithExtendedAttributes AttributeName ;
194 | public export
195 | record Attribute where
196 |   constructor MkAttribute
197 |   attrs : ExtAttributeList
198 |   type  : IdlType
199 |   name  : AttributeName
200 |
201 | %runElab derive "Attribute" [Eq,Show,HasAttributes]
202 |
203 | ||| ReadWriteMaplike ::
204 | |||     MaplikeRest
205 | |||
206 | ||| MaplikeRest ::
207 | |||     maplike < TypeWithExtendedAttributes , TypeWithExtendedAttributes > ;
208 | public export
209 | record Maplike where
210 |   constructor MkMaplike
211 |   fstTpe : Attributed IdlType
212 |   sndTpe : Attributed IdlType
213 |
214 | %runElab derive "Maplike" [Eq,Show,HasAttributes]
215 |
216 | export
217 | HasAttributes Maplike where
218 |   attributes v = fst (v.fstTpe) ++ fst (v.sndTpe)
219 |
220 | ||| ReadWriteSetlike ::
221 | |||     SetlikeRest
222 | |||
223 | ||| SetlikeRest ::
224 | |||     setlike < TypeWithExtendedAttributes > ;
225 | public export
226 | record Setlike where
227 |   constructor MkSetlike
228 |   type : Attributed IdlType
229 |
230 | %runElab derive "Setlike" [Eq,Show,HasAttributes]
231 |
232 | ||| StringifierRest ::
233 | |||     OptionalReadOnly AttributeRest
234 | |||     RegularOperation
235 | |||     ;
236 | |||
237 | ||| Stringifier ::
238 | |||     stringifier StringifierRest
239 | public export
240 | 0 Stringifier : Type
241 | Stringifier = NS I [Attribute, Readonly Attribute, RegularOperation,()]
242 |
243 | ||| StaticMember ::
244 | |||     static StaticMemberRest
245 | |||
246 | ||| StaticMemberRest ::
247 | |||     OptionalReadOnly AttributeRest
248 | |||     RegularOperation
249 | public export
250 | 0 StaticMember : Type
251 | StaticMember = NS I [Attribute, Readonly Attribute, RegularOperation]
252 |
253 | --------------------------------------------------------------------------------
254 | --          Namespace
255 | --------------------------------------------------------------------------------
256 |
257 | ||| NamespaceMember ::
258 | |||     RegularOperation
259 | |||     readonly AttributeRest
260 | public export
261 | 0 NamespaceMember : Type
262 | NamespaceMember = NS I [RegularOperation, Readonly Attribute]
263 |
264 | ||| NamespaceMembers ::
265 | |||     ExtendedAttributeList NamespaceMember NamespaceMembers
266 | |||     ε
267 | public export
268 | 0 NamespaceMembers : Type
269 | NamespaceMembers = List (Attributed NamespaceMember)
270 |
271 | --------------------------------------------------------------------------------
272 | --          Interface
273 | --------------------------------------------------------------------------------
274 |
275 | ||| Constructor ::
276 | |||     constructor ( ArgumentList ) ;
277 | public export
278 | record Constructor where
279 |   constructor MkConstructor
280 |   args : ArgumentList
281 |
282 | %runElab derive "Constructor" [Eq,Show,HasAttributes]
283 |
284 | ||| PartialInterfaceMember ::
285 | |||     Const
286 | |||     Operation
287 | |||     Stringifier
288 | |||     StaticMember
289 | |||     Iterable
290 | |||     AsyncIterable
291 | |||     ReadOnlyMember
292 | |||     ReadWriteAttribute
293 | |||     ReadWriteMaplike
294 | |||     ReadWriteSetlike
295 | |||     InheritAttribute
296 | |||
297 | ||| Iterable ::
298 | |||     iterable < TypeWithExtendedAttributes OptionalType > ;
299 | public export
300 | data PartialInterfaceMember =
301 |     IConst   Const
302 |   | IOp      Operation
303 |   | IStr     Stringifier
304 |   | IStatic  StaticMember
305 |   | IAttr    Attribute
306 |   | IMap     Maplike
307 |   | ISet     Setlike
308 |   | IAttrRO  (Readonly Attribute)
309 |   | IMapRO   (Readonly Maplike)
310 |   | ISetRO   (Readonly Setlike)
311 |   | IAttrInh (Inherit Attribute)
312 |   | IIterable (Attributed IdlType) OptionalType
313 |   | IAsync   (Attributed IdlType) OptionalType ArgumentList
314 |
315 | %runElab derive "PartialInterfaceMember" [Eq,Show,HasAttributes]
316 |
317 |
318 | ||| MixinMember ::
319 | |||     Const
320 | |||     RegularOperation
321 | |||     Stringifier
322 | |||     OptionalReadOnly AttributeRest
323 | public export
324 | data MixinMember =
325 |     MConst   Const
326 |   | MOp      RegularOperation
327 |   | MStr     Stringifier
328 |   | MAttr    Attribute
329 |   | MAttrRO  (Readonly Attribute)
330 |
331 | %runElab derive "MixinMember" [Eq,Show,HasAttributes]
332 |
333 |
334 | ||| PartialInterfaceMembers ::
335 | |||     ExtendedAttributeList PartialInterfaceMember PartialInterfaceMembers
336 | |||     ε
337 | public export
338 | 0 PartialInterfaceMembers : Type
339 | PartialInterfaceMembers = List (Attributed PartialInterfaceMember)
340 |
341 | ||| InterfaceMember ::
342 | |||     PartialInterfaceMember
343 | |||     Constructor
344 | public export
345 | 0 InterfaceMember : Type
346 | InterfaceMember = NS I [Constructor,PartialInterfaceMember]
347 |
348 |
349 | ||| InterfaceMembers ::
350 | |||     ExtendedAttributeList InterfaceMember InterfaceMembers
351 | |||     ε
352 | public export
353 | 0 InterfaceMembers : Type
354 | InterfaceMembers = List (Attributed InterfaceMember)
355 |
356 | ||| MixinMembers ::
357 | |||     ExtendedAttributeList MixinMember MixinMembers
358 | |||     ε
359 | public export
360 | 0 MixinMembers : Type
361 | MixinMembers = List (Attributed MixinMember)
362 |
363 | --------------------------------------------------------------------------------
364 | --          Extractors
365 | --------------------------------------------------------------------------------
366 |
367 | namespace CallbackInterfaceMember
368 |   export
369 |   const : Attributed CallbackInterfaceMember -> Maybe Const
370 |   const (_,Z x) = Just x
371 |   const _       = Nothing
372 |
373 | namespace Dictionary
374 |   export
375 |   optional : DictionaryMember -> Maybe Attribute
376 |   optional (_, Required _ _ _) = Nothing
377 |   optional (_, Optional t n _) =
378 |     Just $ MkAttribute Nil t (MkAttributeName n.value)
379 |
380 |   export
381 |   required : DictionaryMember -> Maybe Attribute
382 |   required (_, Required _ t n) =
383 |     Just $ MkAttribute Nil t (MkAttributeName n.value)
384 |   required (_, Optional _ _ _) = Nothing
385 |
386 | namespace InterfaceMember
387 |   export
388 |   part :  (PartialInterfaceMember -> Maybe a)
389 |        -> Attributed InterfaceMember
390 |        -> Maybe a
391 |   part f (_,(S $ Z $ p)) = f p
392 |   part _ _               = Nothing
393 |
394 | namespace MixinMember
395 |   export
396 |   const : Attributed MixinMember -> Maybe Const
397 |   const (_,MConst x) = Just x
398 |   const _            = Nothing
399 |
400 |   export
401 |   attrRO : Attributed MixinMember -> Maybe (Readonly Attribute)
402 |   attrRO (_, (MAttrRO x)) = Just x
403 |   attrRO _                = Nothing
404 |
405 |   export
406 |   attr : Attributed MixinMember -> Maybe Attribute
407 |   attr (_, (MAttr x)) = Just x
408 |   attr _              = Nothing
409 |
410 | namespace NamespaceMember
411 |
412 |   export
413 |   attrRO : NamespaceMember -> Maybe (Readonly Attribute)
414 |   attrRO (S $ Z x) = Just x
415 |   attrRO (Z _)     = Nothing
416 |
417 | namespace PartialInterfaceMember
418 |   export
419 |   const : PartialInterfaceMember -> Maybe Const
420 |   const (IConst x) = Just x
421 |   const _          = Nothing
422 |
423 |   export
424 |   attrRO : PartialInterfaceMember -> Maybe (Readonly Attribute)
425 |   attrRO (IAttrRO x) = Just x
426 |   attrRO _           = Nothing
427 |
428 |   export
429 |   attr : PartialInterfaceMember -> Maybe Attribute
430 |   attr (IAttr x) = Just x
431 |   attr _         = Nothing
432 |