From cf7c667c46ec8d4c1d53b9e88c1f81cc8be4b091 Mon Sep 17 00:00:00 2001
From: Kris Katterjohn <katterjohn@gmail.com>
Date: Sat, 12 Nov 2022 23:52:51 -0500
Subject: [PATCH] Fix the bogus translations of <= and >=

The translation of <= has been similar to > followed by not (TRP-NOT),
and similarly the translation of >= has been similar to < followed by
not.  This is wrong:

(%i1) foo () := is (%i <= 1)$

(%i2) foo ();
(%o2) false

(%i3) translate (foo)$

(%i4) foo ();
(%o4) true

Also the translator basically assumed that prederror would be true.
The way the not used here was implemented (TRP-NOT), it would behave
like NOT when given a boolean value but otherwise it would simply
return its argument unchanged.  This is not a problem for is/maybe,
but after an upcoming commit (to make if honor prederror) this could
lead to bogus results in conditionals when prederror is false.

Now we translate <= and >= directly, using TRP-INEQUALITY (introduced
in commit 7f12bb7f).

No problems with the test suite, share test suite or rtest_translator.
New tests have been added to rtest_translator.
---
 src/trpred.lisp            | 13 ++++++------
 tests/rtest_translator.mac | 53 ++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 60 insertions(+), 6 deletions(-)

diff --git a/src/trpred.lisp b/src/trpred.lisp
index 04a7c7c54..f9241b9d8 100644
--- a/src/trpred.lisp
+++ b/src/trpred.lisp
@@ -189,6 +189,13 @@
 (defun trp-mgreaterp (form)
   (trp-inequality (cdr form) '> 'mgrp))
 
+(defun trp-mgeqp (form)
+  (trp-inequality (cdr form) '>= 'mgqp))
+
+(defun trp-mleqp (form)
+  ; No mlqp in sight
+  (translate-predicate `((mgeqp) ,@(reverse (cdr form)))))
+
 (defun trp-mequal (form) 
   (destructuring-let (((mode1 . arg1) (translate (cadr form)))
                       ((mode2 . arg2) (translate (caddr form))))
@@ -221,12 +228,6 @@
 (defun trp-mnotequal (form)
   (cons '$any (list 'trp-not (cdr (trp-mequal form)))))
 
-(defun trp-mgeqp (form)
-  (cons '$any (list 'trp-not (cdr (trp-mlessp form)))))
-
-(defun trp-mleqp (form)
-  (cons '$any (list 'trp-not (cdr (trp-mgreaterp form)))))
-
 ;;; sigh, i have to copy a lot of the $assume function too.
 
 (def%tr $assume (form)
diff --git a/tests/rtest_translator.mac b/tests/rtest_translator.mac
index 9d4381af2..80f92b91b 100644
--- a/tests/rtest_translator.mac
+++ b/tests/rtest_translator.mac
@@ -2669,6 +2669,59 @@ true;
 (kill (foo, bar), 0);
 0;
 
+block ([translate : false, l1, l2],
+  local (test, make_fun),
+
+  make_fun (name, pr) ::=
+    buildq ([name, pr],
+      name (x) :=
+        [pr (x <  1),
+         pr (x <= 1),
+         pr (x >  1),
+         pr (x >= 1),
+
+         pr (not (x <  1)),
+         pr (not (x <= 1)),
+         pr (not (x >  1)),
+         pr (not (x >= 1)),
+
+         pr (not not (x <  1)),
+         pr (not not (x <= 1)),
+         pr (not not (x >  1)),
+         pr (not not (x >= 1))]),
+
+  make_fun (foo, is),
+  make_fun (bar, maybe),
+
+  test () :=
+    block ([res : []],
+      block ([prederror : true],
+        push (errcatch (foo ('z)), res)),
+      block ([prederror : false,
+              l : [0, 0.0, 0.0b0,
+                   1, 1.0, 1.0b0,
+                   2, 2.0, 2.0b0,
+                   %i, 1.0 * %i, 1.0b0 * %i,
+                   2 * %i, 2.0 * %i, 2.0b0 * %i,
+                   true, false,
+                   'z, 'z ()]],
+        for x in l do (
+          push (foo (x), res),
+          push (bar (x), res))),
+      res),
+
+  l1 : test (),
+
+  translate_or_lose (foo, bar),
+
+  l2 : test (),
+
+  is (l1 = l2));
+true;
+
+(kill (foo, bar), 0);
+0;
+
 
 
 
-- 
2.11.4.GIT