note description: "RELATION data structure for both specification and implementation." author: "JSO and JW" date: "$Date$" revision: "$Revision$" class REL [G -> attached ANY, H -> attached ANY] inherit SET [PAIR [G, H]] rename as_array as set_as_array end 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]]) do make_empty across a as tup loop extend (create {PAIR [G, H]}.make_from_tuple (tup.item)) end end feature -- Conversion to array. as_array: ARRAY [TUPLE [G, H]] do create Result.make_empty across Current as c loop Result.force (c.item.as_tuple, Result.upper + 1) end Result.compare_objects ensure Current ~ create {REL [G, H]}.make_from_tuple_array (Result) end feature -- Commands for relational operations domain_restrict (ds: SET [G]) -- Keep all pairs whose first values are members of 'ds'. do domain_subtract (domain |\ 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) end domain_restrict_by (g: G) -- Keep pairs whose first values are 'd'. do domain_subtract (domain - g) 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)) end range_restrict (rs: SET [H]) -- Keep all pairs whose second values are members of 'rs'. do range_subtract (range |\ 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) end range_restrict_by (h: H) -- Keep all pairs whose second values are 'h'. do range_subtract (range |\ singleton_h (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)) end domain_subtract (ds: SET [G]) -- Subtract all pairs whose first values are members of 'ds'. local g: G do from imp.start until imp.after loop g := imp.item.first if ds.has (g) then imp.remove else imp.forth end end 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)) end domain_subtract_by (g: G) -- Subtract pairs whose first values are 'g'. do domain_subtract (create {SET [G]}.make_from_array (<<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)) end range_subtract (rs: SET [H]) -- Subtract all pairs whose second values are members of 'rs'. local h: H do from imp.start until imp.after loop h := imp.item.second if rs.has (h) then imp.remove else imp.forth end end 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)) end range_subtract_by (h: H) -- Subtract pairs whose second values are 'h'. do range_subtract (create {SET [H]}.make_from_array (<<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)) end override (r: like Current) -- Update current relation such that it aggres on 'r'. do domain_subtract (r.domain) union (r) ensure Current ~ ((old Current.deep_twin |<< r.domain) |\/| r) end override_by (t: TUPLE [g: G; h: H]) -- Update current relation such that it aggres on 'g |-> h'. do domain_subtract_by (t.g) extend (create {PAIR [G, H]}.make_from_tuple (t)) ensure Current ~ ((old Current.deep_twin @<< t.g) |\/| singleton_gh (t.g, t.h)) end feature -- Status queries is_function: BOOLEAN -- Is current relation a function? -- i.e., each domain value maps to at most one value. local c: ITERATION_CURSOR [PAIR [G, H]] do from Result := True c := new_cursor until not Result or else c.after loop if # image (c.item.first) > 1 then Result := False end c.forth end ensure Result = across domain as d all # image (d.item) = 1 end end is_injection: BOOLEAN -- Is current relation an injective function? -- i.e., no two domain values map to the same range vaule. do Result := is_function and then inverse.is_function ensure Result = (is_function and inverse.is_function) end domain: SET [G] -- Return the domain set of relation. do create Result.make_empty across Current as c loop Result.extend (c.item.first) end end range: SET [H] -- Return the range set of relation. do create Result.make_empty across Current as c loop Result.extend (c.item.second) end end feature -- Queries for relational operations inverse: REL [H, G] do create Result.make_empty across Current as pair loop Result.extend (create {PAIR [H, G]}.make_from_tuple ([pair.item.second, pair.item.first])) end ensure current_rel_unchanged: Current ~ old Current.deep_twin Result.inverse.is_equal (Current) end image alias "[]" (g: G): SET [H] -- Retrieve the set of items that are associated with 'g'. do create Result.make_empty across Current as c loop if c.item.first ~ g then Result.extend (c.item.second) end end 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 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. do Result := Current.deep_twin Result.domain_restrict (ds) 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) end domain_restricted_by alias "@<" (g: G): like Current -- Return a copy of current relation with -- all pairs whose first values are 'g' kept. do Result := Current.deep_twin Result.domain_restrict_by (g) 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)) end 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. do Result := Current.deep_twin Result.range_restrict (rs) 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) end range_restricted_by alias "@>" (h: H): like Current -- Return a copy of current relation with -- all pairs whose second values are 'h' kept. do Result := Current.deep_twin Result.range_restrict_by (h) 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)) end 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. do Result := Current.deep_twin Result.domain_subtract (ds) 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)) end domain_subtracted_by alias "@<<" (g: G): like Current -- Return a new copy of current relation with -- all pairs whose first values 'g' subtracted. do Result := Current.deep_twin Result.domain_subtract_by (g) 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)) end 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. do Result := Current.deep_twin Result.range_subtract (rs) 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)) end range_subtracted_by alias "@>>" (h: H): like Current -- Return a new copy of current relation with -- all pairs whose second values are 'h' subtracted. do Result := Current.deep_twin Result.range_subtract_by (h) 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)) end overriden alias "|<+" (r: like Current): like Current -- Return a copy of current relation that agrres on 'r'. do Result := Current.deep_twin Result.override (r) ensure current_rel_unchanged: Current ~ old Current.deep_twin Result ~ ((Current |<< r.domain) |\/| r) end overriden_by alias "@<+" (t: TUPLE [g: G; h: H]): like Current -- Return a copy of current relation that agrres on 'g |-> h'. do Result := Current.deep_twin Result.override_by (t.g, t.h) ensure current_rel_unchanged: Current ~ old Current.deep_twin Result ~ ((Current @<< t.g) |\/| singleton_gh (t.g, t.h)) end feature -- Agent functions in_domain (g: G; dom: SET [G]): BOOLEAN do if dom.has (g) then Result := True end end in_range (h: H; ran: SET [H]): BOOLEAN do if ran.has (h) then Result := True end end singleton_g (g: G): SET [G] do create Result.make_from_array (<<g>>) ensure # Result = 1 Result.has (g) end singleton_h (h: H): SET [H] do create Result.make_from_array (<<h>>) ensure # Result = 1 Result.has (h) end singleton_gh (g: G; h: H): REL [G, H] do create Result.make_from_tuple_array (<<[g, h]>>) ensure # Result = 1 end end -- class REL
Generated by ISE EiffelStudio