		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Atc-var-assignablep

Check if a variable is assignable, based on whether it is in the innermost scope and based on the variables being currently affected.

Signature
(atc-var-assignablep var innermostp affect) → yes/no
Arguments: var — Guard (symbolp var).; innermostp — Guard (booleanp innermostp).; affect — Guard (symbol-listp affect).
Returns: yes/no — Type (booleanp yes/no), given (booleanp innermostp).

A variable may be destructively assigned to if any of the following conditions apply: (i) it is declared in the innermost scope, because in that case it cannot be accessed after exiting the scope; (ii) it is being affected, because in that case its modified value is returned and used in subsequent code; (iii) no variable is being affected, because in that case there is no subsequent code.

Definitions and Theorems

Function: atc-var-assignablep

(defun atc-var-assignablep (var innermostp affect)
  (declare (xargs :guard (and (symbolp var)
                              (booleanp innermostp)
                              (symbol-listp affect))))
  (let ((__function__ 'atc-var-assignablep))
    (declare (ignorable __function__))
    (or innermostp
        (and (member-eq var affect) t)
        (null affect))))

Theorem: booleanp-of-atc-var-assignablep

(defthm booleanp-of-atc-var-assignablep
 (implies (booleanp innermostp)
          (b* ((yes/no (atc-var-assignablep var innermostp affect)))
            (booleanp yes/no)))
 :rule-classes :rewrite)