:-module(_,[nrev/2],[]).
'$applied_packages'([prelude,nonpure,condcomp,assertions,regtypes,nativeprops,rtchecks_shallow,predefres(res_steps),resdefs,resdefs/resources_decl,basicmodes,argnames,expander]).
:-add_clause_trans(expander_tr:expand_clause/4,9910).
:-entry nrev(Xs,Ys):(list(Xs),var(Ys)).
:-check calls nrev(Xs,Ys):(list(Xs),var(Ys)).
:-true success nrev(Xs,Ys):(list(Xs),var(Ys))=>(list(Xs),list(Ys)).
:-true pred nrev(Xs,Ys):(list(Xs),term(Ys))=>(list(Xs),list(Ys)).
:-true pred nrev(Xs,Ys):(mshare([[Xs],[Xs,Ys],[Ys]]),var(Ys))=>mshare([[Xs,Ys]]).
:-checked calls nrev_i(Xs,Ys):(list(Xs),var(Ys)).
:-checked success nrev_i(Xs,Ys):(list(Xs),var(Ys))=>(list(Xs),list(Ys)).
:-true pred nrev_i(Xs,Ys):(list(Xs),term(Ys))=>(list(Xs),list(Ys)).
:-true pred nrev_i(Xs,Ys):(mshare([[Xs],[Xs,Ys],[Ys]]),var(Ys))=>mshare([[Xs,Ys]]).
:-checked calls appendlast(Xs,Ys,Zs):(list(Xs),term(Ys),term(Zs)).
:-checked success appendlast(Xs,Ys,Zs):(list(Xs),term(Ys),term(Zs))=>(list(Xs),term(Ys),list(Zs)).
:-true pred appendlast(Xs,Ys,Zs):(list(Xs),term(Ys),term(Zs))=>(list(Xs),term(Ys),non_empty_list(Zs)).
:-true pred appendlast(Xs,Ys,Zs):mshare([[Xs],[Xs,Ys],[Xs,Ys,Zs],[Xs,Zs],[Ys],[Ys,Zs],[Zs]])=>mshare([[Xs,Ys,Zs],[Xs,Zs],[Ys,Zs]]).

nrev(_1,_2) :-
        'nrev$pre'(_1,_2),
        'nrev$cls'(_1,_2).
'nrev$pre'(_1,_2) :-
        reify_check(list(_1),[_1],_3),
        reify_check(var(_2),[_2],_4),
        _5 is _3/\_4,
        _6 is _5,
        _7 is _5,
        _8 is _6\/_7,
        warn_if_false(_8,'CP').
'nrev$cls'(A,B) :-
        nrev_i(A,B).
nrev_i([],[]).
nrev_i([X|Xs],Ys) :-
        nrev_i(Xs,Ys0),
        appendlast(Ys0,X,Ys).
appendlast([],X,[X]).
appendlast([E|Y],X,[E|T]) :-
        appendlast(Y,X,T).