FUNCTION compatible_spaces
(sp1 : maths_space, sp2 : maths_space) : BOOLEAN;
LOCAL types1 : SET OF STRING := stripped_typeof (sp1); types2 : SET OF STRING := stripped_typeof (sp2); lgcl : LOGICAL := UNKNOWN; m, n : INTEGER; s1, s2 : maths_space; END_LOCAL; IF 'FINITE_SPACE' IN types1 THEN REPEAT i := 1 TO SIZEOF (sp1\finite_space.members); lgcl := member_of(sp1\finite_space.members[i], sp2); IF lgcl <> FALSE THEN RETURN (TRUE); END_IF; END_REPEAT; RETURN (FALSE); END_IF; IF 'FINITE_SPACE' IN types2 THEN REPEAT i := 1 TO SIZEOF (sp2\finite_space.members); lgcl := member_of(sp2\finite_space.members[i], sp1); IF lgcl <> FALSE THEN RETURN (TRUE); END_IF; END_REPEAT; RETURN (FALSE); END_IF; IF 'ELEMENTARY_SPACE' IN types1 THEN IF sp1\elementary_space.space_id = es_generics THEN RETURN (TRUE); END_IF; IF 'ELEMENTARY_SPACE' IN types2 THEN RETURN (compatible_es_values(sp1\elementary_space.space_id, sp2\elementary_space.space_id)); END_IF; IF ('FINITE_INTEGER_INTERVAL' IN types2) OR ('INTEGER_INTERVAL_FROM_MIN' IN types2) OR ('INTEGER_INTERVAL_TO_MAX' IN types2) THEN RETURN (compatible_es_values(sp1\elementary_space.space_id, es_integers)); END_IF; IF ('FINITE_REAL_INTERVAL' IN types2) OR ('REAL_INTERVAL_FROM_MIN' IN types2) OR ('REAL_INTERVAL_TO_MAX' IN types2) THEN RETURN (compatible_es_values(sp1\elementary_space.space_id, es_reals)); END_IF; IF ('CARTESIAN_COMPLEX_NUMBER_REGION' IN types2) OR ('POLAR_COMPLEX_NUMBER_REGION' IN types2) THEN RETURN (compatible_es_values(sp1\elementary_space.space_id, es_complex_numbers)); END_IF; IF 'TUPLE_SPACE' IN types2 THEN RETURN (FALSE); END_IF; IF 'FUNCTION_SPACE' IN types2 THEN RETURN (bool(sp1\elementary_space.space_id = es_maths_functions)); END_IF; -- Should be unreachable. RETURN (TRUE); END_IF; IF 'ELEMENTARY_SPACE' IN types2 THEN IF sp2\elementary_space.space_id = es_generics THEN RETURN (TRUE); END_IF; IF ('FINITE_INTEGER_INTERVAL' IN types1) OR ('INTEGER_INTERVAL_FROM_MIN' IN types1) OR ('INTEGER_INTERVAL_TO_MAX' IN types1) THEN RETURN (compatible_es_values(sp2\elementary_space.space_id, es_integers)); END_IF; IF ('FINITE_REAL_INTERVAL' IN types1) OR ('REAL_INTERVAL_FROM_MIN' IN types1) OR ('REAL_INTERVAL_TO_MAX' IN types1) THEN RETURN (compatible_es_values(sp2\elementary_space.space_id, es_reals)); END_IF; IF ('CARTESIAN_COMPLEX_NUMBER_REGION' IN types1) OR ('POLAR_COMPLEX_NUMBER_REGION' IN types1) THEN RETURN (compatible_es_values(sp2\elementary_space.space_id, es_complex_numbers)); END_IF; IF 'TUPLE_SPACE' IN types1 THEN RETURN (FALSE); END_IF; IF 'FUNCTION_SPACE' IN types1 THEN RETURN (bool(sp2\elementary_space.space_id = es_maths_functions)); END_IF; -- Should be unreachable. RETURN (TRUE); END_IF; IF subspace_of_es(sp1,es_integers) THEN -- Note that sp1 finite already handled. IF subspace_of_es(sp2,es_integers) THEN -- Note that sp2 finite already handled. RETURN (compatible_intervals(sp1,sp2)); END_IF; RETURN (FALSE); END_IF; IF subspace_of_es(sp2,es_integers) THEN RETURN (FALSE); END_IF; IF subspace_of_es(sp1,es_reals) THEN -- Note that sp1 finite already handled. IF subspace_of_es(sp2,es_reals) THEN -- Note that sp2 finite already handled. RETURN (compatible_intervals(sp1,sp2)); END_IF; RETURN (FALSE); END_IF; IF subspace_of_es(sp2,es_reals) THEN RETURN (FALSE); END_IF; IF subspace_of_es(sp1,es_complex_numbers) THEN -- Note sp1 finite already handled. IF subspace_of_es(sp2,es_complex_numbers) THEN -- Note sp2 finite already handled. RETURN (compatible_complex_number_regions(sp1,sp2)); END_IF; RETURN (FALSE); END_IF; IF subspace_of_es(sp2,es_complex_numbers) THEN RETURN (FALSE); END_IF; IF 'UNIFORM_PRODUCT_SPACE' IN types1 THEN IF 'UNIFORM_PRODUCT_SPACE' IN types2 THEN IF sp1\uniform_product_space.exponent <> sp2\uniform_product_space.exponent THEN RETURN (FALSE); END_IF; RETURN (compatible_spaces(sp1\uniform_product_space.base, sp2\uniform_product_space.base)); END_IF; IF 'LISTED_PRODUCT_SPACE' IN types2 THEN n := SIZEOF (sp2\listed_product_space.factors); IF sp1\uniform_product_space.exponent <> n THEN RETURN (FALSE); END_IF; REPEAT i := 1 TO n; IF NOT compatible_spaces(sp1\uniform_product_space.base, sp2\listed_product_space.factors[i]) THEN RETURN (FALSE); END_IF; END_REPEAT; RETURN (TRUE); END_IF; IF 'EXTENDED_TUPLE_SPACE' IN types2 THEN m := sp1\uniform_product_space.exponent; n := space_dimension(sp2\extended_tuple_space.base); IF m < n THEN RETURN (FALSE); END_IF; IF m = n THEN RETURN (compatible_spaces(sp1, sp2\extended_tuple_space.base)); END_IF; RETURN (compatible_spaces(sp1, assoc_product_space( sp2\extended_tuple_space.base, make_uniform_product_space( sp2\extended_tuple_space.extender, m - n)))); END_IF; IF 'FUNCTION_SPACE' IN types2 THEN RETURN (FALSE); END_IF; -- Should be unreachable. RETURN (TRUE); END_IF; IF 'LISTED_PRODUCT_SPACE' IN types1 THEN n := SIZEOF (sp1\listed_product_space.factors); IF 'UNIFORM_PRODUCT_SPACE' IN types2 THEN IF n <> sp2\uniform_product_space.exponent THEN RETURN (FALSE); END_IF; REPEAT i := 1 TO n; IF NOT compatible_spaces(sp2\uniform_product_space.base, sp1\listed_product_space.factors[i]) THEN RETURN (FALSE); END_IF; END_REPEAT; RETURN (TRUE); END_IF; IF 'LISTED_PRODUCT_SPACE' IN types2 THEN IF n <> SIZEOF (sp2\listed_product_space.factors) THEN RETURN (FALSE); END_IF; REPEAT i := 1 TO n; IF NOT compatible_spaces(sp1\listed_product_space.factors[i], sp2\listed_product_space.factors[i]) THEN RETURN (FALSE); END_IF; END_REPEAT; RETURN (TRUE); END_IF; IF 'EXTENDED_TUPLE_SPACE' IN types2 THEN m := space_dimension(sp2\extended_tuple_space.base); IF n < m THEN RETURN (FALSE); END_IF; IF n = m THEN RETURN (compatible_spaces(sp1, sp2\extended_tuple_space.base)); END_IF; RETURN (compatible_spaces(sp1, assoc_product_space( sp2\extended_tuple_space.base, make_uniform_product_space( sp2\extended_tuple_space.extender, n - m)))); END_IF; IF (schema_prefix + 'FUNCTION_SPACE') IN types2 THEN RETURN (FALSE); END_IF; -- Should be unreachable. RETURN (TRUE); END_IF; IF 'EXTENDED_TUPLE_SPACE' IN types1 THEN IF ('UNIFORM_PRODUCT_SPACE' IN types2) OR ('LISTED_PRODUCT_SPACE' IN types2) THEN RETURN (compatible_spaces(sp2, sp1)); END_IF; IF 'EXTENDED_TUPLE_SPACE' IN types2 THEN IF NOT compatible_spaces(sp1\extended_tuple_space.extender, sp2\extended_tuple_space.extender) THEN RETURN (FALSE); END_IF; n := space_dimension(sp1\extended_tuple_space.base); m := space_dimension(sp2\extended_tuple_space.base); IF n < m THEN RETURN (compatible_spaces(assoc_product_space(sp1\extended_tuple_space.base, make_uniform_product_space(sp1\extended_tuple_space.extender, m - n)), sp2\extended_tuple_space.base)); END_IF; IF n = m THEN RETURN (compatible_spaces(sp1\extended_tuple_space.base, sp2\extended_tuple_space.base)); END_IF; IF n > m THEN RETURN (compatible_spaces(sp1\extended_tuple_space.base, assoc_product_space(sp2\extended_tuple_space.base, make_uniform_product_space(sp2\extended_tuple_space.extender, n - m)))); END_IF; END_IF; IF 'FUNCTION_SPACE' IN types2 THEN RETURN (FALSE); END_IF; -- Should be unreachable. RETURN (TRUE); END_IF; IF 'FUNCTION_SPACE' IN types1 THEN IF 'FUNCTION_SPACE' IN types2 THEN s1 := sp1\function_space.domain_argument; s2 := sp2\function_space.domain_argument; CASE sp1\function_space.domain_constraint OF sc_equal : BEGIN CASE sp2\function_space.domain_constraint OF sc_equal : lgcl := subspace_of(s1, s2) AND subspace_of(s2, s1); sc_subspace : lgcl := subspace_of(s1, s2); sc_member : lgcl := member_of(s1, s2); END_CASE; END; sc_subspace :BEGIN CASE sp2\function_space.domain_constraint OF sc_equal : lgcl := subspace_of(s2, s1); sc_subspace : lgcl := compatible_spaces(s1, s2); sc_member : lgcl := UNKNOWN; END_CASE; END; sc_member :BEGIN CASE sp2\function_space.domain_constraint OF sc_equal : lgcl := member_of(s2, s1); sc_subspace : lgcl := UNKNOWN; sc_member : lgcl := compatible_spaces(s1, s2); END_CASE; END; END_CASE; IF lgcl = FALSE THEN RETURN (FALSE); END_IF; s1 := sp1\function_space.range_argument; s2 := sp2\function_space.range_argument; CASE sp1\function_space.range_constraint OF sc_equal : BEGIN CASE sp2\function_space.range_constraint OF sc_equal : lgcl := subspace_of(s1, s2) AND subspace_of(s2, s1); sc_subspace : lgcl := subspace_of(s1, s2); sc_member : lgcl := member_of(s1, s2); END_CASE; END; sc_subspace :BEGIN CASE sp2\function_space.range_constraint OF sc_equal : lgcl := subspace_of(s2, s1); sc_subspace : lgcl := compatible_spaces(s1, s2); sc_member : lgcl := UNKNOWN; END_CASE; END; sc_member :BEGIN CASE sp2\function_space.range_constraint OF sc_equal : lgcl := member_of(s2, s1); sc_subspace : lgcl := UNKNOWN; sc_member : lgcl := compatible_spaces(s1, s2); END_CASE; END; END_CASE; IF lgcl = FALSE THEN RETURN (FALSE); END_IF; RETURN (TRUE); END_IF; -- Should be unreachable. RETURN (TRUE); END_IF; -- Should be unreachable. RETURN (TRUE); END_FUNCTION; -- compatible_spaces
|