Check if an initializer type matches a type.
(init-type-matchp itype type) → wf?
This is used when comparing the type of an initializer with the declared type of the object.
If the initializer type is a single one, we require its type to match the declared type. We perform an array-to-pointer type conversion, consistently with assignments for scalars [C:6.7.9/11]; for structure types initialized via single expressions [C:6.7.9/13].
If the initializer type is a list, we require the declared type to be an array type such that all the types in the initializer list match the array element type. If the array type has a size, the length of the initializer list must match the array size.
Here we are a bit more restrictive than in [C:6.7.9]. In particular, [C:6.7.9/11] allows scalars to be initialized with singleton lists of expressions (i.e. single expressions between braces); but here we insist on scalars being initialized by single expressions.
Function:
(defun init-type-matchp (itype type) (declare (xargs :guard (and (init-typep itype) (typep type)))) (let ((__function__ 'init-type-matchp)) (declare (ignorable __function__)) (init-type-case itype :single (if (type-equiv type (apconvert-type itype.get)) :wellformed (reserrf (list :init-type-mismatch :required (type-fix type) :supplied (init-type-fix itype)))) :list (if (and (type-case type :array) (equal itype.get (repeat (len itype.get) (type-array->of type))) (or (not (type-array->size type)) (equal (type-array->size type) (len itype.get)))) :wellformed (reserrf (list :init-type-mismatch :required (type-fix type) :supplied (init-type-fix itype)))))))
Theorem:
(defthm wellformed-resultp-of-init-type-matchp (b* ((wf? (init-type-matchp itype type))) (wellformed-resultp wf?)) :rule-classes :rewrite)
Theorem:
(defthm init-type-matchp-of-init-type-fix-itype (equal (init-type-matchp (init-type-fix itype) type) (init-type-matchp itype type)))
Theorem:
(defthm init-type-matchp-init-type-equiv-congruence-on-itype (implies (init-type-equiv itype itype-equiv) (equal (init-type-matchp itype type) (init-type-matchp itype-equiv type))) :rule-classes :congruence)
Theorem:
(defthm init-type-matchp-of-type-fix-type (equal (init-type-matchp itype (type-fix type)) (init-type-matchp itype type)))
Theorem:
(defthm init-type-matchp-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (init-type-matchp itype type) (init-type-matchp itype type-equiv))) :rule-classes :congruence)