		Search-engine friendly clone of the ACL2 documentation.

Scopestack

Vl-scopestack->path-aux

Signature
(vl-scopestack->path-aux x rchars) → rchars
Arguments: x — Guard (vl-scopestack-p x).
Returns: rchars — Type (character-listp rchars), given (character-listp rchars).

Definitions and Theorems

Function: vl-scopestack->path-aux

(defun vl-scopestack->path-aux (x rchars)
  (declare (xargs :guard (vl-scopestack-p x)))
  (let ((__function__ 'vl-scopestack->path-aux))
    (declare (ignorable __function__))
    (vl-scopestack-case
         x :null
         (str::revappend-chars ":null" rchars)
         :global
         (str::revappend-chars "$root" rchars)
         :local
         (b* ((rchars (vl-scopestack->path-aux x.super rchars))
              (rchars (cons #\. rchars))
              (name1 (or (vl-scope->name x.top)
                         "<unnamed " (symbol-name (tag x.top))
                         ">"))
              (rchars (str::revappend-chars name1 rchars)))
           rchars))))

Theorem: character-listp-of-vl-scopestack->path-aux

(defthm character-listp-of-vl-scopestack->path-aux
  (implies (character-listp rchars)
           (b* ((rchars (vl-scopestack->path-aux x rchars)))
             (character-listp rchars)))
  :rule-classes :rewrite)

Theorem: vl-scopestack->path-aux-of-vl-scopestack-fix-x

(defthm vl-scopestack->path-aux-of-vl-scopestack-fix-x
  (equal (vl-scopestack->path-aux (vl-scopestack-fix x)
                                  rchars)
         (vl-scopestack->path-aux x rchars)))

Theorem: vl-scopestack->path-aux-vl-scopestack-equiv-congruence-on-x

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