		Search-engine friendly clone of the ACL2 documentation.

Scopestack

Vl-scopestack->hashkey

Produce a honsed, hopefully-unique hash key for this scope.

Signature
(vl-scopestack->hashkey x) → key
Arguments: x — Guard (vl-scopestack-p x).

Uses the names of the scopes, so: if any scope is not named, it causes a hard error; and if the name of each scope isn't unique within its parent scope, then the hash key won't be unique.

Running addnames before using this should ensure that scopes are named, and the names generated should be unique.

Definitions and Theorems

Function: vl-scopestack->hashkey

(defun vl-scopestack->hashkey (x)
  (declare (xargs :guard (vl-scopestack-p x)))
  (let ((__function__ 'vl-scopestack->hashkey))
    (declare (ignorable __function__))
    (vl-scopestack-case
         x :null nil :global (hons :root nil)
         :local
         (b* ((super (vl-scopestack->hashkey x.super)))
           (hons (or (vl-scope->id x.top)
                     (raise "Unnamed scope under ~x0: ~x1~%"
                            (rev super)
                            x.top))
                 super)))))

Theorem: vl-scopestack->hashkey-of-vl-scopestack-fix-x

(defthm vl-scopestack->hashkey-of-vl-scopestack-fix-x
  (equal (vl-scopestack->hashkey (vl-scopestack-fix x))
         (vl-scopestack->hashkey x)))

Theorem: vl-scopestack->hashkey-vl-scopestack-equiv-congruence-on-x

(defthm vl-scopestack->hashkey-vl-scopestack-equiv-congruence-on-x
  (implies (vl-scopestack-equiv x x-equiv)
           (equal (vl-scopestack->hashkey x)
                  (vl-scopestack->hashkey x-equiv)))
  :rule-classes :congruence)