		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-jliteral

Pretty-print a literal.

Signature
(print-jliteral lit) → part
Arguments: lit — Guard (jliteralp lit).
Returns: part — Type (msgp part).

We pretty-print our limited form of floating-point literals just by appending .0 after their decimal integer digits.

Definitions and Theorems

Function: print-jliteral

(defun print-jliteral (lit)
  (declare (xargs :guard (jliteralp lit)))
  (let ((__function__ 'print-jliteral))
    (declare (ignorable __function__))
    (jliteral-case lit
                   :integer (print-integer-literal lit.get)
                   :floating
                   (b* ((digits (nat-to-dec-string lit.value)))
                     (str::cat digits ".0"))
                   :boolean (if lit.value "true" "false")
                   :character (msg "'~@0'" (print-jchar lit.value))
                   :string (msg "\"~@0\""
                                (print-jchars (explode lit.value)))
                   :null "null")))

Theorem: msgp-of-print-jliteral

(defthm msgp-of-print-jliteral
  (b* ((part (print-jliteral lit)))
    (msgp part))
  :rule-classes :rewrite)