FUNCTION subspace_of
(* SCHEMA FUNCTIONAL_DATA_AND_SCHEMATIC_REPRESENTATION_MIM_LF; *)
FUNCTION subspace_of(space1 : maths_space; space2 : maths_space) : LOGICAL;
LOCAL
spc1 : maths_space := simplify_maths_space(space1);
spc2 : maths_space := simplify_maths_space(space2);
types1 : SET OF STRING := stripped_typeof(spc1);
types2 : SET OF STRING := stripped_typeof(spc2);
lgcl : LOGICAL;
cum : LOGICAL;
es_val : elementary_space_enumerators;
bnd1 : REAL;
bnd2 : REAL;
n : INTEGER;
sp1 : maths_space;
sp2 : maths_space;
prgn1 : polar_complex_number_region;
prgn2 : polar_complex_number_region;
aitv : finite_real_interval;
END_LOCAL;
IF NOT EXISTS(spc1) OR NOT EXISTS(spc2) THEN
RETURN (FALSE);
END_IF;
IF spc2 = the_generics THEN
RETURN (TRUE);
END_IF;
IF 'ELEMENTARY_SPACE' IN types1 THEN
IF NOT ('ELEMENTARY_SPACE' IN types2) THEN
RETURN (FALSE);
END_IF;
es_val := spc2\elementary_space.space_id;
IF spc1\elementary_space.space_id = es_val THEN
RETURN (TRUE);
END_IF;
CASE spc1\elementary_space.space_id OF
es_numbers :
RETURN (FALSE);
es_complex_numbers :
RETURN (es_val = es_numbers);
es_reals :
RETURN (es_val = es_numbers);
es_integers :
RETURN (es_val = es_numbers);
es_logicals :
RETURN (FALSE);
es_booleans :
RETURN (es_val = es_logicals);
es_strings :
RETURN (FALSE);
es_binarys :
RETURN (FALSE);
es_maths_spaces :
RETURN (FALSE);
es_maths_functions :
RETURN (FALSE);
es_generics :
RETURN (FALSE);
END_CASE;
RETURN (UNKNOWN);
END_IF;
IF 'FINITE_INTEGER_INTERVAL' IN types1 THEN
cum := TRUE;
REPEAT i := spc1\finite_integer_interval.min TO spc1\
finite_integer_interval.max;
cum := cum AND member_of(i, spc2);
IF cum = FALSE THEN
RETURN (FALSE);
END_IF;
END_REPEAT;
RETURN (cum);
END_IF;
IF 'INTEGER_INTERVAL_FROM_MIN' IN types1 THEN
IF 'ELEMENTARY_SPACE' IN types2 THEN
es_val := spc2\elementary_space.space_id;
RETURN ((es_val = es_numbers) OR (es_val = es_integers));
END_IF;
IF 'INTEGER_INTERVAL_FROM_MIN' IN types2 THEN
RETURN (spc1\integer_interval_from_min.min >= spc2\
integer_interval_from_min.min);
END_IF;
RETURN (FALSE);
END_IF;
IF 'INTEGER_INTERVAL_TO_MAX' IN types1 THEN
IF 'ELEMENTARY_SPACE' IN types2 THEN
es_val := spc2\elementary_space.space_id;
RETURN ((es_val = es_numbers) OR (es_val = es_integers));
END_IF;
IF 'INTEGER_INTERVAL_TO_MAX' IN types2 THEN
RETURN (spc1\integer_interval_to_max.max <= spc2\integer_interval_to_max.
max);
END_IF;
RETURN (FALSE);
END_IF;
IF 'FINITE_REAL_INTERVAL' IN types1 THEN
IF 'ELEMENTARY_SPACE' IN types2 THEN
es_val := spc2\elementary_space.space_id;
RETURN ((es_val = es_numbers) OR (es_val = es_reals));
END_IF;
IF ('FINITE_REAL_INTERVAL' IN types2) OR ('REAL_INTERVAL_FROM_MIN' IN
types2) OR ('REAL_INTERVAL_TO_MAX' IN types2) THEN
IF min_exists(spc2) THEN
bnd1 := spc1\finite_real_interval.min;
bnd2 := real_min(spc2);
IF (bnd1 < bnd2) OR (bnd1 = bnd2) AND min_included(spc1) AND NOT
min_included(spc2) THEN
RETURN (FALSE);
END_IF;
END_IF;
IF max_exists(spc2) THEN
bnd1 := spc1\finite_real_interval.max;
bnd2 := real_max(spc2);
IF (bnd1 > bnd2) OR (bnd1 = bnd2) AND max_included(spc1) AND NOT
max_included(spc2) THEN
RETURN (FALSE);
END_IF;
END_IF;
RETURN (TRUE);
END_IF;
RETURN (FALSE);
END_IF;
IF 'REAL_INTERVAL_FROM_MIN' IN types1 THEN
IF 'ELEMENTARY_SPACE' IN types2 THEN
es_val := spc2\elementary_space.space_id;
RETURN ((es_val = es_numbers) OR (es_val = es_reals));
END_IF;
IF 'REAL_INTERVAL_FROM_MIN' IN types2 THEN
bnd1 := spc1\real_interval_from_min.min;
bnd2 := spc2\real_interval_from_min.min;
RETURN ((bnd2 < bnd1) OR (bnd2 = bnd1) AND (min_included(spc2) OR NOT
min_included(spc1)));
END_IF;
RETURN (FALSE);
END_IF;
IF 'REAL_INTERVAL_TO_MAX' IN types1 THEN
IF 'ELEMENTARY_SPACE' IN types2 THEN
es_val := spc2\elementary_space.space_id;
RETURN ((es_val = es_numbers) OR (es_val = es_reals));
END_IF;
IF 'REAL_INTERVAL_TO_MAX' IN types2 THEN
bnd1 := spc1\real_interval_to_max.max;
bnd2 := spc2\real_interval_to_max.max;
RETURN ((bnd2 > bnd1) OR (bnd2 = bnd1) AND (max_included(spc2) OR NOT
max_included(spc1)));
END_IF;
RETURN (FALSE);
END_IF;
IF 'CARTESIAN_COMPLEX_NUMBER_REGION' IN types1 THEN
IF 'ELEMENTARY_SPACE' IN types2 THEN
es_val := spc2\elementary_space.space_id;
RETURN ((es_val = es_numbers) OR (es_val = es_complex_numbers));
END_IF;
IF 'CARTESIAN_COMPLEX_NUMBER_REGION' IN types2 THEN
RETURN (subspace_of(spc1\cartesian_complex_number_region.real_constraint
, spc2\cartesian_complex_number_region.real_constraint) AND subspace_of(
spc1\cartesian_complex_number_region.imag_constraint, spc2\
cartesian_complex_number_region.imag_constraint));
END_IF;
IF 'POLAR_COMPLEX_NUMBER_REGION' IN types2 THEN
RETURN (subspace_of(enclose_cregion_in_pregion(spc1, spc2\
polar_complex_number_region.centre), spc2));
END_IF;
RETURN (FALSE);
END_IF;
IF 'POLAR_COMPLEX_NUMBER_REGION' IN types1 THEN
IF 'ELEMENTARY_SPACE' IN types2 THEN
es_val := spc2\elementary_space.space_id;
RETURN ((es_val = es_numbers) OR (es_val = es_complex_numbers));
END_IF;
IF 'CARTESIAN_COMPLEX_NUMBER_REGION' IN types2 THEN
RETURN (subspace_of(enclose_pregion_in_cregion(spc1), spc2));
END_IF;
IF 'POLAR_COMPLEX_NUMBER_REGION' IN types2 THEN
prgn1 := spc1;
prgn2 := spc2;
IF prgn1.centre = prgn2.centre THEN
IF prgn2.direction_constraint.max > PI THEN
aitv := make_finite_real_interval(-PI, open, prgn2.
direction_constraint.max - 2.0 * PI, prgn2.direction_constraint.
max_closure);
RETURN (subspace_of(prgn1.distance_constraint, prgn2.
distance_constraint) AND (subspace_of(prgn1.direction_constraint,
prgn2.direction_constraint) OR subspace_of(prgn1.direction_constraint
, aitv)));
ELSE
RETURN (subspace_of(prgn1.distance_constraint, prgn2.
distance_constraint) AND subspace_of(prgn1.direction_constraint,
prgn2.direction_constraint));
END_IF;
END_IF;
RETURN (subspace_of(enclose_pregion_in_pregion(prgn1, prgn2.centre),
prgn2));
END_IF;
RETURN (FALSE);
END_IF;
IF 'FINITE_SPACE' IN types1 THEN
cum := TRUE;
REPEAT i := 1 TO SIZEOF(spc1\finite_space.members);
cum := cum AND member_of(spc1\finite_space.members[i], spc2);
IF cum = FALSE THEN
RETURN (FALSE);
END_IF;
END_REPEAT;
RETURN (cum);
END_IF;
IF 'PRODUCT_SPACE' IN types1 THEN
IF 'PRODUCT_SPACE' IN types2 THEN
IF space_dimension(spc1) = space_dimension(spc2) THEN
cum := TRUE;
REPEAT i := 1 TO space_dimension(spc1);
cum := cum AND subspace_of(factor_space(spc1, i), factor_space(spc2,
i));
IF cum = FALSE THEN
RETURN (FALSE);
END_IF;
END_REPEAT;
RETURN (cum);
END_IF;
END_IF;
IF 'EXTENDED_TUPLE_SPACE' IN types2 THEN
IF space_dimension(spc1) >= space_dimension(spc2) THEN
cum := TRUE;
REPEAT i := 1 TO space_dimension(spc1);
cum := cum AND subspace_of(factor_space(spc1, i), factor_space(spc2,
i));
IF cum = FALSE THEN
RETURN (FALSE);
END_IF;
END_REPEAT;
RETURN (cum);
END_IF;
END_IF;
RETURN (FALSE);
END_IF;
IF 'EXTENDED_TUPLE_SPACE' IN types1 THEN
IF 'EXTENDED_TUPLE_SPACE' IN types2 THEN
n := space_dimension(spc1);
IF n < space_dimension(spc2) THEN
n := space_dimension(spc2);
END_IF;
cum := TRUE;
REPEAT i := 1 TO n + 1;
cum := cum AND subspace_of(factor_space(spc1, i), factor_space(spc2, i)
);
IF cum = FALSE THEN
RETURN (FALSE);
END_IF;
END_REPEAT;
RETURN (cum);
END_IF;
RETURN (FALSE);
END_IF;
IF 'FUNCTION_SPACE' IN types1 THEN
IF 'ELEMENTARY_SPACE' IN types2 THEN
RETURN (spc2\elementary_space.space_id = es_maths_functions);
END_IF;
IF 'FUNCTION_SPACE' IN types2 THEN
cum := TRUE;
sp1 := spc1\function_space.domain_argument;
sp2 := spc2\function_space.domain_argument;
CASE spc1\function_space.domain_constraint OF
sc_equal :
BEGIN
CASE spc2\function_space.domain_constraint OF
sc_equal :
cum := cum AND equal_maths_spaces(sp1, sp2);
sc_subspace :
cum := cum AND subspace_of(sp1, sp2);
sc_member :
cum := cum AND member_of(sp1, sp2);
END_CASE;
END;
sc_subspace :
BEGIN
CASE spc2\function_space.domain_constraint OF
sc_equal :
RETURN (FALSE);
sc_subspace :
cum := cum AND subspace_of(sp1, sp2);
sc_member :
BEGIN
IF NOT member_of(sp1, sp2) THEN
RETURN (FALSE);
END_IF;
cum := UNKNOWN;
END;
END_CASE;
END;
sc_member :
BEGIN
CASE spc2\function_space.domain_constraint OF
sc_equal :
cum := cum AND space_is_singleton(sp1) AND equal_maths_spaces(
singleton_member_of(sp1), sp2);
sc_subspace :
BEGIN
IF NOT member_of(sp2, sp1) THEN
RETURN (FALSE);
END_IF;
cum := UNKNOWN;
END;
sc_member :
cum := cum AND subspace_of(sp1, sp2);
END_CASE;
END;
END_CASE;
IF cum = FALSE THEN
RETURN (FALSE);
END_IF;
sp1 := spc1\function_space.range_argument;
sp2 := spc2\function_space.range_argument;
CASE spc1\function_space.range_constraint OF
sc_equal :
BEGIN
CASE spc2\function_space.range_constraint OF
sc_equal :
cum := cum AND equal_maths_spaces(sp1, sp2);
sc_subspace :
cum := cum AND subspace_of(sp1, sp2);
sc_member :
cum := cum AND member_of(sp1, sp2);
END_CASE;
END;
sc_subspace :
BEGIN
CASE spc2\function_space.domain_constraint OF
sc_equal :
RETURN (FALSE);
sc_subspace :
cum := cum AND subspace_of(sp1, sp2);
sc_member :
BEGIN
IF NOT member_of(sp1, sp2) THEN
RETURN (FALSE);
END_IF;
cum := UNKNOWN;
END;
END_CASE;
END;
sc_member :
BEGIN
CASE spc2\function_space.domain_constraint OF
sc_equal :
cum := cum AND space_is_singleton(sp1) AND equal_maths_spaces(
singleton_member_of(sp1), sp2);
sc_subspace :
BEGIN
IF NOT member_of(sp2, sp1) THEN
RETURN (FALSE);
END_IF;
cum := UNKNOWN;
END;
sc_member :
cum := cum AND subspace_of(sp1, sp2);
END_CASE;
END;
END_CASE;
RETURN (cum);
END_IF;
RETURN (FALSE);
END_IF;
RETURN (UNKNOWN);
END_FUNCTION;
Referenced By
Defintion subspace_of is references by the following definitions:
[Top Level Definitions] [Exit]Generated by STEP Tools® EXPRESS to HTML Converter
2012-03-27T17:17:33-04:00