share/contrib/boolsimp/rtest_boolsimp.mac

   1 /* Plotting examples -- try these by hand.
   2 plot2d (if x > 1 then log(x) else exp(x), [x, -1, 3]);
   3 f(x) := if x < 0 then -x else sqrt(x);
   4 plot2d (f(x), [x, -2, 2]);
   5  */
   6
   7 (kill (all), load (boolsimp), 0);
   8 0;
   9
  10 /* Test 'if (noun).
  11  */
  12 (expr: if a > b then if a > c then a else d else if b > c then b else c, 0);
  13 0;
  14
  15 (assume (a > b), ev (expr));
  16 '(if a > c then a else d);
  17
  18 (forget (a > b), assume (a > c), ev (expr));
  19 '(if a > b then if a > c then a else d else if b > c then b else c);
  20
  21 block ([x : 17, y : 29], block ([a : 100, b : 'x + 'y, c : x, d : y], ev (expr)));
  22 '(if 100 > x + y then if 100 > 17 then 100 else 29 else if x + y > 17 then x + y else 17);
  23
  24 (forget (a > c), ev (expr));
  25 '(if a > b then (if a > c then a else d) else (if b > c then b else c));
  26
  27 (assume (b < c), ev (expr));
  28 '(if a > b then (if a > c then a else d) else (if b > c then b else c));
  29
  30 (assume (a > c), ev (expr));
  31 a;
  32
  33 (apply (forget, facts ()), []);
  34 [];
  35
  36 (foo (x) := if numberp (x) then if oddp (x) and x > 100 then 'foop (x) else 'nofoop (x)
  37   else 'if 'oddp (x) and x > 100 then 'foop (x) else 'nofoop (x), 0);
  38 0;
  39
  40 foo (17);
  41 'nofoop (17);
  42
  43 foo (117);
  44 'foop (117);
  45
  46 foo (x + y);
  47 'if 'oddp (x + y) and x + y > 100 then 'foop (x + y) else 'nofoop (x + y);
  48
  49 (assume (x < 0, y < 0), foo (x + y));
  50 'nofoop (x + y);
  51
  52 /* assume fails to deduce x + y > 100 given x + y > 1000, oh well.
  53  * (forget (x < 0, y < 0), assume (x + y > 1000), foo (x + y));
  54  */
  55 (forget (x < 0, y < 0), assume (x > 200), foo (x - 50));
  56 'if 'oddp (x - 50) then 'foop (x - 50) else 'nofoop (x - 50);
  57
  58 /* Some examples devised by Stavros Macrakis */
  59
  60 (apply (forget, facts ()), kill (all), 0);
  61 0;
  62
  63 pp: if x > 0 then print(1) else print(2);
  64 '(if x > 0 then print(1) else print(2));
  65
  66 ''pp, x=1;
  67 1;
  68
  69 ''pp, x= -1;
  70 2;
  71
  72 (f (x, y) := if equal (y, 0) then 0 else 1/x, [f (8, n), f (m, 7)]);
  73 [if equal (n, 0) then 0 else 1/8, 1/m];
  74
  75 /* if equal (y, 0) then 0 else 1/0; => division by zero in simplification */
  76 errcatch (f (0, y));
  77 [];
  78
  79 (f(x) := if x <= 0 then 1 else x*f(x - 1), fy : f(y));
  80 '(if y <= 0 then 1 else y*f(y - 1));
  81
  82 ''fy, y=8;
  83 40320;
  84
  85 if equal (x, 0) then 1 else 1/x, x=0;
  86 1;
  87
  88 /* Further examples in the same vein */
  89
  90 pp: if x > 0 then qq1: 1 else qq2: 2;
  91 '(if x > 0 then qq1: 1 else qq2: 2);
  92
  93 (kill (qq1, qq2), ev (pp, x=1));
  94 1;
  95
  96 [qq1, qq2];
  97 [1, 'qq2];
  98
  99 (kill (qq1, qq2), ev (pp, x= -1));
 100 2;
 101
 102 [qq1, qq2];
 103 ['qq1, 2];
 104
 105 block ([aa : 2, bb : 3, cc], if cc > 1 then if aa > 0 then 10*aa else -10*aa else if bb > 0 then bb^2 else -bb^2);
 106 '(if cc > 1 then (if 2 > 0 then 20 else -20) else (if 3 > 0 then 9 else -9));
 107
 108 block ([aa : 2, bb : 3, cc], if cc > 1 and aa > 0 then 10*aa elseif cc > 1 and not aa > 0 then -10*aa elseif  not cc > 1 and  bb > 0 then bb^2 elseif not cc > 1 and not bb > 0 then -bb^2);
 109 '(if cc > 1 then 20 elseif cc <= 1 then 9);
 110
 111 print(FOO) or print(BAR); /* should print "FOO" and "BAR" on successive lines */
 112 FOO or BAR;
 113
 114 print(true) or print(false); /* should print "true" */
 115 true;
 116
 117 (push (a, L) ::= buildq ([a, L], L : cons (a, L)), 0);
 118 0;
 119
 120 (L : [], push (FOO, L) or push (BAR, L));
 121 [FOO] or [BAR, FOO];
 122
 123 L;
 124 [BAR, FOO];
 125
 126 (L : [], '(push (FOO, L) or push (BAR, L)), [op(%%), op(first(%%)), args(first(%%)), op(second(%%)), args(second(%%))]);
 127 ["or", push, '[FOO, L], push, '[BAR, L]];
 128
 129 L;
 130 [];
 131
 132 /* Should find that aa or bb or cc ... is equivalent to
 133  * (is(aa), if %% then %% else (is(bb), if %% then %% else (is(cc), if %% then %% else ...)))
 134  * when all aa, bb, cc, ... evaluate to true or false.
 135  */
 136
 137 (L : [], first (push (false, L)) or first (push (true, L)) or first (push (true, L)), [%%, L]);
 138 [true, [true, false]];
 139
 140 (L : [], (is(first (push (false, L))), if %% then %% else (is(first (push (true, L))), if %% then %% else (is(first (push (true, L))), if %% then %%))), [%%, L]);
 141 [true, [true, false]];
 142
 143 /* Translation of conditionals and boolean expressions.
 144  * Translating this file (rtest_boolsimp.mac) would be a good test,
 145  * but the translator is too broken to translate all of the file.
 146  */
 147
 148 /* Leave this mode_declare for later.
 149  * The effect which would be observable here would be
 150  * to trigger an error if some argument is not true or false.
 151  * But as it stands, the translation code doesn't exploit
 152  * the boolean mode_declare in any way.
 153 mode_declare ([a%, b%, c%, d%], boolean);
 154 [[a%, b%, c%, d%]];
 155  */
 156
 157 /* Example from mailing list 2006/05/04, tnx Barton */
 158
 159 (kill(blurf), blurf(x) := if x < 0 then -1 else 1, 0);
 160 0;
 161
 162 blurf(a);
 163 'if a < 0 then -1 else 1;
 164
 165 (translate(blurf), blurf(a));
 166 'if a < 0 then -1 else 1;
 167
 168 /* Other examples of translated functions */
 169
 170 (my_max (x, y, z) := if x > y and x > z then x elseif y > z then y else z, translate (my_max));
 171 [my_max];
 172
 173 my_max (11, 33, 22);
 174 33;
 175
 176 my_max (a + b, c, 1);
 177 'if a + b > c and a + b > 1 then a + b elseif c > 1 then c else 1;
 178
 179 [assume (c < 1), my_max (a + b, c, 1), forget (c < 1)];
 180 [[c < 1], 'if a + b > c and a + b > 1 then a + b else 1, [c < 1]];
 181
 182 /* explicit resimplification in evaluation (i.e. DEFMSPEC MCOND) not needed,
 183  * since simplification of branches will be handled after evaluation.
 184  */
 185 (kill (a, b, c), b:2, c:2, if a > 0 then b + c else b - c);
 186 if a > 0 then 4 else 0;
 187