		Search-engine friendly clone of the ACL2 documentation.

Read-write-variables

Write-var

Write a variable in the computation state.

Signature
(write-var var val compst) → new-compst
Arguments: var — Guard (identp var).; val — Guard (valuep val).; compst — Guard (compustatep compst).
Returns: new-compst — Type (compustate-resultp new-compst).

First we try automatic storage, if there are frames. If there is an error, we propagate it. If instead the variable was not found, we try static storage.

Definitions and Theorems

Function: write-var

(defun write-var (var val compst)
  (declare (xargs :guard (and (identp var)
                              (valuep val)
                              (compustatep compst))))
  (let ((__function__ 'write-var))
    (declare (ignorable __function__))
    (if (> (compustate-frames-number compst) 0)
        (b* ((new-compst (write-auto-var var val compst))
             ((when (errorp new-compst)) new-compst))
          (or new-compst
              (write-static-var var val compst)))
      (write-static-var var val compst))))

Theorem: compustate-resultp-of-write-var

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

Theorem: compustate-frames-number-of-write-var

(defthm compustate-frames-number-of-write-var
  (b* ((?new-compst (write-var var val compst)))
    (implies (compustatep new-compst)
             (equal (compustate-frames-number new-compst)
                    (compustate-frames-number compst)))))

Theorem: compustate-scopes-numbers-of-write-var

(defthm compustate-scopes-numbers-of-write-var
  (b* ((?new-compst (write-var var val compst)))
    (implies (compustatep new-compst)
             (equal (compustate-scopes-numbers new-compst)
                    (compustate-scopes-numbers compst)))))

Theorem: write-var-of-ident-fix-var

(defthm write-var-of-ident-fix-var
  (equal (write-var (ident-fix var) val compst)
         (write-var var val compst)))

Theorem: write-var-ident-equiv-congruence-on-var

(defthm write-var-ident-equiv-congruence-on-var
  (implies (ident-equiv var var-equiv)
           (equal (write-var var val compst)
                  (write-var var-equiv val compst)))
  :rule-classes :congruence)

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

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

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

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

Theorem: write-var-of-compustate-fix-compst

(defthm write-var-of-compustate-fix-compst
  (equal (write-var var val (compustate-fix compst))
         (write-var var val compst)))

Theorem: write-var-compustate-equiv-congruence-on-compst

(defthm write-var-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (write-var var val compst)
                  (write-var var val compst-equiv)))
  :rule-classes :congruence)