We build an alist that might associate some of the wires to the lists of wires we think they could be typos of.
(typo-detect-aux strs alist) → typo-alist
Function:
(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)) ((when (or (str::substrp "SDN" name1) (str::substrp "SDF" name1))) (typo-detect-aux (cdr strs) alist)) (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:
(defthm alistp-of-typo-detect-aux (b* ((typo-alist (typo-detect-aux strs alist))) (alistp typo-alist)) :rule-classes :rewrite)
Theorem:
(defthm vl-string-keys-p-of-typo-detect-aux (implies (force (string-listp strs)) (vl-string-keys-p (typo-detect-aux strs alist))))
Theorem:
(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))))