Attributes

We present the attributes which we can use with coq-of-ocaml. See the attributes documentation of OCaml for general information about the attributes mechanism. Note that the OCaml attributes do not change the behavior of a program. There are there to help developer tools.

We prefix all the attributes of coq-of-ocaml by coq_. According to the OCaml syntax, depending on the context, you may use a single @ or a double @@.

coq_axiom_with_reason

When we cannot import the definition of a value, we can use the [@coq_axiom_with_reason] attribute to transform it to a Coq axiom. For example:

let[@coq_axiom_with_reason "mutable state"] function_hard_to_translate_to_coq =
  let n = ref 0 in
  fun () ->
    n := !n + 1;
    !n

is translated to:

Definition function_hard_to_translate_to_coq : unit -> Z := axiom.

Note that we must give a reason for the use of [@coq_axiom_with_reason] in a string parameter. We define the axiom value in the coq-of-ocaml's Coq library. The definition of axiom is:

Axiom axiom : forall {A : Set}, A.

coq_cast

With the attribute [@coq_cast] we can force the type in Coq of an arbitrary OCaml expression using the following axiom:

Axiom cast : forall {A : Set} (B : Set), A -> B.

For example, we translate:

type _ t =
  | Int : int t

let f (type a) (kind : a t) (x : a) : int =
  match kind with
  | Int -> (x[@coq_cast] : int) + 1

to:

Inductive t : Set :=
| Int : t.

Definition f {a : Set} (kind : t) (x : a) : int :=
  let 'Int := kind in
  Z.add (cast int x) 1.

Thanks to the cast axiom, we can get the information in Coq that x is of type int. Without this axiom the example would not work. Indeed, we do not track the type equations generated by the GADTs so x would be considered of type a. Without the cast, the Coq code:

Definition f {a : Set} (kind : t) (x : a) : int :=
  let 'Int := kind in
  Z.add x 1.

generates the error:

>   Z.add x 1.
>         ^
Error:
In environment
a : Set
kind : t
x : a
The term "x" has type "a" while it is expected to have type "Z".

coq_force_gadt

The [@coq_force_gadt] attribute forces a type definition to be considered as a GADT during the translation to Coq. In particular, it forces the translation to erase the type parameters. For example:

type 'a standard_list =
  | SNil
  | SCons of 'a * 'a standard_list

type 'a gadt_list =
  | GNil
  | GCons of 'a * 'a gadt_list
[@@coq_force_gadt]

generates:

Inductive standard_list (a : Set) : Set :=
| SNil : standard_list a
| SCons : a -> standard_list a -> standard_list a.

Arguments SNil {_}.
Arguments SCons {_}.

Inductive gadt_list : Set :=
| GNil : gadt_list
| GCons : forall {a : Set}, a -> gadt_list -> gadt_list.

One possible reason to force a type to be a GADT is to make sure that all the inductive types in a mutually recursive type definition have the same (zero) arity, as it is expected by Coq.

coq_implicit

The [@coq_implicit "(A := ...)"] attribute adds an arbitrary annotation on an OCaml identifier or constructor. We typically use this attribute to help Coq to infer implicit types where there is an ambiguity:

let forget x = ()

let u = forget []

generates the following Coq code:

Definition forget {A : Set} (x : A) : unit := tt.

Definition u : unit := forget nil.

which fails to compile due to the error:

> Definition u : unit := forget nil.
>                               ^^^
Error: Cannot infer the implicit parameter A of nil whose type is "Set".

Indeed, the type parameter of this empty list does not matter as it is dropped by the forget function. We can force it to an arbitrary value like unit:

let u = forget ([] [@coq_implicit "(A := unit)"])

so that the generated Coq code compiles:

Definition u : unit := forget (nil (A := unit)).

coq_match_gadt

The [@coq_match_gadt] attribute adds type annotations for the pattern variables in a match. We force the type annotations to be valid using axioms (dynamic casts). For example:

type 'a int_or_bool =
  | Int : int int_or_bool
  | Bool : bool int_or_bool

let to_int (type a) (kind : a int_or_bool) (x : a) : int =
  match[@coq_match_gadt] (kind, x) with
  | (Int, (x : int)) -> x
  | (Bool, (x : bool)) -> if x then 1 else 0

translates to:

Inductive int_or_bool : Set :=
| Int : int_or_bool
| Bool : int_or_bool.

Definition to_int {a : Set} (kind : int_or_bool) (x : a) : Z :=
  match (kind, x) with
  | (Int, _ as x) =>
    let x := cast Z x in
    x
  | (Bool, _ as x) =>
    let x := cast bool x in
    if x then
      1
    else
      0
  end.

The cast operator is a dynamic cast defined by:

Axiom cast : forall {A : Set} (B : Set), A -> B.

Note that without the [@coq_match_gadt] attribute this would generate:

Definition to_int {a : Set} (kind : int_or_bool) (x : a) : Z :=
  match (kind, x) with
  | (Int, _ as x) => x
  | (Bool, _ as x) =>
    if x then
      1
    else
      0
  end.

which is ill-typed in Coq.

coq_match_gadt_with_result

The attribute [@coq_match_gadt_with_result] is similar to [@coq_match_gadt] and also adds a cast for the result of each match branch. Here is an example where it is useful:

let incr_if_int (type a) (kind : a int_or_bool) (x : a) : a =
  match[@coq_match_gadt_with_result] (kind, x) with
  | (Int, (x : int)) -> x + 1
  | (Bool, (x : bool)) -> x 

generates in Coq:

Definition incr_if_int {a : Set} (kind : int_or_bool) (x : a) : a :=
  match (kind, x) with
  | (Int, _ as x) =>
    let x := cast Z x in
    cast a (Z.add x 1)
  | (Bool, _ as x) =>
    let x := cast bool x in
    cast a x
  end.

coq_match_with_default

The [@coq_match_with_default] adds a default branch for match which are syntactically incomplete. For example, when we annotate the following code:

let incr_int (kind_and_value : int int_or_bool * int) : int =
  match[@coq_match_with_default] kind_and_value with
  | (Int, x) -> x + 1

we generate the following valid Coq code:

Definition incr_int (kind_and_value : int_or_bool * Z) : Z :=
  match kind_and_value with
  | (Int, x) => Z.add x 1
  | _ => unreachable_gadt_branch
  end.

even if the match is syntactically incomplete due to the GADT's constraints. We define unreachable_gadt_branch as an axiom by:

Axiom unreachable_gadt_branch : forall {A : Set}, A.

We can combine this attribute with [@coq_match_gadt] or [@coq_match_gadt_with_result] if needed.

coq_mutual_as_notation

The attribute [@coq_mutual_as_notation] makes the definition of a mutually recursive function a notation. For example, we transform the following OCaml code:

let rec double_list l =
  match l with
  | [] -> l
  | n :: l -> double n :: double_list l

and[@coq_mutual_as_notation] double n = 2 * n

to:

Reserved Notation "'double".

Fixpoint double_list (l : list int) : list int :=
  let double := 'double in
  match l with
  | [] => l
  | cons n l => cons (double n) (double_list l)
  end

where "'double" := (fun (n : int) => Z.mul 2 n).

Definition double := 'double.

Without this attribute, we would generate a mutually recursive definition:

Fixpoint double_list (l : list int) : list int :=
  match l with
  | [] => l
  | cons n l => cons (double n) (double_list l)
  end

with double (n : int) : int := Z.mul 2 n.

which is rejected by the type-checker of Coq:

Error:
Recursive definition of double_list is ill-formed.
In environment
double_list : list int -> list int
double : int -> int
l : list int
n : int
l0 : list int
Recursive call to double has principal argument equal to 
"n" instead of "l0".
Recursive definition is:
"fun l : list int =>
 match l with
 | [] => l
 | n :: l0 => double n :: double_list l0
 end".

For recursive notations, you can combine this attribute with @coq_struct to tell coq-of-ocaml to generate a recursive notation. For example, we transform:

type 'a tree =
  | Leaf of 'a
  | Node of 'a tree list

let rec sum (t : int tree) =
  match t with
  | Leaf n -> n
  | Node ts -> sums ts

and[@coq_mutual_as_notation][@coq_struct "ts"] sums (ts : int tree list) =
  match ts with
  | [] -> 0
  | t :: ts -> sum t + sums ts

to:

Reserved Notation "'sums".

Fixpoint sum (t : tree int) : int :=
  let sums := 'sums in
  match t with
  | Leaf n => n
  | Node ts => sums ts
  end

where "'sums" :=
  (fix sums (ts : list (tree int)) {struct ts} : int :=
    match ts with
    | [] => 0
    | cons t ts => Z.add (sum t) (sums ts)
    end).

Definition sums := 'sums.

using the keyword fix for the defintion of sums. In this example too, the type-checker of Coq would reject the definition without a notation.

In the proofs, whenever the definition of sums appears unfolded, you can run the tactic fold sums to hide it.

coq_phantom

When it can, coq-of-ocaml detects phantom types and remove their type annotations. For example, we translate the following OCaml code:

type 'a num = int

type even = Even

let two : even num = 2

to:

Definition num : Set := Z.

Inductive even : Set :=
| Even : even.

Definition two : num := 2.

The reason is that phantom types may generate ambiguities during type inference in Coq.

The [@coq_phantom] attribute forces coq-of-ocaml to consider a type as phantom. This can be useful for abstract types in .mli files, since their definition is not reachable. For example:

type 'a num

translates to:

Parameter num : forall (a : Set), Set.

but:

type 'a num
[@@coq_phantom]

generates:

Parameter num : Set.

coq_plain_module

We may prefer to translate a module to a plain Coq module rather than a record. The [@coq_plain_module] attribute requires a module to be translated as a plain Coq module. For example:

module type T = sig
  type t

  val v : t
end

module M = struct
  type t = int

  let v = 12
end

translates to:

Module T.
  Record signature {t : Set} : Set := {
    t := t;
    v : t;
  }.
End T.

Definition M :=
  let t : Set := int in
  let v := 12 in
  existT (A := unit) (fun _ => _) tt
    {|
      T.v := v
    |}.

With the [@coq_plain_module] attribute we translate:

module type T = sig
  type t

  val v : t
end

module[@coq_plain_module] M = struct
  type t = int

  let v = 12
end

to:

Module T.
  Record signature {t : Set} : Set := {
    t := t;
    v : t;
  }.
End T.

Module M.
  Definition t : Set := int.
  
  Definition v : int := 12.
End M.

coq_precise_signature

In order to distinguish between two signatures with the same value names, we can add the [@coq_precise_signature] attribute. For example, we can translate:

module type Sig1 = sig
  type t

  val f : t -> t -> t * t
end
[@@coq_precise_signature]

module type Sig2 = sig
  type t

  val f : t -> t list
end
[@@coq_precise_signature]

module M1 : Sig1 = struct
  type t = int

  let f n m = (n, m)
end

module M2 : Sig2 = struct
  type t = int

  let f n = []
end

to:

Module Sig1.
  Record signature {t : Set} : Set := {
    t := t;
    f : t -> t -> t * t;
  }.
End Sig1.

Module Sig2.
  Record signature {t : Set} : Set := {
    t := t;
    f : t -> list t;
  }.
End Sig2.

Module M1.
  Definition t : Set := int.
  
  Definition f {A B : Set} (n : A) (m : B) : A * B := (n, m).
  
  Definition module :=
    existT (A := Set) _ t
      {|
        Sig1.f := f
      |}.
End M1.
Definition M1 := M1.module.

Module M2.
  Definition t : Set := int.
  
  Definition f {A B : Set} (n : A) : list B := nil.
  
  Definition module :=
    existT (A := Set) _ t
      {|
        Sig2.f := f
      |}.
End M2.
Definition M2 := M2.module.

Here we can distinguish between the signature Sig1 and Sig2 thanks to the type shape of f. Without this attribute, we would get the following error message:

--- tests/precise_signature.ml:13:1 ----------------------------------------------- module (1/2) ---

  11 | end
  12 | 
> 13 | module M1 : Sig1 = struct
> 14 |   type t = int
> 15 | 
> 16 |   let f n m = (n, m)
> 17 | end
  18 | 
  19 | module M2 : Sig2 = struct
  20 |   type t = int


It is unclear which name this signature has. At least two similar
signatures found, namely:

* Sig1
* Sig2

We were looking for a module signature name for the following shape:
[ f ]
(a shape is a list of names of values and sub-modules)

We use the concept of shape to find the name of a signature for Coq.

Indeed, by default, we only compare signatures based on the names of their fields. With the [@coq_precise_signature] we also use a heuristic to distinguish the types of the values.

coq_struct

For recursive definitions, we can force the name of the parameter on which we do structural recursion using the attribute [@coq_struct "name"]. This has the same effect as the {struct name} keyword in Coq. For example, we translate:

let[@coq_struct "accumulator"] rec length l accumulator =
  match l with
  | [] -> accumulator
  | _ :: l -> length l (accumulator + 1)

to:

Fixpoint length {A : Set} (l : list A) (accumulator : Z) {struct accumulator}
  : Z :=
  match l with
  | [] => accumulator
  | cons _ l => length l (Z.add accumulator 1)
  end.

which is invalid in Coq as the decreasing argument is l.

coq_type_annotation

Sometimes we need to add a type annotation on an expression, either as a documentation or to help the Coq code to compile. We translate this OCaml example:

let n1 =
  let m = 12 in
  let n1 = m[@coq_type_annotation] in
  n1

to:

Definition n1 : int :=
  let m := 12 in
  let n1 := (m : int) in
  n1.

where we add an annotation : int on the expression m. The type we use for the annotation is the type inferred by the OCaml compiler.