FUNCTION compatible_spaces

(* SCHEMA step_merged_ap_schema; *)
-- IN AP242
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 : INTEGER;
      n : INTEGER;
      s1 : maths_space;
      s2 : maths_space;
   END_LOCAL;
      IF 'FINITE_SPACE' IN types1 THEN
         REPEAT i := 1 TO SIZEOF(sp1\finite_space.members) BY 1;
            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) BY 1;
            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;
         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;
         RETURN (TRUE);
      END_IF;
      IF subspace_of_es(sp1, es_integers) THEN
         IF subspace_of_es(sp2, es_integers) THEN
            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
         IF subspace_of_es(sp2, es_reals) THEN
            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
         IF subspace_of_es(sp2, es_complex_numbers) THEN
            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 BY 1;
               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;
         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 BY 1;
               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 BY 1;
               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;
         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;
         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;
         RETURN (TRUE);
      END_IF;
      RETURN (TRUE);
END_FUNCTION;

Referenced By

Defintion compatible_spaces is references by the following definitions:
DefinitionType
 all_members_of_es FUNCTION
 composable_sequence FUNCTION
 definite_integral_expr_check FUNCTION
 equal_maths_values FUNCTION
 free_form_assignment ENTITY
 function_applicability FUNCTION
 member_of FUNCTION
 parallel_composed_function_composability_check FUNCTION
 parallel_composed_function_domain_check FUNCTION


[Top Level Definitions] [Exit]

Generated by STEP Tools® EXPRESS to HTML Converter
2017-01-19T11:17:24-05:00