:- 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. 
%-----  listmember --- is there X in the given list?
:- pred listmember(int,list(int),bool).
:- mode listmember(in,in,out).
:- cata listmember/3-2.

listmember(X,[],Res) :- constr(~Res).
listmember(X,[Y|Ys],B) :-
      constr( B=ite(X=Y,true,B1) ) ,
      listmember(X,Ys,B1).

%-----  treemember --- is there X in the given binary tree?
:- pred treemember(int,tree(int),bool).
:- mode treemember(in,in,out).
:- cata treemember/3-2.

treemember(X,leaf,Res) :- constr(~Res).
treemember(X,node(A,L,R),Res) :- 
    constr( Res=ite(X=A,true,(ResL v ResR)) ),
    treemember(X,L,ResL),
    treemember(X,R,ResR). 
  
%============================================== 
% Verification
:- pred ff1.
ff1 :- 
   constr( ~(LB=SB)),
   listmember(X,L,LB), 
   listmember(X,S,SB),
   treesort(L,S).
    
% contracts (postcondition: true)

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

:- spec bstinsert_list(L,T) ==> listmember(X,L,SL) , treemember(X,T,ST).

:- spec visit(T,L) ==> treemember(X,T,ST), listmember(X,L,SL).

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

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