Further fix for bug in directed-untranslate partially addressed in pr…

…eceding commit.
acl2 · Apr 20, 2018 · 6b7996f · 6b7996f
1 parent 9d95d3e
commit 6b7996f
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 10 deletions.
diff --git a/books/kestrel/utilities/directed-untranslate.lisp b/books/kestrel/utilities/directed-untranslate.lisp
@@ -1653,11 +1653,11 @@
                                                         iff-flg lflg exec-p wrld)))
                         (('if x1 x1-alt x2)
                          (and (eq (car uterm) 'or) ; tterm is (if x1' & x2')
-                              (or (equal x1-alt x1)
-                                  (and iff-flg
-                                       (equal x1-alt *t*)))
                               (cond
-                               ((cddr uterm) ; tterm is (if x1' & x2')
+                               ((and (or (equal x1-alt x1)
+                                         (and iff-flg
+                                              (equal x1-alt *t*)))
+                                     (cddr uterm)) ; tterm is (if x1' & x2')
                                 (untranslate-or
                                  (directed-untranslate-rec (cadr uterm)
                                                            (fargn tterm 1)
@@ -1667,12 +1667,16 @@
                                                            (fargn tterm 3)
                                                            x2 iff-flg lflg
                                                            exec-p wrld)))
+                               ((cddr uterm) ; uterm is (or x y ...)
+                                (directed-untranslate-rec (or-macro (cdr uterm))
+                                                          tterm sterm iff-flg lflg
+                                                          exec-p wrld))
                                ((cdr uterm) ; uterm is (or x)
                                 (directed-untranslate-rec (cadr uterm)
-                                                          tterm sterm t lflg
+                                                          tterm sterm iff-flg lflg
                                                           exec-p wrld))
                                (t ; uterm is (or)
-                                (directed-untranslate-rec t tterm sterm t lflg
+                                (directed-untranslate-rec t tterm sterm iff-flg lflg
                                                           exec-p wrld)))))
                         (('if x1 x2 *t*)
                          (and (eq (car uterm) 'or)

diff --git a/books/workshops/2017/coglio-kaufmann-smith/support/simplify-defun-tests.lisp b/books/workshops/2017/coglio-kaufmann-smith/support/simplify-defun-tests.lisp
@@ -1626,7 +1626,7 @@
      (DECLARE (XARGS :NORMALIZE NIL
                      :GUARD T
                      :VERIFY-GUARDS NIL))
-     (OR (SYMBOLP X) (+ 1 1 Y)))
+     (IF (SYMBOLP X) T (+ 1 1 Y)))
    (DEFUN F2{2} (X Y)
      (DECLARE (XARGS :NORMALIZE NIL
                      :GUARD T
@@ -1636,7 +1636,7 @@
      (DECLARE (XARGS :NORMALIZE NIL
                      :GUARD T
                      :VERIFY-GUARDS NIL))
-     (OR (SYMBOLP X) (+ 2 Y))))
+     (IF (SYMBOLP X) T (+ 2 Y))))
 
 ; A duplicate @-var is OK as long as all occurrences match the same term.  But
 ; the different terms may simplify differently because they are in different
@@ -1982,7 +1982,7 @@
                      :GUARD T
                      :VERIFY-GUARDS NIL))
      (IF (TRUE-LISTP X)
-         (OR (EQL (LEN X) 17) Y)
+         (IF (EQL (LEN X) 17) T Y)
          'DONT-CARE)))
 
   ;; Pattern is actually (if @1 @1 _), so this time the entire body is not
@@ -1997,7 +1997,7 @@
                      :GUARD T
                      :VERIFY-GUARDS NIL))
      (IF (TRUE-LISTP (CONS 3 X))
-         (OR (EQL (LEN X) 17) Y)
+         (IF (EQL (LEN X) 17) T Y)
          'DONT-CARE))))
 
 ;; Matching a specified subterm that has only part of it specified as a