Effectively computes the "self-determined" type of an atom.
(vl-atom-typedecide x ss ctx warnings) → (mv warnings type)
Warning: this function should typically only be called by the expression-sizing transform.
We compute what the type of the atom
The
Function:
(defun vl-atom-typedecide (x ss ctx warnings) (declare (xargs :guard (and (vl-expr-p x) (vl-scopestack-p ss) (vl-context-p ctx) (vl-warninglist-p warnings)))) (declare (xargs :guard (vl-atom-p x))) (let ((__function__ 'vl-atom-typedecide)) (declare (ignorable __function__)) (b* ((ctx (vl-context-fix ctx)) (guts (vl-atom->guts x)) ((when (vl-fast-constint-p guts)) (mv (ok) (vl-constint->origtype guts))) ((when (vl-fast-weirdint-p guts)) (mv (ok) (vl-weirdint->origtype guts))) ((when (vl-fast-string-p guts)) (mv (ok) :vl-unsigned)) ((when (eq (tag guts) :vl-extint)) (mv (ok) :vl-signed)) ((unless (or (vl-fast-id-p guts) (vl-fast-hidpiece-p guts))) (mv (ok) nil))) (vl-index-typedecide x ss ctx warnings))))
Theorem:
(defthm vl-warninglist-p-of-vl-atom-typedecide.warnings (b* (((mv ?warnings common-lisp::?type) (vl-atom-typedecide x ss ctx warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-atom-typedecide.type (b* (((mv ?warnings common-lisp::?type) (vl-atom-typedecide x ss ctx warnings))) (and (vl-maybe-exprtype-p type) (equal (vl-exprtype-p type) (if type t nil)))) :rule-classes :rewrite)
Theorem:
(defthm warning-irrelevance-of-vl-atom-typedecide (let ((ret1 (vl-atom-typedecide x ss ctx warnings)) (ret2 (vl-atom-typedecide x ss nil nil))) (implies (syntaxp (not (and (equal ctx ''nil) (equal warnings ''nil)))) (equal (mv-nth 1 ret1) (mv-nth 1 ret2)))))
Theorem:
(defthm vl-atom-typedecide-of-vl-expr-fix-x (equal (vl-atom-typedecide (vl-expr-fix x) ss ctx warnings) (vl-atom-typedecide x ss ctx warnings)))
Theorem:
(defthm vl-atom-typedecide-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-atom-typedecide x ss ctx warnings) (vl-atom-typedecide x-equiv ss ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-atom-typedecide-of-vl-scopestack-fix-ss (equal (vl-atom-typedecide x (vl-scopestack-fix ss) ctx warnings) (vl-atom-typedecide x ss ctx warnings)))
Theorem:
(defthm vl-atom-typedecide-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-atom-typedecide x ss ctx warnings) (vl-atom-typedecide x ss-equiv ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-atom-typedecide-of-vl-context-fix-ctx (equal (vl-atom-typedecide x ss (vl-context-fix ctx) warnings) (vl-atom-typedecide x ss ctx warnings)))
Theorem:
(defthm vl-atom-typedecide-vl-context-equiv-congruence-on-ctx (implies (vl-context-equiv ctx ctx-equiv) (equal (vl-atom-typedecide x ss ctx warnings) (vl-atom-typedecide x ss ctx-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-atom-typedecide-of-vl-warninglist-fix-warnings (equal (vl-atom-typedecide x ss ctx (vl-warninglist-fix warnings)) (vl-atom-typedecide x ss ctx warnings)))
Theorem:
(defthm vl-atom-typedecide-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-atom-typedecide x ss ctx warnings) (vl-atom-typedecide x ss ctx warnings-equiv))) :rule-classes :congruence)