		Search-engine friendly clone of the ACL2 documentation.

Read-write-variables

Write-static-var

Write a varible in static storage.

Signature
(write-static-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).

If the variable is not found, we return an error. If the variable is found but its current value has a different type from the one of the new value, we return an error. Otherwise, we overwrite the old value with the new one.

Prior to storing the value, we remove its flexible array member, if any. See remove-flexible-array-member.

Definitions and Theorems

Function: write-static-var

(defun write-static-var (var val compst)
 (declare (xargs :guard (and (identp var)
                             (valuep val)
                             (compustatep compst))))
 (let ((__function__ 'write-static-var))
   (declare (ignorable __function__))
   (b* ((static (compustate->static compst))
        (pair (omap::assoc (ident-fix var) static))
        ((when (not pair))
         (error (list :static-var-not-found (ident-fix var))))
        ((unless (equal (type-of-value (cdr pair))
                        (type-of-value val)))
         (error (list :static-var-mistype (ident-fix var)
                      :required (type-of-value (cdr pair))
                      :supplied (type-of-value val))))
        (new-static (omap::update (ident-fix var)
                                  (remove-flexible-array-member val)
                                  static))
        (new-compst (change-compustate compst
                                       :static new-static)))
     new-compst)))

Theorem: compustate-resultp-of-write-static-var

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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