Convert idtokens into trivial vl-parsed-port-identifier-ps.
(vl-parsed-port-identifier-list-from-idtokenlist x) → parsed
This is mostly for Verilog-2005, where port declarations can't have any unpacked dimensions.
Function:
(defun vl-parsed-port-identifier-list-from-idtokenlist (x) (declare (xargs :guard (vl-idtoken-list-p x))) (let ((__function__ 'vl-parsed-port-identifier-list-from-idtokenlist)) (declare (ignorable __function__)) (if (atom x) nil (cons (make-vl-parsed-port-identifier :name (car x) :udims nil) (vl-parsed-port-identifier-list-from-idtokenlist (cdr x))))))
Theorem:
(defthm vl-parsed-port-identifier-list-p-of-vl-parsed-port-identifier-list-from-idtokenlist (implies (and (force (vl-idtoken-list-p x))) (b* ((parsed (vl-parsed-port-identifier-list-from-idtokenlist x))) (vl-parsed-port-identifier-list-p parsed))) :rule-classes :rewrite)