		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabindex-push

Signature
(vl-elabindex-push scope &key (elabindex 'elabindex)) → new-elabindex
Arguments: scope — Guard (vl-scope-p scope).

Definitions and Theorems

Function: vl-elabindex-push-fn

(defun vl-elabindex-push-fn (scope elabindex)
 (declare (xargs :stobjs (elabindex)))
 (declare (xargs :guard (vl-scope-p scope)))
 (let ((__function__ 'vl-elabindex-push))
  (declare (ignorable __function__))
  (b* ((key (vl-scope->elabkey scope))
       (scopes (vl-elabindex->scopes elabindex))
       (scopes (if key (vl-elabscopes-push-named key scopes)
                 (vl-elabscopes-push-anon (make-vl-elabscope)
                                          scopes)))
       (ss (vl-elabindex->ss elabindex))
       (elabindex (vl-elabindex-update-scopes scopes elabindex))
       (elabindex (vl-elabindex-update-undostack
                       (cons (cons (list (vl-elabinstruction-pop 1))
                                   ss)
                             (vl-elabindex->undostack elabindex))
                       elabindex)))
    (vl-elabindex-update-ss (vl-scopestack-push scope ss)
                            elabindex))))

Function: vl-elabindex-push-undo-entry-fn

(defun vl-elabindex-push-undo-entry-fn (elabindex)
  (declare (xargs :stobjs (elabindex)))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-elabindex-push-undo-entry))
    (declare (ignorable __function__))
    (cons (list (vl-elabinstruction-pop 1))
          (vl-elabindex->ss))))

Theorem: return-type-of-vl-elabindex-push-undo-entry

(defthm return-type-of-vl-elabindex-push-undo-entry
  (b* ((undo-entry (vl-elabindex-push-undo-entry-fn elabindex)))
    (and (vl-elabtraversal-p (car undo-entry))
         (vl-scopestack-p (cdr undo-entry))))
  :rule-classes :rewrite)

Theorem: undostack-of-vl-elabindex-push

(defthm undostack-of-vl-elabindex-push
  (equal (vl-elabindex->undostack (vl-elabindex-push scope))
         (cons (vl-elabindex-push-undo-entry)
               (vl-elabindex->undostack))))

Theorem: vl-elabindex-push-fn-of-vl-scope-fix-scope

(defthm vl-elabindex-push-fn-of-vl-scope-fix-scope
  (equal (vl-elabindex-push-fn (vl-scope-fix scope)
                               elabindex)
         (vl-elabindex-push-fn scope elabindex)))

Theorem: vl-elabindex-push-fn-vl-scope-equiv-congruence-on-scope

(defthm vl-elabindex-push-fn-vl-scope-equiv-congruence-on-scope
  (implies (vl-scope-equiv scope scope-equiv)
           (equal (vl-elabindex-push-fn scope elabindex)
                  (vl-elabindex-push-fn scope-equiv elabindex)))
  :rule-classes :congruence)