Determine the (unpacked) type of an expression.
(vl-expr-selfdetermine-type x ss ctx warnings) → (mv successp type new-warnings)
Note: this function isn't used yet, because we don't try to support unpacked array concatenations yet.
In the context of unpacked array concatenations, the expressions inside the concatenation have to have self-determined type. We think this means that it has to be clear from looking at the expression whether it's an unpacked array/struct/whatever. If it is a packed structure, we think it doesn't matter what its type is.
If this function is successful, it returns a datatype. If it is an unpacked datatype, then we think it's the exact self-determined datatype of the expression. However, all packed datatypes are treated the same here -- in particular, the size and signedness of the packed datatype returned doesn't mean anything.
Function:
(defun vl-expr-selfdetermine-type (x ss ctx warnings) (declare (xargs :guard (and (vl-expr-p x) (vl-scopestack-p ss) (vl-context-p ctx) (vl-warninglist-p warnings)))) (let ((__function__ 'vl-expr-selfdetermine-type)) (declare (ignorable __function__)) (b* ((warnings (vl-warninglist-fix warnings)) ((when (vl-atom-p x)) (vl-atom-selfdetermine-type x ss ctx warnings)) ((vl-nonatom x)) ((when (member x.op '(:vl-hid-dot :vl-index))) (b* (((mv warning type) (vl-index-find-type x ss (vl-context-fix ctx))) ((when warning) (mv nil nil (cons warning (vl-warninglist-fix warnings))))) (mv t type warnings))) ((when (eq x.op :vl-qmark)) (b* (((mv ok1 type1 warnings) (vl-expr-selfdetermine-type (second x.args) ss ctx warnings)) ((mv ok2 type2 warnings) (vl-expr-selfdetermine-type (third x.args) ss ctx warnings)) ((unless (and ok1 ok2)) (mv nil nil warnings)) ((when (equal type1 type2)) (mv t type1 warnings)) ((when (and (vl-datatype->packedp type1) (vl-datatype->packedp type2))) (mv t type1 warnings))) (mv nil nil (warn :type :vl-expr-self-determined-type-fail :msg "~a0: Couldn't self-determine the type of ~a1 ~ because the branches have different types: ~a2 ~ versus ~a3." :args (list (vl-context-fix ctx) (vl-expr-fix x) type1 type2))))) ((when (eq x.op :vl-pattern-type)) (b* (((mv warning type) (vl-castexpr->datatype (first x.args) ss)) ((when warning) (mv nil nil (cons warning (vl-warninglist-fix warnings))))) (mv t type warnings))) ((when (or (vl-op-simple-vector-p x.op) (eq x.op :vl-concat))) (mv t *simple-vector-datatype* warnings))) (mv nil nil (warn :type :vl-expr-self-determined-type-fail :msg "~a0: Couldn't self-determine the type of ~a1." :args (list (vl-context-fix ctx) (vl-expr-fix x)))))))
Theorem:
(defthm booleanp-of-vl-expr-selfdetermine-type.successp (b* (((mv ?successp common-lisp::?type ?new-warnings) (vl-expr-selfdetermine-type x ss ctx warnings))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm return-type-of-vl-expr-selfdetermine-type.type (b* (((mv ?successp common-lisp::?type ?new-warnings) (vl-expr-selfdetermine-type x ss ctx warnings))) (implies successp (vl-datatype-p type))) :rule-classes :rewrite)
Theorem:
(defthm vl-warninglist-p-of-vl-expr-selfdetermine-type.new-warnings (b* (((mv ?successp common-lisp::?type ?new-warnings) (vl-expr-selfdetermine-type x ss ctx warnings))) (vl-warninglist-p new-warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr-selfdetermine-type-of-vl-expr-fix-x (equal (vl-expr-selfdetermine-type (vl-expr-fix x) ss ctx warnings) (vl-expr-selfdetermine-type x ss ctx warnings)))
Theorem:
(defthm vl-expr-selfdetermine-type-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-expr-selfdetermine-type x ss ctx warnings) (vl-expr-selfdetermine-type x-equiv ss ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-expr-selfdetermine-type-of-vl-scopestack-fix-ss (equal (vl-expr-selfdetermine-type x (vl-scopestack-fix ss) ctx warnings) (vl-expr-selfdetermine-type x ss ctx warnings)))
Theorem:
(defthm vl-expr-selfdetermine-type-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-expr-selfdetermine-type x ss ctx warnings) (vl-expr-selfdetermine-type x ss-equiv ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-expr-selfdetermine-type-of-vl-context-fix-ctx (equal (vl-expr-selfdetermine-type x ss (vl-context-fix ctx) warnings) (vl-expr-selfdetermine-type x ss ctx warnings)))
Theorem:
(defthm vl-expr-selfdetermine-type-vl-context-equiv-congruence-on-ctx (implies (vl-context-equiv ctx ctx-equiv) (equal (vl-expr-selfdetermine-type x ss ctx warnings) (vl-expr-selfdetermine-type x ss ctx-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-expr-selfdetermine-type-of-vl-warninglist-fix-warnings (equal (vl-expr-selfdetermine-type x ss ctx (vl-warninglist-fix warnings)) (vl-expr-selfdetermine-type x ss ctx warnings)))
Theorem:
(defthm vl-expr-selfdetermine-type-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-expr-selfdetermine-type x ss ctx warnings) (vl-expr-selfdetermine-type x ss ctx warnings-equiv))) :rule-classes :congruence)