Check if all the declaration specifiers in a list are type specifiers or storage class specifiers.
(check-declspec-list-all-tyspec/storspec declspecs) → (mv yes/no tyspecs stor-specs)
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/storspec (declspecs) (declare (xargs :guard (declspec-listp declspecs))) (let ((__function__ 'check-declspec-list-all-tyspec/storspec)) (declare (ignorable __function__)) (b* (((when (endp declspecs)) (mv t nil nil)) (declspec (car declspecs)) ((when (declspec-case declspec :tyspec)) (b* (((mv yes/no tyspecs stor-specs) (check-declspec-list-all-tyspec/storspec (cdr declspecs)))) (if yes/no (mv t (cons (declspec-tyspec->unwrap declspec) tyspecs) stor-specs) (mv nil nil nil)))) ((when (declspec-case declspec :stocla)) (b* (((mv yes/no tyspecs stor-specs) (check-declspec-list-all-tyspec/storspec (cdr declspecs)))) (if yes/no (mv t tyspecs (cons (declspec-stocla->unwrap declspec) stor-specs)) (mv nil nil nil))))) (mv nil nil nil))))
Theorem:
(defthm booleanp-of-check-declspec-list-all-tyspec/storspec.yes/no (b* (((mv ?yes/no ?tyspecs ?stor-specs) (check-declspec-list-all-tyspec/storspec declspecs))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm type-spec-listp-of-check-declspec-list-all-tyspec/storspec.tyspecs (b* (((mv ?yes/no ?tyspecs ?stor-specs) (check-declspec-list-all-tyspec/storspec declspecs))) (type-spec-listp tyspecs)) :rule-classes :rewrite)
Theorem:
(defthm stor-spec-listp-of-check-declspec-list-all-tyspec/storspec.stor-specs (b* (((mv ?yes/no ?tyspecs ?stor-specs) (check-declspec-list-all-tyspec/storspec declspecs))) (stor-spec-listp stor-specs)) :rule-classes :rewrite)
Theorem:
(defthm check-declspec-list-all-tyspec/storspec-of-declspec-list-fix-declspecs (equal (check-declspec-list-all-tyspec/storspec (declspec-list-fix declspecs)) (check-declspec-list-all-tyspec/storspec declspecs)))
Theorem:
(defthm check-declspec-list-all-tyspec/storspec-declspec-list-equiv-congruence-on-declspecs (implies (declspec-list-equiv declspecs declspecs-equiv) (equal (check-declspec-list-all-tyspec/storspec declspecs) (check-declspec-list-all-tyspec/storspec declspecs-equiv))) :rule-classes :congruence)