% ================================================================= :- 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. % ================================================================ % 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(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-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 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 descending' ordered heap: % every father is larger 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)))) ). %----- checking a weakly descending ordered list :- 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(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 ). % -------- maximum of a binary tree ----------- :- pred bintree_max(bintree_int,bool,int). :- mode bintree_max(in,out,out). :- cata bintree_max/3-1. bintree_max(leaf,IsDefMax,Max) :- constr(~IsDefMax & Max=0). % Max can be 0 or any int bintree_max(node(T,L,R),IsDefMax,Max) :- bintree_max(L,IsDefLM,LM), bintree_max(R,IsDefRM,RM), constr(IsDefMax & (((((~IsDefLM & ~IsDefRM) => Max=T) & (( IsDefLM & ~IsDefRM) => Max=ite(T>=LM,T,LM) )) & ((~IsDefLM & IsDefRM) => Max=ite(T>=RM,T,RM) )) & (( IsDefLM & IsDefRM) => Max=ite(T>=LM, ite(T>=RM,T,RM), ite(LM>=RM,LM,RM)) ))). % --- 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. % ff1. Contract on heapsort: sortedness :- pred ff1. ff1 :- constr(~(B)), is_dsorted(S,B), heapsort(L,S). % ---------------------------------------------------------------- % Contract on list_to_heap: :- pred ff11. ff11 :- constr( ~(B)), is_dheap(H,B), list_to_heap(L,H). % ---------------------------------------------------------------- % Contract on insert_heap: :- pred ff2. ff2 :- constr( ~(BH => BH1)), is_dheap(H,BH), is_dheap(H1,BH1), insert_heap(A,H,H1). % ---------------------------------------------------------------- % Contract on heap_to_list: :- pred ff12. ff12 :- constr( ~( (BH => BL))), top(H,IsDefTop,Top), %%%% NOTE THIS CATA %%%%%%%%%%%%%%%%%%%%% To be investigated for multiquery. % for Cata it has been investigated by Ema. % The presence of this catamorphism is required for ff12 is_dheap(H,BH), is_dsorted(L,BL), heap_to_list(H,L). % ---------------------------------------------------------------- % Contract on heap_merge: :- pred ff3. ff3 :- constr(~((BHL & BHR) => BH1)), is_dheap(HL,BHL), is_dheap(HR,BHR), is_dheap(H1,BH1), heap_merge(HL,HR,H1). %---------------------------------------------------------------- :- pred ff4. ff4 :- 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) ))) ), is_dheap(HL,BHL), is_dheap(HR,BHR), is_dheap(HT,BHT), top(HL,IsDefTopL,TopL), top(HR,IsDefTopR,TopR), top(HT,IsDefTopHT,TopHT), mkbtree(T,HL,HR,HT). % =============================================================== :- query ff1/0. :- query ff11/0. :- query ff12/0. :- query ff2/0. :- query ff3/0. :- query ff4/0. % ===============================================================