note
	description: "[
		Quicksort according to Lamport/Meyer.
		The Lampsort algorithm is a simple loop; it does not use recursion, 
		but relies on an interesting data structure, a set of intervals. 
		It is hardly more difficult to understand, 
		and hardly shorter, than the traditional recursive version.
		the recursive version, and its parallelized variants, 
		are only examples of possible implementations
	]"
	author: "JSO"
	date: "$Date$"
	revision: "$Revision$"

class interface
	LAMPSORT [G -> COMPARABLE]

create 
	make (l_a: like a)
		ensure
				a = l_a

feature -- Access

	generating_type: TYPE [detachable LAMPSORT [G]]
			-- Type of current object
			-- (type of which it is a direct instance)
			-- (from ANY)
		ensure -- from ANY
			generating_type_not_void: Result /= Void

	generator: STRING_8
			-- Name of current object's generating class
			-- (base class of the type of which it is a direct instance)
			-- (from ANY)
		ensure -- from ANY
			generator_not_void: Result /= Void
			generator_not_empty: not Result.is_empty
	
feature -- Comparison

	frozen deep_equal (a: detachable ANY; b: like arg #1): BOOLEAN
			-- Are a and b either both void
			-- or attached to isomorphic object structures?
			-- (from ANY)
		ensure -- from ANY
			instance_free: class
			shallow_implies_deep: standard_equal (a, b) implies Result
			both_or_none_void: (a = Void) implies (Result = (b = Void))
			same_type: (Result and (a /= Void)) implies (b /= Void and then a.same_type (b))
			symmetric: Result implies deep_equal (b, a)

	frozen equal (a: detachable ANY; b: like arg #1): BOOLEAN
			-- Are a and b either both void or attached
			-- to objects considered equal?
			-- (from ANY)
		ensure -- from ANY
			instance_free: class
			definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.is_equal (b))

	frozen is_deep_equal (other: LAMPSORT [G]): BOOLEAN
			-- Are Current and other attached to isomorphic object structures?
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
		ensure -- from ANY
			shallow_implies_deep: standard_is_equal (other) implies Result
			same_type: Result implies same_type (other)
			symmetric: Result implies other.is_deep_equal (Current)

	is_equal (other: LAMPSORT [G]): BOOLEAN
			-- Is other attached to an object considered
			-- equal to current object?
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
		ensure -- from ANY
			symmetric: Result implies other ~ Current
			consistent: standard_is_equal (other) implies Result

	frozen standard_equal (a: detachable ANY; b: like arg #1): BOOLEAN
			-- Are a and b either both void or attached to
			-- field-by-field identical objects of the same type?
			-- Always uses default object comparison criterion.
			-- (from ANY)
		ensure -- from ANY
			instance_free: class
			definition: Result = (a = Void and b = Void) or else ((a /= Void and b /= Void) and then a.standard_is_equal (b))

	frozen standard_is_equal (other: LAMPSORT [G]): BOOLEAN
			-- Is other attached to an object of the same type
			-- as current object, and field-by-field identical to it?
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
		ensure -- from ANY
			same_type: Result implies same_type (other)
			symmetric: Result implies other.standard_is_equal (Current)
	
feature -- Status report

	conforms_to (other: ANY): BOOLEAN
			-- Does type of current object conform to type
			-- of other (as per Eiffel: The Language, chapter 13)?
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void

	same_type (other: ANY): BOOLEAN
			-- Is type of current object identical to type of other?
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
		ensure -- from ANY
			definition: Result = (conforms_to (other) and other.conforms_to (Current))
	
feature -- Duplication

	copy (other: LAMPSORT [G])
			-- Update current object using fields of object attached
			-- to other, so as to yield equal objects.
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
			type_identity: same_type (other)
		ensure -- from ANY
			is_equal: Current ~ other

	frozen deep_copy (other: LAMPSORT [G])
			-- Effect equivalent to that of:
			--		copy (other . deep_twin)
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
		ensure -- from ANY
			deep_equal: deep_equal (Current, other)

	frozen deep_twin: LAMPSORT [G]
			-- New object structure recursively duplicated from Current.
			-- (from ANY)
		ensure -- from ANY
			deep_twin_not_void: Result /= Void
			deep_equal: deep_equal (Current, Result)

	frozen standard_copy (other: LAMPSORT [G])
			-- Copy every field of other onto corresponding field
			-- of current object.
			-- (from ANY)
		require -- from ANY
			other_not_void: other /= Void
			type_identity: same_type (other)
		ensure -- from ANY
			is_standard_equal: standard_is_equal (other)

	frozen standard_twin: LAMPSORT [G]
			-- New object field-by-field identical to other.
			-- Always uses default copying semantics.
			-- (from ANY)
		ensure -- from ANY
			standard_twin_not_void: Result /= Void
			equal: standard_equal (Result, Current)

	frozen twin: LAMPSORT [G]
			-- New object equal to Current
			-- twin calls copy; to change copying/twinning semantics, redefine copy.
			-- (from ANY)
		ensure -- from ANY
			twin_not_void: Result /= Void
			is_equal: Result ~ Current
	
feature -- Basic operations

	frozen default: detachable LAMPSORT [G]
			-- Default value of object's type
			-- (from ANY)

	frozen default_pointer: POINTER
			-- Default value of type POINTER
			-- (Avoid the need to write p.default for
			-- some p of type POINTER.)
			-- (from ANY)
		ensure -- from ANY
			instance_free: class

	default_rescue
			-- Process exception for routines with no Rescue clause.
			-- (Default: do nothing.)
			-- (from ANY)

	frozen do_nothing
			-- Execute a null action.
			-- (from ANY)
		ensure -- from ANY
			instance_free: class
	
feature 

	a: ARRAY [G]

	lampsort (i, j: INTEGER_32)
		require
				a.lower <= i
				i <= j
				j <= a.upper

	make (l_a: like a)
		ensure
				a = l_a

	partition (i, j: INTEGER_32)
		require
				a.lower <= i
				i <= j
				j <= a.upper
		ensure
				i - 1 <= pivot1 and pivot1 <= j
				i <= pivot2 and pivot2 <= j + 1
				permutation (a, a.deep_twin)
				across
					i |..| pivot1 as it
				all
					across
						(pivot1 + 1) |..| j as jt
					all
						a [it.item] <= a [jt.item]
					end
				end
				across
					i |..| (pivot2 - 1) as it
				all
					across
						pivot2 |..| j as jt
					all
						a [it.item] <= a [jt.item]
					end
				end

	picked: INTEGER_INTERVAL

	pivot1: INTEGER_32

	pivot2: INTEGER_32

	sort
			-- Lampsort version of quicksort for array a
		ensure
				across
					a.lower |..| (a.upper - 1) as k
				all
					a [k.item] <= a [k.item + 1]
				end
				permutation (old a.deep_twin, a)

	sort2
			-- recursive quicksort
		ensure
				across
					a.lower |..| (a.upper - 1) as k
				all
					a [k.item] <= a [k.item + 1]
				end
				permutation (old a.deep_twin, a)

	sort_recursive (i, j: INTEGER_32)
		require
				a.lower <= i
				i <= j + 1
				j <= a.upper

	swap (m, n: INTEGER_32)
		require
				a.lower <= m
				m <= n
				n <= a.upper
		ensure
				a [m] ~ old a [n] and a [n] ~ old a [m]
	
feature -- Output

	Io: STD_FILES
			-- Handle to standard file setup
			-- (from ANY)
		ensure -- from ANY
			instance_free: class
			io_not_void: Result /= Void

	out: STRING_8
			-- New string containing terse printable representation
			-- of current object
			-- (from ANY)
		ensure -- from ANY
			out_not_void: Result /= Void

	print (o: detachable ANY)
			-- Write terse external representation of o
			-- on standard output.
			-- (from ANY)
		ensure -- from ANY
			instance_free: class

	frozen tagged_out: STRING_8
			-- New string containing terse printable representation
			-- of current object
			-- (from ANY)
		ensure -- from ANY
			tagged_out_not_void: Result /= Void
	
feature -- Platform

	Operating_environment: OPERATING_ENVIRONMENT
			-- Objects available from the operating system
			-- (from ANY)
		ensure -- from ANY
			instance_free: class
			operating_environment_not_void: Result /= Void
	
feature -- array queries

	permutation (a1, a2: like a): BOOLEAN
		ensure
				Result implies a1.count = a2.count and then across
					a1 as it
				all
					a1.occurrences (it.item) = a2.occurrences (it.item)
				end
				not Result implies a1.count /= a2.count or else (across
					a1 as it
				some
					a1.occurrences (it.item) /= a2.occurrences (it.item)
				end)
	
invariant
		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)

end -- class LAMPSORT

Generated by ISE EiffelStudio