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 ((token-punctuatorp token "=") (binop-asg)) ((token-punctuatorp token "*=") (binop-asg-mul)) ((token-punctuatorp token "/=") (binop-asg-div)) ((token-punctuatorp token "%=") (binop-asg-rem)) ((token-punctuatorp token "+=") (binop-asg-add)) ((token-punctuatorp token "-=") (binop-asg-sub)) ((token-punctuatorp token "<<=") (binop-asg-shl)) ((token-punctuatorp token ">>=") (binop-asg-shr)) ((token-punctuatorp token "&=") (binop-asg-and)) ((token-punctuatorp token "^=") (binop-asg-xor)) ((token-punctuatorp token "|=") (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)