		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-typo-detect1

Signature
(vl-lucid-typo-detect1 ss possible-typos reportcard) → reportcard
Arguments: ss — Scope where these possible typos occur.
Guard (vl-scopestack-p ss).; possible-typos — Names of suspiciously unused/unset implicit wires.
Guard (string-listp possible-typos).; reportcard — Reportcard to extend with actual warnings.
Guard (vl-reportcard-p reportcard).
Returns: reportcard — Type (vl-reportcard-p reportcard).

Definitions and Theorems

Function: vl-lucid-typo-detect1

(defun vl-lucid-typo-detect1 (ss possible-typos reportcard)
 (declare (xargs :guard (and (vl-scopestack-p ss)
                             (string-listp possible-typos)
                             (vl-reportcard-p reportcard))))
 (let ((__function__ 'vl-lucid-typo-detect1))
   (declare (ignorable __function__))
   (b*
    ((possible-typos (mergesort (string-list-fix possible-typos)))
     (good-names
          (difference (vl-scopestack->flat-transitive-names-slow ss)
                      possible-typos))
     (typo-alist (typo-detect possible-typos good-names))
     (warnings (vl-possible-typo-warnings typo-alist))
     (topname (vl-scopestack->topname ss))
     (reportcard
          (vl-extend-reportcard-list topname warnings reportcard)))
    reportcard)))

Theorem: vl-reportcard-p-of-vl-lucid-typo-detect1

(defthm vl-reportcard-p-of-vl-lucid-typo-detect1
  (b* ((reportcard
            (vl-lucid-typo-detect1 ss possible-typos reportcard)))
    (vl-reportcard-p reportcard))
  :rule-classes :rewrite)

Theorem: vl-lucid-typo-detect1-of-vl-scopestack-fix-ss

(defthm vl-lucid-typo-detect1-of-vl-scopestack-fix-ss
  (equal (vl-lucid-typo-detect1 (vl-scopestack-fix ss)
                                possible-typos reportcard)
         (vl-lucid-typo-detect1 ss possible-typos reportcard)))

Theorem: vl-lucid-typo-detect1-vl-scopestack-equiv-congruence-on-ss

(defthm vl-lucid-typo-detect1-vl-scopestack-equiv-congruence-on-ss
 (implies
   (vl-scopestack-equiv ss ss-equiv)
   (equal
        (vl-lucid-typo-detect1 ss possible-typos reportcard)
        (vl-lucid-typo-detect1 ss-equiv possible-typos reportcard)))
 :rule-classes :congruence)

Theorem: vl-lucid-typo-detect1-of-string-list-fix-possible-typos

(defthm vl-lucid-typo-detect1-of-string-list-fix-possible-typos
  (equal (vl-lucid-typo-detect1 ss (string-list-fix possible-typos)
                                reportcard)
         (vl-lucid-typo-detect1 ss possible-typos reportcard)))

Theorem: vl-lucid-typo-detect1-string-list-equiv-congruence-on-possible-typos

(defthm
 vl-lucid-typo-detect1-string-list-equiv-congruence-on-possible-typos
 (implies
   (str::string-list-equiv possible-typos possible-typos-equiv)
   (equal
        (vl-lucid-typo-detect1 ss possible-typos reportcard)
        (vl-lucid-typo-detect1 ss possible-typos-equiv reportcard)))
 :rule-classes :congruence)

Theorem: vl-lucid-typo-detect1-of-vl-reportcard-fix-reportcard

(defthm vl-lucid-typo-detect1-of-vl-reportcard-fix-reportcard
  (equal (vl-lucid-typo-detect1 ss possible-typos
                                (vl-reportcard-fix reportcard))
         (vl-lucid-typo-detect1 ss possible-typos reportcard)))

Theorem: vl-lucid-typo-detect1-vl-reportcard-equiv-congruence-on-reportcard

(defthm
 vl-lucid-typo-detect1-vl-reportcard-equiv-congruence-on-reportcard
 (implies
   (vl-reportcard-equiv reportcard reportcard-equiv)
   (equal
        (vl-lucid-typo-detect1 ss possible-typos reportcard)
        (vl-lucid-typo-detect1 ss possible-typos reportcard-equiv)))
 :rule-classes :congruence)