Looks up a HID in a scopestack and looks for a declaration, returning the type and dimensionlist if found.
(vl-hidexpr-find-type x ss ctx) → (mv warning type)
Function:
(defun vl-hidexpr-find-type (x ss ctx) (declare (xargs :guard (and (vl-expr-p x) (vl-scopestack-p ss) (acl2::any-p ctx)))) (declare (xargs :guard (vl-hidexpr-p x))) (let ((__function__ 'vl-hidexpr-find-type)) (declare (ignorable __function__)) (b* ((x (vl-expr-fix x)) ((mv err trace tail) (vl-follow-hidexpr x ss ctx)) ((when err) (mv err nil)) ((vl-hidstep step1) (car trace)) ((when (eq (tag step1.item) :vl-vardecl)) (b* (((vl-vardecl step1.item)) ((mv warning res-type) (vl-datatype-usertype-elim step1.item.type step1.ss 1000)) ((when warning) (mv warning nil))) (vl-hidexpr-traverse-datatype tail res-type)))) (mv (make-vl-warning :type (if (vl-idexpr-p x) :vl-identifier-type-fail :vl-hidexpr-type-fail) :msg "~a0: Failed to find a type for ~s1 because we ~ didn't find a vardecl but rather a ~x2" :args (list ctx x (tag step1.item)) :fn __function__) nil))))
Theorem:
(defthm return-type-of-vl-hidexpr-find-type.warning (b* (((mv common-lisp::?warning common-lisp::?type) (vl-hidexpr-find-type x ss ctx))) (iff (vl-warning-p warning) warning)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-hidexpr-find-type.type (b* (((mv common-lisp::?warning common-lisp::?type) (vl-hidexpr-find-type x ss ctx))) (iff (vl-datatype-p type) (not warning))) :rule-classes :rewrite)
Theorem:
(defthm context-irrelevance-of-vl-hidexpr-find-type (implies (syntaxp (not (equal ctx ''nil))) (b* (((mv err1 type1) (vl-hidexpr-find-type x ss ctx)) ((mv err2 type2) (vl-hidexpr-find-type x ss nil))) (and (iff err1 err2) (equal type1 type2)))))
Theorem:
(defthm vl-hidexpr-find-type-of-vl-expr-fix-x (equal (vl-hidexpr-find-type (vl-expr-fix x) ss ctx) (vl-hidexpr-find-type x ss ctx)))
Theorem:
(defthm vl-hidexpr-find-type-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-hidexpr-find-type x ss ctx) (vl-hidexpr-find-type x-equiv ss ctx))) :rule-classes :congruence)
Theorem:
(defthm vl-hidexpr-find-type-of-vl-scopestack-fix-ss (equal (vl-hidexpr-find-type x (vl-scopestack-fix ss) ctx) (vl-hidexpr-find-type x ss ctx)))
Theorem:
(defthm vl-hidexpr-find-type-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-hidexpr-find-type x ss ctx) (vl-hidexpr-find-type x ss-equiv ctx))) :rule-classes :congruence)
Theorem:
(defthm vl-hidexpr-find-type-of-identity-ctx (equal (vl-hidexpr-find-type x ss (identity ctx)) (vl-hidexpr-find-type x ss ctx)))
Theorem:
(defthm vl-hidexpr-find-type-equal-congruence-on-ctx (implies (equal ctx ctx-equiv) (equal (vl-hidexpr-find-type x ss ctx) (vl-hidexpr-find-type x ss ctx-equiv))) :rule-classes :congruence)