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

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

Function: vl-jp-module-fn
(defun vl-jp-module-fn (x ps)
  (declare (xargs :stobjs (ps)))
  (declare (xargs :guard (vl-module-p x)))
  (let ((__function__ 'vl-jp-module))
    (declare (ignorable __function__))
    (vl-ps-seq (vl-print "{\"tag\": ")
               (jp-sym ':vl-module)
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"name\": ")
               (jp-str (vl-module->name x))
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"imports\": ")
               (vl-jp-importlist (vl-module->imports x))
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"ports\": ")
               (vl-jp-portlist (vl-module->ports x))
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"portdecls\": ")
               (vl-jp-portdecllist (vl-module->portdecls x))
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"vardecls\": ")
               (vl-jp-vardecllist (vl-module->vardecls x))
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"paramdecls\": ")
               (vl-jp-paramdecllist (vl-module->paramdecls x))
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"fundecls\": ")
               (vl-jp-fundecllist (vl-module->fundecls x))
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"taskdecls\": ")
               (vl-jp-taskdecllist (vl-module->taskdecls x))
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"assigns\": ")
               (vl-jp-assignlist (vl-module->assigns x))
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"aliases\": ")
               (vl-jp-aliaslist (vl-module->aliases x))
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"modinsts\": ")
               (vl-jp-modinstlist (vl-module->modinsts x))
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"gateinsts\": ")
               (vl-jp-gateinstlist (vl-module->gateinsts x))
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"alwayses\": ")
               (vl-jp-alwayslist (vl-module->alwayses x))
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"initials\": ")
               (vl-jp-initiallist (vl-module->initials x))
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"genvars\": ")
               (vl-jp-genvarlist (vl-module->genvars x))
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"generates\": ")
               (vl-jp-genelementlist (vl-module->generates x))
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"atts\": ")
               (vl-jp-atts (vl-module->atts x))
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"minloc\": ")
               (vl-jp-location (vl-module->minloc x))
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"maxloc\": ")
               (vl-jp-location (vl-module->maxloc x))
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"origname\": ")
               (jp-str (vl-module->origname x))
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"warnings\": ")
               (vl-jp-warninglist (vl-module->warnings x))
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"comments\": ")
               (vl-jp-commentmap (vl-module->comments x))
               (vl-ps-seq (vl-println ", ")
                          (vl-indent 2))
               (vl-print-str "\"loaditems\": ")
               (vl-jp-genelementlist (vl-module->loaditems x))
               (vl-println? "}"))))