mndrix/mavis

check clause heads for exhaustion

Opened this issue · 0 comments

Consider this code:

:- type thing ---> foo; bar(integer).

%% something(X:thing) is det.
something(foo).

There's some obvious disagreement here. The modeline says that the predicate is deterministic (won't ever fail). However, there is no clause for the bar(integer) case. This is almost certainly a bug.

For each predicate that has a type signature and mode of det or multi, generate random values (using quickcheck:arbitrary/2) for each argument and make sure at least one clause matches. If we find a value for which there are no matching clauses, generate a warning.

Be careful that this doesn't generate false warnings. Prolog often omits cases specifically to generate failure. That's why I suggest that this check must consider the predicate's mode.

Of course, this check should work for types other than algebraic data types. Any type for which we can generate random values should be checkable by this approach.