Wrapping OCAML

How to wrap OCaml modules in F*

Brian Milnes

=========================================================

The basics

As our primary back end is OCaml, the compiler and our libraries call into OCaml code and wrap that those libraries types, values and functions.

You can work on your wrapping either in a F*orge makefile or inside the F* compiler and libraries. As working outside the compile is simplest, we'll start with that and show you how to put them into the F* system when done.

Setting up in F*orge

Create a project directory, in this case we are going just to run the WrapOcaml.{fsti,mli,ml} files with a Main.

See the ForgeManual.md for more details as needed.

Create the Makefile as below to compile both F* code and OCaml code.

FSTAR_SWITCH=opam 
BUILD_FSTAR=1
BUILD_FSTAR_OCAML=1
LINK_FSTAR.EXE_OCAML_EXTRA_LIBS=$(OPAM_HOME)/ocaml/unix.cmxa
FORGE_HOME=$(HOME)/Forge/package
include $(FORGE_HOME)/Makefile

Create an FStar.X.fsti in src/fstar/fst and an FStar_X.mli and FStar_X.ml in src/fstar/ml.

We have created a WrapOCaml.{fsti,mli,ml} here:

• Wrapping OCaml WrapOCaml.mli
• Wrapping OCaml Main.fst
• Wrapping OCaml WrapOCaml.ml
• Wrapping OCaml WrapOCaml.fsti

The wrapping method

Your WrapOCaml.fsti is going to define how F* calls WrapOCaml.ml and your WrapOCaml.mli is going to help you keep track of the types. As you wrap F* in OCaml the types are going to be cut out of the OCaml module you are wrapping ml, so the mli, which is not often done in the F* system is very useful.

When one wraps inside the system the modules are name FStar.X.fsti and FStar_X.mli and FStar_X.ml. There are a large number of wrappers built into F* such which you can reference both inside the sytem and outside the system through the fstar lib.

• ./FStar/lib/fstar/lib/FStar_IO.ml
• ./FStar/lib/fstar/lib/FStar_List.ml

Each type used in WrapOCaml.fsti is going to have to have a direct correspondence with its matching use in FStar_Unix.fsti.

The types that match directly are at least:

• F* unit to OCaml unit.

• F* bool to OCaml bool.

• F* float to OCaml float -- although we have almost no float support.

• F* string to OCaml string.

• F* option 'a to OCaml 'a option.

• F* list 'a to OCaml 'a list.

• F* int64 to OCaml int64.

• F* byte to OCaml byte.

• F* records over these types map to OCaml.

• These base types wrap simply:

   val bool_to_bool       : bool -> bool
   val float_to_float     : float -> float  (* Ya can't get there from here. *)
   val byte_to_byte       : FStar_Bytes.byte -> FStar_Bytes.byte
   val char_to_char       : char -> char

• When your types convert nicely you simply define a wrapping function like this:

 let f = Module.f

Wrapping inductive types

You can simply use an inductive type if you've defined it in F* and your OCaml, but the more common case is you're wrapping an exception from OCaml into one in F*.

• For example:

type prime = | Three | Seven
let prime_to_prime (e: prime) : prime = e  

• Inductive types such as type enum = | One | Two can be wrapped simply though like this:

(*  Take an enum from another module and show its translation. *)

module Enum' = struct
 type enum = | One | Two 
end

type enum = | One | Two 

let of_enum (e : enum) : Enum'.enum =
  match e with
  | One -> Enum'.One
  | Two -> Enum'.Two

let to_enum (e : Enum'.enum) : enum =
  match e with
  | Enum'.One -> One
  | Enum'.Two -> Two

let enum_to_enum (e : enum) : enum = to_enum (of_enum e)

Integers

Integers are somewhat problematic. OCaml has a type int which is implemented as a twos complement 31 bit signed integer on 32 bit architectures and a 63 bit similar on 64 bit architectures. OCaml is using that extra high bit for boxing and garbage collection.

OCaml also has an arbitrarily sized integer package, Z, with the expected Z.t type.

OCaml has a full int64 which corresponds exactly to our Int64.

Our int is translated into Z.t the type of unbounded integers in OCaml on input. So you may have to wrap within using Z.to_int and Z.of_int.

OCaml Z.t on the output is translated into F* int.

All of the UIntN and IntN types can be easily mapped, although *Int128 has few operations on the F* side.

Characters and Strings

OCaml char is a byte of the 256 characters of the latin-1 character set. While FStar.Char is a primitive equality type represented internally by an unsigned 32-bit integer whose value is at most 0x110000. And now it has a UTF-8 character set Uchar.t.

At the moment, WrapOCaml sends over a UTF-8 code as an int and gets it back correctly. But if you wrap and unwrap it with Uchar.to/from_int it distorts.

On the OCaml side you can simply apply normal string operations and they translate nicely.

Bytes

Byte enter and exit OCaml as immutable strings. So you can get an F* bytes (byte array) as a string and make a mutable bytes, operate on it, and then return it as an immutable data structure, i.e., as a string.

let bytes_to_bytes (b : FStar_Bytes.bytes) : FStar_Bytes.bytes   = 
  let len = String.length b in
  let bs  = Bytes.of_string b in
   Bytes.set bs 0 'H';
   Bytes.set bs 1 'I';
   Bytes.to_string bs

Exceptions

Exceptions also do not directly correspond. You can wrap them with functions to translate them but you can't type the functions. Neither FStar nor OCaml seem to have a type for all exceptions. This is probably because it's an extensible type in which new elements can be added.

Installing your wrapper in ulib.

If you're building a new FStar.X.fst* module, it goes in ulib.

The system sources seem to require two copies so far as I can tell. Place your OCaml for FStar_X in:

• ./FStar/ocaml/fstar-lib/FStar_X.ml
• ./FStar/lib/fstar/lib/FStar_X.ml

make build-and-verify-ulib will check it but a make bootstrap will cleanly build the changes for you.

Working inside the F* system

See the wiki for information on how to configure your F*orge and Emacs to allow compilation matching F*'s interior build outside and how to be able to run F* emacs mode on compiler sources.