Grammar-parser-disambiguation
Disambiguation theorems for the parser of ABNF grammars.
If a (list of) terminated tree(s) matches a syntactic entity,
attempting to parse the string at the leaves of the tree(s)
with a parsing function for a different syntactic entity fails, in general.
For example, if a terminated tree matches HTAB,
parse-sp fails on the string at the leaves of the tree:
this is stated by the disambiguation theorem
fail-sp-when-match-htab.
The disambiguation theorems below state this kind of facts.
Essentially, these theorems say that certain syntactic entities
are incompatible with certain parsing functions;
they are used to show that the parser can disambiguate its input
(hence the name of these theorems).
Usage
The disambiguation theorems are used to prove the completeness theorems.
The disambiguation theorems are rewrite rules that are disabled by default.
They are explicitly enabled in the individual completeness theorems.
Some disambiguation theorems are used
to incrementally prove other disambiguation theorems (see below),
also via explicit enabling.
Scope
There are disambiguation theorems
only for some combinations of syntactic entities and parsing functions:
just the ones used to prove the completeness theorems,
and to incrementally prove other disambiguation theorems.
Given the potentially ``quadratic'' number
of disambiguation theorems
(i.e. for all syntactic entities combined with all parsing functions),
some disambiguation theorems group together
multiple tree matching hypotheses or multiple parsing failure conclusions.
For example, fail-bit/digit/hexdig/dot/dash-when-match-slash
asserts the failure of multiple parsing functions
for the given tree matching hypothesis:
this theorem replaces five potential theorems
(one for each parsing function mentioned there).
As another example, fail-cwsp-when-match-alt/conc/rep
asserts the failure of a given parsing function
for multiple syntactic entities matched by the tree:
this theorem replaces three potential theorems
(one for each syntactic entity mentioned there).
More grouping (and thus reduction in the number of disambiguation theorems)
is possible,
but we also try to keep the disambiguation theorems' names
sufficiently descriptive while not excessively long.
Formulation
The formulation of the disambiguation theorems is derived from
the subgoals that arise in the completeness proofs
(and in the incrementally proved disambiguation proofs):
the disambiguation theorems serve to prove those subgoals.
The disambiguation theorems were developed
in the process of proving the completeness theorems,
based on failed subgoals in the latter.
In particular,
the ``asymmetric'' use of trees and parsing functions
to show incompatibility
(as opposed to showing incompatibility
between parsing functions or between trees)
reflects the structure of the subgoals in the completeness theorems;
see the documentation of the completeness theorems for details.
The formulation of each disambiguation theorem also involves
some remaining input
that is appended after the string at the leaves of the tree(s).
That is, each disambiguation theorem says something of this form:
if a (list of) terminated tree(s) matches certain syntactic entities
and possibly satisfies certain disambiguating restrictions, then running certain parsing functions on the append of
(i) the string at the leaves of the tree and
(ii) some remaining input
possibly satisfing certain hypotheses explained below,
fails.
This is similar to the way in which
the completeness theorems are formulated.
Most disambiguation theorems involve a single (list of) tree(s).
Four of them (i.e.
fail-alpha/digit/dash-when-match-*cwsp-close-round/square,
fail-bit/digit/hexdig/dot/dash-when-match-*cwsp-close-round/square,
fail-alt-rest-comp-when-match-*cwsp-close-round/square, and
fail-conc-rest-comp-when-match-*cwsp-close-round/square)
involve a list of trees matching *c-wsp
and a tree matching ")" or "]";
the parsing function in their conclusion
is applied to the append of
(i) the string at the leaves of the list of trees,
(ii) the string at the leaves of the tree, and
(iii) some remaining input.
These four theorems are used
in the completeness proofs of the mutually recursive parsing functions,
precisely in the induction step lemmas
for parse-group and parse-option.
In those lemmas, the tree matching hypothesis reduces to, among others,
the fact that a list of subtrees matches *c-wsp
and that the subtree just after that list matches ")" or "]":
the four disambiguation theorems apply to that (list of) subtree(s).
Note that *c-wsp ")" and *c-wsp "]" are the ending parts
of the definientia of group and option.
Hypotheses on the Remaining Input
In all the disambiguation theorems,
the remaining input (following the string at the leaves of the tree(s))
is denoted by the variable rest-input.
The hypotheses on the remaining input, when present,
are that certain parsing functions fail on the remaining input.
In most cases, the hypotheses on the remaining input are present
when the (list of) tree(s) may have an empty string at the leaves.
When that string is empty,
the incompatibility between the tree(s) and the parsing functions
does not apply.
Thus, each of these theorems includes the hypothesis
that the parsing function fails on the remaining input,
to ensure that the conclusion holds in this case.
For example, in fail-bit-when-match-*cwsp,
if the list of trees is empty,
the incompatibility
between (the first tree of the list matching) c-wsp
and the parsing function parse-bit does not apply;
but the hypothesis that parse-bit fails on rest-input
maintains the truth of the theorem in case the list of trees is empty.
In general, for each of these disambiguation theorems,
the hypothesis asserts the failure on the remaining input
of the same parsing function that the theorem shows to be
incompatible with the syntactic entity matched by the tree(s).
The hypotheses just mentioned could be weakened
to require the parsing failure on the remaining input
only if the string at the leaves of the tree(s) is in fact empty;
however, the stronger hypotheses keep the theorems simpler
without precluding the eventual proof of
the top-level completeness theorem.
Another possibility is to have, instead, hypotheses stating that
the string at the leaves of the tree(s) are not empty;
however, the current formulation seems more readily usable
in the proofs of completeness,
obviating a case split based on whether the string is empty or not.
The disambiguation theorem
fail-equal-slash-when-match-equal-and-rest-fail-slash
has the hypothesis that parse-ichar with argument #\/
fails on the remaining input.
Without this hypothesis,
parse-ichar2 with arguments #\= and #\/ could succeed:
after parsing the "=" in the string at the leaves of the tree,
it could parse a "/" in the remaining input,
obtaining a "=/".
The disambiguation theorem
fail-*digit-star-*digit-when-match-1*digit
has the hypotheses that
both parse-ichar with argument #\*
and parse-digit
fail on the remaining input.
Without the first hypothesis,
parse-*digit-star-*digit could succeed:
after parsing the DIGITs from the string at the leaves of the trees,
it could parse a "*" from the remaining input,
and then zero or more DIGITs,
obtaining a (*DIGIT "*" *DIGIT).
Without the second hypothesis,
parse-*digit-star-*digit could also succeed:
after parsing the DIGITs from the string at the leaves of the trees,
it could parse additional DIGITs from the remaining input,
then a "*",
and then zero or more DIGITs,
obtaining a (*DIGIT "*" *DIGIT).
The second hypothesis is stronger than needed,
because the presence of a DIGIT at the start of the remaining input
does not imply the success of parse-*digit-star-*digit;
however, the stronger hypothesis keeps the theorems simpler
without precluding the eventual proof of
the top-level completeness theorem.
The disambiguation theorem fail-cwsp-when-match-cnl
has the hypothesis that parse-wsp fails on the remaining input.
Without this hypothesis, parse-cwsp could succeed:
after parsing the c-nl from the string at the leaves of the tree,
it could parse a WSP from the remaining input,
obtaining a c-wsp.
The disambiguation theorems
fail-alt-rest-comp-when-match-cnl and
fail-conc-rest-comp-when-match-cnl
also have the hypothesis that parse-wsp fails
on the remaining input.
Without this hypothesis,
parse-alt-rest-comp or
parse-conc-rest-comp
could succeed:
after parsing the c-nl from the string at the leaves of the tree,
it could parse a WSP from the remaining input,
forming the first c-wsp
of a (*c-wsp "/" *c-wsp concatenation)
or of a *(1*c-wsp repetition),
and then proceed to parse more, eventually obtaining
a (*c-wsp "/" *c-wsp concatenation) or *(1*c-wsp repetition).
The hypothesis is stronger than needed,
because the presence of a WSP at the start of the remaining input
does not imply the success of
parse-alt-rest-comp or
parse-conc-rest-comp;
however, the stronger hypothesis keeps the theorems simpler
without precluding the eventual proof of
the top-level completeness theorem.
The disambiguation theorem fail-conc-rest-comp-when-match-*cwsp
has the hypotheses that
both parse-repetition and parse-cwsp
fail on the remaining input.
Without the first hypothesis,
parse-conc-rest-comp could succeed:
after parsing the *c-wsp from the string at the leaves of the trees,
assuming that there is at least one tree,
it could parse a repetition from the remaining input,
obtaining a (1*c-wsp repetition).
Without the second hypothesis,
parse-conc-rest-comp could also succeed:
after parsing the *c-wsp from the string at the leaves of the trees,
it could parse a c-wsp from the remaining input,
and then a repetition,
obtaining a (1*c-wsp repetition).
Hypotheses on the Tree(s)
Many disambiguation theorems include
hypotheses saying that the trees are terminated.
This ensures that the strings at the leaves of the trees
consist of natural numbers and not rule names,
since the incompatibilities with the parsing functions
are in terms of natural numbers.
Some disambiguation theorems do not need these hypotheses
because the syntactic entities can only be matched
by trees whose (starting) leaves are natural numbers.
For instance, in fail-dot-when-match-dash-etc,
the group ("-" ...) can only be matched by a tree
whose first leaf is a natural number,
upon which the incompatibility with the parsing function applies.
A few disambiguation theorems include hypotheses
that the tree(s) satisfy the disambiguating restrictions. These theorems say that parse-wsp fails
on the strings at the leaves of trees
that satisfy the disambiguating restrictions.
Since the restrictions say that these trees cannot start with WSP,
as the syntactic entities matched by the trees
would otherwise allow that,
these hypotheses are essential to the truth of these theorems.
Proof Methods
Most disambiguation theorems are proved by using, via :use hints,
parsing constraint theorems and tree matching constraint theorems
that explicate incompatible constraints
between the parsing functions
and the syntactic entities matched by the trees.
For example, in fail-sp-when-match-htab,
the fact that the tree matches HTAB induces the constraint that
the first natural number of the string at the leaves of the tree is 9,
but the fact that parse-sp succeeds induces the constraint that
the first natural number of the string at the leaves of the tree is 32.
The disambiguation theorems
fail-case-insensitive-string-when-match-case-sensitive-string and
fail-char-val-when-match-num/prose-val
have a :cases hint on whether
the string at the leaves of the tree has a second natural number or not.
Without this hint, the proof fails.
Perhaps this case split is related to the fact that
these disambiguation theorems are proved via constraints that involve
not only the first but also the second natural number in the string,
for LL(2) parts of the grammar.
The proofs of some disambiguation theorems
use other disambiguation theorems.
The former enable the latter explcitly, to use them as rewrite rules.
As explained earlier, some disambiguation theorems group together
multiple tree matching hypotheses or multiple parsing conclusions,
to reduce the potentially quadratic number of theorems.
This means that,
when some of these disambiguation theorems
are used in the proofs of others,
only ``parts'' of the former are actually used.
A disambiguation theorem about a list of trees matching a repetition,
such that another disambiguation theorem exists
about a tree matching the element of that repetition
and about the same parsing function,
is proved just by enabling the latter disambiguation theorem
and tree-list-match-repetition-p,
without any parsing constraint theorems
and tree matching constraint theorems.
For example, fail-bit-when-match-*cwsp is proved just by enabling
fail-bit/digit/hexdig/dot/dash-when-match-cwsp
(of which only the parse-bit failure is used here) and
tree-list-match-repetition-p.
Some disambiguation theorems are proved by
expanding the tree matching hypotheses
and the parsing function calls in the conclusions,
and enabling disambiguation theorems so that they apply to
the resulting subtree matching facts and called parsing functions;
we also enable
predicates like tree-terminatedp and recursive companions and
functions like tree->string and recursive companions,
so that they apply to the subtrees resulting from the matching expansion.
For example,
fail-alpha/digit/dash-when-match-alt-rest-comp is proved by
reducing the tree matching hypothesis to
a list of subtrees matching *c-wsp and a tree matching "/".
Then fail-alpha/digit/dash-when-match-cwsp
is used for the case in which the list of subtrees is not empty,
while fail-alpha/digit/dash-when-match-slash-/-close-round/square
(the slash part)
is used for the case in which the list of subtree is empty.
The proofs of some disambiguation theorems
use certain completeness theorems.
In some cases, this is related to LL(*) parts of the grammar:
the completeness theorems serve to go ``past''
the unbounded look-ahead,
before reaching the point where the constraints
from (sub)tree matching and (called) parsing functions are incompatible.
For example, fail-conc-rest-comp-when-match-alt-rest-comp
shows the incompatibility
between (*c-wsp "/" *c-wsp concatenation)
and (1*c-wsp repetition):
the completeness theorem parse-1*cwsp-when-tree-list-match
is used to go past the unbounded 1*c-wsp
that could start (*c-wsp "/" *c-wsp concatenation)
to show that repetition is incompatible with "/".
As another example, fail-*digit-star-*digit-when-match-1*digit
shows the incompatibility
between (*DIGIT "*" *DIGIT) and 1*DIGIT:
the completeness theorem parse-*digit-when-tree-list-match
is used to go past the unbounded *DIGIT
that could start 1*DIGIT
to show that "*" is incompatible with
the assumptions on the remaining input.
In other disambiguation theorems,
the use of completeness theorems
is not related to LL(*) parts of the grammar,
but is suggested by subgoals involving trees
and parsing functions called by the ones in the theorems' conclusions.
For example, in fail-cwsp-when-match-cnl,
the expansion of parse-cwsp and parse-cnl-wsp
produces a call to parse-cnl
on the string at the leaves of the tree
that the theorem hypothesizes to match c-nl:
thus, parse-cnl-when-tree-match applies here.
When a disambiguation theorem uses a completeness theorem,
the former appears in the file just after the latter,
with a comment referring to the completeness theorem used.
However, the disambiguation theorem is
under the manual topic about disambiguation theorems,
not under the manual topic about completeness theorems.
The disambiguation theorem fail-conc-rest-comp-when-match-*cwsp
uses, as a rewrite rule, the parsing failure propagation theorem fail-conc-rest-comp-when-fail-cwsp.
In some theorems, just enabling some functions does not suffice
to expand them in all the places where they need to be expanded
(presumably due to ACL2's heuristics for expanding recursive functions).
Thus, we use :expand hints in those cases.
Some of the disambiguation theorem proofs
do not seem as systematic as desired.
Two of them use :cases hints
(different from the ones discussed earlier,
which are related to LL(2) parts of the grammar),
one of them uses an :induct hint,
one of them uses a local lemma,
some use various rules about tree-list-match-repetition-p,
and some expand many definitions.
It may be possible to make these proofs more systematic,
by introducing and using
some additional ``intermediate'' disambiguation theorems
and some additional rules about the ABNF semantics.
Subtopics
- Grammar-parser-constraints-from-tree-matching
- Tree maching constraint theorems for the parser of ABNF grammars.
- Grammar-parser-constraints-from-parsing
- Parsing constraint theorems for the parser of ABNF grammars.
- Fail-bit/digit/hexdig/dot/dash-when-match-*cwsp-close-round/square
- Disambiguation between (i) any of
BIT, DIGIT, HEXDIG, ".", and "-" and
(ii) *c-wsp followed by ")" or "]".
- Fail-bit/digit/hexdig/dot/dash-when-match-alt-rest-comp
- Disambiguation between (i) any of
BIT, DIGIT, HEXDIG, ".", and "-" and
(ii) (*c-wsp "/" *c-wsp concatenation).
- Fail-slash/htab/sp/wsp/rep-when-match-cnl
- Disambiguation between
(i) any of
"/",
HTAB,
SP,
WSP, and
repetition and
(ii) c-nl.
- Fail-bit/digit/hexdig/dot/dash-when-match-slash
- Disambiguation between (i) any of
BIT, DIGIT, HEXDIG, ".", and "-" and
(ii) "/".
- Fail-bit/digit/hexdig/dot/dash-when-match-cwsp
- Disambiguation between (i) any of
BIT, DIGIT, HEXDIG, ".", and "-" and
(ii) c-wsp.
- Fail-bit/digit/hexdig/dot/dash-when-match-conc-rest-comp
- Disambiguation between (i) any of
BIT, DIGIT, HEXDIG, ".", and "-" and
(ii) (1*c-wsp repetition).
- Fail-bit/digit/hexdig/dot/dash-when-match-cnl
- Disambiguation between (i) any of
BIT, DIGIT, HEXDIG, ".", and "-" and
(ii) c-nl.
- Fail-bit/digit/hexdig/dot/dash-when-match-close-round/square
- Disambiguation between (i) any of
BIT, DIGIT, HEXDIG, ".", and "-" and
(ii) any of ")" and "]".
- Fail-wsp-when-match-*-rule-/-*cwsp-cnl-and-restriction
- Disambiguation between WSP and
*( rule / (*c-wsp c-nl) ) not followed by WSP,
when the list of trees satisfies the disambiguating restrictions.
- Fail-rulename-when-match-group/option-/-char/num/prose-val
- Disambiguation between rulename and
any of
group,
option,
char-val,
num-val, and
prose-val.
- Fail-a/b/c/d/e/f-when-match-other-a/b/c/d/e/f
- Disambiguation between any two distinct elements among
"A",
"B",
"C",
"D",
"E", and
"F".
- Fail-*digit-star-*digit-when-match-1*digit
- Disambiguation between (*DIGIT "*" *DIGIT)
and 1*DIGIT not followed by DIGIT or "*".
- Fail-digit-when-match-a/b/c/d/e/f
- Disambiguation between DIGIT and
any of
"A",
"B",
"C",
"D",
"E", and
"F".
- Fail-conc-rest-comp-when-match-*cwsp-close-round/square
- Disambiguation between (1*c-wsp repetition)
and *c-wsp followed by ")" or "]".
- Fail-conc-rest-comp-when-match-*cwsp
- Disambiguation between (1*c-wsp repetition)
and *c-wsp not followed by repetition or c-wsp.
- Fail-conc-rest-comp-when-match-alt-rest
- Disambiguation between (1*c-wsp repetition)
and *(*c-wsp "/" *c-wsp concatenation)
not followed by (1*c-wsp repetition).
- Fail-alt-rest-comp-when-match-*cwsp-close-round/square
- Disambiguation between (*c-wsp "/" *c-wsp concatenation)
and *c-wsp followed by ")" or "]".
- Fail-alpha/digit/dash-when-match-*cwsp-close-round/square
- Disambiguation between (ALPHA / DIGIT / "-") and
*c-wsp followed by ")" or "]".
- Fail-alpha/digit/dash-when-match-alt-rest
- Disambiguation between (ALPHA / DIGIT / "-") and
*(*c-wsp "/" *c-wsp concatenation)
not followed by (ALPHA / DIGIT / "-").
- Fail-wsp-when-match-rule-/-*cwsp-cnl-and-restriction
- Disambiguation between WSP and
any of rule and (*c-wsp c-nl),
when the tree satisfies the disambiguating restrictions.
- Fail-hexdig-when-match-alt-rest
- Disambiguation between HEXDIG and
*(*c-wsp "/" *c-wsp concatenation)
not followed by HEXDIG.
- Fail-group-when-match-option-/-char/num/prose-val
- Disambiguation between group and
any of option, char-val, num-val, and prose-val.
- Fail-dot-when-match-alt-rest
- Disambiguation between "." and
*(*c-wsp "/" *c-wsp concatenation)
not followed by ".".
- Fail-digit-when-match-alt-rest
- Disambiguation between DIGIT and
*(*c-wsp "/" *c-wsp concatenation)
not followed by DIGIT.
- Fail-dash-when-match-alt-rest
- Disambiguation between "-" and
*(*c-wsp "/" *c-wsp concatenation)
not followed by "-".
- Fail-cwsp-when-match-cnl
- Disambiguation between between c-wsp
and c-nl not followed by WSP.
- Fail-cwsp-when-match-alt/conc/rep
- Disambiguation between c-wsp and
any of alternation, concatenation, and repetition.
- Fail-conc-rest-comp-when-match-alt-rest-comp
- Disambiguation between (1*c-wsp repetition)
and (*c-wsp "/" *c-wsp concatenation).
- Fail-case-insensitive-string-when-match-case-sensitive-string
- Disambiguation between case-insensitive-string and
case-sensitive-string.
- Fail-bit-when-match-*cwsp
- Disambiguation between BIT and
*c-wsp not followed by BIT.
- Fail-alt-rest-comp-when-match-*cwsp
- Disambiguation between (*c-wsp "/" *c-wsp concatenation)
and *c-wsp
not followed by (*c-wsp "/" *c-wsp concatenation).
- Fail-alpha/digit/dash-when-match-slash-/-close-round/square
- Disambiguation between (ALPHA / DIGIT / "-") and
any of "/", ")", and "]".
- Fail-alpha/digit/dash-when-match-conc-rest
- Disambiguation between (ALPHA / DIGIT / "-") and
*(1*c-wsp repetition)
not followed by (ALPHA / DIGIT / "-").
- Fail-alpha/digit/dash-when-match-alt-rest-comp
- Disambiguation between (ALPHA / DIGIT / "-") and
(*c-wsp "/" *c-wsp concatenation).
- Fail-1st-range-when-match-2nd-range
- Disambiguation between two disjoint numeric ranges.
- Fail-wsp-when-match-*cwsp-cnl-and-restriction
- Disambiguation between WSP and (*c-wsp c-nl)
when the tree satisfies the disambiguating restrictions.
- Fail-wsp-when-match-vchar-/-rule-/-cnl-wsp
- Disambiguation between WSP and
any of VCHAR, rule, and (c-nl WSP).
- Fail-wsp-when-match-cwsp-and-restriction
- Disambiguation between WSP and c-wsp,
when the tree satisfies the disambiguating restrictions.
- Fail-repetition-when-match-slash-/-close-round/square
- Disambiguation between repetition and
any of "/", ")", and "]".
- Fail-option-when-match-char/num/prose-val
- Disambiguation between option and
any of char-val, num-val, and prose-val.
- Fail-hexdig-when-match-hex-val-rest
- Disambiguation between HEXDIG and
[ 1*("." 1*HEXDIG) / ("-" 1*HEXDIG) ]
not followed by HEXDIG.
- Fail-hexdig-when-match-conc-rest
- Disambiguation between HEXDIG and
*(1*c-wsp repetition)
not followed by HEXDIG.
- Fail-equal-slash-when-match-equal-and-rest-fail-slash
- Disambiguation between "=/" and
"=" not followed by "/".
- Fail-dot-when-match-dash-etc
- Disambiguation between "." and ("-" ...).
- Fail-dot-when-match-conc-rest
- Disambiguation between "." and
*(1*c-wsp repetition)
not followed by ".".
- Fail-digit/star-when-match-element
- Disambiguation between (i) any of DIGIT and "*" and
(ii) element.
- Fail-digit-when-match-dec-val-rest
- Disambiguation between DIGIT and
[ 1*("." 1*DIGIT) / ("-" 1*DIGIT) ]
not followed by DIGIT.
- Fail-digit-when-match-conc-rest
- Disambiguation between DIGIT and
*(1*c-wsp repetition)
not followed by DIGIT.
- Fail-dash-when-match-conc-rest
- Disambiguation between "-" and
*(1*c-wsp repetition)
not followed by "-".
- Fail-cwsp-when-match-slash-/-close-round/square
- Disambiguation between c-wsp and
any of "/", ")", and "]".
- Fail-conc-rest-comp-when-match-cnl
- Disambiguation between (1*c-wsp repetition)
and c-nl not followed by WSP.
- Fail-char-val-when-match-num/prose-val
- Disambiguation between char-val and
any of num-val and prose-val.
- Fail-bit-when-match-*-dot-1*bit
- Disambiguation between BIT and
*("." 1*BIT) not followed by BIT.
- Fail-bit-when-match-conc-rest
- Disambiguation between BIT and
*(1*c-wsp repetition)
not followed by BIT.
- Fail-bit-when-match-bin-val-rest
- Disambiguation between BIT and
[ 1*("." 1*BIT) / ("-" 1*BIT) ]
not followed by BIT.
- Fail-bit-when-match-alt-rest
- Disambiguation between BIT and
*(*c-wsp "/" *c-wsp concatenation)
not followed by BIT.
- Fail-alt-rest-comp-when-match-cnl
- Disambiguation between (*c-wsp "/" *c-wsp concatenation)
and c-nl not followed by WSP.
- Fail-alpha/digit/dash-when-match-*cwsp
- Disambiguation between (ALPHA / DIGIT / "-") and
*c-wsp not followed by (ALPHA / DIGIT / "-").
- Fail-1*cwsp-when-match-slash-/-close-round/square
- Disambiguation between 1*c-wsp and
any of "/", ")", and "]".
- Fail-sp-when-match-htab
- Disambiguation between SP and HTAB.
- Fail-slash-when-match-*cwsp
- Disambiguation between "/" and
*c-wsp not followed by "/".
- Fail-slash-when-match-close-round/square
- Disambiguation between "/" and
any of ")" and "]".
- Fail-hexdig-when-match-*cwsp
- Disambiguation between HEXDIG and
*c-wsp not followed by HEXDIG.
- Fail-hexdig-when-match-*-dot-1*hexdig
- Disambiguation between HEXDIG and
*("." 1*HEXDIG) not followed by HEXDIG.
- Fail-dot-when-match-*cwsp
- Disambiguation between "." and
*c-wsp not followed by ".".
- Fail-digit-when-match-*cwsp
- Disambiguation between DIGIT and
*c-wsp not followed by DIGIT.
- Fail-digit-when-match-*-dot-1*digit
- Disambiguation between DIGIT and
*("." 1*DIGIT) not followed by DIGIT.
- Fail-digit-when-match-star/dash
- Disambiguation between DIGIT and
any of "*" and "-".
- Fail-dash-when-match-*cwsp
- Disambiguation between "-" and
*c-wsp not followed by "=".
- Fail-bin-val-when-match-dec/hex-val
- Disambiguation between bin-val and
any of dec-val and hex-val.
- Fail-alpha/digit/dash-when-match-defined-as
- Disambiguation between (ALPHA / DIGIT / "-") and
defined-as.
- Fail-alpha/digit/dash-when-match-cwsp
- Disambiguation between (ALPHA / DIGIT / "-") and c-wsp.
- Fail-alpha/digit/dash-when-match-conc-rest-comp
- Disambiguation between (ALPHA / DIGIT / "-") and
(1*c-wsp repetition).
- Fail-alpha-when-match-digit/dash
- Disambiguation between ALPHA and
any of DIGIT and "-".
- Fail-%i-when-match-quoted-string
- Disambiguation between "%i" and quoted-string.
- Fail-wsp/vchar-when-match-crlf
- Disambiguation between (WSP / VCHAR) and CRLF.
- Fail-slash-when-match-elements
- Disambiguation between "/" and elements.
- Fail-rule-when-match-*cwsp-cnl
- Disambiguation between rule and (*c-wsp c-nl).
- Fail-num-val-when-match-prose-val
- Disambiguation between num-val and prose-val.
- Fail-either-range-when-match-dquote
- Disambiguation between (%x20-21 / %x23-7E) and DQUOTE.
- Fail-either-range-when-match-close-angle
- Disambiguation between (%x20-3D / %x3F-7E) and ">".
- Fail-dec-val-when-match-hex-val
- Disambiguation between dec-val and hex-val.
- Fail-cwsp-when-match-equal-/-equal-slash
- Disambiguation between c-wsp and
any of "=" and "=/".
- Fail-cwsp-when-match-elements
- Disambiguation between c-wsp and elements.
- Fail-comment-when-match-crlf
- Disambiguation between comment and CRLF.
- Fail-alpha/digit/dash-when-match-cnl
- Disambiguation between (ALPHA / DIGIT / "-") and c-nl.
- Fail-0-when-match-1
- Disambiguation between "0" and "1".