Core of computing expression signedness.
(vl-expr-typedecide-aux x ss ctx warnings mode) → (mv warnings type)
Warning: this function should typically only be called by the expression-sizing transform.
These are the same arguments as vl-expr-typedecide except for
Theorem:
(defthm return-type-of-vl-expr-typedecide-aux.warnings (b* (((mv ?warnings common-lisp::?type) (vl-expr-typedecide-aux x ss ctx warnings mode))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-expr-typedecide-aux.type (b* (((mv ?warnings common-lisp::?type) (vl-expr-typedecide-aux x ss ctx warnings mode))) (and (vl-maybe-exprtype-p type) (equal (vl-exprtype-p type) (if type t nil)))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-exprlist-typedecide-aux.warnings (b* (((mv ?warnings ?types) (vl-exprlist-typedecide-aux x ss ctx warnings mode))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-exprlist-typedecide-aux.types (b* (((mv ?warnings ?types) (vl-exprlist-typedecide-aux x ss ctx warnings mode))) (vl-maybe-exprtype-list-p types)) :rule-classes :rewrite)
Theorem:
(defthm vl-exprlist-typedecide-aux-of-cons (equal (vl-exprlist-typedecide-aux (cons a x) ss ctx warnings mode) (b* (((mv warnings car-type) (vl-expr-typedecide-aux a ss ctx warnings mode)) ((mv warnings cdr-type) (vl-exprlist-typedecide-aux x ss ctx warnings mode))) (mv warnings (cons car-type cdr-type)))))
Theorem:
(defthm len-of-vl-exprlist-typedecide-aux (equal (len (mv-nth 1 (vl-exprlist-typedecide-aux x ss ctx warnings mode))) (len x)))
Theorem:
(defthm true-listp-of-vl-exprlist-typedecide-aux (true-listp (mv-nth 1 (vl-exprlist-typedecide-aux x ss ctx warnings mode))) :rule-classes :type-prescription)
Theorem:
(defthm vl-expr-typedecide-aux-of-vl-expr-fix-x (equal (vl-expr-typedecide-aux (vl-expr-fix x) ss ctx warnings mode) (vl-expr-typedecide-aux x ss ctx warnings mode)))
Theorem:
(defthm vl-expr-typedecide-aux-of-vl-scopestack-fix-ss (equal (vl-expr-typedecide-aux x (vl-scopestack-fix ss) ctx warnings mode) (vl-expr-typedecide-aux x ss ctx warnings mode)))
Theorem:
(defthm vl-expr-typedecide-aux-of-vl-context-fix-ctx (equal (vl-expr-typedecide-aux x ss (vl-context-fix ctx) warnings mode) (vl-expr-typedecide-aux x ss ctx warnings mode)))
Theorem:
(defthm vl-expr-typedecide-aux-of-vl-warninglist-fix-warnings (equal (vl-expr-typedecide-aux x ss ctx (vl-warninglist-fix warnings) mode) (vl-expr-typedecide-aux x ss ctx warnings mode)))
Theorem:
(defthm vl-exprlist-typedecide-aux-of-vl-exprlist-fix-x (equal (vl-exprlist-typedecide-aux (vl-exprlist-fix x) ss ctx warnings mode) (vl-exprlist-typedecide-aux x ss ctx warnings mode)))
Theorem:
(defthm vl-exprlist-typedecide-aux-of-vl-scopestack-fix-ss (equal (vl-exprlist-typedecide-aux x (vl-scopestack-fix ss) ctx warnings mode) (vl-exprlist-typedecide-aux x ss ctx warnings mode)))
Theorem:
(defthm vl-exprlist-typedecide-aux-of-vl-context-fix-ctx (equal (vl-exprlist-typedecide-aux x ss (vl-context-fix ctx) warnings mode) (vl-exprlist-typedecide-aux x ss ctx warnings mode)))
Theorem:
(defthm vl-exprlist-typedecide-aux-of-vl-warninglist-fix-warnings (equal (vl-exprlist-typedecide-aux x ss ctx (vl-warninglist-fix warnings) mode) (vl-exprlist-typedecide-aux x ss ctx warnings mode)))
Theorem:
(defthm vl-expr-typedecide-aux-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-expr-typedecide-aux x ss ctx warnings mode) (vl-expr-typedecide-aux x-equiv ss ctx warnings mode))) :rule-classes :congruence)
Theorem:
(defthm vl-expr-typedecide-aux-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-expr-typedecide-aux x ss ctx warnings mode) (vl-expr-typedecide-aux x ss-equiv ctx warnings mode))) :rule-classes :congruence)
Theorem:
(defthm vl-expr-typedecide-aux-vl-context-equiv-congruence-on-ctx (implies (vl-context-equiv ctx ctx-equiv) (equal (vl-expr-typedecide-aux x ss ctx warnings mode) (vl-expr-typedecide-aux x ss ctx-equiv warnings mode))) :rule-classes :congruence)
Theorem:
(defthm vl-expr-typedecide-aux-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-expr-typedecide-aux x ss ctx warnings mode) (vl-expr-typedecide-aux x ss ctx warnings-equiv mode))) :rule-classes :congruence)
Theorem:
(defthm vl-exprlist-typedecide-aux-vl-exprlist-equiv-congruence-on-x (implies (vl-exprlist-equiv x x-equiv) (equal (vl-exprlist-typedecide-aux x ss ctx warnings mode) (vl-exprlist-typedecide-aux x-equiv ss ctx warnings mode))) :rule-classes :congruence)
Theorem:
(defthm vl-exprlist-typedecide-aux-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-exprlist-typedecide-aux x ss ctx warnings mode) (vl-exprlist-typedecide-aux x ss-equiv ctx warnings mode))) :rule-classes :congruence)
Theorem:
(defthm vl-exprlist-typedecide-aux-vl-context-equiv-congruence-on-ctx (implies (vl-context-equiv ctx ctx-equiv) (equal (vl-exprlist-typedecide-aux x ss ctx warnings mode) (vl-exprlist-typedecide-aux x ss ctx-equiv warnings mode))) :rule-classes :congruence)
Theorem:
(defthm vl-exprlist-typedecide-aux-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-exprlist-typedecide-aux x ss ctx warnings mode) (vl-exprlist-typedecide-aux x ss ctx warnings-equiv mode))) :rule-classes :congruence)
Theorem:
(defthm warning-irrelevance-of-vl-expr-typedecide-aux (let ((ret1 (vl-expr-typedecide-aux x ss ctx warnings mode)) (ret2 (vl-expr-typedecide-aux x ss nil nil mode))) (implies (syntaxp (not (and (equal ctx ''nil) (equal warnings ''nil)))) (equal (mv-nth 1 ret1) (mv-nth 1 ret2)))))
Theorem:
(defthm warning-irrelevance-of-vl-exprlist-typedecide-aux (let ((ret1 (vl-exprlist-typedecide-aux x ss ctx warnings mode)) (ret2 (vl-exprlist-typedecide-aux x ss nil nil mode))) (implies (syntaxp (not (and (equal ctx ''nil) (equal warnings ''nil)))) (equal (mv-nth 1 ret1) (mv-nth 1 ret2)))))
Theorem:
(defthm symbolp-of-vl-expr-typedecide-aux (symbolp (mv-nth 1 (vl-expr-typedecide-aux x ss ctx warnings mode))) :rule-classes :type-prescription)
Theorem:
(defthm vl-exprlist-typedecide-aux-when-atom (implies (atom x) (equal (vl-exprlist-typedecide-aux x ss ctx warnings mode) (mv (ok) nil))))