note
	description: "RELATION data structure for both specification and implementation."
	author: "JSO and JW"
	date: "$Date$"
	revision: "$Revision$"

class interface
	REL [G -> attached ANY, H -> attached ANY]

create 
	make_empty,
	make_from_tuple_array

convert
	make_from_tuple_array ({attached ARRAY [TUPLE [G, H]]})

feature -- Constructor

	make_from_tuple_array (a: ARRAY [TUPLE [fst: G; snd: H]])
	
feature -- Conversion to array.

	as_array: ARRAY [TUPLE [G, H]]
		ensure
				Current ~ create {REL [G, H]}.make_from_tuple_array (Result)
	
feature -- Commands for relational operations

	domain_restrict (ds: SET [G])
			-- Keep all pairs whose first values are members of 'ds'.
		ensure
			new_rel_is_a_subset: Current |<: (old Current.deep_twin)
			only_ds_in_new_rel: ((old Current.deep_twin) |\ (Current)).domain ~ (old Current.deep_twin.domain |\ ds)

	domain_restrict_by (g: G)
			-- Keep pairs whose first values are 'd'.
		ensure
			new_rel_is_a_subset: Current |<: (old Current.deep_twin)
			only_g_in_new_rel: ((old Current.deep_twin) |\ (Current)).domain ~ (old Current.deep_twin.domain |\ singleton_g (g))

	range_restrict (rs: SET [H])
			-- Keep all pairs whose second values are members of 'rs'.
		ensure
			new_rel_is_a_subset: Current |<: (old Current.deep_twin)
			only_rs_in_new_rel: ((old Current.deep_twin) |\ (Current)).range ~ (old Current.deep_twin.range |\ rs)

	range_restrict_by (h: H)
			-- Keep all pairs whose second values are 'h'.
		ensure
			new_rel_is_a_subset: Current |<: (old Current.deep_twin)
			only_h_in_new_rel: ((old Current.deep_twin) |\ (Current)).range ~ (old Current.deep_twin.range |\ singleton_h (h))

	domain_subtract (ds: SET [G])
			-- Subtract all pairs whose first values are members of 'ds'.
		ensure
			new_rel_is_a_subset: Current |<: (old Current.deep_twin)
			no_ds_in_new_rel: ((old Current.deep_twin) |\ (Current)).domain ~ ds.comprehension (agent in_domain (?, (old Current.deep_twin).domain))

	domain_subtract_by (g: G)
			-- Subtract pairs whose first values are 'g'.
		ensure
			new_rel_is_a_subset: Current |<: (old Current.deep_twin)
			no_g_in_new_rel: ((old Current.deep_twin) |\ (Current)).domain ~ singleton_g (g).comprehension (agent in_domain (?, (old Current.deep_twin).domain))

	range_subtract (rs: SET [H])
			-- Subtract all pairs whose second values are members of 'rs'.
		ensure
			new_rel_is_a_subset: Current |<: (old Current.deep_twin)
			no_rs_in_new_rel: ((old Current.deep_twin) |\ (Current)).range ~ rs.comprehension (agent in_range (?, (old Current.deep_twin).range))

	range_subtract_by (h: H)
			-- Subtract pairs whose second values are 'h'.
		ensure
			new_rel_is_a_subset: Current |<: (old Current.deep_twin)
			no_h_in_new_rel: ((old Current.deep_twin) |\ (Current)).range ~ singleton_h (h).comprehension (agent in_range (?, (old Current.deep_twin).range))

	override (r: like Current)
			-- Update current relation such that it aggres on 'r'.
		ensure
				Current ~ ((old Current.deep_twin |<< r.domain) |\/| r)

	override_by (t: TUPLE [g: G; h: H])
			-- Update current relation such that it aggres on 'g |-> h'.
		ensure
				Current ~ ((old Current.deep_twin @<< t.g) |\/| singleton_gh (t.g, t.h))
	
feature -- Status queries

	is_function: BOOLEAN
			-- Is current relation a function?
			-- i.e., each domain value maps to at most one value.
		ensure
				Result = across
					domain as d
				all
					# image (d.item) = 1
				end

	is_injection: BOOLEAN
			-- Is current relation an injective function?
			-- i.e., no two domain values map to the same range vaule.
		ensure
				Result = (is_function and inverse.is_function)

	domain: SET [G]
			-- Return the domain set of relation.

	range: SET [H]
			-- Return the range set of relation.
	
feature -- Queries for relational operations

	inverse: REL [H, G]
		ensure
			current_rel_unchanged: Current ~ old Current.deep_twin
				Result.inverse.is_equal (Current)

	image alias "[]" (g: G): SET [H]
			-- Retrieve the set of items that are associated with 'g'.
		ensure
			current_rel_unchanged: Current ~ old Current.deep_twin
				Result.is_empty implies not domain.has (g)
				across
					Result as r
				all
					has (create {PAIR [G, H]}.make_from_tuple ([g, r.item]))
				end
				across
					range.differenced (Result) as r
				all
					not has (create {PAIR [G, H]}.make_from_tuple ([g, r.item]))
				end

	domain_restricted alias "|<" (ds: SET [G]): like Current
			-- Return a copy of current relation with
			-- all pairs whose first values are members of 'ds' kept.
		ensure
			current_rel_unchanged: Current ~ old Current.deep_twin
			new_rel_is_a_subset: Result |<: Current
			only_ds_in_new_rel: (Current |\ Result).domain ~ (domain |\ ds)

	domain_restricted_by alias "@<" (g: G): like Current
			-- Return a copy of current relation with
			-- all pairs whose first values are 'g' kept.
		ensure
			current_rel_unchanged: Current ~ old Current.deep_twin
			new_rel_is_a_subset: Result |<: Current
			only_g_in_new_rel: (Current |\ Result).domain ~ (domain |\ singleton_g (g))

	range_restricted alias "|>" (rs: SET [H]): like Current
			-- Return a copy of current relation with
			-- all pairs whose second values are members of 'rs' kept.
		ensure
			current_rel_unchanged: Current ~ old Current.deep_twin
			new_rel_is_a_subset: Result |<: Current
			only_rs_in_new_rel: (Current |\ Result).range ~ (range |\ rs)

	range_restricted_by alias "@>" (h: H): like Current
			-- Return a copy of current relation with
			-- all pairs whose second values are 'h' kept.
		ensure
			current_rel_unchanged: Current ~ old Current.deep_twin
			new_rel_is_a_subset: Result |<: Current
			only_h_in_new_rel: (Current |\ Result).range ~ (range |\ singleton_h (h))

	domain_subtracted alias "|<<" (ds: SET [G]): like Current
			-- Return a new copy of current relation with
			-- all pairs whose first values are members of 'ds' subtracted.
		ensure
			current_rel_unchanged: Current ~ old Current.deep_twin
			new_rel_is_a_subset: Result |<: Current
			no_ds_in_new_rel: (Current |\ Result).domain ~ ds.comprehension (agent in_domain (?, domain))

	domain_subtracted_by alias "@<<" (g: G): like Current
			-- Return a new copy of current relation with
			-- all pairs whose first values 'g' subtracted.
		ensure
			current_rel_unchanged: Current ~ old Current.deep_twin
			new_rel_is_a_subset: Result |<: Current
			no_ds_in_new_rel: (Current |\ Result).domain ~ singleton_g (g).comprehension (agent in_domain (?, domain))

	range_subtracted alias "|>>" (rs: SET [H]): like Current
			-- Return a new copy of current relation with
			-- all pairs whose second values are members of 'ds' subtracted.
		ensure
			current_rel_unchanged: Current ~ old Current.deep_twin
			new_rel_is_a_subset: Result |<: Current
			no_rs_in_new_rel: (Current |\ Result).range ~ rs.comprehension (agent in_range (?, range))

	range_subtracted_by alias "@>>" (h: H): like Current
			-- Return a new copy of current relation with
			-- all pairs whose second values are 'h' subtracted.
		ensure
			current_rel_unchanged: Current ~ old Current.deep_twin
			new_rel_is_a_subset: Result |<: Current
			no_rs_in_new_rel: (Current |\ Result).range ~ singleton_h (h).comprehension (agent in_range (?, range))

	overriden alias "|<+" (r: like Current): like Current
			-- Return a copy of current relation that agrres on 'r'.
		ensure
			current_rel_unchanged: Current ~ old Current.deep_twin
				Result ~ ((Current |<< r.domain) |\/| r)

	overriden_by alias "@<+" (t: TUPLE [g: G; h: H]): like Current
			-- Return a copy of current relation that agrres on 'g |-> h'.
		ensure
			current_rel_unchanged: Current ~ old Current.deep_twin
				Result ~ ((Current @<< t.g) |\/| singleton_gh (t.g, t.h))
	
feature -- Agent functions

	in_domain (g: G; dom: SET [G]): BOOLEAN

	in_range (h: H; ran: SET [H]): BOOLEAN

	singleton_g (g: G): SET [G]
		ensure
				# Result = 1
				Result.has (g)

	singleton_h (h: H): SET [H]
		ensure
				# Result = 1
				Result.has (h)

	singleton_gh (g: G; h: H): REL [G, H]
		ensure
				# Result = 1
	
end -- class REL

Generated by ISE EiffelStudio