		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabscopes-do-instruction/update

Signature
(vl-elabscopes-do-instruction/update inst scopes) → (mv new-scopes undo)
Arguments: inst — Guard (vl-elabinstruction-p inst).; 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-do-instruction/update

(defun vl-elabscopes-do-instruction/update (inst scopes)
  (declare (xargs :guard (and (vl-elabinstruction-p inst)
                              (vl-elabscopes-p scopes))))
  (let ((__function__ 'vl-elabscopes-do-instruction/update))
    (declare (ignorable __function__))
    (vl-elabinstruction-case
         inst
         :pop (vl-elabscopes-pop/update inst.levels scopes)
         :root (vl-elabscopes-root/update scopes)
         :push-anon (mv (vl-elabscopes-push-anon inst.scope scopes)
                        (list (vl-elabinstruction-pop 1)))
         :push-named (mv (vl-elabscopes-push-named inst.key scopes)
                         (list (vl-elabinstruction-pop 1))))))

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

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

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

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

Theorem: vl-elabscopes-do-instruction/update-of-vl-elabinstruction-fix-inst

(defthm
 vl-elabscopes-do-instruction/update-of-vl-elabinstruction-fix-inst
 (equal
  (vl-elabscopes-do-instruction/update (vl-elabinstruction-fix inst)
                                       scopes)
  (vl-elabscopes-do-instruction/update inst scopes)))

Theorem: vl-elabscopes-do-instruction/update-vl-elabinstruction-equiv-congruence-on-inst

(defthm
 vl-elabscopes-do-instruction/update-vl-elabinstruction-equiv-congruence-on-inst
 (implies
    (vl-elabinstruction-equiv inst inst-equiv)
    (equal (vl-elabscopes-do-instruction/update inst scopes)
           (vl-elabscopes-do-instruction/update inst-equiv scopes)))
 :rule-classes :congruence)

Theorem: vl-elabscopes-do-instruction/update-of-vl-elabscopes-fix-scopes

(defthm
    vl-elabscopes-do-instruction/update-of-vl-elabscopes-fix-scopes
  (equal (vl-elabscopes-do-instruction/update
              inst (vl-elabscopes-fix scopes))
         (vl-elabscopes-do-instruction/update inst scopes)))

Theorem: vl-elabscopes-do-instruction/update-vl-elabscopes-equiv-congruence-on-scopes

(defthm
 vl-elabscopes-do-instruction/update-vl-elabscopes-equiv-congruence-on-scopes
 (implies
    (vl-elabscopes-equiv scopes scopes-equiv)
    (equal (vl-elabscopes-do-instruction/update inst scopes)
           (vl-elabscopes-do-instruction/update inst scopes-equiv)))
 :rule-classes :congruence)