Check if a multiple assignment is safe.
(check-safe-assign-multi targets value varset funtab) → _
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.
Function:
(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:
(defthm reserr-optionp-of-check-safe-assign-multi (b* ((_ (check-safe-assign-multi targets value varset funtab))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)