
   0 | module Text.WebIDL.Codegen.Types
   1 | 
   2 | import Derive.Prelude
   3 | import public Data.SortedMap
   4 | import Text.WebIDL.Types
   5 | 
   6 | %default total
   7 | %language ElabReflection
   8 | 
   9 | --------------------------------------------------------------------------------
  10 | --          Kinds
  11 | --------------------------------------------------------------------------------
  12 | 
  13 | ||| The kind of a WebIDL identifier.
  14 | |||
  15 | ||| This is needed when converting external types to Idris2 types
  16 | ||| in the code generator: Aliases need to be resolved, Enums
  17 | ||| converted to their `String` representation, Callback arguments
  18 | ||| are Idris2 functions that need to be converted to an external
  19 | ||| type.
  20 | public export
  21 | data Kind : Type where
  22 |   KAlias      : Identifier -> Kind
  23 |   KCallback   : Identifier -> Kind
  24 |   KDictionary : Identifier -> Kind
  25 |   KEnum       : Identifier -> Kind
  26 |   KInterface  : (isParent : Bool) -> Identifier -> Kind
  27 |   KMixin      : Identifier -> Kind
  28 |   KOther      : Identifier -> Kind
  29 | 
  30 | %runElab derive "Kind" [Eq,Show]
  31 | 
  32 | public export
  33 | isParent : Kind -> Bool
  34 | isParent (KDictionary _)  = True
  35 | isParent (KInterface b _) = b
  36 | isParent (KMixin _)       = True
  37 | isParent _                = False
  38 | 
  39 | public export
  40 | ident : Kind -> Identifier
  41 | ident (KAlias x)        = x
  42 | ident (KCallback x)     = x
  43 | ident (KDictionary x)   = x
  44 | ident (KEnum x)         = x
  45 | ident (KInterface _ x)  = x
  46 | ident (KMixin x)        = x
  47 | ident (KOther x)        = x
  48 | 
  49 | public export
  50 | kindToString : Kind -> String
  51 | kindToString = value . ident
  52 | 
  53 | public export
  54 | data Wrapper = Direct | Opt | May | OptMay
  55 | 
  56 | public export
  57 | opt : Wrapper -> Wrapper
  58 | opt Direct = Opt
  59 | opt May    = OptMay
  60 | opt i      = i
  61 | 
  62 | public export
  63 | may : Wrapper -> Wrapper
  64 | may Direct = May
  65 | may i      = i
  66 | 
  67 | --------------------------------------------------------------------------------
  68 | --          Types
  69 | --------------------------------------------------------------------------------
  70 | public export
  71 | data SimpleType : Type
  72 | 
  73 | public export
  74 | data CGType : Type
  75 | 
  76 | data SimpleType : Type where
  77 |   ||| The undefined type (or () if it is a return type)
  78 |   Undef        : SimpleType
  79 | 
  80 |   ||| `Boolean` at the FFI, `Bool` in the API.
  81 |   Boolean      : SimpleType
  82 | 
  83 |   ||| A Web IDL interface. This has an instance of `SafeCast`,
  84 |   ||| and is being abstracted over when used in an argument
  85 |   ||| list in the API, but only, when the `isParent` flag is set to true.
  86 |   ||| If this flag is `False`, meaning that there are no subtypes of
  87 |   ||| this type, we do not abstract over the type to improve
  88 |   ||| type inference.
  89 |   Interface   : (isParent : Bool) -> Identifier  -> SimpleType
  90 | 
  91 |   ||| A dictionary, specifying a Javascript object with a
  92 |   ||| set of mandatory and optional attributes.
  93 |   ||| This is always abstracted over, since theoretically
  94 |   ||| every value with the same set of attributes is
  95 |   ||| a dictionary of the given type.
  96 |   |||
  97 |   ||| The type of a dictionary cannot be verified at
  98 |   ||| runtime, therefore they have no instance of `SafeCast`.
  99 |   Dictionary  : Identifier  -> SimpleType
 100 | 
 101 |   ||| A Web IDL `Mixin` is a set of attributes and operations (functions)
 102 |   ||| shared by several types. A type includes a given mixin, if
 103 |   ||| a corresponding `includes` statement is provided in the spec.
 104 |   |||
 105 |   ||| Mixins do not define new types, and whether a value implements
 106 |   ||| a given mixin can typcally not be verified at runtime, therefore
 107 |   ||| mixins come without an instance of `SafeCast`.
 108 |   ||| runtime, therefore they have no instance of `SafeCast`.
 109 |   Mixin  : Identifier  -> SimpleType
 110 | 
 111 |   ||| Primitive type or a wrapper of a primitive.
 112 |   ||| This is the same at the FFI and API and
 113 |   ||| has an instance of `SafeCast`.
 114 |   Primitive : String      -> SimpleType
 115 | 
 116 |   ||| Types that do not change between FFI and API
 117 |   Unchangeable : String      -> SimpleType
 118 | 
 119 |   ||| Enum type at the API, Strings at the FFI
 120 |   Enum         : Identifier  -> SimpleType
 121 | 
 122 |   ||| Some kind of Array
 123 |   Array        : CGType      -> SimpleType
 124 | 
 125 |   ||| Some kind of Record
 126 |   Record       : String      -> CGType -> SimpleType
 127 | 
 128 | data CGType : Type where
 129 |   Any     : CGType
 130 |   Promise : CGType                      -> CGType
 131 |   Simple  : Nullable SimpleType         -> CGType
 132 |   Union   : Nullable (List1 SimpleType) -> CGType
 133 | 
 134 | ||| True, if the type can be used as an index in a
 135 | ||| WebIDL `Getter` or `Setter`, that is, it corresponds
 136 | ||| to either an `unsigned long` or a `DOMString`.
 137 | export
 138 | isIndex : CGType -> Bool
 139 | isIndex (Simple $ NotNull $ Primitive "String") = True
 140 | isIndex (Simple $ NotNull $ Primitive "Bits32") = True
 141 | isIndex _                                       = False
 142 | 
 143 | namespace SimpleType
 144 |   ||| True, if the FFI representation of the given type
 145 |   ||| has a `SafeCast` implementation
 146 |   export
 147 |   safeCast : SimpleType -> Bool
 148 |   safeCast Undef            = True
 149 |   safeCast Boolean          = True
 150 |   safeCast (Interface _ x)  = True
 151 |   safeCast (Dictionary _)   = False
 152 |   safeCast (Mixin _)        = False
 153 |   safeCast (Primitive x)    = True
 154 |   safeCast (Unchangeable x) = False
 155 |   safeCast (Enum x)         = True
 156 |   safeCast (Array x)        = False
 157 |   safeCast (Record x y)     = False
 158 | 
 159 |   ||| True, if the type uses the same representation in
 160 |   ||| the FFI and the API as a function argument
 161 |   export
 162 |   sameArgType : SimpleType -> Bool
 163 |   sameArgType Undef            = True
 164 |   sameArgType Boolean          = False
 165 |   sameArgType (Interface b _)  = not b
 166 |   sameArgType (Dictionary _)   = False
 167 |   sameArgType (Mixin _)        = False
 168 |   sameArgType (Primitive t)    = True
 169 |   sameArgType (Unchangeable _) = True
 170 |   sameArgType (Enum _)         = False
 171 |   sameArgType (Array _)        = True
 172 |   sameArgType (Record _ _)     = True
 173 | 
 174 |   ||| True, if the type uses the same representation in
 175 |   ||| the FFI and the API as a return value.
 176 |   export
 177 |   sameRetType : SimpleType -> Bool
 178 |   sameRetType Undef            = True
 179 |   sameRetType Boolean          = False
 180 |   sameRetType (Interface _ _)  = True
 181 |   sameRetType (Dictionary _)   = True
 182 |   sameRetType (Mixin _)        = True
 183 |   sameRetType (Primitive _)    = True
 184 |   sameRetType (Unchangeable _) = True
 185 |   sameRetType (Enum _)         = False
 186 |   sameRetType (Array _)        = True
 187 |   sameRetType (Record _ _)     = True
 188 | 
 189 |   export
 190 |   inheritance : SimpleType -> Maybe (Identifier,Wrapper)
 191 |   inheritance (Interface True x)  = Just (x,Direct)
 192 |   inheritance (Dictionary x)      = Just (x,Direct)
 193 |   inheritance (Mixin x)           = Just (x,Direct)
 194 |   inheritance _                   = Nothing
 195 | 
 196 | namespace CGType
 197 | 
 198 |   public export
 199 |   simple : SimpleType -> CGType
 200 |   simple = Simple . NotNull
 201 | 
 202 |   public export
 203 |   unchangeable : String -> CGType
 204 |   unchangeable = simple . Unchangeable
 205 | 
 206 |   public export
 207 |   iface : Bool -> Identifier -> CGType
 208 |   iface b = simple . Interface b
 209 | 
 210 |   public export
 211 |   mixin : Identifier -> CGType
 212 |   mixin = simple . Mixin
 213 | 
 214 |   public export
 215 |   dict : Identifier -> CGType
 216 |   dict = simple . Dictionary
 217 | 
 218 |   ||| Wrapps the given kind in return type.
 219 |   export
 220 |   fromKind : Kind -> CGType
 221 |   fromKind (KAlias x)        = unchangeable x.value
 222 |   fromKind (KCallback x)     = unchangeable x.value
 223 |   fromKind (KDictionary x)   = dict x
 224 |   fromKind (KEnum x)         = Simple . NotNull $ Enum x
 225 |   fromKind (KInterface b x)  = iface b x
 226 |   fromKind (KMixin x)        = mixin x
 227 |   fromKind (KOther x)        = unchangeable x.value
 228 | 
 229 |   ||| True, if the FFI representation of the given type
 230 |   ||| has a `SafeCast` implementation
 231 |   export
 232 |   safeCast : CGType -> Bool
 233 |   safeCast Any         = True
 234 |   safeCast (Promise x) = False
 235 |   safeCast (Simple x)  = safeCast $ nullVal x
 236 |   safeCast (Union _)   = False
 237 | 
 238 |   ||| True, if the given type is the same in the API and
 239 |   ||| the FFI when used as an argument
 240 |   export
 241 |   sameArgType : CGType -> Bool
 242 |   sameArgType Any                    = False
 243 |   sameArgType (Promise x)            = True
 244 |   sameArgType (Simple $ MaybeNull _) = False
 245 |   sameArgType (Simple $ NotNull x)   = sameArgType x
 246 |   sameArgType (Union  _)             = False
 247 | 
 248 |   ||| True, if the given type is the same in the API and
 249 |   ||| the FFI when used as a return value
 250 |   export
 251 |   sameRetType : CGType -> Bool
 252 |   sameRetType Any                    = False
 253 |   sameRetType (Promise x)            = True
 254 |   sameRetType (Simple $ MaybeNull _) = False
 255 |   sameRetType (Simple $ NotNull x)   = sameRetType x
 256 |   sameRetType (Union  $ MaybeNull _) = False
 257 |   sameRetType (Union  $ NotNull xs)  = not $ all safeCast xs
 258 | 
 259 |   export
 260 |   inheritance : CGType -> Maybe (Identifier,Wrapper)
 261 |   inheritance (Simple $ MaybeNull x) = map may <$> inheritance x
 262 |   inheritance (Simple $ NotNull x)   = inheritance x
 263 |   inheritance _                      = Nothing
 264 | 
 265 | --------------------------------------------------------------------------------
 266 | --          ReturnType
 267 | --------------------------------------------------------------------------------
 268 | 
 269 | ||| A function's return type.
 270 | public export
 271 | data ReturnType : Type where
 272 |   ||| This will be mapped to `()` in the codegen.
 273 |   Undefined : ReturnType
 274 | 
 275 |   ||| The attribute in question might not be defined
 276 |   ||| The return type will be wrapped in `UndefOr` in
 277 |   ||| the code generator.
 278 |   UndefOr  : CGType -> Maybe Default -> ReturnType
 279 | 
 280 |   ||| Nothing special about the wrapped return type.
 281 |   Def      : CGType -> ReturnType
 282 | 
 283 | ||| Checks if the return type is `Undefined`.
 284 | public export
 285 | isUndefined : ReturnType -> Bool
 286 | isUndefined Undefined = True
 287 | isUndefined _         = False
 288 | 
 289 | namespace ReturnType
 290 | 
 291 |   public export
 292 |   simple : SimpleType -> ReturnType
 293 |   simple = Def . simple
 294 | 
 295 |   public export
 296 |   unchangeable : String -> ReturnType
 297 |   unchangeable = Def . unchangeable
 298 | 
 299 |   ||| Wrapps the given kind in return type.
 300 |   export
 301 |   fromKind : Kind -> ReturnType
 302 |   fromKind = Def . CGType.fromKind
 303 | 
 304 |   ||| True, if the given FFI type has a `SafeCast` instance
 305 |   export
 306 |   safeCast : ReturnType -> Bool
 307 |   safeCast Undefined     = True
 308 |   safeCast (UndefOr x _) = safeCast x
 309 |   safeCast (Def x)       = safeCast x
 310 | 
 311 |   ||| True, if the given return type is the same in the API and
 312 |   ||| the FFI.
 313 |   export
 314 |   sameType : ReturnType -> Bool
 315 |   sameType Undefined     = True
 316 |   sameType (UndefOr _ _) = False
 317 |   sameType (Def x)       = sameRetType x
 318 | 
 319 | --------------------------------------------------------------------------------
 320 | --          Constants
 321 | --------------------------------------------------------------------------------
 322 | 
 323 | public export
 324 | record CGConstType where
 325 |   constructor MkConstType
 326 |   primitive : String
 327 | 
 328 | public export
 329 | record CGConst where
 330 |   constructor MkConst
 331 |   type  : CGConstType
 332 |   name  : Identifier
 333 |   value : ConstValue
 334 | 
 335 | --------------------------------------------------------------------------------
 336 | --          Arguments
 337 | --------------------------------------------------------------------------------
 338 | 
 339 | ||| A function argument in the code generator.
 340 | public export
 341 | data CGArg : Type where
 342 |   ||| A mandatory function argument
 343 |   Mandatory : ArgumentName -> CGType -> CGArg
 344 | 
 345 |   ||| An optional function argument together with its
 346 |   ||| default value if the argument is `undefined`.
 347 |   Optional  : ArgumentName -> CGType -> Default -> CGArg
 348 | 
 349 |   ||| A variadic function argument
 350 |   VarArg    : ArgumentName -> CGType -> CGArg
 351 | 
 352 | export
 353 | argName : CGArg -> ArgumentName
 354 | argName (Mandatory x _)  = x
 355 | argName (Optional x _ _) = x
 356 | argName (VarArg x _)     = x
 357 | 
 358 | export
 359 | argType : CGArg -> CGType
 360 | argType (Mandatory _ y)  = y
 361 | argType (Optional _ y _) = y
 362 | argType (VarArg _ y)     = y
 363 | 
 364 | export
 365 | isOptional : CGArg -> Bool
 366 | isOptional (Optional _ _ _) = True
 367 | isOptional _                = False
 368 | 
 369 | namespace CGArg
 370 | 
 371 |   ||| True, if the given FFI type has a `SafeCast` instance
 372 |   export
 373 |   safeCast : CGArg -> Bool
 374 |   safeCast (Mandatory _ t)  = safeCast t
 375 |   safeCast (Optional _ t _) = safeCast t
 376 |   safeCast (VarArg _ _)     = False
 377 | 
 378 |   ||| True, if the given argument type is the same in the API and
 379 |   ||| the FFI.
 380 |   export
 381 |   sameType : CGArg -> Bool
 382 |   sameType (Mandatory _ t)  = sameArgType t
 383 |   sameType (Optional _ _ _) = False
 384 |   sameType (VarArg _ _)     = False
 385 | 
 386 |   export
 387 |   inheritance : CGArg -> Maybe (Identifier,Wrapper)
 388 |   inheritance (Mandatory _ t)  = inheritance t
 389 |   inheritance (Optional _ t _) = map opt <$> inheritance t
 390 |   inheritance (VarArg _ _)     = Nothing
 391 | 
 392 | public export
 393 | Args : Type
 394 | Args = List CGArg
 395 | 
 396 | --------------------------------------------------------------------------------
 397 | --          Functions
 398 | --------------------------------------------------------------------------------
 399 | 
 400 | ||| A function, for which we will generate some code.
 401 | public export
 402 | data CGFunction : Type where
 403 |   ||| A read-write attribute
 404 |   Attribute :
 405 |        (name : AttributeName)
 406 |     -> (obj  : Kind)
 407 |     -> (tpe  : CGArg)
 408 |     -> (ret  : ReturnType)
 409 |     -> CGFunction
 410 | 
 411 |   ||| An attribute getter.
 412 |   AttributeGet :
 413 |        (name : AttributeName)
 414 |     -> (obj  : Kind)
 415 |     -> (tpe  : ReturnType)
 416 |     -> CGFunction
 417 | 
 418 |   ||| A static attribute setter.
 419 |   StaticAttributeSet :
 420 |        (name : AttributeName)
 421 |     -> (obj  : Kind)
 422 |     -> (tpe  : CGArg)
 423 |     -> CGFunction
 424 | 
 425 |   ||| A static attribute getter.
 426 |   StaticAttributeGet :
 427 |        (name : AttributeName)
 428 |     -> (obj  : Kind)
 429 |     -> (tpe  : ReturnType)
 430 |     -> CGFunction
 431 | 
 432 |   ||| An indexed getter.
 433 |   Getter : (obj : Kind) -> (index : CGArg) -> (tpe : ReturnType) -> CGFunction
 434 | 
 435 |   ||| An indexed setter.
 436 |   Setter : (obj : Kind) -> (index : CGArg) -> (value : CGArg) -> CGFunction
 437 | 
 438 |   ||| An interface constructor with (possibly) optional arguments.
 439 |   Constructor  :  (obj : Kind) -> (args : Args) -> CGFunction
 440 | 
 441 |   ||| An interface constructor with (possibly) optional arguments.
 442 |   DictConstructor : (obj : Kind) -> (args : Args) -> CGFunction
 443 | 
 444 |   ||| A regular function with (possibly) optional arguments.
 445 |   Regular :
 446 |        OperationName
 447 |     -> (obj : Kind)
 448 |     -> Args
 449 |     -> ReturnType
 450 |     -> CGFunction
 451 | 
 452 |   ||| A static function with (possibly) optional arguments.
 453 |   Static :
 454 |        OperationName
 455 |     -> (obj : Kind)
 456 |     -> Args
 457 |     -> ReturnType
 458 |     -> CGFunction
 459 | 
 460 | ||| This is used for sorting lists of functions to
 461 | ||| determine the order in which they appear
 462 | ||| in the generated code.
 463 | |||
 464 | ||| Attributes will come first, sorted by name,
 465 | ||| setters, getters, and unsetter grouped together in
 466 | ||| that order.
 467 | |||
 468 | ||| All other functions come later and will be sorted by name.
 469 | export
 470 | priority : CGFunction -> (Nat,String,Nat)
 471 | priority (DictConstructor n _)       = (0,value (ident n),0)
 472 | priority (Constructor n _)           = (0,value (ident n),0)
 473 | priority (StaticAttributeSet n _ _)  = (1,show n,1)
 474 | priority (StaticAttributeGet n _ _)  = (1,show n,0)
 475 | priority (Static n o _ _)            = (2,n.value ++ value (ident o),0)
 476 | priority (Getter _ _ _)              = (3,"",0)
 477 | priority (Setter _ _ _)              = (3,"",1)
 478 | priority (Attribute n _ _ _)         = (4,show n,0)
 479 | priority (AttributeGet n _ _)        = (4,show n,1)
 480 | priority (Regular n o _ _)           = (5,n.value ++ value (ident o),0)
 481 | 
 482 | --------------------------------------------------------------------------------
 483 | --          Inheritance
 484 | --------------------------------------------------------------------------------
 485 | 
 486 | ||| An external, un-parameterized Javascript type, represented
 487 | ||| by an identifier. Such a type comes with a parent
 488 | ||| type (given as an `inheritance` value in the spec)
 489 | ||| and a number of mixed in types.
 490 | |||
 491 | ||| The actual name of the type is not included, as the set
 492 | ||| of types is given in `Env` as a `SortedMap`.
 493 | public export
 494 | record JSType where
 495 |   constructor MkJSType
 496 |   parent : Maybe Identifier
 497 |   mixins : List Identifier
 498 | 
 499 | ||| The parent types and mixins of a type. This is
 500 | ||| used by the code generator to implement the
 501 | ||| `JS.Inheritance.JSType` instances.
 502 | public export
 503 | record Supertypes where
 504 |   constructor MkSupertypes
 505 |   parents : List Identifier
 506 |   mixins  : List Identifier
 507 | 
 508 | --------------------------------------------------------------------------------
 509 | --          Domain
 510 | --------------------------------------------------------------------------------
 511 | 
 512 | public export
 513 | record CGDict where
 514 |   constructor MkDict
 515 |   name      : Identifier
 516 |   super     : Supertypes
 517 |   functions : List CGFunction
 518 | 
 519 | public export
 520 | record CGIface where
 521 |   constructor MkIface
 522 |   name      : Identifier
 523 |   super     : Supertypes
 524 |   constants : List CGConst
 525 |   functions : List CGFunction
 526 | 
 527 | public export
 528 | record CGMixin where
 529 |   constructor MkMixin
 530 |   name      : Identifier
 531 |   constants : List CGConst
 532 |   functions : List CGFunction
 533 | 
 534 | public export
 535 | record CGCallback where
 536 |   constructor MkCallback
 537 |   name      : Identifier
 538 |   constants : List CGConst
 539 |   type      : ReturnType
 540 |   args      : Args
 541 | 
 542 | public export
 543 | record CGDomain where
 544 |   constructor MkDomain
 545 |   name      : String
 546 |   callbacks : List CGCallback
 547 |   dicts     : List CGDict
 548 |   enums     : List Enum
 549 |   ifaces    : List CGIface
 550 |   mixins    : List CGMixin
 551 | 
 552 | export
 553 | domainFunctions : CGDomain -> List CGFunction
 554 | domainFunctions d =
 555 |      (d.dicts  >>= functions)
 556 |   ++ (d.ifaces >>= functions)
 557 |   ++ (d.mixins >>= functions)
 558 | 
 559 | --------------------------------------------------------------------------------
 560 | --          Environment
 561 | --------------------------------------------------------------------------------
 562 | 
 563 | ||| Codegen environment.
 564 | |||
 565 | ||| This includes a mapping from identifiers to the kinds
 566 | ||| they represent, a mapping from identifiers to their
 567 | ||| inheritance relations (`jsTypes`) and a mapping of
 568 | ||| type aliases.
 569 | |||
 570 | ||| The `maxInheritance` constant is used when calculating a
 571 | ||| type's supertypes to avoid a potentially infinite loop.
 572 | public export
 573 | record Env where
 574 |   constructor MkEnv
 575 |   maxInheritance : Nat
 576 |   kinds          : SortedMap Identifier Kind
 577 |   jsTypes        : SortedMap Identifier JSType
 578 |   aliases        : SortedMap Identifier (IdlTypeF ExtAttributeList Kind)
 579 | 
 580 | --------------------------------------------------------------------------------
 581 | --          Codegen Errors
 582 | --------------------------------------------------------------------------------
 583 | 
 584 | public export
 585 | data CodegenErr : Type where
 586 |   AnyInUnion             : Domain -> CodegenErr
 587 |   CBInterfaceInvalidOps  : Domain -> Identifier -> Nat -> CodegenErr
 588 |   InvalidConstType       : Domain -> CodegenErr
 589 |   InvalidGetter          : Domain -> Identifier -> CodegenErr
 590 |   InvalidSetter          : Domain -> Identifier -> CodegenErr
 591 |   NullableAny            : Domain -> CodegenErr
 592 |   NullablePromise        : Domain -> CodegenErr
 593 |   PromiseInUnion         : Domain -> CodegenErr
 594 |   RegularOpWithoutName   : Domain -> Identifier -> CodegenErr
 595 |   UnresolvedAlias        : Domain -> Identifier -> CodegenErr
 596 | 
 597 | public export
 598 | Codegen : Type -> Type
 599 | Codegen = Either (List CodegenErr)
 600 |