OCaml core

coq-of-ocaml translates the functional core of OCaml to the corresponding Coq constructs. It adds type annotations for each definition. We present how this translation work.

Functions

The OCaml functions are translated to standard Coq functions. For example, the definition of the composition function in OCaml:

let compose g f x =
  g (f x)

produces in Coq:

Definition compose {A B C : Set} (g : A -> B) (f : C -> A) (x : C) : B :=
  g (f x).

The polymorphic variables A, B and C are written explicitly as there are no polymorphic type inference in Coq (it is unclear if type variables should be in Set, Type or Prop for example). These polymorphic variables are set implicit with {...} so that they are inferred when doing function application:

let incr n = n + 1

let plus_two = compose incr incr

is translated to:

Definition incr (n : Z) : Z := Z.add n 1.

Definition plus_two : Z -> Z := compose incr incr.

All the generated types are in Set. You may need to use the -impredicative-set option of Coq to allow complex cases of polymorphism. An alternative is to replace all the generated occurrences of Set by Type. However, this may expose you to universe inconsistencies in proofs.

Pattern-matching

The pattern-matching is handled in Coq. The main difference is that constructors are curryfied:

type 'a sequence =
  | Empty
  | Cons of 'a * 'a sequence

let rec sum s =
  match s with
  | Empty -> 0
  | Cons (n, s') -> n + sum s'

generates:

Inductive sequence (a : Set) : Set :=
| Empty : sequence a
| Cons : a -> sequence a -> sequence a.

Arguments Empty {_}.
Arguments Cons {_}.

Fixpoint sum (s : sequence Z) : Z :=
  match s with
  | Empty => 0
  | Cons n s' => Z.add n (sum s')
  end.

The when clauses on patterns are encoded with a tuple of matches:

let rec sum s =
  match s with
  | Empty -> 0
  | Cons (n, _) when n < 0 -> sum s'
  | Cons (n, s') -> n + sum s'

generates:

Fixpoint sum (s : sequence Z) : Z :=
  match
    (s,
      match s with
      | Cons n s' => OCaml.Stdlib.lt n 0
      | _ => false
      end) with
  | (Empty, _) => 0
  | (Cons n s', true) => sum s'
  | (Cons n s', _) => Z.add n (sum s')
  end.

Records

Coq is more restrictive on the naming of record fields than OCaml. Two different records cannot share a common field name.

type answer = {
  code : int;
  message : string }

generates:

Module answer.
  Record record := {
    code : Z;
    message : string }.
  Definition with_code (r : record) code : record :=
    {| code := code; message := message r |}.
  Definition with_message (r : record) message : record :=
    {| code := code r; message := message |}.
End answer.
Definition answer := answer.record.

Records in Coq are automatically namespaced into a module of the same name. This prevents name collisions between record fields. As Coq has no builtin constructs for substitution in records, coq-of-ocaml generates a with_ function for each of the fields.

To read into the record, the generated code prefixes all the fields by the record's name:

let get_answer_message answer =
  answer.message

generates:

Definition get_answer_message (answer : answer) : string :=
  answer.(answer.message).

Patterns on records are also translated:

let get_answer_code = function
  { code } -> code

generates:

Definition get_answer_code (function_parameter : answer) : Z :=
  let '{| answer.code := code |} := function_parameter in
  code.

Recursive definitions

In Coq all functions must be proven terminating. We disable the termination checks for now by using the TypingFlags plugin (this feature should be included in the upcoming Coq 8.11 release). At the start of every generated files, coq-of-ocaml unset the termination flag:

Require Import TypingFlags.Loader.
Unset Guard Checking.

Unsetting the termination also remove the strict positivity checks for the definition of inductive types. We will probably add an option to re-activate the termination check when possible.

Monadic notations

The OCaml language provides a way to define monadic operators so that we can define programs such as:

let return (x : 'a) : 'a option =
  Some x

let (let*) (x : 'a option) (f : 'a -> 'b option) : 'b option =
  match x with
  | Some x -> f x
  | None -> None

let get_head l =
  match l with
  | [] -> None
  | x :: _ -> Some x

let sum_first_elements l1 l2 =
  let* x1 = get_head l1 in
  let* (x2, x3) = get_head l2 in
  return (x1 + x2 + x3)

We translate the program using similar let-notations in Coq. We require the user to manually insert these notations. For example, here coq-of-ocaml generates:

Definition _return {a : Set} (x : a) : option a := Some x.

Definition op_letstar {a b : Set} (x : option a) (f : a -> option b)
  : option b :=
  match x with
  | Some x => f x
  | None => None
  end.

Definition get_head {A : Set} (l : list A) : option A :=
  match l with
  | [] => None
  | cons x _ => Some x
  end.

Definition sum_first_elements (l1 : list int) (l2 : list (int * int))
  : option int :=
  let* x1 := get_head l1 in
  let* '(x2, x3) := get_head l2 in
  _return (Z.add (Z.add x1 x2) x3).

By adding the following notations in the generated code:

Notation "'let*' x ':=' X 'in' Y" :=
  (op_letstar X (fun x => Y))
  (at level 200, x ident, X at level 100, Y at level 200).

Notation "'let*' ' x ':=' X 'in' Y" :=
  (op_letstar X (fun x => Y))
  (at level 200, x pattern, X at level 100, Y at level 200).

the function get_head compiles. Note that coq-of-ocaml does not generate these notations, and you have to add them by hand.