OCaml to CakeML translator
Possibly translates type-correct OCaml files to equivalent CakeML files. Multi-file programs should be supported eventually, but aren't now.
./formatted <<< 'Some (OCaml code)'
will write the translation of
Some (OCaml code) to stdout. (
Some (OCaml code) will fail because
code are not defined.)
will write the translation of the contents of
myCode.ml prefixed with the contents of the files in
lib/. Currently, this gives translated programs access to translations of OCaml's
CAKE variable in
tests/Makefile to reflect the location of your CakeML interpreter. Then run:
cd tests make make test
Translation failures are shown in the output of
make, and begin with “Error:”. Errors from the CakeML interpreter are shown in the output of
make test, and look like either “” or “”. In the absence of these, “Success” will be printed. The full output of the interpreter is written to the relevant .out files. The binary file produced by
make is a byproduct of the OCaml compiler.
.cml files can be patched after translation. File
a.cml is fed to
boyer-patch (which uses
boyer-patch.sed) for an example. Current patches:
- boyer – avoid falling to the value restriction. The OCaml file has type annotations (e.g
ref ( : head list)), which can't be used in CakeML.
countGraphs currently fails due to trying to match against the pattern
Ok (newPacc, acc), where
Ok is a unary constructor and
(newPacc, acc) is supposed to be a tuple pattern. This is a known issue with CakeML, so fixing this doesn't seem necessary. boyer currently fails because I've botched the translation from SML (or maybe I've hit a problem with OCaml equality between references).