Produce a honsed, hopefully-unique hash key for this scope.
(vl-scopestack->hashkey x) → key
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.
(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)))))
(defthm vl-scopestack->hashkey-of-vl-scopestack-fix-x (equal (vl-scopestack->hashkey (vl-scopestack-fix x)) (vl-scopestack->hashkey 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)