Measure for recurring over type structures.
Function:
(defun type-count (x) (declare (xargs :guard (typep x))) (let ((__function__ 'type-count)) (declare (ignorable __function__)) (case (type-kind x) (:void 1) (:char 1) (:schar 1) (:uchar 1) (:sshort 1) (:ushort 1) (:sint 1) (:uint 1) (:slong 1) (:ulong 1) (:sllong 1) (:ullong 1) (:struct 1) (:pointer (+ 2 (type-count (type-pointer->to x)))) (:array (+ 3 (type-count (type-array->of x)))))))
Theorem:
(defthm natp-of-type-count (b* ((count (type-count x))) (natp count)) :rule-classes :type-prescription)
Theorem:
(defthm type-count-of-type-fix-x (equal (type-count (type-fix x)) (type-count x)))
Theorem:
(defthm type-count-type-equiv-congruence-on-x (implies (type-equiv x x-equiv) (equal (type-count x) (type-count x-equiv))) :rule-classes :congruence)
Theorem:
(defthm type-count-of-type-pointer (implies t (< (+ (type-count to)) (type-count (type-pointer to)))) :rule-classes :linear)
Theorem:
(defthm type-count-of-type-pointer->to (implies (equal (type-kind x) :pointer) (< (type-count (type-pointer->to x)) (type-count x))) :rule-classes :linear)
Theorem:
(defthm type-count-of-type-array (implies t (< (+ (type-count of)) (type-count (type-array of size)))) :rule-classes :linear)
Theorem:
(defthm type-count-of-type-array->of (implies (equal (type-kind x) :array) (< (type-count (type-array->of x)) (type-count x))) :rule-classes :linear)