		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-formal-affectablep

Check if a formal parameter is a affectable.

Signature
(atc-formal-affectablep formal typed-formals) → yes/no
Arguments: formal — Guard (symbolp formal).; typed-formals — Guard (atc-symbol-varinfo-alistp typed-formals).
Returns: yes/no — Type (booleanp yes/no).

By this we mean that the formal parameter either has pointer or array type or refers to an external object. That is, it is the kind of parameter that may be affected in a function, and that therefore must be returned by the function if affected.

Definitions and Theorems

Function: atc-formal-affectablep

(defun atc-formal-affectablep (formal typed-formals)
 (declare
     (xargs :guard (and (symbolp formal)
                        (atc-symbol-varinfo-alistp typed-formals))))
 (let ((__function__ 'atc-formal-affectablep))
   (declare (ignorable __function__))
   (b*
    ((pair (assoc-eq (symbol-fix formal)
                     (atc-symbol-varinfo-alist-fix typed-formals))))
    (and (consp pair)
         (b* ((info (cdr pair))
              (type (atc-var-info->type info)))
           (or (type-case type :pointer)
               (type-case type :array)
               (atc-var-info->externalp info)))))))

Theorem: booleanp-of-atc-formal-affectablep

(defthm booleanp-of-atc-formal-affectablep
  (b* ((yes/no (atc-formal-affectablep formal typed-formals)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: atc-formal-affectablep-of-symbol-fix-formal

(defthm atc-formal-affectablep-of-symbol-fix-formal
  (equal (atc-formal-affectablep (symbol-fix formal)
                                 typed-formals)
         (atc-formal-affectablep formal typed-formals)))

Theorem: atc-formal-affectablep-symbol-equiv-congruence-on-formal

(defthm atc-formal-affectablep-symbol-equiv-congruence-on-formal
  (implies
       (acl2::symbol-equiv formal formal-equiv)
       (equal (atc-formal-affectablep formal typed-formals)
              (atc-formal-affectablep formal-equiv typed-formals)))
  :rule-classes :congruence)

Theorem: atc-formal-affectablep-of-atc-symbol-varinfo-alist-fix-typed-formals

(defthm
 atc-formal-affectablep-of-atc-symbol-varinfo-alist-fix-typed-formals
 (equal (atc-formal-affectablep
             formal
             (atc-symbol-varinfo-alist-fix typed-formals))
        (atc-formal-affectablep formal typed-formals)))

Theorem: atc-formal-affectablep-atc-symbol-varinfo-alist-equiv-congruence-on-typed-formals

(defthm
 atc-formal-affectablep-atc-symbol-varinfo-alist-equiv-congruence-on-typed-formals
 (implies
  (atc-symbol-varinfo-alist-equiv typed-formals typed-formals-equiv)
  (equal (atc-formal-affectablep formal typed-formals)
         (atc-formal-affectablep formal typed-formals-equiv)))
 :rule-classes :congruence)