Skip to main content

Module system

To handle the module system of OCaml, the compiler coq-of-ocaml generates either plain Coq modules or dependent records. It never generates Coq functors or module types. You can use coq-of-ocaml to translate modules, module types, functors and first-class modules.

General mechanism​

Example​

The following code:

module MyModuleForNamespacing = struct
  let foo x = x + 1
  let bar = 12
end

module type COMPARABLE = sig
  type t
  val compare : t -> t -> int
end

module InstanceToUseInFunctors = struct
  type t = string
  let compare = String.compare
end

is translated to:

Module MyModuleForNamespacing.
  Definition foo (x : Z) : Z := Z.add x 1.
  
  Definition bar : Z := 12.
End MyModuleForNamespacing.

Module COMPARABLE.
  Record signature {t : Set} := {
    t := t;
    compare : t -> t -> Z;
  }.
  Arguments signature : clear implicits.
End COMPARABLE.

Definition InstanceToUseInFunctors :=
  let t := string in
  let compare := Stdlib.String.compare in
  existT (fun _ => _) tt
    {|
      COMPARABLE.compare := compare
    |}.

We use a plain module for MyModuleForNamespacing as we think it will not be used in functors or first-class modules. We translate the module type COMPARABLE to a record parametrized by t as this type is abstract. The InstanceToUseInFunctors is translated to a dependent record of type COMPARABLE.signature as it may by used as a parameter for a functor for example. We will see how we determine that a module should translates to a record.

Finding names​

The heuristic is to represent a module by a dependent record if and only if it has a named signature. The name of the signature is then the name of the record type. Each signature is translated to a record type.

The OCaml modules are structurally typed while the Coq records are nominally typed. Thus a large part of the conversion effort is dedicated to the naming of signatures. A signature is named by exploring the environment to find a similar signature definition with its name. Two signatures are deemed similar if they share the same list of names of values and sub-modules at top-level. We do not check for type names or values as they could be removed or changed by the use of type substitutions (operators with type t = ... and with type t := ...). We only check top-level names for efficiency reasons, and because exploring sub-modules resulted in errors in some cases.

We generate an error message when multiple names are found for a signature. For example with:

module type S1 = sig
  val v : string
end

module type S2 = sig
  val v : int
end

module M = struct
  let v = "hi"
end

the module M could have the signatures S1 or S2 as we only look at the value names, so we output the error:

   7 | end
   8 | 
>  9 | module M = struct
  10 |   let v = "hi"
  11 | end
  12 | 


It is unclear which name has this signature. At least two similar
signatures found, namely:
S2, S1

We were looking for a module signature name for the following shape:
[ v ]
(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.

To discriminate between two similar signatures, you can add a dummy tag field. With:

module type S1 = sig
  val this_is_S1 : unit
  val v : string
end

module type S2 = sig
  val this_is_S2 : unit
  val v : int
end

module M = struct
  let this_is_S1 = ()
  let v = "hi"
end

coq-of-ocaml generates without errors:

Module S1.
  Record signature := {
    this_is_S1 : unit;
    v : string;
  }.
End S1.

Module S2.
  Record signature := {
    this_is_S2 : unit;
    v : Z;
  }.
End S2.

Definition M :=
  let this_is_S1 := tt in
  let v := "hi" in
  existT (fun _ => _) tt
    {|
      S1.this_is_S1 := this_is_S1;
      S1.v := v
    |}.

If no signatures are found, the module M is translated to a plain Coq module:

module type S = sig
  val v : string
end

module M = struct
  let not_v = "hi"
end

generates:

Module S.
  Record signature := {
    v : string;
  }.
End S.

Module M.
  Definition not_v : string := "hi".
End M.

Bundled vs unbundled​

In OCaml modules may have some abstract types. In Coq we represent abstract types as type parameters for the records of the signatures. For module values, we instantiate known abstract types and use existential types for unknown abstract types. We always use a single existential {... & ...} on the tuple of unknown types. If all types are known, we still use an existential on the empty tuple for uniformity.

We say that:

  • signatures are always unbundled (with universal types);
  • module are always bundled (with existential types).

Signatures​

Signatures can contain a mix of:

  • abstract types (constant or polymorphic);
  • type definitions as synonyms;
  • values;
  • sub-modules.

A complex example is the following:

module type SubS = sig
  type t
  val v : t
  type size
  val n : size
end

module type S = sig
  type 'a t
  type int_t = int t
  val numbers : int_t
  module Sub : SubS with type t = int_t
  val n : Sub.size
end

which gets translated to:

Module SubS.
  Record signature {t size : Set} := {
    t := t;
    v : t;
    size := size;
    n : size;
  }.
  Arguments signature : clear implicits.
End SubS.

Module S.
  Record signature {t : Set -> Set} {Sub_size : Set} := {
    t := t;
    int_t := t Z;
    numbers : int_t;
    Sub : SubS.signature int_t Sub_size;
    n : Sub.(SubS.size);
  }.
  Arguments signature : clear implicits.
End S.

The signature SubS has two abstract types t and size. We define two synonym record fields t := t and size := size for uniform access.

The signature S is parametrized by its abstract type t and the abstract type Sub_size of its sub-module Sub. The abstract type t is polymorphic and of type Set -> Set. The type synonym int_t is defined as a synonym record field. The sub-module Sub is a field of the record S.signature and of type the record SubS.signature. Its type parameter t is instantiated by int_t. Note that sub-module values appear as unbundled records. This is the only case where module values are unbundled. We made this choice because the abstract types of the sub-module Sub may be instantiated later as in:

S with type Sub.size = int

Finally, a signature field such as n can refer to a type defined in the sub-module Sub.

Modules​

The modules with a named signature are represented as bundled dependent records. The abstract types are generally known at the moment of the definition, but may still be hidden by casting. For example, the following code:

module type Source = sig
  type t
  val x : t
end

module M_NoCast = struct
  type t = int
  let x = 12
end

module M_WithCast : Source = struct
  type t = int
  let x = 12
end

will generate:

Module Source.
  Record signature {t : Set} := {
    t := t;
    x : t;
  }.
  Arguments signature : clear implicits.
End Source.

Definition M_NoCast :=
  let t := Z in
  let x := 12 in
  existT (fun _ => _) tt
    {|
      Source.x := x
    |}.

Definition M_WithCast :=
  let t := Z in
  let x := 12 in
  existT _ _
    {|
      Source.x := x
    |}.

The module M_NoCast has no existential variables while the module M_WithCast has one due to the cast to the Source signature. This is visible in the use a _ to ask Coq to infer the value of this type, in place of a tt to represent the absence of existential variables.

Existential tuples​

In the presence of several existential variables we use tuples of types with primitive projections. Primitive projections help Coq to infer missing values in generated terms, so that we do not need to annotate too much module expressions. These tuples are a variant of the tuples of the standard library. We use the following notations:

[T1 * T2 * ... Tn] (* the type of a tuple *)
[v1, v2, ..., vn]  (* the value of tuple *)

A tuple of n values is encoded as n-1 nested tuples of two values.

Projections​

As modules are always bundled (unless in the case of sub-modules in signatures), we introduce a notation for the Coq projection projT2:

(|bundled_record|)

Thus projections from modules encoded as a record:

let x = M_WithCast.x

typically have this shape in Coq:

Definition x : (|M_WithCast|).(Source.t) := (|M_WithCast|).(Source.x).

We did not add a notation for doing both the projection and the field access, as this would mess up with the inference for implicit variables in polymorphic fields.

Include​

Includes, either in signatures or modules, are generally inlined. For example, with signatures:

module type COMPARABLE = sig
  type t
  val compare : t -> t -> int
end

module type S = sig
  include COMPARABLE
  val ( = ) : t -> t -> bool
  val ( <> ) : t -> t -> bool
  val ( < ) : t -> t -> bool
  val ( <= ) : t -> t -> bool
  val ( >= ) : t -> t -> bool
  val ( > ) : t -> t -> bool
  val equal : t -> t -> bool
  val max : t -> t -> t
  val min : t -> t -> t
end

generates:

Module COMPARABLE.
  Record signature {t : Set} := {
    t := t;
    compare : t -> t -> Z;
  }.
  Arguments signature : clear implicits.
End COMPARABLE.

Module S.
  Record signature {t : Set} := {
    t := t;
    compare : t -> t -> Z;
    op_eq : t -> t -> bool;
    op_ltgt : t -> t -> bool;
    op_lt : t -> t -> bool;
    op_lteq : t -> t -> bool;
    op_gteq : t -> t -> bool;
    op_gt : t -> t -> bool;
    equal : t -> t -> bool;
    max : t -> t -> t;
    min : t -> t -> t;
  }.
  Arguments signature : clear implicits.
End S.

Due to duplications, coq-of-ocaml may generate Coq terms which are larger than the corresponding OCaml code. If you want to keep a generated Coq without duplications, we recommend you to use sub-modules rather than includes.

Functors​

We represent functors as functions over bounded records. Here is the example of a functor declaration:

module Make (P : COMPARABLE) : (S with type t = P.t)

generating:

Parameter Make :
  forall (P : {t : _ & COMPARABLE.signature t}),
    {_ : unit & S.signature (|P|).(COMPARABLE.t)}.

We see that the return type of Make is a dependent type depending on the value of the field COMPARABLE.t of P. A functor may also return another functor.

Here is an example of functor definition and application:

module type Source = sig
  type t
  val x : t
end

module type Target = sig
  type t
  val y : t
end

module F (X : Source) : Target with type t = X.t = struct
  type t = X.t
  let y = X.x
end

module M : Source = struct
  type t = int
  let x = 12
end

module N = F (M)

generating:

Module Source.
  Record signature {t : Set} := {
    t := t;
    x : t;
  }.
  Arguments signature : clear implicits.
End Source.

Module Target.
  Record signature {t : Set} := {
    t := t;
    y : t;
  }.
  Arguments signature : clear implicits.
End Target.

Definition F :=
  fun (X : {t : _ & Source.signature t}) =>
    (let t := (|X|).(Source.t) in
    let y := (|X|).(Source.x) in
    existT (fun _ => _) tt
      {|
        Target.y := y
      |} : {_ : unit & Target.signature (|X|).(Source.t)}).

Definition M :=
  let t := Z in
  let x := 12 in
  existT _ _
    {|
      Source.x := x
    |}.

Definition N :=
  F
    (existT _ _
      {|
        Source.x := (|M|).(Source.x)
      |}).

Applications of functors are represented by standard function applications. We cast the module parameter to make sure he has the correct record type. We cast records by re-creating them with the right field names.

First-class modules​

First-class modules are modules which appear as values in OCaml. The encoding to dependent records provides a perfect way to represent them in Coq. Here is an example from the Tezos source code:

module type Boxed_set = sig
  type elt
  val elt_ty : elt comparable_ty
  module OPS : S.SET with type elt = elt
  val boxed : OPS.t
  val size : int
end

type 'elt set = (module Boxed_set with type elt = 'elt)

let set_mem
  : type elt. elt -> elt set -> bool
  = fun v (module Box) ->
    Box.OPS.mem v Box.boxed

generates:

Module Boxed_set.
  Record signature {elt OPS_t : Set} := {
    elt := elt;
    elt_ty : comparable_ty elt;
    OPS : S.SET.signature elt OPS_t;
    boxed : OPS.(S.SET.t);
    size : Z;
  }.
  Arguments signature : clear implicits.
End Boxed_set.

Definition set (elt : Set) := {OPS_t : _ & Boxed_set.signature elt OPS_t}.

Definition set_mem {elt : Set} (v : elt) (Box : set elt) : bool :=
  (|Box|).(Boxed_set.OPS).(S.SET.mem) v (|Box|).(Boxed_set.boxed).

Many things are happening here, but the main thing to know is that we do not need to represent the OCaml lifts "module to value" or "value to module" since dependent records are already values in Coq.