Semantics of ABNF.

The abstract syntactic entities of ABNF denote tree structures built by expanding the rules. When all the rule names are expanded, the leaves of the tree form a sequence of terminal values, for which the tree is a parse tree.

These concepts are analogous to the ones for the typical notion of formal grammar in textbooks, but because ABNF is more complex, its semantics are more complex.

- Tree-terminatedp
- Notion of terminated tree.
- Tree->string
- String at the leaves of trees.
- String-has-finite-parse-trees-p
- Check if a string has a finite number of parse trees.
- Parse-trees-of-string-p
- Check if a finite set of trees is the set of all and only the parse trees of a string.
- Tree-match-element-p
- Semantics of elements.
- Parse-treep
- Recognize the parse trees of a string, with respect to a rule name and a list of rules.
- Symbol
- Symbols.
- String-unambiguousp
- Notion of unambiguous string.
- Nat-match-insensitive-char-p
- Semantics of characters in case-insensitive character value notations.
- Tree-match-num-val-p
- Semantics of numeric value notations.
- Nats-match-insensitive-chars-p
- Lifting of
`nat-match-insensitive-char-p`to lists. - Tree-option
- Union of trees and
nil . - String-parsablep
- Notion of parsable string.
- Numrep-match-repeat-range-p
- Semantics of repetition ranges.
- Nats-match-sensitive-chars-p
- Lifting of
`nat-match-sensitive-char-p`to lists. - Lookup-rulename
- Collect all the alternatives associated to a rule name from some rules.
- String-ambiguousp
- Notion of ambiguous string.
- Tree-match-char-val-p
- Semantics of character value notations.
- Tree-list-match-repetition-p
- Semantics of repetitions.
- Nat-match-sensitive-char-p
- Semantics of characters in case-sensitive character value notations.
- Parse
- Parse a string.
- Tree-match-prose-val-p
- Semantics of prose value notations.
- Tree-option-result
- Fixtype of errors and optional trees.
- Tree-list-result
- Fixtype of errors and lists of trees.
- Tree-list-list-result
- Fixtype of errors and lists of lists of trees.
- Tree-result
- Fixtype of errors and trees.
- Languagep
- Notion of language.
- Tree-list-list-match-concatenation-p
- Semantics of concatenations.
- Terminal-string-for-rules-p
- Recognize terminal strings generated by a grammar.
- Tree-list-list-match-alternation-p
- Semantics of alternations.
- Tree-list-match-element-p
- Auxiliary function to define
`tree-list-match-repetition-p`. - Parse!
- Parse an unambiguous string.
- Theorems-about-terminated-trees-matching-elements
- Some theorems about terminated trees matching certain elements.
- String
- Strings.
- Tree-set
- Finite sets of trees.
- Trees