|
|
|---|
|
|
|
|---|
Grade of an abstract syntactic expression.
(expr->grade expr) → grade
See pprint-expressions for background.
Function:
(defun expr->grade (expr) (declare (xargs :guard (exprp expr))) (let ((__function__ 'expr->grade)) (declare (ignorable __function__)) (expr-case expr :ident (expr-grade-primary) :const (expr-grade-primary) :arrsub (expr-grade-postfix) :call (expr-grade-postfix) :member (expr-grade-postfix) :memberp (expr-grade-postfix) :postinc (expr-grade-postfix) :postdec (expr-grade-postfix) :preinc (expr-grade-unary) :predec (expr-grade-unary) :unary (expr-grade-unary) :cast (expr-grade-cast) :binary (binop-case expr.op :mul (expr-grade-multiplicative) :div (expr-grade-multiplicative) :rem (expr-grade-multiplicative) :add (expr-grade-additive) :sub (expr-grade-additive) :shl (expr-grade-shift) :shr (expr-grade-shift) :lt (expr-grade-relational) :gt (expr-grade-relational) :le (expr-grade-relational) :ge (expr-grade-relational) :eq (expr-grade-equality) :ne (expr-grade-equality) :bitand (expr-grade-and) :bitxor (expr-grade-xor) :bitior (expr-grade-ior) :logand (expr-grade-logical-and) :logor (expr-grade-logical-or) :asg (expr-grade-assignment) :asg-mul (expr-grade-assignment) :asg-div (expr-grade-assignment) :asg-rem (expr-grade-assignment) :asg-add (expr-grade-assignment) :asg-sub (expr-grade-assignment) :asg-shl (expr-grade-assignment) :asg-shr (expr-grade-assignment) :asg-and (expr-grade-assignment) :asg-xor (expr-grade-assignment) :asg-ior (expr-grade-assignment)) :cond (expr-grade-conditional))))
Theorem:
(defthm expr-gradep-of-expr->grade (b* ((grade (expr->grade expr))) (expr-gradep grade)) :rule-classes :rewrite)
Theorem:
(defthm expr->grade-of-expr-fix-expr (equal (expr->grade (expr-fix expr)) (expr->grade expr)))
Theorem:
(defthm expr->grade-expr-equiv-congruence-on-expr (implies (expr-equiv expr expr-equiv) (equal (expr->grade expr) (expr->grade expr-equiv))) :rule-classes :congruence)