%%% Some list examples.  Note that it's okay to include types
%%% in the module, as well as the signature.

module list_examples.
  
  type member T -> (list T) -> o.
  % X is a member of a list of the form Y::Zs either if Y = X
  % or if X is a member of Zs.  The cases are handled by unification.
  % The failure of (member X nil) is handled by the closed world assumption.
  member X (X::Xs).
  member X (Y::Ys) :- member X Ys.
  
  % an alternative translation would be...
  type member2 T -> (list T) -> o.
  member2 X (Y::Zs) :- X = Y ;
                       not (X = Y), (member2 X Zs).
  
  type append (list T) -> (list T) -> (list T) -> o.
  % The append of lists Xs and Ys is defined by induction
  % on the structure of Xs.
  % basis: if Xs is nil, the result is Ys
  append nil Ys Ys.
  % induction: if Xs has the form X::Xs', then the result is X::Zs,
  % where Zs is (append Xs' Ys Zs).
  append(X::Xs) Ys (X::Zs) :- append Xs Ys Zs.
  
  % Using append, we can do member solely using Prolog's backtracking.
  % The idea is that X is a member of a list L if L can be written as
  % L1 concatenated with X::nil concatenated with L2.  This may seem tricky,
  % but it's just based on that definition.
  type member3 T -> (list T) -> o.
  member3 X L :- append L1 (X::L2) L.
  
  type reverse		(list T) -> (list T) -> o.
  % The reverse of a list L is defined by induction on the structure of L:
  % basis: reverse of nil is nil
  reverse nil nil.
  % induction: if L has the form H::T, its reverse is the reverse of T
  % concatenated with H::nil.
  reverse (Head::Tail) L :- (reverse Tail M), (append M (Head::nil) L).