:- 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,[X,Y]).              % error. correct: 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).
	
% ---   cons
:- pred cons(int,list(int),list(int)).
:- mode cons(in,in,out). 
cons(H,T,[H|T]).
% ==========================================================
% Catamorphisms. 

% ---  treesize 
:- pred treesize(tree(int),int).
:- mode treesize(in,out).
:- cata treesize/2-1.

treesize(leaf,Res) :- Res=1.
treesize(node(A,L,R),Res) :- 
    Res=(1+(ResL+ResR)),
    treesize(L,ResL),
    treesize(R,ResR).

% ---  size on lists
:- pred listsize(list(int),int).
:- mode listsize(in,out).
:- cata listsize/2-1.

listsize([],Res) :- Res=1.
listsize([Y|Ys],Res) :-
   Res=(ResT+1),
   listsize(Ys,ResT).
%============================================== 
% Verification
:- pred ff1.   % for treesort: same cardinality of elements
ff1 :- 
   constr(~(CL=CS)), 
   listsize(L,CL), listsize(S,CS), 
   treesort(L,S).

% contracts (postcondition: true)

:- spec bstinsert(X,T1,T2) ==> treesize(T1,ST1), treesize(T2,ST2) => constr(true).

:- spec bstinsert_list(L,T) ==> listsize(L,SL) , treesize(T,ST) => constr(true).

:- spec visit(T,L) ==> treesize(T,ST), listsize(L,SL) => constr(true).

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

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