		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-jexpr

Pretty-print an expression.

Signature
(print-jexpr expr expected-rank) → part
Arguments: expr — Guard (jexprp expr).; expected-rank — Guard (jexpr-rankp expected-rank).
Returns: part — Type (msgp part).

See here for motivation.

We first pretty-print the expression, and then we wrap it in parentheses if the expected rank is smaller than the actual rank.

When recursively pretty-printing subexpressions, the ranks argument passed for the subexpressions are determined by the relevant grammar rules.

The function to pretty-print lists of expressions takes a single rank argument, because we only need to pretty-print lists of expressions that all have the same required rank.

Theorem: return-type-of-print-jexpr.part

(defthm return-type-of-print-jexpr.part
  (b* ((?part (print-jexpr expr expected-rank)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: return-type-of-print-jexpr-list.parts

(defthm return-type-of-print-jexpr-list.parts
  (b* ((?parts (print-jexpr-list exprs expected-rank)))
    (msg-listp parts))
  :rule-classes :rewrite)

Subtopics

Print-jexpr-list