		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabscopes-do-instruction

Signature
(vl-elabscopes-do-instruction inst scopes &key (allow-empty 'nil)) → new-scopes
Arguments: inst — Guard (vl-elabinstruction-p inst).; scopes — Guard (vl-elabscopes-p scopes).
Returns: new-scopes — Type (vl-elabscopes-p new-scopes).

Definitions and Theorems

Function: vl-elabscopes-do-instruction-fn

(defun vl-elabscopes-do-instruction-fn (inst scopes allow-empty)
 (declare (xargs :guard (and (vl-elabinstruction-p inst)
                             (vl-elabscopes-p scopes))))
 (let ((__function__ 'vl-elabscopes-do-instruction))
  (declare (ignorable __function__))
  (vl-elabinstruction-case
       inst
       :pop (vl-elabscopes-pop inst.levels scopes
                               :allow-empty allow-empty)
       :root (vl-elabscopes-root scopes
                                 :allow-empty allow-empty)
       :push-anon (vl-elabscopes-push-anon inst.scope scopes
                                           :allow-empty allow-empty)
       :push-named
       (vl-elabscopes-push-named inst.key scopes
                                 :allow-empty allow-empty))))

Theorem: vl-elabscopes-p-of-vl-elabscopes-do-instruction

(defthm vl-elabscopes-p-of-vl-elabscopes-do-instruction
  (b*
   ((new-scopes
         (vl-elabscopes-do-instruction-fn inst scopes allow-empty)))
   (vl-elabscopes-p new-scopes))
  :rule-classes :rewrite)

Theorem: vl-elabscopes-do-instruction-fn-of-vl-elabinstruction-fix-inst

(defthm
     vl-elabscopes-do-instruction-fn-of-vl-elabinstruction-fix-inst
 (equal
      (vl-elabscopes-do-instruction-fn (vl-elabinstruction-fix inst)
                                       scopes allow-empty)
      (vl-elabscopes-do-instruction-fn inst scopes allow-empty)))

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

(defthm
 vl-elabscopes-do-instruction-fn-vl-elabinstruction-equiv-congruence-on-inst
 (implies
  (vl-elabinstruction-equiv inst inst-equiv)
  (equal
   (vl-elabscopes-do-instruction-fn inst scopes allow-empty)
   (vl-elabscopes-do-instruction-fn inst-equiv scopes allow-empty)))
 :rule-classes :congruence)

Theorem: vl-elabscopes-do-instruction-fn-of-vl-elabscopes-fix-scopes

(defthm vl-elabscopes-do-instruction-fn-of-vl-elabscopes-fix-scopes
 (equal
    (vl-elabscopes-do-instruction-fn inst (vl-elabscopes-fix scopes)
                                     allow-empty)
    (vl-elabscopes-do-instruction-fn inst scopes allow-empty)))

Theorem: vl-elabscopes-do-instruction-fn-vl-elabscopes-equiv-congruence-on-scopes

(defthm
 vl-elabscopes-do-instruction-fn-vl-elabscopes-equiv-congruence-on-scopes
 (implies
  (vl-elabscopes-equiv scopes scopes-equiv)
  (equal
   (vl-elabscopes-do-instruction-fn inst scopes allow-empty)
   (vl-elabscopes-do-instruction-fn inst scopes-equiv allow-empty)))
 :rule-classes :congruence)