		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-expr

Pretty-print an expression.

Signature
(pprint-expr expr expected-grade options) → part
Arguments: expr — Guard (exprp expr).; expected-grade — Guard (expr-gradep expected-grade).; options — Guard (pprint-options-p options).
Returns: part — Type (msgp part).

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

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

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

When printing unary expressions, we need to be careful about not printing two nested - expressions as -- or two nested + expressions ad ++, otherwise they are interpreted as predecrement or postincrement by the C compiler. Thus, we interpose a space when these two situations occur.

We treat the pretty-printing of conditional expressions slightly differently based on the pretty-printing option about parenthesizing nested conditional expressions. The difference is in the expected grades used for the `then' and `else' subexpressions. If that flag is not set, we print things with minimal parentheses, and therefore we use the top grade for `then' and the conditional grade for `else', consistently with the grammar rule for conditional expressions. This means that if the `then' and/or `else' is a conditional expression, it is not parenthesized. If instead the flag is set, then we use a lower grade for both `then' and `else', precisely the grade just one lower than conditional expressions, namely the grade of logical disjunction. This means that if the `then' and/or `else' is a conditional expression, it is parenthesized, in order to lower its grade.

Theorem: return-type-of-pprint-expr.part

(defthm return-type-of-pprint-expr.part
  (b* ((?part (pprint-expr expr expected-grade options)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: return-type-of-pprint-expr-list.parts

(defthm return-type-of-pprint-expr-list.parts
  (b* ((?parts (pprint-expr-list exprs expected-grade options)))
    (msg-listp parts))
  :rule-classes :rewrite)

Theorem: pprint-expr-of-expr-fix-expr

(defthm pprint-expr-of-expr-fix-expr
  (equal (pprint-expr (expr-fix expr)
                      expected-grade options)
         (pprint-expr expr expected-grade options)))

Theorem: pprint-expr-of-expr-grade-fix-expected-grade

(defthm pprint-expr-of-expr-grade-fix-expected-grade
  (equal (pprint-expr expr (expr-grade-fix expected-grade)
                      options)
         (pprint-expr expr expected-grade options)))

Theorem: pprint-expr-of-pprint-options-fix-options

(defthm pprint-expr-of-pprint-options-fix-options
  (equal (pprint-expr expr expected-grade
                      (pprint-options-fix options))
         (pprint-expr expr expected-grade options)))

Theorem: pprint-expr-list-of-expr-list-fix-exprs

(defthm pprint-expr-list-of-expr-list-fix-exprs
  (equal (pprint-expr-list (expr-list-fix exprs)
                           expected-grade options)
         (pprint-expr-list exprs expected-grade options)))

Theorem: pprint-expr-list-of-expr-grade-fix-expected-grade

(defthm pprint-expr-list-of-expr-grade-fix-expected-grade
  (equal (pprint-expr-list exprs (expr-grade-fix expected-grade)
                           options)
         (pprint-expr-list exprs expected-grade options)))

Theorem: pprint-expr-list-of-pprint-options-fix-options

(defthm pprint-expr-list-of-pprint-options-fix-options
  (equal (pprint-expr-list exprs expected-grade
                           (pprint-options-fix options))
         (pprint-expr-list exprs expected-grade options)))

Theorem: pprint-expr-expr-equiv-congruence-on-expr

(defthm pprint-expr-expr-equiv-congruence-on-expr
  (implies (expr-equiv expr expr-equiv)
           (equal (pprint-expr expr expected-grade options)
                  (pprint-expr expr-equiv expected-grade options)))
  :rule-classes :congruence)

Theorem: pprint-expr-expr-grade-equiv-congruence-on-expected-grade

(defthm pprint-expr-expr-grade-equiv-congruence-on-expected-grade
  (implies (expr-grade-equiv expected-grade expected-grade-equiv)
           (equal (pprint-expr expr expected-grade options)
                  (pprint-expr expr expected-grade-equiv options)))
  :rule-classes :congruence)

Theorem: pprint-expr-pprint-options-equiv-congruence-on-options

(defthm pprint-expr-pprint-options-equiv-congruence-on-options
  (implies (pprint-options-equiv options options-equiv)
           (equal (pprint-expr expr expected-grade options)
                  (pprint-expr expr expected-grade options-equiv)))
  :rule-classes :congruence)

Theorem: pprint-expr-list-expr-list-equiv-congruence-on-exprs

(defthm pprint-expr-list-expr-list-equiv-congruence-on-exprs
 (implies
      (expr-list-equiv exprs exprs-equiv)
      (equal (pprint-expr-list exprs expected-grade options)
             (pprint-expr-list exprs-equiv expected-grade options)))
 :rule-classes :congruence)

Theorem: pprint-expr-list-expr-grade-equiv-congruence-on-expected-grade

(defthm
     pprint-expr-list-expr-grade-equiv-congruence-on-expected-grade
 (implies
      (expr-grade-equiv expected-grade expected-grade-equiv)
      (equal (pprint-expr-list exprs expected-grade options)
             (pprint-expr-list exprs expected-grade-equiv options)))
 :rule-classes :congruence)

Theorem: pprint-expr-list-pprint-options-equiv-congruence-on-options

(defthm pprint-expr-list-pprint-options-equiv-congruence-on-options
 (implies
      (pprint-options-equiv options options-equiv)
      (equal (pprint-expr-list exprs expected-grade options)
             (pprint-expr-list exprs expected-grade options-equiv)))
 :rule-classes :congruence)

Subtopics

Pprint-expr-list