Map a token that is a type qualifier to the correspoding type qualifier.
Function:
(defun token-to-type-qualifier (token) (declare (xargs :guard (tokenp token))) (declare (xargs :guard (token-type-qualifier-p token))) (let ((__function__ 'token-to-type-qualifier)) (declare (ignorable __function__)) (cond ((equal token (token-keyword "const")) (tyqual-const)) ((equal token (token-keyword "restrict")) (tyqual-restrict)) ((equal token (token-keyword "volatile")) (tyqual-volatile)) ((equal token (token-keyword "_Atomic")) (tyqual-atomic)) ((equal token (token-keyword "__restrict")) (tyqual-__restrict)) ((equal token (token-keyword "__restrict__")) (tyqual-__restrict__)) (t (prog2$ (impossible) (irr-tyqual))))))
Theorem:
(defthm tyqualp-of-token-to-type-qualifier (b* ((tyqual (token-to-type-qualifier token))) (tyqualp tyqual)) :rule-classes :rewrite)