module diff_lists.
  
  %%% dl_to_list and list_to_dl work in one direction only, but don't rely
  %%% on the occurs check.
  %%% simplify works in both directions, but relies on the occurs check.
  
  %%% ``dl_to_list DL L'' succeeds if DL represents the list L.
  dl_to_list (diff nil  X) nil :- !.
  dl_to_list (diff X X) nil :- !.
  dl_to_list (diff (X::Y) Z) (X::W) :-
          dl_to_list (diff Y Z) W.
  
  %%% ``list_to_dl L DL'' succeeds if L is represented by the diff list DL.
  list_to_dl nil (diff X X).
  list_to_dl (X::W) (diff (X::Y) Z) :-
          list_to_dl W (diff Y Z).
  
  %%% ``simplify DL L'' succeeds if DL represents the list L.
  simplify (diff X X) nil.
  simplify (diff (X::Y) Z) (X::W) :- simplify (diff Y Z) W.
  
  %%% ``diffappend DL1 DL2 DL3'' succeeds if DL3 is the concatenation
  %%% of DL1 and DL2. Appending difference lists works like the arithmetic:
  %%%	(X-Y) + (Y-Z) = X-Z
  diffappend (diff X Y) (diff Y Z) (diff X Z).