Adjust a parameter type.
Function parameter types are subject to an adjustment [C:6.7.6.3/7]: an array type is converted to a pointer type to the element type. Since we currently do not model type qualifiers, we do not need to take those into account here. Note that the size, if present, is lost.
Function:
(defun adjust-type (type) (declare (xargs :guard (typep type))) (let ((__function__ 'adjust-type)) (declare (ignorable __function__)) (if (type-case type :array) (make-type-pointer :to (type-array->of type)) (type-fix type))))
Theorem:
(defthm typep-of-adjust-type (b* ((type1 (adjust-type type))) (typep type1)) :rule-classes :rewrite)
Theorem:
(defthm adjust-type-of-type-fix-type (equal (adjust-type (type-fix type)) (adjust-type type)))
Theorem:
(defthm adjust-type-type-equiv-congruence-on-type (implies (type-equiv type type-equiv) (equal (adjust-type type) (adjust-type type-equiv))) :rule-classes :congruence)