module lists.

type  nreverse, permutation, reverse  
                      list A -> list A -> o.
type  append, join    list A -> list A -> list A -> o.
type  countup         int -> list int -> int -> o.
type  flatten         list (list A) -> list A -> o.
type  length          list A -> int -> o.
type  memb, member    A -> list A -> o.
type  memb_and_rest   A -> list A -> list A -> o.
type  nth_and_rest    int -> A -> list A -> list A -> o.
type  nth_and_replace int -> A -> list A -> list A -> list A -> o.
type  nth_item        int -> A -> list A -> o.
type  delete_member   A -> list A -> list A -> o.

% (memb X L) succeeds if X is a member of L.  In contrast to ``member'',
% this will succeed as often as X unifies with members of L.

memb X (X :: L).
memb X (Y :: L) :- memb X L.

% (member X L) succeeds if X is a member of L.  In contrast to ``memb'',
% this will succeed only once: for the first unifier of X with a member of L.

member X (X :: L) :- !.
member X (Y :: L) :- member X L.

% (append L K M) succeeds if M is the result of appending K to L.

append nil K K.
append (X :: L) K (X :: M) :- append L K M.

% (join L K M) is similar to append except that members of L that already
% appear in K are not appended to form M.

join nil K K.
join (X :: L) K M :- memb X K, !, join L K M.
join (X :: L) K (X :: M) :- join L K M.

% (memb_and_rest X L M) succeeds for every occurrence of X in L,
% where M is the result of removing that occurrence from L.

memb_and_rest A (A :: Rest) Rest.
memb_and_rest A (B :: Tail) (B :: Rest) :- memb_and_rest A Tail Rest.

% (nth_item N X L) succeeds if the Nth item of L is X, where
% counting starts at 1.

nth_item N A List      :- N < 1, !, fail.
nth_item 1 A (B::Rest) :- !, A = B.
nth_item N A (B::Tail) :- M is (N - 1), nth_item M A Tail.

% (nth_and_rest N X L Rest) succeeds if the Nth item of L is X, and 
% Rest is the rest of L.  Counting starts at 1.  For N = 0, it behaves
% like memb_and_rest.

nth_and_rest 0 A List Rest :- !, memb_and_rest A List Rest.
nth_and_rest 1 A (B::Rest) Rest :- !, A = B.
nth_and_rest N A (B::Tail) (B::Rest) :-
  M is (N - 1), nth_and_rest M A Tail Rest.

% (nth_and_replace N X L Rep K) succeeds if the Nth item of L is X, and 
% K is the result of inserting Rep for X in L.  
% Counting starts at 1.  

nth_and_replace 0 _ _ _ _ :- !, fail.
nth_and_replace 1 A (B::Rest) Rep K :- !, A = B, append Rep Rest K.
nth_and_replace N A (B::Tail) Rep (B::Rest) :-
  M is (N - 1), nth_and_replace M A Tail Rep Rest.

% (reverse L K) succeeds if L and K are two lists that are reverses
% of each other.

reverse L K :- pi rv\(
  (                   rv nil K,
   pi X\(pi N\(pi M\( rv (X::N) M :- rv N (X::M)))))
   => rv L nil).

% (length L N) succeeds if N is the length of list L.

length nil 0.
length (X::L) N :- length L M, N is M + 1.

% (nreverse L K) succeeds if L and K are two lists that are reverses
% of each other.  Implemented using the naive reverse algorithm.

nreverse nil nil.
nreverse (X::L) K :- nreverse L M, append M (X::nil) K.

%  (countup N L M) succeeds when L is the list of integers between N
% and M inclusively and when is L is nil and N > M.

countup N nil M      :-  N > M, !.
countup N (N::nil) N :- !.
countup N (N::L) M   :- N1 is N + 1, countup N1 L M.

% (permutation L K) succeeds if L and K are permutations of each other.

permutation nil nil.
permutation L (H::T) :-
  append V (H::U) L, append V U W, permutation W T.

% (flatten L F) succeeds if F is the result of flatten the list of
% lists L.

flatten (L :: R) F :- flatten R FR, append L FR F.
flatten nil nil.

% (delete_member X L K) succeeds if K is the result of deleting all
%  occurrences of X from L.

delete_member _ nil nil.
delete_member X (X::L)     K  &
delete_member X (Y::L) (Y::K) :- !, delete_member X L K.