--Sort.d

--generic sorting package sana assertions
--adapted on 1/1/99 from the LRM of 12/9/91 by brl

face Sort[rt n ar atMost] is

	required
		type rt 		--the record type of the array to be sorted
		variable n : integer		--the length of the array
		type ar is array [1..n] of rt		--the array type
		function atMost(a:rt,b:rt) return boolean	--is a<=b?
	end required
	
procedure sort(original:ar,final:ar,low:integer,high:integer)
	--add assertions to declarations in package's grammar

end face	--of Sort


body partitionSort:Sort[rt n ar atMost] is

	required
		type rt 		--the record type of the array to be sorted
		variable n : integer		--the length of the array
		type ar is array [1..n] of rt		--the array type
		function atMost(left:rt,right:rt) return boolean	--is a<=b?
	end required
	
procedure sort(original:array [1..n] of rt, final:array [1..n] of rt, low:integer, high:integer) is
	declare
	--nested procedure
	procedure partition(i:integer,j:integer,a:spread array [1..n] of rt,b:spread array [1..n] of rt,k:integer) is
		declare	
			variable lowIndex : shared integer := i;
			variable highIndex : shared integer := j;
			variable h : integer := (i+j)/2;	--pick pivot from middle
		begin		--of partition
			forall t:integer in i..j
			begin
				if
					atMost(a[t],a[h]) =>	--is this element smaller than pivot?
						declare 
							variable s:integer
						begin
							fetchadd(lowIndex,1,s)
							;
							b[s] := a[t]
						end
				[]
					atMost(a[h],a[t]) =>	--is this element bigger than pivot?
						declare 
							variable s:integer
						begin
							fetchadd(highIndex,-1,s)
							;
							b[s] := a[t]
						end
				fi
			end	--of forall t
			;
			k := highIndex
		end	--of partition
		
	--variables for sort body
	variable inter : spread ar
	variable pivot : integer
	
	begin		--of sort body
		if
			low=high => final[low] := original[low]		--just one? then done
		[]
			low<high =>
				begin		--partition then sort again
					partition(low,high,original,inter,pivot)
					;
					sort(inter,final,low,(pivot-1))	--sort lower half
					&
					sort(inter,final,pivot,high)	--sort lower half
				end	--of partition then sort again
		fi
	end 		--of sort
	
end body	--partitionSort:Sort