		Search-engine friendly clone of the ACL2 documentation.

Static-safety-checking

Check-safe-assign-multi

Check if a multiple assignment is safe.

Signature
(check-safe-assign-multi targets value varset funtab) → _
Arguments: targets — Guard (path-listp targets).; value — Guard (funcallp value).; varset — Guard (identifier-setp varset).; funtab — Guard (funtablep funtab).
Returns: _ — Type (reserr-optionp _).

Similarly to check-safe-expression, for now we require each path to be a singleton; see discussion there about non-singleton paths.

We check the function call, and ensure that it returns a number of results equal to the number of variables. The variables must be two or more.

Definitions and Theorems

Function: check-safe-assign-multi

(defun check-safe-assign-multi (targets value varset funtab)
 (declare (xargs :guard (and (path-listp targets)
                             (funcallp value)
                             (identifier-setp varset)
                             (funtablep funtab))))
 (let ((__function__ 'check-safe-assign-multi))
  (declare (ignorable __function__))
  (b*
   (((okf &)
     (check-safe-path-list targets varset))
    ((unless (>= (len targets) 2))
     (reserrf (list :assign-zero-one-path (path-list-fix targets))))
    ((okf results)
     (check-safe-funcall value varset funtab))
    ((unless (= results (len targets)))
     (reserrf (list :assign-single-var-mismatch
                    (path-list-fix targets)
                    results))))
   nil)))

Theorem: reserr-optionp-of-check-safe-assign-multi

(defthm reserr-optionp-of-check-safe-assign-multi
  (b* ((_ (check-safe-assign-multi targets value varset funtab)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: check-safe-assign-multi-of-path-list-fix-targets

(defthm check-safe-assign-multi-of-path-list-fix-targets
  (equal (check-safe-assign-multi (path-list-fix targets)
                                  value varset funtab)
         (check-safe-assign-multi targets value varset funtab)))

Theorem: check-safe-assign-multi-path-list-equiv-congruence-on-targets

(defthm
      check-safe-assign-multi-path-list-equiv-congruence-on-targets
 (implies
  (path-list-equiv targets targets-equiv)
  (equal
       (check-safe-assign-multi targets value varset funtab)
       (check-safe-assign-multi targets-equiv value varset funtab)))
 :rule-classes :congruence)

Theorem: check-safe-assign-multi-of-funcall-fix-value

(defthm check-safe-assign-multi-of-funcall-fix-value
  (equal (check-safe-assign-multi targets (funcall-fix value)
                                  varset funtab)
         (check-safe-assign-multi targets value varset funtab)))

Theorem: check-safe-assign-multi-funcall-equiv-congruence-on-value

(defthm check-safe-assign-multi-funcall-equiv-congruence-on-value
 (implies
  (funcall-equiv value value-equiv)
  (equal
       (check-safe-assign-multi targets value varset funtab)
       (check-safe-assign-multi targets value-equiv varset funtab)))
 :rule-classes :congruence)

Theorem: check-safe-assign-multi-of-identifier-set-fix-varset

(defthm check-safe-assign-multi-of-identifier-set-fix-varset
  (equal (check-safe-assign-multi targets
                                  value (identifier-set-fix varset)
                                  funtab)
         (check-safe-assign-multi targets value varset funtab)))

Theorem: check-safe-assign-multi-identifier-set-equiv-congruence-on-varset

(defthm
  check-safe-assign-multi-identifier-set-equiv-congruence-on-varset
 (implies
  (identifier-set-equiv varset varset-equiv)
  (equal
       (check-safe-assign-multi targets value varset funtab)
       (check-safe-assign-multi targets value varset-equiv funtab)))
 :rule-classes :congruence)

Theorem: check-safe-assign-multi-of-funtable-fix-funtab

(defthm check-safe-assign-multi-of-funtable-fix-funtab
 (equal (check-safe-assign-multi targets
                                 value varset (funtable-fix funtab))
        (check-safe-assign-multi targets value varset funtab)))

Theorem: check-safe-assign-multi-funtable-equiv-congruence-on-funtab

(defthm check-safe-assign-multi-funtable-equiv-congruence-on-funtab
 (implies
  (funtable-equiv funtab funtab-equiv)
  (equal
       (check-safe-assign-multi targets value varset funtab)
       (check-safe-assign-multi targets value varset funtab-equiv)))
 :rule-classes :congruence)