:- pred constr(bool). 
:- mode constr(in). 
:- ignore constr/1.
:- type tree(int) ---> leaf ; node( int, tree(int), tree(int) ). 
% leaf is the EMPTY tree. DUPLICATES ARE ALLOWED.
% ==========================================================
% Program: treesort: 
% list L of integers  
%  --> (by bstinsert_list in) tree T of integers
%  --> (by in-order visit of T) sorted list S of integers 
% S is sorted in WEAKLY ASCENDING order *** WITH duplicates***

% ---   treesort
:- pred treesort(list(int),list(int)).
:- mode treesort(in,out).

treesort(L,S) :- 
  bstinsert_list(L,T),    % making a bstree  
  visit(T,S).             % visiting the tree
  
% ---  	bstinsert 
:- pred bstinsert(int,tree(int),tree(int)).
:- mode bstinsert(in,in,out).

bstinsert(X,leaf,node(X,leaf,leaf)).    
bstinsert(X,node(A,L,R), node(A,L1,R)) :- constr(X=<A), bstinsert(X,L,L1).
bstinsert(X,node(A,L,R), node(A,L,R1)) :- constr(X>A),  bstinsert(X,R,R1).

% ---   bstinsert_list
:- pred bstinsert_list(list(int),tree(int)).
:- mode bstinsert_list(in,out).

bstinsert_list([],leaf).
bstinsert_list([X|Xs],T) :- bstinsert_list(Xs,T1), bstinsert(X,T1,T).

% ---   visit
:- pred visit(tree(int),list(int)).    % in-order visit of the tree: 
:- mode visit(in,out).                 % left-tree --> root --> right-tree

visit(leaf,[]).
visit(node(A,L,R), Xs) :-
  visit(L,XL), visit(R,XR),
  concat4(XL,A,XR,Xs).

% ---   concat4
:- pred concat4(list(int),int,list(int),list(int)).
:- mode concat4(in,in,in,out).  

concat4([],X,Ys,[X|Ys]).
concat4([X|Xs],Y,Ys,[X|Zs]) :-        
	concat4(Xs,Y,Ys,Zs).
	
% ==========================================================
% Catamorphisms. 
%-----  treesum --- sum of integers in nodes of the given binary tree.
:- pred treesum(tree(int),int).
:- mode treesum(in,out).
:- cata treesum/2-1.

treesum(leaf,Res) :- Res=0.
treesum(node(A,L,R),Res) :- 
    Res=((ResL+ResR)+A),
    treesum(L,ResL),
    treesum(R,ResR). 
         
%-----  listsum --- sum of integers in nodes of the given list.
:- pred listsum(list(int),int).
:- mode listsum(in,out).
:- cata listsum/2-1.

listsum([],S) :- S=0.
listsum([H|T],S) :-
  S=(H+ST),
  listsum(T,ST).
  
%============================================== 
% Verification
:- pred ff1.
ff1 :- 
   constr( ~(LS=SS)),
   listsum(L,LS), 
   listsum(S,SS),
   treesort(L,S).
    
% contracts (postcondition: true)

:- spec bstinsert(X,T1,T2) ==> treesum(T1,ST1), treesum(T2,ST2).

:- spec bstinsert_list(L,T) ==> listsum(L,SL), treesum(T,ST).

:- spec visit(T,L) ==> treesum(T,ST), listsum(L,SL).

:- spec concat4(Xs,Y,Ys,Zs) ==> listsum(Xs,SXs), listsum(Ys,SYs), listsum(Zs,SZs).

%==============================================
:- query ff1/0.
%==============================================