Map a token that is an assignment operator to the corresponding assignment operator.
Function:
(defun token-to-assignment-operator (token) (declare (xargs :guard (tokenp token))) (declare (xargs :guard (token-assignment-operator-p token))) (let ((__function__ 'token-to-assignment-operator)) (declare (ignorable __function__)) (cond ((equal token (token-punctuator "=")) (binop-asg)) ((equal token (token-punctuator "*=")) (binop-asg-mul)) ((equal token (token-punctuator "/=")) (binop-asg-div)) ((equal token (token-punctuator "%=")) (binop-asg-rem)) ((equal token (token-punctuator "+=")) (binop-asg-add)) ((equal token (token-punctuator "-=")) (binop-asg-sub)) ((equal token (token-punctuator "<<=")) (binop-asg-shl)) ((equal token (token-punctuator ">>=")) (binop-asg-shr)) ((equal token (token-punctuator "&=")) (binop-asg-and)) ((equal token (token-punctuator "^=")) (binop-asg-xor)) ((equal token (token-punctuator "|=")) (binop-asg-ior)) (t (prog2$ (impossible) (irr-binop))))))
Theorem:
(defthm binopp-of-token-to-assignment-operator (b* ((op (token-to-assignment-operator token))) (binopp op)) :rule-classes :rewrite)