All the HTTP grammar rules, including the referenced URI rules and ABNF core rules.
The HTTP grammar rules include rules defined by prose notation
that refer to the URI grammar rules.
To obtain the complete HTTP grammar rules,
we plug into the HTTP rules the URI rules.
Since the rule
The resulting rules are well-formed and closed, and generate terminal strings consisting only of octets.
Section 1.2 of RFC 7230 lists a number of ABNF core rules
that are included by reference in the HTTP grammar rules.
With the exception of
We keep this constant unexpanded in output.
Definition:
(defconst *all-http-grammar-rules* (plug-rules (plug-rules *http-grammar-rules* (rulelist-rename-rule *uri-grammar-rules* (rulename "host") (rulename "uri-host"))) *core-rules*))
Function:
(defun untranslate-preprocess-*all-http-grammar-rules* (acl2::term acl2::wrld) (if (equal acl2::term (list 'quote *all-http-grammar-rules*)) '*all-http-grammar-rules* (untranslate-preprocess-*http-grammar-rules* acl2::term acl2::wrld)))
Theorem:
(defthm rulelist-wfp-of-*all-http-grammar-rules* (rulelist-wfp *all-http-grammar-rules*))
Theorem:
(defthm rulelist-closedp-of-*all-http-grammar-rules* (rulelist-closedp *all-http-grammar-rules*))
Theorem:
(defthm octet-only-*all-http-grammar-rules* (rulelist-in-termset-p *all-http-grammar-rules* (integers-from-to 0 255)))
Theorem:
(defthm abnf-core-rules-in-*all-http-grammar-rules* (implies (member-equal core-rule *core-rules*) (iff (member-equal core-rule *all-http-grammar-rules*) (member-equal core-rule (list *rule_alpha* *rule_cr* *rule_crlf* *rule_digit* *rule_dquote* *rule_hexdig* *rule_htab* *rule_lf* *rule_octet* *rule_sp* *rule_vchar*)))) :rule-classes nil)