		Search-engine friendly clone of the ACL2 documentation.

Atj-post-translation-remove-array-write-calls

Atj-remove-array-write-calls

Remove array write method calls from a block.

Signature
(atj-remove-array-write-calls block) → new-block
Arguments: block — Guard (jblockp block).
Returns: new-block — Type (jblockp new-block).

This puts together the two transformations described in atj-post-translation-remove-array-write-calls.

We also ensure that, after the transformations, no more array write method calls remain.

Definitions and Theorems

Function: atj-remove-array-write-calls

(defun atj-remove-array-write-calls (block)
 (declare (xargs :guard (jblockp block)))
 (let ((__function__ 'atj-remove-array-write-calls))
  (declare (ignorable __function__))
  (b*
   ((block (atj-remove-array-write-call-asgs-in-jblock block))
    (block (atj-remove-array-write-call-returns-in-jblock block))
    ((unless (atj-ensure-no-array-write-calls block))
     (raise
      "Internal error: ~
                the block ~x0 contains array write method calls."
      block)))
   block)))

Theorem: jblockp-of-atj-remove-array-write-calls

(defthm jblockp-of-atj-remove-array-write-calls
  (b* ((new-block (atj-remove-array-write-calls block)))
    (jblockp new-block))
  :rule-classes :rewrite)

Theorem: atj-remove-array-write-calls-of-jblock-fix-block

(defthm atj-remove-array-write-calls-of-jblock-fix-block
  (equal (atj-remove-array-write-calls (jblock-fix block))
         (atj-remove-array-write-calls block)))

Theorem: atj-remove-array-write-calls-jblock-equiv-congruence-on-block

(defthm
      atj-remove-array-write-calls-jblock-equiv-congruence-on-block
  (implies (jblock-equiv block block-equiv)
           (equal (atj-remove-array-write-calls block)
                  (atj-remove-array-write-calls block-equiv)))
  :rule-classes :congruence)