FUNCTION simplify_function_application

(* SCHEMA mathematical_functions_schema; *)
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;  -- simplify_function_application

Referenced By

Defintion simplify_function_application is references by the following definitions:
DefinitionType
 simplify_generic_expression FUNCTION


[Top Level Definitions] [Exit]

Generated by STEP Tools® EXPRESS to HTML Converter
2012-03-27T17:13:59-04:00