		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Add-var-value

Add a variable with a value to the computation state.

Signature
(add-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 already exists.

Definitions and Theorems

Function: add-var-value

(defun add-var-value (var val cstate)
 (declare (xargs :guard (and (identifierp var)
                             (valuep val)
                             (cstatep cstate))))
 (let ((__function__ 'add-var-value))
  (declare (ignorable __function__))
  (b*
   ((lstate (cstate->local cstate))
    (var-val (omap::assoc (identifier-fix var)
                          lstate))
    ((when (consp var-val))
     (reserrf (list :variable-already-exists (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-add-var-value

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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