# 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_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.