Map a token that is a type specifier consisting of a single keyword to the corresponding type specifier.
(token-to-type-specifier-keyword token) → tyspec
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 ((token-keywordp token "void") (type-spec-void)) ((token-keywordp token "char") (type-spec-char)) ((token-keywordp token "short") (type-spec-short)) ((token-keywordp token "int") (type-spec-int)) ((token-keywordp token "long") (type-spec-long)) ((token-keywordp token "float") (type-spec-float)) ((token-keywordp token "double") (type-spec-double)) ((token-keywordp token "signed") (type-spec-signed (keyword-uscores-none))) ((token-keywordp token "__signed") (type-spec-signed (keyword-uscores-start))) ((token-keywordp token "__signed__") (type-spec-signed (keyword-uscores-both))) ((token-keywordp token "unsigned") (type-spec-unsigned)) ((token-keywordp token "_Bool") (type-spec-bool)) ((token-keywordp token "_Complex") (type-spec-complex)) ((token-keywordp token "__int128") (type-spec-int128)) ((token-keywordp token "_Float128") (type-spec-float128)) ((token-keywordp token "__builtin_va_list") (type-spec-builtin-va-list)) (t (prog2$ (impossible) (irr-type-spec))))))
Theorem:
(defthm type-specp-of-token-to-type-specifier-keyword (b* ((tyspec (token-to-type-specifier-keyword token))) (type-specp tyspec)) :rule-classes :rewrite)