		Search-engine friendly clone of the ACL2 documentation.

Function-recursion

Statements-callees

Functions called by statements, lists of statements, branches, and lists of branches.

Definitions and Theorems

Function: statement-callees

(defun statement-callees (stmt)
 (declare (xargs :guard (statementp stmt)))
 (let ((__function__ 'statement-callees))
   (declare (ignorable __function__))
   (statement-case stmt
                   :let (vardecl-callees stmt.get)
                   :const (constdecl-callees stmt.get)
                   :assign (union (expression-callees stmt.left)
                                  (expression-callees stmt.right))
                   :return (expression-callees stmt.value)
                   :for (union (union (expression-callees stmt.from)
                                      (expression-callees stmt.to))
                               (statement-list-callees stmt.body))
                   :if (union (branch-list-callees stmt.branches)
                              (statement-list-callees stmt.else))
                   :console (console-callees stmt.get)
                   :finalize nil
                   :increment nil
                   :decrement nil
                   :block (statement-list-callees stmt.get))))

Function: statement-list-callees

(defun statement-list-callees (stmts)
  (declare (xargs :guard (statement-listp stmts)))
  (let ((__function__ 'statement-list-callees))
    (declare (ignorable __function__))
    (cond ((endp stmts) nil)
          (t (union (statement-callees (car stmts))
                    (statement-list-callees (cdr stmts)))))))

Function: branch-callees

(defun branch-callees (branch)
  (declare (xargs :guard (branchp branch)))
  (let ((__function__ 'branch-callees))
    (declare (ignorable __function__))
    (union (expression-callees (branch->test branch))
           (statement-list-callees (branch->body branch)))))

Function: branch-list-callees

(defun branch-list-callees (branches)
  (declare (xargs :guard (branch-listp branches)))
  (let ((__function__ 'branch-list-callees))
    (declare (ignorable __function__))
    (cond ((endp branches) nil)
          (t (union (branch-callees (car branches))
                    (branch-list-callees (cdr branches)))))))

Theorem: return-type-of-statement-callees.callees

(defthm return-type-of-statement-callees.callees
  (b* ((?callees (statement-callees stmt)))
    (identifier-setp callees))
  :rule-classes :rewrite)

Theorem: return-type-of-statement-list-callees.callees

(defthm return-type-of-statement-list-callees.callees
  (b* ((?callees (statement-list-callees stmts)))
    (identifier-setp callees))
  :rule-classes :rewrite)

Theorem: return-type-of-branch-callees.callees

(defthm return-type-of-branch-callees.callees
  (b* ((?callees (branch-callees branch)))
    (identifier-setp callees))
  :rule-classes :rewrite)

Theorem: return-type-of-branch-list-callees.callees

(defthm return-type-of-branch-list-callees.callees
  (b* ((?callees (branch-list-callees branches)))
    (identifier-setp callees))
  :rule-classes :rewrite)

Theorem: statement-callees-of-statement-fix-stmt

(defthm statement-callees-of-statement-fix-stmt
  (equal (statement-callees (statement-fix stmt))
         (statement-callees stmt)))

Theorem: statement-list-callees-of-statement-list-fix-stmts

(defthm statement-list-callees-of-statement-list-fix-stmts
  (equal (statement-list-callees (statement-list-fix stmts))
         (statement-list-callees stmts)))

Theorem: branch-callees-of-branch-fix-branch

(defthm branch-callees-of-branch-fix-branch
  (equal (branch-callees (branch-fix branch))
         (branch-callees branch)))

Theorem: branch-list-callees-of-branch-list-fix-branches

(defthm branch-list-callees-of-branch-list-fix-branches
  (equal (branch-list-callees (branch-list-fix branches))
         (branch-list-callees branches)))

Theorem: statement-callees-statement-equiv-congruence-on-stmt

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

Theorem: statement-list-callees-statement-list-equiv-congruence-on-stmts

(defthm
    statement-list-callees-statement-list-equiv-congruence-on-stmts
  (implies (statement-list-equiv stmts stmts-equiv)
           (equal (statement-list-callees stmts)
                  (statement-list-callees stmts-equiv)))
  :rule-classes :congruence)

Theorem: branch-callees-branch-equiv-congruence-on-branch

(defthm branch-callees-branch-equiv-congruence-on-branch
  (implies (branch-equiv branch branch-equiv)
           (equal (branch-callees branch)
                  (branch-callees branch-equiv)))
  :rule-classes :congruence)

Theorem: branch-list-callees-branch-list-equiv-congruence-on-branches

(defthm branch-list-callees-branch-list-equiv-congruence-on-branches
  (implies (branch-list-equiv branches branches-equiv)
           (equal (branch-list-callees branches)
                  (branch-list-callees branches-equiv)))
  :rule-classes :congruence)

Subtopics

Statement-list-callees: Functions called by a list of statements.
Branch-list-callees: Functions called by a list of branchess.
Statement-callees: Functions called by a statement.
Branch-callees: Functions called by a branch.