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

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

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

:- 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.
% --- min of a list
:- 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).
%----
% treemin for ANY binary tree (ok also for trees with duplicate values)
:- pred treemin(bintree_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) 

% ===============================================================
%ff1. Contract on heapsort        
:- pred ff1. 
ff1 :- 
    constr( ~((IsDefLMin = IsDefSMin) & 
    ((IsDefLMin & IsDefSMin) => (MinL=MinS)) )), 
    listmin(L,IsDefLMin,MinL),  
    listmin(S,IsDefSMin,MinS), 
    heapsort(L,S).
%% ---------------
% contract on list_to_heap:   (postcondition: true)            
:- spec list_to_heap(L,H) ==>
   listmin(L,B,NL), treemin(H,B1,NH).
   
% ------------------
% Contract on heap_to_list: (postcondition: true)   
:- spec heap_to_list(H,L) ==> 
   treemin(H,B,SH), listmin(L,B1,LL).
   
% ------------------ 
% Contract on insert_heap:            (postcondition: true)       
:- spec insert_heap(X,H,H1) ==>
   treemin(H,B,SH), treemin(H1,B1,SH1).
   
% ----------------------------------------------------------------
% Contract on heap_merge:             (postcondition: true)             
:- spec heap_merge(HL,HR,H1) ==>
   treemin(HL,B1,SHL), treemin(HR,B2,SHR), treemin(H1,B3,SH1).
%----------------------------------------------------------------
% Contract on mkbtree:                  (postcondition: true)        
:- spec mkbtree(T,HL,HR,H1) ==> 
   treemin(HL,B1,SHL), treemin(HR,B2,SHR), treemin(H1,B3,SH1).

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