Parsing constraint theorems for the parser of ABNF grammars.
If a parsing function succeeds, the parsed input must satisfy certain constraints. For example, if parse-alpha succeeds, the input must be non-empty and start with (the ASCII code of) a letter. As another example, if parse-comment succeeds, the input must be non-empty and start with (the ASCII code of) a semicolon.
The parsing constraint theorems below capture constraints of this kind.
These theorems are used, together with the tree matching constraint theorems, to prove the disambiguation theorems, which in turn are used to prove the completeness theorems.
The parsing constraint theorems have no rule classes.
They are used in the proofs of the disambiguation theorems
via
There are parsing constraint theorems only for some of the parsing functions: just the ones used to prove the disambiguation theorems. Furthermore, each parsing constraint theorem only states necessary, but generally not sufficient, conditions for the success of the corresponding parsing function: it states only the constraints used to prove the disambiguation theorems.
Most parsing constraint theorems state constraints just on the first natural number of the input (the car), because most of the grammar is LL(1); these constraints correspond to `first sets' in LL(1) parsing theory. A few parsing constraint theorems state additional constraints on the second natural number of the input (the cadr), as needed for the LL(2) portions of the grammar.
The proof of each parsing constraint theorem
uses the definition of the corresponding parsing function,
e.g. constraints-from-parse-alpha uses
the definition of parse-alpha.
In constraints-from-parse-repetition,
parse-repetition does not get expanded even if it is enabled
(presumably due to ACL2's heuristics for expanding recursive functions);
thus, we use an explcit
When a parsing function calls another parsing function
that has a parsing constraint theorem,
this theorem is used (via a
Since constraints-from-parse-ichar and constraints-from-parse-ichar2 state constraints with nat-match-insensitive-char-p, and since those two theorems are used in the proofs of many other parsing constraint theorems, the proofs of the latter theorems use the definition nat-match-insensitive-char-p. To avoid enabling it explicitly in many theorems, we enable nat-match-insensitive-char-p just before the parsing constraint theorems and we disable it just after.