# 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 tlet 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 environmenta : Setkind : tx : aThe term "x" has type "a" while it is expected to have type "Z".``

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_listtype '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) -> wrap1type wrap2 =  | Cw2 : ('a -> 'a) -> wrap2let 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)).``

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

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 land[@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)  endwhere "'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)  endwith 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 environmentdouble_list : list int -> list intdouble : int -> intl : list intn : intl0 : list intRecursive 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 listlet rec sum (t : int tree) =  match t with  | Leaf n -> n  | Node ts -> sums tsand[@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  endwhere "'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 = inttype even = Evenlet 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 : tendmodule M = struct  type t = int  let v = 12end``

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 : tendmodule[@coq_plain_module] M = struct  type t = int  let v = 12end``

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 * tend[@@coq_precise_signature]module type Sig2 = sig  type t  val f : t -> t listend[@@coq_precise_signature]module M1 : Sig1 = struct  type t = int  let f n m = (n, m)endmodule 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 = intIt is unclear which name this signature has. At least two similarsignatures found, namely:* Sig1* Sig2We 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`.

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.