Schema: mathematical_functions_schema
SCHEMA mathematical_functions_schema;
REFERENCE FROM
iso13584_generic_expressions_schema -- ISO 13584-20
(binary_generic_expression,
environment,
generic_expression,
generic_literal,
generic_variable,
multiple_arity_generic_expression,
simple_generic_expression,
unary_generic_expression,
variable_semantics);
REFERENCE FROM
iso13584_expressions_schema -- ISO 13584-20
(abs_function
AS abs_expression,
acos_function
AS acos_expression,
and_expression,
asin_function
AS asin_expression,
atan_function
AS atan_expression,
binary_boolean_expression,
binary_function_call
AS binary_numeric_call_expression,
binary_numeric_expression,
boolean_defined_function
AS boolean_defined_expression,
boolean_expression,
boolean_literal,
boolean_variable,
comparison_equal,
comparison_expression,
comparison_greater,
comparison_greater_equal,
comparison_less,
comparison_less_equal,
comparison_not_equal,
concat_expression,
cos_function
AS cos_expression,
defined_function
AS defined_expression,
div_expression,
equals_expression,
exp_function
AS exp_expression,
expression,
format_function
AS format_expression,
index_expression,
int_literal,
int_numeric_variable,
int_value_function
AS int_value_expression,
integer_defined_function
AS integer_defined_expression,
interval_expression,
length_function
AS length_expression,
like_expression,
literal_number,
log_function
AS log_expression,
log10_function
AS log10_expression,
log2_function
AS log2_expression,
maximum_function
AS maximum_expression,
minimum_function
AS minimum_expression,
minus_expression,
minus_function
AS unary_minus_expression,
mod_expression,
mult_expression,
multiple_arity_boolean_expression,
multiple_arity_function_call
AS multiple_arity_numeric_call_expression,
multiple_arity_numeric_expression,
not_expression,
numeric_defined_function
AS numeric_defined_expression,
numeric_expression,
numeric_variable,
odd_function
AS odd_expression,
or_expression,
plus_expression,
power_expression,
real_defined_function
AS real_defined_expression,
real_literal,
real_numeric_variable,
simple_boolean_expression,
simple_numeric_expression,
simple_string_expression,
sin_function
AS sin_expression,
slash_expression,
SQL_mappable_defined_function
AS sql_mappable_defined_expression,
square_root_function
AS square_root_expression,
string_defined_function
AS string_defined_expression,
string_expression,
string_literal,
string_variable,
substring_expression,
tan_function
AS tan_expression,
unary_boolean_expression,
unary_function_call
AS unary_numeric_call_expression,
unary_numeric_expression,
value_function
AS value_expression,
variable,
xor_expression);
REFERENCE FROM
support_resource_schema -- ISO 10303-41
(label,
text);
REFERENCE FROM
external_reference_schema -- ISO 10303-41
(externally_defined_item);
REFERENCE FROM
geometry_schema -- ISO 10303-42
(curve,
dimension_of,
point,
surface,
volume);
CONSTANT
schema_prefix : STRING := 'MATHEMATICAL_FUNCTIONS_SCHEMA.';
the_binarys : elementary_space := make_elementary_space(es_binarys);
the_booleans : elementary_space := make_elementary_space(es_booleans);
the_complex_numbers : elementary_space := make_elementary_space(es_complex_numbers);
the_complex_tuples : extended_tuple_space := make_extended_tuple_space(
the_zero_tuple_space, the_complex_numbers);
the_empty_atom_based_tuple : atom_based_tuple := [];
the_empty_atom_based_value : atom_based_value := the_empty_atom_based_tuple;
the_empty_maths_tuple : maths_tuple := [];
the_empty_maths_value : maths_value := the_empty_maths_tuple;
the_empty_space : finite_space := make_finite_space([]);
the_generics : elementary_space := make_elementary_space(es_generics);
the_integer_tuples : extended_tuple_space := make_extended_tuple_space(
the_zero_tuple_space, the_integers);
the_integers : elementary_space := make_elementary_space(es_integers);
the_logicals : elementary_space := make_elementary_space(es_logicals);
the_maths_spaces : elementary_space := make_elementary_space(es_maths_spaces);
the_neg1_one_interval : finite_real_interval := make_finite_real_interval(
-1.0, closed, 1.0, closed);
the_neghalfpi_halfpi_interval : finite_real_interval := make_finite_real_interval(
-0.5*pi, closed, 0.5*pi, closed);
the_negpi_pi_interval : finite_real_interval := make_finite_real_interval(
-pi, open, pi, closed);
the_nonnegative_reals : real_interval_from_min := make_real_interval_from_min(0.0, closed);
the_numbers : elementary_space := make_elementary_space(es_numbers);
the_real_tuples : extended_tuple_space := make_extended_tuple_space(
the_zero_tuple_space, the_reals);
the_reals : elementary_space := make_elementary_space(es_reals);
the_strings : elementary_space := make_elementary_space(es_strings);
the_tuples : extended_tuple_space := make_extended_tuple_space(
the_zero_tuple_space, the_generics);
the_zero_one_interval : finite_real_interval := make_finite_real_interval(
0.0, closed, 1.0, closed);
the_zero_pi_interval : finite_real_interval := make_finite_real_interval(
0.0, closed, pi, closed);
the_zero_tuple_space : listed_product_space := make_listed_product_space([]);
END_CONSTANT;
TYPE atom_based_tuple =
LIST[0:?] OF atom_based_value;
END_TYPE;
TYPE atom_based_value =
SELECT
(maths_atom,
atom_based_tuple);
END_TYPE;
TYPE dotted_express_identifier =
STRING;
WHERE
syntax: dotted_identifiers_syntax(SELF);
END_TYPE;
TYPE elementary_function_enumerators =
ENUMERATION
OF
(ef_and,
ef_or,
ef_not,
ef_xor,
ef_negate_i,
ef_add_i,
ef_subtract_i,
ef_multiply_i,
ef_divide_i,
ef_mod_i,
ef_exponentiate_i,
ef_eq_i,
ef_ne_i,
ef_gt_i,
ef_lt_i,
ef_ge_i,
ef_le_i,
ef_abs_i,
ef_max_i,
ef_min_i,
ef_if_i,
ef_negate_r,
ef_reciprocal_r,
ef_add_r,
ef_subtract_r,
ef_multiply_r,
ef_divide_r,
ef_mod_r,
ef_exponentiate_r,
ef_exponentiate_ri,
ef_eq_r,
ef_ne_r,
ef_gt_r,
ef_lt_r,
ef_ge_r,
ef_le_r,
ef_abs_r,
ef_max_r,
ef_min_r,
ef_acos_r,
ef_asin_r,
ef_atan2_r,
ef_cos_r,
ef_exp_r,
ef_ln_r,
ef_log2_r,
ef_log10_r,
ef_sin_r,
ef_sqrt_r,
ef_tan_r,
ef_if_r,
ef_form_c,
ef_rpart_c,
ef_ipart_c,
ef_negate_c,
ef_reciprocal_c,
ef_add_c,
ef_subtract_c,
ef_multiply_c,
ef_divide_c,
ef_exponentiate_c,
ef_exponentiate_ci,
ef_eq_c,
ef_ne_c,
ef_conjugate_c,
ef_abs_c,
ef_arg_c,
ef_cos_c,
ef_exp_c,
ef_ln_c,
ef_sin_c,
ef_sqrt_c,
ef_tan_c,
ef_if_c,
ef_subscript_s,
ef_eq_s,
ef_ne_s,
ef_gt_s,
ef_lt_s,
ef_ge_s,
ef_le_s,
ef_subsequence_s,
ef_concat_s,
ef_size_s,
ef_format,
ef_value,
ef_like,
ef_if_s,
ef_subscript_b,
ef_eq_b,
ef_ne_b,
ef_gt_b,
ef_lt_b,
ef_ge_b,
ef_le_b,
ef_subsequence_b,
ef_concat_b,
ef_size_b,
ef_if_b,
ef_subscript_t,
ef_eq_t,
ef_ne_t,
ef_concat_t,
ef_size_t,
ef_entuple,
ef_detuple,
ef_insert,
ef_remove,
ef_if_t,
ef_sum_it,
ef_product_it,
ef_add_it,
ef_subtract_it,
ef_scalar_mult_it,
ef_dot_prod_it,
ef_sum_rt,
ef_product_rt,
ef_add_rt,
ef_subtract_rt,
ef_scalar_mult_rt,
ef_dot_prod_rt,
ef_norm_rt,
ef_sum_ct,
ef_product_ct,
ef_add_ct,
ef_subtract_ct,
ef_scalar_mult_ct,
ef_dot_prod_ct,
ef_norm_ct,
ef_if,
ef_ensemble,
ef_member_of);
END_TYPE;
TYPE elementary_space_enumerators =
ENUMERATION
OF
(es_numbers,
es_complex_numbers,
es_reals,
es_integers,
es_logicals,
es_booleans,
es_strings,
es_binarys,
es_maths_spaces,
es_maths_functions,
es_generics);
END_TYPE;
TYPE express_identifier =
dotted_express_identifier;
WHERE
syntax: dot_count(SELF) = 0;
END_TYPE;
TYPE extension_options =
ENUMERATION
OF
(eo_none,
eo_cont,
eo_cont_right,
eo_cont_left);
END_TYPE;
TYPE input_selector =
positive_integer;
END_TYPE;
TYPE lower_upper =
ENUMERATION
OF
(lower,
upper);
END_TYPE;
TYPE maths_atom =
SELECT
(maths_simple_atom,
maths_enum_atom);
END_TYPE;
TYPE maths_binary =
BINARY;
END_TYPE;
TYPE maths_boolean =
BOOLEAN;
END_TYPE;
TYPE maths_enum_atom =
SELECT
(elementary_space_enumerators,
ordering_type,
lower_upper,
symmetry_type,
elementary_function_enumerators,
open_closed,
space_constraint_type,
repackage_options,
extension_options);
END_TYPE;
TYPE maths_expression =
SELECT
(atom_based_value,
maths_tuple,
generic_expression);
END_TYPE;
TYPE maths_function_select =
SELECT
(maths_function,
elementary_function_enumerators);
END_TYPE;
TYPE maths_integer =
INTEGER;
END_TYPE;
TYPE maths_logical =
LOGICAL;
END_TYPE;
TYPE maths_number =
NUMBER;
END_TYPE;
TYPE maths_real =
REAL;
END_TYPE;
TYPE maths_simple_atom =
SELECT
(maths_number,
maths_real,
maths_integer,
maths_logical,
maths_boolean,
maths_string,
maths_binary);
END_TYPE;
TYPE maths_space_or_function =
SELECT
(maths_space,
maths_function);
END_TYPE;
TYPE maths_string =
STRING;
END_TYPE;
TYPE maths_tuple =
LIST[0:?] OF maths_value;
END_TYPE;
TYPE maths_value =
SELECT
(atom_based_value,
maths_tuple,
generic_expression);
WHERE
constancy: NOT ('GENERIC_EXPRESSION' IN stripped_typeof(SELF)) OR
expression_is_constant(SELF);
END_TYPE;
TYPE nonnegative_integer =
INTEGER;
WHERE
nonnegativity: SELF >= 0;
END_TYPE;
TYPE one_or_two =
positive_integer;
WHERE
in_range: (SELF = 1) OR (SELF = 2);
END_TYPE;
TYPE open_closed =
ENUMERATION
OF
(open,
closed);
END_TYPE;
TYPE ordering_type =
ENUMERATION
OF
(by_rows,
by_columns);
END_TYPE;
TYPE positive_integer =
nonnegative_integer;
WHERE
positivity: SELF > 0;
END_TYPE;
TYPE product_space =
SELECT
(uniform_product_space,
listed_product_space);
END_TYPE;
TYPE real_interval =
SELECT
(real_interval_from_min,
real_interval_to_max,
finite_real_interval,
elementary_space);
WHERE
WR1: NOT ('ELEMENTARY_SPACE' IN stripped_typeof(SELF)) OR
(SELF\elementary_space.space_id = es_reals);
END_TYPE;
TYPE repackage_options =
ENUMERATION
OF
(ro_nochange,
ro_wrap_as_tuple,
ro_unwrap_tuple);
END_TYPE;
TYPE space_constraint_type =
ENUMERATION
OF
(sc_equal,
sc_subspace,
sc_member);
END_TYPE;
TYPE symmetry_type =
ENUMERATION
OF
(identity,
skew,
hermitian,
skew_hermitian);
END_TYPE;
TYPE tuple_space =
EXTENSIBLE
GENERIC_ENTITY
SELECT
(product_space,
extended_tuple_space);
END_TYPE;
TYPE zero_or_one =
nonnegative_integer;
WHERE
in_range: (SELF = 0) OR (SELF = 1);
END_TYPE;
ENTITY abstracted_expression_function
SUBTYPE OF (maths_function, quantifier_expression);
DERIVE
SELF\quantifier_expression.variables : LIST[1:?] OF
UNIQUE
generic_variable := remove_first(SELF\multiple_arity_generic_expression.operands);
expr : generic_expression := SELF\multiple_arity_generic_expression.operands[1];
WHERE
WR1: SIZEOF (QUERY ( operand <*
SELF\multiple_arity_generic_expression.operands | NOT (
has_values_space( operand)))) = 0;
END_ENTITY;
ENTITY application_defined_function
SUBTYPE OF (maths_function);
explicit_domain : tuple_space;
explicit_range : tuple_space;
parameters : LIST[0:?] OF maths_value;
WHERE
WR1: expression_is_constant(explicit_domain);
WR2: expression_is_constant(explicit_range);
END_ENTITY;
ENTITY atom_based_literal
SUBTYPE OF (generic_literal);
lit_value : atom_based_value;
END_ENTITY;
ENTITY b_spline_basis
SUBTYPE OF (maths_function, generic_literal);
degree : nonnegative_integer;
repeated_knots : LIST[2:?] OF REAL;
DERIVE
order : positive_integer := degree + 1;
num_basis : positive_integer := SIZEOF (repeated_knots) - order;
WHERE
WR1: num_basis >= order;
WR2: nondecreasing(repeated_knots);
WR3: repeated_knots[order] < repeated_knots[num_basis+1];
END_ENTITY;
ENTITY b_spline_function
SUBTYPE OF (maths_function, unary_generic_expression);
SELF\unary_generic_expression.operand : maths_function;
basis : LIST[1:?] OF b_spline_basis;
DERIVE
coef : maths_function := SELF\unary_generic_expression.operand;
WHERE
WR1: function_is_table(coef);
WR2: (space_dimension(coef.range) = 1) AND
(number_superspace_of(factor1(coef.range)) = the_reals);
WR3: SIZEOF (basis) <=
SIZEOF (shape_of_array(coef));
WR4: compare_basis_and_coef(basis, coef);
END_ENTITY;
ENTITY banded_matrix
SUBTYPE OF (linearized_table_function);
default_entry : maths_value;
below : INTEGER;
above : INTEGER;
order : ordering_type;
WHERE
WR1: SIZEOF (self\explicit_table_function.shape) = 2;
WR2: -below <= above;
WR3: member_of(default_entry,
factor1(SELF\linearized_table_function.source.range));
END_ENTITY;
ENTITY basic_sparse_matrix
SUBTYPE OF (explicit_table_function, multiple_arity_generic_expression);
SELF\multiple_arity_generic_expression.operands : LIST[3:3] OF maths_function;
default_entry : maths_value;
order : ordering_type;
DERIVE
index : maths_function := SELF\multiple_arity_generic_expression.operands[1];
loc : maths_function := SELF\multiple_arity_generic_expression.operands[2];
val : maths_function := SELF\multiple_arity_generic_expression.operands[3];
WHERE
WR1: function_is_1d_table(index);
WR2: function_is_1d_table(loc);
WR3: function_is_1d_table(val);
WR4: check_sparse_index_domain(index.domain, index_base, shape, order);
WR5: check_sparse_index_to_loc(index.range, loc.domain);
WR6: loc.domain = val.domain;
WR7: check_sparse_loc_range(loc.range, index_base, shape, order);
WR8: member_of(default_entry, val.range);
END_ENTITY;
ENTITY binary_literal
SUBTYPE OF (generic_literal);
lit_value : BINARY;
END_ENTITY;
ENTITY bound_variable_semantics
SUBTYPE OF (variable_semantics);
END_ENTITY;
ENTITY cartesian_complex_number_region
SUBTYPE OF (maths_space, generic_literal);
real_constraint : real_interval;
imag_constraint : real_interval;
WHERE
WR1: min_exists(real_constraint) OR max_exists(real_constraint) OR
min_exists(imag_constraint) OR max_exists(imag_constraint);
END_ENTITY;
ENTITY complex_number_literal
SUBTYPE OF (generic_literal);
real_part : REAL;
imag_part : REAL;
END_ENTITY;
ENTITY complex_number_literal_polar
SUBTYPE OF (complex_number_literal);
modulus : REAL;
argument : REAL;
DERIVE
SELF\complex_number_literal.real_part : REAL := modulus * cos(argument);
SELF\complex_number_literal.imag_part : REAL := modulus * sin(argument);
WHERE
WR1: modulus >= 0;
WR2: {0 <= argument <= 2*PI};
END_ENTITY;
ENTITY constant_function
SUBTYPE OF (maths_function, generic_literal);
sole_output : maths_value;
source_of_domain : maths_space_or_function;
WHERE
WR1: no_cyclic_domain_reference(source_of_domain, [SELF]);
WR2: expression_is_constant(domain_from(source_of_domain));
END_ENTITY;
ENTITY definite_integral_expression
SUBTYPE OF (quantifier_expression);
lower_limit_neg_infinity : BOOLEAN;
upper_limit_pos_infinity : BOOLEAN;
DERIVE
integrand : generic_expression := SELF\multiple_arity_generic_expression.operands[1];
variable_of_integration : maths_variable := SELF\multiple_arity_generic_expression.operands[2];
SELF\quantifier_expression.variables : LIST[1:1] OF
UNIQUE
generic_variable := [variable_of_integration];
WHERE
WR1: has_values_space (integrand);
WR2: space_is_continuum (values_space_of (integrand));
WR3: definite_integral_expr_check (SELF\multiple_arity_generic_expression.operands,
lower_limit_neg_infinity, upper_limit_pos_infinity);
END_ENTITY;
ENTITY definite_integral_function
SUBTYPE OF (maths_function, unary_generic_expression);
SELF\unary_generic_expression.operand : maths_function;
variable_of_integration : input_selector;
lower_limit_neg_infinity : BOOLEAN;
upper_limit_pos_infinity : BOOLEAN;
DERIVE
integrand : maths_function := SELF\unary_generic_expression.operand;
WHERE
WR1: space_is_continuum (integrand.range);
WR2: definite_integral_check (integrand.domain, variable_of_integration,
lower_limit_neg_infinity, upper_limit_pos_infinity);
END_ENTITY;
ENTITY dependent_variable_definition
SUBTYPE OF (unary_generic_expression);
name : label;
description : text;
END_ENTITY;
ENTITY elementary_function
SUBTYPE OF (maths_function, generic_literal);
func_id : elementary_function_enumerators;
END_ENTITY;
ENTITY elementary_space
SUBTYPE OF (maths_space, generic_literal);
space_id : elementary_space_enumerators;
END_ENTITY;
ENTITY explicit_table_function
ABSTRACT SUPERTYPE
OF (ONEOF (listed_real_data,
listed_integer_data,
listed_logical_data,
listed_string_data,
listed_complex_number_data,
listed_data,
externally_listed_data,
linearized_table_function,
basic_sparse_matrix))
SUBTYPE OF (maths_function);
index_base : zero_or_one;
shape : LIST[1:?] OF positive_integer;
END_ENTITY;
ENTITY expression_denoted_function
SUBTYPE OF (maths_function, unary_generic_expression);
DERIVE
expr : generic_expression := SELF\unary_generic_expression.operand;
WHERE
WR1: (schema_prefix + 'FUNCTION_SPACE') IN TYPEOF (values_space_of(expr));
END_ENTITY;
ENTITY extended_tuple_space
SUBTYPE OF (maths_space, generic_literal);
base : tuple_space;
extender : maths_space;
WHERE
WR1: expression_is_constant(base) AND
expression_is_constant(extender);
WR2: no_cyclic_space_reference(SELF, []);
WR3: extender <> the_empty_space;
END_ENTITY;
ENTITY externally_listed_data
SUBTYPE OF (explicit_table_function, generic_literal, externally_defined_item);
value_range : maths_space;
WHERE
WR1: expression_is_constant(value_range);
END_ENTITY;
ENTITY finite_function
SUBTYPE OF (maths_function, generic_literal);
pairs : SET[1:?] OF LIST[2:2] OF maths_value;
WHERE
WR1: VALUE_UNIQUE(list_selected_components(pairs, 1));
END_ENTITY;
ENTITY finite_integer_interval
SUBTYPE OF (maths_space, generic_literal);
min : INTEGER;
max : INTEGER;
DERIVE
size : positive_integer := max - min + 1;
WHERE
WR1: min <= max;
END_ENTITY;
ENTITY finite_real_interval
SUBTYPE OF (maths_space, generic_literal);
min : REAL;
min_closure : open_closed;
max : REAL;
max_closure : open_closed;
WHERE
WR1: min < max;
END_ENTITY;
ENTITY finite_space
SUBTYPE OF (maths_space, generic_literal);
members : SET[0:?] OF maths_value;
WHERE
WR1: VALUE_UNIQUE(members);
WR2: SIZEOF (QUERY (expr <* QUERY (member <* members |
'ISO13584_GENERIC_EXPRESSIONS_SCHEMA.GENERIC_EXPRESSION' IN TYPEOF (member))
| NOT expression_is_constant(expr))) = 0;
WR3: no_cyclic_space_reference(SELF, []);
END_ENTITY;
ENTITY free_variable_semantics
SUBTYPE OF (variable_semantics);
END_ENTITY;
ENTITY function_application
SUBTYPE OF (multiple_arity_generic_expression);
func : maths_function_select;
arguments : LIST[1:?] OF maths_expression;
DERIVE
SELF\multiple_arity_generic_expression.operands : LIST[2:?] OF generic_expression := [convert_to_maths_function(func)] + convert_to_operands(arguments);
WHERE
WR1: function_applicability(func, arguments);
END_ENTITY;
ENTITY function_space
SUBTYPE OF (maths_space, generic_literal);
domain_constraint : space_constraint_type;
domain_argument : maths_space;
range_constraint : space_constraint_type;
range_argument : maths_space;
WHERE
WR1: expression_is_constant(domain_argument) AND
expression_is_constant(range_argument);
WR2: (domain_argument <> the_empty_space) AND
(range_argument <> the_empty_space);
WR3: (domain_constraint <> sc_member) OR NOT
member_of(the_empty_space,domain_argument);
WR4: (range_constraint <> sc_member) OR NOT
member_of(the_empty_space,range_argument);
WR5: NOT (any_space_satisfies(domain_constraint,domain_argument) AND
any_space_satisfies(range_constraint,range_argument));
END_ENTITY;
ENTITY general_linear_function
SUBTYPE OF (maths_function, unary_generic_expression);
SELF\unary_generic_expression.operand : maths_function;
sum_index : one_or_two;
DERIVE
mat : maths_function := SELF\unary_generic_expression.operand;
WHERE
WR1: function_is_2d_table(mat);
WR2: (space_dimension(mat.range) = 1) AND
subspace_of_es(factor1(mat.range),es_numbers);
END_ENTITY;
ENTITY homogeneous_linear_function
SUBTYPE OF (maths_function, unary_generic_expression);
SELF\unary_generic_expression.operand : maths_function;
sum_index : one_or_two;
DERIVE
mat : maths_function := SELF\unary_generic_expression.operand;
WHERE
WR1: function_is_2d_table(mat);
WR2: (space_dimension(mat.range) = 1) AND
subspace_of_es(factor1(mat.range),es_numbers);
END_ENTITY;
ENTITY imported_curve_function
SUBTYPE OF (maths_function, generic_literal);
geometry : curve;
parametric_domain : tuple_space;
WHERE
WR1: expression_is_constant(parametric_domain);
END_ENTITY;
ENTITY imported_point_function
SUBTYPE OF (maths_function, generic_literal);
geometry : point;
END_ENTITY;
ENTITY imported_surface_function
SUBTYPE OF (maths_function, generic_literal);
geometry : surface;
parametric_domain : tuple_space;
WHERE
WR1: expression_is_constant(parametric_domain);
END_ENTITY;
ENTITY imported_volume_function
SUBTYPE OF (maths_function, generic_literal);
geometry : volume;
parametric_domain : tuple_space;
WHERE
WR1: expression_is_constant(parametric_domain);
END_ENTITY;
ENTITY integer_interval_from_min
SUBTYPE OF (maths_space, generic_literal);
min : INTEGER;
END_ENTITY;
ENTITY integer_interval_to_max
SUBTYPE OF (maths_space, generic_literal);
max : INTEGER;
END_ENTITY;
ENTITY integer_tuple_literal
SUBTYPE OF (generic_literal);
lit_value : LIST[1:?] OF INTEGER;
END_ENTITY;
ENTITY linearized_table_function
SUPERTYPE OF
(ONEOF (standard_table_function,
regular_table_function,
triangular_matrix,
symmetric_matrix,
banded_matrix))
SUBTYPE OF (explicit_table_function, unary_generic_expression);
SELF\unary_generic_expression.operand : maths_function;
first : INTEGER;
DERIVE
source : maths_function := SELF\unary_generic_expression.operand;
WHERE
WR1: function_is_1d_array(source);
WR2: member_of(first, source\maths_function.domain);
END_ENTITY;
ENTITY listed_complex_number_data
SUBTYPE OF (explicit_table_function, generic_literal);
values : LIST[2:?] OF REAL;
DERIVE
SELF\explicit_table_function.shape : LIST[1:?] OF positive_integer := [ SIZEOF(values) DIV 2 ];
WHERE
WR1: NOT ODD(SIZEOF(values));
END_ENTITY;
ENTITY listed_data
SUBTYPE OF (explicit_table_function, generic_literal);
values : LIST[1:?] OF maths_value;
value_range : maths_space;
DERIVE
SELF\explicit_table_function.shape : LIST[1:?] OF positive_integer := [SIZEOF (values)];
WHERE
WR1: expression_is_constant(value_range);
WR2: SIZEOF (QUERY (val <* values | NOT (member_of( val, value_range)))) = 0;
END_ENTITY;
ENTITY listed_integer_data
SUBTYPE OF (explicit_table_function, generic_literal);
values : LIST[1:?] OF INTEGER;
DERIVE
SELF\explicit_table_function.shape : LIST[1:?] OF positive_integer := [SIZEOF (values)];
END_ENTITY;
ENTITY listed_logical_data
SUBTYPE OF (explicit_table_function, generic_literal);
values : LIST[1:?] OF LOGICAL;
DERIVE
SELF\explicit_table_function.shape : LIST[1:?] OF positive_integer := [SIZEOF (values)];
END_ENTITY;
ENTITY listed_product_space
SUBTYPE OF (maths_space, generic_literal);
factors : LIST[0:?] OF maths_space;
WHERE
WR1: SIZEOF (QUERY (space <* factors |
NOT (expression_is_constant(space)))) = 0;
WR2: no_cyclic_space_reference(SELF, []);
WR3: NOT (the_empty_space IN factors);
END_ENTITY;
ENTITY listed_real_data
SUBTYPE OF (explicit_table_function, generic_literal);
values : LIST[1:?] OF REAL;
DERIVE
SELF\explicit_table_function.shape : LIST[1:?] OF positive_integer := [SIZEOF (values)];
END_ENTITY;
ENTITY listed_string_data
SUBTYPE OF (explicit_table_function, generic_literal);
values : LIST[1:?] OF STRING;
DERIVE
SELF\explicit_table_function.shape : LIST[1:?] OF positive_integer := [SIZEOF (values)];
END_ENTITY;
ENTITY logical_literal
SUBTYPE OF (generic_literal);
lit_value : LOGICAL;
END_ENTITY;
ENTITY mathematical_description;
described : maths_expression;
describing : STRING;
encoding : label;
END_ENTITY;
ENTITY maths_boolean_variable
SUBTYPE OF (maths_variable, boolean_variable);
WHERE
WR1: subspace_of_es(SELF\maths_variable.values_space,es_booleans);
END_ENTITY;
ENTITY maths_enum_literal
SUBTYPE OF (generic_literal);
lit_value : maths_enum_atom;
END_ENTITY;
ENTITY maths_function
ABSTRACT SUPERTYPE
OF (ONEOF (finite_function,
constant_function,
selector_function,
elementary_function,
restriction_function,
repackaging_function,
reindexed_array_function,
series_composed_function,
parallel_composed_function,
explicit_table_function,
homogeneous_linear_function,
general_linear_function,
b_spline_basis,
b_spline_function,
rationalize_function,
partial_derivative_function,
definite_integral_function,
abstracted_expression_function,
expression_denoted_function,
imported_point_function,
imported_curve_function,
imported_surface_function,
imported_volume_function,
application_defined_function))
SUBTYPE OF (generic_expression);
DERIVE
domain : tuple_space := derive_function_domain(SELF);
range : tuple_space := derive_function_range(SELF);
END_ENTITY;
ENTITY maths_integer_variable
SUBTYPE OF (maths_variable, int_numeric_variable);
WHERE
WR1: subspace_of_es(SELF\maths_variable.values_space,es_integers);
END_ENTITY;
ENTITY maths_real_variable
SUBTYPE OF (maths_variable, real_numeric_variable);
WHERE
WR1: subspace_of_es(SELF\maths_variable.values_space,es_reals);
END_ENTITY;
ENTITY maths_space
ABSTRACT SUPERTYPE
OF (ONEOF (elementary_space,
finite_integer_interval,
integer_interval_from_min,
integer_interval_to_max,
finite_real_interval,
real_interval_from_min,
real_interval_to_max,
cartesian_complex_number_region,
polar_complex_number_region,
finite_space,
uniform_product_space,
listed_product_space,
extended_tuple_space,
function_space))
SUBTYPE OF (generic_expression);
END_ENTITY;
ENTITY maths_string_variable
SUBTYPE OF (maths_variable, string_variable);
WHERE
WR1: subspace_of_es(SELF\maths_variable.values_space,es_strings);
END_ENTITY;
ENTITY maths_tuple_literal
SUBTYPE OF (generic_literal);
lit_value : LIST[0:?] OF maths_value;
END_ENTITY;
ENTITY maths_variable
SUBTYPE OF (generic_variable);
values_space : maths_space;
name : label;
WHERE
WR1: expression_is_constant(values_space);
END_ENTITY;
ENTITY parallel_composed_function
SUBTYPE OF (maths_function, multiple_arity_generic_expression);
source_of_domain : maths_space_or_function;
prep_functions : LIST[1:?] OF maths_function;
final_function : maths_function_select;
DERIVE
SELF\multiple_arity_generic_expression.operands : LIST[2:?] OF generic_expression := convert_to_operands_prcmfn(source_of_domain, prep_functions, final_function);
WHERE
WR1: no_cyclic_domain_reference(source_of_domain, [SELF]);
WR2: expression_is_constant(domain_from(source_of_domain));
WR3: parallel_composed_function_domain_check(domain_from(source_of_domain),
prep_functions);
WR4: parallel_composed_function_composability_check(prep_functions, final_function);
END_ENTITY;
ENTITY partial_derivative_expression
SUBTYPE OF (unary_generic_expression);
d_variables : LIST[1:?] OF maths_variable;
extension : extension_options;
DERIVE
derivand : generic_expression := SELF\unary_generic_expression.operand;
WHERE
WR1: has_values_space (derivand);
WR2: space_is_continuum (values_space_of (derivand));
WR3: SIZEOF (QUERY (vbl <* d_variables | (NOT subspace_of (values_space_of (vbl),
the_reals)) AND (NOT subspace_of (values_space_of (vbl), the_complex_numbers))
)) = 0;
END_ENTITY;
ENTITY partial_derivative_function
SUBTYPE OF (maths_function, unary_generic_expression);
SELF\unary_generic_expression.operand : maths_function;
d_variables : LIST[1:?] OF input_selector;
extension : extension_options;
DERIVE
derivand : maths_function := SELF\unary_generic_expression.operand;
WHERE
WR1: space_is_continuum (derivand.range);
WR2: partial_derivative_check (derivand.domain, d_variables);
END_ENTITY;
ENTITY polar_complex_number_region
SUBTYPE OF (maths_space, generic_literal);
centre : complex_number_literal;
distance_constraint : real_interval;
direction_constraint : finite_real_interval;
WHERE
WR1: min_exists(distance_constraint) AND (real_min(distance_constraint) >= 0.0);
WR2: {-PI <= direction_constraint.min < PI};
WR3: direction_constraint.max - direction_constraint.min <= 2.0*PI;
WR4: (direction_constraint.max - direction_constraint.min < 2.0*PI) OR
(direction_constraint.min_closure = open);
WR5: (direction_constraint.max - direction_constraint.min < 2.0*PI) OR
(direction_constraint.max_closure = open) OR
(direction_constraint.min = -PI);
WR6: (real_min(distance_constraint) > 0.0) OR max_exists(distance_constraint) OR
(direction_constraint.max - direction_constraint.min < 2.0*PI) OR
(direction_constraint.max_closure = open);
END_ENTITY;
ENTITY quantifier_expression
ABSTRACT SUPERTYPE
SUBTYPE OF (multiple_arity_generic_expression);
variables : LIST[1:?] OF
UNIQUE
generic_variable;
WHERE
WR1: SIZEOF (QUERY (vrbl <* variables | NOT (vrbl IN
SELF\multiple_arity_generic_expression.operands))) = 0;
WR2: SIZEOF (QUERY (vrbl <* variables | NOT ((schema_prefix +
'BOUND_VARIABLE_SEMANTICS') IN TYPEOF (vrbl.interpretation.semantics)))) = 0;
END_ENTITY;
ENTITY rationalize_function
SUBTYPE OF (maths_function, unary_generic_expression);
SELF\unary_generic_expression.operand : maths_function;
DERIVE
fun : maths_function := SELF\unary_generic_expression.operand;
WHERE
WR1: (space_dimension(fun.domain) = 1) AND (space_dimension(fun.range) = 1);
WR2: number_tuple_subspace_check(factor1(fun.range));
WR3: space_dimension(factor1(fun.range)) > 1;
END_ENTITY;
ENTITY real_interval_from_min
SUBTYPE OF (maths_space, generic_literal);
min : REAL;
min_closure : open_closed;
END_ENTITY;
ENTITY real_interval_to_max
SUBTYPE OF (maths_space, generic_literal);
max : REAL;
max_closure : open_closed;
END_ENTITY;
ENTITY real_tuple_literal
SUBTYPE OF (generic_literal);
lit_value : LIST[1:?] OF REAL;
END_ENTITY;
ENTITY regular_table_function
SUBTYPE OF (linearized_table_function);
increments : LIST[1:?] OF INTEGER;
WHERE
WR1: SIZEOF (increments) = SIZEOF (self\explicit_table_function.shape);
WR2: extremal_position_check(self);
END_ENTITY;
ENTITY reindexed_array_function
SUBTYPE OF (maths_function, unary_generic_expression);
SELF\unary_generic_expression.operand : maths_function;
starting_indices : LIST[1:?] OF INTEGER;
WHERE
WR1: function_is_array(SELF\unary_generic_expression.operand);
WR2: SIZEOF(starting_indices) = SIZEOF(shape_of_array(
SELF\unary_generic_expression.operand));
END_ENTITY;
ENTITY repackaging_function
SUBTYPE OF (maths_function, unary_generic_expression);
SELF\unary_generic_expression.operand : maths_function;
input_repack : repackage_options;
output_repack : repackage_options;
selected_output : nonnegative_integer;
WHERE
WR1: (input_repack <> ro_wrap_as_tuple) OR
((space_dimension(operand.domain) = 1) AND
((schema_prefix + 'TUPLE_SPACE') IN TYPEOF (factor1(operand.domain))));
WR2: (output_repack <> ro_unwrap_tuple) OR
((space_dimension(operand.range) = 1) AND
((schema_prefix + 'TUPLE_SPACE') IN TYPEOF (factor1(operand.range))));
WR3: selected_output <= space_dimension( repackage(
operand.range, output_repack));
END_ENTITY;
ENTITY restriction_function
SUBTYPE OF (maths_function, unary_generic_expression);
SELF\unary_generic_expression.operand : maths_space;
END_ENTITY;
ENTITY selector_function
SUBTYPE OF (maths_function, generic_literal);
selector : input_selector;
source_of_domain : maths_space_or_function;
WHERE
WR1: no_cyclic_domain_reference(source_of_domain, [SELF]);
WR2: expression_is_constant(domain_from(source_of_domain));
END_ENTITY;
ENTITY series_composed_function
SUBTYPE OF (maths_function, multiple_arity_generic_expression);
SELF\multiple_arity_generic_expression.operands : LIST[2:?] OF maths_function;
WHERE
WR1: composable_sequence(SELF\multiple_arity_generic_expression.operands);
END_ENTITY;
ENTITY standard_table_function
SUBTYPE OF (linearized_table_function);
order : ordering_type;
WHERE
WR1: extremal_position_check(SELF);
END_ENTITY;
ENTITY strict_triangular_matrix
SUBTYPE OF (triangular_matrix);
main_diagonal_value : maths_value;
END_ENTITY;
ENTITY symmetric_banded_matrix
SUBTYPE OF (symmetric_matrix);
default_entry : maths_value;
above : nonnegative_integer;
WHERE
WR1: member_of(default_entry,
factor1(SELF\linearized_table_function.source.range));
END_ENTITY;
ENTITY symmetric_matrix
SUBTYPE OF (linearized_table_function);
symmetry : symmetry_type;
triangle : lower_upper;
order : ordering_type;
WHERE
WR1: SIZEOF (SELF\explicit_table_function.shape) = 2;
WR2: SELF\explicit_table_function.shape[1] =
SELF\explicit_table_function.shape[2];
WR3: NOT (symmetry = symmetry_type.skew) OR (
(space_dimension(SELF\linearized_table_function.source.range) = 1) AND
subspace_of_es(factor1(SELF\linearized_table_function.source.range),
es_numbers));
WR4: NOT ((symmetry = symmetry_type.hermitian) OR (symmetry = symmetry_type.skew_hermitian)) OR (
(space_dimension(SELF\linearized_table_function.source.range) = 1) AND
subspace_of_es(factor1(SELF\linearized_table_function.source.range),
es_complex_numbers));
END_ENTITY;
ENTITY triangular_matrix
SUBTYPE OF (linearized_table_function);
default_entry : maths_value;
lo_up : lower_upper;
order : ordering_type;
WHERE
WR1: SIZEOF (SELF\explicit_table_function.shape) = 2;
WR2: member_of(default_entry, SELF\maths_function.range);
END_ENTITY;
ENTITY uniform_product_space
SUBTYPE OF (maths_space, generic_literal);
base : maths_space;
exponent : positive_integer;
WHERE
WR1: expression_is_constant(base);
WR2: no_cyclic_space_reference(SELF, []);
WR3: base <> the_empty_space;
END_ENTITY;
FUNCTION all_members_of_es
(sv : SET[0:?] OF maths_value; es : elementary_space_enumerators) : LOGICAL;
CONSTANT
base_types : SET OF STRING := ['NUMBER','COMPLEX_NUMBER_LITERAL','REAL',
'INTEGER','LOGICAL','BOOLEAN','STRING','BINARY','MATHS_SPACE',
'MATHS_FUNCTION','LIST','ELEMENTARY_SPACE_ENUMERATORS','ORDERING_TYPE',
'LOWER_UPPER','SYMMETRY_TYPE','ELEMENTARY_FUNCTION_ENUMERATORS',
'OPEN_CLOSED','SPACE_CONSTRAINT_TYPE','REPACKAGE_OPTIONS',
'EXTENSION_OPTIONS'];
END_CONSTANT;
LOCAL
v : maths_value;
key_type : STRING := '';
types : SET OF STRING;
ge : generic_expression;
cum : LOGICAL := TRUE;
vspc : maths_space;
END_LOCAL;
IF NOT EXISTS (sv) OR NOT EXISTS (es) THEN RETURN (FALSE); END_IF;
CASE es OF
es_numbers : key_type := 'NUMBER';
es_complex_numbers : key_type := 'COMPLEX_NUMBER_LITERAL';
es_reals : key_type := 'REAL';
es_integers : key_type := 'INTEGER';
es_logicals : key_type := 'LOGICAL';
es_booleans : key_type := 'BOOLEAN';
es_strings : key_type := 'STRING';
es_binarys : key_type := 'BINARY';
es_maths_spaces : key_type := 'MATHS_SPACE';
es_maths_functions : key_type := 'MATHS_FUNCTION';
es_generics : RETURN (TRUE);
END_CASE;
REPEAT i := 1 TO SIZEOF (sv);
IF NOT EXISTS (sv[i]) THEN RETURN (FALSE); END_IF;
v := simplify_maths_value(sv[i]);
types := stripped_typeof(v);
IF key_type IN types THEN SKIP; END_IF;
IF (es = es_numbers) AND ('COMPLEX_NUMBER_LITERAL' IN types) THEN SKIP; END_IF;
IF SIZEOF (base_types * types) > 0 THEN RETURN (FALSE); END_IF;
-- Must be a generic_expression which doesn't simplify and which is not a
-- complex_number_literal, maths_space, or maths_function.
ge := v;
IF has_values_space(ge) THEN
vspc := values_space_of(ge);
IF NOT subspace_of_es(vspc,es) THEN
IF NOT compatible_spaces(vspc,make_elementary_space(es)) THEN
RETURN (FALSE);
END_IF;
cum := UNKNOWN;
END_IF;
ELSE
cum := UNKNOWN;
END_IF;
IF cum = FALSE THEN RETURN (FALSE); END_IF;
END_REPEAT;
RETURN (cum);
END_FUNCTION;
FUNCTION any_space_satisfies
(sc : space_constraint_type; spc : maths_space) : BOOLEAN;
LOCAL
spc_id : elementary_space_enumerators;
END_LOCAL;
IF (sc = sc_equal) OR NOT ('ELEMENTARY_SPACE' IN stripped_typeof(spc)) THEN
RETURN (FALSE);
END_IF;
spc_id := spc\elementary_space.space_id;
IF sc = sc_subspace THEN
RETURN (bool(spc_id = es_generics));
END_IF;
IF sc = sc_member THEN
RETURN (bool((spc_id = es_generics) OR (spc_id = es_maths_spaces)));
END_IF;
-- Should be unreachable.
RETURN (?);
END_FUNCTION;
FUNCTION assoc_product_space
(ts1 : tuple_space; ts2 : tuple_space) : tuple_space;
LOCAL
types1 : SET OF STRING := stripped_typeof (ts1);
types2 : SET OF STRING := stripped_typeof (ts2);
up1, up2 : uniform_product_space := make_uniform_product_space(the_reals,1);
lp1, lp2, lps : listed_product_space := the_zero_tuple_space;
et1, et2, ets : extended_tuple_space := the_tuples;
use_up1, use_up2, use_lp1, use_lp2 : BOOLEAN;
factors : LIST OF maths_space := [];
tspace : tuple_space;
END_LOCAL;
-- Identify type of first operand
IF 'UNIFORM_PRODUCT_SPACE' IN types1 THEN
up1 := ts1; use_up1 := true; use_lp1 := false;
ELSE
IF 'LISTED_PRODUCT_SPACE' IN types1 THEN
lp1 := ts1; use_up1 := false; use_lp1 := true;
ELSE
IF NOT ('EXTENDED_TUPLE_SPACE' IN types1) THEN
-- Unreachable when this function was written.
RETURN (?);
END_IF;
et1 := ts1; use_up1 := false; use_lp1 := false;
END_IF;
END_IF;
-- Identify type of second operand
IF 'UNIFORM_PRODUCT_SPACE' IN types2 THEN
up2 := ts2; use_up2 := true; use_lp2 := false;
ELSE
IF 'LISTED_PRODUCT_SPACE' IN types2 THEN
lp2 := ts2; use_up2 := false; use_lp2 := true;
ELSE
IF NOT ('EXTENDED_TUPLE_SPACE' IN types2) THEN
-- Unreachable when this function was written.
RETURN (?);
END_IF;
et2 := ts2; use_up2 := false; use_lp2 := false;
END_IF;
END_IF;
-- Construction for each combination of cases
IF use_up1 THEN
IF use_up2 THEN
IF up1.base = up2.base THEN
tspace := make_uniform_product_space(up1.base, up1.exponent + up2.exponent);
ELSE
factors := [up1.base : up1.exponent, up2.base : up2.exponent];
tspace := make_listed_product_space(factors);
END_IF;
ELSE
IF use_lp2 THEN
-- Avoid compiler confusion by breaking into two lines.
factors := [up1.base : up1.exponent];
factors := factors + lp2.factors;
tspace := make_listed_product_space(factors);
ELSE
tspace := assoc_product_space(up1, et2.base);
tspace := make_extended_tuple_space(tspace, et2.extender);
END_IF;
END_IF;
ELSE
IF use_lp1 THEN
IF use_up2 THEN
-- Avoid compiler confusion by breaking into two lines.
factors := [up2.base : up2.exponent];
factors := lp1.factors + factors;
tspace := make_listed_product_space(factors);
ELSE
IF use_lp2 THEN
tspace := make_listed_product_space(lp1.factors + lp2.factors);
ELSE
tspace := assoc_product_space(lp1, et2.base);
tspace := make_extended_tuple_space(tspace, et2.extender);
END_IF;
END_IF;
ELSE
IF use_up2 THEN
IF et1.extender = up2.base THEN
tspace := assoc_product_space(et1.base, up2);
tspace := make_extended_tuple_space(tspace, et1.extender);
ELSE
-- No subtype is available to represent this cartesian product.
RETURN (?);
END_IF;
ELSE
IF use_lp2 THEN
factors := lp2.factors;
REPEAT i := 1 TO SIZEOF (factors);
IF et1.extender <> factors[i] THEN
-- No subtype available to represent this cartesian product.
RETURN (?);
END_IF;
END_REPEAT;
tspace := assoc_product_space(et1.base, lp2);
tspace := make_extended_tuple_space(tspace, et1.extender);
ELSE
IF et1.extender = et2.extender THEN
-- Next line may assign indeterminate (?) to tspace.
tspace := assoc_product_space(et1, et2.base);
ELSE
-- No subtype available to represent this cartesian product.
RETURN (?);
END_IF;
END_IF;
END_IF;
END_IF;
END_IF;
RETURN (tspace);
END_FUNCTION;
FUNCTION atan2
(y : REAL; x : REAL) : REAL;
LOCAL
r : REAL;
END_LOCAL;
IF (y = 0.0) AND (x = 0.0) THEN RETURN (?); END_IF;
r := atan(y,x);
IF x < 0.0 THEN
IF y < 0.0 THEN r := r - PI;
ELSE r := r + PI; END_IF;
END_IF;
RETURN (r);
END_FUNCTION;
FUNCTION bool
(lgcl : LOGICAL) : BOOLEAN;
IF NOT EXISTS (lgcl) THEN RETURN (FALSE); END_IF;
IF lgcl <> TRUE THEN RETURN (FALSE); END_IF;
RETURN (TRUE);
END_FUNCTION;
FUNCTION check_sparse_index_domain
(idxdom : tuple_space; base : zero_or_one; shape : LIST[1:?] OF positive_integer; order : ordering_type) : BOOLEAN;
LOCAL
mthspc : maths_space;
interval : finite_integer_interval;
i : INTEGER;
END_LOCAL;
mthspc := factor1(idxdom);
-- A consequence of WR1 of basic_sparse_matrix is that here we need only
-- consider the case that mthspc is a finite integer interval and is the only
-- factor space of idxdom.
interval := mthspc;
IF order = by_rows THEN i := 1; ELSE i := 2; END_IF;
RETURN (bool((interval.min <= base) AND (interval.max >= base + shape[i])));
END_FUNCTION;
FUNCTION check_sparse_index_to_loc
(index_range : tuple_space; loc_domain : tuple_space) : BOOLEAN;
LOCAL
temp : maths_space;
idx_rng_itvl, loc_dmn_itvl : finite_integer_interval;
END_LOCAL;
temp := factor1 (index_range);
IF (schema_prefix + 'TUPLE_SPACE') IN TYPEOF (temp) THEN
temp := factor1 (temp);
END_IF;
IF NOT ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN TYPEOF (temp)) THEN
RETURN (FALSE);
END_IF;
idx_rng_itvl := temp;
temp := factor1 (loc_domain);
IF (schema_prefix + 'TUPLE_SPACE') IN TYPEOF (temp) THEN
temp := factor1 (temp);
END_IF;
IF NOT ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN TYPEOF (temp)) THEN
RETURN (FALSE);
END_IF;
loc_dmn_itvl := temp;
RETURN (bool((loc_dmn_itvl.min <= idx_rng_itvl.min) AND
(idx_rng_itvl.max <= loc_dmn_itvl.max+1)));
END_FUNCTION;
FUNCTION check_sparse_loc_range
(locrng : tuple_space; base : zero_or_one; shape : LIST[1:?] OF positive_integer; order : ordering_type) : BOOLEAN;
LOCAL
mthspc : maths_space;
interval : finite_integer_interval;
i : INTEGER;
END_LOCAL;
IF space_dimension(locrng) <> 1 THEN RETURN (FALSE); END_IF;
mthspc := factor1(locrng);
IF NOT ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN TYPEOF (mthspc)) THEN
RETURN (FALSE);
END_IF;
interval := mthspc;
IF order = by_rows THEN i := 2; ELSE i := 1; END_IF;
RETURN (bool((interval.min >= base) AND (interval.max <= base + shape[i] - 1)));
END_FUNCTION;
FUNCTION compare_basis_and_coef
(basis : LIST[1:?] OF b_spline_basis; coef : maths_function) : BOOLEAN;
LOCAL
shape : LIST OF positive_integer;
END_LOCAL;
IF NOT EXISTS (basis) OR NOT EXISTS (coef) THEN RETURN (FALSE); END_IF;
shape := shape_of_array(coef);
IF NOT EXISTS (shape) THEN RETURN (FALSE); END_IF;
IF SIZEOF (shape) < SIZEOF (basis) THEN RETURN (FALSE); END_IF;
REPEAT i := 1 TO SIZEOF (basis);
IF (basis[i].num_basis = shape[i]) <> TRUE THEN RETURN (FALSE); END_IF;
END_REPEAT;
RETURN (TRUE);
END_FUNCTION;
FUNCTION compare_list_and_value
(lv : LIST[0:?] OF GENERIC : G; op : elementary_function_enumerators; v : GENERIC : G) : BOOLEAN;
IF NOT EXISTS (lv) OR NOT EXISTS (op) OR NOT EXISTS (v) THEN
RETURN (FALSE);
END_IF;
REPEAT i := 1 TO SIZEOF (lv);
IF NOT compare_values(lv[i], op, v) THEN
RETURN (FALSE);
END_IF;
END_REPEAT;
RETURN (TRUE);
END_FUNCTION;
FUNCTION compare_values
(v1 : GENERIC : G; op : elementary_function_enumerators; v2 : GENERIC : G) : BOOLEAN;
LOCAL
logl : LOGICAL := UNKNOWN;
END_LOCAL;
IF NOT EXISTS (v1) OR NOT EXISTS (op) OR NOT EXISTS (v2) THEN
RETURN (FALSE);
END_IF;
CASE op OF
ef_eq_i : logl := (v1 = v2);
ef_ne_i : logl := (v1 <> v2);
ef_gt_i : logl := (v1 > v2);
ef_lt_i : logl := (v1 < v2);
ef_ge_i : logl := (v1 >= v2);
ef_le_i : logl := (v1 <= v2);
END_CASE;
IF EXISTS (logl) THEN
IF logl = TRUE THEN RETURN (TRUE); END_IF;
END_IF;
RETURN (FALSE);
END_FUNCTION;
FUNCTION compatible_complex_number_regions
(sp1 : maths_space; sp2 : maths_space) : BOOLEAN;
LOCAL
typenames : SET OF string := stripped_typeof (sp1);
crgn1, crgn2 : cartesian_complex_number_region;
prgn1, prgn2, prgn1c2, prgn2c1 : polar_complex_number_region;
sp1_is_crgn, sp2_is_crgn : BOOLEAN;
END_LOCAL;
IF 'CARTESIAN_COMPLEX_NUMBER_REGION' IN typenames THEN
sp1_is_crgn := TRUE;
crgn1 := sp1;
ELSE
IF 'POLAR_COMPLEX_NUMBER_REGION' IN typenames THEN
sp1_is_crgn := FALSE;
prgn1 := sp1;
ELSE
-- Improper usage: Default response is to assume compatibility.
RETURN (TRUE);
END_IF;
END_IF;
typenames := stripped_typeof (sp2);
IF 'CARTESIAN_COMPLEX_NUMBER_REGION' IN typenames THEN
sp2_is_crgn := TRUE;
crgn2 := sp2;
ELSE
IF 'POLAR_COMPLEX_NUMBER_REGION' IN typenames THEN
sp2_is_crgn := FALSE;
prgn2 := sp2;
ELSE
-- Improper usage: Default response is to assume compatibility.
RETURN (TRUE);
END_IF;
END_IF;
IF sp1_is_crgn AND sp2_is_crgn THEN
-- two cartesian regions
RETURN (compatible_intervals(crgn1.real_constraint, crgn2.real_constraint)
AND compatible_intervals(crgn1.imag_constraint, crgn2.imag_constraint));
END_IF;
IF NOT sp1_is_crgn AND NOT sp2_is_crgn AND
(prgn1.centre.real_part = prgn2.centre.real_part) AND
(prgn1.centre.imag_part = prgn2.centre.imag_part) THEN
-- two polar regions with common centre
IF NOT compatible_intervals(prgn1.distance_constraint,
prgn2.distance_constraint) THEN
RETURN (FALSE);
END_IF;
IF compatible_intervals(prgn1.direction_constraint,
prgn2.direction_constraint) THEN
RETURN (TRUE);
END_IF;
-- Deal with direction ambiguity by 2 pi.
IF (prgn1.direction_constraint.max > PI) AND (prgn2.direction_constraint.max < PI)
THEN
RETURN (compatible_intervals(prgn2.direction_constraint,
make_finite_real_interval(-PI,open,prgn1.direction_constraint.max-2.0*PI,
prgn1.direction_constraint.max_closure)));
END_IF;
IF (prgn2.direction_constraint.max > PI) AND (prgn1.direction_constraint.max < PI)
THEN
RETURN (compatible_intervals(prgn1.direction_constraint,
make_finite_real_interval(-PI,open,prgn2.direction_constraint.max-2.0*PI,
prgn2.direction_constraint.max_closure)));
END_IF;
RETURN (FALSE);
END_IF;
-- Make do with imperfect tests for remaining cases.
IF sp1_is_crgn AND NOT sp2_is_crgn THEN
crgn2 := enclose_pregion_in_cregion(prgn2);
prgn1 := enclose_cregion_in_pregion(crgn1,prgn2.centre);
RETURN (compatible_complex_number_regions(crgn1,crgn2)
AND compatible_complex_number_regions(prgn1,prgn2));
END_IF;
IF NOT sp1_is_crgn AND sp2_is_crgn THEN
crgn1 := enclose_pregion_in_cregion(prgn1);
prgn2 := enclose_cregion_in_pregion(crgn2,prgn1.centre);
RETURN (compatible_complex_number_regions(crgn1,crgn2)
AND compatible_complex_number_regions(prgn1,prgn2));
END_IF;
-- Two polar regions with different centres
prgn1c2 := enclose_pregion_in_pregion(prgn1,prgn2.centre);
prgn2c1 := enclose_pregion_in_pregion(prgn2,prgn1.centre);
RETURN (compatible_complex_number_regions(prgn1,prgn2c1)
AND compatible_complex_number_regions(prgn1c2,prgn2));
END_FUNCTION;
FUNCTION compatible_es_values
(esval1 : elementary_space_enumerators; esval2 : elementary_space_enumerators) : BOOLEAN;
LOCAL
esval1_is_numeric, esval2_is_numeric : LOGICAL;
END_LOCAL;
IF (esval1 = esval2) OR (esval1 = es_generics) OR (esval2 = es_generics) THEN
RETURN (TRUE);
END_IF;
esval1_is_numeric := (esval1 >= es_numbers) AND (esval1 <= es_integers);
esval2_is_numeric := (esval2 >= es_numbers) AND (esval2 <= es_integers);
IF (esval1_is_numeric AND (esval2 = es_numbers)) OR
(esval2_is_numeric AND (esval1 = es_numbers)) THEN
RETURN (TRUE);
END_IF;
IF esval1_is_numeric XOR esval2_is_numeric THEN
RETURN (FALSE);
END_IF;
IF ((esval1 = es_logicals) AND (esval2 = es_booleans)) OR
((esval1 = es_booleans) AND (esval2 = es_logicals)) THEN
RETURN (TRUE);
END_IF;
-- All other cases are incompatible
RETURN (FALSE);
END_FUNCTION;
FUNCTION compatible_intervals
(sp1 : maths_space; sp2 : maths_space) : BOOLEAN;
LOCAL
amin, amax : REAL;
END_LOCAL;
IF min_exists(sp1) AND max_exists(sp2) THEN
amin := real_min(sp1); amax := real_max(sp2);
IF amin > amax THEN RETURN (FALSE); END_IF;
IF amin = amax THEN
RETURN (min_included(sp1) AND max_included(sp2));
END_IF;
END_IF;
IF min_exists(sp2) AND max_exists(sp1) THEN
amin := real_min(sp2); amax := real_max(sp1);
IF amin > amax THEN RETURN (FALSE); END_IF;
IF amin = amax THEN
RETURN (min_included(sp2) AND max_included(sp1));
END_IF;
END_IF;
RETURN (TRUE);
END_FUNCTION;
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;
FUNCTION composable_sequence
(operands : LIST[2:?] OF maths_function) : BOOLEAN;
REPEAT i := 1 TO SIZEOF (operands) - 1;
IF NOT compatible_spaces (operands[i].range, operands[i+1].domain) THEN
RETURN (FALSE);
END_IF;
END_REPEAT;
RETURN (TRUE);
END_FUNCTION;
FUNCTION convert_to_literal
(val : maths_atom) : generic_literal;
LOCAL
types : SET OF STRING := TYPEOF (val);
END_LOCAL;
IF 'INTEGER' IN types THEN RETURN (make_int_literal (val)); END_IF;
IF 'REAL' IN types THEN RETURN (make_real_literal (val)); END_IF;
IF 'BOOLEAN' IN types THEN RETURN (make_boolean_literal (val)); END_IF;
IF 'STRING' IN types THEN RETURN (make_string_literal (val)); END_IF;
IF 'LOGICAL' IN types THEN RETURN (make_logical_literal (val)); END_IF;
IF 'BINARY' IN types THEN RETURN (make_binary_literal (val)); END_IF;
IF (schema_prefix + 'MATHS_ENUM_ATOM') IN types THEN
RETURN (make_maths_enum_literal (val));
END_IF;
-- Should be unreachable
RETURN (?);
END_FUNCTION;
FUNCTION convert_to_maths_function
(func : maths_function_select) : maths_function;
LOCAL
efenum : elementary_function_enumerators;
mthfun : maths_function;
END_LOCAL;
IF (schema_prefix + 'MATHS_FUNCTION') IN TYPEOF (func) THEN
mthfun := func;
ELSE
efenum := func;
mthfun := make_elementary_function (efenum);
END_IF;
RETURN (mthfun);
END_FUNCTION;
FUNCTION convert_to_maths_value
(val : GENERIC : G) : maths_value;
LOCAL
types : SET OF STRING := TYPEOF (val);
ival : maths_integer;
rval : maths_real;
nval : maths_number;
tfval : maths_boolean;
lval : maths_logical;
sval : maths_string;
bval : maths_binary;
tval : maths_tuple := the_empty_maths_tuple;
mval : maths_value;
END_LOCAL;
IF (schema_prefix + 'MATHS_VALUE') IN types THEN RETURN (val); END_IF;
IF 'INTEGER' IN types THEN ival := val; RETURN (ival); END_IF;
IF 'REAL' IN types THEN rval := val; RETURN (rval); END_IF;
IF 'NUMBER' IN types THEN nval := val; RETURN (nval); END_IF;
IF 'BOOLEAN' IN types THEN tfval := val; RETURN (tfval); END_IF;
IF 'LOGICAL' IN types THEN lval := val; RETURN (lval); END_IF;
IF 'STRING' IN types THEN sval := val; RETURN (sval); END_IF;
IF 'BINARY' IN types THEN bval := val; RETURN (bval); END_IF;
IF 'LIST' IN types THEN
REPEAT i := 1 TO SIZEOF (val);
mval := convert_to_maths_value (val[i]);
IF NOT EXISTS (mval) THEN RETURN (?); END_IF;
INSERT (tval, mval, i-1);
END_REPEAT;
RETURN (tval);
END_IF;
RETURN (?);
END_FUNCTION;
FUNCTION convert_to_operand
(val : maths_value) : generic_expression;
LOCAL
types : SET OF STRING := stripped_typeof (val);
END_LOCAL;
-- Use intermediate variables of appropriate declared types to help the compilers.
IF 'GENERIC_EXPRESSION' IN types THEN RETURN (val); END_IF;
IF 'MATHS_ATOM' IN types THEN RETURN (convert_to_literal (val)); END_IF;
IF 'ATOM_BASED_VALUE' IN types THEN RETURN (make_atom_based_literal(val)); END_IF;
IF 'MATHS_TUPLE' IN types THEN RETURN (make_maths_tuple_literal(val)); END_IF;
-- Should be unreachable
RETURN (?);
END_FUNCTION;
FUNCTION convert_to_operands
(values : AGGREGATE OF maths_value) : LIST[0:?] OF generic_expression;
LOCAL
operands : LIST OF generic_expression := [];
loc : INTEGER := 0;
END_LOCAL;
IF NOT EXISTS (values) THEN RETURN (?); END_IF;
REPEAT i := LOINDEX (values) TO HIINDEX (values);
INSERT (operands, convert_to_operand (values[i]), loc);
loc := loc + 1;
END_REPEAT;
RETURN (operands);
END_FUNCTION;
FUNCTION convert_to_operands_prcmfn
(srcdom : maths_space_or_function; prepfun : LIST[0:?] OF maths_function; finfun : maths_function_select) : LIST[2:?] OF generic_expression;
LOCAL
operands : LIST OF generic_expression := [];
END_LOCAL;
INSERT (operands, srcdom, 0);
REPEAT i := 1 TO SIZEOF (prepfun);
INSERT (operands, prepfun[i], i);
END_REPEAT;
INSERT (operands, convert_to_maths_function (finfun), SIZEOF (prepfun)+1);
RETURN (operands);
END_FUNCTION;
FUNCTION definite_integral_check
(domain : tuple_space; vrblint : input_selector; lowerinf : BOOLEAN; upperinf : BOOLEAN) : BOOLEAN;
LOCAL
domn : tuple_space := domain;
fspc : maths_space;
dim : nonnegative_integer;
k : positive_integer;
END_LOCAL;
IF (space_dimension (domain) = 1) AND ((schema_prefix + 'TUPLE_SPACE') IN
TYPEOF (factor1 (domain))) THEN
domn := factor1 (domain);
END_IF;
dim := space_dimension (domn);
k := vrblint;
IF k > dim THEN RETURN (FALSE); END_IF;
fspc := factor_space (domn, k);
IF NOT ((schema_prefix + 'REAL_INTERVAL') IN TYPEOF (fspc)) THEN
RETURN (FALSE);
END_IF;
IF lowerinf AND min_exists (fspc) THEN RETURN (FALSE); END_IF;
IF upperinf AND max_exists (fspc) THEN RETURN (FALSE); END_IF;
RETURN (TRUE);
END_FUNCTION;
FUNCTION definite_integral_expr_check
(operands : LIST[2:?] OF generic_expression; lowerinf : BOOLEAN; upperinf : BOOLEAN) : BOOLEAN;
LOCAL
nops : INTEGER := 2;
vspc : maths_space;
dim : nonnegative_integer;
k : positive_integer;
bspc : maths_space;
END_LOCAL;
IF NOT lowerinf THEN nops := nops + 1; END_IF;
IF NOT upperinf THEN nops := nops + 1; END_IF;
IF SIZEOF (operands) <> nops THEN RETURN (FALSE); END_IF;
IF NOT ('GENERIC_VARIABLE' IN stripped_typeof(operands[2])) THEN
RETURN (FALSE);
END_IF;
IF NOT has_values_space (operands[2]) THEN RETURN (FALSE); END_IF;
vspc := values_space_of (operands[2]);
IF NOT ('REAL_INTERVAL' IN stripped_typeof(vspc)) THEN RETURN (FALSE); END_IF;
IF lowerinf THEN
IF min_exists (vspc) THEN RETURN (FALSE); END_IF;
k := 3;
ELSE
IF NOT has_values_space (operands[3]) THEN RETURN (FALSE); END_IF;
bspc := values_space_of (operands[3]);
IF NOT compatible_spaces (bspc, vspc) THEN RETURN (FALSE); END_IF;
k := 4;
END_IF;
IF upperinf THEN
IF max_exists (vspc) THEN RETURN (FALSE); END_IF;
ELSE
IF NOT has_values_space (operands[k]) THEN RETURN (FALSE); END_IF;
bspc := values_space_of (operands[k]);
IF NOT compatible_spaces (bspc, vspc) THEN RETURN (FALSE); END_IF;
END_IF;
RETURN (TRUE);
END_FUNCTION;
FUNCTION derive_definite_integral_domain
(igrl : definite_integral_function) : tuple_space;
FUNCTION process_product_space(spc : product_space;
idx, prefix : INTEGER;
vdomn : maths_space) : product_space;
LOCAL
uspc : uniform_product_space;
expnt : INTEGER;
factors : LIST OF maths_space;
END_LOCAL;
IF (schema_prefix + 'UNIFORM_PRODUCT_SPACE') IN TYPEOF (spc) THEN
uspc := spc;
expnt := uspc.exponent + prefix;
IF idx <= uspc.exponent THEN expnt := expnt - 1; END_IF;
IF expnt = 0 THEN
RETURN (make_listed_product_space([]));
ELSE
RETURN (make_uniform_product_space(uspc.base,expnt));
END_IF;
ELSE
factors := spc\listed_product_space.factors;
IF idx <= SIZEOF (factors) THEN REMOVE (factors, idx); END_IF;
IF prefix > 0 THEN
INSERT (factors, vdomn, 0);
IF prefix > 1 THEN INSERT (factors, vdomn, 0); END_IF;
END_IF;
RETURN (make_listed_product_space(factors));
END_IF;
END_FUNCTION; -- process_product_space
-- Resume body of derive_definite_integral_domain function
LOCAL
idomn : tuple_space := igrl.integrand.domain;
types : SET OF STRING := TYPEOF (idomn);
idx : INTEGER := igrl.variable_of_integration;
tupled : BOOLEAN := bool(((space_dimension(idomn) = 1) AND
((schema_prefix + 'TUPLE_SPACE') IN types)));
prefix : INTEGER := 0;
espc : extended_tuple_space;
vdomn : maths_space;
END_LOCAL;
IF tupled THEN
idomn := factor1(idomn);
types := TYPEOF (idomn);
END_IF;
IF igrl.lower_limit_neg_infinity THEN prefix := prefix + 1; END_IF;
IF igrl.upper_limit_pos_infinity THEN prefix := prefix + 1; END_IF;
vdomn := factor_space(idomn,idx);
IF (schema_prefix + 'EXTENDED_TUPLE_SPACE') IN types THEN
espc := idomn;
idomn := make_extended_tuple_space(process_product_space(espc.base,idx,
prefix,vdomn),espc.extender);
ELSE
idomn := process_product_space(idomn,idx,prefix,vdomn);
END_IF;
IF tupled THEN RETURN (one_tuples_of(idomn));
ELSE RETURN (idomn); END_IF;
END_FUNCTION;
FUNCTION derive_elementary_function_domain
(ef_val : elementary_function_enumerators) : tuple_space;
IF NOT EXISTS (ef_val) THEN RETURN (?); END_IF;
CASE ef_val OF
ef_and : RETURN (make_extended_tuple_space (the_zero_tuple_space, the_logicals));
ef_or : RETURN (make_extended_tuple_space (the_zero_tuple_space, the_logicals));
ef_not : RETURN (make_uniform_product_space (the_logicals, 1));
ef_xor : RETURN (make_uniform_product_space (the_logicals, 2));
ef_negate_i : RETURN (make_uniform_product_space (the_integers, 1));
ef_add_i : RETURN (the_integer_tuples);
ef_subtract_i : RETURN (make_uniform_product_space (the_integers, 2));
ef_multiply_i : RETURN (the_integer_tuples);
ef_divide_i : RETURN (make_uniform_product_space (the_integers, 2));
ef_mod_i : RETURN (make_uniform_product_space (the_integers, 2));
ef_exponentiate_i : RETURN (make_uniform_product_space (the_integers, 2));
ef_eq_i : RETURN (make_uniform_product_space (the_integers, 2));
ef_ne_i : RETURN (make_uniform_product_space (the_integers, 2));
ef_gt_i : RETURN (make_uniform_product_space (the_integers, 2));
ef_lt_i : RETURN (make_uniform_product_space (the_integers, 2));
ef_ge_i : RETURN (make_uniform_product_space (the_integers, 2));
ef_le_i : RETURN (make_uniform_product_space (the_integers, 2));
ef_abs_i : RETURN (make_uniform_product_space (the_integers, 1));
ef_if_i : RETURN (make_listed_product_space ([the_logicals, the_integers,
the_integers]));
ef_negate_r : RETURN (make_uniform_product_space (the_reals, 1));
ef_reciprocal_r : RETURN (make_uniform_product_space (the_reals, 1));
ef_add_r : RETURN (the_real_tuples);
ef_subtract_r : RETURN (make_uniform_product_space (the_reals, 2));
ef_multiply_r : RETURN (the_real_tuples);
ef_divide_r : RETURN (make_uniform_product_space (the_reals, 2));
ef_mod_r : RETURN (make_uniform_product_space (the_reals, 2));
ef_exponentiate_r : RETURN (make_listed_product_space ([the_nonnegative_reals,
the_reals]));
ef_exponentiate_ri : RETURN (make_listed_product_space ([the_reals, the_integers]));
ef_eq_r : RETURN (make_uniform_product_space (the_reals, 2));
ef_ne_r : RETURN (make_uniform_product_space (the_reals, 2));
ef_gt_r : RETURN (make_uniform_product_space (the_reals, 2));
ef_lt_r : RETURN (make_uniform_product_space (the_reals, 2));
ef_ge_r : RETURN (make_uniform_product_space (the_reals, 2));
ef_le_r : RETURN (make_uniform_product_space (the_reals, 2));
ef_abs_r : RETURN (make_uniform_product_space (the_reals, 1));
ef_acos_r : RETURN (make_uniform_product_space (the_neg1_one_interval, 1));
ef_asin_r : RETURN (make_uniform_product_space (the_neg1_one_interval, 1));
ef_atan2_r : RETURN (make_uniform_product_space (the_reals, 2));
ef_cos_r : RETURN (make_uniform_product_space (the_reals, 1));
ef_exp_r : RETURN (make_uniform_product_space (the_reals, 1));
ef_ln_r : RETURN (make_uniform_product_space (the_nonnegative_reals, 1));
ef_log2_r : RETURN (make_uniform_product_space (the_nonnegative_reals, 1));
ef_log10_r : RETURN (make_uniform_product_space (the_nonnegative_reals, 1));
ef_sin_r : RETURN (make_uniform_product_space (the_reals, 1));
ef_sqrt_r : RETURN (make_uniform_product_space (the_nonnegative_reals, 1));
ef_tan_r : RETURN (make_uniform_product_space (the_reals, 1));
ef_if_r : RETURN (make_listed_product_space ([the_logicals, the_reals, the_reals]));
ef_negate_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_reciprocal_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_add_c : RETURN (the_complex_tuples);
ef_subtract_c : RETURN (make_uniform_product_space (the_complex_numbers, 2));
ef_multiply_c : RETURN (the_complex_tuples);
ef_divide_c : RETURN (make_uniform_product_space (the_complex_numbers, 2));
ef_exponentiate_c : RETURN (make_uniform_product_space (the_complex_numbers, 2));
ef_exponentiate_ci : RETURN (make_listed_product_space ([the_complex_numbers,
the_integers]));
ef_eq_c : RETURN (make_uniform_product_space (the_complex_numbers, 2));
ef_ne_c : RETURN (make_uniform_product_space (the_complex_numbers, 2));
ef_conjugate_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_abs_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_arg_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_cos_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_exp_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_ln_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_sin_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_sqrt_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_tan_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_if_c : RETURN (make_listed_product_space ([the_logicals, the_complex_numbers,
the_complex_numbers]));
ef_subscript_s : RETURN (make_listed_product_space ([the_strings, the_integers]));
ef_eq_s : RETURN (make_uniform_product_space (the_strings, 2));
ef_ne_s : RETURN (make_uniform_product_space (the_strings, 2));
ef_gt_s : RETURN (make_uniform_product_space (the_strings, 2));
ef_lt_s : RETURN (make_uniform_product_space (the_strings, 2));
ef_ge_s : RETURN (make_uniform_product_space (the_strings, 2));
ef_le_s : RETURN (make_uniform_product_space (the_strings, 2));
ef_subsequence_s : RETURN (make_listed_product_space ([the_strings, the_integers,
the_integers]));
ef_concat_s : RETURN (make_extended_tuple_space (the_zero_tuple_space, the_strings));
ef_size_s : RETURN (make_uniform_product_space (the_strings, 1));
ef_format : RETURN (make_listed_product_space ([the_numbers, the_strings]));
ef_value : RETURN (make_uniform_product_space (the_strings, 1));
ef_like : RETURN (make_uniform_product_space (the_strings, 2));
ef_if_s : RETURN (make_listed_product_space ([the_logicals, the_strings,
the_strings]));
ef_subscript_b : RETURN (make_listed_product_space ([the_binarys, the_integers]));
ef_eq_b : RETURN (make_uniform_product_space (the_binarys, 2));
ef_ne_b : RETURN (make_uniform_product_space (the_binarys, 2));
ef_gt_b : RETURN (make_uniform_product_space (the_binarys, 2));
ef_lt_b : RETURN (make_uniform_product_space (the_binarys, 2));
ef_ge_b : RETURN (make_uniform_product_space (the_binarys, 2));
ef_le_b : RETURN (make_uniform_product_space (the_binarys, 2));
ef_subsequence_b : RETURN (make_listed_product_space ([the_binarys, the_integers,
the_integers]));
ef_concat_b : RETURN (make_extended_tuple_space (the_zero_tuple_space, the_binarys));
ef_size_b : RETURN (make_uniform_product_space (the_binarys, 1));
ef_if_b : RETURN (make_listed_product_space ([the_logicals, the_binarys,
the_binarys]));
ef_subscript_t : RETURN (make_listed_product_space ([the_tuples, the_integers]));
ef_eq_t : RETURN (make_uniform_product_space (the_tuples, 2));
ef_ne_t : RETURN (make_uniform_product_space (the_tuples, 2));
ef_concat_t : RETURN (make_extended_tuple_space (the_zero_tuple_space, the_tuples));
ef_size_t : RETURN (make_uniform_product_space (the_tuples, 1));
ef_entuple : RETURN (the_tuples);
ef_detuple : RETURN (make_uniform_product_space (the_generics, 1));
ef_insert : RETURN (make_listed_product_space ([the_tuples, the_generics,
the_integers]));
ef_remove : RETURN (make_listed_product_space ([the_tuples, the_integers]));
ef_if_t : RETURN (make_listed_product_space ([the_logicals, the_tuples,
the_tuples]));
ef_sum_it : RETURN (make_uniform_product_space (the_integer_tuples, 1));
ef_product_it : RETURN (make_uniform_product_space (the_integer_tuples, 1));
ef_add_it : RETURN (make_extended_tuple_space (the_integer_tuples,
the_integer_tuples));
ef_subtract_it : RETURN (make_uniform_product_space (the_integer_tuples, 2));
ef_scalar_mult_it : RETURN (make_listed_product_space ([the_integers,
the_integer_tuples]));
ef_dot_prod_it : RETURN (make_uniform_product_space (the_integer_tuples, 2));
ef_sum_rt : RETURN (make_uniform_product_space (the_real_tuples, 1));
ef_product_rt : RETURN (make_uniform_product_space (the_real_tuples, 1));
ef_add_rt : RETURN (make_extended_tuple_space (the_real_tuples, the_real_tuples));
ef_subtract_rt : RETURN (make_uniform_product_space (the_real_tuples, 2));
ef_scalar_mult_rt : RETURN (make_listed_product_space ([the_reals,
the_real_tuples]));
ef_dot_prod_rt : RETURN (make_uniform_product_space (the_real_tuples, 2));
ef_norm_rt : RETURN (make_uniform_product_space (the_real_tuples, 1));
ef_sum_ct : RETURN (make_uniform_product_space (the_complex_tuples, 1));
ef_product_ct : RETURN (make_uniform_product_space (the_complex_tuples, 1));
ef_add_ct : RETURN (make_extended_tuple_space (the_complex_tuples,
the_complex_tuples));
ef_subtract_ct : RETURN (make_uniform_product_space (the_complex_tuples, 2));
ef_scalar_mult_ct : RETURN (make_listed_product_space ([the_complex_numbers,
the_complex_tuples]));
ef_dot_prod_ct : RETURN (make_uniform_product_space (the_complex_tuples, 2));
ef_norm_ct : RETURN (make_uniform_product_space (the_complex_tuples, 1));
ef_if : RETURN (make_listed_product_space ([the_logicals, the_generics,
the_generics]));
ef_ensemble : RETURN (the_tuples);
ef_member_of : RETURN (make_listed_product_space ([the_generics, the_maths_spaces]));
OTHERWISE : RETURN (?);
END_CASE;
END_FUNCTION;
FUNCTION derive_elementary_function_range
(ef_val : elementary_function_enumerators) : tuple_space;
IF NOT EXISTS (ef_val) THEN RETURN (?); END_IF;
CASE ef_val OF
ef_and : RETURN (make_uniform_product_space (the_logicals, 1));
ef_or : RETURN (make_uniform_product_space (the_logicals, 1));
ef_not : RETURN (make_uniform_product_space (the_logicals, 1));
ef_xor : RETURN (make_uniform_product_space (the_logicals, 2));
ef_negate_i : RETURN (make_uniform_product_space (the_integers, 1));
ef_add_i : RETURN (make_uniform_product_space (the_integers, 1));
ef_subtract_i : RETURN (make_uniform_product_space (the_integers, 1));
ef_multiply_i : RETURN (make_uniform_product_space (the_integers, 1));
ef_divide_i : RETURN (make_uniform_product_space (the_integers, 1));
ef_mod_i : RETURN (make_uniform_product_space (the_integers, 1));
ef_exponentiate_i : RETURN (make_uniform_product_space (the_integers, 1));
ef_eq_i : RETURN (make_uniform_product_space (the_logicals, 1));
ef_ne_i : RETURN (make_uniform_product_space (the_logicals, 1));
ef_gt_i : RETURN (make_uniform_product_space (the_logicals, 1));
ef_lt_i : RETURN (make_uniform_product_space (the_logicals, 1));
ef_ge_i : RETURN (make_uniform_product_space (the_logicals, 1));
ef_le_i : RETURN (make_uniform_product_space (the_logicals, 1));
ef_abs_i : RETURN (make_uniform_product_space (the_integers, 1));
ef_if_i : RETURN (make_uniform_product_space (the_integers, 1));
ef_negate_r : RETURN (make_uniform_product_space (the_reals, 1));
ef_reciprocal_r : RETURN (make_uniform_product_space (the_reals, 1));
ef_add_r : RETURN (make_uniform_product_space (the_reals, 1));
ef_subtract_r : RETURN (make_uniform_product_space (the_reals, 1));
ef_multiply_r : RETURN (make_uniform_product_space (the_reals, 1));
ef_divide_r : RETURN (make_uniform_product_space (the_reals, 1));
ef_mod_r : RETURN (make_uniform_product_space (the_reals, 1));
ef_exponentiate_r : RETURN (make_uniform_product_space (the_reals, 1));
ef_exponentiate_ri : RETURN (make_uniform_product_space (the_reals, 1));
ef_eq_r : RETURN (make_uniform_product_space (the_logicals, 1));
ef_ne_r : RETURN (make_uniform_product_space (the_logicals, 1));
ef_gt_r : RETURN (make_uniform_product_space (the_logicals, 1));
ef_lt_r : RETURN (make_uniform_product_space (the_logicals, 1));
ef_ge_r : RETURN (make_uniform_product_space (the_logicals, 1));
ef_le_r : RETURN (make_uniform_product_space (the_logicals, 1));
ef_abs_r : RETURN (make_uniform_product_space (the_nonnegative_reals, 1));
ef_acos_r : RETURN (make_uniform_product_space (the_zero_pi_interval, 1));
ef_asin_r : RETURN (make_uniform_product_space (the_neghalfpi_halfpi_interval, 1));
ef_atan2_r : RETURN (make_uniform_product_space (the_negpi_pi_interval, 1));
ef_cos_r : RETURN (make_uniform_product_space (the_neg1_one_interval, 1));
ef_exp_r : RETURN (make_uniform_product_space (the_nonnegative_reals, 1));
ef_ln_r : RETURN (make_uniform_product_space (the_reals, 1));
ef_log2_r : RETURN (make_uniform_product_space (the_reals, 1));
ef_log10_r : RETURN (make_uniform_product_space (the_reals, 1));
ef_sin_r : RETURN (make_uniform_product_space (the_neg1_one_interval, 1));
ef_sqrt_r : RETURN (make_uniform_product_space (the_nonnegative_reals, 1));
ef_tan_r : RETURN (make_uniform_product_space (the_reals, 1));
ef_if_r : RETURN (make_uniform_product_space (the_reals, 1));
ef_negate_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_reciprocal_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_add_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_subtract_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_multiply_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_divide_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_exponentiate_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_exponentiate_ci : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_eq_c : RETURN (make_uniform_product_space (the_logicals, 1));
ef_ne_c : RETURN (make_uniform_product_space (the_logicals, 1));
ef_conjugate_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_abs_c : RETURN (make_uniform_product_space (the_nonnegative_reals, 1));
ef_arg_c : RETURN (make_uniform_product_space (the_negpi_pi_interval, 1));
ef_cos_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_exp_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_ln_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_sin_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_sqrt_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_tan_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_if_c : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_subscript_s : RETURN (make_uniform_product_space (the_strings, 1));
ef_eq_s : RETURN (make_uniform_product_space (the_logicals, 1));
ef_ne_s : RETURN (make_uniform_product_space (the_logicals, 1));
ef_gt_s : RETURN (make_uniform_product_space (the_logicals, 1));
ef_lt_s : RETURN (make_uniform_product_space (the_logicals, 1));
ef_ge_s : RETURN (make_uniform_product_space (the_logicals, 1));
ef_le_s : RETURN (make_uniform_product_space (the_logicals, 1));
ef_subsequence_s : RETURN (make_uniform_product_space (the_strings, 1));
ef_concat_s : RETURN (make_uniform_product_space (the_strings, 1));
ef_size_s : RETURN (make_uniform_product_space (the_integers, 1));
ef_format : RETURN (make_uniform_product_space (the_strings, 1));
ef_value : RETURN (make_uniform_product_space (the_reals, 1));
ef_like : RETURN (make_uniform_product_space (the_booleans, 1));
ef_if_s : RETURN (make_uniform_product_space (the_strings, 1));
ef_subscript_b : RETURN (make_uniform_product_space (the_binarys, 1));
ef_eq_b : RETURN (make_uniform_product_space (the_logicals, 1));
ef_ne_b : RETURN (make_uniform_product_space (the_logicals, 1));
ef_gt_b : RETURN (make_uniform_product_space (the_logicals, 1));
ef_lt_b : RETURN (make_uniform_product_space (the_logicals, 1));
ef_ge_b : RETURN (make_uniform_product_space (the_logicals, 1));
ef_le_b : RETURN (make_uniform_product_space (the_logicals, 1));
ef_subsequence_b : RETURN (make_uniform_product_space (the_binarys, 1));
ef_concat_b : RETURN (make_uniform_product_space (the_binarys, 1));
ef_size_b : RETURN (make_uniform_product_space (the_integers, 1));
ef_if_b : RETURN (make_uniform_product_space (the_binarys, 1));
ef_subscript_t : RETURN (make_uniform_product_space (the_generics, 1));
ef_eq_t : RETURN (make_uniform_product_space (the_logicals, 1));
ef_ne_t : RETURN (make_uniform_product_space (the_logicals, 1));
ef_concat_t : RETURN (make_uniform_product_space (the_tuples, 1));
ef_size_t : RETURN (make_uniform_product_space (the_integers, 1));
ef_entuple : RETURN (make_uniform_product_space (the_tuples, 1));
ef_detuple : RETURN (the_tuples);
ef_insert : RETURN (make_uniform_product_space (the_tuples, 1));
ef_remove : RETURN (make_uniform_product_space (the_tuples, 1));
ef_if_t : RETURN (make_uniform_product_space (the_tuples, 1));
ef_sum_it : RETURN (make_uniform_product_space (the_integers, 1));
ef_product_it : RETURN (make_uniform_product_space (the_integers, 1));
ef_add_it : RETURN (make_uniform_product_space (the_integer_tuples, 1));
ef_subtract_it : RETURN (make_uniform_product_space (the_integer_tuples, 1));
ef_scalar_mult_it : RETURN (make_uniform_product_space (the_integer_tuples, 1));
ef_dot_prod_it : RETURN (make_uniform_product_space (the_integers, 1));
ef_sum_rt : RETURN (make_uniform_product_space (the_reals, 1));
ef_product_rt : RETURN (make_uniform_product_space (the_reals, 1));
ef_add_rt : RETURN (make_uniform_product_space (the_real_tuples, 1));
ef_subtract_rt : RETURN (make_uniform_product_space (the_real_tuples, 1));
ef_scalar_mult_rt : RETURN (make_uniform_product_space (the_real_tuples, 1));
ef_dot_prod_rt : RETURN (make_uniform_product_space (the_reals, 1));
ef_norm_rt : RETURN (make_uniform_product_space (the_reals, 1));
ef_sum_ct : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_product_ct : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_add_ct : RETURN (make_uniform_product_space (the_complex_tuples, 1));
ef_subtract_ct : RETURN (make_uniform_product_space (the_complex_tuples, 1));
ef_scalar_mult_ct : RETURN (make_uniform_product_space (the_complex_tuples, 1));
ef_dot_prod_ct : RETURN (make_uniform_product_space (the_complex_numbers, 1));
ef_norm_ct : RETURN (make_uniform_product_space (the_nonnegative_reals, 1));
ef_if : RETURN (make_uniform_product_space (the_generics, 1));
ef_ensemble : RETURN (make_uniform_product_space (the_maths_spaces, 1));
ef_member_of : RETURN (make_uniform_product_space (the_logicals, 1));
OTHERWISE : RETURN (?);
END_CASE;
END_FUNCTION;
FUNCTION derive_finite_function_domain
(pairs : SET[1:?] OF LIST[2:2] OF maths_value) : tuple_space;
LOCAL
result : SET OF maths_value := [];
END_LOCAL;
-- An ambiguity in ISO 10303-11:1994 pages 99-101 leaves the result of the following
-- three lines ambiguous in those cases where an operand is simultaneously a member
-- of the base type and the aggregate type.
-- REPEAT i := 1 TO SIZEOF (pairs);
-- result := result + pairs[i][1];
-- END_REPEAT;
-- The next line unions an empty set and the desired list to get the desired set.
result := result + list_selected_components (pairs, 1);
RETURN (one_tuples_of (make_finite_space (result)));
END_FUNCTION;
FUNCTION derive_finite_function_range
(pairs : SET[1:?] OF LIST[2:2] OF maths_value) : tuple_space;
LOCAL
result : SET OF maths_value := [];
END_LOCAL;
-- An ambiguity in ISO 10303-11:1994 pages 99-101 leaves the result of the following
-- three lines ambiguous in those cases where an operand is simultaneously a member
-- of the base type and the aggregate type.
-- REPEAT i := 1 TO SIZEOF (pairs);
-- result := result + pairs[i][2];
-- END_REPEAT;
-- The next line unions an empty set and the desired list to get the desired set.
result := result + list_selected_components (pairs, 2);
RETURN (one_tuples_of (make_finite_space (result)));
END_FUNCTION;
FUNCTION derive_function_domain
(func : maths_function) : tuple_space;
LOCAL
typenames : SET OF STRING := stripped_typeof(func);
tspace : tuple_space := make_listed_product_space ([]);
shape : LIST OF positive_integer;
sidxs : LIST OF INTEGER := [0];
itvl : finite_integer_interval;
factors : LIST OF finite_integer_interval := [];
is_uniform : BOOLEAN := TRUE;
END_LOCAL;
IF 'FINITE_FUNCTION' IN typenames THEN
RETURN (derive_finite_function_domain (func\finite_function.pairs));
END_IF;
IF 'CONSTANT_FUNCTION' IN typenames THEN
RETURN (domain_from (func\constant_function.source_of_domain));
END_IF;
IF 'SELECTOR_FUNCTION' IN typenames THEN
RETURN (domain_from (func\selector_function.source_of_domain));
END_IF;
IF 'ELEMENTARY_FUNCTION' IN typenames THEN
RETURN (derive_elementary_function_domain (func\elementary_function.func_id));
END_IF;
IF 'RESTRICTION_FUNCTION' IN typenames THEN
RETURN (one_tuples_of (func\restriction_function.operand));
END_IF;
IF 'REPACKAGING_FUNCTION' IN typenames THEN
IF func\repackaging_function.input_repack = ro_nochange THEN
RETURN (func\repackaging_function.operand.domain);
END_IF;
IF func\repackaging_function.input_repack = ro_wrap_as_tuple THEN
RETURN (factor1 (func\repackaging_function.operand.domain));
END_IF;
IF func\repackaging_function.input_repack = ro_unwrap_tuple THEN
RETURN (one_tuples_of (func\repackaging_function.operand.domain));
END_IF;
-- Unreachable, as there is no other possible value for input_repack.
RETURN (?);
END_IF;
IF 'REINDEXED_ARRAY_FUNCTION' IN typenames THEN
shape := shape_of_array(func\unary_generic_expression.operand);
sidxs := func\reindexed_array_function.starting_indices;
REPEAT i := 1 TO SIZEOF (shape);
itvl := make_finite_integer_interval (sidxs[i], sidxs[i]+shape[i]-1);
INSERT (factors, itvl, i-1);
IF shape[i] <> shape[1] THEN is_uniform := FALSE; END_IF;
END_REPEAT;
IF is_uniform THEN
RETURN (make_uniform_product_space (factors[1], SIZEOF (shape)));
END_IF;
RETURN (make_listed_product_space (factors));
END_IF;
IF 'SERIES_COMPOSED_FUNCTION' IN typenames THEN
RETURN (func\series_composed_function.operands[1].domain);
END_IF;
IF 'PARALLEL_COMPOSED_FUNCTION' IN typenames THEN
RETURN (domain_from (func\parallel_composed_function.source_of_domain));
END_IF;
IF 'EXPLICIT_TABLE_FUNCTION' IN typenames THEN
shape := func\explicit_table_function.shape;
sidxs[1] := func\explicit_table_function.index_base;
REPEAT i := 1 TO SIZEOF (shape);
itvl := make_finite_integer_interval (sidxs[1], sidxs[1]+shape[i]-1);
INSERT (factors, itvl, i-1);
IF shape[i] <> shape[1] THEN is_uniform := FALSE; END_IF;
END_REPEAT;
IF is_uniform THEN
RETURN (make_uniform_product_space (factors[1], SIZEOF (shape)));
END_IF;
RETURN (make_listed_product_space (factors));
END_IF;
IF 'HOMOGENEOUS_LINEAR_FUNCTION' IN typenames THEN
RETURN (one_tuples_of (make_uniform_product_space
(factor1 (func\homogeneous_linear_function.mat.range),
func\homogeneous_linear_function.mat\explicit_table_function.shape
[func\homogeneous_linear_function.sum_index])));
END_IF;
IF 'GENERAL_LINEAR_FUNCTION' IN typenames THEN
RETURN (one_tuples_of (make_uniform_product_space
(factor1 (func\general_linear_function.mat.range),
func\general_linear_function.mat\explicit_table_function.shape
[func\general_linear_function.sum_index] - 1)));
END_IF;
IF 'B_SPLINE_BASIS' IN typenames THEN
RETURN (one_tuples_of (make_finite_real_interval
(func\b_spline_basis.repeated_knots[func\b_spline_basis.order], closed,
func\b_spline_basis.repeated_knots[func\b_spline_basis.num_basis+1], closed)));
END_IF;
IF 'B_SPLINE_FUNCTION' IN typenames THEN
REPEAT i := 1 TO SIZEOF (func\b_spline_function.basis);
tspace := assoc_product_space (tspace, func\b_spline_function.basis[i].domain);
END_REPEAT;
RETURN (one_tuples_of (tspace));
END_IF;
IF 'RATIONALIZE_FUNCTION' IN typenames THEN
RETURN (func\rationalize_function.fun.domain);
END_IF;
IF 'PARTIAL_DERIVATIVE_FUNCTION' IN typenames THEN
RETURN (func\partial_derivative_function.derivand.domain);
END_IF;
IF 'DEFINITE_INTEGRAL_FUNCTION' IN typenames THEN
RETURN (derive_definite_integral_domain(func));
END_IF;
IF 'ABSTRACTED_EXPRESSION_FUNCTION' IN typenames THEN
REPEAT i := 1 TO SIZEOF (func\abstracted_expression_function.variables);
tspace := assoc_product_space (tspace, one_tuples_of (values_space_of
(func\abstracted_expression_function.variables[i])));
END_REPEAT;
RETURN (tspace);
END_IF;
IF 'EXPRESSION_DENOTED_FUNCTION' IN typenames THEN
RETURN (values_space_of (func\expression_denoted_function.expr)\function_space.
domain_argument);
END_IF;
IF 'IMPORTED_POINT_FUNCTION' IN typenames THEN
RETURN (one_tuples_of (make_listed_product_space ([])));
END_IF;
IF 'IMPORTED_CURVE_FUNCTION' IN typenames THEN
RETURN (func\imported_curve_function.parametric_domain);
END_IF;
IF 'IMPORTED_SURFACE_FUNCTION' IN typenames THEN
RETURN (func\imported_surface_function.parametric_domain);
END_IF;
IF 'IMPORTED_VOLUME_FUNCTION' IN typenames THEN
RETURN (func\imported_volume_function.parametric_domain);
END_IF;
IF 'APPLICATION_DEFINED_FUNCTION' IN typenames THEN
RETURN (func\application_defined_function.explicit_domain);
END_IF;
-- Unreachable, as no other subtypes of maths_function are permissible without
-- first modifying this function to account for them.
RETURN (?);
END_FUNCTION;
FUNCTION derive_function_range
(func : maths_function) : tuple_space;
LOCAL
typenames : SET OF STRING := stripped_typeof(func);
tspace : tuple_space := make_listed_product_space ([]);
m, n : nonnegative_integer := 0;
temp : INTEGER := 0;
END_LOCAL;
IF 'FINITE_FUNCTION' IN typenames THEN
RETURN (derive_finite_function_range (func\finite_function.pairs));
END_IF;
IF 'CONSTANT_FUNCTION' IN typenames THEN
RETURN (one_tuples_of (make_finite_space ([func\constant_function.sole_output])));
END_IF;
IF 'SELECTOR_FUNCTION' IN typenames THEN
tspace := func.domain;
IF (space_dimension(tspace) = 1) AND ((schema_prefix + 'TUPLE_SPACE') IN
TYPEOF (tspace)) THEN
tspace := factor1 (tspace);
END_IF;
RETURN (one_tuples_of (factor_space (tspace, func\selector_function.selector)));
END_IF;
IF 'ELEMENTARY_FUNCTION' IN typenames THEN
RETURN (derive_elementary_function_range (func\elementary_function.func_id));
END_IF;
IF 'RESTRICTION_FUNCTION' IN typenames THEN
RETURN (one_tuples_of (func\restriction_function.operand));
END_IF;
IF 'REPACKAGING_FUNCTION' IN typenames THEN
tspace := func\repackaging_function.operand.range;
IF func\repackaging_function.output_repack = ro_wrap_as_tuple THEN
tspace := one_tuples_of (tspace);
END_IF;
IF func\repackaging_function.output_repack = ro_unwrap_tuple THEN
tspace := factor1 (tspace);
END_IF;
IF func\repackaging_function.selected_output > 0 THEN
tspace := one_tuples_of (factor_space (tspace,
func\repackaging_function.selected_output));
END_IF;
RETURN (tspace);
END_IF;
IF 'REINDEXED_ARRAY_FUNCTION' IN typenames THEN
RETURN (func\unary_generic_expression.operand\maths_function.range);
END_IF;
IF 'SERIES_COMPOSED_FUNCTION' IN typenames THEN
RETURN (func\series_composed_function.operands[SIZEOF
(func\series_composed_function.operands)].range);
END_IF;
IF 'PARALLEL_COMPOSED_FUNCTION' IN typenames THEN
RETURN (func\parallel_composed_function.final_function.range);
END_IF;
IF 'EXPLICIT_TABLE_FUNCTION' IN typenames THEN
IF 'LISTED_REAL_DATA' IN typenames THEN
RETURN (one_tuples_of (the_reals));
END_IF;
IF 'LISTED_INTEGER_DATA' IN typenames THEN
RETURN (one_tuples_of (the_integers));
END_IF;
IF 'LISTED_LOGICAL_DATA' IN typenames THEN
RETURN (one_tuples_of (the_logicals));
END_IF;
IF 'LISTED_STRING_DATA' IN typenames THEN
RETURN (one_tuples_of (the_strings));
END_IF;
IF 'LISTED_COMPLEX_NUMBER_DATA' IN typenames THEN
RETURN (one_tuples_of (the_complex_numbers));
END_IF;
IF 'LISTED_DATA' IN typenames THEN
RETURN (one_tuples_of (func\listed_data.value_range));
END_IF;
IF 'EXTERNALLY_LISTED_DATA' IN typenames THEN
RETURN (one_tuples_of (func\externally_listed_data.value_range));
END_IF;
IF 'LINEARIZED_TABLE_FUNCTION' IN typenames THEN
RETURN (func\linearized_table_function.source.range);
END_IF;
IF 'BASIC_SPARSE_MATRIX' IN typenames THEN
RETURN (func\basic_sparse_matrix.val.range);
END_IF;
-- Unreachable, as no other subtypes of explicit_table_function are permissible
-- without first modifying this function to account for them.
RETURN (?);
END_IF;
IF 'HOMOGENEOUS_LINEAR_FUNCTION' IN typenames THEN
RETURN (one_tuples_of (make_uniform_product_space
(factor1 (func\homogeneous_linear_function.mat.range),
func\homogeneous_linear_function.mat\explicit_table_function.shape
[3 - func\homogeneous_linear_function.sum_index])));
END_IF;
IF 'GENERAL_LINEAR_FUNCTION' IN typenames THEN
RETURN (one_tuples_of (make_uniform_product_space
(factor1 (func\general_linear_function.mat.range),
func\general_linear_function.mat\explicit_table_function.shape
[3 - func\general_linear_function.sum_index])));
END_IF;
IF 'B_SPLINE_BASIS' IN typenames THEN
RETURN (one_tuples_of (make_uniform_product_space (the_reals,
func\b_spline_basis.num_basis)));
END_IF;
IF 'B_SPLINE_FUNCTION' IN typenames THEN
tspace := factor1 (func\b_spline_function.coef.domain);
m := SIZEOF (func\b_spline_function.basis);
n := space_dimension (tspace);
IF m = n THEN
RETURN (one_tuples_of (the_reals));
END_IF;
IF m = n - 1 THEN
RETURN (one_tuples_of (make_uniform_product_space (the_reals,
factor_space (tspace, n)\finite_integer_interval.size)));
END_IF;
tspace := extract_factors (tspace, m+1, n);
RETURN (one_tuples_of (make_function_space (sc_equal, tspace, sc_subspace,
number_superspace_of (func\b_spline_function.coef.range))));
END_IF;
IF 'RATIONALIZE_FUNCTION' IN typenames THEN
tspace := factor1 (func\rationalize_function.fun.range);
n := space_dimension (tspace);
RETURN (one_tuples_of (make_uniform_product_space (number_superspace_of (
factor1 (tspace)), n-1)));
END_IF;
IF 'PARTIAL_DERIVATIVE_FUNCTION' IN typenames THEN
RETURN (drop_numeric_constraints (
func\partial_derivative_function.derivand.range));
END_IF;
IF 'DEFINITE_INTEGRAL_FUNCTION' IN typenames THEN
RETURN (drop_numeric_constraints (
func\definite_integral_function.integrand.range));
END_IF;
IF 'ABSTRACTED_EXPRESSION_FUNCTION' IN typenames THEN
RETURN (one_tuples_of(values_space_of(func\abstracted_expression_function.expr)));
END_IF;
IF 'EXPRESSION_DENOTED_FUNCTION' IN typenames THEN
RETURN (values_space_of (func\expression_denoted_function.expr)\function_space.
range_argument);
END_IF;
IF 'IMPORTED_POINT_FUNCTION' IN typenames THEN
temp := dimension_of (func\imported_point_function.geometry);
RETURN (one_tuples_of (make_uniform_product_space (the_reals, temp)));
END_IF;
IF 'IMPORTED_CURVE_FUNCTION' IN typenames THEN
temp := dimension_of (func\imported_curve_function.geometry);
RETURN (one_tuples_of (make_uniform_product_space (the_reals, temp)));
END_IF;
IF 'IMPORTED_SURFACE_FUNCTION' IN typenames THEN
temp := dimension_of (func\imported_surface_function.geometry);
RETURN (one_tuples_of (make_uniform_product_space (the_reals, temp)));
END_IF;
IF 'IMPORTED_VOLUME_FUNCTION' IN typenames THEN
temp := dimension_of (func\imported_volume_function.geometry);
RETURN (one_tuples_of (make_uniform_product_space (the_reals, temp)));
END_IF;
IF 'APPLICATION_DEFINED_FUNCTION' IN typenames THEN
RETURN (func\application_defined_function.explicit_range);
END_IF;
-- Unreachable, as no other subtypes of maths_function are permissible without
-- first modifying this function to account for them.
RETURN (?);
END_FUNCTION;
FUNCTION domain_from
(ref : maths_space_or_function) : tuple_space;
LOCAL
typenames : SET OF STRING := stripped_typeof(ref);
func : maths_function;
END_LOCAL;
IF NOT EXISTS (ref) THEN RETURN (?); END_IF;
IF 'TUPLE_SPACE' IN typenames THEN RETURN (ref); END_IF;
IF 'MATHS_SPACE' IN typenames THEN RETURN (one_tuples_of (ref)); END_IF;
func := ref;
IF 'CONSTANT_FUNCTION' IN typenames THEN
RETURN (domain_from (func\constant_function.source_of_domain));
END_IF;
IF 'SELECTOR_FUNCTION' IN typenames THEN
RETURN (domain_from (func\selector_function.source_of_domain));
END_IF;
IF 'PARALLEL_COMPOSED_FUNCTION' IN typenames THEN
RETURN (domain_from (func\parallel_composed_function.source_of_domain));
END_IF;
RETURN (func.domain);
END_FUNCTION;
FUNCTION dot_count
(str : STRING) : INTEGER;
LOCAL
n : INTEGER := 0;
END_LOCAL;
REPEAT i := 1 TO LENGTH (str);
IF str[i] = '.' THEN n := n + 1; END_IF;
END_REPEAT;
RETURN (n);
END_FUNCTION;
FUNCTION dotted_identifiers_syntax
(str : STRING) : BOOLEAN;
LOCAL
k : positive_integer;
m : positive_integer;
END_LOCAL;
IF NOT EXISTS (str) THEN RETURN (FALSE); END_IF;
k := parse_express_identifier (str, 1);
IF k = 1 THEN RETURN (FALSE); END_IF;
REPEAT WHILE k <= LENGTH (str);
IF (str[k] <> '.') OR (k = LENGTH (str)) THEN RETURN (FALSE); END_IF;
m := parse_express_identifier (str, k+1);
IF m = k + 1 THEN RETURN (FALSE); END_IF;
k := m;
END_REPEAT;
RETURN (TRUE);
END_FUNCTION;
FUNCTION drop_numeric_constraints
(spc : maths_space) : maths_space;
LOCAL
typenames : SET OF STRING := stripped_typeof(spc);
tspc : listed_product_space;
factors : LIST OF maths_space := [];
xspc : extended_tuple_space;
END_LOCAL;
IF 'UNIFORM_PRODUCT_SPACE' IN typenames THEN
RETURN (make_uniform_product_space (drop_numeric_constraints (
spc\uniform_product_space.base), spc\uniform_product_space.exponent));
END_IF;
IF 'LISTED_PRODUCT_SPACE' IN typenames THEN
tspc := spc;
REPEAT i := 1 TO SIZEOF (tspc.factors);
INSERT (factors, drop_numeric_constraints (tspc.factors[i]), i-1);
END_REPEAT;
RETURN (make_listed_product_space (factors));
END_IF;
IF 'EXTENDED_TUPLE_SPACE' IN typenames THEN
xspc := spc;
RETURN (make_extended_tuple_space (drop_numeric_constraints (xspc.base),
drop_numeric_constraints (xspc.extender)));
END_IF;
IF subspace_of_es (spc, es_numbers) THEN
RETURN (number_superspace_of (spc));
END_IF;
RETURN (spc);
END_FUNCTION;
FUNCTION enclose_cregion_in_pregion
(crgn : cartesian_complex_number_region; centre : complex_number_literal) : polar_complex_number_region;
FUNCTION angle(a : REAL) : REAL;
REPEAT WHILE a > PI; a := a - 2.0*PI; END_REPEAT;
REPEAT WHILE a <= -PI; a := a + 2.0*PI; END_REPEAT;
RETURN (a);
END_FUNCTION;
-- Determine whether a real is strictly within a real interval
FUNCTION strictly_in(z : REAL;
zitv : real_interval) : LOGICAL;
RETURN ((NOT min_exists(zitv) OR (z > real_min(zitv))) AND
(NOT max_exists(zitv) OR (z < real_max(zitv))));
END_FUNCTION;
-- Include direction in minmax collection
PROCEDURE angle_minmax( ab, a : REAL;
a_in : BOOLEAN;
VAR amin, amax : REAL;
VAR amin_in, amax_in : BOOLEAN);
a := angle(a - ab);
IF amin = a THEN amin_in := amin_in OR a_in; END_IF;
IF amin > a THEN amin := a; amin_in := a_in; END_IF;
IF amax = a THEN amax_in := amax_in OR a_in; END_IF;
IF amax < a THEN amax := a; amax_in := a_in; END_IF;
END_PROCEDURE;
-- Include distance in max collection
PROCEDURE range_max( r : REAL;
incl : BOOLEAN;
VAR rmax : REAL;
VAR rmax_in : BOOLEAN);
IF rmax = r THEN rmax_in := rmax_in OR incl; END_IF;
IF rmax < r THEN rmax := r; rmax_in := incl; END_IF;
END_PROCEDURE;
-- Include distance in min collection
PROCEDURE range_min( r : REAL;
incl : BOOLEAN;
VAR rmin : REAL;
VAR rmin_in : BOOLEAN);
IF rmin = r THEN rmin_in := rmin_in OR incl; END_IF;
IF (rmin < 0.0) OR (rmin > r) THEN rmin := r; rmin_in := incl; END_IF;
END_PROCEDURE;
LOCAL
xitv, yitv : real_interval;
is_xmin, is_xmax, is_ymin, is_ymax : BOOLEAN;
xmin, xmax, ymin, ymax, xc, yc : REAL := 0.0;
xmin_in, xmax_in, ymin_in, ymax_in : BOOLEAN := FALSE;
rmin, rmax : REAL := -1.0;
amin : REAL := 4.0;
amax : REAL := -4.0;
rmax_exists, outside : BOOLEAN := TRUE;
rmin_in, rmax_in, amin_in, amax_in : BOOLEAN := FALSE;
ab, a, r : REAL := 0.0;
incl : BOOLEAN;
ritv : real_interval;
aitv : finite_real_interval;
minclo, maxclo : open_closed := open;
END_LOCAL;
IF NOT EXISTS (crgn) OR NOT EXISTS (centre) THEN RETURN (?); END_IF;
-- Extract elementary input information
xitv := crgn.real_constraint;
yitv := crgn.imag_constraint;
xc := centre.real_part;
yc := centre.imag_part;
is_xmin := min_exists(xitv);
is_xmax := max_exists(xitv);
is_ymin := min_exists(yitv);
is_ymax := max_exists(yitv);
IF is_xmin THEN xmin := real_min(xitv); xmin_in := min_included(xitv); END_IF;
IF is_xmax THEN xmax := real_max(xitv); xmax_in := max_included(xitv); END_IF;
IF is_ymin THEN ymin := real_min(yitv); ymin_in := min_included(yitv); END_IF;
IF is_ymax THEN ymax := real_max(yitv); ymax_in := max_included(yitv); END_IF;
rmax_exists := is_xmin AND is_xmax AND is_ymin AND is_ymax;
-- Identify base direction with respect to which all relevant directions lie
-- within +/- 0.5*PI, or that the centre lies properly inside crgn.
IF is_xmin AND (xc <= xmin) THEN ab := 0.0;
ELSE IF is_ymin AND (yc <= ymin) THEN ab := 0.5*PI;
ELSE IF is_ymax AND (yc >= ymax) THEN ab := -0.5*PI;
ELSE IF is_xmax AND (xc >= xmax) THEN ab := PI;
ELSE outside := FALSE;
END_IF; END_IF; END_IF; END_IF;
IF NOT outside AND NOT rmax_exists THEN
RETURN (?); -- No enclosing polar region exists (requires whole plane)
END_IF;
-- Identify any closest point on a side but not a corner.
IF is_xmin AND (xc <= xmin) AND strictly_in(yc,yitv) THEN
rmin := xmin - xc; rmin_in := xmin_in;
ELSE IF is_ymin AND (yc <= ymin) AND strictly_in(xc,xitv) THEN
rmin := ymin - yc; rmin_in := ymin_in;
ELSE IF is_ymax AND (yc >= ymax) AND strictly_in(xc,xitv) THEN
rmin := yc - ymax; rmin_in := ymax_in;
ELSE IF is_xmax AND (xc >= xmax) AND strictly_in(yc,yitv) THEN
rmin := xc - xmax; rmin_in := xmax_in;
END_IF; END_IF; END_IF; END_IF;
IF is_xmin THEN
IF is_ymin THEN -- Consider lower left corner
r := SQRT((xmin-xc)**2 + (ymin-yc)**2);
incl := xmin_in AND ymin_in;
IF rmax_exists THEN range_max(r,incl,rmax,rmax_in); END_IF;
IF outside THEN
IF r > 0.0 THEN
range_min(r,incl,rmin,rmin_in);
a := angle(atan2(ymin-yc,xmin-xc) - ab);
IF xc = xmin THEN incl := xmin_in; END_IF;
IF yc = ymin THEN incl := ymin_in; END_IF;
angle_minmax(ab,a,incl,amin,amax,amin_in,amax_in);
ELSE -- Centre at lower left corner
rmin := 0.0; rmin_in := xmin_in AND ymin_in;
amin := angle(0.0-ab); amin_in := ymin_in;
amax := angle(0.5*PI-ab); amax_in := xmin_in;
END_IF;
END_IF;
ELSE IF xc <= xmin THEN -- Consider points near (xmin, -infinity)
angle_minmax(ab,-0.5*PI,(xc=xmin) AND xmin_in,amin,amax,amin_in,amax_in);
END_IF; END_IF;
IF NOT is_ymax AND (xc <= xmin) THEN -- Consider points near (xmin, +infinity)
angle_minmax(ab,0.5*PI,(xc=xmin) AND xmin_in,amin,amax,amin_in,amax_in);
END_IF;
END_IF;
IF is_ymin THEN
IF is_xmax THEN -- Consider lower right corner
r := SQRT((xmax-xc)**2 + (ymin-yc)**2);
incl := xmax_in AND ymin_in;
IF rmax_exists THEN range_max(r,incl,rmax,rmax_in); END_IF;
IF outside THEN
IF r > 0.0 THEN
range_min(r,incl,rmin,rmin_in);
a := angle(atan2(ymin-yc,xmax-xc) - ab);
IF xc = xmax THEN incl := xmax_in; END_IF;
IF yc = ymin THEN incl := ymin_in; END_IF;
angle_minmax(ab,a,incl,amin,amax,amin_in,amax_in);
ELSE -- Centre at lower right corner
rmin := 0.0; rmin_in := xmax_in AND ymin_in;
amin := angle(0.5*PI-ab); amin_in := ymin_in;
amax := angle(PI-ab); amax_in := xmax_in;
END_IF;
END_IF;
ELSE IF yc <= ymin THEN -- Consider points near (+infinity, ymin)
angle_minmax(ab,0.0,(yc=ymin) AND ymin_in,amin,amax,amin_in,amax_in);
END_IF; END_IF;
IF NOT is_xmin AND (yc <= ymin) THEN -- Consider points near (-infinity, ymin)
angle_minmax(ab,PI,(yc=ymin) AND ymin_in,amin,amax,amin_in,amax_in);
END_IF;
END_IF;
IF is_xmax THEN
IF is_ymax THEN -- Consider upper right corner
r := SQRT((xmax-xc)**2 + (ymax-yc)**2);
incl := xmax_in AND ymax_in;
IF rmax_exists THEN range_max(r,incl,rmax,rmax_in); END_IF;
IF outside THEN
IF r > 0.0 THEN
range_min(r,incl,rmin,rmin_in);
a := angle(atan2(ymax-yc,xmax-xc) - ab);
IF xc = xmax THEN incl := xmax_in; END_IF;
IF yc = ymax THEN incl := ymax_in; END_IF;
angle_minmax(ab,a,incl,amin,amax,amin_in,amax_in);
ELSE -- Centre at lower left corner
rmin := 0.0; rmin_in := xmax_in AND ymax_in;
amin := angle(-PI-ab); amin_in := ymax_in;
amax := angle(-0.5*PI-ab); amax_in := xmax_in;
END_IF;
END_IF;
ELSE IF xc >= xmax THEN -- Consider points near (xmax, +infinity)
angle_minmax(ab,0.5*PI,(xc=xmax) AND xmax_in,amin,amax,amin_in,amax_in);
END_IF; END_IF;
IF NOT is_ymin AND (xc >= xmax) THEN -- Consider points near (xmax, -infinity)
angle_minmax(ab,-0.5*PI,(xc=xmax) AND xmax_in,amin,amax,amin_in,amax_in);
END_IF;
END_IF;
IF is_ymax THEN
IF is_xmin THEN -- Consider upper left corner
r := SQRT((xmin-xc)**2 + (ymax-yc)**2);
incl := xmin_in AND ymax_in;
IF rmax_exists THEN range_max(r,incl,rmax,rmax_in); END_IF;
IF outside THEN
IF r > 0.0 THEN
range_min(r,incl,rmin,rmin_in);
a := angle(atan2(ymax-yc,xmin-xc) - ab);
IF xc = xmin THEN incl := xmin_in; END_IF;
IF yc = ymax THEN incl := ymax_in; END_IF;
angle_minmax(ab,a,incl,amin,amax,amin_in,amax_in);
ELSE -- Centre at lower right corner
rmin := 0.0; rmin_in := xmin_in AND ymax_in;
amin := angle(0.5*PI-ab); amin_in := ymax_in;
amax := angle(PI-ab); amax_in := xmin_in;
END_IF;
END_IF;
ELSE IF yc >= ymax THEN -- Consider points near (-infinity, ymax)
angle_minmax(ab,PI,(yc=ymax) AND ymax_in,amin,amax,amin_in,amax_in);
END_IF; END_IF;
IF NOT is_xmax AND (yc >= ymax) THEN -- Consider points near (+infinity, ymax)
angle_minmax(ab,0.0,(yc=ymax) AND ymax_in,amin,amax,amin_in,amax_in);
END_IF;
END_IF;
IF outside THEN -- Change direction origin from ab back to zero
amin := angle(amin+ab);
IF amin = PI THEN amin := -PI; END_IF;
amax := angle(amax+ab);
IF amax <= amin THEN amax := amax + 2.0*PI; END_IF;
ELSE
amin := -PI; amin_in := FALSE;
amax := PI; amax_in := FALSE;
END_IF;
IF amin_in THEN minclo := closed; END_IF;
IF amax_in THEN maxclo := closed; END_IF;
aitv := make_finite_real_interval(amin,minclo,amax,maxclo);
minclo := open;
IF rmin_in THEN minclo := closed; END_IF;
IF rmax_exists THEN
maxclo := open;
IF rmax_in THEN maxclo := closed; END_IF;
ritv := make_finite_real_interval(rmin,minclo,rmax,maxclo);
ELSE
ritv := make_real_interval_from_min(rmin,minclo);
END_IF;
RETURN (make_polar_complex_number_region(centre,ritv,aitv));
END_FUNCTION;
FUNCTION enclose_pregion_in_cregion
(prgn : polar_complex_number_region) : cartesian_complex_number_region;
PROCEDURE nearest_good_direction(acart : REAL;
aitv : finite_real_interval;
VAR a : REAL;
VAR a_in : BOOLEAN);
a := acart; a_in := TRUE;
IF a < aitv.min THEN
-- a+2.0*PI > aitv.min automatically!
IF a+2.0*PI < aitv.max THEN RETURN; END_IF;
IF a+2.0*PI = aitv.max THEN a_in := max_included(aitv); RETURN; END_IF;
ELSE IF a = aitv.min THEN a_in := min_included(aitv); RETURN;
ELSE IF a < aitv.max THEN RETURN;
ELSE IF a = aitv.max THEN a_in := max_included(aitv); RETURN;
END_IF; END_IF; END_IF; END_IF;
IF COS(acart - aitv.max) >= COS(acart - aitv.min) THEN
a := aitv.max; a_in := max_included(aitv);
ELSE
a := aitv.min; a_in := min_included(aitv);
END_IF;
END_PROCEDURE;
LOCAL
xc, yc, xmin, xmax, ymin, ymax : REAL := 0.0;
ritv, xitv, yitv : real_interval;
aitv : finite_real_interval;
xmin_exists, xmax_exists, ymin_exists, ymax_exists : BOOLEAN;
xmin_in, xmax_in, ymin_in, ymax_in : BOOLEAN := FALSE;
a, r : REAL := 0.0;
a_in : BOOLEAN := FALSE;
min_clo, max_clo : open_closed := open;
END_LOCAL;
IF NOT EXISTS (prgn) THEN RETURN (?); END_IF;
-- Extract elementary input data
xc := prgn.centre.real_part;
yc := prgn.centre.imag_part;
ritv := prgn.distance_constraint;
aitv := prgn.direction_constraint;
-- Determine xmin data
nearest_good_direction(PI,aitv,a,a_in);
IF COS(a) >= 0.0 THEN
xmin_exists := TRUE;
xmin := xc + real_min(ritv)*COS(a);
xmin_in := a_in AND (min_included(ritv) OR (COS(a) = 0.0));
ELSE
IF max_exists(ritv) THEN
xmin_exists := TRUE;
xmin := xc + real_max(ritv)*COS(a);
xmin_in := a_in AND max_included(ritv);
ELSE
xmin_exists := FALSE;
END_IF;
END_IF;
-- Determine xmax data
nearest_good_direction(0.0,aitv,a,a_in);
IF COS(a) <= 0.0 THEN
xmax_exists := TRUE;
xmax := xc + real_min(ritv)*COS(a);
xmax_in := a_in AND (min_included(ritv) OR (COS(a) = 0.0));
ELSE
IF max_exists(ritv) THEN
xmax_exists := TRUE;
xmax := xc + real_max(ritv)*COS(a);
xmax_in := a_in AND max_included(ritv);
ELSE
xmax_exists := FALSE;
END_IF;
END_IF;
-- Determine ymin data
nearest_good_direction(-0.5*PI,aitv,a,a_in);
IF SIN(a) >= 0.0 THEN
ymin_exists := TRUE;
ymin := yc + real_min(ritv)*SIN(a);
ymin_in := a_in AND (min_included(ritv) OR (SIN(a) = 0.0));
ELSE
IF max_exists(ritv) THEN
ymin_exists := TRUE;
ymin := yc + real_max(ritv)*SIN(a);
ymin_in := a_in AND max_included(ritv);
ELSE
ymin_exists := FALSE;
END_IF;
END_IF;
-- Determine ymax data
nearest_good_direction(0.5*PI,aitv,a,a_in);
IF SIN(a) <= 0.0 THEN
ymax_exists := TRUE;
ymax := yc + real_min(ritv)*SIN(a);
ymax_in := a_in AND (min_included(ritv) OR (SIN(a) = 0.0));
ELSE
IF max_exists(ritv) THEN
ymax_exists := TRUE;
ymax := yc + real_max(ritv)*SIN(a);
ymax_in := a_in AND max_included(ritv);
ELSE
ymax_exists := FALSE;
END_IF;
END_IF;
-- Construct result
IF NOT (xmin_exists OR xmax_exists OR ymin_exists OR ymax_exists) THEN
RETURN (?); -- No finite boundaries exist
END_IF;
-- Construct real_constraint
IF xmin_exists THEN
IF xmin_in THEN min_clo := closed; ELSE min_clo := open; END_IF;
IF xmax_exists THEN
IF xmax_in THEN max_clo := closed; ELSE max_clo := open; END_IF;
xitv := make_finite_real_interval(xmin,min_clo,xmax,max_clo);
ELSE
xitv := make_real_interval_from_min(xmin,min_clo);
END_IF;
ELSE
IF xmax_exists THEN
IF xmax_in THEN max_clo := closed; ELSE max_clo := open; END_IF;
xitv := make_real_interval_to_max(xmax,max_clo);
ELSE
xitv := the_reals;
END_IF;
END_IF;
-- Construct imag_constraint
IF ymin_exists THEN
IF ymin_in THEN min_clo := closed; ELSE min_clo := open; END_IF;
IF ymax_exists THEN
IF ymax_in THEN max_clo := closed; ELSE max_clo := open; END_IF;
yitv := make_finite_real_interval(ymin,min_clo,ymax,max_clo);
ELSE
yitv := make_real_interval_from_min(ymin,min_clo);
END_IF;
ELSE
IF ymax_exists THEN
IF ymax_in THEN max_clo := closed; ELSE max_clo := open; END_IF;
yitv := make_real_interval_to_max(ymax,max_clo);
ELSE
yitv := the_reals;
END_IF;
END_IF;
-- Construct cartesian region
RETURN (make_cartesian_complex_number_region(xitv,yitv));
END_FUNCTION;
FUNCTION enclose_pregion_in_pregion
(prgn : polar_complex_number_region; centre : complex_number_literal) : polar_complex_number_region;
FUNCTION angle(a : REAL) : REAL;
REPEAT WHILE a > PI; a := a - 2.0*PI; END_REPEAT;
REPEAT WHILE a <= -PI; a := a + 2.0*PI; END_REPEAT;
RETURN (a);
END_FUNCTION;
-- Find proper limits for direction interval
PROCEDURE angle_range(VAR amin, amax : REAL);
amin := angle(amin);
IF amin = PI THEN amin := -PI; END_IF;
amax := angle(amax);
IF amax <= amin THEN amax := amax + 2.0*PI; END_IF;
END_PROCEDURE;
-- Determine whether a direction is strictly within a direction interval
FUNCTION strictly_in(a : REAL;
aitv : finite_real_interval) : LOGICAL;
a := angle(a);
RETURN ({aitv.min < a < aitv.max} OR {aitv.min < a+2.0*PI < aitv.max});
END_FUNCTION;
-- Find min and max and related inclusion booleans among four candidates,
-- using a base direction chosen to ensure the algebraic comparisons are valid.
PROCEDURE find_aminmax( ab,a0,a1,a2,a3 : REAL;
in0,in1,in2,in3 : BOOLEAN;
VAR amin,amax : REAL;
VAR amin_in,amax_in : BOOLEAN);
LOCAL
a : REAL;
END_LOCAL;
amin := angle(a0-ab); amin_in := in0;
amax := amin; amax_in := in0;
a := angle(a1-ab);
IF a = amin THEN amin_in := amin_in OR in1; END_IF;
IF a < amin THEN amin := a; amin_in := in1; END_IF;
IF a = amax THEN amax_in := amax_in OR in1; END_IF;
IF a > amax THEN amax := a; amax_in := in1; END_IF;
a := angle(a2-ab);
IF a = amin THEN amin_in := amin_in OR in2; END_IF;
IF a < amin THEN amin := a; amin_in := in2; END_IF;
IF a = amax THEN amax_in := amax_in OR in2; END_IF;
IF a > amax THEN amax := a; amax_in := in2; END_IF;
a := angle(a3-ab);
IF a = amin THEN amin_in := amin_in OR in3; END_IF;
IF a < amin THEN amin := a; amin_in := in3; END_IF;
IF a = amax THEN amax_in := amax_in OR in3; END_IF;
IF a > amax THEN amax := a; amax_in := in3; END_IF;
amin := amin+ab;
amax := amax+ab;
angle_range(amin,amax);
END_PROCEDURE;
LOCAL
ritp, ritv : real_interval;
aitp, aitv : finite_real_interval;
xp, yp, xc, yc, rmax, rmin, amin, amax, rc, acp, apc : REAL := 0.0;
rmax_in, rmin_in, amin_in, amax_in : BOOLEAN := FALSE;
rmxp, rmnp, x, y, r, a, ab, r0, a0, r1, a1, r2, a2, r3, a3 : REAL := 0.0;
in0, in1, in2, in3, inn : BOOLEAN := FALSE;
minclo, maxclo : open_closed := open;
END_LOCAL;
-- Extract elementary input information
IF NOT EXISTS (prgn) OR NOT EXISTS (centre) THEN RETURN (?); END_IF;
xp := prgn.centre.real_part;
yp := prgn.centre.imag_part;
ritp := prgn.distance_constraint;
aitp := prgn.direction_constraint;
xc := centre.real_part;
yc := centre.imag_part;
IF (xc = xp) AND (yc = yp) THEN RETURN (prgn); END_IF;
rc := SQRT((xp-xc)**2 + (yp-yc)**2);
acp := atan2(yp-yc,xp-xc);
apc := atan2(yc-yp,xc-xp);
rmnp := real_min(ritp);
-- Analyse cases by existence of max distance and direction limits
IF max_exists(ritp) THEN
rmxp := real_max(ritp);
IF aitp.max - aitp.min = 2.0*PI THEN
-- annulus or disk, with or without slot or puncture
inn := NOT max_included(aitp); -- slot exists;
a := angle(aitp.min); -- slot direction
rmax := rc+rmxp; rmax_in := max_included(ritp);
IF inn AND (acp = a) THEN rmax_in := FALSE; END_IF;
IF rc > rmxp THEN
a0 := ASIN(rmxp/rc);
amin := angle(acp-a0); amin_in := max_included(ritp);
IF amin = PI THEN amin := -PI; END_IF;
amax := angle(acp+a0); amax_in := amin_in;
IF amax < amin THEN amax := amax + 2.0*PI; END_IF;
rmin := rc-rmxp; rmin_in := amin_in;
IF inn THEN
-- slotted case
IF apc = a THEN rmin_in := FALSE; END_IF;
IF angle(amin+0.5*PI) = a THEN amin_in := FALSE; END_IF;
IF angle(amax-0.5*PI) = a THEN amax_in := FALSE; END_IF;
END_IF;
ELSE IF rc = rmxp THEN
amin := angle(acp-0.5*PI); amin_in := FALSE;
IF amin = PI THEN amin := -PI; END_IF;
amax := angle(acp+0.5*PI); amax_in := FALSE;
IF amax < amin THEN amax := amax + 2.0*PI; END_IF;
rmin := 0.0; rmin_in := max_included(ritp);
IF inn AND (apc = a) THEN rmin_in := FALSE; END_IF;
ELSE IF rc > rmnp THEN
IF inn AND (apc = a) THEN -- in the slot
rmin := 0.0; rmin_in := FALSE;
amin := aitp.min; amin_in := FALSE;
amax := aitp.max; amax_in := FALSE;
ELSE
rmin := 0.0; rmin_in := TRUE;
amin := -PI; amin_in := FALSE;
amax := PI; amax_in := TRUE;
END_IF;
ELSE
rmin := rmnp-rc; rmin_in := min_included(ritp);
amin := -PI; amin_in := FALSE;
amax := PI; amax_in := TRUE;
IF inn THEN -- Special cases when aligned with slot
IF apc = a THEN
rmin_in := FALSE;
amin := aitp.min; amin_in := FALSE;
amax := aitp.max; amax_in := FALSE;
ELSE IF acp = a THEN
amin := aitp.min; amin_in := FALSE;
amax := aitp.max; amax_in := FALSE;
END_IF; END_IF;
END_IF;
END_IF; END_IF; END_IF;
ELSE -- direction range < 2*PI
-- Compute data for corners with respect to xc,yc
x := xp + rmxp*cos(aitp.min) - xc;
y := yp + rmxp*sin(aitp.min) - yc;
r0 := SQRT(x**2 + y**2);
in0 := max_included(ritp) AND min_included(aitp);
IF r0 <> 0.0 THEN a0 := atan2(y,x); END_IF;
x := xp + rmxp*cos(aitp.max) - xc;
y := yp + rmxp*sin(aitp.max) - yc;
r1 := SQRT(x**2 + y**2);
in1 := max_included(ritp) AND max_included(aitp);
IF r1 <> 0.0 THEN a1 := atan2(y,x); END_IF;
x := xp + rmnp*cos(aitp.max) - xc;
y := yp + rmnp*sin(aitp.max) - yc;
r2 := SQRT(x**2 + y**2);
in2 := min_included(ritp) AND max_included(aitp);
IF r2 <> 0.0 THEN a2 := atan2(y,x); ELSE a2 := a1; in2 := in1; END_IF;
IF r1 = 0.0 THEN a1 := a2; in1 := in2; END_IF;
x := xp + rmnp*cos(aitp.min) - xc;
y := yp + rmnp*sin(aitp.min) - yc;
r3 := SQRT(x**2 + y**2);
in3 := min_included(ritp) AND min_included(aitp);
IF r3 <> 0.0 THEN a3 := atan2(y,x); ELSE a3 := a0; in3 := in0; END_IF;
IF r0 = 0.0 THEN a0 := a3; in0 := in3; END_IF;
IF rmnp = 0.0 THEN in2 := min_included(ritp); in3 := in2; END_IF;
IF (apc = angle(aitp.min)) OR (acp = angle(aitp.min)) THEN
in0 := min_included(aitp);
in3 := in0;
ELSE IF (apc = angle(aitp.max)) OR (acp = angle(aitp.max)) THEN
in1 := max_included(aitp);
in2 := in1;
END_IF; END_IF;
-- Find rmax
IF strictly_in(acp,aitp) THEN
rmax := rc+rmxp; rmax_in := max_included(ritp);
ELSE
rmax := r0; rmax_in := in0;
IF rmax = r1 THEN rmax_in := rmax_in OR in1; END_IF;
IF rmax < r1 THEN rmax := r1; rmax_in := in1; END_IF;
IF rmax = r2 THEN rmax_in := rmax_in OR in2; END_IF;
IF rmax < r2 THEN rmax := r2; rmax_in := in2; END_IF;
IF rmax = r3 THEN rmax_in := rmax_in OR in3; END_IF;
IF rmax < r3 THEN rmax := r3; rmax_in := in3; END_IF;
END_IF;
-- Find rmin
IF strictly_in(apc,aitp) THEN
IF rc >= rmxp THEN
rmin := rc-rmxp; rmin_in := max_included(ritp);
ELSE IF rc <= rmnp THEN
rmin := rmnp-rc; rmin_in := min_included(ritp);
ELSE
rmin := 0.0; rmin_in := TRUE;
END_IF; END_IF;
ELSE
rmin := r0; rmin_in := in0;
a := apc-aitp.min;
r := rc*COS(a);
IF {rmnp < r < rmxp} THEN -- use nearest point on line segment
rmin := rc*SIN(ABS(a)); rmin_in := min_included(aitp);
END_IF;
a := apc-aitp.max;
r := rc*COS(a);
IF {rmnp < r < rmxp} THEN -- try nearest point on line segment
r := rc*SIN(ABS(a)); inn := max_included(aitp);
IF r = rmin THEN rmin_in := rmin_in OR inn; END_IF;
IF r < rmin THEN rmin := r; rmin_in := inn; END_IF;
END_IF;
IF r1 = rmin THEN rmin_in := rmin_in OR in1; END_IF;
IF r1 < rmin THEN rmin := r1; rmin_in := in1; END_IF;
IF r2 = rmin THEN rmin_in := rmin_in OR in2; END_IF;
IF r2 < rmin THEN rmin := r2; rmin_in := in2; END_IF;
IF r3 = rmin THEN rmin_in := rmin_in OR in3; END_IF;
IF r3 < rmin THEN rmin := r3; rmin_in := in3; END_IF;
END_IF;
-- Find amin and amax, initially with respect to base direction ab.
IF rc >= rmxp THEN -- outside outer circle
ab := acp;
find_aminmax(ab,a0,a1,a2,a3,in0,in1,in2,in3,amin,amax,amin_in,amax_in);
a := ACOS(rmxp/rc);
IF strictly_in(apc-a,aitp) THEN
amin := ab-ASIN(rmxp/rc); amin_in := max_included(ritp);
END_IF;
IF strictly_in(apc+a,aitp) THEN
amax := ab+ASIN(rmxp/rc); amax_in := max_included(ritp);
END_IF;
angle_range(amin,amax);
ELSE IF rc > rmnp THEN
ab := angle(0.5*(aitp.min+aitp.max)); -- reference direction
find_aminmax(ab,a0,a1,a2,a3,in0,in1,in2,in3,amin,amax,amin_in,amax_in);
ELSE
-- Using base direction midway in prgn, compute all directions using
-- values which ensure a3 < a2 and a0 < a1 algebraically.
ab := angle(0.5*(aitp.min+aitp.max)); -- reference direction
a0 := angle(a0-ab);
a1 := angle(a1-ab);
a2 := angle(a2-ab);
a3 := angle(a3-ab);
IF a3 > a2 THEN a2 := a2 + 2.0*PI; END_IF;
IF a0 > a1 THEN a0 := a0 + 2.0*PI; END_IF;
IF a3 < a0 THEN amin := a3; amin_in := in3;
ELSE amin := a0; amin_in := in0; END_IF;
IF a2 > a1 THEN amax := a2; amax_in := in2;
ELSE amax := a1; amax_in := in1; END_IF;
IF (amax - amin > 2.0*PI) OR
((amax - amin = 2.0*PI) AND (amin_in OR amax_in)) THEN
-- Cannot see out
amin := -PI; amin_in := FALSE;
amax := PI; amax_in := TRUE;
ELSE
amin := amin + ab;
amax := amax + ab;
angle_range(amin,amax);
END_IF;
END_IF; END_IF;
END_IF;
IF rmin_in THEN minclo := closed; END_IF;
IF rmax_in THEN maxclo := closed; END_IF;
ritv := make_finite_real_interval(rmin,minclo,rmax,maxclo);
ELSE -- Not max_exists(ritp)
IF (rc > rmnp) AND strictly_in(apc,aitp) THEN
RETURN (?); -- No pregion exists. (Would require whole plane.)
END_IF;
IF aitp.max - aitp.min = 2.0*PI THEN
-- complement of disk, with or without slot
a := angle(aitp.min); -- slot direction
IF rc > rmnp THEN -- already excluded if not aligned with slot
IF max_included(aitp) THEN
RETURN (?); -- No pregion exists. (Would require whole plane.)
END_IF;
rmin := 0.0; rmin_in := FALSE;
amin := aitp.min; amin_in := FALSE;
amax := aitp.max; amax_in := FALSE;
ELSE
rmin := rmnp-rc; rmin_in := min_included(ritp);
amin := -PI; amin_in := FALSE;
amax := PI; amax_in := TRUE;
IF NOT max_included(aitp) THEN -- Special cases when aligned with slot
IF apc = a THEN
rmin_in := FALSE;
amin := aitp.min; amin_in := FALSE;
amax := aitp.max; amax_in := FALSE;
ELSE IF acp = a THEN
amin := aitp.min; amin_in := FALSE;
amax := aitp.max; amax_in := FALSE;
END_IF; END_IF;
END_IF;
END_IF;
ELSE -- direction range < 2*PI
-- Compute data for corners with respect to xc,yc (two at infinity)
a0 := angle(aitp.min);
in0 := FALSE;
a1 := angle(aitp.max);
in1 := FALSE;
x := xp + rmnp*cos(aitp.max) - xc;
y := yp + rmnp*sin(aitp.max) - yc;
r2 := SQRT(x**2 + y**2);
in2 := min_included(ritp) AND max_included(aitp);
IF r2 <> 0.0 THEN a2 := atan2(y,x); ELSE a2 := a1; in2 := in1; END_IF;
x := xp + rmnp*cos(aitp.min) - xc;
y := yp + rmnp*sin(aitp.min) - yc;
r3 := SQRT(x**2 + y**2);
in3 := min_included(ritp) AND min_included(aitp);
IF r3 <> 0.0 THEN a3 := atan2(y,x); ELSE a3 := a0; in3 := in0; END_IF;
IF rmnp = 0.0 THEN in2 := min_included(ritp); in3 := in2; END_IF;
IF (apc = angle(aitp.min)) OR (acp = angle(aitp.min)) THEN
in0 := min_included(aitp);
in3 := in0;
ELSE IF (apc = angle(aitp.max)) OR (acp = angle(aitp.max)) THEN
in1 := max_included(aitp);
in2 := in1;
END_IF; END_IF;
-- Find rmin
IF strictly_in(apc,aitp) THEN
rmin := rmnp-rc; rmin_in := min_included(ritp);
ELSE
rmin := r2; rmin_in := in2;
a := apc-aitp.min;
r := rc*COS(a);
IF rmnp < r THEN -- use nearest point on aitp.min ray
rmin := rc*SIN(ABS(a)); rmin_in := min_included(aitp);
END_IF;
a := apc-aitp.max;
r := rc*COS(a);
IF rmnp < r THEN -- try nearest point on aitp.max ray
r := rc*SIN(ABS(a)); inn := max_included(aitp);
IF r = rmin THEN rmin_in := rmin_in OR inn; END_IF;
IF r < rmin THEN rmin := r; rmin_in := inn; END_IF;
END_IF;
IF r3 = rmin THEN rmin_in := rmin_in OR in3; END_IF;
IF r3 < rmin THEN rmin := r3; rmin_in := in3; END_IF;
END_IF;
-- Find amin and amax
ab := angle(0.5*(aitp.min+aitp.max)); -- reference direction
IF rc > rmnp THEN
find_aminmax(ab,a0,a1,a2,a3,in0,in1,in2,in3,amin,amax,amin_in,amax_in);
ELSE
-- Using base direction midway in prgn, compute all directions using
-- values which ensure a3 < a2 and a0 < a1 algebraically.
a0 := angle(a0-ab);
a1 := angle(a1-ab);
a2 := angle(a2-ab);
a3 := angle(a3-ab);
IF a3 > a2 THEN a2 := a2 + 2.0*PI; END_IF;
IF a0 > a1 THEN a0 := a0 + 2.0*PI; END_IF;
IF a3 < a0 THEN amin := a3; amin_in := in3;
ELSE amin := a0; amin_in := in0; END_IF;
IF a2 > a1 THEN amax := a2; amax_in := in2;
ELSE amax := a1; amax_in := in1; END_IF;
IF (amax - amin > 2.0*PI) OR
((amax - amin = 2.0*PI) AND (amin_in OR amax_in)) THEN
-- Cannot see out
amin := -PI; amin_in := FALSE;
amax := PI; amax_in := TRUE;
IF (rmin = 0.0) AND rmin_in THEN
RETURN (?); -- No pregion exists. (Would require whole plane.)
END_IF;
ELSE
amin := amin + ab;
amax := amax + ab;
angle_range(amin,amax);
END_IF;
END_IF;
END_IF;
IF rmin_in THEN minclo := closed; END_IF;
ritv := make_real_interval_from_min(rmin,minclo);
END_IF;
minclo := open; maxclo := open;
IF amin_in THEN minclo := closed; END_IF;
IF amax_in THEN maxclo := closed; END_IF;
aitv := make_finite_real_interval(amin,minclo,amax,maxclo);
-- Construct polar region
RETURN (make_polar_complex_number_region(centre,ritv,aitv));
END_FUNCTION;
FUNCTION equal_cregion_pregion
(crgn : cartesian_complex_number_region; prgn : polar_complex_number_region) : LOGICAL;
LOCAL
arng, amin, xc, yc : REAL;
aitv, xitv, yitv : real_interval;
c_in : BOOLEAN;
END_LOCAL;
IF NOT EXISTS (crgn) OR NOT EXISTS (prgn) THEN RETURN (FALSE); END_IF;
IF max_exists(prgn.distance_constraint) THEN RETURN (FALSE); END_IF;
IF real_min(prgn.distance_constraint) <> 0.0 THEN RETURN (FALSE); END_IF;
c_in := min_included(prgn.distance_constraint);
aitv := prgn.direction_constraint;
amin := aitv.min;
arng := aitv.max - amin;
xc := prgn.centre.real_part;
yc := prgn.centre.imag_part;
xitv := crgn.real_constraint;
yitv := crgn.imag_constraint;
IF arng = 0.5*PI THEN
IF amin = 0.0 THEN -- quadrant to upper right
RETURN (NOT max_exists(xitv) AND NOT max_exists(yitv) AND min_exists(xitv)
AND min_exists(yitv) AND (real_min(xitv) = xc) AND (real_min(yitv) = yc)
AND ((c_in AND min_included(aitv) AND max_included(aitv)
AND min_included(xitv) AND min_included(yitv))
OR (NOT c_in AND NOT min_included(aitv) AND max_included(aitv)
AND min_included(xitv) AND NOT min_included(yitv))
OR (NOT c_in AND min_included(aitv) AND NOT max_included(aitv)
AND NOT min_included(xitv) AND min_included(yitv))
OR (NOT c_in AND NOT min_included(aitv) AND NOT max_included(aitv)
AND NOT min_included(xitv) AND NOT min_included(yitv))));
END_IF;
IF amin = 0.5*PI THEN -- quadrant to upper left
RETURN (max_exists(xitv) AND NOT max_exists(yitv) AND NOT min_exists(xitv)
AND min_exists(yitv) AND (real_max(xitv) = xc) AND (real_min(yitv) = yc)
AND ((c_in AND min_included(aitv) AND max_included(aitv)
AND max_included(xitv) AND min_included(yitv))
OR (NOT c_in AND NOT min_included(aitv) AND max_included(aitv)
AND max_included(xitv) AND NOT min_included(yitv))
OR (NOT c_in AND min_included(aitv) AND NOT max_included(aitv)
AND NOT max_included(xitv) AND min_included(yitv))
OR (NOT c_in AND NOT min_included(aitv) AND NOT max_included(aitv)
AND NOT max_included(xitv) AND NOT min_included(yitv))));
END_IF;
IF amin = -PI THEN -- quadrant to lower left
RETURN (max_exists(xitv) AND max_exists(yitv) AND NOT min_exists(xitv)
AND NOT min_exists(yitv) AND (real_max(xitv) = xc) AND (real_max(yitv) = yc)
AND ((c_in AND min_included(aitv) AND max_included(aitv)
AND max_included(xitv) AND max_included(yitv))
OR (NOT c_in AND NOT min_included(aitv) AND max_included(aitv)
AND max_included(xitv) AND NOT max_included(yitv))
OR (NOT c_in AND min_included(aitv) AND NOT max_included(aitv)
AND NOT max_included(xitv) AND max_included(yitv))
OR (NOT c_in AND NOT min_included(aitv) AND NOT max_included(aitv)
AND NOT max_included(xitv) AND NOT max_included(yitv))));
END_IF;
IF amin = -0.5*PI THEN -- quadrant to lower right
RETURN (NOT max_exists(xitv) AND max_exists(yitv) AND min_exists(xitv)
AND NOT min_exists(yitv) AND (real_min(xitv) = xc) AND (real_max(yitv) = yc)
AND ((c_in AND min_included(aitv) AND max_included(aitv)
AND min_included(xitv) AND max_included(yitv))
OR (NOT c_in AND NOT min_included(aitv) AND max_included(aitv)
AND min_included(xitv) AND NOT max_included(yitv))
OR (NOT c_in AND min_included(aitv) AND NOT max_included(aitv)
AND NOT min_included(xitv) AND max_included(yitv))
OR (NOT c_in AND NOT min_included(aitv) AND NOT max_included(aitv)
AND NOT min_included(xitv) AND NOT max_included(yitv))));
END_IF;
END_IF;
IF arng = PI THEN
IF amin = 0.0 THEN -- upper half space
RETURN (NOT max_exists(xitv) AND NOT max_exists(yitv) AND NOT min_exists(xitv)
AND min_exists(yitv) AND (real_min(yitv) = yc)
AND ((c_in AND min_included(aitv) AND max_included(aitv)
AND min_included(yitv))
OR (NOT c_in AND NOT min_included(aitv) AND NOT max_included(aitv)
AND NOT min_included(yitv))));
END_IF;
IF amin = 0.5*PI THEN -- left half space
RETURN (max_exists(xitv) AND NOT max_exists(yitv) AND NOT min_exists(xitv)
AND NOT min_exists(yitv) AND (real_max(xitv) = xc)
AND ((c_in AND min_included(aitv) AND max_included(aitv)
AND max_included(xitv))
OR (NOT c_in AND NOT min_included(aitv) AND NOT max_included(aitv)
AND NOT max_included(xitv))));
END_IF;
IF amin = -PI THEN -- lower half space
RETURN (NOT max_exists(xitv) AND max_exists(yitv) AND NOT min_exists(xitv)
AND NOT min_exists(yitv) AND (real_max(yitv) = yc)
AND ((c_in AND min_included(aitv) AND max_included(aitv)
AND max_included(yitv))
OR (NOT c_in AND NOT min_included(aitv) AND NOT max_included(aitv)
AND NOT max_included(yitv))));
END_IF;
IF amin = -0.5*PI THEN -- right half space
RETURN (NOT max_exists(xitv) AND NOT max_exists(yitv) AND min_exists(xitv)
AND NOT min_exists(yitv) AND (real_min(xitv) = xc)
AND ((c_in AND min_included(aitv) AND max_included(aitv)
AND min_included(xitv))
OR (NOT c_in AND NOT min_included(aitv) AND NOT max_included(aitv)
AND NOT min_included(xitv))));
END_IF;
END_IF;
RETURN (FALSE);
END_FUNCTION;
FUNCTION equal_maths_functions
(fun1 : maths_function; fun2 : maths_function) : LOGICAL;
LOCAL
cum : LOGICAL;
END_LOCAL;
IF fun1 = fun2 THEN RETURN (TRUE); END_IF;
cum := equal_maths_spaces(fun1.domain,fun2.domain);
IF cum = FALSE THEN RETURN (FALSE); END_IF;
cum := cum AND equal_maths_spaces(fun1.range,fun2.range);
IF cum = FALSE THEN RETURN (FALSE); END_IF;
-- A lot of further analysis is possible, but not required.
RETURN (UNKNOWN);
END_FUNCTION;
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, set2 : SET OF maths_value;
cum : LOGICAL := TRUE;
base : maths_space;
expnt : INTEGER;
factors : LIST OF maths_space;
factors2 : LIST OF maths_space;
fs1, fs2 : function_space;
cum2 : LOGICAL;
END_LOCAL;
IF spc1 = spc2 THEN RETURN (TRUE); END_IF;
-- Consider cases where it is not yet certain that spc1 <> spc2.
IF 'FINITE_SPACE' IN spc1types THEN
set1 := spc1\finite_space.members;
IF 'FINITE_SPACE' IN spc2types THEN
-- Members may have different but equivalent representations and in
-- different orders. May also have disguised repeats in same set of members.
set2 := spc2\finite_space.members;
REPEAT i := 1 TO SIZEOF (set1);
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);
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;
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;
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
-- Quadrants and half spaces have two representations
RETURN (equal_cregion_pregion(spc1,spc2));
END_IF;
IF ('POLAR_COMPLEX_NUMBER_REGION' IN spc1types) AND
('CARTESIAN_COMPLEX_NUMBER_REGION' IN spc2types) THEN
-- Quadrants and half spaces have two representations
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);
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);
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);
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
-- Safety check. Should be unreachable.
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;
-- Remaining cases too complex.
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
-- Safety check. Should be unreachable.
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;
-- Remaining cases too complex.
RETURN (UNKNOWN);
END_IF;
cum := cum AND equal_maths_spaces(fs1.range_argument,fs2.range_argument);
RETURN (cum);
END_IF;
RETURN (FALSE);
END_FUNCTION;
FUNCTION equal_maths_values
(val1 : maths_value; val2 : maths_value) : LOGICAL;
FUNCTION mem_of_vs(val1, val2 : maths_value) : LOGICAL;
IF NOT has_values_space(val2) THEN RETURN (UNKNOWN); END_IF;
IF NOT member_of(val1,values_space_of(val2)) THEN RETURN (FALSE); END_IF;
RETURN (UNKNOWN);
END_FUNCTION; -- mem_of_vs
LOCAL
types1, types2 : SET OF STRING;
list1, list2 : LIST OF maths_value;
cum : LOGICAL := TRUE;
END_LOCAL;
IF NOT EXISTS (val1) OR NOT EXISTS (val2) THEN RETURN (FALSE); END_IF;
IF val1 = val2 THEN RETURN (TRUE); END_IF;
types1 := stripped_typeof (val1);
types2 := stripped_typeof (val2);
IF ('MATHS_ATOM' IN types1) OR ('COMPLEX_NUMBER_LITERAL' IN types1) THEN
IF 'MATHS_ATOM' IN types2 THEN RETURN (FALSE); END_IF;
IF 'COMPLEX_NUMBER_LITERAL' IN types2 THEN RETURN (FALSE); END_IF;
IF 'LIST' IN types2 THEN RETURN (FALSE); END_IF;
IF 'MATHS_SPACE' IN types2 THEN RETURN (FALSE); END_IF;
IF 'MATHS_FUNCTION' IN types2 THEN RETURN (FALSE); END_IF;
IF 'GENERIC_EXPRESSION' IN types2 THEN RETURN (mem_of_vs(val1,val2)); END_IF;
RETURN (UNKNOWN);
END_IF;
IF ('MATHS_ATOM' IN types2) OR ('COMPLEX_NUMBER_LITERAL' IN types2) THEN
RETURN (equal_maths_values(val2,val1));
END_IF;
IF 'LIST' IN types1 THEN
IF 'LIST' IN types2 THEN
list1 := val1;
list2 := val2;
IF SIZEOF (list1) <> SIZEOF (list2) THEN RETURN (FALSE); END_IF;
REPEAT i := 1 TO SIZEOF (list1);
cum := cum AND equal_maths_values (list1[i], list2[i]);
IF cum = FALSE THEN RETURN (FALSE); END_IF;
END_REPEAT;
RETURN (cum);
END_IF;
IF 'MATHS_SPACE' IN types2 THEN RETURN (FALSE); END_IF;
IF 'MATHS_FUNCTION' IN types2 THEN RETURN (FALSE); END_IF;
IF 'GENERIC_EXPRESSION' IN types2 THEN RETURN (mem_of_vs(val1,val2)); END_IF;
RETURN (UNKNOWN);
END_IF;
IF 'LIST' IN types2 THEN RETURN (equal_maths_values(val2,val1)); END_IF;
IF 'MATHS_SPACE' IN types1 THEN
IF 'MATHS_SPACE' IN types2 THEN
RETURN (equal_maths_spaces(val1,val2));
END_IF;
IF 'MATHS_FUNCTION' IN types2 THEN RETURN (FALSE); END_IF;
IF 'GENERIC_EXPRESSION' IN types2 THEN RETURN (mem_of_vs(val1,val2)); END_IF;
RETURN (UNKNOWN);
END_IF;
IF 'MATHS_SPACE' IN types2 THEN RETURN (equal_maths_values(val2,val1)); END_IF;
IF 'MATHS_FUNCTION' IN types1 THEN
IF 'MATHS_FUNCTION' IN types2 THEN
RETURN (equal_maths_functions(val1,val2));
END_IF;
IF 'GENERIC_EXPRESSION' IN types2 THEN RETURN (mem_of_vs(val1,val2)); END_IF;
RETURN (UNKNOWN);
END_IF;
IF 'MATHS_FUNCTION' IN types2 THEN RETURN (equal_maths_values(val2,val1)); END_IF;
IF ('GENERIC_EXPRESSION' IN types1) AND ('GENERIC_EXPRESSION' IN types2) THEN
IF NOT has_values_space(val1) OR NOT has_values_space(val2) THEN
RETURN (UNKNOWN);
END_IF;
IF NOT compatible_spaces(values_space_of(val1),values_space_of(val2)) THEN
RETURN (FALSE);
END_IF;
END_IF;
RETURN (UNKNOWN);
END_FUNCTION;
FUNCTION es_subspace_of_es
(es1 : elementary_space_enumerators; es2 : elementary_space_enumerators) : BOOLEAN;
IF NOT EXISTS (es1) OR NOT EXISTS (es2) THEN RETURN (FALSE); END_IF;
IF es1 = es2 THEN RETURN (TRUE); END_IF;
IF es2 = es_generics THEN RETURN (TRUE); END_IF;
IF (es1 = es_booleans) AND (es2 = es_logicals) THEN RETURN (TRUE); END_IF;
IF (es2 = es_numbers) AND ((es1 = es_complex_numbers) OR (es1 = es_reals) OR
(es1 = es_integers)) THEN RETURN (TRUE); END_IF;
RETURN (FALSE);
END_FUNCTION;
FUNCTION expression_is_constant
(expr : generic_expression) : BOOLEAN;
RETURN (bool(SIZEOF (free_variables_of (expr)) = 0));
END_FUNCTION;
FUNCTION extract_factors
(tspace : tuple_space; m : INTEGER; n : INTEGER) : tuple_space;
LOCAL
tsp : tuple_space := the_zero_tuple_space;
END_LOCAL;
REPEAT i := m TO n;
tsp := assoc_product_space (tsp, factor_space (tspace, i));
END_REPEAT;
RETURN (tsp);
END_FUNCTION;
FUNCTION extremal_position_check
(fun : linearized_table_function) : BOOLEAN;
LOCAL
source_domain : maths_space;
source_interval : finite_integer_interval;
index : INTEGER := 1;
base : INTEGER;
shape : LIST OF positive_integer;
ndim : positive_integer;
slo, shi : INTEGER;
sublo : LIST OF INTEGER := [];
subhi : LIST OF INTEGER := [];
END_LOCAL;
IF NOT EXISTS (fun) THEN RETURN (FALSE); END_IF;
source_domain := factor1 (fun.source.domain);
IF (schema_prefix + 'TUPLE_SPACE') IN TYPEOF (source_domain) THEN
source_domain := factor1 (source_domain);
END_IF;
IF NOT ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN TYPEOF (source_domain)) THEN
RETURN (FALSE);
END_IF;
source_interval := source_domain;
base := fun\explicit_table_function.index_base;
shape := fun\explicit_table_function.shape;
IF (schema_prefix + 'STANDARD_TABLE_FUNCTION') IN TYPEOF (fun) THEN
REPEAT j := 1 TO SIZEOF (shape);
index := index * shape[j];
END_REPEAT;
index := fun.first + index - 1;
RETURN (bool({source_interval.min <= index <= source_interval.max}));
END_IF;
IF (schema_prefix + 'REGULAR_TABLE_FUNCTION') IN TYPEOF (fun) THEN
ndim := SIZEOF (fun\explicit_table_function.shape);
REPEAT j:= 1 TO ndim;
slo := base;
shi := base + shape[j] - 1;
IF fun\regular_table_function.increments[j] >= 0 THEN
INSERT (sublo, slo, j-1);
INSERT (subhi, shi, j-1);
ELSE
INSERT (sublo, shi, j-1);
INSERT (subhi, slo, j-1);
END_IF;
END_REPEAT;
index := regular_indexing (sublo, base, shape,
fun\regular_table_function.increments, fun.first);
IF NOT ({source_interval.min <= index <= source_interval.max}) THEN
RETURN (FALSE);
END_IF;
index := regular_indexing (subhi, base, shape,
fun\regular_table_function.increments, fun.first);
IF NOT ({source_interval.min <= index <= source_interval.max}) THEN
RETURN (FALSE);
END_IF;
RETURN (TRUE);
END_IF;
RETURN (FALSE);
END_FUNCTION;
FUNCTION factor1
(tspace : tuple_space) : maths_space;
LOCAL
typenames : SET OF STRING := TYPEOF (tspace);
END_LOCAL;
IF (schema_prefix + 'UNIFORM_PRODUCT_SPACE') IN typenames THEN
RETURN (tspace\uniform_product_space.base);
END_IF;
IF (schema_prefix + 'LISTED_PRODUCT_SPACE') IN typenames THEN
RETURN (tspace\listed_product_space.factors[1]);
-- This path could return the indeterminate value if the list is empty.
-- This is the correct result for this case.
END_IF;
IF (schema_prefix + 'EXTENDED_TUPLE_SPACE') IN typenames THEN
RETURN (factor1 (tspace\extended_tuple_space.base));
END_IF;
-- Should not be reachable.
RETURN (?);
END_FUNCTION;
FUNCTION factor_space
(tspace : tuple_space; idx : positive_integer) : maths_space;
LOCAL
typenames : SET OF STRING := TYPEOF (tspace);
END_LOCAL;
IF (schema_prefix + 'UNIFORM_PRODUCT_SPACE') IN typenames THEN
IF idx <= tspace\uniform_product_space.exponent THEN
RETURN (tspace\uniform_product_space.base);
END_IF;
RETURN (?);
END_IF;
IF (schema_prefix + 'LISTED_PRODUCT_SPACE') IN typenames THEN
IF idx <= SIZEOF (tspace\listed_product_space.factors) THEN
RETURN (tspace\listed_product_space.factors[idx]);
END_IF;
RETURN (?);
END_IF;
IF (schema_prefix + 'EXTENDED_TUPLE_SPACE') IN typenames THEN
IF idx <= space_dimension (tspace\extended_tuple_space.base) THEN
RETURN (factor_space (tspace\extended_tuple_space.base, idx));
END_IF;
RETURN (tspace\extended_tuple_space.extender);
END_IF;
-- Should not be reachable.
RETURN (?);
END_FUNCTION;
FUNCTION free_variables_of
(expr : generic_expression) : SET[0:?] OF generic_variable;
LOCAL
typenames : SET OF STRING := stripped_typeof(expr);
result : SET OF generic_variable := [];
exprs : LIST OF generic_expression := [];
END_LOCAL;
IF 'GENERIC_LITERAL' IN typenames THEN
RETURN (result);
END_IF;
IF 'GENERIC_VARIABLE' IN typenames THEN
result := result + expr;
RETURN (result);
END_IF;
IF 'QUANTIFIER_EXPRESSION' IN typenames THEN
exprs := QUERY (ge <* expr\multiple_arity_generic_expression.operands |
NOT (ge IN expr\quantifier_expression.variables));
REPEAT i := 1 TO SIZEOF (exprs);
result := result + free_variables_of (exprs[i]);
END_REPEAT;
REPEAT i := 1 TO SIZEOF (expr\quantifier_expression.variables);
result := result - expr\quantifier_expression.variables[i];
END_REPEAT;
RETURN (result);
END_IF;
IF 'UNARY_GENERIC_EXPRESSION' IN typenames THEN
RETURN (free_variables_of (expr\unary_generic_expression.operand));
END_IF;
IF 'BINARY_GENERIC_EXPRESSION' IN typenames THEN
result := free_variables_of (expr\binary_generic_expression.operands[1]);
RETURN (result + free_variables_of (expr\binary_generic_expression.operands[2]));
END_IF;
IF 'MULTIPLE_ARITY_GENERIC_EXPRESSION' IN typenames THEN
REPEAT i := 1 TO SIZEOF (expr\multiple_arity_generic_expression.operands);
result := result + free_variables_of (
expr\multiple_arity_generic_expression.operands[i]);
END_REPEAT;
RETURN (result);
END_IF;
-- In this case the subtype shall not contain any variable (see IP1 in
-- generic_expression).
RETURN (result);
END_FUNCTION;
FUNCTION function_applicability
(func : maths_function_select; arguments : LIST[1:?] OF maths_value) : BOOLEAN;
LOCAL
domain : tuple_space := convert_to_maths_function(func).domain;
domain_types : SET OF STRING := TYPEOF (domain);
narg : positive_integer := SIZEOF (arguments);
arg : generic_expression;
END_LOCAL;
IF (schema_prefix + 'PRODUCT_SPACE') IN domain_types THEN
IF space_dimension (domain) <> narg THEN RETURN (FALSE); END_IF;
ELSE
IF (schema_prefix + 'EXTENDED_TUPLE_SPACE') IN domain_types THEN
IF space_dimension (domain) > narg THEN RETURN (FALSE); END_IF;
ELSE
RETURN (FALSE); -- Should be unreachable
END_IF;
END_IF;
REPEAT i := 1 TO narg;
arg := convert_to_operand (arguments[i]);
IF NOT has_values_space (arg) THEN RETURN (FALSE); END_IF;
IF NOT compatible_spaces (factor_space (domain, i), values_space_of (arg)) THEN
RETURN (FALSE);
END_IF;
END_REPEAT;
RETURN (TRUE);
END_FUNCTION;
FUNCTION function_is_1d_array
(func : maths_function) : BOOLEAN;
LOCAL
temp : maths_space;
END_LOCAL;
IF NOT EXISTS (func) THEN RETURN (FALSE); END_IF;
IF space_dimension (func.domain) <> 1 THEN RETURN (FALSE); END_IF;
temp := factor1 (func.domain);
IF (schema_prefix + 'PRODUCT_SPACE') IN TYPEOF (temp) THEN
IF space_dimension (temp) <> 1 THEN RETURN (FALSE); END_IF;
temp := factor1 (temp);
END_IF;
IF (schema_prefix + 'FINITE_INTEGER_INTERVAL') IN TYPEOF (temp) THEN
RETURN (TRUE);
END_IF;
RETURN (FALSE);
END_FUNCTION;
FUNCTION function_is_1d_table
(func : maths_function) : BOOLEAN;
LOCAL
temp : maths_space;
itvl : finite_integer_interval;
END_LOCAL;
IF NOT EXISTS (func) THEN RETURN (FALSE); END_IF;
IF space_dimension (func.domain) <> 1 THEN RETURN (FALSE); END_IF;
temp := factor1 (func.domain);
IF (schema_prefix + 'PRODUCT_SPACE') IN TYPEOF (temp) THEN
IF space_dimension (temp) <> 1 THEN RETURN (FALSE); END_IF;
temp := factor1 (temp);
END_IF;
IF (schema_prefix + 'FINITE_INTEGER_INTERVAL') IN TYPEOF (temp) THEN
itvl := temp;
RETURN (bool((itvl.min = 0) OR (itvl.min = 1)));
END_IF;
RETURN (FALSE);
END_FUNCTION;
FUNCTION function_is_2d_table
(func : maths_function) : BOOLEAN;
LOCAL
temp : maths_space;
pspace : product_space;
itvl1, itvl2 : finite_integer_interval;
END_LOCAL;
IF NOT EXISTS (func) THEN RETURN (FALSE); END_IF;
IF space_dimension (func.domain) <> 1 THEN RETURN (FALSE); END_IF;
temp := factor1 (func.domain);
IF NOT ('PRODUCT_SPACE' IN stripped_typeof(temp)) THEN RETURN (FALSE); END_IF;
pspace := temp;
IF space_dimension (pspace) <> 2 THEN RETURN (FALSE); END_IF;
temp := factor1 (pspace);
IF NOT ('FINITE_INTEGER_INTERVAL' IN stripped_typeof(temp)) THEN
RETURN (FALSE);
END_IF;
itvl1 := temp;
temp := factor_space (pspace, 2);
IF NOT ('FINITE_INTEGER_INTERVAL' IN stripped_typeof(temp)) THEN
RETURN (FALSE);
END_IF;
itvl2 := temp;
RETURN (bool((itvl1.min = itvl2.min) AND ((itvl1.min = 0) OR (itvl1.min = 1))));
END_FUNCTION;
FUNCTION function_is_array
(func : maths_function) : BOOLEAN;
LOCAL
tspace : tuple_space;
temp : maths_space;
END_LOCAL;
IF NOT EXISTS (func) THEN RETURN (FALSE); END_IF;
tspace := func.domain;
IF (space_dimension (tspace) = 1) AND ((schema_prefix + 'TUPLE_SPACE') IN
TYPEOF (factor1 (tspace))) THEN
tspace := factor1 (tspace);
END_IF;
IF NOT ((schema_prefix + 'PRODUCT_SPACE') IN TYPEOF (tspace)) THEN
RETURN (FALSE);
END_IF;
REPEAT i := 1 TO space_dimension (tspace);
temp := factor_space (tspace, i);
IF NOT ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN TYPEOF (temp)) THEN
RETURN (FALSE);
END_IF;
END_REPEAT;
RETURN (TRUE);
END_FUNCTION;
FUNCTION function_is_table
(func : maths_function) : BOOLEAN;
LOCAL
tspace : tuple_space;
temp : maths_space;
base : INTEGER;
END_LOCAL;
IF NOT EXISTS (func) THEN RETURN (FALSE); END_IF;
tspace := func.domain;
IF (space_dimension (tspace) = 1) AND ((schema_prefix + 'TUPLE_SPACE') IN
TYPEOF (factor1 (tspace))) THEN
tspace := factor1 (tspace);
END_IF;
IF NOT ((schema_prefix + 'PRODUCT_SPACE') IN TYPEOF (tspace)) THEN
RETURN (FALSE);
END_IF;
temp := factor1 (tspace);
IF NOT ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN TYPEOF (temp)) THEN
RETURN (FALSE);
END_IF;
base := temp\finite_integer_interval.min;
IF (base <> 0) AND (base <> 1) THEN
RETURN (FALSE);
END_IF;
REPEAT i := 2 TO space_dimension (tspace);
temp := factor_space (tspace, i);
IF NOT ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN TYPEOF (temp)) THEN
RETURN (FALSE);
END_IF;
IF temp\finite_integer_interval.min <> base THEN RETURN (FALSE); END_IF;
END_REPEAT;
RETURN (TRUE);
END_FUNCTION;
FUNCTION has_values_space
(expr : generic_expression) : BOOLEAN;
LOCAL
typenames : SET OF STRING := stripped_typeof (expr);
END_LOCAL;
IF 'EXPRESSION' IN typenames THEN
RETURN (bool(('NUMERIC_EXPRESSION' IN typenames) OR
('STRING_EXPRESSION' IN typenames) OR
('BOOLEAN_EXPRESSION' IN typenames)));
END_IF;
IF 'MATHS_FUNCTION' IN typenames THEN
RETURN (TRUE);
END_IF;
IF 'FUNCTION_APPLICATION' IN typenames THEN
RETURN (TRUE);
END_IF;
IF 'MATHS_SPACE' IN typenames THEN
RETURN (TRUE);
END_IF;
IF 'MATHS_VARIABLE' IN typenames THEN
RETURN (TRUE);
END_IF;
IF 'DEPENDENT_VARIABLE_DEFINITION' IN typenames THEN
RETURN (has_values_space (expr\unary_generic_expression.operand));
END_IF;
IF 'COMPLEX_NUMBER_LITERAL' IN typenames THEN
RETURN (TRUE);
END_IF;
IF 'LOGICAL_LITERAL' IN typenames THEN
RETURN (TRUE);
END_IF;
IF 'BINARY_LITERAL' IN typenames THEN
RETURN (TRUE);
END_IF;
IF 'MATHS_ENUM_LITERAL' IN typenames THEN
RETURN (TRUE);
END_IF;
IF 'REAL_TUPLE_LITERAL' IN typenames THEN
RETURN (TRUE);
END_IF;
IF 'INTEGER_TUPLE_LITERAL' IN typenames THEN
RETURN (TRUE);
END_IF;
IF 'ATOM_BASED_LITERAL' IN typenames THEN
RETURN (TRUE);
END_IF;
IF 'MATHS_TUPLE_LITERAL' IN typenames THEN
RETURN (TRUE);
END_IF;
IF 'PARTIAL_DERIVATIVE_EXPRESSION' IN typenames THEN
RETURN (TRUE);
END_IF;
IF 'DEFINITE_INTEGRAL_EXPRESSION' IN typenames THEN
RETURN (TRUE);
END_IF;
RETURN (FALSE);
END_FUNCTION;
FUNCTION list_selected_components
(aggr : AGGREGATE OF LIST[0:?] OF maths_value; k : positive_integer) : LIST[0:?] OF maths_value;
LOCAL
result : LIST OF maths_value := [];
j : INTEGER := 0;
END_LOCAL;
REPEAT i := LOINDEX (aggr) TO HIINDEX (aggr);
IF k <= SIZEOF (aggr[i]) THEN
INSERT (result, aggr[i][k], j);
j := j + 1;
END_IF;
END_REPEAT;
RETURN (result);
END_FUNCTION;
FUNCTION make_abstracted_expression_function
(operands : LIST[2:?] OF generic_expression) : abstracted_expression_function;
RETURN (abstracted_expression_function()
|| maths_function()
|| generic_expression()
|| quantifier_expression (remove_first (operands)) -- derived
|| multiple_arity_generic_expression (operands) );
END_FUNCTION;
FUNCTION make_atom_based_literal
(lit_value : atom_based_value) : atom_based_literal;
RETURN (atom_based_literal (lit_value)
|| generic_literal()
|| simple_generic_expression()
|| generic_expression() );
END_FUNCTION;
FUNCTION make_b_spline_basis
(degree : nonnegative_integer; repeated_knots : LIST[2:?] OF REAL) : b_spline_basis;
RETURN (b_spline_basis (degree, repeated_knots)
|| maths_function()
|| generic_expression()
|| generic_literal()
|| simple_generic_expression() );
END_FUNCTION;
FUNCTION make_b_spline_function
(coef : maths_function; bases : LIST[1:?] OF b_spline_basis) : b_spline_function;
RETURN (b_spline_function (bases)
|| maths_function()
|| generic_expression()
|| unary_generic_expression (coef) );
END_FUNCTION;
FUNCTION make_banded_matrix
(index_base : zero_or_one; shape : LIST[1:?] OF positive_integer; source : maths_function; first : INTEGER; default_entry : maths_value; below : INTEGER; above : INTEGER; order : ordering_type) : banded_matrix;
RETURN (banded_matrix (default_entry, below, above, order)
|| linearized_table_function (first)
|| explicit_table_function (index_base, shape)
|| maths_function()
|| generic_expression()
|| unary_generic_expression (source) );
END_FUNCTION;
FUNCTION make_basic_sparse_matrix
(index_base : zero_or_one; shape : LIST[1:?] OF positive_integer; operands : LIST[3:3] OF maths_function; default_entry : maths_value; order : ordering_type) : basic_sparse_matrix;
RETURN (basic_sparse_matrix (default_entry, order)
|| explicit_table_function (index_base, shape)
|| maths_function()
|| generic_expression()
|| multiple_arity_generic_expression (operands) );
END_FUNCTION;
FUNCTION make_binary_literal
(lit_value : BINARY) : binary_literal;
RETURN (binary_literal (lit_value)
|| generic_literal()
|| simple_generic_expression()
|| generic_expression() );
END_FUNCTION;
FUNCTION make_boolean_literal
(lit_value : BOOLEAN) : boolean_literal;
RETURN (boolean_literal (lit_value)
|| simple_boolean_expression()
|| boolean_expression()
|| expression()
|| generic_expression()
|| simple_generic_expression()
|| generic_literal() );
END_FUNCTION;
FUNCTION make_cartesian_complex_number_region
(real_constraint : real_interval; imag_constraint : real_interval) : cartesian_complex_number_region;
RETURN (cartesian_complex_number_region (real_constraint, imag_constraint)
|| maths_space()
|| generic_expression()
|| generic_literal()
|| simple_generic_expression() );
END_FUNCTION;
FUNCTION make_complex_number_literal
(rpart : REAL; ipart : REAL) : complex_number_literal;
RETURN (complex_number_literal (rpart, ipart)
|| generic_literal()
|| simple_generic_expression()
|| generic_expression() );
END_FUNCTION;
FUNCTION make_constant_function
(sole_value : maths_value; src_of_domn : maths_space_or_function) : constant_function;
RETURN (constant_function (sole_value, src_of_domn)
|| maths_function()
|| generic_expression()
|| generic_literal()
|| simple_generic_expression() );
END_FUNCTION;
FUNCTION make_cos_expression
(operand : numeric_expression) : cos_function;
RETURN (cos_expression()
|| unary_numeric_call_expression()
|| unary_numeric_expression()
|| numeric_expression()
|| expression()
|| generic_expression()
|| unary_generic_expression (operand) );
END_FUNCTION;
FUNCTION make_definite_integral_expression
(operands : LIST[2:4] OF generic_expression; loinf : BOOLEAN; upinf : BOOLEAN) : definite_integral_expression;
RETURN (definite_integral_expression (loinf, upinf)
|| quantifier_expression ([operands[2]])
|| multiple_arity_generic_expression (operands)
|| generic_expression() );
END_FUNCTION;
FUNCTION make_definite_integral_function
(integrand : maths_function; varintg : input_selector; loinf : BOOLEAN; upinf : BOOLEAN) : definite_integral_function;
RETURN (definite_integral_function (varintg, loinf, upinf)
|| maths_function()
|| generic_expression()
|| unary_generic_expression (integrand) );
END_FUNCTION;
FUNCTION make_elementary_function
(func_id : elementary_function_enumerators) : elementary_function;
RETURN (elementary_function (func_id)
|| maths_function()
|| generic_expression()
|| generic_literal()
|| simple_generic_expression() );
END_FUNCTION;
FUNCTION make_elementary_space
(space_id : elementary_space_enumerators) : elementary_space;
RETURN (elementary_space (space_id)
|| maths_space()
|| generic_expression()
|| generic_literal()
|| simple_generic_expression() );
END_FUNCTION;
FUNCTION make_environment
(varbl : generic_variable; sem : variable_semantics) : environment;
RETURN (environment (varbl, sem) );
END_FUNCTION;
FUNCTION make_expression_denoted_function
(expression : generic_expression) : expression_denoted_function;
RETURN (expression_denoted_function()
|| maths_function()
|| generic_expression()
|| unary_generic_expression (expression) );
END_FUNCTION;
FUNCTION make_extended_tuple_space
(base : tuple_space; extender : maths_space) : extended_tuple_space;
RETURN (extended_tuple_space (base, extender)
|| maths_space ()
|| generic_expression()
|| generic_literal ()
|| simple_generic_expression() );
END_FUNCTION;
FUNCTION make_finite_function
(pairs : SET[1:?] OF LIST[2:2] OF maths_value) : finite_function;
RETURN (finite_function (pairs)
|| maths_function()
|| generic_expression()
|| generic_literal()
|| simple_generic_expression() );
END_FUNCTION;
FUNCTION make_finite_integer_interval
(min : INTEGER; max : INTEGER) : finite_integer_interval;
RETURN (finite_integer_interval (min, max)
|| maths_space()
|| generic_expression()
|| generic_literal()
|| simple_generic_expression() );
END_FUNCTION;
FUNCTION make_finite_real_interval
(min : REAL; minclo : open_closed; max : REAL; maxclo : open_closed) : finite_real_interval;
RETURN (finite_real_interval (min, minclo, max, maxclo)
|| maths_space()
|| generic_expression()
|| generic_literal()
|| simple_generic_expression() );
END_FUNCTION;
FUNCTION make_finite_space
(members : SET[0:?] OF maths_value) : finite_space;
RETURN (finite_space (members)
|| maths_space()
|| generic_expression()
|| generic_literal()
|| simple_generic_expression() );
END_FUNCTION;
FUNCTION make_function_application
(afunction : maths_function_select; arguments : LIST[1:?] OF maths_value) : function_application;
RETURN (function_application (afunction, arguments)
|| multiple_arity_generic_expression (convert_to_maths_function (afunction) +
convert_to_operands (arguments)) -- derived
|| generic_expression() );
END_FUNCTION;
FUNCTION make_function_space
(domain_constraint : space_constraint_type; domain_argument : maths_space; range_constraint : space_constraint_type; range_argument : maths_space) : function_space;
RETURN (function_space (domain_constraint, domain_argument, range_constraint,
range_argument)
|| maths_space()
|| generic_expression()
|| generic_literal()
|| simple_generic_expression() );
END_FUNCTION;
FUNCTION make_general_linear_function
(mat : maths_function; sum_index : one_or_two) : general_linear_function;
RETURN (general_linear_function (sum_index)
|| maths_function()
|| generic_expression()
|| unary_generic_expression (mat) );
END_FUNCTION;
FUNCTION make_int_literal
(lit_value : INTEGER) : int_literal;
RETURN (int_literal ()
|| literal_number(lit_value)
|| simple_numeric_expression()
|| numeric_expression()
|| expression()
|| generic_expression()
|| simple_generic_expression()
|| generic_literal() );
END_FUNCTION;
FUNCTION make_integer_interval_from_min
(min : INTEGER) : integer_interval_from_min;
RETURN (integer_interval_from_min (min)
|| maths_space()
|| generic_expression()
|| generic_literal()
|| simple_generic_expression() );
END_FUNCTION;
FUNCTION make_listed_complex_number_data
(index_base : zero_or_one; values : LIST[2:?] OF REAL) : listed_complex_number_data;
RETURN (listed_complex_number_data (values)
|| explicit_table_function (index_base, [SIZEOF (values)/2]) -- 2nd derived
|| maths_function()
|| generic_expression()
|| generic_literal()
|| simple_generic_expression() );
END_FUNCTION;
FUNCTION make_listed_data
(index_base : zero_or_one; values : LIST[2:?] OF maths_value; value_range : maths_space) : listed_data;
RETURN (listed_data (values, value_range)
|| explicit_table_function (index_base, [SIZEOF (values)]) -- 2nd derived
|| maths_function()
|| generic_expression()
|| generic_literal()
|| simple_generic_expression() );
END_FUNCTION;
FUNCTION make_listed_integer_data
(index_base : zero_or_one; values : LIST[1:?] OF INTEGER) : listed_integer_data;
RETURN (listed_integer_data (values)
|| explicit_table_function (index_base, [SIZEOF (values)]) -- 2nd derived
|| maths_function()
|| generic_expression()
|| generic_literal()
|| simple_generic_expression() );
END_FUNCTION;
FUNCTION make_listed_product_space
(factors : LIST[0:?] OF maths_space) : listed_product_space;
RETURN (listed_product_space (factors)
|| maths_space()
|| generic_expression()
|| generic_literal()
|| simple_generic_expression() );
END_FUNCTION;
FUNCTION make_listed_real_data
(index_base : zero_or_one; values : LIST[1:?] OF REAL) : listed_real_data;
RETURN (listed_real_data (values)
|| explicit_table_function (index_base, [SIZEOF (values)]) -- 2nd derived
|| maths_function()
|| generic_expression()
|| generic_literal()
|| simple_generic_expression() );
END_FUNCTION;
FUNCTION make_logical_literal
(lit_value : LOGICAL) : logical_literal;
RETURN (logical_literal (lit_value)
|| generic_literal()
|| simple_generic_expression()
|| generic_expression() );
END_FUNCTION;
FUNCTION make_maths_enum_literal
(lit_value : maths_enum_atom) : maths_enum_literal;
RETURN (maths_enum_literal (lit_value)
|| generic_literal()
|| simple_generic_expression()
|| generic_expression() );
END_FUNCTION;
FUNCTION make_maths_real_variable
(values_space : maths_space; name : label) : maths_real_variable;
RETURN (expression() || numeric_expression() || simple_numeric_expression()
|| maths_real_variable()
|| maths_variable (values_space, name)
|| generic_variable()
|| simple_generic_expression()
|| generic_expression()
|| real_numeric_variable()
|| numeric_variable()
|| variable() );
END_FUNCTION;
FUNCTION make_maths_tuple_literal
(lit_value : LIST[0:?] OF maths_value) : maths_tuple_literal;
RETURN (maths_tuple_literal (lit_value)
|| generic_literal()
|| simple_generic_expression()
|| generic_expression() );
END_FUNCTION;
FUNCTION make_mult_expression
(operands : LIST[2:?] OF generic_expression) : mult_expression;
RETURN (mult_expression()
|| multiple_arity_numeric_expression()
|| numeric_expression()
|| expression()
|| generic_expression()
|| multiple_arity_generic_expression (operands) );
END_FUNCTION;
FUNCTION make_parallel_composed_function
(srcdom : maths_space_or_function; prepfuncs : LIST[2:?] OF maths_function; finfunc : maths_function_select) : parallel_composed_function;
RETURN (parallel_composed_function (srcdom, prepfuncs, finfunc)
|| maths_function()
|| generic_expression()
|| multiple_arity_generic_expression (convert_to_operands_prcmfn (
srcdom, prepfuncs, finfunc)) );
END_FUNCTION;
FUNCTION make_partial_derivative_expression
(derivand : generic_expression; dvars : LIST[1:?] OF maths_variable; extend : extension_options) : partial_derivative_expression;
RETURN (partial_derivative_expression (dvars, extend)
|| unary_generic_expression (derivand)
|| generic_expression() );
END_FUNCTION;
FUNCTION make_partial_derivative_function
(derivand : maths_function; dvars : LIST[1:?] OF input_selector; extend : extension_options) : partial_derivative_function;
RETURN (partial_derivative_function (dvars, extend)
|| maths_function()
|| generic_expression()
|| unary_generic_expression (derivand) );
END_FUNCTION;
FUNCTION make_polar_complex_number_region
(centre : complex_number_literal; dis_constraint : real_interval; dir_constraint : finite_real_interval) : polar_complex_number_region;
RETURN (polar_complex_number_region (centre, dis_constraint, dir_constraint)
|| maths_space()
|| generic_expression()
|| generic_literal()
|| simple_generic_expression() );
END_FUNCTION;
FUNCTION make_rationalize_function
(fun : maths_function) : rationalize_function;
RETURN (rationalize_function()
|| maths_function()
|| generic_expression()
|| unary_generic_expression (fun) );
END_FUNCTION;
FUNCTION make_real_interval_from_min
(min : REAL; minclo : open_closed) : real_interval_from_min;
RETURN (real_interval_from_min (min, minclo)
|| maths_space()
|| generic_expression()
|| generic_literal()
|| simple_generic_expression() );
END_FUNCTION;
FUNCTION make_real_interval_to_max
(max : REAL; maxclo : open_closed) : real_interval_to_max;
RETURN (real_interval_to_max (max, maxclo)
|| maths_space()
|| generic_expression()
|| generic_literal()
|| simple_generic_expression() );
END_FUNCTION;
FUNCTION make_real_literal
(lit_value : REAL) : real_literal;
RETURN (real_literal ()
|| literal_number(lit_value)
|| simple_numeric_expression()
|| numeric_expression()
|| expression()
|| generic_expression()
|| simple_generic_expression()
|| generic_literal() );
END_FUNCTION;
FUNCTION make_regular_table_function
(index_base : zero_or_one; shape : LIST[1:?] OF positive_integer; operand : maths_function; first : INTEGER; increments : LIST[1:?] OF INTEGER) : regular_table_function;
RETURN (regular_table_function (increments)
|| linearized_table_function (first)
|| explicit_table_function (index_base, shape)
|| maths_function()
|| generic_expression()
|| unary_generic_expression (operand) );
END_FUNCTION;
FUNCTION make_reindexed_array_function
(func : maths_function; start_idxs : LIST[1:?] OF INTEGER) : reindexed_array_function;
RETURN (reindexed_array_function(start_idxs)
|| maths_function()
|| generic_expression()
|| unary_generic_expression (func) );
END_FUNCTION;
FUNCTION make_repackaging_function
(operand : maths_function; input_repack : repackage_options; output_repack : repackage_options; selected_output : nonnegative_integer) : repackaging_function;
RETURN (repackaging_function (input_repack, output_repack, selected_output)
|| maths_function()
|| generic_expression()
|| unary_generic_expression (operand) );
END_FUNCTION;
FUNCTION make_selector_function
(selector : input_selector; src_of_domn : maths_space_or_function) : selector_function;
RETURN (selector_function (selector, src_of_domn)
|| maths_function()
|| generic_expression()
|| generic_literal()
|| simple_generic_expression() );
END_FUNCTION;
FUNCTION make_series_composed_function
(functions : LIST[2:?] OF maths_function) : series_composed_function;
RETURN (series_composed_function()
|| maths_function()
|| generic_expression()
|| multiple_arity_generic_expression (functions) );
END_FUNCTION;
FUNCTION make_sin_expression
(operand : numeric_expression) : sin_function;
RETURN (sin_expression()
|| unary_numeric_call_expression()
|| unary_numeric_expression()
|| numeric_expression()
|| expression()
|| generic_expression()
|| unary_generic_expression (operand) );
END_FUNCTION;
FUNCTION make_standard_table_function
(index_base : zero_or_one; shape : LIST[1:?] OF positive_integer; operand : maths_function; first : INTEGER; order : ordering_type) : standard_table_function;
RETURN (standard_table_function (order)
|| linearized_table_function (first)
|| explicit_table_function (index_base, shape)
|| maths_function()
|| generic_expression()
|| unary_generic_expression (operand) );
END_FUNCTION;
FUNCTION make_strict_triangular_matrix
(index_base : zero_or_one; shape : LIST[1:?] OF positive_integer; source : maths_function; first : INTEGER; default_entry : maths_value; lo_up : lower_upper; order : ordering_type; main_diagonal_value : maths_value) : strict_triangular_matrix;
RETURN (strict_triangular_matrix (main_diagonal_value)
|| triangular_matrix (default_entry, lo_up, order)
|| linearized_table_function (first)
|| explicit_table_function (index_base, shape)
|| maths_function()
|| generic_expression()
|| unary_generic_expression (source) );
END_FUNCTION;
FUNCTION make_string_literal
(lit_value : STRING) : string_literal;
RETURN (string_literal (lit_value)
|| simple_string_expression()
|| string_expression()
|| expression()
|| generic_expression()
|| simple_generic_expression()
|| generic_literal() );
END_FUNCTION;
FUNCTION make_unary_minus_expression
(operand : numeric_expression) : minus_function;
RETURN (unary_minus_expression()
|| unary_numeric_call_expression()
|| unary_numeric_expression()
|| numeric_expression()
|| expression()
|| generic_expression()
|| unary_generic_expression (operand) );
END_FUNCTION;
FUNCTION make_uniform_product_space
(base : maths_space; exponent : positive_integer) : uniform_product_space;
RETURN (uniform_product_space (base, exponent)
|| maths_space()
|| generic_expression()
|| generic_literal()
|| simple_generic_expression() );
END_FUNCTION;
FUNCTION max_exists
(spc : maths_space) : BOOLEAN;
LOCAL
types : SET OF STRING := TYPEOF (spc);
END_LOCAL;
RETURN (bool(((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN types) OR
((schema_prefix + 'INTEGER_INTERVAL_TO_MAX') IN types) OR
((schema_prefix + 'FINITE_REAL_INTERVAL') IN types) OR
((schema_prefix + 'REAL_INTERVAL_TO_MAX') IN types)));
END_FUNCTION;
FUNCTION max_included
(spc : maths_space) : BOOLEAN;
LOCAL
types : SET OF STRING := TYPEOF (spc);
END_LOCAL;
IF ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN types) OR
((schema_prefix + 'INTEGER_INTERVAL_TO_MAX') IN types) THEN
RETURN (TRUE);
END_IF;
IF ((schema_prefix + 'FINITE_REAL_INTERVAL') IN types) THEN
RETURN (bool(spc\finite_real_interval.max_closure = closed));
END_IF;
IF ((schema_prefix + 'REAL_INTERVAL_TO_MAX') IN types) THEN
RETURN (bool(spc\real_interval_to_max.max_closure = closed));
END_IF;
RETURN (FALSE);
END_FUNCTION;
FUNCTION member_of
(val : GENERIC : G; spc : maths_space) : LOGICAL;
FUNCTION fedex(val : AGGREGATE OF GENERIC:X;
i : INTEGER) : GENERIC:X;
RETURN (val[i]);
END_FUNCTION; -- fedex
LOCAL
v : maths_value := simplify_maths_value (convert_to_maths_value (val));
vtypes : SET OF STRING := stripped_typeof (v);
s : maths_space := simplify_maths_space (spc);
stypes : SET OF STRING := stripped_typeof (s);
tmp_int : INTEGER;
tmp_real : REAL;
tmp_cmplx : complex_number_literal;
lgcl, cum : LOGICAL;
vspc, sspc : maths_space;
smem : SET OF maths_value;
factors : LIST OF maths_space;
END_LOCAL;
IF NOT EXISTS (s) THEN
RETURN (FALSE);
END_IF;
IF NOT EXISTS (v) THEN
RETURN (s = the_generics);
END_IF;
IF ('GENERIC_EXPRESSION' IN vtypes) AND
NOT ('MATHS_SPACE' IN vtypes) AND
NOT ('MATHS_FUNCTION' IN vtypes) AND
NOT ('COMPLEX_NUMBER_LITERAL' IN vtypes) THEN
IF has_values_space (v) THEN
vspc := values_space_of (v);
IF subspace_of (vspc, s) THEN
RETURN (TRUE);
END_IF;
IF NOT compatible_spaces (vspc, s) THEN
RETURN (FALSE);
END_IF;
RETURN (UNKNOWN);
END_IF;
RETURN (UNKNOWN);
END_IF;
IF 'ELEMENTARY_SPACE' IN stypes THEN
CASE s\elementary_space.space_id OF
es_numbers : RETURN (('NUMBER' IN vtypes) OR
('COMPLEX_NUMBER_LITERAL' IN vtypes));
es_complex_numbers : RETURN ('COMPLEX_NUMBER_LITERAL' IN vtypes);
es_reals : RETURN (('REAL' IN vtypes) AND NOT ('INTEGER' IN vtypes));
es_integers : RETURN ('INTEGER' IN vtypes);
es_logicals : RETURN ('LOGICAL' IN vtypes);
es_booleans : RETURN ('BOOLEAN' IN vtypes);
es_strings : RETURN ('STRING' IN vtypes);
es_binarys : RETURN ('BINARY' IN vtypes);
es_maths_spaces : RETURN ('MATHS_SPACE' IN vtypes);
es_maths_functions : RETURN ('MATHS_FUNCTION' IN vtypes);
es_generics : RETURN (TRUE);
END_CASE;
END_IF;
IF 'FINITE_INTEGER_INTERVAL' IN stypes THEN
IF 'INTEGER' IN vtypes THEN
tmp_int := v;
RETURN ({s\finite_integer_interval.min <= tmp_int <=
s\finite_integer_interval.max});
END_IF;
RETURN (FALSE);
END_IF;
IF 'INTEGER_INTERVAL_FROM_MIN' IN stypes THEN
IF 'INTEGER' IN vtypes THEN
tmp_int := v;
RETURN (s\integer_interval_from_min.min <= tmp_int);
END_IF;
RETURN (FALSE);
END_IF;
IF 'INTEGER_INTERVAL_TO_MAX' IN stypes THEN
IF 'INTEGER' IN vtypes THEN
tmp_int := v;
RETURN (tmp_int <= s\integer_interval_to_max.max);
END_IF;
RETURN (FALSE);
END_IF;
IF 'FINITE_REAL_INTERVAL' IN stypes THEN
IF ('REAL' IN vtypes) AND NOT ('INTEGER' IN vtypes) THEN
tmp_real := v;
IF s\finite_real_interval.min_closure = closed THEN
IF s\finite_real_interval.max_closure = closed THEN
RETURN ({s\finite_real_interval.min <= tmp_real <=
s\finite_real_interval.max});
ELSE
RETURN ({s\finite_real_interval.min <= tmp_real <
s\finite_real_interval.max});
END_IF;
ELSE
IF s\finite_real_interval.max_closure = closed THEN
RETURN ({s\finite_real_interval.min < tmp_real <=
s\finite_real_interval.max});
ELSE
RETURN ({s\finite_real_interval.min < tmp_real <
s\finite_real_interval.max});
END_IF;
END_IF;
END_IF;
RETURN (FALSE);
END_IF;
IF 'REAL_INTERVAL_FROM_MIN' IN stypes THEN
IF ('REAL' IN vtypes) AND NOT ('INTEGER' IN vtypes) THEN
tmp_real := v;
IF s\real_interval_from_min.min_closure = closed THEN
RETURN (s\real_interval_from_min.min <= tmp_real);
ELSE
RETURN (s\real_interval_from_min.min < tmp_real);
END_IF;
END_IF;
RETURN (FALSE);
END_IF;
IF 'REAL_INTERVAL_TO_MAX' IN stypes THEN
IF ('REAL' IN vtypes) AND NOT ('INTEGER' IN vtypes) THEN
tmp_real := v;
IF s\real_interval_to_max.max_closure = closed THEN
RETURN (tmp_real <= s\real_interval_to_max.max);
ELSE
RETURN (tmp_real < s\real_interval_to_max.max);
END_IF;
END_IF;
RETURN (FALSE);
END_IF;
IF 'CARTESIAN_COMPLEX_NUMBER_REGION' IN stypes THEN
IF 'COMPLEX_NUMBER_LITERAL' IN vtypes THEN
RETURN (member_of(v\complex_number_literal.real_part,
s\cartesian_complex_number_region.real_constraint) AND
member_of(v\complex_number_literal.imag_part,
s\cartesian_complex_number_region.imag_constraint));
END_IF;
RETURN (FALSE);
END_IF;
IF 'POLAR_COMPLEX_NUMBER_REGION' IN stypes THEN
IF 'COMPLEX_NUMBER_LITERAL' IN vtypes THEN
tmp_cmplx := v;
tmp_cmplx.real_part := tmp_cmplx.real_part -
s\polar_complex_number_region.centre.real_part;
tmp_cmplx.imag_part := tmp_cmplx.imag_part -
s\polar_complex_number_region.centre.imag_part;
tmp_real := SQRT (tmp_cmplx.real_part**2 + tmp_cmplx.imag_part**2);
IF NOT member_of(tmp_real,
s\polar_complex_number_region.distance_constraint) THEN
RETURN (FALSE);
END_IF;
IF tmp_real = 0.0 THEN
RETURN (TRUE); -- The centre has no direction.
END_IF;
tmp_real := atan2(tmp_cmplx.imag_part,tmp_cmplx.real_part);
RETURN (member_of(tmp_real,
s\polar_complex_number_region.direction_constraint) OR
member_of(tmp_real + 2.0*PI,
s\polar_complex_number_region.direction_constraint));
END_IF;
RETURN (FALSE);
END_IF;
IF 'FINITE_SPACE' IN stypes THEN
smem := s\finite_space.members;
cum := FALSE;
REPEAT i := 1 TO SIZEOF (smem);
cum := cum OR equal_maths_values(v,smem[i]);
IF cum = TRUE THEN
RETURN (TRUE);
END_IF;
END_REPEAT;
RETURN (cum);
END_IF;
IF 'UNIFORM_PRODUCT_SPACE' IN stypes THEN
IF 'LIST' IN vtypes THEN
IF SIZEOF (v) = s\uniform_product_space.exponent THEN
sspc := s\uniform_product_space.base;
cum := TRUE;
REPEAT i := 1 TO SIZEOF (v);
cum := cum AND member_of(v[i],sspc);
-- cum := cum AND member_of (fedex (v, i), sspc);
-- See note above for explanation of fedex()
IF cum = FALSE THEN
RETURN (FALSE);
END_IF;
END_REPEAT;
RETURN (cum);
END_IF;
END_IF;
RETURN (FALSE);
END_IF;
IF 'LISTED_PRODUCT_SPACE' IN stypes THEN
IF 'LIST' IN vtypes THEN
factors := s\listed_product_space.factors;
IF SIZEOF (v) = SIZEOF (factors) THEN
cum := TRUE;
REPEAT i := 1 TO SIZEOF (v);
cum := cum AND member_of(v[i],factors[i]);
-- cum := cum AND member_of (fedex (v, i), factors[i]);
-- See note above for explanation of fedex()
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 stypes THEN
IF 'LIST' IN vtypes THEN
sspc := s\extended_tuple_space.base;
tmp_int := space_dimension(sspc);
IF SIZEOF (v) >= tmp_int THEN
cum := TRUE;
REPEAT i := 1 TO tmp_int;
cum := cum AND member_of(v[i],factor_space(sspc,i));
-- cum := cum AND member_of (fedex (v, i), factor_space (sspc, i));
-- See note above for explanation of fedex()
IF cum = FALSE THEN
RETURN (FALSE);
END_IF;
END_REPEAT;
sspc := s\extended_tuple_space.extender;
REPEAT i := tmp_int+1 TO SIZEOF (v);
cum := cum AND member_of(v[i],sspc);
IF cum = FALSE THEN
RETURN (FALSE);
END_IF;
END_REPEAT;
RETURN (cum);
END_IF;
END_IF;
RETURN (FALSE);
END_IF;
IF 'FUNCTION_SPACE' IN stypes THEN
IF 'MATHS_FUNCTION' IN vtypes THEN
vspc := v\maths_function.domain;
sspc := s\function_space.domain_argument;
CASE s\function_space.domain_constraint OF
sc_equal : cum := equal_maths_spaces (vspc, sspc);
sc_subspace : cum := subspace_of (vspc, sspc);
sc_member : cum := member_of (vspc, sspc);
END_CASE;
IF cum = FALSE THEN
RETURN (FALSE);
END_IF;
vspc := v\maths_function.range;
sspc := s\function_space.range_argument;
CASE s\function_space.range_constraint OF
sc_equal : cum := cum AND equal_maths_spaces (vspc, sspc);
sc_subspace : cum := cum AND subspace_of (vspc, sspc);
sc_member : cum := cum AND member_of (vspc, sspc);
END_CASE;
RETURN (cum);
END_IF;
RETURN (FALSE);
END_IF;
-- Should be unreachable
RETURN (UNKNOWN);
END_FUNCTION;
FUNCTION min_exists
(spc : maths_space) : BOOLEAN;
LOCAL
types : SET OF STRING := TYPEOF (spc);
END_LOCAL;
RETURN (bool(((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN types) OR
((schema_prefix + 'INTEGER_INTERVAL_FROM_MIN') IN types) OR
((schema_prefix + 'FINITE_REAL_INTERVAL') IN types) OR
((schema_prefix + 'REAL_INTERVAL_FROM_MIN') IN types)));
END_FUNCTION;
FUNCTION min_included
(spc : maths_space) : BOOLEAN;
LOCAL
types : SET OF STRING := TYPEOF (spc);
END_LOCAL;
IF ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN types) OR
((schema_prefix + 'INTEGER_INTERVAL_FROM_MIN') IN types) THEN
RETURN (TRUE);
END_IF;
IF ((schema_prefix + 'FINITE_REAL_INTERVAL') IN types) THEN
RETURN (bool(spc\finite_real_interval.min_closure = closed));
END_IF;
IF ((schema_prefix + 'REAL_INTERVAL_FROM_MIN') IN types) THEN
RETURN (bool(spc\real_interval_from_min.min_closure = closed));
END_IF;
RETURN (FALSE);
END_FUNCTION;
FUNCTION no_cyclic_domain_reference
(ref : maths_space_or_function; used : SET[0:?] OF maths_function) : BOOLEAN;
LOCAL
typenames : SET OF STRING := TYPEOF (ref);
func : maths_function;
END_LOCAL;
IF (NOT EXISTS (ref)) OR (NOT EXISTS (used)) THEN
RETURN (FALSE);
END_IF;
IF (schema_prefix + 'MATHS_SPACE') IN typenames THEN
RETURN (TRUE);
END_IF;
func := ref;
IF func IN used THEN
RETURN (FALSE);
END_IF;
IF (schema_prefix + 'CONSTANT_FUNCTION') IN typenames THEN
RETURN (no_cyclic_domain_reference (func\constant_function.source_of_domain,
used + [func]));
END_IF;
IF (schema_prefix + 'SELECTOR_FUNCTION') IN typenames THEN
RETURN (no_cyclic_domain_reference (func\selector_function.source_of_domain,
used + [func]));
END_IF;
IF (schema_prefix + 'PARALLEL_COMPOSED_FUNCTION') IN typenames THEN
RETURN (no_cyclic_domain_reference (
func\parallel_composed_function.source_of_domain, used + [func]));
END_IF;
RETURN (TRUE);
END_FUNCTION;
FUNCTION no_cyclic_space_reference
(spc : maths_space; refs : SET[0:?] OF maths_space) : BOOLEAN;
LOCAL
types : SET OF STRING;
refs_plus : SET OF maths_space;
END_LOCAL;
IF (spc IN refs) THEN
RETURN (FALSE);
END_IF;
types := TYPEOF (spc);
refs_plus := refs + spc;
IF (schema_prefix + 'FINITE_SPACE') IN types THEN
RETURN (bool(SIZEOF (QUERY (sp <* QUERY (mem <* spc\finite_space.members |
(schema_prefix + 'MATHS_SPACE') IN TYPEOF (mem)) |
NOT no_cyclic_space_reference (sp, refs_plus))) = 0));
END_IF;
IF (schema_prefix + 'UNIFORM_PRODUCT_SPACE') IN types THEN
RETURN (no_cyclic_space_reference (spc\uniform_product_space.base, refs_plus));
END_IF;
IF (schema_prefix + 'LISTED_PRODUCT_SPACE') IN types THEN
RETURN (bool(SIZEOF (QUERY (fac <* spc\listed_product_space.factors |
NOT no_cyclic_space_reference (fac, refs_plus))) = 0));
END_IF;
IF (schema_prefix + 'EXTENDED_TUPLE_SPACE') IN types THEN
RETURN (no_cyclic_space_reference (spc\extended_tuple_space.base, refs_plus)
AND no_cyclic_space_reference (spc\extended_tuple_space.extender, refs_plus));
END_IF;
-- spc contains no references to other spaces
RETURN (TRUE);
END_FUNCTION;
FUNCTION nondecreasing
(lr : LIST[0:?] OF REAL) : BOOLEAN;
IF NOT EXISTS (lr) THEN
RETURN (FALSE);
END_IF;
REPEAT j := 2 TO SIZEOF (lr);
IF lr[j] < lr[j-1] THEN
RETURN (FALSE);
END_IF;
END_REPEAT;
RETURN (TRUE);
END_FUNCTION;
FUNCTION number_superspace_of
(spc : maths_space) : elementary_space;
IF subspace_of_es(spc,es_integers) THEN RETURN (the_integers); END_IF;
IF subspace_of_es(spc,es_reals) THEN RETURN (the_reals); END_IF;
IF subspace_of_es(spc,es_complex_numbers) THEN RETURN (the_complex_numbers); END_IF;
IF subspace_of_es(spc,es_numbers) THEN RETURN (the_numbers); END_IF;
RETURN (?);
END_FUNCTION;
FUNCTION number_tuple_subspace_check
(spc : maths_space) : LOGICAL;
LOCAL
types : SET OF STRING := stripped_typeof(spc);
factors : LIST OF maths_space;
cum : LOGICAL := TRUE;
END_LOCAL;
IF 'UNIFORM_PRODUCT_SPACE' IN types THEN
RETURN (subspace_of_es(spc\uniform_product_space.base,es_numbers));
END_IF;
IF 'LISTED_PRODUCT_SPACE' IN types THEN
factors := spc\listed_product_space.factors;
REPEAT i := 1 TO SIZEOF (factors);
cum := cum AND subspace_of_es(factors[i],es_numbers);
END_REPEAT;
RETURN (cum);
END_IF;
IF 'EXTENDED_TUPLE_SPACE' IN types THEN
cum := subspace_of_es(spc\extended_tuple_space.extender,es_numbers);
cum := cum AND number_tuple_subspace_check(spc\extended_tuple_space.base);
RETURN (cum);
END_IF;
RETURN (FALSE);
END_FUNCTION;
FUNCTION one_tuples_of
(spc : maths_space) : tuple_space;
RETURN (make_uniform_product_space (spc, 1));
END_FUNCTION;
FUNCTION parallel_composed_function_composability_check
(funcs : LIST[0:?] OF maths_function; final : maths_function_select) : BOOLEAN;
LOCAL
tplsp : tuple_space := the_zero_tuple_space;
finfun : maths_function := convert_to_maths_function (final);
END_LOCAL;
REPEAT i := 1 TO SIZEOF (funcs);
tplsp := assoc_product_space (tplsp, funcs[i].range);
END_REPEAT;
RETURN (compatible_spaces (tplsp, finfun.domain));
END_FUNCTION;
FUNCTION parallel_composed_function_domain_check
(comdom : tuple_space; funcs : LIST[0:?] OF maths_function) : BOOLEAN;
REPEAT i := 1 TO SIZEOF (funcs);
IF NOT (compatible_spaces (comdom, funcs[i].domain)) THEN
RETURN (FALSE);
END_IF;
END_REPEAT;
RETURN (TRUE);
END_FUNCTION;
FUNCTION parse_express_identifier
(s : STRING; i : positive_integer) : positive_integer;
LOCAL
k : positive_integer;
END_LOCAL;
k := i;
IF i <= LENGTH (s) THEN
IF (s[i] LIKE '@') THEN
REPEAT UNTIL (k > LENGTH (s)) OR
((s[k] <> '_') AND NOT (s[k] LIKE '@') AND NOT (s[k] LIKE '#'));
k := k + 1;
END_REPEAT;
END_IF;
END_IF;
RETURN (k);
END_FUNCTION;
FUNCTION partial_derivative_check
(domain : tuple_space; d_vars : LIST[1:?] OF input_selector) : BOOLEAN;
LOCAL
domn : tuple_space := domain;
fspc : maths_space;
dim : INTEGER;
k : INTEGER;
END_LOCAL;
IF (space_dimension (domain) = 1) AND ((schema_prefix + 'TUPLE_SPACE') IN
TYPEOF (factor1 (domain))) THEN
domn := factor1 (domain);
END_IF;
dim := space_dimension (domn);
REPEAT i := 1 TO SIZEOF (d_vars);
k := d_vars[i];
IF k > dim THEN
RETURN (FALSE);
END_IF;
fspc := factor_space (domn, k);
IF (NOT subspace_of_es (fspc,es_reals)) AND
(NOT subspace_of_es (fspc,es_complex_numbers)) THEN
RETURN (FALSE);
END_IF;
END_REPEAT;
RETURN (TRUE);
END_FUNCTION;
FUNCTION real_max
(spc : maths_space) : REAL;
LOCAL
types : SET OF STRING := TYPEOF (spc);
END_LOCAL;
IF ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN types) THEN
RETURN (spc\finite_integer_interval.max);
END_IF;
IF ((schema_prefix + 'INTEGER_INTERVAL_TO_MAX') IN types) THEN
RETURN (spc\integer_interval_to_max.max);
END_IF;
IF ((schema_prefix + 'FINITE_REAL_INTERVAL') IN types) THEN
RETURN (spc\finite_real_interval.max);
END_IF;
IF ((schema_prefix + 'REAL_INTERVAL_TO_MAX') IN types) THEN
RETURN (spc\real_interval_to_max.max);
END_IF;
RETURN (?);
END_FUNCTION;
FUNCTION real_min
(spc : maths_space) : REAL;
LOCAL
types : SET OF STRING := TYPEOF (spc);
END_LOCAL;
IF ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN types) THEN
RETURN (spc\finite_integer_interval.min);
END_IF;
IF ((schema_prefix + 'INTEGER_INTERVAL_FROM_MIN') IN types) THEN
RETURN (spc\integer_interval_from_min.min);
END_IF;
IF ((schema_prefix + 'FINITE_REAL_INTERVAL') IN types) THEN
RETURN (spc\finite_real_interval.min);
END_IF;
IF ((schema_prefix + 'REAL_INTERVAL_FROM_MIN') IN types) THEN
RETURN (spc\real_interval_from_min.min);
END_IF;
RETURN (?);
END_FUNCTION;
FUNCTION regular_indexing
(sub : LIST[0:?] OF INTEGER; base : zero_or_one; shape : LIST[1:?] OF positive_integer; inc : LIST[1:?] OF INTEGER; first : INTEGER) : INTEGER;
LOCAL
k : INTEGER;
index : INTEGER;
END_LOCAL;
IF NOT EXISTS (sub) OR NOT EXISTS (base) OR NOT EXISTS (shape) OR
NOT EXISTS (inc) OR NOT EXISTS (first) THEN
RETURN (?);
END_IF;
IF (SIZEOF (sub) <> SIZEOF (inc)) OR (SIZEOF (sub) <> SIZEOF (shape)) THEN
RETURN (?);
END_IF;
index := first;
REPEAT j := 1 TO SIZEOF (sub);
IF NOT EXISTS (sub[j]) OR NOT EXISTS (inc[j]) THEN
RETURN (?);
END_IF;
k := sub[j] - base;
IF NOT ({0 <= k < shape[j]}) THEN
RETURN (?);
END_IF;
index := index + k*inc[j];
END_REPEAT;
RETURN (index);
END_FUNCTION;
FUNCTION remove_first
(alist : LIST[0:?] OF GENERIC : GEN) : LIST[0:?] OF GENERIC : GEN;
LOCAL
blist : LIST OF GENERIC:GEN := alist;
END_LOCAL;
IF SIZEOF (blist) > 0 THEN
REMOVE (blist, 1);
END_IF;
RETURN (blist);
END_FUNCTION;
FUNCTION repackage
(tspace : tuple_space; repckg : repackage_options) : tuple_space;
CASE repckg OF
ro_nochange : RETURN (tspace);
ro_wrap_as_tuple : RETURN (one_tuples_of (tspace));
ro_unwrap_tuple : RETURN (factor1 (tspace));
OTHERWISE : RETURN (?);
END_CASE;
END_FUNCTION;
FUNCTION shape_of_array
(func : maths_function) : LIST[0:?] OF positive_integer;
LOCAL
tspace : tuple_space;
temp : maths_space;
result : LIST OF positive_integer := [];
END_LOCAL;
IF (schema_prefix + 'EXPLICIT_TABLE_FUNCTION') IN TYPEOF (func) THEN
RETURN (func\explicit_table_function.shape);
END_IF;
tspace := func.domain;
IF (space_dimension (tspace) = 1) AND ((schema_prefix + 'TUPLE_SPACE') IN
TYPEOF (factor1 (tspace))) THEN
tspace := factor1 (tspace);
END_IF;
REPEAT i := 1 TO space_dimension (tspace);
temp := factor_space (tspace, i);
IF NOT ((schema_prefix + 'FINITE_INTEGER_INTERVAL') IN TYPEOF (temp)) THEN
RETURN (?);
END_IF;
INSERT (result, temp\finite_integer_interval.size, i-1);
END_REPEAT;
RETURN (result);
END_FUNCTION;
FUNCTION simplify_function_application
(expr : function_application) : maths_value;
FUNCTION ctmv(x : GENERIC:G) : maths_value;
RETURN (convert_to_maths_value(x));
END_FUNCTION; -- local abbreviation for convert_to_maths_value function
PROCEDURE parts( c : complex_number_literal;
VAR x, y : REAL);
x := c.real_part; y := c.imag_part;
END_PROCEDURE; -- parts
FUNCTION makec(x, y : REAL) : complex_number_literal;
RETURN (make_complex_number_literal(x,y));
END_FUNCTION; -- local abbreviation for make_complex_number_literal function
FUNCTION good_t(v : maths_value;
tn : STRING) : BOOLEAN;
LOCAL
tpl : LIST OF maths_value;
END_LOCAL;
IF 'LIST' IN TYPEOF (v) THEN
tpl := v;
REPEAT i := 1 TO SIZEOF (tpl);
IF NOT (tn IN TYPEOF (tpl[i])) THEN RETURN (FALSE); END_IF;
END_REPEAT;
RETURN (TRUE);
END_IF;
RETURN (FALSE);
END_FUNCTION; -- good_t
CONSTANT
cnlit : STRING := schema_prefix + 'COMPLEX_NUMBER_LITERAL';
END_CONSTANT;
LOCAL
types : SET OF STRING := stripped_typeof(expr.func);
ef_val : elementary_function_enumerators;
is_elementary : BOOLEAN := FALSE;
v, v1, v2, v3 : maths_value;
vlist : LIST OF maths_value := [];
gexpr : generic_expression;
pairs : SET [1:?] OF LIST [2:2] OF maths_value;
boo : BOOLEAN;
lgc, cum : LOGICAL;
j, k, n : INTEGER;
p, q, r, s, t, u : REAL;
str, st2 : STRING;
bin, bi2 : BINARY;
tpl, tp2 : LIST OF maths_value;
mem :SET OF maths_value := [];
END_LOCAL;
REPEAT i := 1 TO SIZEOF (expr.arguments);
v := simplify_maths_value(expr.arguments[i]);
INSERT (vlist, v, i-1);
END_REPEAT;
IF SIZEOF (vlist) >= 1 THEN v1 := vlist[1]; END_IF;
IF SIZEOF (vlist) >= 2 THEN v2 := vlist[2]; END_IF;
IF SIZEOF (vlist) >= 3 THEN v3 := vlist[3]; END_IF;
IF 'ELEMENTARY_FUNCTION_ENUMERATORS' IN types THEN
ef_val := expr.func;
is_elementary := TRUE;
END_IF;
IF 'ELEMENTARY_FUNCTION' IN types THEN
ef_val := expr.func\elementary_function.func_id;
is_elementary := TRUE;
END_IF;
IF is_elementary THEN
CASE ef_val OF
ef_and : BEGIN
cum := TRUE;
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF 'LOGICAL' IN TYPEOF (vlist[i]) THEN
lgc := vlist[i]; cum := cum AND lgc;
IF lgc = FALSE THEN RETURN (ctmv(FALSE)); END_IF;
REMOVE (vlist, i);
END_IF;
END_REPEAT;
IF SIZEOF (vlist) = 0 THEN RETURN (ctmv(cum)); END_IF;
IF cum <> TRUE THEN INSERT (vlist, ctmv(cum), 0); END_IF;
IF SIZEOF (vlist) = 1 THEN RETURN (vlist[1]); END_IF;
END;
ef_or : BEGIN
cum := FALSE;
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF 'LOGICAL' IN TYPEOF (vlist[i]) THEN
lgc := vlist[i]; cum := cum OR lgc;
IF lgc = TRUE THEN RETURN (ctmv(TRUE)); END_IF;
REMOVE (vlist, i);
END_IF;
END_REPEAT;
IF SIZEOF (vlist) = 0 THEN RETURN (ctmv(cum)); END_IF;
IF cum <> FALSE THEN INSERT (vlist, ctmv(cum), 0); END_IF;
IF SIZEOF (vlist) = 1 THEN RETURN (vlist[1]); END_IF;
END;
ef_not :
IF 'LOGICAL' IN TYPEOF (v1) THEN lgc := v1; RETURN (ctmv(NOT lgc)); END_IF;
ef_xor : BEGIN
IF 'LOGICAL' IN TYPEOF (v1) THEN
lgc := v1;
IF 'LOGICAL' IN TYPEOF (v2) THEN cum := v2; RETURN (ctmv(lgc XOR cum));
ELSE IF lgc = FALSE THEN RETURN (ctmv(v2));
ELSE IF lgc = UNKNOWN THEN RETURN (ctmv(UNKNOWN));
ELSE RETURN (make_function_application(ef_not,[v2]));
END_IF; END_IF; END_IF;
ELSE IF 'LOGICAL' IN TYPEOF (v2) THEN
lgc := v2;
IF lgc = FALSE THEN RETURN (ctmv(v1));
ELSE IF lgc = UNKNOWN THEN RETURN (ctmv(UNKNOWN));
ELSE RETURN (make_function_application(ef_not,[v1]));
END_IF; END_IF;
END_IF; END_IF;
END;
ef_negate_i :
IF 'INTEGER' IN TYPEOF (v1) THEN j := v1; RETURN (ctmv(-j)); END_IF;
ef_add_i : BEGIN
j := 0;
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF 'INTEGER' IN TYPEOF (vlist[i]) THEN
k := vlist[i]; j := j + k;
REMOVE (vlist, i);
END_IF;
END_REPEAT;
IF SIZEOF (vlist) = 0 THEN RETURN (ctmv(j)); END_IF;
IF j <> 0 THEN INSERT (vlist, ctmv(j), 0); END_IF;
IF SIZEOF (vlist) = 1 THEN RETURN (vlist[1]); END_IF;
END;
ef_subtract_i :
IF ('INTEGER' IN TYPEOF (v1)) AND ('INTEGER' IN TYPEOF (v2)) THEN
j := v1; k := v2; RETURN (ctmv(j - k));
END_IF;
ef_multiply_i : BEGIN
j := 1;
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF 'INTEGER' IN TYPEOF (vlist[i]) THEN
k := vlist[i]; j := j * k;
REMOVE (vlist, i);
END_IF;
END_REPEAT;
IF SIZEOF (vlist) = 0 THEN RETURN (ctmv(j)); END_IF;
IF j <> 1 THEN INSERT (vlist, ctmv(j), 0); END_IF;
IF SIZEOF (vlist) = 1 THEN RETURN (vlist[1]); END_IF;
END;
ef_divide_i :
IF ('INTEGER' IN TYPEOF (v1)) AND ('INTEGER' IN TYPEOF (v2)) THEN
j := v1; k := v2; RETURN (ctmv(j DIV k));
END_IF;
ef_mod_i :
IF ('INTEGER' IN TYPEOF (v1)) AND ('INTEGER' IN TYPEOF (v2)) THEN
j := v1; k := v2; RETURN (ctmv(j MOD k));
END_IF;
ef_exponentiate_i :
IF ('INTEGER' IN TYPEOF (v1)) AND ('INTEGER' IN TYPEOF (v2)) THEN
j := v1; k := v2; n := 1;
REPEAT i := 1 TO ABS(k); n := n * j; END_REPEAT;
IF k < 0 THEN n := 1 DIV n; END_IF;
RETURN (ctmv(n));
END_IF;
ef_eq_i :
IF ('INTEGER' IN TYPEOF (v1)) AND ('INTEGER' IN TYPEOF (v2)) THEN
j := v1; k := v2; RETURN (ctmv(j = k));
END_IF;
ef_ne_i :
IF ('INTEGER' IN TYPEOF (v1)) AND ('INTEGER' IN TYPEOF (v2)) THEN
j := v1; k := v2; RETURN (ctmv(j <> k));
END_IF;
ef_gt_i :
IF ('INTEGER' IN TYPEOF (v1)) AND ('INTEGER' IN TYPEOF (v2)) THEN
j := v1; k := v2; RETURN (ctmv(j > k));
END_IF;
ef_lt_i :
IF ('INTEGER' IN TYPEOF (v1)) AND ('INTEGER' IN TYPEOF (v2)) THEN
j := v1; k := v2; RETURN (ctmv(j < k));
END_IF;
ef_ge_i :
IF ('INTEGER' IN TYPEOF (v1)) AND ('INTEGER' IN TYPEOF (v2)) THEN
j := v1; k := v2; RETURN (ctmv(j >= k));
END_IF;
ef_le_i :
IF ('INTEGER' IN TYPEOF (v1)) AND ('INTEGER' IN TYPEOF (v2)) THEN
j := v1; k := v2; RETURN (ctmv(j <= k));
END_IF;
ef_abs_i :
IF 'INTEGER' IN TYPEOF (v1) THEN j := v1; RETURN (ctmv(ABS(j))); END_IF;
ef_max_i : BEGIN
boo := FALSE;
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF 'INTEGER' IN TYPEOF (vlist[i]) THEN
IF boo THEN k := vlist[i]; IF k > j THEN j := k; END_IF;
ELSE j := vlist[i]; boo := TRUE; END_IF;
REMOVE (vlist, i);
END_IF;
END_REPEAT;
IF SIZEOF (vlist) = 0 THEN RETURN (ctmv(j)); END_IF;
IF boo THEN INSERT (vlist, ctmv(j), 0); END_IF;
IF SIZEOF (vlist) = 1 THEN RETURN (vlist[1]); END_IF;
END;
ef_min_i : BEGIN
boo := FALSE;
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF 'INTEGER' IN TYPEOF (vlist[i]) THEN
IF boo THEN k := vlist[i]; IF k < j THEN j := k; END_IF;
ELSE j := vlist[i]; boo := TRUE; END_IF;
REMOVE (vlist, i);
END_IF;
END_REPEAT;
IF SIZEOF (vlist) = 0 THEN RETURN (ctmv(j)); END_IF;
IF boo THEN INSERT (vlist, ctmv(j), 0); END_IF;
IF SIZEOF (vlist) = 1 THEN RETURN (vlist[1]); END_IF;
END;
-- ef_if_i : combined with ef_if
ef_negate_r :
IF 'REAL' IN TYPEOF (v1) THEN r := v1; RETURN (ctmv(-r)); END_IF;
ef_reciprocal_r :
IF 'REAL' IN TYPEOF (v1) THEN r := v1; RETURN (ctmv(1.0/r)); END_IF;
ef_add_r : BEGIN
r := 0.0;
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF 'REAL' IN TYPEOF (vlist[i]) THEN
s := vlist[i]; r := r + s;
REMOVE (vlist, i);
END_IF;
END_REPEAT;
IF SIZEOF (vlist) = 0 THEN RETURN (ctmv(r)); END_IF;
IF r <> 0.0 THEN INSERT (vlist, ctmv(r), 0); END_IF;
IF SIZEOF (vlist) = 1 THEN RETURN (vlist[1]); END_IF;
END;
ef_subtract_r :
IF ('REAL' IN TYPEOF (v1)) AND ('REAL' IN TYPEOF (v2)) THEN
r := v1; s := v2; RETURN (ctmv(r - s));
END_IF;
ef_multiply_r : BEGIN
r := 1.0;
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF 'REAL' IN TYPEOF (vlist[i]) THEN
s := vlist[i]; r := r * s;
REMOVE (vlist, i);
END_IF;
END_REPEAT;
IF SIZEOF (vlist) = 0 THEN RETURN (ctmv(r)); END_IF;
IF r <> 1.0 THEN INSERT (vlist, ctmv(r), 0); END_IF;
IF SIZEOF (vlist) = 1 THEN RETURN (vlist[1]); END_IF;
END;
ef_divide_r :
IF ('REAL' IN TYPEOF (v1)) AND ('REAL' IN TYPEOF (v2)) THEN
r := v1; s := v2; RETURN (ctmv(r / s));
END_IF;
ef_mod_r :
IF ('REAL' IN TYPEOF (v1)) AND ('REAL' IN TYPEOF (v2)) THEN
r := v1; s := v2; t := r/s; j := t DIV 1;
IF (t < 0.0) AND (j <> t) THEN j := j - 1; END_IF;
RETURN (ctmv(r - j * s));
END_IF;
ef_exponentiate_r :
IF ('REAL' IN TYPEOF (v1)) AND ('REAL' IN TYPEOF (v2)) THEN
r := v1; s := v2; RETURN (ctmv(r ** s));
END_IF;
ef_exponentiate_ri :
IF ('REAL' IN TYPEOF (v1)) AND ('INTEGER' IN TYPEOF (v2)) THEN
r := v1; k := v2; t := 1.0;
REPEAT i := 1 TO ABS(k); t := t * r; END_REPEAT;
IF k < 0 THEN t := 1.0/t; END_IF;
RETURN (ctmv(t));
END_IF;
ef_eq_r :
IF ('REAL' IN TYPEOF (v1)) AND ('REAL' IN TYPEOF (v2)) THEN
r := v1; s := v2; RETURN (ctmv(r = s));
END_IF;
ef_ne_r :
IF ('REAL' IN TYPEOF (v1)) AND ('REAL' IN TYPEOF (v2)) THEN
r := v1; s := v2; RETURN (ctmv(r <> s));
END_IF;
ef_gt_r :
IF ('REAL' IN TYPEOF (v1)) AND ('REAL' IN TYPEOF (v2)) THEN
r := v1; s := v2; RETURN (ctmv(r > s));
END_IF;
ef_lt_r :
IF ('REAL' IN TYPEOF (v1)) AND ('REAL' IN TYPEOF (v2)) THEN
r := v1; s := v2; RETURN (ctmv(r < s));
END_IF;
ef_ge_r :
IF ('REAL' IN TYPEOF (v1)) AND ('REAL' IN TYPEOF (v2)) THEN
r := v1; s := v2; RETURN (ctmv(r >= s));
END_IF;
ef_le_r :
IF ('REAL' IN TYPEOF (v1)) AND ('REAL' IN TYPEOF (v2)) THEN
r := v1; s := v2; RETURN (ctmv(r <= s));
END_IF;
ef_abs_r :
IF 'REAL' IN TYPEOF (v1) THEN r := v1; RETURN (ctmv(ABS(r))); END_IF;
ef_max_r : BEGIN
boo := FALSE;
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF 'REAL' IN TYPEOF (vlist[i]) THEN
IF boo THEN s := vlist[i]; IF s > r THEN r := s; END_IF;
ELSE r := vlist[i]; boo := TRUE; END_IF;
REMOVE (vlist, i);
END_IF;
END_REPEAT;
IF SIZEOF (vlist) = 0 THEN RETURN (ctmv(r)); END_IF;
IF boo THEN INSERT (vlist, ctmv(r), 0); END_IF;
IF SIZEOF (vlist) = 1 THEN RETURN (vlist[1]); END_IF;
END;
ef_min_r : BEGIN
boo := FALSE;
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF 'REAL' IN TYPEOF (vlist[i]) THEN
IF boo THEN s := vlist[i]; IF s < r THEN r := s; END_IF;
ELSE r := vlist[i]; boo := TRUE; END_IF;
REMOVE (vlist, i);
END_IF;
END_REPEAT;
IF SIZEOF (vlist) = 0 THEN RETURN (ctmv(r)); END_IF;
IF boo THEN INSERT (vlist, ctmv(r), 0); END_IF;
IF SIZEOF (vlist) = 1 THEN RETURN (vlist[1]); END_IF;
END;
ef_acos_r :
IF 'REAL' IN TYPEOF (v1) THEN r := v1; RETURN (ctmv(ACOS(r))); END_IF;
ef_asin_r :
IF 'REAL' IN TYPEOF (v1) THEN r := v1; RETURN (ctmv(ASIN(r))); END_IF;
ef_atan2_r :
IF ('REAL' IN TYPEOF (v1)) AND ('REAL' IN TYPEOF (v2)) THEN
r := v1; s := v2; RETURN (ctmv(atan2(r,s)));
END_IF;
ef_cos_r :
IF 'REAL' IN TYPEOF (v1) THEN r := v1; RETURN (ctmv(COS(r))); END_IF;
ef_exp_r :
IF 'REAL' IN TYPEOF (v1) THEN r := v1; RETURN (ctmv(EXP(r))); END_IF;
ef_ln_r :
IF 'REAL' IN TYPEOF (v1) THEN r := v1; RETURN (ctmv(LOG(r))); END_IF;
ef_log2_r :
IF 'REAL' IN TYPEOF (v1) THEN r := v1; RETURN (ctmv(LOG2(r))); END_IF;
ef_log10_r :
IF 'REAL' IN TYPEOF (v1) THEN r := v1; RETURN (ctmv(LOG10(r))); END_IF;
ef_sin_r :
IF 'REAL' IN TYPEOF (v1) THEN r := v1; RETURN (ctmv(SIN(r))); END_IF;
ef_sqrt_r :
IF 'REAL' IN TYPEOF (v1) THEN r := v1; RETURN (ctmv(SQRT(r))); END_IF;
ef_tan_r :
IF 'REAL' IN TYPEOF (v1) THEN r := v1; RETURN (ctmv(TAN(r))); END_IF;
-- ef_if_r : combined with ef_if
ef_form_c :
IF ('REAL' IN TYPEOF (v1)) AND ('REAL' IN TYPEOF (v2)) THEN
r := v1; s := v2; RETURN (makec(r,s));
END_IF;
ef_rpart_c :
IF cnlit IN TYPEOF (v1) THEN
RETURN (ctmv(v1\complex_number_literal.real_part));
END_IF;
ef_ipart_c :
IF cnlit IN TYPEOF (v1) THEN
RETURN (ctmv(v1\complex_number_literal.imag_part));
END_IF;
ef_negate_c :
IF cnlit IN TYPEOF (v1) THEN parts(v1,p,q); RETURN (makec(-p,-q)); END_IF;
ef_reciprocal_c :
IF cnlit IN TYPEOF (v1) THEN
parts(v1,p,q); t := p*p + q*q; RETURN (makec(p/t,-q/t));
END_IF;
ef_add_c : BEGIN
p := 0.0; q := 0.0;
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF cnlit IN TYPEOF (vlist[i]) THEN
parts(vlist[i],r,s); p := p + r; q := q + s;
REMOVE (vlist, i);
END_IF;
END_REPEAT;
IF SIZEOF (vlist) = 0 THEN RETURN (makec(p,q)); END_IF;
IF p*p+q*q <> 0.0 THEN INSERT (vlist, makec(p,q), 0); END_IF;
IF SIZEOF (vlist) = 1 THEN RETURN (vlist[1]); END_IF;
END;
ef_subtract_c :
IF (cnlit IN TYPEOF (v1)) AND (cnlit IN TYPEOF (v2)) THEN
parts(v1,p,q); parts(v2,r,s); RETURN (makec(p-r,q-s));
END_IF;
ef_multiply_c : BEGIN
p := 1.0; q := 0.0;
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF cnlit IN TYPEOF (vlist[i]) THEN
parts(vlist[i],r,s); p := p*r-q*s; q := p*s+q*r;
REMOVE (vlist, i);
END_IF;
END_REPEAT;
IF SIZEOF (vlist) = 0 THEN RETURN (makec(p,q)); END_IF;
IF (p <> 1.0) OR (q <> 0.0) THEN INSERT (vlist, makec(p,q), 0); END_IF;
IF SIZEOF (vlist) = 1 THEN RETURN (vlist[1]); END_IF;
END;
ef_divide_c :
IF (cnlit IN TYPEOF (v1)) AND (cnlit IN TYPEOF (v2)) THEN
parts(v1,p,q); parts(v2,r,s); t := r*r+s*s;
RETURN (makec((p*r+q*s)/t,(q*r-p*s)/t));
END_IF;
ef_exponentiate_c :
IF (cnlit IN TYPEOF (v1)) AND (cnlit IN TYPEOF (v2)) THEN
parts(v1,p,q); parts(v2,r,s); t := 0.5*LOG(p*p+q*q); u := atan2(q,p);
p := r*t-s*u; q := r*u+s*t; r := EXP(p);
RETURN (makec(r*COS(q),r*SIN(q)));
END_IF;
ef_exponentiate_ci :
IF (cnlit IN TYPEOF (v1)) AND ('INTEGER' IN TYPEOF (v2)) THEN
parts(v1,p,q); k := v2; r := 1.0; s := 0.0;
REPEAT i := 1 TO ABS(k); r := p*r-q*s; s := p*s+q*r; END_REPEAT;
IF k < 0 THEN t := r*r+s*s; r := r/t; s := -s/t; END_IF;
RETURN (makec(r,s));
END_IF;
ef_eq_c :
IF (cnlit IN TYPEOF (v1)) AND (cnlit IN TYPEOF (v2)) THEN
parts(v1,p,q); parts(v2,r,s); RETURN (ctmv((p = r) AND (q = s)));
END_IF;
ef_ne_c :
IF (cnlit IN TYPEOF (v1)) AND (cnlit IN TYPEOF (v2)) THEN
parts(v1,p,q); parts(v2,r,s); RETURN (ctmv((p <> r) OR (q <> s)));
END_IF;
ef_conjugate_c :
IF cnlit IN TYPEOF (v1) THEN parts(v1,p,q); RETURN (makec(p,-q)); END_IF;
ef_abs_c :
IF cnlit IN TYPEOF (v1) THEN
parts(v1,p,q); RETURN (ctmv(SQRT(p*p+q*q)));
END_IF;
ef_arg_c :
IF cnlit IN TYPEOF (v1) THEN
parts(v1,p,q); RETURN (ctmv(atan2(q,p)));
END_IF;
ef_cos_c :
IF cnlit IN TYPEOF (v1) THEN
parts(v1,p,q); t := 0.5*EXP(-q); u := 0.5*EXP(q);
RETURN (makec((t+u)*COS(p),(t-u)*SIN(p)));
END_IF;
ef_exp_c :
IF cnlit IN TYPEOF (v1) THEN
parts(v1,p,q); RETURN (makec(EXP(p)*COS(q),EXP(p)*SIN(q)));
END_IF;
ef_ln_c :
IF cnlit IN TYPEOF (v1) THEN
parts(v1,p,q); RETURN (makec(0.5*LOG(p*p+q*q),atan2(q,p)));
END_IF;
ef_sin_c :
IF cnlit IN TYPEOF (v1) THEN
parts(v1,p,q); t := 0.5*EXP(-q); u := 0.5*EXP(q);
RETURN (makec((t+u)*SIN(p),(u-t)*COS(p)));
END_IF;
ef_sqrt_c :
IF cnlit IN TYPEOF (v1) THEN
parts(v1,p,q); t := SQRT(SQRT(p*p+q*q)); u := 0.5*atan2(q,p);
RETURN (makec(t*COS(u),t*SIN(u)));
END_IF;
ef_tan_c :
IF cnlit IN TYPEOF (v1) THEN
parts(v1,p,q); t := EXP(2.0*q) + EXP(-2.0*q) + 2.0*COS(2.0*p);
RETURN (makec(2.0*SIN(2.0*p)/t,(EXP(-2.0*q)-EXP(2.0*q))/t));
END_IF;
-- ef_if_c : combined with ef_if
ef_subscript_s :
IF ('STRING' IN TYPEOF (v1)) AND ('INTEGER' IN TYPEOF (v2)) THEN
str := v1; k := v2; RETURN (ctmv(str[k]));
END_IF;
ef_eq_s :
IF ('STRING' IN TYPEOF (v1)) AND ('STRING' IN TYPEOF (v2)) THEN
str := v1; st2 := v2; RETURN (ctmv(str = st2));
END_IF;
ef_ne_s :
IF ('STRING' IN TYPEOF (v1)) AND ('STRING' IN TYPEOF (v2)) THEN
str := v1; st2 := v2; RETURN (ctmv(str <> st2));
END_IF;
ef_gt_s :
IF ('STRING' IN TYPEOF (v1)) AND ('STRING' IN TYPEOF (v2)) THEN
str := v1; st2 := v2; RETURN (ctmv(str > st2));
END_IF;
ef_lt_s :
IF ('STRING' IN TYPEOF (v1)) AND ('STRING' IN TYPEOF (v2)) THEN
str := v1; st2 := v2; RETURN (ctmv(str < st2));
END_IF;
ef_ge_s :
IF ('STRING' IN TYPEOF (v1)) AND ('STRING' IN TYPEOF (v2)) THEN
str := v1; st2 := v2; RETURN (ctmv(str >= st2));
END_IF;
ef_le_s :
IF ('STRING' IN TYPEOF (v1)) AND ('STRING' IN TYPEOF (v2)) THEN
str := v1; st2 := v2; RETURN (ctmv(str <= st2));
END_IF;
ef_subsequence_s :
IF ('STRING' IN TYPEOF (v1)) AND ('INTEGER' IN TYPEOF (v2)) AND
('INTEGER' IN TYPEOF (v3)) THEN
str := v1; j := v2; k := v3; RETURN (ctmv(str[j:k]));
END_IF;
ef_concat_s : BEGIN
str := '';
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF 'STRING' IN TYPEOF (vlist[i]) THEN
st2 := vlist[i]; str := str + st2;
REMOVE (vlist, i);
ELSE IF str <> '' THEN
INSERT (vlist, ctmv(str), i);
str := '';
END_IF; END_IF;
END_REPEAT;
IF SIZEOF (vlist) = 0 THEN RETURN (ctmv(str)); END_IF;
IF str <> '' THEN INSERT (vlist, ctmv(str), 0); END_IF;
IF SIZEOF (vlist) = 1 THEN RETURN (vlist[1]); END_IF;
END;
ef_size_s :
IF 'STRING' IN TYPEOF (v1) THEN str:=v1; RETURN (ctmv(LENGTH(str))); END_IF;
ef_format :
IF ('NUMBER' IN TYPEOF (v1)) AND ('STRING' IN TYPEOF (v2)) THEN
RETURN (ctmv(FORMAT(v1,v2)));
END_IF;
ef_value :
IF 'STRING' IN TYPEOF (v1) THEN str:=v1; RETURN (ctmv(VALUE(str))); END_IF;
ef_like :
IF ('STRING' IN TYPEOF (v1)) AND ('STRING' IN TYPEOF (v2)) THEN
RETURN (ctmv(v1 LIKE v2));
END_IF;
-- ef_if_s : combined with ef_if
ef_subscript_b :
IF ('BINARY' IN TYPEOF (v1)) AND ('INTEGER' IN TYPEOF (v2)) THEN
bin := v1; k := v2; RETURN (ctmv(bin[k]));
END_IF;
ef_eq_b :
IF ('BINARY' IN TYPEOF (v1)) AND ('BINARY' IN TYPEOF (v2)) THEN
bin := v1; bi2 := v2; RETURN (ctmv(bin = bi2));
END_IF;
ef_ne_b :
IF ('BINARY' IN TYPEOF (v1)) AND ('BINARY' IN TYPEOF (v2)) THEN
bin := v1; bi2 := v2; RETURN (ctmv(bin <> bi2));
END_IF;
ef_gt_b :
IF ('BINARY' IN TYPEOF (v1)) AND ('BINARY' IN TYPEOF (v2)) THEN
bin := v1; bi2 := v2; RETURN (ctmv(bin > bi2));
END_IF;
ef_lt_b :
IF ('BINARY' IN TYPEOF (v1)) AND ('BINARY' IN TYPEOF (v2)) THEN
bin := v1; bi2 := v2; RETURN (ctmv(bin < bi2));
END_IF;
ef_ge_b :
IF ('BINARY' IN TYPEOF (v1)) AND ('BINARY' IN TYPEOF (v2)) THEN
bin := v1; bi2 := v2; RETURN (ctmv(bin >= bi2));
END_IF;
ef_le_b :
IF ('BINARY' IN TYPEOF (v1)) AND ('BINARY' IN TYPEOF (v2)) THEN
bin := v1; bi2 := v2; RETURN (ctmv(bin <= bi2));
END_IF;
ef_subsequence_b :
IF ('BINARY' IN TYPEOF (v1)) AND ('INTEGER' IN TYPEOF (v2)) AND
('INTEGER' IN TYPEOF (v3)) THEN
bin := v1; j := v2; k := v3; RETURN (ctmv(bin[j:k]));
END_IF;
ef_concat_b : BEGIN
boo := FALSE;
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF 'BINARY' IN TYPEOF (vlist[i]) THEN
IF boo THEN bi2 := vlist[i]; bin := bin + bi2;
ELSE bin := vlist[i]; boo := TRUE; END_IF;
REMOVE (vlist, i);
ELSE IF boo THEN
INSERT (vlist, ctmv(bin), i);
boo := FALSE;
END_IF; END_IF;
END_REPEAT;
IF SIZEOF (vlist) = 0 THEN RETURN (ctmv(bin)); END_IF;
IF boo THEN INSERT (vlist, ctmv(bin), 0); END_IF;
IF SIZEOF (vlist) = 1 THEN RETURN (vlist[1]); END_IF;
END;
ef_size_b :
IF 'BINARY' IN TYPEOF (v1) THEN bin:=v1; RETURN (ctmv(BLENGTH(bin))); END_IF;
-- ef_if_b : combined with ef_if
ef_subscript_t :
IF ('LIST' IN TYPEOF (v1)) AND ('INTEGER' IN TYPEOF (v2)) THEN
tpl := v1; k := v2; RETURN (ctmv(tpl[k]));
END_IF;
ef_eq_t :
IF ('LIST' IN TYPEOF (v1)) AND ('LIST' IN TYPEOF (v2)) THEN
lgc := equal_maths_values(v1,v2);
IF lgc <> UNKNOWN THEN RETURN (ctmv(lgc)); END_IF;
END_IF;
ef_ne_t :
IF ('LIST' IN TYPEOF (v1)) AND ('LIST' IN TYPEOF (v2)) THEN
lgc := equal_maths_values(v1,v2);
IF lgc <> UNKNOWN THEN RETURN (ctmv(NOT lgc)); END_IF;
END_IF;
ef_concat_t : BEGIN
tpl := [];
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF 'STRING' IN TYPEOF (vlist[i]) THEN
tp2 := vlist[i]; tpl := tpl + tp2;
REMOVE (vlist, i);
ELSE IF SIZEOF (tpl) <> 0 THEN
INSERT (vlist, ctmv(tpl), i);
tpl := [];
END_IF; END_IF;
END_REPEAT;
IF SIZEOF (vlist) = 0 THEN RETURN (ctmv(tpl)); END_IF;
IF SIZEOF (tpl) <> 0 THEN INSERT (vlist, ctmv(tpl), 0); END_IF;
IF SIZEOF (vlist) = 1 THEN RETURN (vlist[1]); END_IF;
END;
ef_size_t :
IF 'LIST' IN TYPEOF (v1) THEN tpl:=v1; RETURN (ctmv(SIZEOF(tpl))); END_IF;
ef_entuple :
RETURN (ctmv(vlist));
ef_detuple : -- This can have multiple outputs, but the expression only
-- denotes the first.
IF 'LIST' IN TYPEOF (v1) THEN tpl:=v1; RETURN (ctmv(tpl[1])); END_IF;
ef_insert :
IF ('LIST' IN TYPEOF (v1)) AND ('INTEGER' IN TYPEOF (v3)) THEN
tpl := v1; k := v3; INSERT (tpl, v2, k); RETURN (ctmv(tpl));
END_IF;
ef_remove :
IF ('LIST' IN TYPEOF (v1)) AND ('INTEGER' IN TYPEOF (v2)) THEN
tpl := v1; k := v2; REMOVE (tpl, k); RETURN (ctmv(tpl));
END_IF;
-- ef_if_t : combined with ef_if
ef_sum_it :
IF good_t(v1,'INTEGER') THEN
tpl := v1; j := 0;
REPEAT i := 1 TO SIZEOF (tpl); j := j + tpl[i]; END_REPEAT;
RETURN (ctmv(j));
END_IF;
ef_product_it :
IF good_t(v1,'INTEGER') THEN
tpl := v1; j := 1;
REPEAT i := 1 TO SIZEOF (tpl); j := j * tpl[i]; END_REPEAT;
RETURN (ctmv(j));
END_IF;
ef_add_it : BEGIN
boo := FALSE;
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF good_t(vlist[i],'INTEGER') THEN
IF NOT boo THEN tpl := vlist[i]; boo := TRUE;
ELSE
tp2 := vlist[i];
IF SIZEOF (tpl) <> SIZEOF (tp2) THEN RETURN (?); END_IF;
REPEAT l := 1 TO SIZEOF (tpl); tpl[j] := tpl[j] + tp2[j]; END_REPEAT;
END_IF;
REMOVE (vlist, i);
END_IF;
END_REPEAT;
IF SIZEOF (vlist) = 0 THEN RETURN (ctmv(tpl)); END_IF;
IF boo THEN INSERT (vlist, ctmv(tpl), 0); END_IF;
IF SIZEOF (vlist) = 1 THEN RETURN (vlist[1]); END_IF;
END;
ef_subtract_it :
IF good_t(v1,'INTEGER') AND good_t(v2,'INTEGER') THEN
tpl := v1; tp2 := v2;
IF SIZEOF (tpl) <> SIZEOF (tp2) THEN RETURN (?); END_IF;
REPEAT i := 1 TO SIZEOF (tpl); tpl[i] := tpl[i] - tp2[i]; END_REPEAT;
RETURN (ctmv(tpl));
END_IF;
ef_scalar_mult_it :
IF ('INTEGER' IN TYPEOF (v1)) AND good_t(v2,'INTEGER') THEN
j := v1; tpl := v2;
REPEAT i := 1 TO SIZEOF (tpl); tpl[i] := j * tpl[i]; END_REPEAT;
RETURN (ctmv(tpl));
END_IF;
ef_dot_prod_it :
IF good_t(v1,'INTEGER') AND good_t(v2,'INTEGER') THEN
tpl := v1; tp2 := v2; j := 0;
IF SIZEOF (tpl) <> SIZEOF (tp2) THEN RETURN (?); END_IF;
REPEAT i := 1 TO SIZEOF (tpl); j := j + tpl[i] * tp2[i]; END_REPEAT;
RETURN (ctmv(j));
END_IF;
ef_sum_rt :
IF good_t(v1,'REAL') THEN
tpl := v1; r := 0.0;
REPEAT i := 1 TO SIZEOF (tpl); r := r + tpl[i]; END_REPEAT;
RETURN (ctmv(r));
END_IF;
ef_product_rt :
IF good_t(v1,'REAL') THEN
tpl := v1; r := 1.0;
REPEAT i := 1 TO SIZEOF (tpl); r := r * tpl[i]; END_REPEAT;
RETURN (ctmv(r));
END_IF;
ef_add_rt : BEGIN
boo := FALSE;
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF good_t(vlist[i],'REAL') THEN
IF NOT boo THEN tpl := vlist[i]; boo := TRUE;
ELSE
tp2 := vlist[i];
IF SIZEOF (tpl) <> SIZEOF (tp2) THEN RETURN (?); END_IF;
REPEAT l := 1 TO SIZEOF (tpl); tpl[j] := tpl[j] + tp2[j]; END_REPEAT;
END_IF;
REMOVE (vlist, i);
END_IF;
END_REPEAT;
IF SIZEOF (vlist) = 0 THEN RETURN (ctmv(tpl)); END_IF;
IF boo THEN INSERT (vlist, ctmv(tpl), 0); END_IF;
IF SIZEOF (vlist) = 1 THEN RETURN (vlist[1]); END_IF;
END;
ef_subtract_rt :
IF good_t(v1,'REAL') AND good_t(v2,'REAL') THEN
tpl := v1; tp2 := v2;
IF SIZEOF (tpl) <> SIZEOF (tp2) THEN RETURN (?); END_IF;
REPEAT i := 1 TO SIZEOF (tpl); tpl[i] := tpl[i] - tp2[i]; END_REPEAT;
RETURN (ctmv(tpl));
END_IF;
ef_scalar_mult_rt :
IF ('REAL' IN TYPEOF (v1)) AND good_t(v2,'REAL') THEN
r := v1; tpl := v2;
REPEAT i := 1 TO SIZEOF (tpl); tpl[i] := r * tpl[i]; END_REPEAT;
RETURN (ctmv(tpl));
END_IF;
ef_dot_prod_rt :
IF good_t(v1,'REAL') AND good_t(v2,'REAL') THEN
tpl := v1; tp2 := v2; r := 0;
IF SIZEOF (tpl) <> SIZEOF (tp2) THEN RETURN (?); END_IF;
REPEAT i := 1 TO SIZEOF (tpl); r := r + tpl[i] * tp2[i]; END_REPEAT;
RETURN (ctmv(r));
END_IF;
ef_norm_rt :
IF good_t(v1,'REAL') THEN
tpl := v1; r := 0.0;
REPEAT i := 1 TO SIZEOF (tpl); r := r + tpl[i]*tpl[i]; END_REPEAT;
RETURN (ctmv(SQRT(r)));
END_IF;
ef_sum_ct :
IF good_t(v1,cnlit) THEN
tpl := v1; p := 0.0; q := 0.0;
REPEAT i:=1 TO SIZEOF (tpl); parts(tpl[i],r,s); p:=p+r; q:=q+s; END_REPEAT;
RETURN (makec(p,q));
END_IF;
ef_product_ct :
IF good_t(v1,cnlit) THEN
tpl := v1; p := 1.0; q := 0.0;
REPEAT i := 1 TO SIZEOF (tpl);
parts(tpl[i],r,s); p := p*r-q*s; q := p*s+q*r;
END_REPEAT;
RETURN (makec(p,q));
END_IF;
ef_add_ct : BEGIN
boo := FALSE;
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF good_t(vlist[i],cnlit) THEN
IF NOT boo THEN tpl := vlist[i]; boo := TRUE;
ELSE
tp2 := vlist[i];
IF SIZEOF (tpl) <> SIZEOF (tp2) THEN RETURN (?); END_IF;
REPEAT l := 1 TO SIZEOF (tpl);
parts(tpl[j],p,q); parts(tp2[j],r,s); tpl[j] := makec(p+r,q+s);
END_REPEAT;
END_IF;
REMOVE (vlist, i);
END_IF;
END_REPEAT;
IF SIZEOF (vlist) = 0 THEN RETURN (ctmv(tpl)); END_IF;
IF boo THEN INSERT (vlist, ctmv(tpl), 0); END_IF;
IF SIZEOF (vlist) = 1 THEN RETURN (vlist[1]); END_IF;
END;
ef_subtract_ct :
IF good_t(v1,cnlit) AND good_t(v2,cnlit) THEN
tpl := v1; tp2 := v2;
IF SIZEOF (tpl) <> SIZEOF (tp2) THEN RETURN (?); END_IF;
REPEAT i := 1 TO SIZEOF (tpl);
parts(tpl[i],p,q); parts(tp2[i],r,s); tpl[i] := makec(p-r,q-s);
END_REPEAT;
RETURN (ctmv(tpl));
END_IF;
ef_scalar_mult_ct :
IF (cnlit IN TYPEOF (v1)) AND good_t(v2,cnlit) THEN
parts(v1,p,q); tpl := v2;
REPEAT i := 1 TO SIZEOF (tpl);
parts(tpl[i],r,s); tpl[i] := makec(p*r-q*s,p*s+q*r);
END_REPEAT;
RETURN (ctmv(tpl));
END_IF;
ef_dot_prod_ct :
IF good_t(v1,cnlit) AND good_t(v2,cnlit) THEN
tpl := v1; tp2 := v2; t := 0.0; u := 0.0;
IF SIZEOF (tpl) <> SIZEOF (tp2) THEN RETURN (?); END_IF;
REPEAT i := 1 TO SIZEOF (tpl);
parts(tpl[i],p,q); parts(tp2[i],r,s); t := t + p*r+q*s; u := u + q*r-p*s;
END_REPEAT;
RETURN (makec(t,u));
END_IF;
ef_norm_ct :
IF good_t(v1,cnlit) THEN
tpl := v1; r := 0.0;
REPEAT i := 1 TO SIZEOF (tpl); parts(tpl[i],p,q); r:=r+p*p+q*q; END_REPEAT;
RETURN (ctmv(SQRT(r)));
END_IF;
ef_if, ef_if_i, ef_if_r, ef_if_c, ef_if_s, ef_if_b, ef_if_t :
IF 'LOGICAL' IN TYPEOF (v1) THEN
lgc := v1; IF lgc THEN RETURN (v2); ELSE RETURN (v3); END_IF;
END_IF;
ef_ensemble : -- (mem + vlist) effectively converts list to set
RETURN (make_finite_space(mem + vlist));
ef_member_of :
IF (schema_prefix + 'MATHS_SPACE') IN TYPEOF (v2) THEN
lgc := member_of(v1,v2);
IF lgc <> UNKNOWN THEN RETURN (ctmv(lgc)); END_IF;
END_IF;
END_CASE;
RETURN (make_function_application(expr.func,vlist));
END_IF;
IF 'ABSTRACTED_EXPRESSION_FUNCTION' IN types THEN
gexpr := substitute(expr.func\abstracted_expression_function.expr,
expr.func\quantifier_expression.variables,vlist);
RETURN (simplify_generic_expression(gexpr));
END_IF;
IF 'FINITE_FUNCTION' IN types THEN
pairs := expr.func\finite_function.pairs;
REPEAT i := 1 TO SIZEOF (pairs);
IF equal_maths_values(vlist[1],pairs[i][1]) THEN
RETURN (simplify_maths_value(pairs[i][2]));
END_IF;
END_REPEAT;
RETURN (make_function_application(expr.func,vlist));
END_IF;
RETURN (expr);
END_FUNCTION;
FUNCTION simplify_generic_expression
(expr : generic_expression) : maths_value;
FUNCTION restore_unary(expr : unary_generic_expression;
opnd : generic_expression) : generic_expression;
expr.operand := opnd;
RETURN (expr);
END_FUNCTION; -- restore_unary
FUNCTION restore_binary(expr : binary_generic_expression;
opd1, opd2 : generic_expression) : generic_expression;
expr.operands[1] := opd1;
expr.operands[2] := opd2;
RETURN (expr);
END_FUNCTION; -- restore_binary
FUNCTION restore_mulary(expr : multiple_arity_generic_expression;
ops : LIST OF generic_expression) : generic_expression;
expr.operands := ops;
RETURN (expr);
END_FUNCTION; -- restore_mulary
FUNCTION make_number_literal(nmb : NUMBER) : generic_literal;
IF 'INTEGER' IN TYPEOF (nmb) THEN RETURN (make_int_literal(nmb)); END_IF;
RETURN (make_real_literal(nmb));
END_FUNCTION; -- make_number_literal;
LOCAL
types : SET OF STRING := stripped_typeof (expr);
v1, v2 : maths_value;
vlist : LIST OF maths_value := [];
op1, op2 : generic_expression;
oplist : LIST OF generic_expression := [];
opnds : LIST [2:?] OF generic_expression;
n, m : INTEGER;
finfun : maths_function_select;
boo : BOOLEAN;
str : STRING;
nmb : NUMBER;
END_LOCAL;
-- Unwrap the elementary kinds of literals
IF 'INT_LITERAL' IN types THEN
RETURN (convert_to_maths_value (expr\int_literal.the_value));
END_IF;
IF 'REAL_LITERAL' IN types THEN
RETURN (convert_to_maths_value (expr\real_literal.the_value));
END_IF;
IF 'BOOLEAN_LITERAL' IN types THEN
RETURN (convert_to_maths_value (expr\boolean_literal.the_value));
END_IF;
IF 'STRING_LITERAL' IN types THEN
RETURN (convert_to_maths_value (expr\string_literal.the_value));
END_IF;
IF 'COMPLEX_NUMBER_LITERAL' IN types THEN
RETURN (expr); -- No simpler expression available
END_IF;
IF 'LOGICAL_LITERAL' IN types THEN
RETURN (convert_to_maths_value (expr\logical_literal.lit_value));
END_IF;
IF 'BINARY_LITERAL' IN types THEN
RETURN (convert_to_maths_value (expr\binary_literal.lit_value));
END_IF;
IF 'MATHS_ENUM_LITERAL' IN types THEN
RETURN (expr\maths_enum_literal.lit_value);
END_IF;
IF 'REAL_TUPLE_LITERAL' IN types THEN
RETURN (convert_to_maths_value (expr\real_tuple_literal.lit_value));
END_IF;
IF 'INTEGER_TUPLE_LITERAL' IN types THEN
RETURN (convert_to_maths_value (expr\integer_tuple_literal.lit_value));
END_IF;
IF 'ATOM_BASED_LITERAL' IN types THEN
RETURN (expr\atom_based_literal.lit_value);
END_IF;
IF 'MATHS_TUPLE_LITERAL' IN types THEN
RETURN (convert_to_maths_value (expr\maths_tuple_literal.lit_value));
END_IF;
-- Simplify one special class of literals
IF 'MATHS_SPACE' IN types THEN
RETURN (simplify_maths_space(expr));
END_IF;
-- Simplify one special kind of expression
IF 'FUNCTION_APPLICATION' IN types THEN
RETURN (simplify_function_application(expr));
END_IF;
-- Separate and simplify the operands
IF 'UNARY_GENERIC_EXPRESSION' IN types THEN
v1 := simplify_generic_expression(expr\unary_generic_expression.operand);
op1 := convert_to_operand(v1);
END_IF;
IF 'BINARY_GENERIC_EXPRESSION' IN types THEN
v1 := simplify_generic_expression(expr\binary_generic_expression.operands[1]);
op1 := convert_to_operand(v1);
v2 := simplify_generic_expression(expr\binary_generic_expression.operands[2]);
op2 := convert_to_operand(v2);
END_IF;
IF 'MULTIPLE_ARITY_GENERIC_EXPRESSION' IN types THEN
opnds := expr\multiple_arity_generic_expression.operands;
REPEAT i := 1 TO SIZEOF (opnds);
v1 := simplify_generic_expression(opnds[i]);
INSERT (vlist, v1, i-1);
INSERT (oplist, convert_to_operand(v1), i-1);
END_REPEAT;
END_IF;
-- Simplify the one kind of maths_function which derives its operands.
IF 'PARALLEL_COMPOSED_FUNCTION' IN types THEN
v1 := vlist[1];
n := SIZEOF (vlist);
finfun := vlist[n];
REMOVE (vlist, n);
REMOVE (vlist, 1);
RETURN (make_parallel_composed_function(v1,vlist,finfun));
END_IF;
-- Simplify individual kinds of expressions. It is not necessary to cover all cases.
IF ('ABS_EXPRESSION' IN types) AND ('NUMBER' IN TYPEOF (v1)) THEN
RETURN (convert_to_maths_value (ABS(v1)));
END_IF;
IF ('ACOS_EXPRESSION' IN types) AND ('NUMBER' IN TYPEOF (v1)) THEN
RETURN (convert_to_maths_value (ACOS(v1)));
END_IF;
IF 'AND_EXPRESSION' IN types THEN
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF 'BOOLEAN' IN TYPEOF (vlist[i]) THEN
boo := vlist[i];
IF NOT boo THEN RETURN (convert_to_maths_value(FALSE)); END_IF;
REMOVE (oplist, i);
END_IF;
END_REPEAT;
IF SIZEOF (oplist) = 0 THEN RETURN (convert_to_maths_value(TRUE)); END_IF;
IF SIZEOF (oplist) = 1 THEN RETURN (oplist[1]); END_IF;
END_IF;
IF ('ASIN_EXPRESSION' IN types) AND ('NUMBER' IN TYPEOF (v1)) THEN
RETURN (convert_to_maths_value (ASIN(v1)));
END_IF;
IF ('ATAN_EXPRESSION' IN types) AND
('NUMBER' IN TYPEOF (v1)) AND ('NUMBER' IN TYPEOF (v2)) THEN
RETURN (convert_to_maths_value (ATAN(v1,v2)));
END_IF;
IF ('COMPARISON_EXPRESSION' IN types) AND (
(('NUMBER' IN TYPEOF (v1)) AND ('NUMBER' IN TYPEOF (v2))) OR
(('STRING' IN TYPEOF (v1)) AND ('STRING' IN TYPEOF (v2))) OR
(('BOOLEAN' IN TYPEOF (v1)) AND ('BOOLEAN' IN TYPEOF (v2))) ) THEN
IF 'COMPARISON_EQUAL' IN types THEN boo := bool(v1 = v2);
ELSE IF 'COMPARISON_GREATER' IN types THEN boo := bool(v1 > v2);
ELSE IF 'COMPARISON_GREATER_EQUAL' IN types THEN boo := bool(v1 >= v2);
ELSE IF 'COMPARISON_LESS' IN types THEN boo := bool(v1 < v2);
ELSE IF 'COMPARISON_LESS_EQUAL' IN types THEN boo := bool(v1 <= v2);
ELSE IF 'COMPARISON_NOT_EQUAL' IN types THEN boo := bool(v1 <> v2);
ELSE IF 'LIKE_EXPRESSION' IN types THEN boo := bool(v1 LIKE v2);
ELSE RETURN (?); -- Unreachable
END_IF; END_IF; END_IF; END_IF; END_IF; END_IF; END_IF;
RETURN (convert_to_maths_value (boo));
END_IF;
IF 'CONCAT_EXPRESSION' IN types THEN
str := '';
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF 'STRING' IN TYPEOF (vlist[i]) THEN
str := vlist[i] + str;
REMOVE (oplist, i);
ELSE IF LENGTH(str) > 0 THEN
INSERT (oplist, make_string_literal(str), i);
str := '';
END_IF; END_IF;
END_REPEAT;
IF SIZEOF (oplist) = 0 THEN RETURN (convert_to_maths_value(str)); END_IF;
IF LENGTH(str) > 0 THEN INSERT (oplist, make_string_literal(str), 0); END_IF;
IF SIZEOF (oplist) = 1 THEN RETURN (oplist[1]); END_IF;
END_IF;
IF ('COS_EXPRESSION' IN types) AND ('NUMBER' IN TYPEOF (v1)) THEN
RETURN (convert_to_maths_value (COS(v1)));
END_IF;
IF ('DIV_EXPRESSION' IN types) AND
('NUMBER' IN TYPEOF (v1)) AND ('NUMBER' IN TYPEOF (v2)) THEN
RETURN (convert_to_maths_value (v1 DIV v2));
END_IF;
IF 'EQUALS_EXPRESSION' IN types THEN
opnds := expr\binary_generic_expression.operands;
RETURN (convert_to_maths_value (opnds[1] :=: opnds[2]));
END_IF;
IF ('EXP_EXPRESSION' IN types) AND ('NUMBER' IN TYPEOF (v1)) THEN
RETURN (convert_to_maths_value (EXP(v1)));
END_IF;
IF ('FORMAT_EXPRESSION' IN types) AND
('NUMBER' IN TYPEOF (v1)) AND ('STRING' IN TYPEOF (v2)) THEN
RETURN (convert_to_maths_value (FORMAT(v1,v2)));
END_IF;
IF ('INDEX_EXPRESSION' IN types) AND
('STRING' IN TYPEOF (v1)) AND ('NUMBER' IN TYPEOF (v2)) THEN
str := v1; n := v2;
RETURN (convert_to_maths_value (str[n]));
END_IF;
IF ('INT_VALUE_EXPRESSION' IN types) AND ('STRING' IN TYPEOF (v1)) THEN
RETURN (convert_to_maths_value (VALUE(v1)));
END_IF;
IF 'INTERVAL_EXPRESSION' IN types THEN
str := '';
IF 'NUMBER' IN TYPEOF (vlist[1]) THEN str := 'NUMBER'; END_IF;
IF 'STRING' IN TYPEOF (vlist[1]) THEN str := 'STRING'; END_IF;
IF 'BOOLEAN' IN TYPEOF (vlist[1]) THEN str := 'BOOLEAN'; END_IF;
IF (LENGTH (str) > 0) AND (str IN TYPEOF (vlist[2])) AND
(str IN TYPEOF (vlist[3])) THEN
RETURN (convert_to_maths_value ({vlist[1] <= vlist[2] <= vlist[3]}));
END_IF;
END_IF;
IF ('LENGTH_EXPRESSION' IN types) AND ('STRING' IN TYPEOF (v1)) THEN
RETURN (convert_to_maths_value (LENGTH(v1)));
END_IF;
IF ('LOG_EXPRESSION' IN types) AND ('NUMBER' IN TYPEOF (v1)) THEN
RETURN (convert_to_maths_value (LOG(v1)));
END_IF;
IF ('LOG10_EXPRESSION' IN types) AND ('NUMBER' IN TYPEOF (v1)) THEN
RETURN (convert_to_maths_value (LOG10(v1)));
END_IF;
IF ('LOG2_EXPRESSION' IN types) AND ('NUMBER' IN TYPEOF (v1)) THEN
RETURN (convert_to_maths_value (LOG2(v1)));
END_IF;
IF 'MAXIMUM_EXPRESSION' IN types THEN
boo := FALSE;
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF 'NUMBER' IN TYPEOF (vlist[i]) THEN
IF boo THEN
IF nmb < vlist[i] THEN nmb := vlist[i]; END_IF;
ELSE
nmb := vlist[i]; boo := TRUE;
END_IF;
REMOVE (oplist, i);
END_IF;
END_REPEAT;
IF SIZEOF (oplist) = 0 THEN RETURN (convert_to_maths_value(nmb)); END_IF;
IF boo THEN INSERT (oplist, make_number_literal(nmb), 0); END_IF;
END_IF;
IF 'MINIMUM_EXPRESSION' IN types THEN
boo := FALSE;
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF 'NUMBER' IN TYPEOF (vlist[i]) THEN
IF boo THEN
IF nmb > vlist[i] THEN nmb := vlist[i]; END_IF;
ELSE
nmb := vlist[i]; boo := TRUE;
END_IF;
REMOVE (oplist, i);
END_IF;
END_REPEAT;
IF SIZEOF (oplist) = 0 THEN RETURN (convert_to_maths_value(nmb)); END_IF;
IF boo THEN INSERT (oplist, make_number_literal(nmb), 0); END_IF;
END_IF;
IF ('MINUS_EXPRESSION' IN types) AND
('NUMBER' IN TYPEOF (v1)) AND ('NUMBER' IN TYPEOF (v2)) THEN
RETURN (convert_to_maths_value (v1 - v2));
END_IF;
IF ('MOD_EXPRESSION' IN types) AND
('NUMBER' IN TYPEOF (v1)) AND ('NUMBER' IN TYPEOF (v2)) THEN
RETURN (convert_to_maths_value (v1 MOD v2));
END_IF;
IF 'MULT_EXPRESSION' IN types THEN
nmb := 1;
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF 'NUMBER' IN TYPEOF (vlist[i]) THEN
nmb := nmb * vlist[i];
REMOVE (oplist, i);
END_IF;
END_REPEAT;
IF SIZEOF (oplist) = 0 THEN RETURN (convert_to_maths_value(nmb)); END_IF;
IF nmb <> 1 THEN INSERT (oplist, make_number_literal(nmb), 0); END_IF;
IF SIZEOF (oplist) = 1 THEN RETURN (oplist[1]); END_IF;
END_IF;
IF ('NOT_EXPRESSION' IN types) AND ('BOOLEAN' IN TYPEOF (v1)) THEN
boo := v1;
RETURN (convert_to_maths_value (NOT(boo)));
END_IF;
IF ('ODD_EXPRESSION' IN types) AND ('INTEGER' IN TYPEOF (v1)) THEN
RETURN (convert_to_maths_value (ODD(v1)));
END_IF;
IF 'OR_EXPRESSION' IN types THEN
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF 'BOOLEAN' IN TYPEOF (vlist[i]) THEN
boo := vlist[i];
IF boo THEN RETURN (convert_to_maths_value(TRUE)); END_IF;
REMOVE (oplist, i);
END_IF;
END_REPEAT;
IF SIZEOF (oplist) = 0 THEN RETURN (convert_to_maths_value(FALSE)); END_IF;
IF SIZEOF (oplist) = 1 THEN RETURN (oplist[1]); END_IF;
END_IF;
IF 'PLUS_EXPRESSION' IN types THEN
nmb := 0;
REPEAT i := SIZEOF (vlist) TO 1 BY -1;
IF 'NUMBER' IN TYPEOF (vlist[i]) THEN
nmb := nmb + vlist[i];
REMOVE (oplist, i);
END_IF;
END_REPEAT;
IF SIZEOF (oplist) = 0 THEN RETURN (convert_to_maths_value(nmb)); END_IF;
IF nmb <> 0 THEN INSERT (oplist, make_number_literal(nmb), 0); END_IF;
IF SIZEOF (oplist) = 1 THEN RETURN (oplist[1]); END_IF;
END_IF;
IF ('POWER_EXPRESSION' IN types) AND
('NUMBER' IN TYPEOF (v1)) AND ('NUMBER' IN TYPEOF (v2)) THEN
RETURN (convert_to_maths_value (v1 ** v2));
END_IF;
IF ('SIN_EXPRESSION' IN types) AND ('NUMBER' IN TYPEOF (v1)) THEN
RETURN (convert_to_maths_value (SIN(v1)));
END_IF;
IF ('SLASH_EXPRESSION' IN types) AND
('NUMBER' IN TYPEOF (v1)) AND ('NUMBER' IN TYPEOF (v2)) THEN
RETURN (convert_to_maths_value (v1 / v2));
END_IF;
IF ('SQUARE_ROOT_EXPRESSION' IN types) AND ('NUMBER' IN TYPEOF (v1)) THEN
RETURN (convert_to_maths_value (SQRT(v1)));
END_IF;
IF ('SUBSTRING_EXPRESSION' IN types) AND
('STRING' IN TYPEOF (vlist[1])) AND ('NUMBER' IN TYPEOF (vlist[2])) AND
('NUMBER' IN TYPEOF (vlist[3])) THEN
str := vlist[1]; n := vlist[2]; m := vlist[3];
RETURN (convert_to_maths_value (str[n:m]));
END_IF;
IF ('TAN_EXPRESSION' IN types) AND ('NUMBER' IN TYPEOF (v1)) THEN
RETURN (convert_to_maths_value (TAN(v1)));
END_IF;
IF ('UNARY_MINUS_EXPRESSION' IN types) AND ('NUMBER' IN TYPEOF (v1)) THEN
nmb := v1;
RETURN (convert_to_maths_value (-nmb));
END_IF;
IF ('VALUE_EXPRESSION' IN types) AND ('STRING' IN TYPEOF (v1)) THEN
RETURN (convert_to_maths_value (VALUE(v1)));
END_IF;
IF ('XOR_EXPRESSION' IN types) AND
('BOOLEAN' IN TYPEOF (v1)) AND ('BOOLEAN' IN TYPEOF (v2)) THEN
RETURN (convert_to_maths_value (v1 XOR v2));
END_IF;
-- No special simplification defined, return same with simplified operands.
IF 'UNARY_GENERIC_EXPRESSION' IN types THEN
RETURN (restore_unary(expr,op1));
END_IF;
IF 'BINARY_GENERIC_EXPRESSION' IN types THEN
RETURN (restore_binary(expr,op1,op2));
END_IF;
IF 'MULTIPLE_ARITY_GENERIC_EXPRESSION' IN types THEN
RETURN (restore_mulary(expr,oplist));
END_IF;
-- Should be unreachable, but for safety, return unsimplified expression.
RETURN (expr);
END_FUNCTION;
FUNCTION simplify_maths_space
(spc : maths_space) : maths_space;
LOCAL
stypes : SET OF STRING := stripped_typeof (spc);
sset : SET OF maths_value;
zset : SET OF maths_value := [];
zval : maths_value;
zspc : maths_space;
zallint : BOOLEAN := TRUE;
zint, zmin, zmax : INTEGER;
factors : LIST OF maths_space;
zfactors : LIST OF maths_space := [];
rspc : maths_space;
END_LOCAL;
IF 'FINITE_SPACE' IN stypes THEN
sset := spc\finite_space.members;
REPEAT i := 1 TO SIZEOF (sset);
zval := simplify_maths_value(sset[i]);
zset := zset + [zval];
IF zallint AND ('INTEGER' IN TYPEOF (zval)) THEN
zint := zval;
IF i = 1 THEN
zmin := zint;
zmax := zint;
ELSE
IF zint < zmin THEN
zmin := zint;
END_IF;
IF zint > zmax THEN
zmax := zint;
END_IF;
END_IF;
ELSE
zallint := FALSE;
END_IF;
END_REPEAT;
IF zallint AND (SIZEOF(zset) = zmax-zmin+1) THEN
RETURN (make_finite_integer_interval(zmin,zmax));
END_IF;
RETURN (make_finite_space(zset));
END_IF;
IF 'UNIFORM_PRODUCT_SPACE' IN stypes THEN
zspc := simplify_maths_space(spc\uniform_product_space.base);
RETURN (make_uniform_product_space(zspc,spc\uniform_product_space.exponent));
END_IF;
IF 'LISTED_PRODUCT_SPACE' IN stypes THEN
factors := spc\listed_product_space.factors;
REPEAT i := 1 TO SIZEOF (factors);
INSERT (zfactors, simplify_maths_space(factors[i]), i-1);
END_REPEAT;
RETURN (make_listed_product_space(zfactors));
END_IF;
IF 'EXTENDED_TUPLE_SPACE' IN stypes THEN
zspc := simplify_maths_space(spc\extended_tuple_space.base);
rspc := simplify_maths_space(spc\extended_tuple_space.extender);
RETURN (make_extended_tuple_space(zspc,rspc));
END_IF;
IF 'FUNCTION_SPACE' IN stypes THEN
zspc := simplify_maths_space(spc\function_space.domain_argument);
rspc := simplify_maths_space(spc\function_space.range_argument);
RETURN (make_function_space(spc\function_space.domain_constraint,zspc,
spc\function_space.range_constraint,rspc));
END_IF;
RETURN (spc);
END_FUNCTION;
FUNCTION simplify_maths_value
(val : maths_value) : maths_value;
LOCAL
vtypes : SET OF STRING := stripped_typeof(val);
vlist : LIST OF maths_value;
nlist : LIST OF maths_value := [];
END_LOCAL;
IF 'GENERIC_EXPRESSION' IN vtypes THEN
RETURN (simplify_generic_expression(val));
END_IF;
IF 'LIST' IN vtypes THEN
vlist := val;
REPEAT i := 1 TO SIZEOF (vlist);
INSERT (nlist, simplify_maths_value(vlist[i]), i-1);
END_REPEAT;
RETURN (convert_to_maths_value(nlist));
END_IF;
RETURN (val);
END_FUNCTION;
FUNCTION singleton_member_of
(spc : maths_space) : maths_value;
LOCAL
types : SET OF STRING := stripped_typeof (spc);
END_LOCAL;
IF 'FINITE_SPACE' IN types THEN
IF SIZEOF (spc\finite_space.members) = 1 THEN
RETURN (spc\finite_space.members[1]);
END_IF;
RETURN (?);
END_IF;
IF 'FINITE_INTEGER_INTERVAL' IN types THEN
IF spc\finite_integer_interval.size = 1 THEN
RETURN (spc\finite_integer_interval.min);
END_IF;
RETURN (?);
END_IF;
RETURN (?);
END_FUNCTION;
FUNCTION space_dimension
(tspace : tuple_space) : nonnegative_integer;
LOCAL
types : SET OF STRING := TYPEOF (tspace);
END_LOCAL;
IF (schema_prefix + 'UNIFORM_PRODUCT_SPACE') IN types THEN
RETURN (tspace\uniform_product_space.exponent);
END_IF;
IF (schema_prefix + 'LISTED_PRODUCT_SPACE') IN types THEN
RETURN (SIZEOF (tspace\listed_product_space.factors));
END_IF;
IF (schema_prefix + 'EXTENDED_TUPLE_SPACE') IN types THEN
-- In the case of an extended_tuple_space, the minimum dimension is returned.
RETURN (space_dimension (tspace\extended_tuple_space.base));
END_IF;
-- Should be unreachable
RETURN (?);
END_FUNCTION;
FUNCTION space_is_continuum
(space : maths_space) : BOOLEAN;
LOCAL
typenames : SET OF STRING := TYPEOF (space);
factors : LIST OF maths_space;
END_LOCAL;
IF NOT EXISTS (space) THEN
RETURN (FALSE);
END_IF;
IF subspace_of_es(space,es_reals) OR subspace_of_es(space,es_complex_numbers) THEN
RETURN (TRUE);
END_IF;
IF (schema_prefix + 'UNIFORM_PRODUCT_SPACE') IN typenames THEN
RETURN (space_is_continuum(space\uniform_product_space.base));
END_IF;
IF (schema_prefix + 'LISTED_PRODUCT_SPACE') IN typenames THEN
factors := space\listed_product_space.factors;
IF SIZEOF(factors) = 0 THEN
RETURN (FALSE);
END_IF;
REPEAT i := 1 TO SIZEOF (factors);
IF NOT space_is_continuum(factors[i]) THEN
RETURN (FALSE);
END_IF;
END_REPEAT;
RETURN (TRUE);
END_IF;
RETURN (FALSE);
END_FUNCTION;
FUNCTION space_is_singleton
(spc : maths_space) : BOOLEAN;
LOCAL
types : SET OF STRING := stripped_typeof (spc);
END_LOCAL;
IF 'FINITE_SPACE' IN types THEN
RETURN (bool(SIZEOF (spc\finite_space.members) = 1));
END_IF;
IF 'FINITE_INTEGER_INTERVAL' IN types THEN
RETURN (bool(spc\finite_integer_interval.size = 1));
END_IF;
RETURN (FALSE);
END_FUNCTION;
FUNCTION stripped_typeof
(arg : GENERIC : G) : SET[0:?] OF STRING;
LOCAL
types : SET OF STRING := TYPEOF (arg);
stypes : SET OF STRING := [];
n : INTEGER := LENGTH (schema_prefix);
END_LOCAL;
REPEAT i := 1 TO SIZEOF (types);
IF types[i][1:n] = schema_prefix THEN
stypes := stypes + types[i][n+1:LENGTH(types[i])];
ELSE
stypes := stypes + types[i];
END_IF;
END_REPEAT;
RETURN (stypes);
END_FUNCTION;
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, cum : LOGICAL;
es_val : elementary_space_enumerators;
bnd1, bnd2 : REAL;
n : INTEGER;
sp1, sp2 : maths_space;
prgn1, 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;
-- Note that the cases (spc2=the_generics) and (spc1=spc2) have been handled.
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;
-- Should be unreachable.
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;
-- Should be unreachable
RETURN (UNKNOWN);
END_FUNCTION;
FUNCTION subspace_of_es
(spc : maths_space; es : elementary_space_enumerators) : LOGICAL;
LOCAL
types : SET OF STRING := stripped_typeof(spc);
END_LOCAL;
IF NOT EXISTS (spc) OR NOT EXISTS (es) THEN RETURN (FALSE); END_IF;
IF 'ELEMENTARY_SPACE' IN types THEN
RETURN (es_subspace_of_es(spc\elementary_space.space_id,es));
END_IF;
IF 'FINITE_SPACE' IN types THEN
RETURN (all_members_of_es(spc\finite_space.members,es));
END_IF;
CASE es OF
es_numbers : RETURN (
('FINITE_INTEGER_INTERVAL' IN types) OR
('INTEGER_INTERVAL_FROM_MIN' IN types) OR
('INTEGER_INTERVAL_TO_MAX' IN types) OR
('FINITE_REAL_INTERVAL' IN types) OR
('REAL_INTERVAL_FROM_MIN' IN types) OR
('REAL_INTERVAL_TO_MAX' IN types) OR
('CARTESIAN_COMPLEX_NUMBER_REGION' IN types) OR
('POLAR_COMPLEX_NUMBER_REGION' IN types) );
es_complex_numbers : RETURN (
('CARTESIAN_COMPLEX_NUMBER_REGION' IN types) OR
('POLAR_COMPLEX_NUMBER_REGION' IN types) );
es_reals : RETURN (
('FINITE_REAL_INTERVAL' IN types) OR
('REAL_INTERVAL_FROM_MIN' IN types) OR
('REAL_INTERVAL_TO_MAX' IN types) );
es_integers : RETURN (
('FINITE_INTEGER_INTERVAL' IN types) OR
('INTEGER_INTERVAL_FROM_MIN' IN types) OR
('INTEGER_INTERVAL_TO_MAX' IN types) );
es_logicals : RETURN (FALSE);
es_booleans : RETURN (FALSE);
es_strings : RETURN (FALSE);
es_binarys : RETURN (FALSE);
es_maths_spaces : RETURN (FALSE);
es_maths_functions : RETURN ('FUNCTION_SPACE' IN types);
es_generics : RETURN (TRUE);
END_CASE;
RETURN (UNKNOWN);
END_FUNCTION;
FUNCTION substitute
(expr : generic_expression; vars : LIST[1:?] OF generic_variable; vals : LIST[1:?] OF maths_value) : generic_expression;
LOCAL
types : SET OF STRING := stripped_typeof(expr);
opnds : LIST OF generic_expression;
op1, op2 : generic_expression;
qvars : LIST OF generic_variable;
srcdom : maths_space_or_function;
prpfun : LIST [1:?] OF maths_function;
finfun : maths_function_select;
END_LOCAL;
IF SIZEOF (vars) <> SIZEOF (vals) THEN RETURN (?); END_IF;
IF 'GENERIC_LITERAL' IN types THEN RETURN (expr); END_IF;
IF 'GENERIC_VARIABLE' IN types THEN
REPEAT i := 1 TO SIZEOF (vars);
IF expr :=: vars[i] THEN RETURN (vals[i]); END_IF;
END_REPEAT;
RETURN (expr);
END_IF;
IF 'QUANTIFIER_EXPRESSION' IN types THEN
qvars := expr\quantifier_expression.variables;
-- Variables subject to a quantifier do not participate in this kind of
-- substitution process.
REPEAT i := SIZEOF (vars) TO 1 BY -1;
IF vars[i] IN qvars THEN
REMOVE (vars, i);
REMOVE (vals, i);
END_IF;
END_REPEAT;
opnds := expr\multiple_arity_generic_expression.operands;
REPEAT i := 1 TO SIZEOF (opnds);
IF NOT (opnds[i] IN qvars) THEN
expr\multiple_arity_generic_expression.operands[i] :=
substitute(opnds[i],vars,vals);
-- This technique will not work on subtypes of quantifier_expression
-- which derive their operands from other attributes!
END_IF;
END_REPEAT;
RETURN (expr); -- operands modified!
END_IF;
IF 'UNARY_GENERIC_EXPRESSION' IN types THEN
op1 := expr\unary_generic_expression.operand;
expr\unary_generic_expression.operand := substitute(op1, vars, vals);
-- This technique will not work on subtypes of unary_generic_expression
-- which derive their operands from other attributes!
END_IF;
IF 'BINARY_GENERIC_EXPRESSION' IN types THEN
op1 := expr\binary_generic_expression.operands[1];
expr\binary_generic_expression.operands[1] := substitute(op1, vars, vals);
op2 := expr\binary_generic_expression.operands[2];
expr\binary_generic_expression.operands[2] := substitute(op2, vars, vals);
-- This technique will not work on subtypes of binary_generic_expression
-- which derive their operands from other attributes!
END_IF;
IF 'PARALLEL_COMPOSED_FUNCTION' IN types THEN
-- Subtype of multiple_arity_generic_expression which derives its operands.
srcdom := expr\parallel_composed_function.source_of_domain;
prpfun := expr\parallel_composed_function.prep_functions;
finfun := expr\parallel_composed_function.final_function;
srcdom := substitute(srcdom,vars,vals);
REPEAT i := 1 TO SIZEOF (prpfun);
prpfun[i] := substitute(prpfun[i],vars,vals);
END_REPEAT;
IF 'MATHS_FUNCTION' IN stripped_typeof(finfun) THEN
finfun := substitute(finfun,vars,vals);
END_IF;
RETURN (make_parallel_composed_function(srcdom,prpfun,finfun));
END_IF;
IF 'MULTIPLE_ARITY_GENERIC_EXPRESSION' IN types THEN
opnds := expr\multiple_arity_generic_expression.operands;
REPEAT i := 1 TO SIZEOF (opnds);
expr\multiple_arity_generic_expression.operands[i] :=
substitute(opnds[i],vars,vals);
-- This technique will not work on subtypes of multiple_arity_generic_
-- expression which derive their operands from other attributes!
END_REPEAT;
END_IF;
RETURN (expr);
END_FUNCTION;
FUNCTION values_space_of
(expr : generic_expression) : maths_space;
LOCAL
e_prefix : STRING := 'ISO13584_EXPRESSIONS_SCHEMA.';
typenames : SET OF STRING := TYPEOF (expr);
END_LOCAL;
IF (schema_prefix + 'MATHS_VARIABLE') IN typenames THEN
RETURN (expr\maths_variable.values_space);
END_IF;
IF (e_prefix + 'EXPRESSION') IN typenames THEN
IF (e_prefix + 'NUMERIC_EXPRESSION') IN typenames THEN
IF expr\numeric_expression.is_int THEN
IF (e_prefix + 'INT_LITERAL') IN typenames THEN
RETURN (make_finite_space ([expr\int_literal.the_value]));
ELSE
RETURN (the_integers);
END_IF;
ELSE
IF (e_prefix + 'REAL_LITERAL') IN typenames THEN
RETURN (make_finite_space ([expr\real_literal.the_value]));
ELSE
RETURN (the_reals);
END_IF;
END_IF;
END_IF;
IF (e_prefix + 'BOOLEAN_EXPRESSION') IN typenames THEN
IF (e_prefix + 'BOOLEAN_LITERAL') IN typenames THEN
RETURN (make_finite_space ([expr\boolean_literal.the_value]));
ELSE
RETURN (the_booleans);
END_IF;
END_IF;
IF (e_prefix + 'STRING_EXPRESSION') IN typenames THEN
IF (e_prefix + 'STRING_LITERAL') IN typenames THEN
RETURN (make_finite_space ([expr\string_literal.the_value]));
ELSE
RETURN (the_strings);
END_IF;
END_IF;
RETURN (?); -- unknown subtype of expression
END_IF;
IF (schema_prefix + 'MATHS_FUNCTION') IN typenames THEN
IF expression_is_constant (expr) THEN
RETURN (make_finite_space ([expr]));
ELSE
RETURN (make_function_space (sc_equal, expr\maths_function.domain,
sc_equal, expr\maths_function.range));
END_IF;
END_IF;
IF (schema_prefix + 'FUNCTION_APPLICATION') IN typenames THEN
RETURN (expr\function_application.func.range);
END_IF;
IF (schema_prefix + 'MATHS_SPACE') IN typenames THEN
IF expression_is_constant (expr) THEN
RETURN (make_finite_space ([expr]));
ELSE
-- This case cannot occur in this version of the schema.
-- When it becomes possible, the subtypes should be analysed and
-- more finely defined spaces returned.
RETURN (make_elementary_space (es_maths_spaces));
END_IF;
END_IF;
IF (schema_prefix + 'DEPENDENT_VARIABLE_DEFINITION') IN typenames THEN
RETURN (values_space_of (expr\unary_generic_expression.operand));
END_IF;
IF (schema_prefix + 'COMPLEX_NUMBER_LITERAL') IN typenames THEN
RETURN (make_finite_space ([expr]));
END_IF;
IF (schema_prefix + 'LOGICAL_LITERAL') IN typenames THEN
RETURN (make_finite_space ([expr\logical_literal.lit_value]));
END_IF;
IF (schema_prefix + 'BINARY_LITERAL') IN typenames THEN
RETURN (make_finite_space ([expr\binary_literal.lit_value]));
END_IF;
IF (schema_prefix + 'MATHS_ENUM_LITERAL') IN typenames THEN
RETURN (make_finite_space ([expr\maths_enum_literal.lit_value]));
END_IF;
IF (schema_prefix + 'REAL_TUPLE_LITERAL') IN typenames THEN
RETURN (make_finite_space ([expr\real_tuple_literal.lit_value]));
END_IF;
IF (schema_prefix + 'INTEGER_TUPLE_LITERAL') IN typenames THEN
RETURN (make_finite_space ([expr\integer_tuple_literal.lit_value]));
END_IF;
IF (schema_prefix + 'ATOM_BASED_LITERAL') IN typenames THEN
RETURN (make_finite_space ([expr\atom_based_literal.lit_value]));
END_IF;
IF (schema_prefix + 'MATHS_TUPLE_LITERAL') IN typenames THEN
RETURN (make_finite_space ([expr\maths_tuple_literal.lit_value]));
END_IF;
IF (schema_prefix + 'PARTIAL_DERIVATIVE_EXPRESSION') IN typenames THEN
RETURN (drop_numeric_constraints (values_space_of (
expr\partial_derivative_expression.derivand)));
END_IF;
IF (schema_prefix + 'DEFINITE_INTEGRAL_EXPRESSION') IN typenames THEN
RETURN (drop_numeric_constraints (values_space_of (
expr\definite_integral_expression.integrand)));
END_IF;
RETURN (?);
END_FUNCTION;
END_SCHEMA; -- mathematical_functions_schema