• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
    • Break-rewrite
    • Proof-builder
    • Accumulated-persistence
    • Cgen
    • Forward-chaining-reports
    • Proof-tree
    • Print-gv
    • Dmr
    • With-brr-data
    • Splitter
    • Guard-debug
    • Set-debugger-enable
    • Redo-flat
    • Time-tracker
    • Set-check-invariant-risk
    • Removable-runes
    • Efficiency
    • Explain-near-miss
    • Tail-biting
    • Failed-forcing
    • Sneaky
    • Invariant-risk
    • Failure
    • Measure-debug
    • Dead-events
    • Compare-objects
    • Prettygoals
    • Remove-hyps
    • Type-prescription-debugging
    • Pstack
    • Trace
    • Set-register-invariant-risk
    • Walkabout
    • Disassemble$
    • Nil-goal
    • Cw-gstack
    • Set-guard-msg
    • Find-lemmas
    • Watch
    • Quick-and-dirty-subsumption-replacement-step
    • Profile-all
    • Profile-ACL2
    • Set-print-gv-defaults
    • Minimal-runes
    • Spacewalk
    • Try-gl-concls
    • Near-misses
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Debugging

Compare-objects

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 x and y are two (almost) arbitrary objects but which must both be cons trees for the comparison to be non-trivial. The output (described below) might be confusing if either object contains keywords of the form :<|s...|>, where the ellipsis is the decimal representation of a natural number. For example, the output would be confusing if x or y contained :|<s1>| because compare-objects inserts tokens like that to mark differences.

Compare-objects walks through both objects to detect where corresponding substructures first differ. It replaces differences by the keyword symbols :|<s1>|, :|<s2>|, :|<s3>|, ..., which we call ``placeholders.'' It then assembles a ``legend'' that displays triplets of the form (si xi yi) where si is a placeholder marking a position in the common superstructure of both x and y and xi and yi are the substructures of x and y, respectively, at that position that differ. Compare-objects returns a list consisting of the ``common object'' showing the shared superstructure and the legend.

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 brr command :explain-near-miss sometimes calls compare-objects to show the differences between two unequal quoted constants involved in a mismatch. When :explain-near-miss prettyprints the output of compare-object it does so with an evisc-tuple that simplifies the placeholders. :Explain-near-miss would display the second example above as

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

Compare-objects might be especially helpful when looking at big lambda objects as produced by translating and rewriting loop$ expressions. For example, below we use compare-objects to discover where two large DO$ terms differ.

 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))))

Compare-objects tells us that a position :|<s1>| the first term calls ASSOC-EQ-SAFE while the second one calls ASSOC-EQ.