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