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