		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Write-vars-values

Lift write-var-value to lists.

Signature
(write-vars-values vars vals cstate) → new-cstate
Arguments: vars — Guard (identifier-listp vars).; vals — Guard (value-listp vals).; cstate — Guard (cstatep cstate).
Returns: new-cstate — Type (cstate-resultp new-cstate).

It is an error if there are extra values or extra variables. Their number must be the same. We make this a run-time check because it is part of the conditions to be checked by the defensive dynamic semantics.

Definitions and Theorems

Function: write-vars-values

(defun write-vars-values (vars vals cstate)
 (declare (xargs :guard (and (identifier-listp vars)
                             (value-listp vals)
                             (cstatep cstate))))
 (let ((__function__ 'write-vars-values))
   (declare (ignorable __function__))
   (b*
     (((when (endp vars))
       (if (endp vals)
           (cstate-fix cstate)
         (reserrf (list :extra-values (value-list-fix vals)))))
      ((when (endp vals))
       (reserrf (list :extra-variables (identifier-list-fix vars))))
      ((okf cstate)
       (write-var-value (car vars)
                        (car vals)
                        cstate)))
     (write-vars-values (cdr vars)
                        (cdr vals)
                        cstate))))

Theorem: cstate-resultp-of-write-vars-values

(defthm cstate-resultp-of-write-vars-values
  (b* ((new-cstate (write-vars-values vars vals cstate)))
    (cstate-resultp new-cstate))
  :rule-classes :rewrite)

Theorem: error-info-wfp-of-write-vars-values

(defthm error-info-wfp-of-write-vars-values
  (b* ((?new-cstate (write-vars-values vars vals cstate)))
    (implies (reserrp new-cstate)
             (error-info-wfp new-cstate))))

Theorem: write-vars-values-of-identifier-list-fix-vars

(defthm write-vars-values-of-identifier-list-fix-vars
  (equal (write-vars-values (identifier-list-fix vars)
                            vals cstate)
         (write-vars-values vars vals cstate)))

Theorem: write-vars-values-identifier-list-equiv-congruence-on-vars

(defthm write-vars-values-identifier-list-equiv-congruence-on-vars
  (implies (identifier-list-equiv vars vars-equiv)
           (equal (write-vars-values vars vals cstate)
                  (write-vars-values vars-equiv vals cstate)))
  :rule-classes :congruence)

Theorem: write-vars-values-of-value-list-fix-vals

(defthm write-vars-values-of-value-list-fix-vals
  (equal (write-vars-values vars (value-list-fix vals)
                            cstate)
         (write-vars-values vars vals cstate)))

Theorem: write-vars-values-value-list-equiv-congruence-on-vals

(defthm write-vars-values-value-list-equiv-congruence-on-vals
  (implies (value-list-equiv vals vals-equiv)
           (equal (write-vars-values vars vals cstate)
                  (write-vars-values vars vals-equiv cstate)))
  :rule-classes :congruence)

Theorem: write-vars-values-of-cstate-fix-cstate

(defthm write-vars-values-of-cstate-fix-cstate
  (equal (write-vars-values vars vals (cstate-fix cstate))
         (write-vars-values vars vals cstate)))

Theorem: write-vars-values-cstate-equiv-congruence-on-cstate

(defthm write-vars-values-cstate-equiv-congruence-on-cstate
  (implies (cstate-equiv cstate cstate-equiv)
           (equal (write-vars-values vars vals cstate)
                  (write-vars-values vars vals cstate-equiv)))
  :rule-classes :congruence)