(vl-funcall-typedecide x ss scopes) → (mv warnings class)
Function:
(defun vl-funcall-typedecide (x ss scopes) (declare (xargs :guard (and (vl-expr-p x) (vl-scopestack-p ss) (vl-elabscopes-p scopes)))) (declare (xargs :guard (vl-expr-case x :vl-call (not x.systemp) :otherwise nil))) (let ((__function__ 'vl-funcall-typedecide)) (declare (ignorable __function__)) (b* (((vl-call x) (vl-expr-fix x)) (warnings nil) ((mv err trace ?context ?tail) (vl-follow-scopeexpr x.name ss)) ((when err) (mv (fatal :type :vl-typedecide-fail :msg "Failed to find function ~a0: ~@1" :args (list (vl-scopeexpr->expr x.name) err)) :vl-error-class)) ((vl-hidstep lookup) (car trace)) ((unless (eq (tag lookup.item) :vl-fundecl)) (mv (fatal :type :vl-typedecide-fail :msg "In function call ~a0, function name does not ~ refer to a fundecl but instead ~a1" :args (list x lookup.item)) :vl-error-class)) ((vl-fundecl lookup.item)) (fnscopes (vl-elabscopes-traverse (rev lookup.elabpath) scopes)) (info (vl-elabscopes-item-info lookup.item.name fnscopes)) (item (or info lookup.item)) ((unless (eq (tag item) :vl-fundecl)) (mv (fatal :type :vl-selfsize-fail :msg "In function call ~a0, function name does not ~ refer to a fundecl but instead ~a1" :args (list x item)) :vl-error-class)) ((vl-fundecl item)) ((mv err rettype) (vl-datatype-usertype-resolve item.rettype lookup.ss)) ((when err) (mv (fatal :type :vl-typedecide-fail :msg "In function call ~a0, the function's return ~ type ~a1 had unresolvable usertypes: ~@2" :args (list x item.rettype err)) :vl-error-class)) ((unless (vl-datatype-packedp rettype)) (mv (ok) :vl-other-class)) ((mv caveat class) (vl-datatype-arithclass rettype)) (warnings (vl-signedness-ambiguity-warning x class caveat))) (mv (ok) class))))
Theorem:
(defthm vl-warninglist-p-of-vl-funcall-typedecide.warnings (b* (((mv ?warnings common-lisp::?class) (vl-funcall-typedecide x ss scopes))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-arithclass-p-of-vl-funcall-typedecide.class (b* (((mv ?warnings common-lisp::?class) (vl-funcall-typedecide x ss scopes))) (vl-arithclass-p class)) :rule-classes :rewrite)
Theorem:
(defthm vl-funcall-typedecide-of-vl-expr-fix-x (equal (vl-funcall-typedecide (vl-expr-fix x) ss scopes) (vl-funcall-typedecide x ss scopes)))
Theorem:
(defthm vl-funcall-typedecide-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-funcall-typedecide x ss scopes) (vl-funcall-typedecide x-equiv ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-funcall-typedecide-of-vl-scopestack-fix-ss (equal (vl-funcall-typedecide x (vl-scopestack-fix ss) scopes) (vl-funcall-typedecide x ss scopes)))
Theorem:
(defthm vl-funcall-typedecide-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-funcall-typedecide x ss scopes) (vl-funcall-typedecide x ss-equiv scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-funcall-typedecide-of-vl-elabscopes-fix-scopes (equal (vl-funcall-typedecide x ss (vl-elabscopes-fix scopes)) (vl-funcall-typedecide x ss scopes)))
Theorem:
(defthm vl-funcall-typedecide-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-funcall-typedecide x ss scopes) (vl-funcall-typedecide x ss scopes-equiv))) :rule-classes :congruence)