coq-community / coqffi

Automatically generates Coq FFI bindings to OCaml libraries [maintainer=@lthms]
https://coq-community.org/coqffi/
MIT License
35 stars 8 forks source link

Support higher-order primitives in the Lwt feature #64

Closed lthms closed 3 years ago

lthms commented 3 years ago

With this patch, we greatly improve the support for Lwt by dealing with so-called higher-order primitives, where the [Lwt.t] type was not only appearing as the head position of the return type (e.g. ['a Lwt.t]), but also elsewhere (for instance, in one of its arguments).

Previously, only the head [Lwt.t] of the return type was generalize in the typeclass, so for instance, [bind] would have been translated as follows:

Lwt.t a -> (a -> Lwt.t b) -> m a

With this patch, the other [Lwt.t] are also generalized

m a -> (a -> m b) -> m a

To implement that, I had to modify how the primitive monadification was handle. In particular, this lead to the introduction of the notion of [Placeholder] that can be injected and later filled.

Finally, this patch paves the road towards supporting higher-order primitives in synchronous interfaces too.

Fixes #63