		Search-engine friendly clone of the ACL2 documentation.
Json-encoders
Vl-jp-interface

Print the JSON encoding of a vl-interface-p to ps.
Signature
(vl-jp-interface x &key (ps 'ps)) → ps
Arguments: x — Guard (vl-interface-p x).
Definitions and Theorems

Function: vl-jp-interface-fn
(defun vl-jp-interface-fn (x ps)
 (declare (xargs :stobjs (ps)))
 (declare (xargs :guard (vl-interface-p x)))
 (let ((__function__ 'vl-jp-interface))
   (declare (ignorable __function__))
   (vl-ps-seq
        (vl-print "{\"tag\": ")
        (jp-sym ':vl-interface)
        (vl-print ", ")
        (vl-print-str "\"name\": ")
        (jp-str (vl-interface->name x))
        (vl-println? ", ")
        (vl-print-str "\"imports\": ")
        (vl-jp-importlist (vl-interface->imports x))
        (vl-println? ", ")
        (vl-print-str "\"ports\": ")
        (vl-jp-portlist (vl-interface->ports x))
        (vl-println? ", ")
        (vl-print-str "\"portdecls\": ")
        (vl-jp-portdecllist (vl-interface->portdecls x))
        (vl-println? ", ")
        (vl-print-str "\"modports\": ")
        (vl-jp-modportlist (vl-interface->modports x))
        (vl-println? ", ")
        (vl-print-str "\"vardecls\": ")
        (vl-jp-vardecllist (vl-interface->vardecls x))
        (vl-println? ", ")
        (vl-print-str "\"paramdecls\": ")
        (vl-jp-paramdecllist (vl-interface->paramdecls x))
        (vl-println? ", ")
        (vl-print-str "\"fundecls\": ")
        (vl-jp-fundecllist (vl-interface->fundecls x))
        (vl-println? ", ")
        (vl-print-str "\"taskdecls\": ")
        (vl-jp-taskdecllist (vl-interface->taskdecls x))
        (vl-println? ", ")
        (vl-print-str "\"typedefs\": ")
        (vl-jp-typedeflist (vl-interface->typedefs x))
        (vl-println? ", ")
        (vl-print-str "\"dpiimports\": ")
        (vl-jp-dpiimportlist (vl-interface->dpiimports x))
        (vl-println? ", ")
        (vl-print-str "\"dpiexports\": ")
        (vl-jp-dpiexportlist (vl-interface->dpiexports x))
        (vl-println? ", ")
        (vl-print-str "\"properties\": ")
        (vl-jp-propertylist (vl-interface->properties x))
        (vl-println? ", ")
        (vl-print-str "\"sequences\": ")
        (vl-jp-sequencelist (vl-interface->sequences x))
        (vl-println? ", ")
        (vl-print-str "\"clkdecls\": ")
        (vl-jp-clkdecllist (vl-interface->clkdecls x))
        (vl-println? ", ")
        (vl-print-str "\"gclkdecls\": ")
        (vl-jp-gclkdecllist (vl-interface->gclkdecls x))
        (vl-println? ", ")
        (vl-print-str "\"defaultdisables\": ")
        (vl-jp-defaultdisablelist (vl-interface->defaultdisables x))
        (vl-println? ", ")
        (vl-print-str "\"binds\": ")
        (vl-jp-bindlist (vl-interface->binds x))
        (vl-println? ", ")
        (vl-print-str "\"classes\": ")
        (vl-jp-classlist (vl-interface->classes x))
        (vl-println? ", ")
        (vl-print-str "\"elabtasks\": ")
        (vl-jp-elabtasklist (vl-interface->elabtasks x))
        (vl-println? ", ")
        (vl-print-str "\"modinsts\": ")
        (vl-jp-modinstlist (vl-interface->modinsts x))
        (vl-println? ", ")
        (vl-print-str "\"assigns\": ")
        (vl-jp-assignlist (vl-interface->assigns x))
        (vl-println? ", ")
        (vl-print-str "\"aliases\": ")
        (vl-jp-aliaslist (vl-interface->aliases x))
        (vl-println? ", ")
        (vl-print-str "\"assertions\": ")
        (vl-jp-assertionlist (vl-interface->assertions x))
        (vl-println? ", ")
        (vl-print-str "\"cassertions\": ")
        (vl-jp-cassertionlist (vl-interface->cassertions x))
        (vl-println? ", ")
        (vl-print-str "\"alwayses\": ")
        (vl-jp-alwayslist (vl-interface->alwayses x))
        (vl-println? ", ")
        (vl-print-str "\"initials\": ")
        (vl-jp-initiallist (vl-interface->initials x))
        (vl-println? ", ")
        (vl-print-str "\"finals\": ")
        (vl-jp-finallist (vl-interface->finals x))
        (vl-println? ", ")
        (vl-print-str "\"generates\": ")
        (vl-jp-genelementlist (vl-interface->generates x))
        (vl-println? ", ")
        (vl-print-str "\"genvars\": ")
        (vl-jp-genvarlist (vl-interface->genvars x))
        (vl-println? ", ")
        (vl-print-str "\"warnings\": ")
        (vl-jp-warninglist (vl-interface->warnings x))
        (vl-println? ", ")
        (vl-print-str "\"minloc\": ")
        (vl-jp-location (vl-interface->minloc x))
        (vl-println? ", ")
        (vl-print-str "\"maxloc\": ")
        (vl-jp-location (vl-interface->maxloc x))
        (vl-println? ", ")
        (vl-print-str "\"atts\": ")
        (vl-jp-atts (vl-interface->atts x))
        (vl-println? ", ")
        (vl-print-str "\"origname\": ")
        (jp-str (vl-interface->origname x))
        (vl-println? ", ")
        (vl-print-str "\"comments\": ")
        (vl-jp-commentmap (vl-interface->comments x))
        (vl-println? ", ")
        (vl-print-str "\"parse-temps\": ")
        (vl-jp-maybe-parse-temps (vl-interface->parse-temps x))
        (vl-println? "}"))))