		Search-engine friendly clone of the ACL2 documentation.

Vl-make-dupeinst-alist

Vl-make-dupeinst-alist-aux

Signature
(vl-make-dupeinst-alist-aux x alist) → new-alist
Arguments: x — Guard (vl-modinstlist-p x).; alist — Guard (vl-dupeinst-alistp alist).
Returns: new-alist — Type (vl-dupeinst-alistp new-alist), given the guard.

Definitions and Theorems

Function: vl-make-dupeinst-alist-aux

(defun vl-make-dupeinst-alist-aux (x alist)
 (declare (xargs :guard (and (vl-modinstlist-p x)
                             (vl-dupeinst-alistp alist))))
 (let ((__function__ 'vl-make-dupeinst-alist-aux))
  (declare (ignorable __function__))
  (b*
   (((when (atom x)) alist)
    (x1 (car x))
    ((vl-modinst x1) x1)
    ((when (eq (vl-arguments-kind x1.portargs)
               :vl-arguments-named))
     (and *dupeinst-check-debug*
          (vl-cw-ps-seq
               (vl-cw "~a0: Arguments not resolved, skipping!~%"
                      x1)))
     (vl-make-dupeinst-alist-aux (cdr x)
                                 alist))
    ((mv inputs ?outputs inouts unknowns)
     (vl-partition-plainargs (vl-arguments-plain->args x1.portargs)
                             nil nil nil nil))
    ((unless (and (atom inouts) (atom unknowns)))
     (and
       *dupeinst-check-debug*
       (vl-cw-ps-seq
            (vl-cw "~a0: Arguments too hard (inouts or unknowns).~%"
                   x1)))
     (vl-make-dupeinst-alist-aux (cdr x)
                                 alist))
    (ins (vl-plainarglist->exprs inputs))
    ((when (member nil ins))
     (and
        *dupeinst-check-debug*
        (vl-cw-ps-seq (vl-cw "~a0: Blanks in argument list.~%" x1)))
     (vl-make-dupeinst-alist-aux (cdr x)
                                 alist))
    (ins (vl-exprlist-strip ins))
    (key (make-vl-dupeinst-key :modname x1.modname
                               :inputs ins))
    (look (hons-get key alist))
    (alist (hons-acons key (cons x1 (cdr look))
                       alist)))
   (vl-make-dupeinst-alist-aux (cdr x)
                               alist))))

Theorem: vl-dupeinst-alistp-of-vl-make-dupeinst-alist-aux

(defthm vl-dupeinst-alistp-of-vl-make-dupeinst-alist-aux
  (implies (and (force (vl-modinstlist-p x))
                (force (vl-dupeinst-alistp alist)))
           (b* ((new-alist (vl-make-dupeinst-alist-aux x alist)))
             (vl-dupeinst-alistp new-alist)))
  :rule-classes :rewrite)