xls
xls copied to clipboard
[DSLX] quickcheck support for parametric functions
cc @hmontero1205
In #70 support for quickchecking non-parametric functions is introduced -- we'll want a way to let the quickcheck "driver" instantiate parametric functions with the ability to put constraints on the parametric values. One nice aspect of this is the quickcheck driver can use normal functions to test properties of normal values (e.g. filtering via is_even
as a predicate on a given parametric N: u32
) and then use that value to drive the instantiation. This will make the quickcheck less vectorizable, but we can vector-test some number of samples for any given parametric N
chosen to get some batch efficiency.
Not currently on the "implement soon" radar so marking as long-term enhancement.
It seems at least possible to quickcheck parametric function by instanciating them explicitly:
fn func1<N: u32>(a: uN[N], b: uN[N]) -> uN[N] {
a + b
}
fn func2<N: u32>(a: uN[N], b: uN[N]) -> uN[N] {
b + a
}
#[quickcheck(test_count=50000)]
fn prop_func1_equal_func2(a: u32, b: u32) -> bool {
func1<u32:32>(a, b) == func2<u32:32>(a, b)
}
[ RUN QUICKCHECK ] prop_func1_equal_func2 count: 50000
[ OK ] prop_func1_equal_func2