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
sumsappears unfolded, you can run the tacticfold sumsto 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.