% =================================================================
:- 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. DUPLICATE integer values ARE ALLOWED.
% ================================================================
% ***** In bodies of program clauses: only variables (not structures), no catamorphisms.
% Program: ascending 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.
% ----------------------------------
% -- 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. 

% ----------------------------------
% Making a weakly-ascending list out of a 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(T,Left,Right)) :- T=Top.  
     
% -----
:- 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 ascending' ordered heap:
% every father is smaller than or equal to each of its children.
:- pred is_aheap(bintree_int,bool).
:- mode is_aheap(in,out).
:- cata is_aheap/2-1.

is_aheap(leaf,Res) :- constr( Res ).
is_aheap(node(Top,L,R),Res) :-
    top(L,IsTopL,TopL), top(R,IsTopR,TopR),   
    is_aheap(L,ResL), is_aheap(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)))) ).   

%----- checking a weakly ascending ordered list
:- pred is_asorted(list(int),bool).
:- mode is_asorted(in,out).
:- cata is_asorted/2-1.

is_asorted([],Res) :- constr( Res ).
is_asorted([H|T],Res) :-
    hd(T,IsDefT,HdT),
    is_asorted(T,ResT), 
    constr(ite(IsDefT,ite(H=<HdT,Res=ResT,Res=false),Res=true)). 
    
% --------  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 ).  
            
% --- head of list ---
:- pred hd(list(int),bool,int).
:- mode hd(in,out,out).
:- cata hd/3-1.

hd([],IsDef,Hd) :- constr( ~IsDef & Hd=0 ).      % Hd can be any int
hd([H|T],IsDef,Hd) :- constr( IsDef & Hd=H ).

% ===============================================================
% Prove contracts of program predicates, not of catamorphisms.
:- pred ff1.
ff1 :-
  constr(~(B)),
  is_asorted(S,B),
  heapsort(L,S).
% ----------------------------------------------------------------            
% Contract on list_to_heap:            %   
:- pred ff2.     
ff2 :-
  constr( ~(B)), is_aheap(H,B),
  list_to_heap(L,H).
% ----------------------------------------------------------------            
% Contract on insert_heap:               
:- pred ff3.     
ff3 :-
  constr( ~(BH => BH1)), 
  is_aheap(H,BH), is_aheap(H1,BH1),
  insert_heap(A,H,H1).
% ----------------------------------------------------------------            
% Contract on heap_to_list:           . 
:- pred ff4.                 
ff4 :-
  constr( ~( (BH => BL) & (Top=HdL))),
  % top(H,IsDefTop,Top),   hd(L,IsDef,HdL) or is_aheap(H,Bout) do not work
  %%%% NOTE THIS CATA "top" %%%%%%%%%%%%%% To be investigated.
  % for Cata it has been investigated by Ema.
  % The presence of this catamorphism produces 4-sat:
  % otherwise in MQ: Mono:unsat--Mono:sat--Poly:unsat--Poly:sat
  top(H,IsDefTop,Top), hd(L,IsDef,HdL), % this is required for 4-sat.  
  is_aheap(H,BH), is_asorted(L,BL), 
  heap_to_list(H,L).
% *************  SAY SOMETHING ABOUT top FOR heap_to_list OR heap_merge IS NECESSARY
% *************  TO GET 4-sat.  THIS VERSION GETS 4-sat.
% ----------------------------------------------------------------
% Contract on heap_merge:
:- pred ff5.    
ff5 :-
  constr(~(((BHL & BHR) => BHT) ) ),
  is_aheap(HL,BHL), is_aheap(HR,BHR), is_aheap(HT,BHT),
  heap_merge(HL,HR,HT).
%----------------------------------------------------------------   
:- pred ff6.   
ff6 :-
 constr(~( (((  ((( IsDefTopL & IsDefTopR) & (T=<TopL & T=<TopR)) => ((BHL & BHR) => BHT)) 
             &  (((( IsDefTopL & ~IsDefTopR) & T=<TopL) & BHL) => BHT)            
             ) &  (((~IsDefTopL &  IsDefTopR) & (T=<TopR & BHR)) => BHT) 
             ) &  ((~IsDefTopL & ~IsDefTopR) => BHT)
             ) &  (T=TopHT))),  
 is_aheap(HL,BHL), is_aheap(HR,BHR), is_aheap(HT,BHT),
 top(HL,IsDefTopL,TopL), top(HR,IsDefTopR,TopR), top(HT,IsDefTopHT,TopHT),
 mkbtree(T,HL,HR,HT).
% ===============================================================
:- query ff1/0. 
:- query ff2/0. 
:- query ff3/0. 
:- query ff4/0. 
:- query ff5/0. 
:- query ff6/0. 
% ===============================================================