		Search-engine friendly clone of the ACL2 documentation.

Sv-ansi-port-interpretation

Vl-process-ansi-ports

Top level function for turning parsed ansi port declarations into proper VL structures.

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

Definitions and Theorems

Function: vl-process-ansi-ports

(defun vl-process-ansi-ports (x warnings)
  (declare (xargs :guard (and (vl-parsed-ansi-portlist-p x)
                              (vl-warninglist-p warnings))))
  (let ((__function__ 'vl-process-ansi-ports))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (mv (ok) nil nil nil))
         ((mv ifacep
              ports-acc portdecls-acc vardecls-acc)
          (vl-process-first-ansi-port (car x)))
         ((mv warnings
              ports-acc portdecls-acc vardecls-acc)
          (vl-process-subsequent-ansi-ports
               (cdr x)
               ifacep warnings
               ports-acc portdecls-acc vardecls-acc)))
      (mv warnings (rev ports-acc)
          (rev portdecls-acc)
          (rev vardecls-acc)))))

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

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

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

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

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

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

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

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