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 ((equal token (token-keyword "void")) (type-spec-void)) ((equal token (token-keyword "char")) (type-spec-char)) ((equal token (token-keyword "short")) (type-spec-short)) ((equal token (token-keyword "int")) (type-spec-int)) ((equal token (token-keyword "long")) (type-spec-long)) ((equal token (token-keyword "float")) (type-spec-float)) ((equal token (token-keyword "double")) (type-spec-double)) ((equal token (token-keyword "signed")) (type-spec-signed)) ((equal token (token-keyword "unsigned")) (type-spec-unsigned)) ((equal token (token-keyword "_Bool")) (type-spec-bool)) ((equal token (token-keyword "_Complex")) (type-spec-complex)) (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)