:- 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),
  concat(XL,A,XR,Xs).

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

concat([],X,Ys,[X|Ys]).
concat([X|Xs],Y,Ys,[X|Zs]) :-        
	concat(Xs,Y,Ys,Zs).
	
% ---   cons
:- pred cons(int,list(int),list(int)).
:- mode cons(in,in,out). 
cons(H,T,[H|T]).
% ==========================================================
% Catamorphisms. 
% Binary Search Tree 
:- pred bstree(tree(int),bool).
:- mode bstree(in,out).
:- cata bstree/2-1.

bstree(leaf,B) :- constr(B).
bstree(node(N,L,R),B) :- 
  bstree(L,BL), 
  bstree(R,BR),
  treemax(L,IsDefL,MaxL), 
  treemin(R,IsDefR,MinR),
  constr( ( (GeqLeft=(IsDefL  => N>=MaxL)) &
            (LeqRight=(IsDefR => N=<MinR)) ) &
            (B= ((GeqLeft & BL) & (LeqRight & BR)))).

% ---
:- pred treemax(tree(int),bool,int).  
:- mode treemax(in,out,out).
:- cata treemax/3-1.

treemax(leaf,IsDef,Max) :- constr(~IsDef & Max=0).         % Max can be any int.
treemax(node(N,L,R),IsDef,Max) :- 
  treemax(L,IsDefL,MaxL),
  treemax(R,IsDefR,MaxR),
  constr(IsDef & 
         (Max= ite(IsDefL & IsDefR, 
                     ite(MaxL>=MaxR, 
                          ite(MaxL>=N,MaxL,N), 
                          ite(MaxR>=N,MaxR,N) ),            % max(MaxL,max(MaxR,N))
                     ite(IsDefL,
                          ite(MaxL>=N,MaxL,N),              % max(MaxL,N)
                          ite(IsDefR & MaxR>=N,MaxR,N))))). % max(MaxR,N)
% ---
:- 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) ),            % min(MinL,min(MinR,N))
                     ite(IsDefL,
                          ite(MinL=<N,MinL,N),              % min(MinL,N)
                          ite(IsDefR & MinR=<N,MinR,N))))). % min(MinR,N)
                          
%-----  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). 

%----- checking a weakly ascending ordered list
:- pred is_asorted(list(int),bool).
:- mode is_asorted(in,out).
:- cata is_asorted/2-1.

is_asorted([],Res) :- constr(Res).
is_asorted([H|T],Res) :-
    hd(T,IsDefT,HdT),
    is_asorted(T,ResT),
    constr(Res=(IsDefT => (H=<HdT & ResT))).
    
% ---
:- pred hd(list(int),bool,int).
:- mode hd(in,out,out).
:- cata hd/3-1.

hd([],IsDef,Hd) :- constr( ~IsDef & Hd=0 ).      % 0 can be any int
hd([H|T],IsDef,Hd) :- constr( IsDef & Hd=H ).

% ---
:- pred listmin(list(int),bool,int).  
:- mode listmin(in,out,out).
:- cata listmin/3-1.

listmin([],IsDef,A) :- constr( ((~IsDef) & (A=0)) ). % 0 can be any integer
listmin([H|T],IsDef,Min) :-
         constr(( IsDef & (Min = ite(IsDefT, ite(H<MinT,H,MinT), H)) )), 
         listmin(T,IsDefT,MinT).

% --- 
:- pred listmax(list(int),bool,int).    
:- mode listmax(in,out,out).
:- cata listmax/3-1.

listmax([],IsDef,A) :- constr(((~IsDef) & (A=0))). % 0 can be any integer
listmax([H|T],IsDef,Max) :-
         constr(( IsDef & (Max = ite(IsDefT, ite(H>MaxT,H,MaxT), H)) )), 
         listmax(T,IsDefT,MaxT).
         
% ---  count on lists
:- pred listcount(int,list(int),int).
:- mode listcount(in,in,out).
:- cata listcount/3-2.

listcount(X,[],Res) :- constr( Res=0 ).
listcount(X,[Y|Ys],Res) :-
    constr( Res=ite(X=Y,(ResT+1),ResT) ),
    listcount(X,Ys,ResT).

%============================================== 
% Verification
:- pred ff1.        % for treesort:  same multiset of elements
ff1 :- 
   constr(~(CL=CS)), 
   listcount(X,L,CL), listcount(X,S,CS), 
   treesort(L,S).
   
:- pred ff2.        % for bstinsert  
ff2 :-
      constr(~(  C2=ite(X=Y, C1+1, C1) )),
      treecount(Y,T1,C1), treecount(Y,T2,C2),
      bstinsert(X,T1,T2).

:- pred ff3.       % for bstinsert_list
ff3 :- 
  constr(~(CL=CT)),
  listcount(X,L,CL), treecount(X,T,CT), 
  bstinsert_list(L,T).

:- pred ff4.       % for visit
ff4 :-
  constr( ~(CT=CL)), 
  treecount(X,T,CT), listcount(X,L,CL),                    
  visit(T,L).

:- pred ff5.       % for concat
ff5 :-  
 constr(~(CZs = ite(X=Y, CXs+CYs+1, CXs+CYs))),
  listcount(X,Xs,CXs), listcount(X,Ys,CYs), listcount(X,Zs,CZs), 
  concat(Xs,Y,Ys,Zs).
  
%==============================================
:- query ff1/0.
:- query ff2/0.
:- query ff3/0.
:- query ff4/0.
:- query ff5/0.
%==============================================