		Search-engine friendly clone of the ACL2 documentation.

Vl-portlist-p

Vl-collect-regular-ports

Filter a vl-portlist-p to collect only the regular ports.

Signature
(vl-collect-regular-ports x) → ifports
Arguments: x — Guard (vl-portlist-p x).
Returns: ifports — Type (and (vl-portlist-p ifports) (vl-regularportlist-p ifports)).

Definitions and Theorems

Function: vl-collect-regular-ports

(defun vl-collect-regular-ports (x)
 (declare (xargs :guard (vl-portlist-p x)))
 (let ((__function__ 'vl-collect-regular-ports))
  (declare (ignorable __function__))
  (mbe
      :logic
      (b* (((when (atom x)) nil)
           (x1 (vl-port-fix (car x)))
           ((when (eq (tag x1) :vl-regularport))
            (cons x1 (vl-collect-regular-ports (cdr x)))))
        (vl-collect-regular-ports (cdr x)))
      :exec
      (if (atom x)
          nil
        (with-local-nrev (vl-collect-regular-ports-exec x nrev))))))

Theorem: return-type-of-vl-collect-regular-ports

(defthm return-type-of-vl-collect-regular-ports
  (b* ((ifports (vl-collect-regular-ports x)))
    (and (vl-portlist-p ifports)
         (vl-regularportlist-p ifports)))
  :rule-classes :rewrite)

Theorem: vl-collect-regular-ports-exec-removal

(defthm vl-collect-regular-ports-exec-removal
  (equal (vl-collect-regular-ports-exec x nrev)
         (append nrev (vl-collect-regular-ports x))))

Theorem: vl-collect-regular-ports-when-atom

(defthm vl-collect-regular-ports-when-atom
  (implies (atom x)
           (equal (vl-collect-regular-ports x)
                  nil)))

Theorem: vl-collect-regular-ports-of-cons

(defthm vl-collect-regular-ports-of-cons
  (equal (vl-collect-regular-ports (cons a x))
         (if (eq (tag (vl-port-fix a))
                 :vl-regularport)
             (cons (vl-port-fix a)
                   (vl-collect-regular-ports x))
           (vl-collect-regular-ports x))))

Theorem: vl-collect-regular-ports-of-vl-portlist-fix-x

(defthm vl-collect-regular-ports-of-vl-portlist-fix-x
  (equal (vl-collect-regular-ports (vl-portlist-fix x))
         (vl-collect-regular-ports x)))

Theorem: vl-collect-regular-ports-vl-portlist-equiv-congruence-on-x

(defthm vl-collect-regular-ports-vl-portlist-equiv-congruence-on-x
  (implies (vl-portlist-equiv x x-equiv)
           (equal (vl-collect-regular-ports x)
                  (vl-collect-regular-ports x-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-collect-regular-ports-exec