% =================================================================
:- pred constr(bool).
:- mode constr(in).
:- ignore constr/1.
:- type bintree_int ---> leaf ; node(int,bintree_int,bintree_int).
% This is a binary tree supporting a heap. 
% leaf is the EMPTY bintree_int. Nodes may have DUPLICATE integer values.
% ================================================================
% Program: descending sorting.
:- pred heapsort(list(int),list(int)).
:- mode heapsort(in,out).

heapsort(L,SL) :-
  list_to_heap(L,H), heap_to_list(H,SL).
  
% ===============================================================
% making a heap out of a list.
% Program predicate: not be a catamorphism.
:- pred list_to_heap(list(int),bintree_int).
:- mode list_to_heap(in,out).

list_to_heap([],leaf).
list_to_heap([X|Xs], Heap) :-
  list_to_heap(Xs, HeapXs), 
  insert_heap(X, HeapXs, Heap).

% ------- % descending heap
:- pred insert_heap(int,bintree_int,bintree_int).
:- mode insert_heap(in,in,out).

insert_heap(X, leaf, node(X,leaf,leaf)).
insert_heap(X, node(Top,L,R), node(Top,R,L1)) :- % Torsion! node(Top,R,L1), not node(Top,L1,R), and
         constr(X=<Top), insert_heap(X,L,L1).   % top unchanged. Insert X in the left son-node.
insert_heap(X, node(Top,L,R), node(X,R,L1)) :-   % Torsion! node(Top,R,L1), not node(Top,L1,R), and
         constr(X>Top), insert_heap(Top,L,L1).  % X on top. Insert Top in the left son-node.
        
%% ------- % ascending heap
%:- pred insert_heap(int,bintree_int,bintree_int).
%:- mode insert_heap(in,in,out).
%
%insert_heap(X, leaf, node(X,leaf,leaf)).
%insert_heap(X, node(Top,L,R), node(Top,R,L1)) :- % Torsion! node(Top,R,L1), not node(Top,L1,R), and
%          constr(X>Top), insert_heap(X,L,L1).    % Top unchanged. Insert X in the left son-node.
%insert_heap(X, node(Top,L,R), node(X,R,L1)) :-   % Torsion! node(Top,R,L1), not node(Top,L1,R), and
%          constr(X=<Top), insert_heap(Top,L,L1). % X on top. Insert Top in the left son-node.

% ----------------------------------
% Making a weakly-descending list out of a weakly-descending heap.
% Program predicate: need not be a catamorphism.
:- pred heap_to_list(bintree_int,list(int)).
:- mode heap_to_list(in,out).   

heap_to_list(leaf,[]).
heap_to_list(node(Top,leaf,leaf), [Top]).                                    
heap_to_list(node(Top,node(LTop,LL,LR),leaf), [Top|Tail]) :-                   
   mkbtree(LTop,LL,LR,NewHeap),
   heap_to_list(NewHeap,Tail).
heap_to_list(node(Top,leaf,node(RTop,RL,RR)), [Top|Tail]) :-                  
   mkbtree(RTop,RL,RR,NewHeap),
   heap_to_list(NewHeap,Tail).
heap_to_list(node(Top,node(LT,LL,LR),node(RT,RL,RR)), [Top|Tail]) :-        
    mkbtree(LT,LL,LR,NewLHeap), mkbtree(RT,RL,RR,NewRHeap),
    heap_merge(NewLHeap,NewRHeap,MergedHeap),
    heap_to_list(MergedHeap,Tail).

%% ----------------------------------
%% Making a weakly-ascending list out of a weakly-ascending heap.
%% Program predicate: need not be a catamorphism.
%:- pred heap_to_list(bintree_int,list(int)). % visiting from left-to-right
%:- mode heap_to_list(in,out).   
%
%heap_to_list(leaf, []).
%heap_to_list(node(Top,leaf,leaf), [Top]).                                    
%heap_to_list(node(Top,node(LTop,LL,LR),leaf), [Top|Tail]) :-                   
%    mkbtree(LTop,LL,LR,NewHeap),
%    heap_to_list(NewHeap,Tail).
%heap_to_list(node(Top,leaf,node(RTop,RL,RR)), [Top|Tail]) :-                  
%    mkbtree(RTop,RL,RR,NewHeap),
%    heap_to_list(NewHeap,Tail).
%heap_to_list(node(Top,node(LT,LL,LR),node(RT,RL,RR)), [Top|Tail]) :-        
%     mkbtree(LT,LL,LR,NewLHeap), mkbtree(RT,RL,RR,NewRHeap),
%     heap_merge(NewLHeap,NewRHeap,MergedHeap),
%     heap_to_list(MergedHeap,Tail).

% ----------------------------------
:- pred mkbtree(int,bintree_int,bintree_int,bintree_int).
:- mode mkbtree(in,in,in,out).

mkbtree(Top,Left,Right, node(Top,Left,Right)).  

% -----
:- pred heap_merge(bintree_int,bintree_int,bintree_int).
:- mode heap_merge(in,in,out).                % heap_merge is a total function

heap_merge(leaf,leaf, leaf).                           
heap_merge(node(LTop,LL,LR),leaf, node(LTop,LL,LR)).   
heap_merge(leaf,node(RTop,RL,RR), node(RTop,RL,RR)).   
heap_merge(node(LTop,LL,LR),node(RTop,RL,RR), node(RTop,node(LTop,LL,LR),MergedHeap)) :- 
          LTop =< RTop, heap_merge(RL,RR,MergedHeap).
heap_merge(node(LTop,LL,LR),node(RTop,RL,RR), node(LTop,MergedHeap,node(RTop,RL,RR))) :- 
          LTop > RTop, heap_merge(LL,LR,MergedHeap).   

% ===============================================================
% catamorphisms
%----- checking a 'weakly descending' ordered heap:
% every father is smaller than or equal to each of its children.
:- pred is_dheap(bintree_int,bool).
:- mode is_dheap(in,out).
:- cata is_dheap/2-1.

is_dheap(leaf,Res) :- constr( Res ).
is_dheap(node(Top,L,R),Res) :-
    top(L,IsTopL,TopL), top(R,IsTopR,TopR),   
    is_dheap(L,ResL), is_dheap(R,ResR),
    constr(Res=ite((((IsTopL & IsTopR)  & (Top>=TopL & Top>=TopR)) & (ResL & ResR)), true,
       ite((( IsTopL & ~IsTopR) & (Top>=TopL)),  ResL,
       ite(((~IsTopL &  IsTopR) & (Top>=TopR)),  ResR,
       ite( (~IsTopL & ~IsTopR), true, false)))) ).   
       
% --------  top of a binary tree  -----------
:- pred top(bintree_int,bool,int).     
:- mode top(in,out,out).
:- cata top/3-1.

top(leaf,IsDefTop,Top) :- constr( ~IsDefTop & Top=0 ).       % Top can be 0 or any int  
top(node(T,L,R),IsDefTop,Top) :- constr( IsDefTop & Top=T ).  
            
% ----
:- pred is_dsorted(list(int),bool).
:- mode is_dsorted(in,out).
:- cata is_dsorted/2-1.

is_dsorted([],Res) :- constr(Res).
is_dsorted([H|T],Res) :-
    hd(T,IsDefT,HdT),
    is_dsorted(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 ).    % 0 can be any int.
hd([H|T],IsDef,Hd) :- constr( IsDef & Hd=H ).

% ===============================================================
%ff1. Contract on heapsort     
:- pred ff1.
ff1 :- 
  constr(~(SS)), 
% is_dsorted(L,SL),  %% ok also with/without this catamorphism on L
  is_dsorted(S,SS),  
  heapsort(L,S).

%% abstractions:
%       
%:- spec list_to_heap(L,H) ==>
%       is_dsorted(L,NL), is_dheap(H,B) => constr(true).
%  
%:- spec heap_to_list(H,L) ==> 
%       is_dheap(H,BH), is_dsorted(L,BL) => constr(true).
%     
%:- spec insert_heap(X,H,H1) ==> is_dheap(H,BH), is_dheap(H1,BH1) => constr(true).
%       
%:- spec heap_merge(HL,HR,H1) ==>
%        is_dheap(HL,BHL), is_dheap(HR,BHR), is_dheap(H1,BH1) => constr(true).
%       
%:- spec mkbtree(T,HL,HR,H1) ==>  is_dheap(HL,BHL), is_dheap(HR,BHR), is_dheap(HT,BHT)
%           => constr(true). 
%           
%%--- less catamorphisms are also ok (compare with uncommented ones)   
%:- spec list_to_heap(L,H) ==>
%       is_dsorted(L,NL). %, is_dheap(H,B) => constr(true).
%  
%:- spec heap_to_list(H,L) ==> 
%       is_dheap(H,BH). %, is_dsorted(L,BL) => constr(true).
%     
%:- spec insert_heap(X,H,H1) ==>  is_dheap(H,BH) => constr(true).
%   %is_dheap(H,BH), is_dheap(H1,BH1) => constr(true).
%       
%:- spec heap_merge(HL,HR,H1) ==>
%        is_dheap(HL,BHL), is_dheap(HR,BHR), is_dheap(H1,BH1) => constr(true).
%       
%:- spec mkbtree(T,HL,HR,H1) ==>  is_dheap(HL,BHL), is_dheap(HR,BHR), is_dheap(HT,BHT)

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

%  Catamorphic abstraction

:- cata_abs list(int) ==> is_dsorted(T,ResT).
:- cata_abs bintree_int ==> is_dheap(HL,BHL).

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