(vl-nameclash-warning-summary name locals imports) → summary
Function:
(defun vl-nameclash-warning-summary (name locals imports) (declare (xargs :guard (and (stringp name) (vl-scopeitem-alist-p locals) (vl-importresult-alist-p imports)))) (let ((__function__ 'vl-nameclash-warning-summary)) (declare (ignorable __function__)) (b* ((name (string-fix name)) (locals (vl-scopeitem-alist-fix locals)) (imports (vl-importresult-alist-fix imports)) (localdecls (vl-nameclash-collect-local-decls name locals)) (importdecls (vl-nameclash-collect-import-decls name imports)) (clashdecls (append localdecls importdecls)) ((unless (<= 2 (len clashdecls))) (raise "Programming error -- not actually a name clash? ~x0~%" name) "") (decl1 (first clashdecls)) (decl2 (second clashdecls)) (decl1.loc (if (eq (tag decl1) :vl-import) (vl-import->loc decl1) (vl-scopeitem->loc decl1))) (decl2.loc (if (eq (tag decl2) :vl-import) (vl-import->loc decl2) (vl-scopeitem->loc decl2)))) (with-local-ps (vl-ps-update-autowrap-col 100) (vl-ps-update-autowrap-ind 10) (vl-print "name clash for ") (vl-print-str name) (vl-println ":") (vl-indent 6) (vl-print " // From ") (vl-print-loc decl1.loc) (vl-println "") (vl-indent 6) (vl-cw "~a0~%" decl1) (vl-indent 6) (vl-print " // From ") (vl-print-loc decl2.loc) (vl-println "") (vl-indent 6) (vl-cw "~a0~%" decl2) (if (atom (cddr clashdecls)) ps (vl-ps-seq (vl-println "") (vl-indent 6) (vl-print " // And ") (vl-print-nat (- (len clashdecls) 2)) (vl-print " more (not shown).")))))))
Theorem:
(defthm stringp-of-vl-nameclash-warning-summary (b* ((summary (vl-nameclash-warning-summary name locals imports))) (stringp summary)) :rule-classes :type-prescription)
Theorem:
(defthm vl-nameclash-warning-summary-of-str-fix-name (equal (vl-nameclash-warning-summary (str-fix name) locals imports) (vl-nameclash-warning-summary name locals imports)))
Theorem:
(defthm vl-nameclash-warning-summary-streqv-congruence-on-name (implies (streqv name name-equiv) (equal (vl-nameclash-warning-summary name locals imports) (vl-nameclash-warning-summary name-equiv locals imports))) :rule-classes :congruence)
Theorem:
(defthm vl-nameclash-warning-summary-of-vl-scopeitem-alist-fix-locals (equal (vl-nameclash-warning-summary name (vl-scopeitem-alist-fix locals) imports) (vl-nameclash-warning-summary name locals imports)))
Theorem:
(defthm vl-nameclash-warning-summary-vl-scopeitem-alist-equiv-congruence-on-locals (implies (vl-scopeitem-alist-equiv locals locals-equiv) (equal (vl-nameclash-warning-summary name locals imports) (vl-nameclash-warning-summary name locals-equiv imports))) :rule-classes :congruence)
Theorem:
(defthm vl-nameclash-warning-summary-of-vl-importresult-alist-fix-imports (equal (vl-nameclash-warning-summary name locals (vl-importresult-alist-fix imports)) (vl-nameclash-warning-summary name locals imports)))
Theorem:
(defthm vl-nameclash-warning-summary-vl-importresult-alist-equiv-congruence-on-imports (implies (vl-importresult-alist-equiv imports imports-equiv) (equal (vl-nameclash-warning-summary name locals imports) (vl-nameclash-warning-summary name locals imports-equiv))) :rule-classes :congruence)