|
|
|---|
|
|
|
|---|
Pretty-print an expression.
(print-jexpr expr expected-rank) → 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:
(defthm return-type-of-print-jexpr.part (b* ((?part (print-jexpr expr expected-rank))) (msgp part)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-print-jexpr-list.parts (b* ((?parts (print-jexpr-list exprs expected-rank))) (msg-listp parts)) :rule-classes :rewrite)