How instrument Prolog code to check determinism

Question

We want to instrument our Prolog code by automatic determinism checks. So in the spirit of Ciao assertions we would declare :- pred <functor>/<arity> is <determinism>, where <determinism> can take the values:

Value	Description
det	have exactly one solution, then that mode is deterministic
semidet	either have no solutions or have one solution, then that mode is semideterministic
multi	have at least one solution but may have more, then that mode is multisolution
nondet	have zero or more solutions, then that mode is nondeterministic

https://www.mercurylang.org/information/doc-latest/mercury_ref/Determinism-categories.html

Here is an example expected behaviour, take this Prolog text input:

:- pred r/1 is multi.
r(b).
r(c).
r(c).

And then this query output:

?- r(a).
Error: Unknown pattern: assertion_failure(multi)
?- r(b).
Yes
?- r(c).
Yes ;
Yes

Since most Prolog systems have term expansion and goal expansion, it seems to be a suitable language to inject such assertions at compile time by some Prolog code itself. How would one go about and implement such an instrumentation?

Answer 1

We can analyse the determinism categories by the errors situations they need to detect. There are two different error situations which span all the determinism categories. The error situations refer to the goal that is called with the given predicate indicator:

Value	Finite Failure	Multiple Solutions
det	Forbidden	Forbidden
semidet	Allowed	Forbidden
multi	Forbidden	Allowed
nondet	Allowed	Allowed

For the determinism categories 'nondet', nothing needs to be done. For the other determinism categories we install a wrapper. This wrapper will have the given predicate indicator and call a auxiliary predicate that collects the rules of the given predicate indicator. For finite failure we find this suggestion in the literature:

Debugging Prolog Using Annotations
M. Kula - Published 2000
https://pdfs.semanticscholar.org/0d14/e5c3d88cf280ca5b37fae15b58fde9986544.pdf

But we simply use the soft cut instead:

(Call *-> true; assertion_failure)

For multiple solutions we use call_nth/2, which is also found in many Prolog systems meanwhile:

call_nth(Call, Count), (Count > 1 -> assertion_failure; true)

A link to the code with the corresponding rewriting is given at the end. Also collection of examples is given at the end. We can show two more of the examples. Take this Prolog text input:

:- pred p/1 is semidet.
p(b).
p(c).
p(c).

:- pred q/1 is det.
q(b).
q(c).
q(c).

The wrapper produces these results:

?- p(a).
No
?- p(b).
Yes
?- p(c).
Yes ;
Error: Unknown pattern: assertion_failure(semidet)

?- q(a).
Error: Unknown pattern: assertion_failure(det)
    q/1
?- q(b).
Yes
?- q(c).
Yes ;
Error: Unknown pattern: assertion_failure(det)

Open source:

Assertion Wrapper
https://gist.github.com/jburse/d5e95099e3d83f6f09b2cb2a91da719c#file-assertion-pl

Assertion Demo
https://gist.github.com/jburse/d5e95099e3d83f6f09b2cb2a91da719c#file-demo-pl