		Search-engine friendly clone of the ACL2 documentation.

Increment-elim

Vl-expr-increwrite

Main function for rewriting expressions.

Signature
(vl-expr-increwrite x loc) → (mv new-x pre post)
Arguments: x — Expression to rewrite. May contain increments, decrements, or assignment expressions.
Guard (vl-expr-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-expr-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-expr-increwrite

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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