🐓 September 13, 2019
The coq-of-ocaml compiler transforms OCaml programs to Coq ones. There usually are many errors in each file to import (the Coq language tends to be stricter than OCaml and we do not want to import code with too much encoding). Fixing errors may be the most time consuming part of an import. We present a system to display all the errors at once instead of one by one. We believe that it helps to get a quick idea of how difficult a file is to translate, while having a sense of progress when fixing the errors.
We develop coq-of-ocaml at 🐙 Nomadic Labs with the aim to formally verify OCaml programs, and in particular the implementation of the crypto-currency Tezos. If you want to use this tool for your own projects, please do not hesitate to look at our website or contact us!
Take this perfectly valid OCaml program:
let foo x = if x then assert false (* no assert in Coq *) else begin print_endline "bar"; (* no sequencing of side-effects in Coq *) true end
We would like to report that both the
assert and the sequencing of effects with
; are not available in Coq.
To import programs,
coq-of-ocaml runs a single pass on the OCaml’s typed abstract syntax tree. During the recursive exploration of the syntax tree, we would like to explore both branches of the
if to report both errors. We need a way to accumulate errors along the way and not block at the first mistake. Since
coq-of-ocaml has a single pass, we hope to get most of the errors doing so.
To encapsulate the error handling mechanism, we define the following free monad in OCaml (
coq-of-ocaml is implemented in OCaml):
module Command = struct type 'a t = | GetEnv : Env.t t | Raise : Error.Category.t * string -> 'a t end module Wrapper = struct type t = | SetEnv of Env.t | SetLoc of Loc.t end type 'a t = | All : 'a t * 'b t -> ('a * 'b) t | Bind : 'b t * ('b -> 'a t) -> 'a t | Command of 'a Command.t | Return of 'a | Wrapper of Wrapper.t * 'a t
There are three main constructs to note:
Allwhich combines the results of two computations, both of which may fail. It allows to accumulate errors in each branch of the syntax tree;
Command, especially the case
Raiseto create an error at the current code location;
Wrapper, especially the case
SetLocto set the current code location in (and only in) the following computation.
We also have primitives
SetEnv to manipulate the current OCaml environment from the AST. The
Return are the standard monadic primitives. We chose a free-monad in order to isolate the definition of side-effects and, one day, import
coq-of-ocaml to Coq.
coq-of-ocaml using the
All primitive as much as possible (typically when two computations were not depending on each other). Since the current OCaml environment and location are handled by the monad, we cleaned the code to propagate their values. Having done that, retrieving the complete list of errors was mostly given for free.
In order to present a nice output to the user, we decided to do the following: