-
Notifications
You must be signed in to change notification settings - Fork 232
Compiler hacking: Calling an OCaml or F# library from the F* sources
First, recall that the compiler is programmed in the shared subset of F* and F#. So, the filename extensions we use in the compiler sources are .fs and fsi, for compatibility with F#. However, these files are also valid F* files.
We routinely call library functions from OCaml or F# from the F* sources. It's pretty straightforward, but involves a few steps.
A good example of this is the use of string buffers. See:
- Interface file, valid both in F* and F#: src/basic/boot/FStar.StringBuffer.fsi
- F# implementation src/basic/boot/FStar.StringBuffer.fs
- OCaml implementation src/basic/ml/FStar_StringBuffer.ml
- Create an interface file for the functionality you wish to call.
For instance, in FStar.StringBuffer.fsi is a pretty straightforward interface.
- Implement the interface in F# and OCaml
Note, the OCaml implementation has to anticipate the name-mangling the F* introduces on extraction. See FStar_StringBuffer.ml
- Building it:
- For the F# build, you need to add the .fsi and .fs to the suitable .fsproj file for the Visual Studio build
- For the OCaml build, add your new .fsi file to the ALL_BOOT variable in src/Makefile (around line 46). This is not always necessary, but it's a reasonable rule to follow. Depending on the way you named your file, you may need to add your module to the NOEXTRACT variable in src/Makefile.boot. Most common cases should not require this.
-
Now you should be able to just build as usual,
make -C src
for the F# build andmake boot
for the bootstrapping build. -
Now, elsewhere in the F* sources, you should just be able to call your newly added library as normal.
Note, if it's just a single small primitive it may be easier to add it to src/basic/boot/FStar.Util.fsi, to src/basic/boot/NotFStar.Util.fst (The F# implementation of this module) and to src/basic/ml/FStar_Util.ml (the OCaml implementation). These modules already aggregate many library functions and the build system is already aware of them. So, for small additions, extending FStar.Util is the way to go.