Check if all the declaration specifiers in a list are type specifiers or storage class specifiers.
(check-declspec-list-all-tyspec/stoclaspec declspecs) → (mv yes/no tyspecs stoclaspecs)
If the check succeeds, also return the lists of type specifiers and storage class specifiers, in the same order.
Function:
(defun check-declspec-list-all-tyspec/stoclaspec (declspecs) (declare (xargs :guard (declspec-listp declspecs))) (let ((__function__ 'check-declspec-list-all-tyspec/stoclaspec)) (declare (ignorable __function__)) (b* (((when (endp declspecs)) (mv t nil nil)) (declspec (car declspecs)) ((when (declspec-case declspec :tyspec)) (b* (((mv yes/no tyspecs stoclaspecs) (check-declspec-list-all-tyspec/stoclaspec (cdr declspecs)))) (if yes/no (mv t (cons (declspec-tyspec->unwrap declspec) tyspecs) stoclaspecs) (mv nil nil nil)))) ((when (declspec-case declspec :stocla)) (b* (((mv yes/no tyspecs stoclaspecs) (check-declspec-list-all-tyspec/stoclaspec (cdr declspecs)))) (if yes/no (mv t tyspecs (cons (declspec-stocla->unwrap declspec) stoclaspecs)) (mv nil nil nil))))) (mv nil nil nil))))
Theorem:
(defthm booleanp-of-check-declspec-list-all-tyspec/stoclaspec.yes/no (b* (((mv ?yes/no ?tyspecs ?stoclaspecs) (check-declspec-list-all-tyspec/stoclaspec declspecs))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm tyspec-listp-of-check-declspec-list-all-tyspec/stoclaspec.tyspecs (b* (((mv ?yes/no ?tyspecs ?stoclaspecs) (check-declspec-list-all-tyspec/stoclaspec declspecs))) (tyspec-listp tyspecs)) :rule-classes :rewrite)
Theorem:
(defthm stoclaspec-listp-of-check-declspec-list-all-tyspec/stoclaspec.stoclaspecs (b* (((mv ?yes/no ?tyspecs ?stoclaspecs) (check-declspec-list-all-tyspec/stoclaspec declspecs))) (stoclaspec-listp stoclaspecs)) :rule-classes :rewrite)
Theorem:
(defthm check-declspec-list-all-tyspec/stoclaspec-of-declspec-list-fix-declspecs (equal (check-declspec-list-all-tyspec/stoclaspec (declspec-list-fix declspecs)) (check-declspec-list-all-tyspec/stoclaspec declspecs)))
Theorem:
(defthm check-declspec-list-all-tyspec/stoclaspec-declspec-list-equiv-congruence-on-declspecs (implies (declspec-list-equiv declspecs declspecs-equiv) (equal (check-declspec-list-all-tyspec/stoclaspec declspecs) (check-declspec-list-all-tyspec/stoclaspec declspecs-equiv))) :rule-classes :congruence)