length/2 improvements

[UWN]

The current length/2 implementation works nicely for Prolog with syntactic unification and also with rational trees. But for constraints (and to start with, freeze/2) there are still some issues where a naïve implementation (correctly) fails, whereas Scryer currently gives up with a resource error (#29):

?- freeze(L,L=[]), length(L,L). 
caught: error(resource_error(finite_memory),length/2) % now fails

It further improves upon the naive implementation for very large N (#31):

?- freeze(L,L=[_|L]), N is 2^64, length(L,N). 
GNU MP: Cannot allocate memory (size=8) % now fails

\+ \+ copy_term(Vs,Vs,[]) should eventually be replaced by a correctly implemented copy_term(Vs,Vs,[]) (#1272).

det_length_rundown/2 could be implemented in Rust creating all N cells en bloc, as there is no possibility to make it fail earlier. This in turn might produce a resource error much faster, since a single such check in advance is required in stead of N such checks.

And finally, there are still some open issues which are currently handled as the naïve implementation does. Roughly all cases where length(L,N) starts to enumerate all lengths but some constraints are attached like #30 which still does not produce a resource error rapidly. However, it seems that such cases lead to an extremely complex implementation. So I leave them as is. At least for the moment.

Concerning the cooperation of clpz and length/2, it is not obvious how to make this without resorting to a specific ad hoc solution. Some considerations to this end are here and here. So for the time being, the following query still does not terminate:

?- N in 1..3, length(L, N).
   N = 1, L = [_A]
;  N = 2, L = [_A,_B]
;  N = 3, L = [_A,_B,_C]
;  % still looping

---

:- use_module(library(error)).

:- meta_predicate(resource_error(+,0)).
% should be :- meta_predicate(resource_error(+,:)).
resource_error(Resource, Context) :-
   throw(error(resource_error(Resource), Context)).

length(Xs0, N) :-
   '$skip_max_list'(M, N, Xs0,Xs),
   !,
   (  Xs == [] -> N = M
   ;  nonvar(Xs) -> var(N), Xs = [_|_], resource_error(finite_memory,length/2)
   ;  nonvar(N) -> R is N-M, length_rundown(Xs, R)
   ;  N == Xs -> failingvarskip(Xs), resource_error(finite_memory,length/2)
   ;  length_addendum(Xs, N, M)
   ).
length(_, N) :-
   integer(N), !,
   domain_error(not_less_than_zero, N, length/2).
length(_, N) :-
   type_error(integer, N, length/2).

length_rundown(Xs, 0) :- !, Xs = [].
length_rundown(Vs, N) :-
    \+ \+ copy_term(Vs,Vs,[]), % unconstrained
    !,
    det_length_rundown(Vs, N).
length_rundown([_|Xs], N) :- % force unification
    N1 is N-1,
    length(Xs, N1). % maybe some new info on Xs

% This could be written in Rust directly, no general unification
det_length_rundown(Xs, 0) :- !, Xs = [].
det_length_rundown([_|Xs], N) :-
    N1 is N-1,
    det_length_rundown(Xs, N1).

failingvarskip(Xs) :-
    \+ \+ copy_term(Xs,Xs,[]), % unconstrained
    !.
failingvarskip([_|Xs0]) :- % force unification
    '$skip_max_list'(_, _, Xs0,Xs),
    (  nonvar(Xs) -> Xs = [_|_]
	 ;  failingvarskip(Xs)
    ).

length_addendum([], N, N).
length_addendum([_|Xs], N, M) :-
    M1 is M + 1,
    length_addendum(Xs, N, M1).