		Search-engine friendly clone of the ACL2 documentation.

Vl-immdeps

Vl-immdeps-add-item

Safely add a dependency onto an item (i.e., a parameter, variable, function name, type name, etc.)

Signature
(vl-immdeps-add-item name ans &key (ss 'ss) (ctx 'ctx)) → new-ans
Arguments: name — Name being referenced.
Guard (stringp name).; ans — Answer we are building.
Guard (vl-immdeps-p ans).; ss — Our current scope.
Guard (vl-scopestack-p ss).; ctx — Context for warnings.
Guard (any-p ctx).
Returns: new-ans — Type (vl-immdeps-p new-ans).

Some cases:

If name refers to a top-level item, we add a dependency onto it.
If it refers to an item from some other package, we instead add a dependency onto that package.
If it refers to a local item, we don't add any dependency onto it.
If it isn't declared, we add a warning instead of a dependency.

Definitions and Theorems

Function: vl-immdeps-add-item-fn

(defun vl-immdeps-add-item-fn (name ans ss ctx)
 (declare (xargs :guard (and (stringp name)
                             (vl-immdeps-p ans)
                             (vl-scopestack-p ss)
                             (any-p ctx))))
 (let ((__function__ 'vl-immdeps-add-item))
   (declare (ignorable __function__))
   (b*
    ((name (string-fix name))
     (ans (vl-immdeps-fix ans))
     ((mv item item-ss pkg)
      (vl-scopestack-find-item/context name ss))
     ((unless item)
      (vl-immdeps-add-error ans
                            :type :vl-undeclared-identifier
                            :msg "~a0: missing declaration for ~a1."
                            :args (list ctx name)
                            :fatalp t))
     ((when pkg)
      (vl-immdeps-add-pkgdep pkg ans))
     ((when (vl-scopestack-toplevel-p item-ss))
      (vl-immdeps-add-raw-dependency name ans)))
    ans)))

Theorem: vl-immdeps-p-of-vl-immdeps-add-item

(defthm vl-immdeps-p-of-vl-immdeps-add-item
  (b* ((new-ans (vl-immdeps-add-item-fn name ans ss ctx)))
    (vl-immdeps-p new-ans))
  :rule-classes :rewrite)

Theorem: vl-immdeps-add-item-fn-of-str-fix-name

(defthm vl-immdeps-add-item-fn-of-str-fix-name
  (equal (vl-immdeps-add-item-fn (str-fix name)
                                 ans ss ctx)
         (vl-immdeps-add-item-fn name ans ss ctx)))

Theorem: vl-immdeps-add-item-fn-streqv-congruence-on-name

(defthm vl-immdeps-add-item-fn-streqv-congruence-on-name
  (implies (streqv name name-equiv)
           (equal (vl-immdeps-add-item-fn name ans ss ctx)
                  (vl-immdeps-add-item-fn name-equiv ans ss ctx)))
  :rule-classes :congruence)

Theorem: vl-immdeps-add-item-fn-of-vl-immdeps-fix-ans

(defthm vl-immdeps-add-item-fn-of-vl-immdeps-fix-ans
  (equal (vl-immdeps-add-item-fn name (vl-immdeps-fix ans)
                                 ss ctx)
         (vl-immdeps-add-item-fn name ans ss ctx)))

Theorem: vl-immdeps-add-item-fn-vl-immdeps-equiv-congruence-on-ans

(defthm vl-immdeps-add-item-fn-vl-immdeps-equiv-congruence-on-ans
  (implies (vl-immdeps-equiv ans ans-equiv)
           (equal (vl-immdeps-add-item-fn name ans ss ctx)
                  (vl-immdeps-add-item-fn name ans-equiv ss ctx)))
  :rule-classes :congruence)

Theorem: vl-immdeps-add-item-fn-of-vl-scopestack-fix-ss

(defthm vl-immdeps-add-item-fn-of-vl-scopestack-fix-ss
  (equal (vl-immdeps-add-item-fn name ans (vl-scopestack-fix ss)
                                 ctx)
         (vl-immdeps-add-item-fn name ans ss ctx)))

Theorem: vl-immdeps-add-item-fn-vl-scopestack-equiv-congruence-on-ss

(defthm vl-immdeps-add-item-fn-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-immdeps-add-item-fn name ans ss ctx)
                  (vl-immdeps-add-item-fn name ans ss-equiv ctx)))
  :rule-classes :congruence)

Theorem: vl-immdeps-add-item-fn-of-identity-ctx

(defthm vl-immdeps-add-item-fn-of-identity-ctx
  (equal (vl-immdeps-add-item-fn name ans ss (identity ctx))
         (vl-immdeps-add-item-fn name ans ss ctx)))

Theorem: vl-immdeps-add-item-fn-equal-congruence-on-ctx

(defthm vl-immdeps-add-item-fn-equal-congruence-on-ctx
  (implies (equal ctx ctx-equiv)
           (equal (vl-immdeps-add-item-fn name ans ss ctx)
                  (vl-immdeps-add-item-fn name ans ss ctx-equiv)))
  :rule-classes :congruence)