Check if a single variable declaration is safe.
(check-safe-variable-single name init varset funtab) → varset?
This is used by check-safe-statement: see that function's documentation for background.
The name of the variable must be an identifier that is not already in the variable table. The expression is checked if present, and it must return exactly one result.
Function:
(defun check-safe-variable-single (name init varset funtab) (declare (xargs :guard (and (identifierp name) (expression-optionp init) (identifier-setp varset) (funtablep funtab)))) (let ((__function__ 'check-safe-variable-single)) (declare (ignorable __function__)) (b* ((name (identifier-fix name)) (init (expression-option-fix init)) ((okf varset-new) (add-var name varset)) ((when (not init)) varset-new) ((okf results) (check-safe-expression init varset funtab)) ((unless (= results 1)) (reserrf (list :declare-single-var-mismatch name results)))) varset-new)))
Theorem:
(defthm identifier-set-resultp-of-check-safe-variable-single (b* ((varset? (check-safe-variable-single name init varset funtab))) (identifier-set-resultp varset?)) :rule-classes :rewrite)
Theorem:
(defthm check-safe-variable-single-of-identifier-fix-name (equal (check-safe-variable-single (identifier-fix name) init varset funtab) (check-safe-variable-single name init varset funtab)))
Theorem:
(defthm check-safe-variable-single-identifier-equiv-congruence-on-name (implies (identifier-equiv name name-equiv) (equal (check-safe-variable-single name init varset funtab) (check-safe-variable-single name-equiv init varset funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-variable-single-of-expression-option-fix-init (equal (check-safe-variable-single name (expression-option-fix init) varset funtab) (check-safe-variable-single name init varset funtab)))
Theorem:
(defthm check-safe-variable-single-expression-option-equiv-congruence-on-init (implies (expression-option-equiv init init-equiv) (equal (check-safe-variable-single name init varset funtab) (check-safe-variable-single name init-equiv varset funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-variable-single-of-identifier-set-fix-varset (equal (check-safe-variable-single name init (identifier-set-fix varset) funtab) (check-safe-variable-single name init varset funtab)))
Theorem:
(defthm check-safe-variable-single-identifier-set-equiv-congruence-on-varset (implies (identifier-set-equiv varset varset-equiv) (equal (check-safe-variable-single name init varset funtab) (check-safe-variable-single name init varset-equiv funtab))) :rule-classes :congruence)
Theorem:
(defthm check-safe-variable-single-of-funtable-fix-funtab (equal (check-safe-variable-single name init varset (funtable-fix funtab)) (check-safe-variable-single name init varset funtab)))
Theorem:
(defthm check-safe-variable-single-funtable-equiv-congruence-on-funtab (implies (funtable-equiv funtab funtab-equiv) (equal (check-safe-variable-single name init varset funtab) (check-safe-variable-single name init varset funtab-equiv))) :rule-classes :congruence)