|
|
|---|
|
|
|
|---|
Check if a preprocessing lexeme is a token or a newline.
During preprocessing, newline characters are significant: see grammar rules in [C17:6.10/1]. Preprocessing is largely line-oriented. In our preprocessor, newline characters are captured as newline lexemes (see plexeme).
[C17:5.1.1.2/3] requires that comments, including line comments, are turned into single space characters; we do not actually do that, to preserve the comment information, but conceptually we need our preprocessor to behave as if we did. This means that, if we are looking for tokens or newline characters, we must also consider line comments, because they are always followed by a newline character; recall that line comments exclude the ending newline [C17:6.4.9/2]. Although block comments may include newlines, those are part of the comment: the whole comment is turned into a space character, and so there are no newlines to consider here.
Function:
(defun plexeme-token/newline-p (lexeme) (declare (xargs :guard (plexemep lexeme))) (or (plexeme-tokenp lexeme) (plexeme-case lexeme :newline) (plexeme-case lexeme :line-comment)))
Theorem:
(defthm booleanp-of-plexeme-token/newline-p (b* ((yes/no (plexeme-token/newline-p lexeme))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm plexeme-token/newline-p-of-plexeme-fix-lexeme (equal (plexeme-token/newline-p (plexeme-fix lexeme)) (plexeme-token/newline-p lexeme)))
Theorem:
(defthm plexeme-token/newline-p-plexeme-equiv-congruence-on-lexeme (implies (plexeme-equiv lexeme lexeme-equiv) (equal (plexeme-token/newline-p lexeme) (plexeme-token/newline-p lexeme-equiv))) :rule-classes :congruence)