(vl-make-dupeinst-alist-aux x alist) → new-alist
Function:
(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:
(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)