		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Expr-nocallsp

Check if an expression does not contain any function calls.

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

Definitions and Theorems

Function: expr-nocallsp

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

Theorem: booleanp-of-expr-nocallsp

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

Theorem: expr-nocallsp-of-expr-fix-expr

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

Theorem: expr-nocallsp-expr-equiv-congruence-on-expr

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