show differences between two ACL2 objects

In theorem prover output it can sometimes be difficult to see where two Lisp objects differ. (Emacs' compare-windows can often help.) This function is an attempt to help while remaining entirely in ACL2.

General Form: (compare-objects x y)

where

For example,

ACL2 !>(compare-objects '(a b c) '(a b . c)) ((:OBJ (A B . :|<s1>|)) (:LEGEND ((:|<s1>| (C) C)))) ACL2 !>(compare-objects '(f x y (g x '(a b c))) '(f y x (g x '(a b c . d)))) ((:OBJ (F :|<s1>| :|<s2>| (G X '(A B C . :|<s3>|)))) (:LEGEND ((:|<s1>| X Y) (:|<s2>| Y X) (:|<s3>| NIL D))))

By the way, the `explain-near-miss` sometimes
calls `evisc-tuple` that
simplifies the placeholders.

((:OBJ '(F <s1> <s2> (G X '(A B C . <s3>)))) (:LEGEND ((<s1> X Y) (<s2> Y X) (<s3> NIL D)))).

`loop$`
expressions. For example, below we use

ACL2 !>(compare-objects '(DO$ ; First term '(LAMBDA (ALIST) (ACL2-COUNT (CDR (ASSOC-EQ-SAFE 'LST ALIST)))) (CONS (CONS 'LST LST0) '((ANS . 0))) '(LAMBDA (ALIST) (IF (ENDP (CDR (ASSOC-EQ-SAFE 'LST ALIST))) (CONS ':RETURN (CONS (CDR (ASSOC-EQ-SAFE 'ANS ALIST)) (CONS (CONS (CONS 'LST (CDR (ASSOC-EQ-SAFE 'LST ALIST))) (CONS (CONS 'ANS (CDR (ASSOC-EQ-SAFE 'ANS ALIST))) 'NIL)) 'NIL))) (CONS 'NIL (CONS 'NIL (CONS (CONS (CONS 'LST (CDR (CDR (ASSOC-EQ-SAFE 'LST ALIST)))) (CONS (CONS 'ANS (BINARY-+ '1 (CDR (ASSOC-EQ-SAFE 'ANS ALIST)))) 'NIL)) 'NIL))))) '(LAMBDA (ALIST) (CONS 'NIL (CONS 'NIL (CONS (CONS (CONS 'LST (CDR (ASSOC-EQ-SAFE 'LST ALIST))) (CONS (CONS 'ANS (CDR (ASSOC-EQ-SAFE 'ANS ALIST))) 'NIL)) 'NIL)))) '(NIL) 'NIL) '(DO$ ; Second term '(LAMBDA (ALIST) (ACL2-COUNT (CDR (ASSOC-EQ-SAFE 'LST ALIST)))) (CONS (CONS 'LST LST0) '((ANS . 0))) '(LAMBDA (ALIST) (IF (ENDP (CDR (ASSOC-EQ-SAFE 'LST ALIST))) (CONS ':RETURN (CONS (CDR (ASSOC-EQ-SAFE 'ANS ALIST)) (CONS (CONS (CONS 'LST (CDR (ASSOC-EQ-SAFE 'LST ALIST))) (CONS (CONS 'ANS (CDR (ASSOC-EQ-SAFE 'ANS ALIST))) 'NIL)) 'NIL))) (CONS 'NIL (CONS 'NIL (CONS (CONS (CONS 'LST (CDR (CDR (ASSOC-EQ-SAFE 'LST ALIST)))) (CONS (CONS 'ANS (BINARY-+ '1 (CDR (ASSOC-EQ 'ANS ALIST)))) 'NIL)) 'NIL))))) '(LAMBDA (ALIST) (CONS 'NIL (CONS 'NIL (CONS (CONS (CONS 'LST (CDR (ASSOC-EQ-SAFE 'LST ALIST))) (CONS (CONS 'ANS (CDR (ASSOC-EQ-SAFE 'ANS ALIST))) 'NIL)) 'NIL)))) '(NIL) 'NIL)) ((:OBJ (DO$ '(LAMBDA (ALIST) (ACL2-COUNT (CDR (ASSOC-EQ-SAFE 'LST ALIST)))) (CONS (CONS 'LST LST0) '((ANS . 0))) '(LAMBDA (ALIST) (IF (ENDP (CDR (ASSOC-EQ-SAFE 'LST ALIST))) (CONS ':RETURN (CONS (CDR (ASSOC-EQ-SAFE 'ANS ALIST)) (CONS (CONS (CONS 'LST (CDR (ASSOC-EQ-SAFE 'LST ALIST))) (CONS (CONS 'ANS (CDR (ASSOC-EQ-SAFE 'ANS ALIST))) 'NIL)) 'NIL))) (CONS 'NIL (CONS 'NIL (CONS (CONS (CONS 'LST (CDR (CDR (ASSOC-EQ-SAFE 'LST ALIST)))) (CONS (CONS 'ANS (BINARY-+ '1 (CDR (:|<s1>| 'ANS ALIST)))) 'NIL)) 'NIL))))) '(LAMBDA (ALIST) (CONS 'NIL (CONS 'NIL (CONS (CONS (CONS 'LST (CDR (ASSOC-EQ-SAFE 'LST ALIST))) (CONS (CONS 'ANS (CDR (ASSOC-EQ-SAFE 'ANS ALIST))) 'NIL)) 'NIL)))) '(NIL) 'NIL)) (:LEGEND ((:|<s1>| ASSOC-EQ-SAFE ASSOC-EQ))))