% =================================================================
:- pred constr(bool).
:- mode constr(in).
:- ignore constr/1.
% =================================================================
% Program
% rev2(L,R): 
% list R is obtaining by reversing twice list L. We have L=R.
:- pred rev2(list(int),list(int)).
:- mode rev2(in,out).

rev2([],R) :- rev(EL,S), rev(S,R), emptylist(EL).
rev2([H|T],R) :- cons(H,T,HT), rev(HT,S), rev(S,R).

% rev(L,R): 
% list R is the reversal of list L
:- pred rev(list(int),list(int)).
:- mode rev(in,out).

rev([],[]).
rev([H|T],R) :-
  rev(T,S),
  snoc(S,H,R).

% snoc(L,X,S): 
% list S is obtained by inserting the element X at the end of list L
:- pred snoc(list(int),int,list(int)).
:- mode snoc(in,in,out).

snoc([],X,[X]).
snoc([X|Xs],Y,[X|Zs]) :-
  snoc(Xs,Y,Zs).
  
:- pred emptylist(list(int)).
:- mode emptylist(in,in,out).
emptylist([]).

:- pred cons(int,list(int),list(int)).
:- mode cons(in,in,out).
cons(H,T,[H|T]).

% =================================================================
% Catamorphisms
% ------ hd(L,IsDef,Hd): IsDef is true iff L is a nonempty list and
% if IsDef=true then Hd is the head of L
:- 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)). 

% ------ isASorted(L,Res):  
% Res= true iff L is weakly-ascending.
:- pred isASorted(list(int),bool).   
:- mode isASorted(in,out). 
:- cata isASorted/2-1.

isASorted([],Res) :- constr(Res).
isASorted([H|T],Res) :-
    hd(T,IsDefT,HdT), 
    isASorted(T,ResT),
    constr(Res = (IsDefT => (H=<HdT & ResT))).
    
% ------ isDSorted(L,Res): 
% Res= true iff L is weakly-descending.
:- pred isDSorted(list(int),bool).   
:- mode isDSorted(in,out). 
:- cata isDSorted/2-1.

isDSorted([],Res) :- constr(Res).
isDSorted([H|T],Res) :-
    hd(T,IsDefT,HdT), 
    isDSorted(T,ResT),
    constr(Res = (IsDefT => (H>=HdT & ResT))).

% ------ listMin(L,IsDef,Min):  IsDef=true iff L is a nonempty list and
%    if IsDef then Min is the minimum element on the list L
:- pred listMin(list(int),bool,int).  
:- mode listMin(in,out,out).  
:- cata listMin/3-1.

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

% ------ listMax(L,IsDef,Max):  IsDef=true iff L is a nonempty list and
% if IsDef then Max is the maximum element on the list L
:- pred listMax(list(int),bool,int).  
:- mode listMax(in,out,out).  
:- cata listMax/3-1.

listMax([],IsDef,Max) :- constr( (~IsDef) & Max=0 ).    % 0 can be any int.
listMax([H|T],IsDef,Max) :-  
     listMax(T,IsDefT,MaxT),  
     constr( (IsDef & (Max = ite(IsDefT, ite(H>MaxT, H, MaxT), H ) ) ) ).    

% =================================================================
% ------ Verification of contract on rev2: 
% If list R is the twice-reverse of list L then 
% L is weakly-descending iff R is weakly-descending    
:- pred ff1.
ff1 :-
  constr( ~(DL=DR) ), 
  isDSorted(L,DL),
  rev2(L,R),
  isDSorted(R,DR).

% ------ Verification of contract on rev:  

:- pred ff2.
ff2 :-
    constr( ~( (DL=AR) & (AL=DR) ) ), 
    isDSorted(L,DL), isASorted(L,AL),
    rev(L,R),
    isASorted(R,AR), isDSorted(R,DR).


% ------ Verification of contracts on snoc: 
% for a weakly-descending or weakly-ascending list A
:- pred ff3.
ff3 :- 
  constr(~( (DC=(IsDef => (DA & X=<Min))) & ( AC=(IsDef => (AA & X>=Max))) )),
  isDSorted(A,DA), listMin(A,IsDef,Min), isDSorted(C,DC),
  isASorted(A,AA), listMax(A,IsDef,Max), isASorted(C,AC),
  snoc(A,X,C). 

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