Formal API reference and preconditions

[fredrik-johansson]

One idea we've discussed in several contexts is to have an official tool to convert our API to machine-readable format for wrappers. We've also discussed having more documentation generated from the source code. We've also discussed the problem that many functions are under-specified.

Suppose we were to do something like this, where I've chosen a somewhat nontrivial function to illustrate:

int _gr_poly_divrem(gr_ptr Q, gr_srcptr R, gr_srcptr A, slong lenA, gr_srcptr B, slong lenB, gr_ctx_t ctx)
{
    slong lenQ = lenA - lenB + 1;    // simple helper variable declarations may precede preconditions
    slong lenR = lenB - 1;

    FLINT_REQUIRE(lenA >= lenB);
    FLINT_REQUIRE(lenB >= 1);

    FLINT_REQUIRE_VEC(Q, lenQ, ctx);
    FLINT_REQUIRE_VEC(R, lenR, ctx);
    FLINT_REQUIRE_VEC(A, lenA, ctx);
    FLINT_REQUIRE_VEC(B, lenB, ctx);

    FLINT_REQUIRE_VEC_NOALIAS(Q, lenQ, A, lenA, ctx);
    FLINT_REQUIRE_VEC_NOALIAS(Q, lenQ, B, lenB, ctx);
    FLINT_REQUIRE_VEC_NOALIAS(R, lenR, B, lenB, ctx);
    FLINT_REQUIRE_VEC_SAME_OR_NOALIAS(R, lenR, A, lenA, ctx);

    ...
}

Most obviously, we could turn REQUIRE macros into asserts when asserts are enabled.

I'm guessing it would be reasonably straightforward to write a tool that extracts function signatures and their subsequent REQUIRE statements and dumps them to an easily machine-readable file which in turn could be used by wrapper generators.

One could then also autogenerate human-readable specifications for the FLINT documentation. For the example, I guess the output would be something like this:

• lenA >= lenB
• lenB >= 1
• lenQ = lenA - lenB + 1
• lenR = lenB - 1
• Q is a pointer to an array of lenQ initialized elements of ctx
• R is a pointer to an array of lenR initialized elements of ctx
• A is a pointer to an array of lenA initialized elements of ctx
• B is a pointer to an array of lenB initialized elements of ctx
• {Q[0], ..., Q[lenQ-1]} and {A[0], ..., A[lenA - 1]} must not overlap in memory
• {Q[0], ..., Q[lenQ-1]} and {B[0], ..., B[lenB - 1]} must not overlap in memory
• {R[0], ..., R[lenR-1]} and {B[0], ..., B[lenB - 1]} must not overlap in memory
• R and A may point to exactly the same location; otherwise, {R[0], ..., R[lenR - 1]} and {A[0], ..., A[lenA - 1]} must not overlap in memory

[albinahlback]

I gave a thumbs up for the thought and discussion. I'm not sure whether I like the idea.

[Joel-Dahne]

I was not present at the discussions so I don't know what has already been said, but I can give some comments either way.

It sounds like a useful thing to have! But also sounds like a lot of work to get done, in particular for all already existing functions. In terms of wrapping Flint I'm not sure how helpful a partial implementation would be, if only half of the functions are handled then one would still have to do something else for the other half that is not handled.

It is also not clear what to do with conditions that are harder to express ("the value for lenQ should be equal to the lenAth Bernoulli number" say), I'm not sure to what extent there are any such examples though.