		Search-engine friendly clone of the ACL2 documentation.

Nameclash

Vl-nameclash-warning-summary

Signature
(vl-nameclash-warning-summary name locals imports) → summary
Arguments: name — Guard (stringp name).; locals — Guard (vl-scopeitem-alist-p locals).; imports — Guard (vl-importresult-alist-p imports).
Returns: summary — Type (stringp summary).

Definitions and Theorems

Function: vl-nameclash-warning-summary

(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: stringp-of-vl-nameclash-warning-summary

(defthm stringp-of-vl-nameclash-warning-summary
  (b* ((summary (vl-nameclash-warning-summary name locals imports)))
    (stringp summary))
  :rule-classes :type-prescription)

Theorem: vl-nameclash-warning-summary-of-str-fix-name

(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: vl-nameclash-warning-summary-streqv-congruence-on-name

(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: vl-nameclash-warning-summary-of-vl-scopeitem-alist-fix-locals

(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: vl-nameclash-warning-summary-vl-scopeitem-alist-equiv-congruence-on-locals

(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: vl-nameclash-warning-summary-of-vl-importresult-alist-fix-imports

(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: vl-nameclash-warning-summary-vl-importresult-alist-equiv-congruence-on-imports

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