		Search-engine friendly clone of the ACL2 documentation.

Increment-elim

Vl-exprlist-increwrite

Main function for rewriting expression lists.

Signature
(vl-exprlist-increwrite x loc) → (mv new-x pre post)
Arguments: x — Expressions to rewrite. May contain increments, decrements, or assignment expressions.
Guard (vl-exprlist-p x).; loc — Location to use for new assignment statements.
Guard (vl-location-p loc).
Returns: new-x — Rewritten version of x, free of increment, decrement, and assignment operators. Equivalent to x assuming that: (1) the pre-increment stuff is done first, (2) the post-increment stuff is done afterwards, and (3) there are no ambiguities.
Type (vl-exprlist-p new-x).; pre — New assignments that must happen before new-x, in the proper order that they should be performed in.
Type (vl-stmtlist-p pre).; post — New assignments that must happen after new-x, in the proper order that they should be performed in.
Type (vl-stmtlist-p post).

Definitions and Theorems

Function: vl-exprlist-increwrite

(defun vl-exprlist-increwrite (x loc)
  (declare (xargs :guard (and (vl-exprlist-p x)
                              (vl-location-p loc))))
  (let ((__function__ 'vl-exprlist-increwrite))
    (declare (ignorable __function__))
    (b* ((x (vl-exprlist-fix x))
         ((unless (vl-exprlist-has-incexprs-p x))
          (mv x nil nil))
         ((mv new-x pre-rev post-rev)
          (vl-exprlist-increwrite-aux x nil nil loc)))
      (mv new-x (rev pre-rev)
          (rev post-rev)))))

Theorem: vl-exprlist-p-of-vl-exprlist-increwrite.new-x

(defthm vl-exprlist-p-of-vl-exprlist-increwrite.new-x
  (b* (((mv ?new-x ?pre ?post)
        (vl-exprlist-increwrite x loc)))
    (vl-exprlist-p new-x))
  :rule-classes :rewrite)

Theorem: vl-stmtlist-p-of-vl-exprlist-increwrite.pre

(defthm vl-stmtlist-p-of-vl-exprlist-increwrite.pre
  (b* (((mv ?new-x ?pre ?post)
        (vl-exprlist-increwrite x loc)))
    (vl-stmtlist-p pre))
  :rule-classes :rewrite)

Theorem: vl-stmtlist-p-of-vl-exprlist-increwrite.post

(defthm vl-stmtlist-p-of-vl-exprlist-increwrite.post
  (b* (((mv ?new-x ?pre ?post)
        (vl-exprlist-increwrite x loc)))
    (vl-stmtlist-p post))
  :rule-classes :rewrite)

Theorem: vl-exprlist-increwrite-of-vl-exprlist-fix-x

(defthm vl-exprlist-increwrite-of-vl-exprlist-fix-x
  (equal (vl-exprlist-increwrite (vl-exprlist-fix x)
                                 loc)
         (vl-exprlist-increwrite x loc)))

Theorem: vl-exprlist-increwrite-vl-exprlist-equiv-congruence-on-x

(defthm vl-exprlist-increwrite-vl-exprlist-equiv-congruence-on-x
  (implies (vl-exprlist-equiv x x-equiv)
           (equal (vl-exprlist-increwrite x loc)
                  (vl-exprlist-increwrite x-equiv loc)))
  :rule-classes :congruence)

Theorem: vl-exprlist-increwrite-of-vl-location-fix-loc

(defthm vl-exprlist-increwrite-of-vl-location-fix-loc
  (equal (vl-exprlist-increwrite x (vl-location-fix loc))
         (vl-exprlist-increwrite x loc)))

Theorem: vl-exprlist-increwrite-vl-location-equiv-congruence-on-loc

(defthm vl-exprlist-increwrite-vl-location-equiv-congruence-on-loc
  (implies (vl-location-equiv loc loc-equiv)
           (equal (vl-exprlist-increwrite x loc)
                  (vl-exprlist-increwrite x loc-equiv)))
  :rule-classes :congruence)