Pretty-print a full vl-ctxelement-p.
(vl-pp-ctxelement-full x &key (ps 'ps)) → ps
This sometimes produces output that is too big. If you just want a quick summary instead, see vl-pp-ctxelement-summary.
Function:
(defun vl-pp-ctxelement-full-fn (x ps) (declare (xargs :stobjs (ps))) (declare (xargs :guard (vl-ctxelement-p x))) (let ((__function__ 'vl-pp-ctxelement-full)) (declare (ignorable __function__)) (b* ((x (vl-ctxelement-fix x))) (case (tag x) (:vl-regularport (vl-pp-regularport x)) (:vl-interfaceport (vl-pp-interfaceport x)) (:vl-portdecl (vl-pp-portdecl x)) (:vl-assign (vl-pp-assign x)) (:vl-vardecl (vl-pp-vardecl x)) (:vl-paramdecl (vl-pp-paramdecl x)) (:vl-fundecl (vl-pp-fundecl x)) (:vl-taskdecl (vl-pp-taskdecl x)) (:vl-modinst (vl-pp-modinst x nil)) (:vl-gateinst (vl-pp-gateinst x)) (:vl-always (vl-pp-always x)) (:vl-initial (vl-pp-initial x)) (:vl-final (vl-pp-final x)) (:vl-alias (vl-pp-alias x)) (:vl-typedef (vl-pp-typedef x)) (:vl-fwdtypedef (vl-pp-fwdtypedef x)) (:vl-modport (vl-pp-modport x)) (:vl-import (vl-pp-import x)) (:vl-property (vl-pp-property x)) (:vl-sequence (vl-pp-sequence x)) (:vl-clkdecl (vl-pp-clkdecl x)) (:vl-gclkdecl (vl-pp-gclkdecl x)) (:vl-defaultdisable (vl-pp-defaultdisable x)) (:vl-dpiimport (vl-pp-dpiimport x)) (:vl-dpiexport (vl-pp-dpiexport x)) (:vl-bind (vl-pp-bind x nil)) (:vl-class (vl-pp-class x)) (:vl-covergroup (vl-pp-covergroup x)) (:vl-elabtask (vl-pp-elabtask x)) (:vl-assertion (vl-pp-assertion x :include-name t)) (:vl-cassertion (vl-pp-cassertion x :include-name t)) ((:vl-genif :vl-genloop :vl-gencase :vl-genbegin :vl-genarray :vl-genbase) (vl-pp-genelement x)) (otherwise (prog2$ (impossible) ps))))))
Theorem:
(defthm vl-pp-ctxelement-full-fn-of-vl-ctxelement-fix-x (equal (vl-pp-ctxelement-full-fn (vl-ctxelement-fix x) ps) (vl-pp-ctxelement-full-fn x ps)))
Theorem:
(defthm vl-pp-ctxelement-full-fn-vl-ctxelement-equiv-congruence-on-x (implies (vl-ctxelement-equiv x x-equiv) (equal (vl-pp-ctxelement-full-fn x ps) (vl-pp-ctxelement-full-fn x-equiv ps))) :rule-classes :congruence)