		Search-engine friendly clone of the ACL2 documentation.

Sv-ansi-port-interpretation

Vl-process-subsequent-ansi-ports

Signature
(vl-process-subsequent-ansi-ports x prev-ifacep warnings ports-acc portdecls-acc vardecls-acc) → (mv warnings ports-acc portdecls-acc vardecls-acc)
Arguments: x — Guard (vl-parsed-ansi-portlist-p x).; prev-ifacep — Guard (booleanp prev-ifacep).; warnings — Guard (vl-warninglist-p warnings).; ports-acc — Guard (vl-portlist-p ports-acc).; portdecls-acc — Guard (vl-portdecllist-p portdecls-acc).; vardecls-acc — Guard (vl-vardecllist-p vardecls-acc).
Returns: warnings — Type (vl-warninglist-p warnings).; ports-acc — Type (vl-portlist-p ports-acc).; portdecls-acc — Type (vl-portdecllist-p portdecls-acc).; vardecls-acc — Type (vl-vardecllist-p vardecls-acc).

Definitions and Theorems

Function: vl-process-subsequent-ansi-ports

(defun vl-process-subsequent-ansi-ports
       (x prev-ifacep warnings
          ports-acc portdecls-acc vardecls-acc)
 (declare (xargs :guard (and (vl-parsed-ansi-portlist-p x)
                             (booleanp prev-ifacep)
                             (vl-warninglist-p warnings)
                             (vl-portlist-p ports-acc)
                             (vl-portdecllist-p portdecls-acc)
                             (vl-vardecllist-p vardecls-acc))))
 (declare
      (xargs :guard (and (consp ports-acc)
                         (equal (vl-interfaceport-p (car ports-acc))
                                prev-ifacep)
                         (equal (vl-regularport-p (car ports-acc))
                                (not prev-ifacep))
                         (implies (not prev-ifacep)
                                  (and (consp portdecls-acc)
                                       (consp vardecls-acc))))))
 (let ((__function__ 'vl-process-subsequent-ansi-ports))
   (declare (ignorable __function__))
   (b* (((when (atom x))
         (mv (vl-warninglist-fix warnings)
             (vl-portlist-fix ports-acc)
             (vl-portdecllist-fix portdecls-acc)
             (vl-vardecllist-fix vardecls-acc)))
        ((mv ifacep1 warnings
             ports-acc portdecls-acc vardecls-acc)
         (vl-process-subsequent-ansi-port
              (car x)
              prev-ifacep warnings
              ports-acc portdecls-acc vardecls-acc)))
     (vl-process-subsequent-ansi-ports
          (cdr x)
          ifacep1 warnings
          ports-acc portdecls-acc vardecls-acc))))

Theorem: vl-warninglist-p-of-vl-process-subsequent-ansi-ports.warnings

(defthm
      vl-warninglist-p-of-vl-process-subsequent-ansi-ports.warnings
  (b* (((mv ?warnings
            ?ports-acc ?portdecls-acc ?vardecls-acc)
        (vl-process-subsequent-ansi-ports
             x prev-ifacep warnings
             ports-acc portdecls-acc vardecls-acc)))
    (vl-warninglist-p warnings))
  :rule-classes :rewrite)

Theorem: vl-portlist-p-of-vl-process-subsequent-ansi-ports.ports-acc

(defthm vl-portlist-p-of-vl-process-subsequent-ansi-ports.ports-acc
  (b* (((mv ?warnings
            ?ports-acc ?portdecls-acc ?vardecls-acc)
        (vl-process-subsequent-ansi-ports
             x prev-ifacep warnings
             ports-acc portdecls-acc vardecls-acc)))
    (vl-portlist-p ports-acc))
  :rule-classes :rewrite)

Theorem: vl-portdecllist-p-of-vl-process-subsequent-ansi-ports.portdecls-acc

(defthm
 vl-portdecllist-p-of-vl-process-subsequent-ansi-ports.portdecls-acc
 (b* (((mv ?warnings
           ?ports-acc ?portdecls-acc ?vardecls-acc)
       (vl-process-subsequent-ansi-ports
            x prev-ifacep warnings
            ports-acc portdecls-acc vardecls-acc)))
   (vl-portdecllist-p portdecls-acc))
 :rule-classes :rewrite)

Theorem: vl-vardecllist-p-of-vl-process-subsequent-ansi-ports.vardecls-acc

(defthm
  vl-vardecllist-p-of-vl-process-subsequent-ansi-ports.vardecls-acc
  (b* (((mv ?warnings
            ?ports-acc ?portdecls-acc ?vardecls-acc)
        (vl-process-subsequent-ansi-ports
             x prev-ifacep warnings
             ports-acc portdecls-acc vardecls-acc)))
    (vl-vardecllist-p vardecls-acc))
  :rule-classes :rewrite)