All the SMTP grammar rules, including the referenced ABNF core rules.
The SMTP grammar references
The resulting rules are well-formed and closed. They generate terminal strings consisting only of ASCII codes
We keep this constant unexpanded in output.
Definition:
(defconst *all-smtp-grammar-rules* (plug-rules (plug-rules *smtp-grammar-rules* (rulelist-rename-rule (rulelist-rename-rule (rulelist-rename-rule (rulelist-rename-rule *imf-grammar-rules* (rulename "local-part") (rulename "imf-local-part")) (rulename "quoted-string") (rulename "imf-quoted-string")) (rulename "domain") (rulename "imf-domain")) (rulename "atom") (rulename "imf-atom"))) *core-rules*))
Function:
(defun untranslate-preprocess-*all-smtp-grammar-rules* (acl2::term acl2::wrld) (if (equal acl2::term (list 'quote *all-smtp-grammar-rules*)) '*all-smtp-grammar-rules* (untranslate-preprocess-*smtp-grammar-rules* acl2::term acl2::wrld)))
Theorem:
(defthm rulelist-wfp-of-*all-smtp-grammar-rules* (rulelist-wfp *all-smtp-grammar-rules*))
Theorem:
(defthm rulelist-closedp-of-*all-smtp-grammar-rules* (rulelist-closedp *all-smtp-grammar-rules*))
Theorem:
(defthm ascii-only-*all-smtp-grammar-rules* (rulelist-in-termset-p *all-smtp-grammar-rules* (integers-from-to 0 127)))
Theorem:
(defthm abnf-core-rules-in-*all-smtp-grammar-rules* (implies (member-equal core-rule *core-rules*) (iff (member-equal core-rule *all-smtp-grammar-rules*) (member-equal core-rule (list *rule_alpha* *rule_cr* *rule_crlf* *rule_digit* *rule_dquote* *rule_hexdig* *rule_htab* *rule_lf* *rule_sp* *rule_vchar* *rule_wsp*)))) :rule-classes nil)