This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)
        | Unused (* the value is not used at all *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)
        | Unused (* the value is not used at all *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)
        | Unused (* the value is not used at all *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.