mndrix/mavis

mode and determinism checking

Opened this issue · 1 comments

It might be convenient to have mavis check the mode of a predicate's arguments as well as that predicate's determinism. I've speculated on this elsewhere. Wouter Beek suggested a similar idea:

Have you also thought of auto-checking the determinism that is mentioned in the plDoc?

He provides the following code that could help in the implementation (attributed to Ulrich Neumerkel):

%! call_nth(:Goal, +N:nonneg) is semidet.
% Calls the given goal the given number of times.
%
% This does not exclude the case in which the goal
%  could have been executed more than `N` times.
%
% @arg Goal A nondeterministic goal.
% @arg N A nonnegative integer.

call_nth(Goal, C):-
  State = count(0),
  Goal,
  arg(1, State, C1),
  C2 is C1 + 1,
  nb_setarg(1, State, C2),
  C = C2.

%! call_semidet(:Goal) is det.
% Executes the given semi-deterministic goal exactly once,
%  i.e., regardless of any open choice points.
% If the goal is not semideterministic, an error is thrown.
%
% @error error(mode_error(semidet, Goal),
%        context(call_semidet/1, 'Message left empty.'))

call_semidet(Goal):-
  (
    call_nth(Goal, 2)
  ->
    mode_error(semidet, Goal)
  ;
    once(Goal)
  ).

It may be fruitful to make use of the following for the automated mode checking part: http://www.swi-prolog.org/pack/file_details/type_check/prolog/type_check.pl?show=src