Safely add a dependency onto an item (i.e., a parameter, variable, function name, type name, etc.)
(vl-immdeps-add-item name ans &key (ss 'ss) (ctx 'ctx)) → new-ans
Some cases:
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)