		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Expr-purep

Check if an expression is pure.

Signature
(expr-purep expr) → yes/no
Arguments: expr — Guard (exprp expr).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: expr-purep

(defun expr-purep (expr)
  (declare (xargs :guard (exprp expr)))
  (expr-case expr
             :ident t
             :const t
             :arrsub (and (expr-purep expr.arr)
                          (expr-purep expr.sub))
             :call nil
             :member (expr-purep expr.target)
             :memberp (expr-purep expr.target)
             :postinc nil
             :postdec nil
             :preinc nil
             :predec nil
             :unary (expr-purep expr.arg)
             :cast (expr-purep expr.arg)
             :binary (and (binop-purep expr.op)
                          (expr-purep expr.arg1)
                          (expr-purep expr.arg2))
             :cond (and (expr-purep expr.test)
                        (expr-purep expr.then)
                        (expr-purep expr.else))))

Theorem: booleanp-of-expr-purep

(defthm booleanp-of-expr-purep
  (b* ((yes/no (expr-purep expr)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: expr-purep-of-expr-fix-expr

(defthm expr-purep-of-expr-fix-expr
  (equal (expr-purep (expr-fix expr))
         (expr-purep expr)))

Theorem: expr-purep-expr-equiv-congruence-on-expr

(defthm expr-purep-expr-equiv-congruence-on-expr
  (implies (expr-equiv expr expr-equiv)
           (equal (expr-purep expr)
                  (expr-purep expr-equiv)))
  :rule-classes :congruence)