In-terminal-set
ABNF grammars that generate only terminals in given sets.
If all the terminal value notations used in a rule list denote values
that belong to a certain set of terminals (natural numbers),
then the terminal strings of that rule list
consist of only terminals that belong to that set.
This is proved below.
For example, if all the terminal value notations are octets,
the terminal strings consist of octets
and can be parsed starting from character strings
(since ACL2::characters are isomorphic to octets)
instead of natural numbers.
Subtopics
- Leaves-in-termset-when-match-alt/conc/rep/elem-in-termset
- Alternations, concatenation, repetitions, and elements
whose terminal value notations all denote values in a set,
can be matched only by (lists of (lists of)) trees
whose terminal leaves are in the set.
- Symbol-in-termset-p
- Check if a symbol is either a rule name or a natural number in a set.
- Rulelist-in-termset-p
- Check if all the terminal value notations in a list of rules
denote values in a set.
- String-in-termset-p
- Check if a string consists of terminals in a set and rule names.
- Char-insensitive-in-termset-p
- Check if the code of a character,
as well as the codes of its uppercase or lowercase counterparts,
are in a set.
- Chars-sensitive-in-termset-p
- Lift char-sensitive-in-termset-p to lists.
- Chars-insensitive-in-termset-p
- Lift char-insensitive-in-termset-p to lists.
- Concatenation-in-termset-p
- Check if all the terminal value notations in a concatenation
denote values in a set.
- Char-val-in-termset-p
- Check if a character value notation denotes values in a set.
- Alternation-in-termset-p
- Check if all the terminal value notations in an alternation
denote values in a set.
- Prose-val-in-termset-p
- A prose value notation is unconstrained,
so it cannot be guaranteed to denote values in a set.
- Num-val-in-termset-p
- Check if a numeric value notation denotes values in a set.
- Char-sensitive-in-termset-p
- Check if the code of a character is in a set.
- Rule-in-termset-p
- Check if all the terminal value notations in a rule
denote values in a set.
- Repetition-in-termset-p
- Check if all the terminal value notations in a repetition
denote values in a set,
or the repetition consists of zero instances.
- Terminal-strings-in-termset-when-rules-in-termset
- Rules whose terminal value notations all denote values in a set,
generate terminal strings consisting of terminals in the set.
- Element-in-termset-p
- Check if all the terminal value notations in an element
denote values in a set.
- Nats-in-termset-when-match-sensitive-chars-in-termset
- Lemma to prove
leaves-in-termset-when-match-char-val-in-termset.
- Nats-in-termset-when-match-insensitive-chars-in-termset
- Lemma to prove
leaves-in-termset-when-match-char-val-in-termset.
- Leaves-in-termset-when-match-char-val-in-termset
- Character value notations that denote terminals in a set
can be matched only by trees whose terminal leaves are in the set.
- Nat-in-termset-when-match-sensitive-char-in-termset
- Lemma to prove
nats-in-termset-when-match-sensitive-chars-in-termset.
- Nat-in-termset-when-match-insensitive-char-in-termset
- Lemma to prove
nats-in-termset-when-match-insensitive-chars-in-termset.
- Leaves-in-termset-when-match-num-val-in-termset
- Numeric value notations that denote values in a set
can be matched only by trees whose terminal leaves are in the set.
