		Search-engine friendly clone of the ACL2 documentation.

Vl-convert-namedargs

Vl-find-namedarg

Look up an argument by name in a named argument list.

Signature
(vl-find-namedarg name args) → *
Arguments: name — Guard (stringp name).; args — Guard (vl-namedarglist-p args).

We once used some fast-alist stuff here, but now I think that it isn't worthwhile since most module instances either have relatively few arguments or are instantiated infrequently. It'd be easy enough to write an version that uses fast-alists when there are many arguments if performance becomes a problem.

Definitions and Theorems

Function: vl-find-namedarg

(defun vl-find-namedarg (name args)
  (declare (xargs :guard (and (stringp name)
                              (vl-namedarglist-p args))))
  (let ((__function__ 'vl-find-namedarg))
    (declare (ignorable __function__))
    (cond ((atom args) nil)
          ((equal (vl-namedarg->name (car args))
                  name)
           (vl-namedarg-fix (car args)))
          (t (vl-find-namedarg name (cdr args))))))

Theorem: vl-find-namedarg-under-iff

(defthm vl-find-namedarg-under-iff
  (iff (vl-find-namedarg name args)
       (member-equal name (vl-namedarglist->names args))))

Theorem: vl-namedarg-p-of-vl-find-namedarg

(defthm vl-namedarg-p-of-vl-find-namedarg
  (equal (vl-namedarg-p (vl-find-namedarg name args))
         (if (member-equal name (vl-namedarglist->names args))
             t
           nil)))

Theorem: vl-find-namedarg-of-vl-namedarglist-fix-args

(defthm vl-find-namedarg-of-vl-namedarglist-fix-args
  (equal (vl-find-namedarg name (vl-namedarglist-fix args))
         (vl-find-namedarg name args)))

Theorem: vl-find-namedarg-vl-namedarglist-equiv-congruence-on-args

(defthm vl-find-namedarg-vl-namedarglist-equiv-congruence-on-args
  (implies (vl-namedarglist-equiv args args-equiv)
           (equal (vl-find-namedarg name args)
                  (vl-find-namedarg name args-equiv)))
  :rule-classes :congruence)