% =================================================================
:- 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 btree. 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.
:- 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).

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

insert_heap(X, leaf, node(X1,leaf,leaf)) :- constr(X=X1).
insert_heap(X, node(Top,L,R), node(Top1,R,L1)) :-   % Torsion! node(Top,R,L1), not node(Top,L1,R), and
    constr(Top1=Top & X=<Top), insert_heap(X,L,L1). % top unchanged. Insert X in the left son-node.
insert_heap(X, node(Top,L,R), node(X1,R,L1)) :-     % Torsion! node(Top,R,L1), not node(Top,L1,R), and
    constr(X=X1 & X>Top), insert_heap(Top,L,L1).    % X on top. Insert Top in the left son-node.
% ----------------------------------
% -- The NEW insertion is done, in an alternate way,
% -- into the left child and into the right child.
% -- The resulting heap is **balanced** (as it should be for complexity reasons in heapsort), that is,
% -- the depths of any two leaves differ at most by 1 unit.
% In the last level of the heap, the leaves are not necessarily contiguous, i.e.,
% they are not necessarily flushed to the left or to the right of the frontier of the tree

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

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

% ----------------------------------
% Making a weakly-descending list out of a heap.
:- 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).

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

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.
%-----  listcount --- 3rd arg: how many X's in a list
:- pred listcount(int,list(int),int).
:- mode listcount(in,in,out).
:- cata listcount/3-2.

listcount(X,[],Res) :- constr( Res=0 ).
listcount(X,[H|T],Res) :-
   constr( Res=ite(X=H,ResT+1,ResT) ),
   listcount(X,T,ResT).

%-----  btreecount --- 3rd arg: how many X's in a binary heap.
:- pred btreecount(int,bintree_int,int).
:- mode btreecount(in,in,out).
:- cata btreecount/3-2.         

btreecount(X,leaf,Res) :- constr( Res=0 ).
btreecount(X,node(A,L,R),Res) :-
    constr(Res=ite(X=A,(ResL+ResR+1),(ResL+ResR))),
    btreecount(X,L,ResL),
    btreecount(X,R,ResR).

% ===============================================================
% ff1. Contract on heapsort: length         
:- pred ff1.        
ff1 :-
   constr(~(NL=NS)),
   listcount(X,L,NL), listcount(X,S,NS),
   heapsort(L,S).
% ----------------
% Contract on list_to_heap:               
:- pred ff11.      
ff11 :-
    constr( ~(NL=NH)), listcount(X,L,NL), btreecount(X,H,NH),
    list_to_heap(L,H).
% ------------------
% Contract on heap_to_list:           
:- pred ff12.                 
ff12 :-
    constr( ~(NH=NL)),
    btreecount(X,H,NH), listcount(X,L,NL), 
    heap_to_list(H,L).
% ------------------ 
% Contract on insert_heap:               
:- pred ff2.      
ff2 :-
    constr( ~(NH1=ite(X=A,NH+1,NH))), 
    btreecount(X,H,NH), btreecount(X,H1,NH1),
    insert_heap(A,H,H1).
% ------------------------
% Contract on heap_merge:                            
:- pred ff3.    
ff3 :-
   constr(~(SHL + SHR = SH1)),
   btreecount(X,HL,SHL), btreecount(X,HR,SHR), btreecount(X,H1,SH1),
   heap_merge(HL,HR,H1).
%----------------------------------------------------------------
% Contract on mkbtree:                     
          
:- pred ff4.    
ff4 :-
   constr(~(SH1 = ite(X=T,SHL+SHR+1,SHL+SHR))),
   btreecount(X,HL,SHL), btreecount(X,HR,SHR), btreecount(X,H1,SH1),
   mkbtree(T,HL,HR,H1).

% ===============================================================
:- query ff1/0.
:- query ff11/0.
:- query ff12/0.
:- query ff2/0.
:- query ff3/0.
:- query ff4/0.
% ===============================================================

% --------------------------------------------------