• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
          • Atj
            • Atj-implementation
              • Atj-types
              • Atj-java-primitive-array-model
              • Atj-java-abstract-syntax
              • Atj-input-processing
              • Atj-java-pretty-printer
                • Jexpr-rank
                • Print-jexprs
                  • Print-jchar
                  • Print-jstatems+jblocks
                  • Print-jclasses+jcmembers
                  • Jbinop-expected-ranks
                  • Jexpr->rank
                  • Jexpr-rank-<=
                  • Print-jexpr
                  • Print-optional-integer-type-suffix
                  • Print-octdig/uscore-list
                  • Print-oct-integer-literal
                  • Print-jcunit
                  • Print-hexdig/uscore-list
                  • Print-hex-integer-literal
                  • Print-decdig/uscore-list
                  • Print-dec-integer-literal
                  • Print-bindig/uscore-list
                  • Print-bin-integer-literal
                  • Print-integer-literal
                  • Print-octdig/uscore
                  • Print-jmethod
                  • Print-jfield
                  • Print-hexdig/uscore
                  • Print-decdig/uscore
                  • Print-bindig/uscore
                  • Print-jclass-list
                  • Print-jlocvar
                  • Print-jliteral
                  • Print-jcinitializer
                  • Print-jline
                  • Print-jimports
                  • Print-jchars
                  • Print-comma-sep
                  • Print-jimport
                  • Print-jbinop
                  • Print-primitive-type
                  • Print-jparam-list
                  • Print-jlines-to-channel
                  • Jexpr-rank-index
                  • Atj-indent
                  • Print-to-jfile
                  • Print-jparam
                  • Print-jaccess
                  • Print-oct-digit
                  • Print-junop
                  • Print-jtype
                  • Print-jresult
                  • Print-hex-digit
                  • Print-dec-digit
                  • Print-bin-digit
                  • Print-jline-blank
                • Atj-code-generation
                • Atj-java-primitives
                • Atj-java-primitive-arrays
                • Atj-type-macros
                • Atj-java-syntax-operations
                • Atj-fn
                • Atj-library-extensions
                • Atj-java-input-types
                • Atj-test-structures
                • Aij-notions
                • Atj-macro-definition
              • Atj-tutorial
            • Aij
            • Language
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Atj-java-pretty-printer

    Print-jexprs

    Pretty-printing of expressions.

    The tree structure of the abstract syntax of Java expressions describes the grouping of nested subexpressions. For instance, the tree

    (jexpr-binary (jbinop-mul)
                  (jexpr-binary (jbinop-add)
                                (jexpr-name "x")
                                (jexpr-name "y"))
                  (jexpr-name "z"))

    represents the expression (x + y) * z. Note that, when this expression is written in concrete syntax as just done, parentheses must be added, because * binds tighter (i.e. has a higher priority) than + in Java.

    The relative priorities of Java operators are implicitly defined by the Java grammar of expressions, which also defines the left vs. right associativity of binary operators. For instance, with reference to the ABNF grammar, the rules tell us that (i) + binds tighter than * and (ii) + is left-associative:

    • Consider an expression x + y * z. In order to parse this as a multiplicative-expression, x + y would have to be a multiplicative-expression, which is not. Thus, the original expression can only be parsed as an additive-expression.
    • Consider an expression x * y + z. In order to parse this as a multiplicative-expression, y + z would have to be a unary-expression, which is not. Thus, the original expression can only be parsed as an additive-expression.
    • Consider an expression x + y + z. In order to right-associate it (i.e. x + (y + z)), y + z would have to be a multiplicative-expression, which is not. Thus, the original expression can only be left-associated (i.e. (x + y) + z).

    Our pretty-printer adds parentheses based on the relative priorities of the Java operators and the left or right associativity of the Java binary operators, following the grammar. The approach is explained in the following paragraphs.

    We define ``ranks'' of expressions that correspond to certain nonterminals of the Java grammar, such as a the rank of additive expressions corresponding to the nonterminal additive-expression. We define a mapping from the expressions of our abstract syntax to their ranks, e.g. (jexpr-binary (jbinop-add) ... ...) and (jexpr-binary (jbinop-sub) ... ...) are mapped to the rank of additive expressions.

    We define a partial order on expression ranks that is the reflexive and transitive closure of the binary relation that consists of the pairs rank1 < rank2 such that there is a grammar (sub)rule nonterm2 = nonterm1 saying that the nonterminal nonterm2 corresponding to rank2 may expand to the nonterminal nonterm1 corresponding to rank1. For instance, rank1 is the rank of multiplicative expressions and rank2 is the rank of additive expressions, because there is a (sub)rule additive-expression = multiplicative-expression in the grammar. (Here by 'subrule' we mean a rule not necessarily in the grammar but obtainable by selecting just some of the alternatives in the definiens that are separated by slashes in ABNF.) The nonterminal additive-expression also has other alternatives, but those are not single nonterminals; here we are only concerned with single nonterminals as rule definientia. The reason is explained below.

    Besides the abstract syntactic expression to pretty-print, the pretty-printer for expression has an argument that is the rank of expression that must be pretty-printed at that point. At the top level, this second argument is the rank of top-level expressions, i.e. the rank that corresponds to the nonterminal expression. As the pretty-printer descends into subexpressions, the second argument is changed according to the grammar rule corresponding to the super-expressions. For instance, when pretty-printing the left and right subexpressions of a super-expression (jbinary-expr (jbinop-add) left right), we recursively call the pretty-printer twice, once on left and once on right. Because of the grammar rule additive-expression = additive-expression "+" multiplicative-expression that corresponds to the super-expression, the recursive call on left will have as second argument the rank of additive-expression, while the recursive call on right will have as second argument the rank of multiplicative-expression. The second argument of the pretty-printer is used as follows: the pretty-printer compares the second argument (i.e. the expected rank of expression) with the rank of the expression passed as first argument (i.e. the actual rank of expression), according to the partial order on expression ranks described above; if the actual rank is less than or equal to the expected rank, the expression is pretty-printed without parentheses, otherwise parentheses are added. The reason why no parentheses are needed in the first case is that the nonterminal for the expected rank can be expanded, possibly in multiple steps, into the nonterminal for the actual rank: or conversely, the actual expression can be parsed into an expression of the expected rank. On the other hand, if the actual rank is greater than, or unrelated to, the expected rank, there is no such possibility; by adding parentheses, we ``change'' the rank of the actual expression into the bottom of the partial order, i.e. the rank corresponding to primary, which again lets the parenthesized expression be parsed into an expression of the expected rank.

    For instance, consider the abstract syntax tree for (x + y) * z, shown earlier as motivating example. Assume that it is pretty-printed as a top-level expression, i.e. that the second argument is the rank of expression (the expected rank). Since the actual rank of the expression is the one for multiplicative-expression, which is less than or equal to the one for expression (via assignment-expression, conditional-expression, conditional-or-expression, conditional-and-expression, inclusive-or-expression, exclusive-or-expression, and-expression, equality-expression, relational-expression, shift-expression, and additive-expression), no parentheses are printed at the top level. When pretty-printing the left subexpression x + y, the expected rank is multiplicative-expression: since the actual rank of x + y is additive-expression, which is greater than the expected rank, parentheses must be added, as mentioned when the example was first presented. On the other hand, when pretty-printing the right subexpression z, the expected rank is unary-expression: since the actual rank of z is primary, which is less than the expected rank, no parentheses are printed.

    The partial order on expression ranks only considers, as mentioned, (sub)rules of the form nonterm2 = nonterm1 where nonterm1 is a single nonterminal. Rule definientia that are not single terminals are captured as tree structures in our abstract syntax, and thus have their own explicit rank. On the other hand, single-nonterminal definientia do not correspond to any tree structure, but rather allow the same expression to have, in effect, different ranks (a form of subtyping).