		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabscopes-traverse/update

Signature
(vl-elabscopes-traverse/update trav scopes) → (mv new-scopes undo)
Arguments: trav — Guard (vl-elabtraversal-p trav).; scopes — Guard (vl-elabscopes-p scopes).
Returns: new-scopes — Type (vl-elabscopes-p new-scopes).; undo — Reversed elabpath that undoes this traversal.
Type (vl-elabtraversal-p undo).

Definitions and Theorems

Function: vl-elabscopes-traverse/update

(defun vl-elabscopes-traverse/update (trav scopes)
  (declare (xargs :guard (and (vl-elabtraversal-p trav)
                              (vl-elabscopes-p scopes))))
  (let ((__function__ 'vl-elabscopes-traverse/update))
    (declare (ignorable __function__))
    (if (atom trav)
        (mv (vl-elabscopes-fix scopes) nil)
      (b* (((mv scopes undo1)
            (vl-elabscopes-do-instruction/update (car trav)
                                                 scopes))
           ((mv scopes undo2)
            (vl-elabscopes-traverse/update (cdr trav)
                                           scopes)))
        (mv scopes
            (vl-elabpaths-append undo1 undo2))))))

Theorem: vl-elabscopes-p-of-vl-elabscopes-traverse/update.new-scopes

(defthm vl-elabscopes-p-of-vl-elabscopes-traverse/update.new-scopes
  (b* (((mv ?new-scopes ?undo)
        (vl-elabscopes-traverse/update trav scopes)))
    (vl-elabscopes-p new-scopes))
  :rule-classes :rewrite)

Theorem: vl-elabtraversal-p-of-vl-elabscopes-traverse/update.undo

(defthm vl-elabtraversal-p-of-vl-elabscopes-traverse/update.undo
  (b* (((mv ?new-scopes ?undo)
        (vl-elabscopes-traverse/update trav scopes)))
    (vl-elabtraversal-p undo))
  :rule-classes :rewrite)

Theorem: vl-elabscopes-traverse/update-of-vl-elabtraversal-fix-trav

(defthm vl-elabscopes-traverse/update-of-vl-elabtraversal-fix-trav
  (equal (vl-elabscopes-traverse/update (vl-elabtraversal-fix trav)
                                        scopes)
         (vl-elabscopes-traverse/update trav scopes)))

Theorem: vl-elabscopes-traverse/update-vl-elabtraversal-equiv-congruence-on-trav

(defthm
 vl-elabscopes-traverse/update-vl-elabtraversal-equiv-congruence-on-trav
 (implies (vl-elabtraversal-equiv trav trav-equiv)
          (equal (vl-elabscopes-traverse/update trav scopes)
                 (vl-elabscopes-traverse/update trav-equiv scopes)))
 :rule-classes :congruence)

Theorem: vl-elabscopes-traverse/update-of-vl-elabscopes-fix-scopes

(defthm vl-elabscopes-traverse/update-of-vl-elabscopes-fix-scopes
 (equal
     (vl-elabscopes-traverse/update trav (vl-elabscopes-fix scopes))
     (vl-elabscopes-traverse/update trav scopes)))

Theorem: vl-elabscopes-traverse/update-vl-elabscopes-equiv-congruence-on-scopes

(defthm
 vl-elabscopes-traverse/update-vl-elabscopes-equiv-congruence-on-scopes
 (implies (vl-elabscopes-equiv scopes scopes-equiv)
          (equal (vl-elabscopes-traverse/update trav scopes)
                 (vl-elabscopes-traverse/update trav scopes-equiv)))
 :rule-classes :congruence)