Map a token that is a unary operator to the corresponding unary operator.
By this we mean a unary operator according to the grammar, not our abstract syntax, which has a broader notion of unary operator.
Function:
(defun token-to-unary-operator (token) (declare (xargs :guard (tokenp token))) (declare (xargs :guard (token-unary-operator-p token))) (let ((__function__ 'token-to-unary-operator)) (declare (ignorable __function__)) (cond ((equal token (token-punctuator "&")) (unop-address)) ((equal token (token-punctuator "*")) (unop-indir)) ((equal token (token-punctuator "+")) (unop-plus)) ((equal token (token-punctuator "-")) (unop-minus)) ((equal token (token-punctuator "~")) (unop-bitnot)) ((equal token (token-punctuator "!")) (unop-lognot)) (t (prog2$ (impossible) (irr-unop))))))
Theorem:
(defthm unopp-of-token-to-unary-operator (b* ((op (token-to-unary-operator token))) (unopp op)) :rule-classes :rewrite)