		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-jstatems+jblocks

Pretty-print a statement or block.

Note that we print the statements that form a block one after the other, without surrounding them with curly braces. We do print curly braces when printing method declarations and if statements, producing valid Java concrete syntax, but our current treatment of blocks is somewhat ``improper'', because syntactically blocks include curly braces. This impropriety should be remedied in future versions of this pretty-printer.

Definitions and Theorems

Function: print-jstatem

(defun print-jstatem (statem indent-level)
 (declare (xargs :guard (and (jstatemp statem)
                             (natp indent-level))))
 (let ((__function__ 'print-jstatem))
  (declare (ignorable __function__))
  (jstatem-case
   statem
   :locvar (list (print-jlocvar statem.get indent-level))
   :expr
   (list (print-jline
              (msg "~@0;"
                   (print-jexpr statem.get (jexpr-rank-expression)))
              indent-level))
   :return
   (list
     (if statem.expr?
       (print-jline
            (msg "return ~@0;"
                 (print-jexpr statem.expr? (jexpr-rank-expression)))
            indent-level)
       (print-jline "return;" indent-level)))
   :throw
   (list
        (print-jline
             (msg "throw ~@0;"
                  (print-jexpr statem.expr (jexpr-rank-expression)))
             indent-level))
   :break (list (print-jline "break;" indent-level))
   :continue (list (print-jline "continue;" indent-level))
   :if
   (append
    (list
        (print-jline
             (msg "if (~@0) {"
                  (print-jexpr statem.test (jexpr-rank-expression)))
             indent-level))
    (print-jblock statem.then (1+ indent-level))
    (list (print-jline "}" indent-level)))
   :ifelse
   (append
    (list
        (print-jline
             (msg "if (~@0) {"
                  (print-jexpr statem.test (jexpr-rank-expression)))
             indent-level))
    (print-jblock statem.then (1+ indent-level))
    (list (print-jline "} else {" indent-level))
    (print-jblock statem.else (1+ indent-level))
    (list (print-jline "}" indent-level)))
   :while
   (append
    (list
        (print-jline
             (msg "while (~@0) {"
                  (print-jexpr statem.test (jexpr-rank-expression)))
             indent-level))
    (print-jblock statem.body (1+ indent-level))
    (list (print-jline "}" indent-level)))
   :do
   (append
    (list (print-jline "do {" indent-level))
    (print-jblock statem.body (1+ indent-level))
    (list
        (print-jline
             (msg "} while (~@0);"
                  (print-jexpr statem.test (jexpr-rank-expression)))
             indent-level)))
   :for
   (append
    (list
      (print-jline
           (msg "for (~@0; ~@1; ~@2) {"
                (print-jexpr statem.init (jexpr-rank-expression))
                (print-jexpr statem.test (jexpr-rank-expression))
                (print-jexpr statem.update (jexpr-rank-expression)))
           indent-level))
    (print-jblock statem.body (1+ indent-level))
    (list (print-jline "}" indent-level))))))

Function: print-jblock

(defun print-jblock (block indent-level)
  (declare (xargs :guard (and (jblockp block)
                              (natp indent-level))))
  (let ((__function__ 'print-jblock))
    (declare (ignorable __function__))
    (cond ((endp block) nil)
          (t (append (print-jstatem (car block) indent-level)
                     (print-jblock (cdr block)
                                   indent-level))))))

Theorem: return-type-of-print-jstatem.lines

(defthm return-type-of-print-jstatem.lines
  (b* ((?lines (print-jstatem statem indent-level)))
    (msg-listp lines))
  :rule-classes :rewrite)

Theorem: return-type-of-print-jblock.lines

(defthm return-type-of-print-jblock.lines
  (b* ((?lines (print-jblock block indent-level)))
    (msg-listp lines))
  :rule-classes :rewrite)

Subtopics

Print-jstatem
Print-jblock