		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Jexpr->rank

Rank of an abstract syntactic expression.

Signature
(jexpr->rank expr) → rank
Arguments: expr — Guard (jexprp expr).
Returns: rank — Type (jexpr-rankp rank).

See here for motivation.

Expressions that do not have their own rank (e.g. literals) are mapped to the rank of the most specific nonterminal that they (more precisely, their concrete syntactic counterpart) can be generated from: this is rank :primary for most of them, except that expression names are mapped to rank :postfix and that cast expressions are mapped to rank :unary.

Definitions and Theorems

Function: jexpr->rank

(defun jexpr->rank (expr)
  (declare (xargs :guard (jexprp expr)))
  (let ((__function__ 'jexpr->rank))
    (declare (ignorable __function__))
    (jexpr-case
         expr
         :literal (jexpr-rank-primary)
         :name (jexpr-rank-postfix)
         :newarray (jexpr-rank-primary)
         :newarray-init (jexpr-rank-primary)
         :array (jexpr-rank-primary)
         :newclass (jexpr-rank-primary)
         :field (jexpr-rank-primary)
         :method (jexpr-rank-primary)
         :smethod (jexpr-rank-primary)
         :imethod (jexpr-rank-primary)
         :postinc (jexpr-rank-postfix)
         :postdec (jexpr-rank-postfix)
         :cast (jexpr-rank-unary)
         :unary (jexpr-rank-unary)
         :binary (jbinop-case expr.op
                              :mul (jexpr-rank-multiplicative)
                              :div (jexpr-rank-multiplicative)
                              :rem (jexpr-rank-multiplicative)
                              :add (jexpr-rank-additive)
                              :sub (jexpr-rank-additive)
                              :shl (jexpr-rank-shift)
                              :sshr (jexpr-rank-shift)
                              :ushr (jexpr-rank-shift)
                              :lt (jexpr-rank-relational)
                              :gt (jexpr-rank-relational)
                              :le (jexpr-rank-relational)
                              :ge (jexpr-rank-relational)
                              :eq (jexpr-rank-equality)
                              :ne (jexpr-rank-equality)
                              :and (jexpr-rank-and)
                              :xor (jexpr-rank-exclusive-or)
                              :ior (jexpr-rank-inclusive-or)
                              :condand (jexpr-rank-conditional-and)
                              :condor (jexpr-rank-conditional-or)
                              :asg (jexpr-rank-assignment)
                              :asg-mul (jexpr-rank-assignment)
                              :asg-div (jexpr-rank-assignment)
                              :asg-rem (jexpr-rank-assignment)
                              :asg-add (jexpr-rank-assignment)
                              :asg-sub (jexpr-rank-assignment)
                              :asg-shl (jexpr-rank-assignment)
                              :asg-sshr (jexpr-rank-assignment)
                              :asg-ushr (jexpr-rank-assignment)
                              :asg-and (jexpr-rank-assignment)
                              :asg-xor (jexpr-rank-assignment)
                              :asg-ior (jexpr-rank-assignment))
         :instanceof (jexpr-rank-relational)
         :cond (jexpr-rank-conditional)
         :paren (jexpr-rank-primary))))

Theorem: jexpr-rankp-of-jexpr->rank

(defthm jexpr-rankp-of-jexpr->rank
  (b* ((rank (jexpr->rank expr)))
    (jexpr-rankp rank))
  :rule-classes :rewrite)