		Search-engine friendly clone of the ACL2 documentation.

Parser

Token-unary-expression-start-p

Check if an optional token may start a unary expression.

Signature
(token-unary-expression-start-p token? gcc) → yes/no
Arguments: token? — Guard (token-optionp token?).; gcc — Guard (booleanp gcc).
Returns: yes/no — Type (booleanp yes/no).

Looking at the grammar, a unary expression may be a postfix expression, which always starts with (or is) a primary expression, or it is a compound literal, which starts with an open parenthesis, which is already covered by the possible starts of a primary expression. In addition, a unary expression may start with a preincrement or predecrement operator, or a unary operator as defined in the grammar, or a sizeof keyword, or an _Alignof keyword.

We also compare the token against the GCC extension variants __alignof and __alignof__ of _Alignof. Note that this variant is a keywords only if GCC extensions are supported: lex-identifier/keyword checks the GCC flag of the parser state. So the comparison here with that variant keyword will always fail if GCC extensions are not supported, because in that case both __alignof__ would be an identifier token, not a keyword token.

We also include, in the comparison, the __real__ and __imag__ operators, which are keyword tokens only if GCC extensions are enabled.

If GCC extensions are enabled, we also include the unary operator && in the comparison.

Definitions and Theorems

Function: token-unary-expression-start-p

(defun token-unary-expression-start-p (token? gcc)
  (declare (xargs :guard (and (token-optionp token?)
                              (booleanp gcc))))
  (let ((__function__ 'token-unary-expression-start-p))
    (declare (ignorable __function__))
    (or (token-primary-expression-start-p token?)
        (token-punctuatorp token? "++")
        (token-punctuatorp token? "--")
        (token-punctuatorp token? "&")
        (token-punctuatorp token? "*")
        (token-punctuatorp token? "+")
        (token-punctuatorp token? "-")
        (token-punctuatorp token? "~")
        (token-punctuatorp token? "!")
        (token-keywordp token? "sizeof")
        (token-keywordp token? "_Alignof")
        (token-keywordp token? "__alignof")
        (token-keywordp token? "__alignof__")
        (token-keywordp token? "__real__")
        (token-keywordp token? "__imag__")
        (and gcc (token-punctuatorp token? "&&")))))

Theorem: booleanp-of-token-unary-expression-start-p

(defthm booleanp-of-token-unary-expression-start-p
  (b* ((yes/no (token-unary-expression-start-p token? gcc)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: non-nil-when-token-unary-expression-start-p

(defthm non-nil-when-token-unary-expression-start-p
  (implies (token-unary-expression-start-p token? gcc)
           token?)
  :rule-classes :forward-chaining)