:- 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. 

% ----
% treemin for ANY binary tree (ok also for trees with duplicate values)
:- pred treemin(tree(int),bool,int). 
:- mode treemin(in,out,out).
:- cata treemin/3-1.

treemin(leaf,IsDef,Min) :- constr(~IsDef & Min=0). % Min can be any int
treemin(node(N,L,R),IsDef,Min) :- 
    treemin(L,IsDefL,MinL),
    treemin(R,IsDefR,MinR),
  constr(IsDef & 
         (Min= ite(IsDefL & IsDefR, 
                     ite(MinL<MinR, 
                          ite(MinL<N,MinL,N), 
                          ite(MinR<N,MinR,N) ),            
                     ite(IsDefL,
                          ite(MinL<N,MinL,N),             
                          ite(IsDefR & MinR<N,MinR,N))))).  
% catamorphisms       
% --- min of a list
:- pred listmin(list(int),bool,int). 
:- mode listmin(in,out,out).  
:- cata listmin/3-1.

listmin([],IsDef,A) :- constr( ((~IsDef) & (A=0)) ).
listmin([H|T],IsDef,Min) :-
         constr( IsDef & (Min = ite(IsDefT, ite(H<MinT,H,MinT), H )) ),
         listmin(T,IsDefT,MinT).
%============================================== 
% Verification
:- pred ff1.   % for treesort: same cardinality of elements
ff1 :- 
    constr( ~((IsDefLMin = IsDefSMin) & 
    ((IsDefLMin & IsDefSMin) => (LMin=SMin)) )), 
    listmin(L,IsDefLMin,LMin), listmin(S,IsDefSMin,SMin),
    treesort(L,S).
    
% contracts (postcondition: true)

:- spec bstinsert(X,T1,T2) ==> treemin(T1,B1,ST1), treemin(T2,B2,ST2).

:- spec bstinsert_list(L,T) ==> listmin(L,B1,SL) , treemin(T,B2,ST).

:- spec visit(T,L) ==> treemin(T,B1,ST), listmin(L,B2,SL).

:- spec concat4(Xs,Y,Ys,Zs) ==> listmin(Xs,B1,SXs), listmin(Ys,B2,SYs), listmin(Zs,B3,SZs) 
              .

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