		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Stmts/blocks-nocallsp

Check if statements, block items, and lists of block items do not contain any function calls.

Definitions and Theorems

Function: stmt-nocallsp

(defun stmt-nocallsp (stmt)
  (declare (xargs :guard (stmtp stmt)))
  (let ((__function__ 'stmt-nocallsp))
    (declare (ignorable __function__))
    (stmt-case stmt
               :labeled (and (label-nocallsp stmt.label)
                             (stmt-nocallsp stmt.body))
               :compound (block-item-list-nocallsp stmt.items)
               :expr (expr-nocallsp stmt.get)
               :null t
               :if (and (expr-nocallsp stmt.test)
                        (stmt-nocallsp stmt.then))
               :ifelse (and (expr-nocallsp stmt.test)
                            (stmt-nocallsp stmt.then)
                            (stmt-nocallsp stmt.else))
               :switch (and (expr-nocallsp stmt.ctrl)
                            (stmt-nocallsp stmt.body))
               :while (and (expr-nocallsp stmt.test)
                           (stmt-nocallsp stmt.body))
               :dowhile (and (stmt-nocallsp stmt.body)
                             (expr-nocallsp stmt.test))
               :for (and (expr-option-nocallsp stmt.init)
                         (expr-option-nocallsp stmt.test)
                         (expr-option-nocallsp stmt.next)
                         (stmt-nocallsp stmt.body))
               :goto t
               :continue t
               :break t
               :return (expr-option-nocallsp stmt.value))))

Function: block-item-nocallsp

(defun block-item-nocallsp (item)
  (declare (xargs :guard (block-itemp item)))
  (let ((__function__ 'block-item-nocallsp))
    (declare (ignorable __function__))
    (block-item-case item
                     :declon (obj-declon-nocallsp item.get)
                     :stmt (stmt-nocallsp item.get))))

Function: block-item-list-nocallsp

(defun block-item-list-nocallsp (items)
  (declare (xargs :guard (block-item-listp items)))
  (let ((__function__ 'block-item-list-nocallsp))
    (declare (ignorable __function__))
    (or (endp items)
        (and (block-item-nocallsp (car items))
             (block-item-list-nocallsp (cdr items))))))

Theorem: return-type-of-stmt-nocallsp.yes/no

(defthm return-type-of-stmt-nocallsp.yes/no
  (b* ((?yes/no (stmt-nocallsp stmt)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: return-type-of-block-item-nocallsp.yes/no

(defthm return-type-of-block-item-nocallsp.yes/no
  (b* ((?yes/no (block-item-nocallsp item)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: return-type-of-block-item-list-nocallsp.yes/no

(defthm return-type-of-block-item-list-nocallsp.yes/no
  (b* ((?yes/no (block-item-list-nocallsp items)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: stmt-nocallsp-of-stmt-fix-stmt

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

Theorem: block-item-nocallsp-of-block-item-fix-item

(defthm block-item-nocallsp-of-block-item-fix-item
  (equal (block-item-nocallsp (block-item-fix item))
         (block-item-nocallsp item)))

Theorem: block-item-list-nocallsp-of-block-item-list-fix-items

(defthm block-item-list-nocallsp-of-block-item-list-fix-items
  (equal (block-item-list-nocallsp (block-item-list-fix items))
         (block-item-list-nocallsp items)))

Theorem: stmt-nocallsp-stmt-equiv-congruence-on-stmt

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

Theorem: block-item-nocallsp-block-item-equiv-congruence-on-item

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

Theorem: block-item-list-nocallsp-block-item-list-equiv-congruence-on-items

(defthm
 block-item-list-nocallsp-block-item-list-equiv-congruence-on-items
 (implies (block-item-list-equiv items items-equiv)
          (equal (block-item-list-nocallsp items)
                 (block-item-list-nocallsp items-equiv)))
 :rule-classes :congruence)

Function: block-item-list-nocalls

(defun block-item-list-nocalls (x)
  (declare (xargs :guard (block-item-listp x)))
  (let ((__function__ 'block-item-list-nocalls))
    (declare (ignorable __function__))
    (if (consp x)
        (and (block-item-nocallsp (car x))
             (block-item-list-nocalls (cdr x)))
      t)))

Theorem: block-item-list-nocalls-of-cons

(defthm block-item-list-nocalls-of-cons
  (equal (block-item-list-nocalls (cons acl2::a acl2::x))
         (and (block-item-nocallsp acl2::a)
              (block-item-list-nocalls acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: block-item-list-nocalls-of-cdr-when-block-item-list-nocalls

(defthm block-item-list-nocalls-of-cdr-when-block-item-list-nocalls
  (implies (block-item-list-nocalls (double-rewrite acl2::x))
           (block-item-list-nocalls (cdr acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: block-item-list-nocalls-when-not-consp

(defthm block-item-list-nocalls-when-not-consp
  (implies (not (consp acl2::x))
           (block-item-list-nocalls acl2::x))
  :rule-classes ((:rewrite)))

Theorem: block-item-nocallsp-of-car-when-block-item-list-nocalls

(defthm block-item-nocallsp-of-car-when-block-item-list-nocalls
  (implies (block-item-list-nocalls acl2::x)
           (block-item-nocallsp (car acl2::x)))
  :rule-classes ((:rewrite)))

Theorem: block-item-list-nocalls-of-append

(defthm block-item-list-nocalls-of-append
  (equal (block-item-list-nocalls (append acl2::a acl2::b))
         (and (block-item-list-nocalls acl2::a)
              (block-item-list-nocalls acl2::b)))
  :rule-classes ((:rewrite)))

Theorem: block-item-list-nocalls-of-list-fix

(defthm block-item-list-nocalls-of-list-fix
  (equal (block-item-list-nocalls (list-fix acl2::x))
         (block-item-list-nocalls acl2::x))
  :rule-classes ((:rewrite)))

Theorem: block-item-list-nocalls-of-rev

(defthm block-item-list-nocalls-of-rev
  (equal (block-item-list-nocalls (rev acl2::x))
         (block-item-list-nocalls (list-fix acl2::x)))
  :rule-classes ((:rewrite)))

Subtopics

Block-item-nocallsp: Check if a block item does not contain any function calls.
Block-item-list-nocallsp: Check if a list of block items does not contain any function calls.
Stmt-nocallsp: Check if a statement does not contain any function calls.