% list concatenation: linear in the length of the first argument
app([],Ys,Ys).
app([X|Xs],Ys,[X|Zs]) :- app(Xs,Ys,Zs).

% concatenation of difference lists: constant time
app_dl(L-M, M-N, L-N).

% naive reverse (quadratic time!)
nrev([],[]).
nrev([X|Xs],L) :- nrev(Xs,Ys), app(Ys,[X],L).

% naive reverse with difference lists:
rev_dl([],L-L).
rev_dl([X|Xs],L-M) :- rev_dl(Xs,UR-T), app_dl(UR-T, [X|N]-N, L-M).

% reverse in linear time:
rev(Xs,Ys) :- rev_dl2(Xs,Ys,[]).

rev_dl2([],L,L).
rev_dl2([X|Xs],L,N) :- rev_dl2(Xs,L,[X|N]).