• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
        • Warnings
        • Primitives
        • Use-set
        • Syntax
        • Getting-started
        • Utilities
        • Loader
        • Transforms
        • Lint
        • Mlib
        • Server
        • Kit
        • Printer
          • Ps
          • Basic-printing
          • Verilog-printing
          • Printing-locally
          • Formatted-printing
          • Accessing-printed-output
          • Vl-printedlist
          • Json-printing
            • Json-encoders
              • Vl-jp-module
              • Vl-jp-warning
              • Vl-jp-constint
              • Vl-jp-vardecl
              • Jp-sym-main
              • Vl-jp-fundecl
              • Vl-jp-taskdecl
              • Vl-jp-modinst
              • Vl-jp-gateinst
              • Vl-jp-portdecl
              • Vl-jp-modport-port
              • Vl-jp-interfaceport
              • Vl-jp-expr
              • Vl-jp-assign
              • Jp-str
              • Vl-jp-warninglist
              • Vl-jp-vardecllist
              • Vl-jp-taskdecllist
              • Vl-jp-regularportlist
              • Vl-jp-portdecllist
              • Vl-jp-plainarglist
              • Vl-jp-paramvaluelist
              • Vl-jp-paramdecllist
              • Vl-jp-paramdecl
              • Vl-jp-packeddimensionlist
              • Vl-jp-namedparamvaluelist
              • Vl-jp-namedarglist
              • Vl-jp-modport-portlist
              • Vl-jp-modinstlist
              • Vl-jp-modelementlist
              • Vl-jp-interfaceportlist
              • Vl-jp-initiallist
              • Vl-jp-genelementlist
              • Vl-jp-gateinstlist
              • Vl-jp-fwdtypedef
              • Vl-jp-fundecllist
              • Vl-jp-enumitemlist
              • Jp-nat
              • Vl-jp-weirdint
              • Vl-jp-repeateventcontrol
              • Vl-jp-regularport
              • Vl-jp-rangelist
              • Vl-jp-portlist
              • Vl-jp-plainarg
              • Vl-jp-namedparamvalue
              • Vl-jp-namedarg
              • Vl-jp-modulelist
              • Vl-jp-modport
              • Vl-jp-location
              • Vl-jp-initial
              • Vl-jp-importlist
              • Vl-jp-import
              • Vl-jp-genvarlist
              • Vl-jp-genvar
              • Vl-jp-gatestrength
              • Vl-jp-gatedelay
              • Vl-jp-eventcontrol
              • Vl-jp-evatomlist
              • Vl-jp-enumitem
              • Vl-jp-enumbasetype
              • Vl-jp-assignlist
              • Vl-jp-alwayslist
              • Vl-jp-always
              • Vl-jp-aliaslist
              • Vl-jp-alias
              • Jp-object
              • Vl-jp-time
              • Vl-jp-sysfunname
              • Vl-jp-range
              • Vl-jp-evatom
              • Vl-jp-delaycontrol
              • Vl-jp-basictype
              • Vl-jp-typename
              • Vl-jp-tagname
              • Vl-jp-string
              • Vl-jp-real
              • Vl-jp-keyguts
              • Vl-jp-id
              • Vl-jp-hidpiece
              • Vl-jp-funname
              • Vl-jp-extint
              • Vl-jp-arguments
              • Vl-jp-paramvalue
              • Vl-jp-packeddimension
              • Vl-jp-maybe-packeddimension
              • Vl-jp-maybe-nettypename
              • Vl-jp-maybe-direction
              • Vl-jp-maybe-cstrength
              • Jp-timeunit
              • Jp-keygutstype
              • Jp-bool
              • Jp-bitlist
              • Jp-bit
              • Jp-bignat
              • Jp-basictypekind
              • Vl-jp-randomqualifier
              • Vl-jp-port
              • Vl-jp-nettypename
              • Vl-jp-maybe-gatedelay
              • Vl-jp-maybe-exprtype
              • Vl-jp-lifetime
              • Vl-jp-gatetype
              • Vl-jp-exprtype
              • Vl-jp-evatomtype
              • Vl-jp-dstrength
              • Vl-jp-direction
              • Vl-jp-deassign-type
              • Vl-jp-cstrength
              • Vl-jp-coretypename
              • Vl-jp-casetype
              • Vl-jp-casecheck
              • Vl-jp-assign-type
              • Vl-jp-alwaystype
              • Jp-maybe-string
              • Jp-maybe-nat
              • Jp-sym
        • Esim-vl
        • Well-formedness
      • Sv
      • Fgl
      • Vwsim
      • Vl
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Math
    • Testing-utilities
  • Json-printing

Json-encoders

A table of JSON encoders to use for for different kinds of data.

A JSON encoder is a function of the following signature:

encode-foo : foo * ps --> ps

Where foo is expected to be an object of some type foop, and ps is the vl2014 printer state stobj, ps. Each such routine is responsible for printing a JSON encoding of its foop argument. Each such function may assume that ps is set to text mode.

The encoder table is a simple association of foop to encode-foo functions. We can use it to automatically generate encoders for, e.g., defaggregate structures.

Definitions and Theorems

Function: get-json-encoders

(defun get-json-encoders (world)
  "Look up the current alist of json encoders."
  (cdr (assoc 'encoders
              (table-alist 'vl-json world))))

Function: get-json-encoder

(defun get-json-encoder (foop world)
  (let ((entry (assoc foop (get-json-encoders world))))
    (if entry (cdr entry)
      (er hard? 'get-json-encoder
          "No json encoder defined for ~x0.~%"
          foop))))

Subtopics

Vl-jp-module
Print the JSON encoding of a vl-module-p to ps.
Vl-jp-warning
Special, custom JSON encoder for warnings.
Vl-jp-constint
Print the JSON encoding of a vl-constint-p to ps.
Vl-jp-vardecl
Print the JSON encoding of a vl-vardecl-p to ps.
Jp-sym-main
Encode a simple symbol as a JSON string, including the surrounding quotes.
Vl-jp-fundecl
Print the JSON encoding of a vl-fundecl-p to ps.
Vl-jp-taskdecl
Print the JSON encoding of a vl-taskdecl-p to ps.
Vl-jp-modinst
Print the JSON encoding of a vl-modinst-p to ps.
Vl-jp-gateinst
Print the JSON encoding of a vl-gateinst-p to ps.
Vl-jp-portdecl
Print the JSON encoding of a vl-portdecl-p to ps.
Vl-jp-modport-port
Print the JSON encoding of a vl-modport-port-p to ps.
Vl-jp-interfaceport
Print the JSON encoding of a vl-interfaceport-p to ps.
Vl-jp-expr
Vl-jp-assign
Print the JSON encoding of a vl-assign-p to ps.
Jp-str
Print the JSON encoding of a string, handling all escaping correctly and including the surrounding quotes.
Vl-jp-warninglist
Prints out the elements of a vl-warninglist-p with the enclosing brackets.
Vl-jp-vardecllist
Prints out the elements of a vl-vardecllist-p with the enclosing brackets.
Vl-jp-taskdecllist
Prints out the elements of a vl-taskdecllist-p with the enclosing brackets.
Vl-jp-regularportlist
Prints out the elements of a vl-regularportlist-p with the enclosing brackets.
Vl-jp-portdecllist
Prints out the elements of a vl-portdecllist-p with the enclosing brackets.
Vl-jp-plainarglist
Prints out the elements of a vl-plainarglist-p with the enclosing brackets.
Vl-jp-paramvaluelist
Prints out the elements of a vl-paramvaluelist-p with the enclosing brackets.
Vl-jp-paramdecllist
Prints out the elements of a vl-paramdecllist-p with the enclosing brackets.
Vl-jp-paramdecl
Print the JSON encoding of a vl-paramdecl-p to ps.
Vl-jp-packeddimensionlist
Prints out the elements of a vl-packeddimensionlist-p with the enclosing brackets.
Vl-jp-namedparamvaluelist
Prints out the elements of a vl-namedparamvaluelist-p with the enclosing brackets.
Vl-jp-namedarglist
Prints out the elements of a vl-namedarglist-p with the enclosing brackets.
Vl-jp-modport-portlist
Prints out the elements of a vl-modport-portlist-p with the enclosing brackets.
Vl-jp-modinstlist
Prints out the elements of a vl-modinstlist-p with the enclosing brackets.
Vl-jp-modelementlist
Prints out the elements of a vl-modelementlist-p with the enclosing brackets.
Vl-jp-interfaceportlist
Prints out the elements of a vl-interfaceportlist-p with the enclosing brackets.
Vl-jp-initiallist
Prints out the elements of a vl-initiallist-p with the enclosing brackets.
Vl-jp-genelementlist
Prints out the elements of a vl-genelementlist-p with the enclosing brackets.
Vl-jp-gateinstlist
Prints out the elements of a vl-gateinstlist-p with the enclosing brackets.
Vl-jp-fwdtypedef
Print the JSON encoding of a vl-fwdtypedef-p to ps.
Vl-jp-fundecllist
Prints out the elements of a vl-fundecllist-p with the enclosing brackets.
Vl-jp-enumitemlist
Prints out the elements of a vl-enumitemlist-p with the enclosing brackets.
Jp-nat
Encode a probably small natural number as a JSON number.
Vl-jp-weirdint
Print the JSON encoding of a vl-weirdint-p to ps.
Vl-jp-repeateventcontrol
Print the JSON encoding of a vl-repeateventcontrol-p to ps.
Vl-jp-regularport
Print the JSON encoding of a vl-regularport-p to ps.
Vl-jp-rangelist
Prints out the elements of a vl-rangelist-p with the enclosing brackets.
Vl-jp-portlist
Prints out the elements of a vl-portlist-p with the enclosing brackets.
Vl-jp-plainarg
Print the JSON encoding of a vl-plainarg-p to ps.
Vl-jp-namedparamvalue
Print the JSON encoding of a vl-namedparamvalue-p to ps.
Vl-jp-namedarg
Print the JSON encoding of a vl-namedarg-p to ps.
Vl-jp-modulelist
Prints out the elements of a vl-modulelist-p with the enclosing brackets.
Vl-jp-modport
Print the JSON encoding of a vl-modport-p to ps.
Vl-jp-location
Print the JSON encoding of a vl-location-p to ps.
Vl-jp-initial
Print the JSON encoding of a vl-initial-p to ps.
Vl-jp-importlist
Prints out the elements of a vl-importlist-p with the enclosing brackets.
Vl-jp-import
Print the JSON encoding of a vl-import-p to ps.
Vl-jp-genvarlist
Prints out the elements of a vl-genvarlist-p with the enclosing brackets.
Vl-jp-genvar
Print the JSON encoding of a vl-genvar-p to ps.
Vl-jp-gatestrength
Print the JSON encoding of a vl-gatestrength-p to ps.
Vl-jp-gatedelay
Print the JSON encoding of a vl-gatedelay-p to ps.
Vl-jp-eventcontrol
Print the JSON encoding of a vl-eventcontrol-p to ps.
Vl-jp-evatomlist
Prints out the elements of a vl-evatomlist-p with the enclosing brackets.
Vl-jp-enumitem
Print the JSON encoding of a vl-enumitem-p to ps.
Vl-jp-enumbasetype
Print the JSON encoding of a vl-enumbasetype-p to ps.
Vl-jp-assignlist
Prints out the elements of a vl-assignlist-p with the enclosing brackets.
Vl-jp-alwayslist
Prints out the elements of a vl-alwayslist-p with the enclosing brackets.
Vl-jp-always
Print the JSON encoding of a vl-always-p to ps.
Vl-jp-aliaslist
Prints out the elements of a vl-aliaslist-p with the enclosing brackets.
Vl-jp-alias
Print the JSON encoding of a vl-alias-p to ps.
Jp-object
Utility for printing JSON objects, which in some other languages might be called alists, dictionaries, hashes, records, etc.
Vl-jp-time
Print the JSON encoding of a vl-time-p to ps.
Vl-jp-sysfunname
Print the JSON encoding of a vl-sysfunname-p to ps.
Vl-jp-range
Print the JSON encoding of a vl-range-p to ps.
Vl-jp-evatom
Print the JSON encoding of a vl-evatom-p to ps.
Vl-jp-delaycontrol
Print the JSON encoding of a vl-delaycontrol-p to ps.
Vl-jp-basictype
Print the JSON encoding of a vl-basictype-p to ps.
Vl-jp-typename
Print the JSON encoding of a vl-typename-p to ps.
Vl-jp-tagname
Print the JSON encoding of a vl-tagname-p to ps.
Vl-jp-string
Print the JSON encoding of a vl-string-p to ps.
Vl-jp-real
Print the JSON encoding of a vl-real-p to ps.
Vl-jp-keyguts
Print the JSON encoding of a vl-keyguts-p to ps.
Vl-jp-id
Print the JSON encoding of a vl-id-p to ps.
Vl-jp-hidpiece
Print the JSON encoding of a vl-hidpiece-p to ps.
Vl-jp-funname
Print the JSON encoding of a vl-funname-p to ps.
Vl-jp-extint
Print the JSON encoding of a vl-extint-p to ps.
Vl-jp-arguments
Vl-jp-paramvalue
Vl-jp-packeddimension
Vl-jp-maybe-packeddimension
Vl-jp-maybe-nettypename
Vl-jp-maybe-direction
Vl-jp-maybe-cstrength
Jp-timeunit
Encode a vl-timeunit-p as a JSON string.
Jp-keygutstype
Encode a vl-keygutstype-p as a JSON string.
Jp-bool
Encode a booleanp into JSON as true or false.
Jp-bitlist
Encode a vl-bitlist-p as a JSON string.
Jp-bit
Encode a vl-bit-p as a JSON string.
Jp-bignat
Encode a potentially large natural number as a JSON string.
Jp-basictypekind
Encode a vl-basictypekind-p as a JSON string.
Vl-jp-randomqualifier
Vl-jp-port
Vl-jp-nettypename
Vl-jp-maybe-gatedelay
Vl-jp-maybe-exprtype
Vl-jp-lifetime
Vl-jp-gatetype
Vl-jp-exprtype
Vl-jp-evatomtype
Vl-jp-dstrength
Vl-jp-direction
Vl-jp-deassign-type
Vl-jp-cstrength
Vl-jp-coretypename
Vl-jp-casetype
Vl-jp-casecheck
Vl-jp-assign-type
Vl-jp-alwaystype
Jp-maybe-string
Jp-maybe-nat
Jp-sym
Optimized version of jp-sym-main.