		Search-engine friendly clone of the ACL2 documentation.

Hid-tools

Vl-follow-scopeexpr

Follow a scope expression to find the associated declaration.

Signature
(vl-follow-scopeexpr x ss &key strictp) → (mv err trace context tail)
Arguments: x — Scope expression to follow.
Guard (vl-scopeexpr-p x).; ss — Scopestack where the lookup originates.
Guard (vl-scopestack-p ss).; strictp — Require all array indices and bounds to be resolved?.
Guard (booleanp strictp).
Returns: err — A message for any error.
Type (iff (vl-msg-p err) err).; trace — On success: a non-empty trace that records all the items we went through to resolve this HID. The car of the trace is the final declaration for this HID.
Type (vl-hidtrace-p trace).; context — On success, a scopecontext showing where the hid is found.
Type (implies (not err) (vl-scopecontext-p context)).; tail — On success: the remainder of x after arriving at the declaration. This may include array indexing or structure indexing.
Type (vl-hidexpr-p tail).

Definitions and Theorems

Function: vl-follow-scopeexpr-fn

(defun vl-follow-scopeexpr-fn (x ss strictp)
 (declare (xargs :guard (and (vl-scopeexpr-p x)
                             (vl-scopestack-p ss)
                             (booleanp strictp))))
 (let ((__function__ 'vl-follow-scopeexpr))
  (declare (ignorable __function__))
  (vl-scopeexpr-case
   x :end
   (vl-follow-hidexpr x.hid ss
                      :strictp strictp
                      :origx x
                      :elabpath nil)
   :colon
   (b*
    ((x (vl-scopeexpr-fix x))
     ((unless (stringp x.first))
      (mv
         (vmsg "~a0: The scope modifier '~x1' is not yet supported."
               x
               (case x.first (:vl-local "local")
                     (:vl-$unit "$unit")
                     (otherwise "??UNKNOWN??")))
         nil nil (vl-scopeexpr->hid x)))
     ((mv package pkg-ss elabkey classp)
      (b* (((mv class class-ss)
            (vl-scopestack-find-class/ss x.first ss))
           ((when class)
            (mv class
                class-ss (vl-elabkey-class x.first)
                t))
           ((mv package pkg-ss)
            (vl-scopestack-find-package/ss x.first ss)))
        (mv package
            pkg-ss (vl-elabkey-package x.first)
            nil)))
     ((unless package)
      (mv (vmsg "~a0: Package/class ~s1 not found.."
                x x.first)
          nil nil (vl-scopeexpr->hid x)))
     (pkg-ss (vl-scopestack-push package pkg-ss))
     ((unless (vl-scopeexpr-case x.rest :end))
      (mv
       (vmsg
        "~a0: Multiple levels of :: operators are ~
                                     not yet supported."
        x)
       nil nil (vl-scopeexpr->hid x)))
     (elabpath (list (vl-elabinstruction-push-named elabkey)
                     (vl-elabinstruction-root)))
     ((mv err trace context tail)
      (vl-follow-hidexpr (vl-scopeexpr-end->hid x.rest)
                         pkg-ss
                         :strictp strictp
                         :origx x
                         :elabpath elabpath))
     ((when err) (mv err trace context tail))
     ((unless (vl-scopecontext-case context :local))
      (mv nil trace context tail)))
    (mv nil trace
        (if classp (make-vl-scopecontext-class :class package)
          (make-vl-scopecontext-package :pkg package))
        tail)))))

Theorem: return-type-of-vl-follow-scopeexpr.err

(defthm return-type-of-vl-follow-scopeexpr.err
  (b* (((mv ?err
            common-lisp::?trace ?context set::?tail)
        (vl-follow-scopeexpr-fn x ss strictp)))
    (iff (vl-msg-p err) err))
  :rule-classes :rewrite)

Theorem: vl-hidtrace-p-of-vl-follow-scopeexpr.trace

(defthm vl-hidtrace-p-of-vl-follow-scopeexpr.trace
  (b* (((mv ?err
            common-lisp::?trace ?context set::?tail)
        (vl-follow-scopeexpr-fn x ss strictp)))
    (vl-hidtrace-p trace))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-follow-scopeexpr.context

(defthm return-type-of-vl-follow-scopeexpr.context
  (b* (((mv ?err
            common-lisp::?trace ?context set::?tail)
        (vl-follow-scopeexpr-fn x ss strictp)))
    (implies (not err)
             (vl-scopecontext-p context)))
  :rule-classes :rewrite)

Theorem: vl-hidexpr-p-of-vl-follow-scopeexpr.tail

(defthm vl-hidexpr-p-of-vl-follow-scopeexpr.tail
  (b* (((mv ?err
            common-lisp::?trace ?context set::?tail)
        (vl-follow-scopeexpr-fn x ss strictp)))
    (vl-hidexpr-p tail))
  :rule-classes :rewrite)

Theorem: consp-of-vl-follow-scopeexpr.trace

(defthm consp-of-vl-follow-scopeexpr.trace
  (b* (((mv ?err
            common-lisp::?trace ?context set::?tail)
        (vl-follow-scopeexpr-fn x ss strictp)))
    (implies (not err) (consp trace))))

Theorem: count-of-vl-follow-scopeexpr.tail

(defthm count-of-vl-follow-scopeexpr.tail
  (b* (((mv ?err
            common-lisp::?trace ?context set::?tail)
        (vl-follow-scopeexpr-fn x ss strictp)))
    (< (vl-hidexpr-count tail)
       (vl-scopeexpr-count x)))
  :rule-classes :linear)

Theorem: vl-subhid-p-of-vl-follow-scopeexpr

(defthm vl-subhid-p-of-vl-follow-scopeexpr
  (b* (((mv ?err
            common-lisp::?trace ?context set::?tail)
        (vl-follow-scopeexpr-fn x ss strictp)))
    (implies (not err)
             (vl-subhid-p tail (vl-scopeexpr->hid x)))))

Theorem: vl-follow-scopeexpr-fn-of-vl-scopeexpr-fix-x

(defthm vl-follow-scopeexpr-fn-of-vl-scopeexpr-fix-x
  (equal (vl-follow-scopeexpr-fn (vl-scopeexpr-fix x)
                                 ss strictp)
         (vl-follow-scopeexpr-fn x ss strictp)))

Theorem: vl-follow-scopeexpr-fn-vl-scopeexpr-equiv-congruence-on-x

(defthm vl-follow-scopeexpr-fn-vl-scopeexpr-equiv-congruence-on-x
  (implies (vl-scopeexpr-equiv x x-equiv)
           (equal (vl-follow-scopeexpr-fn x ss strictp)
                  (vl-follow-scopeexpr-fn x-equiv ss strictp)))
  :rule-classes :congruence)

Theorem: vl-follow-scopeexpr-fn-of-vl-scopestack-fix-ss

(defthm vl-follow-scopeexpr-fn-of-vl-scopestack-fix-ss
  (equal (vl-follow-scopeexpr-fn x (vl-scopestack-fix ss)
                                 strictp)
         (vl-follow-scopeexpr-fn x ss strictp)))

Theorem: vl-follow-scopeexpr-fn-vl-scopestack-equiv-congruence-on-ss

(defthm vl-follow-scopeexpr-fn-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-follow-scopeexpr-fn x ss strictp)
                  (vl-follow-scopeexpr-fn x ss-equiv strictp)))
  :rule-classes :congruence)

Theorem: vl-follow-scopeexpr-fn-of-bool-fix-strictp

(defthm vl-follow-scopeexpr-fn-of-bool-fix-strictp
  (equal (vl-follow-scopeexpr-fn x ss (acl2::bool-fix strictp))
         (vl-follow-scopeexpr-fn x ss strictp)))

Theorem: vl-follow-scopeexpr-fn-iff-congruence-on-strictp

(defthm vl-follow-scopeexpr-fn-iff-congruence-on-strictp
  (implies (iff strictp strictp-equiv)
           (equal (vl-follow-scopeexpr-fn x ss strictp)
                  (vl-follow-scopeexpr-fn x ss strictp-equiv)))
  :rule-classes :congruence)