		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Expr->grade

Grade of an abstract syntactic expression.

Signature
(expr->grade expr) → grade
Arguments: expr — Guard (expressionp expr).
Returns: grade — Type (expr-gradep grade).

See pprint-expression-algorithm for background.

Definitions and Theorems

Function: expr->grade

(defun expr->grade (expr)
  (declare (xargs :guard (expressionp expr)))
  (let ((__function__ 'expr->grade))
    (declare (ignorable __function__))
    (expression-case
         expr
         :literal (expr-grade-primary)
         :var/const (expr-grade-primary)
         :assoc-const (expr-grade-primary)
         :unary (expr-grade-unary)
         :binary (binop-case expr.op
                             :pow (expr-grade-exponential)
                             :mul (expr-grade-multiplicative)
                             :div (expr-grade-multiplicative)
                             :rem (expr-grade-multiplicative)
                             :add (expr-grade-additive)
                             :sub (expr-grade-additive)
                             :shr (expr-grade-shift)
                             :shl (expr-grade-shift)
                             :bitand (expr-grade-bitwise-and)
                             :bitior (expr-grade-bitwise-ior)
                             :bitxor (expr-grade-bitwise-xor)
                             :lt (expr-grade-ordering)
                             :gt (expr-grade-ordering)
                             :le (expr-grade-ordering)
                             :ge (expr-grade-ordering)
                             :eq (expr-grade-equality)
                             :ne (expr-grade-equality)
                             :and (expr-grade-conjunctive)
                             :or (expr-grade-disjunctive)
                             :nand (expr-grade-postfix)
                             :nor (expr-grade-postfix)
                             :pow-wrapped (expr-grade-postfix)
                             :mul-wrapped (expr-grade-postfix)
                             :div-wrapped (expr-grade-postfix)
                             :rem-wrapped (expr-grade-postfix)
                             :add-wrapped (expr-grade-postfix)
                             :sub-wrapped (expr-grade-postfix)
                             :shr-wrapped (expr-grade-postfix)
                             :shl-wrapped (expr-grade-postfix))
         :unit (expr-grade-primary)
         :tuple (expr-grade-primary)
         :tuple-component (expr-grade-postfix)
         :struct (expr-grade-primary)
         :struct-component (expr-grade-postfix)
         :cond (expr-grade-conditional)
         :internal-call (expr-grade-primary)
         :external-call (expr-grade-primary)
         :static-call (expr-grade-primary))))

Theorem: expr-gradep-of-expr->grade

(defthm expr-gradep-of-expr->grade
  (b* ((grade (expr->grade expr)))
    (expr-gradep grade))
  :rule-classes :rewrite)

Theorem: expr->grade-of-expression-fix-expr

(defthm expr->grade-of-expression-fix-expr
  (equal (expr->grade (expression-fix expr))
         (expr->grade expr)))

Theorem: expr->grade-expression-equiv-congruence-on-expr

(defthm expr->grade-expression-equiv-congruence-on-expr
  (implies (expression-equiv expr expr-equiv)
           (equal (expr->grade expr)
                  (expr->grade expr-equiv)))
  :rule-classes :congruence)