		Search-engine friendly clone of the ACL2 documentation.

Typo-detection

Typo-detect-aux

We build an alist that might associate some of the wires to the lists of wires we think they could be typos of.

Signature
(typo-detect-aux strs alist) → typo-alist
Arguments: strs — A list of strings, generally the "implicit wires" for a module.
Guard (string-listp strs).; alist — A partitioning alist, generally constructed from the "explicit wires" for the module.
Guard (alistp alist).
Returns: typo-alist — Type (alistp typo-alist).

Definitions and Theorems

Function: typo-detect-aux

(defun typo-detect-aux (strs alist)
  (declare (xargs :guard (and (string-listp strs)
                              (alistp alist))))
  (declare
       (xargs :guard (and (vl-string-keys-p alist)
                          (vl-character-list-list-values-p alist))))
  (let ((__function__ 'typo-detect-aux))
    (declare (ignorable __function__))
    (b* (((when (atom strs)) nil)
         (name1 (car strs))
         (partition1 (typo-partition (explode name1)))
         (typos1 (typo-find-plausible-typos1 partition1 alist))
         ((when typos1)
          (cons (cons name1 typos1)
                (typo-detect-aux (cdr strs) alist))))
      (typo-detect-aux (cdr strs) alist))))

Theorem: alistp-of-typo-detect-aux

(defthm alistp-of-typo-detect-aux
  (b* ((typo-alist (typo-detect-aux strs alist)))
    (alistp typo-alist))
  :rule-classes :rewrite)

Theorem: vl-string-keys-p-of-typo-detect-aux

(defthm vl-string-keys-p-of-typo-detect-aux
  (implies (force (string-listp strs))
           (vl-string-keys-p (typo-detect-aux strs alist))))

Theorem: vl-string-list-values-p-of-typo-detect-aux

(defthm vl-string-list-values-p-of-typo-detect-aux
  (implies (force (vl-string-keys-p alist))
           (vl-string-list-values-p (typo-detect-aux strs alist))))