		Search-engine friendly clone of the ACL2 documentation.

Computation-states

Write-object

Write an object in the computation state.

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

If the object designator is a static variable, we write it in static storage. If the object designator is an automatic variable, we index the frame stack, we index the scope stack, and we find the variable by name, writing the new value there, provided it has the same type as the existing value; note that, as explained in objdesign, the indices start at the bottom, i.e. the end of the lists, so we reverse the lists before indexing them. If the object designator is for allocated storage, we check whether the heap has an object at the address, of the same type as the new object (note that, for arrays, the type includes the number of elements). If this checks succeed, we overwrite the object in the heap.

Otherwise, we retrieve the super-object, and we update its element or member, provided that the super-object is of the right kind. Then we recursively write the updated super-object.

If the object designator is an address, we store the value without removing the flexible array member (see remove-flexible-array-member). In all other cases, we remove it.

Definitions and Theorems

Function: write-object

(defun write-object (objdes val compst)
 (declare (xargs :guard (and (objdesignp objdes)
                             (valuep val)
                             (compustatep compst))))
 (let ((__function__ 'write-object))
  (declare (ignorable __function__))
  (objdesign-case
   objdes :static
   (b* ((static (compustate->static compst))
        (var+val (omap::assoc objdes.name static))
        ((when (not var+val))
         (error (list :static-var-not-found objdes.name)))
        ((unless (equal (type-of-value (cdr var+val))
                        (type-of-value val)))
         (error (list :static-var-mistype objdes.name
                      :required (type-of-value (cdr var+val))
                      :supplied (type-of-value val))))
        (new-static (omap::update objdes.name
                                  (remove-flexible-array-member val)
                                  static))
        (new-compst (change-compustate compst
                                       :static new-static)))
     new-compst)
   :auto
   (b*
    ((rev-frames (rev (compustate->frames compst)))
     ((unless (< objdes.frame (len rev-frames)))
      (error (list :frame-index-out-of-range objdes.frame)))
     (frame (nth objdes.frame rev-frames))
     (rev-scopes (rev (frame->scopes frame)))
     ((unless (< objdes.scope (len rev-scopes)))
      (error (list :scope-index-out-of-range objdes.scope)))
     (scope (nth objdes.scope rev-scopes))
     (var+val (omap::assoc objdes.name scope))
     ((unless (consp var+val))
      (error (list :name-not-found objdes.name)))
     (oldval (cdr var+val))
     (newval val)
     ((unless (equal (type-of-value newval)
                     (type-of-value oldval)))
      (error (list :write-auto-object-mistype objdes.name
                   :old (type-of-value oldval)
                   :new (type-of-value newval))))
     (new-scope (omap::update objdes.name
                              (remove-flexible-array-member newval)
                              scope))
     (rev-new-scopes (update-nth objdes.scope new-scope rev-scopes))
     (new-frame (change-frame frame
                              :scopes (rev rev-new-scopes)))
     (rev-new-frames (update-nth objdes.frame new-frame rev-frames))
     (new-compst (change-compustate compst
                                    :frames (rev rev-new-frames))))
    new-compst)
   :alloc
   (b* ((addr objdes.get)
        (heap (compustate->heap compst))
        (addr+obj (omap::assoc addr heap))
        ((unless (consp addr+obj))
         (error (list :address-not-found addr)))
        (obj (cdr addr+obj))
        ((unless (equal (type-of-value val)
                        (type-of-value obj)))
         (error (list :write-alloc-object-mistype
                      :old (type-of-value obj)
                      :new (type-of-value val))))
        (new-heap (omap::update addr (value-fix val)
                                heap))
        (new-compst (change-compustate compst
                                       :heap new-heap)))
     new-compst)
   :element
   (b* ((super (read-object objdes.super compst))
        ((when (errorp super)) super)
        ((unless (value-case super :array))
         (error (list :objdesign-mismatch (objdesign-fix objdes)
                      :required :array
                      :supplied super)))
        (new-super (value-array-write objdes.index val super))
        ((when (errorp new-super)) new-super))
     (write-object objdes.super new-super compst))
   :member
   (b* ((super (read-object objdes.super compst))
        ((when (errorp super)) super)
        ((unless (value-case super :struct))
         (error (list :objdesign-mismatch (objdesign-fix objdes)
                      :required :struct
                      :supplied super)))
        (new-super (value-struct-write objdes.name val super))
        ((when (errorp new-super)) new-super))
     (write-object objdes.super new-super compst)))))

Theorem: compustate-resultp-of-write-object

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

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

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

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

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

Theorem: compustatep-of-write-object-of-objdesign-of-var

(defthm compustatep-of-write-object-of-objdesign-of-var
 (b* ((objdes (objdesign-of-var var compst)))
  (implies objdes
           (equal (compustatep (write-object objdes val compst))
                  (equal (type-of-value (read-object objdes compst))
                         (type-of-value val))))))

Theorem: write-object-of-objdesign-fix-objdes

(defthm write-object-of-objdesign-fix-objdes
  (equal (write-object (objdesign-fix objdes)
                       val compst)
         (write-object objdes val compst)))

Theorem: write-object-objdesign-equiv-congruence-on-objdes

(defthm write-object-objdesign-equiv-congruence-on-objdes
  (implies (objdesign-equiv objdes objdes-equiv)
           (equal (write-object objdes val compst)
                  (write-object objdes-equiv val compst)))
  :rule-classes :congruence)

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

(defthm write-object-of-value-fix-val
  (equal (write-object objdes (value-fix val)
                       compst)
         (write-object objdes val compst)))

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

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

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

(defthm write-object-of-compustate-fix-compst
  (equal (write-object objdes val (compustate-fix compst))
         (write-object objdes val compst)))

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

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