Map a token that is a type specifier consisting of a single keyword to the corresponding type specifier.
Function:
(defun token-to-type-specifier-keyword (token) (declare (xargs :guard (tokenp token))) (declare (xargs :guard (token-type-specifier-keyword-p token))) (let ((__function__ 'token-to-type-specifier-keyword)) (declare (ignorable __function__)) (cond ((equal token (token-keyword "void")) (tyspec-void)) ((equal token (token-keyword "char")) (tyspec-char)) ((equal token (token-keyword "short")) (tyspec-short)) ((equal token (token-keyword "int")) (tyspec-int)) ((equal token (token-keyword "long")) (tyspec-long)) ((equal token (token-keyword "float")) (tyspec-float)) ((equal token (token-keyword "double")) (tyspec-double)) ((equal token (token-keyword "signed")) (tyspec-signed)) ((equal token (token-keyword "unsigned")) (tyspec-unsigned)) ((equal token (token-keyword "_Bool")) (tyspec-bool)) ((equal token (token-keyword "_Complex")) (tyspec-complex)) (t (prog2$ (impossible) (irr-tyspec))))))
Theorem:
(defthm tyspecp-of-token-to-type-specifier-keyword (b* ((tyspec (token-to-type-specifier-keyword token))) (tyspecp tyspec)) :rule-classes :rewrite)