Determine whether we're in an ANSI or non-ANSI port list.
(vl-port-starts-ansi-port-list-p port1) → ansi-p
To tell which version we are in, we follow the rule suggested in 23.2.2.3 (pg 667):
For the first port in the port list: if the direction, port kind, and data type are all omitted, then the port shall be assumed to be a member of a non-ANSI style list_of_ports...
Function:
(defun vl-port-starts-ansi-port-list-p (port1) (declare (xargs :guard (vl-parsed-ansi-port-p port1))) (let ((__function__ 'vl-port-starts-ansi-port-list-p)) (declare (ignorable __function__)) (b* (((vl-parsed-ansi-port port1)) ((when port1.dir) t)) (case (tag port1.head) (:vl-parsed-interface-head t) (:vl-parsed-portdecl-head (b* (((vl-parsed-portdecl-head port1.head)) ((when (or port1.head.nettype port1.head.var-p port1.head.explicit-p port1.head.implicit-p)) t)) nil)) (otherwise (impossible))))))
Theorem:
(defthm booleanp-of-vl-port-starts-ansi-port-list-p (b* ((ansi-p (vl-port-starts-ansi-port-list-p port1))) (booleanp ansi-p)) :rule-classes :type-prescription)