:- pred constr(bool). 
:- mode constr(in). 
:- ignore constr/1.
:- type tree(int) ---> leaf ; node( int, tree(int), tree(int) ).
% Note: duplicates are NOT allowed.   
% ==========================================================
% Deletion from a binary search tree. treesum. 
% https://algs4.cs.princeton.edu/32bst/
% ==========================================================

% Note: if X does not occur in tree(int), BSTdelete(X,tree(int)) = tree(int).
:- pred bstdelete(int,tree(int),tree(int)).   
:- mode bstdelete(in,in,out).

bstdelete(X,leaf,node(A,leaf,leaf)).          % Functionally, bstdelete(X,leaf)=leaf.
                     % error above: node(A,leaf,leaf) ---> leaf
bstdelete(X,node(A,leaf,R), R) :- constr(X=A).
bstdelete(X,node(A,L,leaf), L) :- constr(X=A).
bstdelete(X,node(A,L,R), node(Succ,L,Rd) ) :-  constr(X=A & IsDef), 
        bstdeletemin(R, Rd, Succ, IsDef).  % (R w/o Succ) = Rd. Succ is the minimum of R. 

bstdelete(X,node(A,L,R), node(A,L1,R)) :- constr(X<A), bstdelete(X,L,L1).
bstdelete(X,node(A,L,R), node(A,L,R1)) :- constr(A<X), bstdelete(X,R,R1).

% ---
:- pred bstdeletemin(tree(int),tree(int),int,bool).     
:- mode bstdeletemin(in,out,out,out).

bstdeletemin(leaf,leaf,X,IsDef) :- constr(X=0 & ~IsDef). % 0 can be any int value.
bstdeletemin(node(A,leaf,R),R,X,IsDef) :- constr(X=A & IsDef). 
bstdeletemin(node(A,LeftT,R),node(A,T,R),X,IsDef) :- constr(IsDef),
        bstdeletemin(LeftT,T,X,IsDef).  

% ==========================================================
% catamorphisms
:- pred bstree(tree(int),bool).
:- mode bstree(in,out).
:- cata bstree/2-1.

% bstree checks whether or not a tree is a binary search tree.
bstree(leaf,B) :- constr(B).   % Values increasing left-to-right
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 for ANY binary tree (ok also for trees with duplicate values)
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)
% ----
% 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))))).
                          
  %-----  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). 
                        
% ==========================================================
% Verification. 
:- pred ff1.
ff1 :- 
   constr( ~((B1 & (X=Y)) => ((R2=R1-1) v (R2=R1))) ),
   bstree(T1,B1), bstree(T2,B2),
   treecount(X,T1,R1), 
   bstdelete(Y,T1,T2),
   treecount(X,T2,R2).

%% postcondition true
%
%:- spec bstdeletemin(T1,T2,X,B) ==> bstree(T1,B1), bstree(T2,B2),
%             treecount(X,T1,T1M), treecount(X,T2,T2M) => constr(true).
% ==========================================================
:- query ff1/0.
% ==========================================================

%  Catamorphic abstraction

:- cata_abs tree(int) ==> bstree(T1,B1), treecount(Z,T1,T1M).

% =================================================================