From 2e0f088b05c4f67274830d80f4e282fe15b9ab53 Mon Sep 17 00:00:00 2001 From: Kris Katterjohn Date: Sun, 13 Nov 2022 00:11:05 -0500 Subject: [PATCH] Change the translation of # to avoid the problematic TRP-NOT The translation of # is the last user of TRP-NOT (see commits cf7c667c and f7b46967 for more on TRP-NOT). Instead of wrapping the translation of = in a call to TRP-NOT, let's just translate # as the logical negation of =. Then we can just remove TRP-NOT. 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 | 7 +++++++ 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/src/trpred.lisp b/src/trpred.lisp index d2acfd5cb..b5abcc22c 100644 --- a/src/trpred.lisp +++ b/src/trpred.lisp @@ -204,6 +204,9 @@ `(eql ,arg1 ,arg2) `(like ,arg1 ,arg2))))) +(defun trp-mnotequal (form) + (translate-predicate `((mnot) ((mequal) ,@(cdr form))))) + (defun trp-$equality (args lisp-op max-op) (let* ((arg1 (translate (car args))) (arg2 (translate (cadr args))) @@ -221,16 +224,6 @@ (defun trp-$notequal (form) (trp-$equality (cdr form) '/= 'mnqp)) -;; Logical not for predicates. Do the expected thing, except return -(defun trp-not (val) - (case val - ((t) nil) - ((nil) t) - (otherwise val))) - -(defun trp-mnotequal (form) - (cons '$any (list 'trp-not (cdr (trp-mequal 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 0ec6aec93..62eabc457 100644 --- a/tests/rtest_translator.mac +++ b/tests/rtest_translator.mac @@ -2690,6 +2690,13 @@ block ([translate : false, l1, l2], pr (not not (x > 1)), pr (not not (x >= 1)), + pr (x = 1), + pr (x # 1), + pr (not (x = 1)), + pr (not (x # 1)), + pr (not not (x = 1)), + pr (not not (x # 1)), + pr (equal (x, 1)), pr (notequal (x, 1)), pr (not equal (x, 1)), -- 2.11.4.GIT