Choicepoint pruning needs a cut, but I think the compiler should be sharp enough to do it by itself

I'm doing an exercise of writing a between/3 that takes an additional step value.

This is an interesting exercise, quickly showing:

the advantage of tagged integers (i.e. use pos(X) instead of X if X is a positive integer to take advantage of pattern matching)
the magic inherent in making the predicate as deterministic as possible (do not leave a choicepoint open at the end of the sequence)
the interest in passing a "flag" array to the predicate to fine-tune behaviour (in this case, should it throw or fail if the sequence is empty?)

But also:

the less than well-thought-out format of the ISO standard exception terms (using compound terms instead of lists to ferry info ... WTF!)
the naming of the exception-throwing predicates in library(error) (why not call them throw_... instead of confusingly giving them the same name as the exception term, will people really want to call(domain_error(...))?
the fact that must_be/2 cannot take additional position information about which arg exactly caused a problem (why!)

The complete code is between_with_step.pl ... not yet fully unit tested.

Now I have set up the following predicate

between_enum(+Start,+TaggedEnd,+TaggedStep,-Value)

which emits the next value of the increasing or decreasing sequence of integers. It uses pattern matching of tagged values. In particular, the case "end value if the sequence is an integer" (as opposed to an atom denoting infinity) and "the step is positive" is given by the following subset of clauses matching the terms int(End) and pos(Step):

% ---
% Case of "positive step" pos(Step) and "integer end" int(End) (not infinite end)
% ---

% Past end of sequence. Occurs only if the sequence is empty on entry.

between_enum(Start,int(End),pos(_),_) :- 
   Start > End,!,fail. 

% Last entry in sequence, emit "Start" as "Value" and don't allow backtracking!
% The test "Start < End" is redundant here.

between_enum(Start,int(End),pos(Step),Start) :- 
   Start < End, Start+Step >  End, !. 

% More entries exist in sequence, emit "Start" as "Value" and DO allow backtracking!
% The test "Start < End" is redundant here.
% The test "Start+Step =< End" is redundant here, being the complement of the cut-off preceding clause

between_enum(Start,int(End),pos(Step),Start) :-
   Start < End, Start+Step =< End.    

% Recursive alternative to the above, digging for more values!
% The test "Start < End" is redundant here.
% The test "Start+Step =< End" is redundant here

between_enum(Start,int(End),pos(Step),Value) :-
   Start < End, Start+Step =< End, 
   NewStart is Start+Step, 
   %!, % NEEDED TO MAINTAIN DETERMINACY ON LAST VALUE
   between_enum(NewStart,int(End),pos(Step),Value).

Now, to be fully deterministic at the end of the enumeration, the following clause needs a cut:

between_enum(Start,int(End),pos(Step),Value) :-
   Start < End, Start+Step =< End, 
   NewStart is Start+Step, 
   !, % <---- HERE
   between_enum(NewStart,int(End),pos(Step),Value).

Otherwise:

With cut:

?- between(10,15,1,Value).
Value = 10 ;
Value = 11 ;
Value = 12 ;
Value = 13 ;
Value = 14 ;
Value = 15.        % This is the end for sure!

Without cut:

?- between(10,15,1,Value).
Value = 10 ;
Value = 11 ;
Value = 12 ;
Value = 13 ;
Value = 14 ;
Value = 15 ;      % Unsure whether this is the end?
false.            % Well, turns out it is the end, really!

Shouldn't the compiler be muscular enough to determine that no further matches are possible after between_enum(Start,int(End),pos(Step),Value) - this being the last one in the series tagged with

int/1 on 2nd position and
pos/1 on third position?

This SWI-Prolog 8.1.

Edit

Could be that the compiler just indexes on the first two arguments. There is a no need for a cut in

between_enum(Start,int(End),neg(Step),Value)

which is followed only by

between_enum(Start,inf,neg(Step),Value)

as well as

between_enum(Start,minf,neg(Step),Value)

And so it can bloody well distinguish inf, minf and int(_).

Solution

This is Prolog system dependent, and depends on the available automatisms for indexing or on the available directives for indexing. For example SWI-Prolog has automatic deep indexing, but some idiosyncrasies concerning automatic multi-argument indexing. So for the example from madgen:

first(tag1(_),_).
first(tag2(_),_).

second(_,tag1(_)).
second(_,tag2(_)).

I get in my system, both queries do not leave a choice point:

Jekejeke Prolog 4, Runtime Library 1.4.7

?- first(tag1(1),2).
Yes

?- second(2,tag1(1)).
Yes

On the other hand in SWI-Prolog, a choice point is left in the second query:

SWI-Prolog (threaded, 64 bits, version 8.3.17)

?- first(tag1(1),2).
true.

?- second(2,tag1(1)).
true ;
false.

This can be quite annoying, and often facade predicates need to be used to reorder the arguments, to make them more suitable to the SWI-Prolog specific indexing.