Restructure letrec tests, use expect tests by gasche · Pull Request #1937 · ocaml/ocaml

gasche · 2018-07-28T11:06:13Z

Before this PR, there was a test directory letrec-disallowed, containing examples that should be rejected statically by the recursive-value-checker, and a directory letrec that contains both examples that should be accepted by the recursive-value checker, and tests for the recursive compilation strategy.

After this PR, the tests are split between letrec-check which tests the static recursive-value-checker, and letrec-compilation that tests the compilation strategy. letrec-compilation is mostly the old letrec unchanged. letrec-check corresponds to letrec-disallowed plus letrec/allowed.ml, reordered to be grouped by language features (with both should-pass and should-not-pass in each file), and using expect tests.

While preparing this PR I realize that a new feature would be useful for expect tests: I would like to be able to write [%%expect normal], and have this accept any toplevel output that contains only feedback on declarations, no warnings nor errors. (cc @trefis @Octachron).

Consider for example:

module type S = sig               val y : float end;;
module type T = sig val x : float val y : float end;;
type t = T : (module S) -> t;;
[%%expect{|
module type S = sig val y : float end
module type T = sig val x : float val y : float end
type t = T : (module S) -> t
|}];;

let rec x = let module M = (val m) in T (module M)
and (m : (module T)) = (module (struct let x = 10.0 and y = 20.0 end) : T);;
[%%expect{|
Line 1, characters 12-50:
  let rec x = let module M = (val m) in T (module M)
              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This kind of expression is not allowed as right-hand side of `let rec'
|}];;

I would like to write instead:

module type S = sig               val y : float end;;
module type T = sig val x : float val y : float end;;
type t = T : (module S) -> t;;
[%%expect normal];;

let rec x = let module M = (val m) in T (module M)
and (m : (module T)) = (module (struct let x = 10.0 and y = 20.0 end) : T);;
[%%expect{|
Line 1, characters 12-50:
  let rec x = let module M = (val m) in T (module M)
              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This kind of expression is not allowed as right-hand side of `let rec'
|}];;

…ion tests

(no change entry needed)

v-gb · 2018-07-29T07:38:52Z

It's not entirely clear how to support this [%%expect normal] idea [1], but the original version of this expect test tool has a #verbose boolean directive for this purpose, which disables the printing of types/values (https://github.com/janestreet/toplevel_expect_test/blob/6a48060ae864df73eb2412214952a95d063df9be/src/main.ml#L111), so you could probably simply add the 4 relevant lines to your pull request.

[1] these extensions nodes are not attached to the declaration doing the printing, so it seems the tool would need to look ahead to see if it should silence the printing or not, but then it's not clear what to print/what corrections to generate on things like:

expr1;;
expr2;;
expr3;;
expr4;;
[%%expect normal]
[%%expect some-warning]
[%%expect normal]

gasche · 2018-07-29T08:19:18Z

My understanding is that [%%expect] talks about the toplevel behavior on the input since the last [%%expect] marker (or the beginning of the file), so your last example would not work: the first %%expect normal would be checked about the output of all the phrases (and fail if any of them emits a warning), and the second %%expect {| ... warning ... |} would always fail as it only observes an empty output.

Regarding the implementation, the difficulty comes from the fact that the expect-tool does not distinguish between the "normal" output of the toplevel and warnings/errors, due to a lack of abstraction in the Toploop API. There are many reasons why we want to improve the abstraction there (for example, to make the life of utop easier), so hopefully we could improve on that at some point, which would also make %%expect normal very easy to implement.

Thanks for pointing out #verbose; I suspect that it would be far from as convenient to use in practice, but maybe there would be a compromise approach: if we preprocess the toplevel phrases to detect the phrases whose following expectation is normal, then we can know at phrase-execution time whether we want verbose output or not.

Octachron · 2018-07-29T12:12:07Z

Differentiating the warning and error messages is definitely doable in expect_test itself (i.e. I have a relatively short prototype implementation). Nevertheless, I agree that it would be nice to add to the toplevel API a version of exec_phrase that redirect all outputs to differentiated formatters during the phrase execution .

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.

ghost · 2018-07-31T10:42:47Z

Another possibility would be to add a new construction to the language to display typing error. i.e. something like this:

# [%try_typing 42]
- (unit, string) error = Ok ()
# [%try_typing 1 + 'e']
- (unit, string) error = Error "This expression ..."

then we wouldn't even need two kind of expectation tests, i.e. normal inline expectation tests and toplevel expectation tests.

For instance the example above would be written this way:

module type S = sig               val y : float end
module type T = sig val x : float val y : float end
type t = T : (module S) -> t

let%test _ =
  print_error [%try_typing 
    let rec x = let module M = (val m) in T (module M)
    and (m : (module T)) = (module (struct let x = 10.0 and y = 20.0 end) : T)];
  [%expect{|
Line 1, characters 12-50:
  let rec x = let module M = (val m) in T (module M)
              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This kind of expression is not allowed as right-hand side of `let rec'
|}]

which would make it clearer what is being tested what is part of the test harness.

gasche · 2018-08-06T10:00:56Z

Would someone be willing to review this PR? It's just moving tests around and improving them.

trefis · 2018-08-06T10:29:28Z

I'm on it.

trefis

I only partially check the last commit: it's incredibly tedious to follow all the moves at the same time as the reordering.
But for the few things I looked for, any that disappeared from one place reappeared in another. So I'm just going to trust that you didn't drop any test of the floor while doing the moves.

The other two commits are obviously correct.

gasche · 2018-08-06T11:26:22Z

Thanks! Probabilistic reviewing is the future.

trefis · 2018-08-06T12:00:44Z

Either that or atomic commits :)

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.

gasche added the no-change-entry-needed label Jul 28, 2018

gasche force-pushed the letrec-tests branch 3 times, most recently from 2e535e9 to 14120e4 Compare July 28, 2018 15:07

gasche mentioned this pull request Jul 28, 2018

rec_check: remove the duplicate array_type_kind classifier, use Typeopt #1922

Merged

gasche force-pushed the letrec-tests branch from 14120e4 to 644b2a8 Compare July 29, 2018 07:23

gasche added 3 commits July 29, 2018 09:28

letrec testsuite: split tests between static-check tests and compilat…

a0210af

…ion tests

tests/letrec-check: convert most tests to expect-test

b0bb1b6

tests/letrec-check: order the basic tests by language features

644b2a8

(no change entry needed)

gasche mentioned this pull request Jul 30, 2018

New implementations of the static check for recursive definitions #1942

Merged

trefis approved these changes Aug 6, 2018

View reviewed changes

gasche merged commit f370748 into ocaml:trunk Aug 6, 2018

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Restructure letrec tests, use expect tests#1937

Restructure letrec tests, use expect tests#1937
gasche merged 3 commits intoocaml:trunkfrom
gasche:letrec-tests

gasche commented Jul 28, 2018

Uh oh!

v-gb commented Jul 29, 2018

Uh oh!

gasche commented Jul 29, 2018

Uh oh!

Octachron commented Jul 29, 2018

Uh oh!

ghost commented Jul 31, 2018

Uh oh!

gasche commented Aug 6, 2018

Uh oh!

trefis commented Aug 6, 2018

Uh oh!

trefis left a comment

Uh oh!

gasche commented Aug 6, 2018

Uh oh!

trefis commented Aug 6, 2018

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

gasche commented Jul 28, 2018

Uh oh!

v-gb commented Jul 29, 2018

Uh oh!

gasche commented Jul 29, 2018

Uh oh!

Octachron commented Jul 29, 2018

Uh oh!

ghost commented Jul 31, 2018

Uh oh!

gasche commented Aug 6, 2018

Uh oh!

trefis commented Aug 6, 2018

Uh oh!

trefis left a comment

Choose a reason for hiding this comment

Uh oh!

gasche commented Aug 6, 2018

Uh oh!

trefis commented Aug 6, 2018

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants