Revise frontmatter grammar, add ⊥ rule

The prior commit added a grammar for frontmatter, but the grammar
notation available at the time that commit was prepared couldn't
express all of the invariants the language requires.  Opening and
closing fences must have the same dash count.  Indented fences must
be rejected as an error.  And once an opening fence is recognized,
the parser must commit -- it can't backtrack and reinterpret the
dashes as tokens.

Since then, we've added named range repeats, hard cut, and negative
lookahead to the grammar notation.  With these, we can express the
invariants directly.

In this commit, we rewrite the frontmatter grammar.  Named range
repeats let the closing fence reference the opening fence's
dash count.  Hard cut commits the parse after the opening
dashes.  And `FRONTMATTER_INVALID` uses hard cut followed by
the bottom rule (`^ ⊥`) to express that indented fences are a
recognized-and-rejected syntactic form.  We also add `⊥` as a
primitive rule in the Notation chapter, move `HORIZONTAL_WHITESPACE`
to Whitespace, and fix some minor editorial matters such as
indentation and comment style.

Author: traviscross

src/frontmatter.md

@@ -4,27 +4,35 @@ r[frontmatter]
 r[frontmatter.syntax]
 ```grammar,lexer
 @root FRONTMATTER ->
-      FRONTMATTER_FENCE HORIZONTAL_WHITESPACE* INFOSTRING? HORIZONTAL_WHITESPACE* LF
-      (FRONTMATTER_LINE LF )*
-      FRONTMATTER_FENCE[^matched-fence] HORIZONTAL_WHITESPACE* LF
+    WHITESPACE_ONLY_LINE*
+    !FRONTMATTER_INVALID
+    FRONTMATTER_MAIN
 
-FRONTMATTER_FENCE -> `-`{3..255}
+WHITESPACE_ONLY_LINE -> (!LF WHITESPACE)* LF
 
-INFOSTRING -> (XID_Start | `_`) ( XID_Continue | `-` | `.` )*
+FRONTMATTER_INVALID -> (!LF WHITESPACE)+ `---` ^ ⊥
 
-FRONTMATTER_LINE -> (~INVALID_FRONTMATTER_LINE_START (~INVALID_FRONTMATTER_LINE_CONTINUE)*)?
+FRONTMATTER_MAIN ->
+    `-`{n:3..=255} ^ FRONTMATTER_REST
 
-INVALID_FRONTMATTER_LINE_START -> (FRONTMATTER_FENCE[^escaped-fence] | CR | LF)
+FRONTMATTER_REST ->
+    FRONTMATTER_FENCE_START
+    FRONTMATTER_LINE*
+    FRONTMATTER_FENCE_END
 
-INVALID_FRONTMATTER_LINE_CONTINUE -> CR | LF
+FRONTMATTER_FENCE_START ->
+    MAYBE_INFOSTRING_OR_WS LF
 
-HORIZONTAL_WHITESPACE ->
-      U+0009  // horizontal tab, `'\t'`
-    | U+0020  // space, `' '`
-```
+FRONTMATTER_FENCE_END ->
+    `-`{n} HORIZONTAL_WHITESPACE* ( LF | EOF )
+
+FRONTMATTER_LINE -> !`-`{n} ~[LF CR]* LF
 
-[^matched-fence]: The closing fence must have the same number of `-` as the opening fence
-[^escaped-fence]: A `FRONTMATTER_FENCE` at the beginning of a `FRONTMATTER_LINE` is only invalid if it has the same or more `-` as the `FRONTMATTER_FENCE`
+MAYBE_INFOSTRING_OR_WS ->
+    HORIZONTAL_WHITESPACE* INFOSTRING? HORIZONTAL_WHITESPACE*
+
+INFOSTRING -> (XID_Start | `_`) ( XID_Continue | `-` | `.` )*
+```
 
 r[frontmatter.intro]
 Frontmatter is an optional section for content intended for external tools without requiring these tools to have full knowledge of the Rust grammar.

src/notation.md

@@ -45,6 +45,18 @@ Mizushima et al. introduced [cut operators][cut operator paper] to parsing expre
 
 The hard cut operator is necessary because some tokens in Rust begin with a prefix that is itself a valid token. For example, `c"` begins a C string literal, but `c` alone is a valid identifier. Without the cut, if `c"\0"` failed to lex as a C string literal (because null bytes are not allowed in C strings), the parser could backtrack and lex it as two tokens: the identifier `c` and the string literal `"\0"`. The [cut after `c"`] prevents this --- once the opening delimiter is recognized, the parser cannot go back. The same reasoning applies to [byte literals], [byte string literals], [raw string literals], and other literals with prefixes that are themselves valid tokens.
 
+r[notation.grammar.bottom]
+### The bottom rule
+
+In logic, ⊥ (*bottom*) represents *absurdity* --- a proposition that is always false. In type theory, it is the *empty type* --- a type with no inhabitants. The grammar borrows both senses: the rule ⊥ matches nothing --- not any character, not even the end of input.
+
+```grammar,notation
+// The bottom rule does not match anything.
+⊥ -> !(CHAR | EOF)
+```
+
+Placed after a [hard cut operator], ⊥ makes a rule fail unconditionally once the parser has committed past the cut. This gives the grammar a way to express recognition without acceptance. The parser identifies the input, commits so that no other alternative can be tried, and then rejects it. In the frontmatter grammar, for example, [FRONTMATTER_INVALID] uses `^ ⊥` to recognize an opening fence preceded by whitespace on the same line --- input that is close enough to frontmatter to rule out other interpretations but is not valid.
+
 r[notation.grammar.string-tables]
 ### String table productions
 

src/whitespace.md

@@ -16,6 +16,10 @@ WHITESPACE ->
     | U+2028 // Line separator
     | U+2029 // Paragraph separator
 
+HORIZONTAL_WHITESPACE ->
+      U+0009 // Horizontal tab, `'\t'`
+    | U+0020 // Space, `' '`
+
 TAB -> U+0009 // Horizontal tab, `'\t'`
 
 LF -> U+000A  // Line feed, `'\n'`