idris2-webidl

KO | EN

gitlite — search

#python #java #python3 #arduino #golang #machine-learning #rust #html #flask #javascript #seismology #nodejs

★ 16 Open GitHub ↗

Parsers and (eventually) Idris code generator for WebIDL documents

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# [ WIP ] idris2-webidl: A Generator for Idris2 Web Bindings

Parsers and (eventually) Idris code generator for WebIDL documents

## Progress

- [x] WebIDL parser
  - [x] Parse WebIDL toplevel specs into a syntax tree
        (types can be found in the `Text.WebIDL.Types` submodules).
  - [x] Encode syntax trees back to valid WebIDL
  - [x] Property test for parsers and encoders
- [ ] Idris2 code generator
  - [ ] Foreign function implementations
    - [x] Attribute getters
    - [x] Attribute setters
    - [x] Regular function implementations
    - [x] Interface constructors
    - [x] Dictionary constructors
    - [x] Static functions
    - [x] Function to callback converters
    - [ ] Iterables
    - [ ] Namespace members
    - [x] Setters and Getters
    - [x] Stringifiers
    - [ ] Setlikes (no instance in spec)
    - [ ] Maplikes (no instance in spec)
  - [ ] API function implementations
    - [x] Attribute getters
    - [x] Attribute setters
    - [x] Optional attribute unsetters
    - [x] Optional attribute getters supporting a default return value
    - [x] Regular functions (no optional arguments or variadic argument)
    - [x] Functions with optional arguments
          (including a second version with the optional arguments
          missing)
    - [x] Functions with a variadic argument
    - [x] Function to callback converters
    - [x] Static functions
    - [ ] Iterables
    - [ ] Namespace members
    - [x] Setters and Getters
    - [x] Stringifiers
    - [ ] Setlikes (no instance in spec)
    - [ ] Maplikes (no instance in spec)
  - [x] Marshalling
    - [x] from enum types to `String` and back
    - [x] from `Maybe` to `Nullable` and back
    - [x] from `Union` to `NS I` (from `Data.SOP.NS`) and back
    - [x] from `UndefOr` to an appropriate Idris2 ADT
    - [x] from Idris2 functions to callback types

## Codegen Notes

### Transferring WebIDL types to Idris2 types

WebIDL types can be found in module `Text.WebIDL.Types.Type`.
Here is an summary about how these types are being mapped to
Idris2 types by the code generator. Eventually, the list below
will also give additional information about functionality
required from these bindings, but in a first step

* `Undefined`: This type actually has two Idris2 representations.
   As a function argument, it is mapped to an external
   `Undefined` Idris2 type. As an unwrapped return value, it
   is mapped to `()`.

* Integral types: These are mapped to the following types
  * `octet` : `Bits8`
  * `byte` : `Int8`
  * `unsigned short` : `Bits16`
  * `short` : `Int16`
  * `unsigned long` : `Bits32`
  * `long` : `Int32`
  * `unsigned long long` : `UInt64`
  * `long long` : `UInt64`

Up to 32-bit integers, these all implement the usual numeric
  interfaces (including `Data.Bits`). The 64-bit types are
  still lacking an API, as they are represented by `Number`
  in the backend and this doesn't support integer operations
  at this precision. Will have to do some reading on how these
  are handled elsewhere (for instance in PureScript).

* Floating point types: These are mapped to `Double` for
  simplicity. Not yet sure whether it is worth to treat `float`
  and `unrestricted float` differently.

* `bigint` : This is obviously mapped to `Integer`.

* `boolean` : This gets its own external `Boolean` type with
   marshalling functions from and to Idris2 `Bool`.

* String types: `DOMString` and `USVString` are ordinary Idris2
  strings, `ByteString` gets its own external type (API yet to be
  defined).

* Buffer related types: These are mapped to external types
  of the same name. APIs are yet to be defined.

* Nullable types: These get their own external type `Nullable`
  like in PureScript, with functionality to convert from
  and to `Maybe`.

* `Any`: This is mapped to `AnyPtr`.

* `Promise`: This is mapped to an external type of the same name.
  API yet to be defined (have a look at PureScript again).

* `Object`: This is mapped to an external type of the same name.
  The API should at least provide an `IO` function for returning an
  empty object.

* `Symbol`: This is mapped to an external type of the same name.
  API yet to be defined.

* `Record`: Again, this gets its own parameterized external type.
   API yet to be defined. In Idris2, it should be possible to
   make sure that the key parameter can only be `String`
   or `ByteString`.

* Union types : These are mapped to an external `Union` type
  parameterized by a list of types listing the choices.
  It should be straight forward to marshall from an n-ary sum
  (`Data.SOP.NS`) to a union type. Marshalling back requires some
  thinking, however.

* Callbacks : These get their own external types. We should, however,
  provide a way to for each callback type marshall from a corresponding
  Idris2 function to the callback (as in PureScript, these should be
  `IO` actions, as they create new objects in the backend). I'm not
  sure whether it will be necessary to marshall from a callback
  back to an Idris2 function.

* Enums: These are treated as `String` in FFI calls, but
  get their own Idris2 enum type with proper conversions
  from and to their `String` representation.

* Interfaces : These git their own external types. Their API is generated
  by this code generator from the idl specs.
  API yet to be defined.

* Dictionaries : These get their own external types. Their API is generated
  by this code generator from the idl specs. In addition, each dictionary
  should get one or two (if the dictionary has optional attributes)
  constructor.

* Mixins : These just get their own external types without any
  constructor.

* Constants : Right now, these are implemented as plain Idris2
  nullary functions. Eventually, I'd like define proper Idris2 types
  for these and define rules for the code generator, where to
  replace the primitive types by these Idris2 types. This is future work,
  however.

### Inheritance and Mixins

WebIDL specifies inheritance relations for interfaces and dictionaries.
The code generator generates implementations for a `JSType` interface,
listing a type's parent types and included mixins. The API supports
then safe upcasting from a type to one of its parent types or mixins.

Downcasting is trickier, as it requires a way to inspect the
type of a value at runtime. The web API should provide a `SafeCast` interface
for types, which can be checked at runtime. This includes
all Idris2 primitives, the external numeric types, `String`, `Object`,
`Symbol`, `Undefine`, `Boolean`, and all interfaces and dictionary types,
whose type can be inspected by traversing a value's prototype chain.

idris2-webidl

Explore Similar Repositories

Was this content helpful?

Recent Feedback

Download README