Get the packed dimensions from any datatype.
(vl-datatype->pdims x) → pdims
Function:
(defun vl-datatype->pdims (x) (declare (xargs :guard (vl-datatype-p x))) (let ((__function__ 'vl-datatype->pdims)) (declare (ignorable __function__)) (vl-datatype-case x :vl-coretype x.pdims :vl-struct x.pdims :vl-union x.pdims :vl-enum x.pdims :vl-usertype x.pdims)))
Theorem:
(defthm vl-dimensionlist-p-of-vl-datatype->pdims (b* ((pdims (vl-datatype->pdims x))) (vl-dimensionlist-p pdims)) :rule-classes :rewrite)
Theorem:
(defthm vl-datatype->pdims-of-vl-datatype-fix-x (equal (vl-datatype->pdims (vl-datatype-fix x)) (vl-datatype->pdims x)))
Theorem:
(defthm vl-datatype->pdims-vl-datatype-equiv-congruence-on-x (implies (vl-datatype-equiv x x-equiv) (equal (vl-datatype->pdims x) (vl-datatype->pdims x-equiv))) :rule-classes :congruence)
These are goofy rules: normally we want to normalize things to
Theorem:
(defthm vl-datatype-pdims-when-vl-coretype (implies (vl-datatype-case x :vl-coretype) (and (implies (syntaxp (and (consp x) (eq (car x) 'vl-coretype))) (equal (vl-datatype->pdims x) (vl-coretype->pdims x))) (implies (syntaxp (not (and (consp x) (eq (car x) 'vl-coretype)))) (equal (vl-coretype->pdims x) (vl-datatype->pdims x))))))
Theorem:
(defthm vl-datatype-pdims-when-vl-struct (implies (vl-datatype-case x :vl-struct) (and (implies (syntaxp (and (consp x) (eq (car x) 'vl-struct))) (equal (vl-datatype->pdims x) (vl-struct->pdims x))) (implies (syntaxp (not (and (consp x) (eq (car x) 'vl-struct)))) (equal (vl-struct->pdims x) (vl-datatype->pdims x))))))
Theorem:
(defthm vl-datatype-pdims-when-vl-union (implies (vl-datatype-case x :vl-union) (and (implies (syntaxp (and (consp x) (eq (car x) 'vl-union))) (equal (vl-datatype->pdims x) (vl-union->pdims x))) (implies (syntaxp (not (and (consp x) (eq (car x) 'vl-union)))) (equal (vl-union->pdims x) (vl-datatype->pdims x))))))
Theorem:
(defthm vl-datatype-pdims-when-vl-enum (implies (vl-datatype-case x :vl-enum) (and (implies (syntaxp (and (consp x) (eq (car x) 'vl-enum))) (equal (vl-datatype->pdims x) (vl-enum->pdims x))) (implies (syntaxp (not (and (consp x) (eq (car x) 'vl-enum)))) (equal (vl-enum->pdims x) (vl-datatype->pdims x))))))
Theorem:
(defthm vl-datatype-pdims-when-vl-usertype (implies (vl-datatype-case x :vl-usertype) (and (implies (syntaxp (and (consp x) (eq (car x) 'vl-usertype))) (equal (vl-datatype->pdims x) (vl-usertype->pdims x))) (implies (syntaxp (not (and (consp x) (eq (car x) 'vl-usertype)))) (equal (vl-usertype->pdims x) (vl-datatype->pdims x))))))