		Search-engine friendly clone of the ACL2 documentation.

Concrete-syntax

Grammar

ABNF grammar for PFCSes.

As in other languages, the grammar consists of two sub-grammars: a lexical (sub)grammar and a syntactic (sub)grammar. These are both in the same ABNF grammar file.

Subtopics

Abnf-tree-with-root-p: Recognize CSTs whose root is the given rule name, for the ABNF grammar of PFCS.
Cst-token-conc?
Cst-list-list-conc-matchp$
Cst-list-list-alt-matchp$
Cst-whitespace-conc?
Cst-constraint-conc?
Cst-list-rep-matchp$
Cst-list-elem-matchp$
Cst-letter-conc?
Cst-lexeme-conc?
Abnf-tree-wrap-fn
Abnf-tree-wrap: Wrap a CST into a nest of CSTs with the given rule names as roots (in the order given) and each with a single subtree, ending with the original tree.
Cst-matchp$
*grammar*: The grammar of PFCSes, in ACL2.
Cst-whitespace-conc2-rep-elem
Cst-whitespace-conc1-rep-elem
Cst-constraint-conc2-rep-elem
Cst-constraint-conc1-rep-elem
Cst-whitespace-conc2-rep
Cst-whitespace-conc1-rep
Cst-uppercase-letter-conc-rep-elem
Cst-uppercase-letter-conc-rep
Cst-relation-constraint-conc
Cst-lowercase-letter-conc-rep-elem
Cst-lowercase-letter-conc-rep
Cst-lexeme-conc2-rep-elem
Cst-lexeme-conc1-rep-elem
Cst-letter-conc2-rep-elem
Cst-letter-conc1-rep-elem
Cst-equality-constraint-conc
Cst-constraint-conc2-rep
Cst-constraint-conc1-rep
Cst-carriage-return-conc-rep-elem
Cst-carriage-return-conc-rep
Cst-whitespace-conc2
Cst-whitespace-conc1
Cst-uppercase-letter-conc
Cst-token-conc4-rep-elem
Cst-token-conc3-rep-elem
Cst-token-conc2-rep-elem
Cst-token-conc1-rep-elem
Cst-lowercase-letter-conc
Cst-line-terminator-conc
Cst-line-feed-conc-rep-elem
Cst-lexeme-conc2-rep
Cst-lexeme-conc1-rep
Cst-letter-conc2-rep
Cst-letter-conc1-rep
Cst-expression-conc-rep-elem
Cst-constraint-conc2
Cst-constraint-conc1
Cst-carriage-return-conc
Cst-token-conc4-rep
Cst-token-conc4
Cst-token-conc3-rep
Cst-token-conc3
Cst-token-conc2-rep
Cst-token-conc2
Cst-token-conc1-rep
Cst-token-conc1
Cst-space-conc-rep-elem
Cst-line-feed-conc-rep
Cst-line-feed-conc
Cst-lexeme-conc2
Cst-lexeme-conc1
Cst-letter-conc2
Cst-letter-conc1
Cst-identifier-conc
Cst-expression-conc-rep
Cst-expression-conc
Cst-digit-conc-rep-elem
Cst-definition-conc
Cst-system-conc
Cst-space-conc-rep
Cst-space-conc
Cst-numeral-conc
Cst-integer-conc
Cst-digit-conc-rep
Cst-digit-conc
Abnf-tree-list-with-root-p: Lift abnf-tree-with-root-p to lists.
Cst-%x61-7a-nat
Cst-%x41-5a-nat
Cst-%x30-39-nat