:- pred constr(bool). 
:- mode constr(in). 
:- ignore constr/1.
:- type tree(int) ---> leaf ; node( int, tree(int), tree(int) ).
%                 empty tree     key  left-subtree right-subtree
% Note: duplicates are NOT allowed.   
% ==========================================================
% Program. 
% Binary Search Tree 
% https://algs4.cs.princeton.edu/32bst/
:- pred bstdeletemin(tree(int),tree(int),int,bool).          
:- mode bstdeletemin(in,out,out,out).
                           % error: X=0 & IsDef should be X=0 & ~IsDef
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). 

% ==========================================================
% bstree checks whether or not a tree is a binary search tree.
:- pred bstree(tree(int),bool).
:- mode bstree(in,out).
:- cata bstree/2-1.

bstree(leaf,B) :- constr(B).   % NO duplicates. 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). 
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)

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

treesize(leaf,S) :- S=0. 
treesize(node(A,L,R),S) :- S=LS+RS+1,
    treesize(L,LS), treesize(R,RS).

%%---- 
%% checking whether or not a binary tree is a leaf.
:- pred is_leaf(tree(int),bool).
:- mode is_leaf(in,out).
:- cata is_leaf/2-1.

is_leaf(leaf,B) :- constr(B).   
is_leaf(node(A,L,R),B) :- constr(~B).
    
% ==========================================================
% Contract on bstdeletemin:
% Deleting the minimum from leaf keeps leaf unchanged.
% Deleting the minimum from node(A,L,R) of size S  
% generates a bstree of size S-1.
%Verification.
:- pred ff1.
ff1 :- 
  constr(~((((IsDef & BIn) & BOut) => (SOut=ite(LeafB,SIn,SIn-1))) & 
                  (SIn=0 => SOut=0) )), 
        bstree(BstIn,BIn), bstree(BstOut,BOut),
        treesize(BstIn,SIn), treesize(BstOut,SOut), 
        is_leaf(BstIn,LeafB),
        bstdeletemin(BstIn,BstOut,Min,IsDef).

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