Get the self-determined type for a datatype.
(vl-datatype-exprtype x) → (mv successp errmsg type)
BOZO we don't try very hard yet. Eventually this will need to know how to look up the sizes of user-defined types, etc.
BOZO At the moment we treat unpacked stuff just like packed stuff, and there's not much error checking for using unpacked stuff improperly.
Function:
(defun vl-datatype-exprtype (x) (declare (xargs :guard (vl-datatype-p x))) (let ((__function__ 'vl-datatype-exprtype)) (declare (ignorable __function__)) (b* (((fun (fail reason)) (mv nil reason nil)) ((fun (success width)) (mv t nil width)) ((when (consp (vl-datatype->udims x))) (success :vl-unsigned))) (vl-datatype-case x (:vl-coretype (case x.name ((:vl-byte :vl-shortint :vl-int :vl-longint :vl-integer :vl-time :vl-bit :vl-logic :vl-reg) (success (if x.signedp :vl-signed :vl-unsigned))) (otherwise (success nil)))) (:vl-enum (fail "bozo: implement enum typing")) (:vl-struct (b* (((unless x.packedp) (success :vl-unsigned))) (success (if x.signedp :vl-signed :vl-unsigned)))) (:vl-union (b* (((unless x.packedp) (success :vl-unsigned))) (success (if x.signedp :vl-signed :vl-unsigned)))) (:vl-usertype (fail "vl-datatype-exprtype can't handle unresolved usertypes"))))))
Theorem:
(defthm booleanp-of-vl-datatype-exprtype.successp (b* (((mv ?successp ?errmsg common-lisp::?type) (vl-datatype-exprtype x))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm maybe-stringp-of-vl-datatype-exprtype.errmsg (b* (((mv ?successp ?errmsg common-lisp::?type) (vl-datatype-exprtype x))) (maybe-stringp errmsg)) :rule-classes :type-prescription)
Theorem:
(defthm vl-maybe-exprtype-p-of-vl-datatype-exprtype.type (b* (((mv ?successp ?errmsg common-lisp::?type) (vl-datatype-exprtype x))) (vl-maybe-exprtype-p type)) :rule-classes :rewrite)
Theorem:
(defthm vl-datatype-exprtype-of-vl-datatype-fix-x (equal (vl-datatype-exprtype (vl-datatype-fix x)) (vl-datatype-exprtype x)))
Theorem:
(defthm vl-datatype-exprtype-vl-datatype-equiv-congruence-on-x (implies (vl-datatype-equiv x x-equiv) (equal (vl-datatype-exprtype x) (vl-datatype-exprtype x-equiv))) :rule-classes :congruence)