Random generation of UExps #1337
Conversation
ruiz-m
force-pushed
the
haz3l-properties2
branch
from
d3bd895 to
f8754df
Compare
|
@ruiz-m could you leave instructions in the README.md file for how to run the quickcheck tests ( |
|
Alright. I might need to work on adding some code to print the term |
| [ | ||
| ("Elaboration", Test_Elaboration.elaboration_tests), | ||
| ("Type Assignment", Test_TypeAssignment.type_assignment_tests), | ||
| ("Random tests", Test_TypeAssignment.random_tests), |
There was a problem hiding this comment.
We should still mark these as Type Assignment tests. What do you think about TypeAssignment.random or TypeAssignment.property_tests for the name. We still don't have a format for doing hierarchies of tests. Dot separated matching the module structure makes sense to me.
| let m = Test_Elaboration.mk_map(u); | ||
| let d = Elaborator.dhexp_of_uexp(m, u, false); | ||
| let ty = Elaborator.fixed_exp_typ(m, u); | ||
| let test = () => | ||
| Alcotest.check( | ||
| Alcotest.pass, | ||
| "Random expression", | ||
| unit, | ||
| TypeAssignment.property_test(ty, d, m) | ||
| ? unit : Alcotest.fail("Term: " ++ UExp.show(u)), | ||
| ); | ||
| test_case("Type assignment", `Quick, test); | ||
| }, | ||
| QCheck.Gen.generate(~n=10, pure_random_uexp), |
There was a problem hiding this comment.
I think we probably want each property to be it's own test as opposed to each generated value resulting in a new test. We could then mark the tests as Slow instead of Quick so we don't slow the test runs down. It's worth looking into https://github.com/c-cube/qcheck?tab=readme-ov-file#integration-within-alcotest to see if we can go straight from the qcheck runner to alcotest.
There was a problem hiding this comment.
It's also worth doing something on the assertion to be closer to the equality we want to test so the error messages are better. We can probably do better but this is something:
let testable_typ = testable(Fmt.using(Typ.pretty_print, Fmt.string), Typ.eq);
//Generate purely random uexp test cases for alcotest
let random_tests =
List.map(
(u: UExp.t) => {
print_endline("Term: " ++ UExp.show(u));
let m: Statics.Map.t = Test_Elaboration.mk_map(u);
let d: option(DHExp.t) = Elaborator.dhexp_of_uexp(m, u, false);
let ty: option(Typ.t) = Elaborator.fixed_exp_typ(m, u);
let dhexp_typ =
Option.bind(d, TypeAssignment.typ_of_dhexp(Builtins.ctx_init, m));
let test = () =>
Alcotest.check(
Alcotest.option(testable_typ),
"Random expression: " ++ UExp.show(u),
dhexp_typ,
ty,
);
test_case("Type assignment", `Quick, test);
},
QCheck.Gen.generate(~n=10, pure_random_uexp),
);There was a problem hiding this comment.
Qcheck has first class support for generating long/short tests https://github.com/c-cube/qcheck?tab=readme-ov-file#long-tests
| let property_test = (uexp_typ: Typ.t, dhexp: DHExp.t, m: Statics.Map.t): bool => { | ||
| let dhexp_typ = typ_of_dhexp(Builtins.ctx_init, m, dhexp); | ||
| let property_test = | ||
| (uexp_typ: option(Typ.t), dhexp: option(DHExp.t), m: Statics.Map.t) | ||
| : bool => { | ||
| let dhexp_typ = | ||
| switch (dhexp) { | ||
| | None => None | ||
| | Some(dhexp) => typ_of_dhexp(Builtins.ctx_init, m, dhexp) | ||
| }; | ||
|
|
||
| switch (dhexp_typ) { | ||
| | None => false | ||
| | Some(dh_typ) => Typ.eq(dh_typ, uexp_typ) | ||
| switch (uexp_typ, dhexp_typ) { | ||
| | (None, None) => true | ||
| | (Some(uexp_typ), Some(dhexp_typ)) => Typ.eq(dhexp_typ, uexp_typ) | ||
| | _ => false | ||
| }; | ||
| }; |
There was a problem hiding this comment.
We should move this to the test file.
There was a problem hiding this comment.
Up to you but the property can also be written as:
let property_test =
(uexp_typ: option(Typ.t), dhexp: option(DHExp.t), m: Statics.Map.t)
: bool => {
let dhexp_typ = Option.bind(dhexp, typ_of_dhexp(Builtins.ctx_init, m))
Option.equal(Typ.eq, uexp_typ, dhexp_typ);
};
| ); | ||
|
|
||
| //Generates a UExp with no regard to the typing rules | ||
| let pure_random_uexp: QCheck.Gen.t(UExp.t) = |
There was a problem hiding this comment.
We should try to build a full arbitrary instance for the types so we can add printers/shrinking functions in the future like https://github.com/c-cube/qcheck?tab=readme-ov-file#mirrors-and-trees
There was a problem hiding this comment.
I feel like we should be able to use the ppx https://github.com/c-cube/qcheck/tree/main/src/ppx_deriving_qcheck for at least the simple variants.
There was a problem hiding this comment.
@ruiz-m just an fyi that I hit this bug when doing some of my own testing c-cube/qcheck#269 (comment). So be wary if you're trying to use deriving for recursive types.
|
We need to make sure that we're outputting the random seed for any failing tests before merging so that we can reproduce test failures locally. It would be terrible if the tests fail on CI and we can never reproduce them. I would assume using the native integration between qcheck and alcotest would do this but we need to confirm. |
|
@7h3kk1d Thank you for the feedback. It might take me some time to work on these fixes, but I will do them |
Feel free to let me know if there's any particular way I can help. |
Random generation of UExp for property-based testing.
The QCheck library was used to perform random generation of values.
The Alcotest library was used for unit testing.
The purely random generation of uexps will reveal some bugs.