		Search-engine friendly clone of the ACL2 documentation.

Vl-portlist-p

Vl-collect-interface-ports

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

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

Definitions and Theorems

Function: vl-collect-interface-ports

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

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

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

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

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

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

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

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

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

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

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

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

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

Subtopics

Vl-collect-interface-ports-exec