Skip to main content

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_grab_existentials​

When translating terms that mentions existential variables it might be necessary to make that existential variable explicit. To achieve this we use the [@coq_grab_existentials] attribute. Here is an example:

type wrap1 =
  | Cw1 : ('a -> 'b) -> wrap1

type wrap2 =
  | Cw2 : ('a -> 'a) -> wrap2

let w2_of_w1 (w : wrap2) : wrap1  =
  match [@coq_grab_existentials]w with
  | Cw2 f ->
    Cw1 (fun y -> f y)

Notice that the type of inj is 'a -> 'a for some existential variable 'a. Since coq-of-ocaml always generates fully anotated code, we need to explicitely name 'a in order to properly anotate the type of y in the body of Cw1. This gives us the following translation:

Inductive wrap1 : Set :=
| Cw1 : forall {a b : Set}, (a -> b) -> wrap1.

Inductive wrap2 : Set :=
| Cw2 : forall {a : Set}, (a -> a) -> wrap2.

Definition w2_of_w1 (w : wrap2) : wrap1 :=
  let 'Cw2 f := w in
  let 'existT _ __Cw2_'a f as exi :=
    existT (A := Set) (fun __Cw2_'a => __Cw2_'a -> __Cw2_'a) _ f
    return
      let fst := projT1 exi in
      let __Cw2_'a := fst in
      wrap1 in
  Cw1 (fun (y : __Cw2_'a) => f y).

In the coq side we use an existT to grab these existential variables. The key here is that this allows us to explicitely name 'a as __Cw2_'a.

The return clause is used to bind this new name in the return type of the term that is being built, in this example it wouldn't be necessary but we generate the same code for a simpler boilerplate.

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_tag_gadt​

We use this tag in order to generate GADTs with a closer semantics to OCaml. Using this tag we translate the following code:

type 'a term =
  | T_Int : int -> int term
  | T_String : string -> string term
  | T_Sum : int term * int term -> int term
[@@coq_tag_gadt]

to:

Inductive term : vtag -> Set :=
| T_Int : int -> term int_tag
| T_String : string -> term string_tag
| T_Sum : term int_tag -> term int_tag -> term int_tag.

To see its usefulness translating impossible branches without extra axioms check coq_tagged_match

coq_tagged_match​

With the coq_tag_gadt attribute we can translate OCaml code closer to its actual semantics. This allows us to translate pattern matches with impossible branches without the use of axioms. For example:

type 'a term =
  | Int : int -> int term
  | String : string -> string term
  | Sum : int term * int term -> int term
[@@coq_tag_gadt]

let rec get_int (e : int term) : int =
  match[@coq_tagged_match][@coq_match_with_default] e with
  | Int n -> n
  | Sum (e1, e2) -> get_int e1 + get_int e2
  | _ -> .

Will be translated to:

Inductive term : vtag -> Set :=
| Int : int -> term int_tag
| String : string -> term string_tag
| Sum : term int_tag -> term int_tag -> term int_tag.

Fixpoint get_int (e : term int_tag) : int :=
  match e in term t0 return t0 = int_tag -> int with
  | Int n => fun eq0 => ltac:(subst; exact n)
  | Sum e1 e2 =>
    fun eq0 => ltac:(subst; exact (Z.add (get_int e1) (get_int e2)))
  | _ => ltac:(discriminate)
  end eq_refl.

Notice that without the use of tags we would have the following code instead:

Inductive term : Set :=
| Int : int -> term
| String : string -> term
| Sum : expr -> expr -> term
| Pair : expr -> expr -> term.


Fixpoint get_int (e : term) : int :=
  match e with
  | Int n => n
  | Sum e1 e2 => Z.add (get_int e1) (get_int e2)
  | _ => unreachable_gadt_branch
  end.

As we can see this naive translation uses the unreachable_gadt_branch axiom.

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.