FUNCTION equal_maths_spaces

(* SCHEMA step_merged_ap_schema; *)
-- IN AP242
FUNCTION equal_maths_spaces
      (spc1 : maths_space;
       spc2 : maths_space ) : LOGICAL;
   LOCAL
      spc1types : SET OF STRING := stripped_typeof(spc1);
      spc2types : SET OF STRING := stripped_typeof(spc2);
      set1 : SET OF maths_value;
      set2 : SET OF maths_value;
      cum : LOGICAL := TRUE;
      base : maths_space;
      expnt : INTEGER;
      factors : LIST OF maths_space;
      factors2 : LIST OF maths_space;
      fs1 : function_space;
      fs2 : function_space;
      cum2 : LOGICAL;
   END_LOCAL;
      IF spc1 = spc2 THEN
         RETURN (TRUE);
      END_IF;
      IF 'FINITE_SPACE' IN spc1types THEN
         set1 := spc1\finite_space.members;
         IF 'FINITE_SPACE' IN spc2types THEN
            set2 := spc2\finite_space.members;
            REPEAT i := 1 TO SIZEOF(set1) BY 1;
               cum := cum AND member_of(set1[i], spc2);
               IF cum = FALSE THEN
                  RETURN (FALSE);
               END_IF;
            END_REPEAT;
            IF cum = TRUE THEN
               REPEAT i := 1 TO SIZEOF(set2) BY 1;
                  cum := cum AND member_of(set2[i], spc1);
                  IF cum = FALSE THEN
                     RETURN (FALSE);
                  END_IF;
               END_REPEAT;
            END_IF;
            RETURN (cum);
         END_IF;
         IF 'FINITE_INTEGER_INTERVAL' IN spc2types THEN
            set2 := [];
            REPEAT i := spc2\finite_integer_interval.min TO spc2\finite_integer_interval.max BY 1;
               set2 := set2 + [ i ];
            END_REPEAT;
            RETURN (equal_maths_spaces(spc1, make_finite_space(set2)));
         END_IF;
      END_IF;
      IF ('FINITE_INTEGER_INTERVAL' IN spc1types) AND ('FINITE_SPACE' IN spc2types) THEN
         set1 := [];
         REPEAT i := spc1\finite_integer_interval.min TO spc1\finite_integer_interval.max BY 1;
            set1 := set1 + [ i ];
         END_REPEAT;
         RETURN (equal_maths_spaces(make_finite_space(set1), spc2));
      END_IF;
      IF ('CARTESIAN_COMPLEX_NUMBER_REGION' IN spc1types) AND ('POLAR_COMPLEX_NUMBER_REGION' IN spc2types) THEN
         RETURN (equal_cregion_pregion(spc1, spc2));
      END_IF;
      IF ('POLAR_COMPLEX_NUMBER_REGION' IN spc1types) AND ('CARTESIAN_COMPLEX_NUMBER_REGION' IN spc2types) THEN
         RETURN (equal_cregion_pregion(spc2, spc1));
      END_IF;
      IF 'UNIFORM_PRODUCT_SPACE' IN spc1types THEN
         base := spc1\uniform_product_space.base;
         expnt := spc1\uniform_product_space.exponent;
         IF 'UNIFORM_PRODUCT_SPACE' IN spc2types THEN
            IF expnt <> spc2\uniform_product_space.exponent THEN
               RETURN (FALSE);
            END_IF;
            RETURN (equal_maths_spaces(base, spc2\uniform_product_space.base));
         END_IF;
         IF 'LISTED_PRODUCT_SPACE' IN spc2types THEN
            factors := spc2\listed_product_space.factors;
            IF expnt <> SIZEOF(factors) THEN
               RETURN (FALSE);
            END_IF;
            REPEAT i := 1 TO SIZEOF(factors) BY 1;
               cum := cum AND equal_maths_spaces(base, factors[i]);
               IF cum = FALSE THEN
                  RETURN (FALSE);
               END_IF;
            END_REPEAT;
            RETURN (cum);
         END_IF;
      END_IF;
      IF 'LISTED_PRODUCT_SPACE' IN spc1types THEN
         factors := spc1\listed_product_space.factors;
         IF 'UNIFORM_PRODUCT_SPACE' IN spc2types THEN
            IF spc2\uniform_product_space.exponent <> SIZEOF(factors) THEN
               RETURN (FALSE);
            END_IF;
            base := spc2\uniform_product_space.base;
            REPEAT i := 1 TO SIZEOF(factors) BY 1;
               cum := cum AND equal_maths_spaces(base, factors[i]);
               IF cum = FALSE THEN
                  RETURN (FALSE);
               END_IF;
            END_REPEAT;
            RETURN (cum);
         END_IF;
         IF 'LISTED_PRODUCT_SPACE' IN spc2types THEN
            factors2 := spc2\listed_product_space.factors;
            IF SIZEOF(factors) <> SIZEOF(factors2) THEN
               RETURN (FALSE);
            END_IF;
            REPEAT i := 1 TO SIZEOF(factors) BY 1;
               cum := cum AND equal_maths_spaces(factors[i], factors2[i]);
               IF cum = FALSE THEN
                  RETURN (FALSE);
               END_IF;
            END_REPEAT;
            RETURN (cum);
         END_IF;
      END_IF;
      IF ('EXTENDED_TUPLE_SPACE' IN spc1types) AND ('EXTENDED_TUPLE_SPACE' IN spc2types) THEN
         RETURN (equal_maths_spaces(spc1\extended_tuple_space.extender, spc2\extended_tuple_space.extender) AND equal_maths_spaces(spc1\extended_tuple_space.base, spc2\extended_tuple_space.base));
      END_IF;
      IF ('FUNCTION_SPACE' IN spc1types) AND ('FUNCTION_SPACE' IN spc2types) THEN
         fs1 := spc1;
         fs2 := spc2;
         IF fs1.domain_constraint <> fs2.domain_constraint THEN
            IF (fs1.domain_constraint = sc_equal) OR (fs2.domain_constraint = sc_equal) THEN
               RETURN (FALSE);
            END_IF;
            IF fs1.domain_constraint <> sc_subspace THEN
               fs1 := spc2;
               fs2 := spc1;
            END_IF;
            IF (fs1.domain_constraint <> sc_subspace) OR (fs2.domain_constraint <> sc_member) THEN
               RETURN (UNKNOWN);
            END_IF;
            IF any_space_satisfies(fs1.domain_constraint, fs1.domain_argument) <> any_space_satisfies(fs2.domain_constraint, fs2.domain_argument) THEN
               RETURN (FALSE);
            END_IF;
            IF NOT ('FINITE_SPACE' IN stripped_typeof(fs2.domain_argument)) THEN
               RETURN (FALSE);
            END_IF;
            IF SIZEOF([ 'FINITE_SPACE', 'FINITE_INTEGER_INTERVAL' ] * stripped_typeof(fs1.domain_argument)) = 0 THEN
               RETURN (FALSE);
            END_IF;
            RETURN (UNKNOWN);
         END_IF;
         cum := equal_maths_spaces(fs1.domain_argument, fs2.domain_argument);
         IF cum = FALSE THEN
            RETURN (FALSE);
         END_IF;
         IF fs1.range_constraint <> fs2.range_constraint THEN
            IF (fs1.range_constraint = sc_equal) OR (fs2.range_constraint = sc_equal) THEN
               RETURN (FALSE);
            END_IF;
            IF fs1.range_constraint <> sc_subspace THEN
               fs1 := spc2;
               fs2 := spc1;
            END_IF;
            IF (fs1.range_constraint <> sc_subspace) OR (fs2.range_constraint <> sc_member) THEN
               RETURN (UNKNOWN);
            END_IF;
            IF any_space_satisfies(fs1.range_constraint, fs1.range_argument) <> any_space_satisfies(fs2.range_constraint, fs2.range_argument) THEN
               RETURN (FALSE);
            END_IF;
            IF NOT ('FINITE_SPACE' IN stripped_typeof(fs2.range_argument)) THEN
               RETURN (FALSE);
            END_IF;
            IF SIZEOF([ 'FINITE_SPACE', 'FINITE_INTEGER_INTERVAL' ] * stripped_typeof(fs1.range_argument)) = 0 THEN
               RETURN (FALSE);
            END_IF;
            RETURN (UNKNOWN);
         END_IF;
         cum := cum AND equal_maths_spaces(fs1.range_argument, fs2.range_argument);
         RETURN (cum);
      END_IF;
      RETURN (FALSE);
END_FUNCTION;

Referenced By

Defintion equal_maths_spaces is references by the following definitions:
DefinitionType
 equal_maths_functions FUNCTION
 equal_maths_values FUNCTION
 member_of FUNCTION
 subspace_of FUNCTION


[Top Level Definitions] [Exit]

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