Top level function for turning parsed ansi port declarations into proper VL structures.
(vl-process-ansi-ports x warnings) → (mv warnings ports portdecls vardecls)
Function:
(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:
(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:
(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:
(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:
(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)