:- 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,leaf).  %error: 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. 
%-----  treecount --- how many X's in the given binary tree.
:- pred treecount(int,tree(int),int).
:- mode treecount(in,in,out).
:- cata treecount/3-2.

treecount(X,leaf,Res) :- constr( Res=0 ).
treecount(X,node(A,L,R),Res) :- 
    constr( Res=ite(X=A,ResL+ResR+1,ResL+ResR) ),
    treecount(X,L,ResL),
    treecount(X,R,ResR). 

%-----  listcount --- how many X's in the given list.
:- pred listcount(int,list(int),int).
:- mode listcount(in,in,out).
:- cata listcount/3-2.

listcount(X,[],N) :- N=0.
listcount(X,[H|T],N) :-
  constr( (N=ite(X=H,(NT+1),NT)) ),
  listcount(X,T,NT).
  
  
%============================================== 
% Verification
:- pred ff1.
ff1 :- 
   constr( ~(LB=SB)),
   listcount(X,L,LB), 
   listcount(X,S,SB),
   treesort(L,S).
    
% contracts (postcondition: true)

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

:- spec bstinsert_list(L,T) ==> listcount(X,L,SL) , treecount(X,T,ST).

:- spec visit(T,L) ==> treecount(X,T,ST), listcount(X,L,SL).

:- spec concat4(Xs,Y,Ys,Zs) ==> listcount(X,Xs,BXs), listcount(X,Ys,BYs), listcount(X,Zs,BZs).

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