Developer notes

Translating from Coq into OCaml

Coq lets us fine tune the extraction process, as per Chapter 23 of the Coq’s manual. We can override the translation of an inductive type by supplying the target type and the target constructors. For instance, the following excerpt converts Coq’s bool type into OCaml’s bool.

Extract Inductive bool => "bool" [ "true" "false" ].

The keyword Inlined Constant lets us override the translation of a Coq definition by supplying an existing target definition. As an example, Coq’s negb can be translated into OCaml’s not with the code below.

Extract Inlined Constant negb => "not".

After setting up the translation overrides, we can initiate code generation. The code listing creates a file ocaml/cg.ml (relative to the working path of coqc) that consists of the translation of all definitions listed in the statement, along with any indirect dependency.

Extraction "ocaml/cg.ml"
  build (* graph generation *)
  Phaser.reduces_trace (* given a trace produce a state *)
  Phaser.reduces_dec (* performs a reduction step *)
  PhaseOrdering.Phaser.hb_dec (* checks if phaser p1 happens-before p2 *)
  WellFormed.Phaser.well_formed_dec (* checks if phaser is well-formed *)
  Phaser.well_ordered_dec (* checks if phaser is well-ordered *)
  Phaser.par_dec (* checks if p1 is concurrent with p2 *).

Translating from OCaml into JavaScript

Our goal is to expose the generated module ocaml/cg.ml as a JavaScript library. We achieve this with js_of_ocaml. However, the JavaScript code that js_of_ocaml generates cannot be invoked directly by external JavaScript code. We need to write some serialization code and specify which OCaml functions to expose as JavaScript functions.

Generated JavaScript data structures can be manipualated by the user as opaque data, but the generated data types are unintuitive. In order to help the user understand and debug its application code, we provide serialization to idiomatic JavaScript data structures.

We serialize enumerated types as strings, as is the case of registration modes.

let _REG = "reg"
let _SO = "SO"
let _WO = "WO"
let _SW = "SW"

let reg_of_string s : Cg.regmode =
    let s = trim s in
    if s = _WO then Cg.WAIT_ONLY
    else if s = _SO then Cg.SIGNAL_ONLY
    else if s = _SW then Cg.SIGNAL_WAIT
    else raise (Failure "reg_of_string")

let string_of_reg r =
    match r with
    | Cg.SIGNAL_ONLY -> _SO
    | Cg.SIGNAL_WAIT -> _SW
    | Cg.WAIT_ONLY -> _WO

We serialize an OCaml record as a JavaScript object with function Js.Unsafe.obj fields, where fields is an array that pairs field names (of type string) and field value (abstracted away as type Js.Unsafe.any with function Js.Unsafe.inject). Function Js.string converts an OCaml string into a JavaScript string.

let taskview_to_js (v:Cg.taskview) =
    Js.Unsafe.obj [|
        ("wp", Cg.wait_phase v |> Js.Unsafe.inject);
        ("sp", Cg.signal_phase v |> Js.Unsafe.inject);
        ("mode", Cg.mode v |> string_of_reg |> Js.string |> Js.Unsafe.inject)
    |]

When deserializing a record from a JavaScript object we load a field name with the ## — this operator is a js_of_ocaml syntactic extension. Nonsurpringly, function Js.to_string converts a JavaScript string into an OCaml string.

let js_to_taskview j : Cg.taskview =
    {
        Cg.wait_phase = j##wp;
        Cg.signal_phase = j##sp;
        Cg.mode = j##mode |> Js.to_string |> reg_of_string;
    }

Finally, we create an object that exposes the public-facing interface of our library. The global environment that is JavaScript-visible is an object that can be manipulated with Js.Unsafe.global. Here, we assign our library-object to variabel hj. This object includes a field for each of the functions we want to expose, akin to an OCaml module. OCaml functions become available to JavaScript with Js.wrap_callback. The code inside each wrapped function just deserializes the parameters from JavaScript into the data types generated by Coq.

let _ = 
    (* ... other functions ... *)
    let wo = Js.wrap_callback (fun x ->
        Cg.well_ordered_dec (js_to_phaser x) |> js_of_bool
    ) in
    Js.Unsafe.global##hj <-
        (* assign the API object *)
        Js.Unsafe.obj [|
            ("run_trace", Js.Unsafe.inject run_trace);
            ("graph", Js.Unsafe.inject build_cg);
            ("run", Js.Unsafe.inject run);
            ("hb", Js.Unsafe.inject hb);
            ("par", Js.Unsafe.inject par);
            ("wf", Js.Unsafe.inject wf);
            ("wo", Js.Unsafe.inject wo);
        |]

Setting up the project

To compile our project we use ocamlbuild. We follow example 3 of the manual.

There are three files that require setting up to use js_of_ocaml: _tags, Makefile, and myocamlbuild.ml. First, we edit file _tags where we declare that module main depends on js_of_ocaml. Package js_of_ocaml is mandatory. Package js_of_ocaml.syntax and syntax extension camlp4o are necessary for the JavaScript method syntax, which is used when serializing to and from JavaScript objects.

<main.*>: package(js_of_ocaml.syntax),package(js_of_ocaml),syntax(camlp4o)

Next, we edit the variable declaration of OCB_FLAGS of our Makefile to add support for a js_of_ocaml plugin.

OCB_FLAGS = -use-ocamlfind -I . -plugin-tag "package(js_of_ocaml.ocamlbuild)"

Finally, we create the plugin file myocamlbuild.ml with these contents:

let _ = Ocamlbuild_plugin.dispatch Ocamlbuild_js_of_ocaml.dispatcher