(vl-process-first-ansi-port x) → (mv ifacep ports-acc portdecls-acc vardecls-acc)
Note: we assume that the first port in the list has at least a direction, port kind, or data type. Otherwise, per Section 23.2.2.3, the ports are supposed to be assumed to be a non-ANSI style list of ports, so we shouldn't be trying to parse the ports as a list of ansi ports at all!
Function:
(defun vl-process-first-ansi-port (x) (declare (xargs :guard (vl-parsed-ansi-port-p x))) (let ((__function__ 'vl-process-first-ansi-port)) (declare (ignorable __function__)) (b* (((vl-parsed-ansi-port x)) ((vl-parsed-port-identifier x.id)) (name (vl-idtoken->name x.id.name)) (loc (vl-token->loc x.id.name))) (case (tag x.head) (:vl-parsed-interface-head (b* ((new-port (make-vl-interfaceport :name name :ifname (vl-parsed-interface-head->ifname x.head) :modport (vl-parsed-interface-head->modport x.head) :udims x.id.udims :loc loc))) (mv t (list new-port) nil nil))) (:vl-parsed-portdecl-head (b* (((vl-parsed-portdecl-head x.head)) (ports (list (make-vl-regularport :name name :expr (vl-idexpr name nil nil) :loc loc))) (complete-p t) (dir (or x.dir :vl-inout)) (nettype (vl-nettype-for-parsed-ansi-port dir x.head)) (type x.head.type) ((cons portdecls vardecls) (vl-make-ports-and-maybe-nets (list x.id) :dir dir :nettype nettype :type type :complete-p complete-p :atts x.atts))) (mv nil ports portdecls vardecls))) (otherwise (progn$ (impossible) (mv t (list (make-vl-interfaceport :name "bogus" :ifname "bogus")) nil nil)))))))
Theorem:
(defthm booleanp-of-vl-process-first-ansi-port.ifacep (b* (((mv ?ifacep ?ports-acc ?portdecls-acc ?vardecls-acc) (vl-process-first-ansi-port x))) (booleanp ifacep)) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-vl-process-first-ansi-port.ports-acc (b* (((mv ?ifacep ?ports-acc ?portdecls-acc ?vardecls-acc) (vl-process-first-ansi-port x))) (and (vl-portlist-p ports-acc) (consp ports-acc) (equal (vl-interfaceport-p (car ports-acc)) ifacep) (equal (vl-regularport-p (car ports-acc)) (not ifacep)))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-process-first-ansi-port.portdecls-acc (b* (((mv ?ifacep ?ports-acc ?portdecls-acc ?vardecls-acc) (vl-process-first-ansi-port x))) (and (vl-portdecllist-p portdecls-acc) (implies (not ifacep) (consp portdecls-acc)))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-process-first-ansi-port.vardecls-acc (b* (((mv ?ifacep ?ports-acc ?portdecls-acc ?vardecls-acc) (vl-process-first-ansi-port x))) (and (vl-vardecllist-p vardecls-acc) (implies (not ifacep) (consp vardecls-acc)))) :rule-classes :rewrite)