Check if a multiple variable declaration is safe.
(check-safe-variable-multi names init varset funtab) → varset?
This is used by check-safe-statement: see that function's documentation for background.
The name of the variables must be identifiers that are not already in the variable table. They must also be distinct and at least two. The expression is checked if present, and it must return the same number of results as the number of variables.
Function:
(defun check-safe-variable-multi (names init varset funtab) (declare (xargs :guard (and (identifier-listp names) (funcall-optionp init) (identifier-setp varset) (funtablep funtab)))) (let ((__function__ 'check-safe-variable-multi)) (declare (ignorable __function__)) (b* ((names (identifier-list-fix names)) (init (funcall-option-fix init)) ((okf varset-new) (add-vars names varset)) ((unless (>= (len names) 2)) (reserrf (list :declare-zero-one-var names))) ((when (not init)) varset-new) ((okf results) (check-safe-funcall init varset funtab)) ((unless (= results (len names))) (reserrf (list :declare-multi-var-mismatch names results)))) varset-new)))
Theorem:
(defthm identifier-set-resultp-of-check-safe-variable-multi (b* ((varset? (check-safe-variable-multi names init varset funtab))) (identifier-set-resultp varset?)) :rule-classes :rewrite)
Theorem:
(defthm check-safe-variable-multi-of-identifier-list-fix-names (equal (check-safe-variable-multi (identifier-list-fix names) init varset funtab) (check-safe-variable-multi names init varset funtab)))
Theorem:
(defthm check-safe-variable-multi-identifier-list-equiv-congruence-on-names (implies (identifier-list-equiv names names-equiv) (equal (check-safe-variable-multi names init varset funtab) (check-safe-variable-multi names-equiv init varset funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-variable-multi-of-funcall-option-fix-init (equal (check-safe-variable-multi names (funcall-option-fix init) varset funtab) (check-safe-variable-multi names init varset funtab)))
Theorem:
(defthm check-safe-variable-multi-funcall-option-equiv-congruence-on-init (implies (funcall-option-equiv init init-equiv) (equal (check-safe-variable-multi names init varset funtab) (check-safe-variable-multi names init-equiv varset funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-variable-multi-of-identifier-set-fix-varset (equal (check-safe-variable-multi names init (identifier-set-fix varset) funtab) (check-safe-variable-multi names init varset funtab)))
Theorem:
(defthm check-safe-variable-multi-identifier-set-equiv-congruence-on-varset (implies (identifier-set-equiv varset varset-equiv) (equal (check-safe-variable-multi names init varset funtab) (check-safe-variable-multi names init varset-equiv funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-variable-multi-of-funtable-fix-funtab (equal (check-safe-variable-multi names init varset (funtable-fix funtab)) (check-safe-variable-multi names init varset funtab)))
Theorem:
(defthm check-safe-variable-multi-funtable-equiv-congruence-on-funtab (implies (funtable-equiv funtab funtab-equiv) (equal (check-safe-variable-multi names init varset funtab) (check-safe-variable-multi names init varset funtab-equiv))) :rule-classes :congruence)