		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Write-var-value

Write a variable value to the computation state.

Signature
(write-var-value var val cstate) → new-cstate
Arguments: var — Guard (identifierp var).; val — Guard (valuep val).; cstate — Guard (cstatep cstate).
Returns: new-cstate — Type (cstate-resultp new-cstate).

An error is returned if the variable does not exist.

Definitions and Theorems

Function: write-var-value

(defun write-var-value (var val cstate)
  (declare (xargs :guard (and (identifierp var)
                              (valuep val)
                              (cstatep cstate))))
  (let ((__function__ 'write-var-value))
    (declare (ignorable __function__))
    (b* ((lstate (cstate->local cstate))
         (var-val (omap::assoc (identifier-fix var)
                               lstate))
         ((unless (consp var-val))
          (reserrf (list :variable-not-found (identifier-fix var))))
         (new-lstate (omap::update (identifier-fix var)
                                   (value-fix val)
                                   lstate))
         (new-cstate (change-cstate cstate
                                    :local new-lstate)))
      new-cstate)))

Theorem: cstate-resultp-of-write-var-value

(defthm cstate-resultp-of-write-var-value
  (b* ((new-cstate (write-var-value var val cstate)))
    (cstate-resultp new-cstate))
  :rule-classes :rewrite)

Theorem: error-info-wfp-of-write-var-value

(defthm error-info-wfp-of-write-var-value
  (b* ((?new-cstate (write-var-value var val cstate)))
    (implies (reserrp new-cstate)
             (error-info-wfp new-cstate))))

Theorem: write-var-value-of-identifier-fix-var

(defthm write-var-value-of-identifier-fix-var
  (equal (write-var-value (identifier-fix var)
                          val cstate)
         (write-var-value var val cstate)))

Theorem: write-var-value-identifier-equiv-congruence-on-var

(defthm write-var-value-identifier-equiv-congruence-on-var
  (implies (identifier-equiv var var-equiv)
           (equal (write-var-value var val cstate)
                  (write-var-value var-equiv val cstate)))
  :rule-classes :congruence)

Theorem: write-var-value-of-value-fix-val

(defthm write-var-value-of-value-fix-val
  (equal (write-var-value var (value-fix val)
                          cstate)
         (write-var-value var val cstate)))

Theorem: write-var-value-value-equiv-congruence-on-val

(defthm write-var-value-value-equiv-congruence-on-val
  (implies (value-equiv val val-equiv)
           (equal (write-var-value var val cstate)
                  (write-var-value var val-equiv cstate)))
  :rule-classes :congruence)

Theorem: write-var-value-of-cstate-fix-cstate

(defthm write-var-value-of-cstate-fix-cstate
  (equal (write-var-value var val (cstate-fix cstate))
         (write-var-value var val cstate)))

Theorem: write-var-value-cstate-equiv-congruence-on-cstate

(defthm write-var-value-cstate-equiv-congruence-on-cstate
  (implies (cstate-equiv cstate cstate-equiv)
           (equal (write-var-value var val cstate)
                  (write-var-value var val cstate-equiv)))
  :rule-classes :congruence)