:- pred constr(bool). 
:- mode constr(in). 
:- ignore constr/1.
:- type tree(A) ---> leaf ; node( A, tree(A), tree(A) ). 
% type of trees whose nodes have values of type A (which may be 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(X,T1,T), bstinsert_list(Xs,T1).

% ---   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),
  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]) :-          % non-linear heads are allowed
	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 ).      % Hd can be any int
hd([H|T],IsDef,Hd) :- constr( IsDef & Hd=H ).

% ---
:- pred listmin(list(int),bool,int).             % Lists may have duplicates: e.g. [2,3,2,5]
:- 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)) )),  % ok H<MinT
         listmin(T,IsDefT,MinT).

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

listmax([],IsDef,A) :- constr(((~IsDef) & (A=0))).% A can be any int
listmax([H|T],IsDef,Max) :-
         constr(( IsDef & (Max = ite(IsDefT, ite(H>MaxT,H,MaxT), H)) )), % ok H>MaxT
         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:  proved sortedness 
ff1 :- 
   constr(~(B)), 
   is_asorted(S,B), 
   treesort(L,S).
   
:- pred ff2.        % for bstinsert  proved
ff2 :-
      constr(~( (B1 = B2) )), 
      bstree(T1,B1), bstree(T2,B2), 
      bstinsert(X,T1,T2).

:- pred ff3.       % proved for bstinsert_list
ff3 :- 
  constr(~( B )), 
  bstree(T,B),  
  bstinsert_list(L,T).

:- pred ff4.       % proved  for visit
ff4 :-
  constr( ~( (B1 => B2) ) ), 
  bstree(T,B1), 
  is_asorted(L,B2),
  listmin(L,IsDefMinL,MinL), listmax(L,IsDefMaxL,MaxL),     % Extra catas seem needed  
  visit(T,L).

:- pred ff5.       % proved for concat
ff5 :-  
  constr(~( ((( (IsDefXs  &  (IsDefYs & (MaxXs=<Y & Y=<MinYs))) v
               (~IsDefXs  &  (IsDefYs & Y=<MinYs)))        v
                (IsDefXs  & (~IsDefYs & (MaxXs=<Y))))     v
               (~IsDefXs  &  ~IsDefYs))
                => ((B3 & B4) = B5) )),
  listmax(Xs,IsDefXs,MaxXs),
  listmin(Ys,IsDefYs,MinYs),
  is_asorted(Xs,B3),
  is_asorted(Ys,B4),
  is_asorted(Zs,B5),
  concat(Xs,Y,Ys,Zs).

% ===============================================================
:- query ff1/0. 
:- query ff2/0. 
:- query ff3/0. 
:- query ff4/0. 
:- query ff5/0. 
% ===============================================================