:- pred constr(bool). 
:- mode constr(in). 
:- ignore constr/1.

:- type tree(int) ---> leaf ; node( int, tree(int), tree(int) ).
% ==========================================================
% Program. 
% Binary Search Tree - duplicates not allowed
%%%%%%%  TREE VISIT %%%%%%%
:- pred visit(tree(int),list(int)). % pre-order tree visitor
:- mode visit(in,out).
visit(leaf,[]).
visit(node(A,L,R), Xs) :-
  visit(L,XL),
  visit(R,XR),
  concat4(XL,A,XR,Xs).

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

% checking the strictly ascending order of the elements of a list
:- pred is_str_asorted(list(int),bool).
:- mode is_str_asorted(in,out).
:- cata is_str_asorted/2-1.

is_str_asorted([],Res) :- constr(Res).
is_str_asorted([H|T],Res) :-
    hd(T,IsDefT,HdT),
    is_str_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 ).    % Any int value for Hd
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)) ).
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)) ).
listmax([H|T],IsDef,Max) :-
         constr(( IsDef & (Max = ite(IsDefT, ite(H>MaxT,H,MaxT), H)) )),
         listmax(T,IsDefT,MaxT).

% ==========================================================
% Verification
:- pred ff1.
ff1 :-
% constr( ~((B1 => B2) & (MinT=MinL & MaxT=MaxL)) ),
  constr( ~(B1 => B2) ),
  bstree(T,B1),
  is_str_asorted(L,B2),
 % treemin(T,IsDefT1,MinT), treemax(T,IsDefT2,MaxT), % Extra catas
 % listmin(L,IsDefL1,MinL), listmax(L,IsDefL2,MaxL), % Extra catas 
  visit(T,L).
  
%:- pred ff2.
%ff2 :- 
%      constr(~( ((( (IsDefXs  & (IsDefYs & (MaxXs<Y & Y<MinYs))) v
%                 (~IsDefXs & (IsDefYs & Y<MinYs)))        v
%                 (IsDefXs  & (~IsDefYs & (MaxXs<Y))))     v
%                 (~IsDefXs & ~IsDefYs))
%                  => ((B3 & B4) = B5) )),
%      is_str_asorted(Xs,B3), is_str_asorted(Ys,B4), is_str_asorted(Zs,B5), 
%      listmax(Xs,IsDefXs,MaxXs), listmin(Ys,IsDefYs,MinYs),
%      concat4(Xs,Y,Ys,Zs).
% ==========================================================
:- query ff1/0.
%:- query ff2/0.
% ==========================================================

%  Catamorphic abstraction

:- cata_abs tree(int) ==> bstree(T1,B1).
:- cata_abs list(int) ==> is_str_asorted(L,B2),
                          listmax(L,IsDefMax,MaxL), 
                          listmin(L,IsDefMin,MinL).
%    
% Timeout (30s) for Z3 and Eldarica if not listmax and listmin 
% in the previous two lines, 
% the two "Extra catas" lines above being commented.
% ===========================================================