		Search-engine friendly clone of the ACL2 documentation.

Duplicate-detect

Vl-duplicate-assign-locations

Signature
(vl-duplicate-assign-locations dupe fixed orig) → matches
Arguments: dupe — Some assign that was duplicated (fixed).
Guard (vl-assign-p dupe).; fixed — Fixed versions of orig.
Guard (vl-assignlist-p fixed).; orig — Original module instances, i.e., before fixing.
Guard (vl-assignlist-p orig).
Returns: matches — Locations of instances matching dupe.
Type (vl-locationlist-p matches), given the guard.

Definitions and Theorems

Function: vl-duplicate-assign-locations

(defun vl-duplicate-assign-locations (dupe fixed orig)
  (declare (xargs :guard (and (vl-assign-p dupe)
                              (vl-assignlist-p fixed)
                              (vl-assignlist-p orig))))
  (declare (xargs :guard (same-lengthp fixed orig)))
  (let ((__function__ 'vl-duplicate-assign-locations))
    (declare (ignorable __function__))
    (b* (((when (atom fixed)) nil)
         (rest (vl-duplicate-assign-locations dupe (cdr fixed)
                                              (cdr orig)))
         ((when (equal dupe (car fixed)))
          (cons (vl-assign->loc (car orig))
                rest)))
      rest)))

Theorem: vl-locationlist-p-of-vl-duplicate-assign-locations

(defthm vl-locationlist-p-of-vl-duplicate-assign-locations
 (implies
     (and (force (vl-assign-p dupe))
          (force (vl-assignlist-p fixed))
          (force (vl-assignlist-p orig))
          (force (same-lengthp fixed orig)))
     (b* ((matches (vl-duplicate-assign-locations dupe fixed orig)))
       (vl-locationlist-p matches)))
 :rule-classes :rewrite)