*all-http-message-grammar-rules*
All the HTTP grammar rules
that define the first-level structure of messages.
Starting from the top-level rule HTTP-message that defines messages,
not all the rules in *all-http-grammar-rules* are reached
when generating strings of terminals.
The rules that are not reached serve to define
the format of certain field values and
the format for the chunked transfer coding.
The rules reached starting from HTTP-message provide
a first-level definition of messages.
According to these rules, strings of terminals (octets)
are parsed into trees rooted at HTTP-message.
In these parse trees, field values are ``opaque'',
i.e. they are essentially unstructured sequences of certain octets,
according to the field-content rule.
These field values can be parsed further according to the other rules.
The rules reached starting from HTTP-message
are well-formed and closed.
Since they are a subset of *all-http-grammar-rules*,
they also generate terminal strings consisting only of octets.
Definition: *all-http-message-grammar-rules*
(defconst *all-http-message-grammar-rules*
(trans-rules-of-names (list (rulename "HTTP-message"))
*all-http-grammar-rules*))
Definitions and Theorems
Theorem: rulelist-wfp-of-*all-http-message-grammar-rules*
(defthm rulelist-wfp-of-*all-http-message-grammar-rules*
(rulelist-wfp *all-http-message-grammar-rules*))
Theorem: rulelist-closedp-of-*all-http-message-grammar-rules*
(defthm rulelist-closedp-of-*all-http-message-grammar-rules*
(rulelist-closedp *all-http-message-grammar-rules*))
