		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabscopes-pop/update-one

Pop a scope off the stack, updating its entry in the outer scope.

Signature
(vl-elabscopes-pop/update-one scopes) → (mv new-scopes revpath)
Arguments: scopes — Guard (vl-elabscopes-p scopes).
Returns: new-scopes — Type (vl-elabscopes-p new-scopes).; revpath — Type (vl-elabtraversal-p revpath).

Definitions and Theorems

Function: vl-elabscopes-pop/update-one

(defun vl-elabscopes-pop/update-one (scopes)
 (declare (xargs :guard (vl-elabscopes-p scopes)))
 (let ((__function__ 'vl-elabscopes-pop/update-one))
   (declare (ignorable __function__))
   (b*
     ((scopes (vl-elabscopes-fix scopes))
      ((when (< (len scopes) 2))
       (raise "Not enough scopes remaining to pop!~%")
       (mv scopes nil))
      ((list* (cons scope1key scope1)
              (cons scope2key scope2)
              rest)
       scopes)
      ((unless scope1key)
       (mv (cdr scopes)
           (list (vl-elabinstruction-push-anon scope1))))
      (scope2
           (vl-elabscope-update-subscope? scope1key scope1 scope2)))
     (mv (cons (cons scope2key scope2) rest)
         (list (vl-elabinstruction-push-named scope1key))))))

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

(defthm vl-elabscopes-p-of-vl-elabscopes-pop/update-one.new-scopes
  (b* (((mv ?new-scopes ?revpath)
        (vl-elabscopes-pop/update-one scopes)))
    (vl-elabscopes-p new-scopes))
  :rule-classes :rewrite)

Theorem: vl-elabtraversal-p-of-vl-elabscopes-pop/update-one.revpath

(defthm vl-elabtraversal-p-of-vl-elabscopes-pop/update-one.revpath
  (b* (((mv ?new-scopes ?revpath)
        (vl-elabscopes-pop/update-one scopes)))
    (vl-elabtraversal-p revpath))
  :rule-classes :rewrite)

Theorem: count-of-vl-elabscopes-pop/update-one-weak

(defthm count-of-vl-elabscopes-pop/update-one-weak
 (b* (((mv ?new-scopes ?revpath)
       (vl-elabscopes-pop/update-one scopes)))
   (<= (len new-scopes)
       (len (vl-elabscopes-fix scopes))))
 :rule-classes
 ((:linear :trigger-terms
           ((len (mv-nth 0
                         (vl-elabscopes-pop/update-one scopes)))))))

Theorem: count-of-vl-elabscopes-pop/update-one-strong

(defthm count-of-vl-elabscopes-pop/update-one-strong
 (b* (((mv ?new-scopes ?revpath)
       (vl-elabscopes-pop/update-one scopes)))
   (implies (and (consp (vl-elabscopes-fix scopes))
                 (consp (cdr (vl-elabscopes-fix scopes))))
            (< (len new-scopes)
               (len (vl-elabscopes-fix scopes)))))
 :rule-classes
 ((:linear :trigger-terms
           ((len (mv-nth 0
                         (vl-elabscopes-pop/update-one scopes)))))))

Theorem: vl-elabscopes-pop/update-one-of-vl-elabscopes-fix-scopes

(defthm vl-elabscopes-pop/update-one-of-vl-elabscopes-fix-scopes
  (equal (vl-elabscopes-pop/update-one (vl-elabscopes-fix scopes))
         (vl-elabscopes-pop/update-one scopes)))

Theorem: vl-elabscopes-pop/update-one-vl-elabscopes-equiv-congruence-on-scopes

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