		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabindex-traverse

Signature
(vl-elabindex-traverse ss path &key (elabindex 'elabindex)) → new-elabindex
Arguments: ss — Guard (vl-scopestack-p ss).; path — Guard (vl-elabtraversal-p path).

Definitions and Theorems

Function: vl-elabindex-traverse-fn

(defun vl-elabindex-traverse-fn (ss path elabindex)
  (declare (xargs :stobjs (elabindex)))
  (declare (xargs :guard (and (vl-scopestack-p ss)
                              (vl-elabtraversal-p path))))
  (let ((__function__ 'vl-elabindex-traverse))
    (declare (ignorable __function__))
    (b* (((mv scopes rev-undo)
          (vl-elabscopes-traverse/update
               path (vl-elabindex->scopes elabindex)))
         (elabindex (vl-elabindex-update-scopes scopes elabindex))
         (elabindex (vl-elabindex-update-undostack
                         (cons (cons (rev rev-undo)
                                     (vl-elabindex->ss elabindex))
                               (vl-elabindex->undostack elabindex))
                         elabindex)))
      (vl-elabindex-update-ss (vl-scopestack-fix ss)
                              elabindex))))

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

(defun vl-elabindex-traverse-undo-entry-fn (path elabindex)
  (declare (xargs :stobjs (elabindex)))
  (declare (xargs :guard (vl-elabtraversal-p path)))
  (let ((__function__ 'vl-elabindex-traverse-undo-entry))
    (declare (ignorable __function__))
    (b* (((mv ?scopes rev-undo)
          (vl-elabscopes-traverse/update
               path (vl-elabindex->scopes elabindex))))
      (cons (rev rev-undo)
            (vl-elabindex->ss)))))

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

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

Theorem: undostack-of-vl-elabindex-traverse

(defthm undostack-of-vl-elabindex-traverse
  (equal (vl-elabindex->undostack (vl-elabindex-traverse ss path))
         (cons (vl-elabindex-traverse-undo-entry path)
               (vl-elabindex->undostack))))

Theorem: vl-elabindex-traverse-undo-entry-fn-of-vl-elabtraversal-fix-path

(defthm
   vl-elabindex-traverse-undo-entry-fn-of-vl-elabtraversal-fix-path
 (equal
    (vl-elabindex-traverse-undo-entry-fn (vl-elabtraversal-fix path)
                                         elabindex)
    (vl-elabindex-traverse-undo-entry-fn path elabindex)))

Theorem: vl-elabindex-traverse-undo-entry-fn-vl-elabtraversal-equiv-congruence-on-path

(defthm
 vl-elabindex-traverse-undo-entry-fn-vl-elabtraversal-equiv-congruence-on-path
 (implies
   (vl-elabtraversal-equiv path path-equiv)
   (equal
        (vl-elabindex-traverse-undo-entry-fn path elabindex)
        (vl-elabindex-traverse-undo-entry-fn path-equiv elabindex)))
 :rule-classes :congruence)

Theorem: vl-elabindex-traverse-fn-of-vl-scopestack-fix-ss

(defthm vl-elabindex-traverse-fn-of-vl-scopestack-fix-ss
  (equal (vl-elabindex-traverse-fn (vl-scopestack-fix ss)
                                   path elabindex)
         (vl-elabindex-traverse-fn ss path elabindex)))

Theorem: vl-elabindex-traverse-fn-vl-scopestack-equiv-congruence-on-ss

(defthm
      vl-elabindex-traverse-fn-vl-scopestack-equiv-congruence-on-ss
  (implies
       (vl-scopestack-equiv ss ss-equiv)
       (equal (vl-elabindex-traverse-fn ss path elabindex)
              (vl-elabindex-traverse-fn ss-equiv path elabindex)))
  :rule-classes :congruence)

Theorem: vl-elabindex-traverse-fn-of-vl-elabtraversal-fix-path

(defthm vl-elabindex-traverse-fn-of-vl-elabtraversal-fix-path
  (equal (vl-elabindex-traverse-fn ss (vl-elabtraversal-fix path)
                                   elabindex)
         (vl-elabindex-traverse-fn ss path elabindex)))

Theorem: vl-elabindex-traverse-fn-vl-elabtraversal-equiv-congruence-on-path

(defthm
 vl-elabindex-traverse-fn-vl-elabtraversal-equiv-congruence-on-path
 (implies
      (vl-elabtraversal-equiv path path-equiv)
      (equal (vl-elabindex-traverse-fn ss path elabindex)
             (vl-elabindex-traverse-fn ss path-equiv elabindex)))
 :rule-classes :congruence)