Extracting OCaml modules with
When developing code with Imandra, we write our programs in
.ire (Imandra-reason) for Reason syntax.
Imandra is both a programming language and a logic, and as such it incorporates
arbitrary precision (integer and rational) arithmetic with their standard
mathematical semantics. This deviates from 'normal' OCaml in which
int is of
fixed precision, for example.
When using Imandra, this arbitrary precision semantics is used both for code
execution and reasoning. For example, during an Imandra session, integer
literals are parsed as values of the arbitrary precision
Z.t type, resp.,
rather than to standard (OCaml) machine integers.
Imandra also comes with its own prelude of functions that have been
As well as reasoning about them, you can execute your
directly with Imandra itself. However at some point you will probably want to
compile a verified module or group of modules into a larger program using an
OCaml toolchain (either the standard OCaml toolchain or Bucklescript). This is
imandra-extract fits in, allowing you to extract
imandra-extract binary comes bundled with your Imandra
let int_of_bit (a : bool) : Z.t = if a then 1 else 0 let rec int_of_bits (a : bool list) : Z.t = match a with |  -> 0 | a :: a' -> int_of_bit a + 2 * (int_of_bits a')
We can then use
imandra-extract on this file:
imandra-extract my_module.iml -o my_module.ml
This creates an
.ml file similar to the following:
(* generated by imandra-extract from "my_module.iml" *) open Imandra_prelude;; (* start generated code here *) #1 "test.iml" let int_of_bit (a : bool) = (if a then Z.of_string "1" else Z.of_string "0" : Z.t) #4 "test.iml" let rec int_of_bits (a : bool list) = (match a with |  -> Z.of_string "0" | a::a' -> (int_of_bit a) + ((Z.of_string "2") * (int_of_bits a')) : Z.t)
As you can see, the literals are wrapped with the appropriate
functions, and the
Imandra_prelude module has been opened (which is opened
implicitly when running Imandra).
As this is now just a regular
.ml program, it can be compiled alongside other
OCaml modules - you will however need to install the extracted
as a dependency in your project. View the project and README for
imandra-prelude on GitHub: https://github.com/aestheticIntegration/imandra-prelude.