Rule list that *concrete-syntax-rules-parsed* abstracts to.
Applying the grammar abstractor to the parse tree
obtained by applying the grammar parser
to the file
Furthermore, the rule list thus obtained is identical to *concrete-syntax-rules*, which is the definition of the concrete syntax of ABNF written manually using the abstract syntax of ABNF.
We use add-const-to-untranslate-preprocess to keep this constant unexpanded in output.
Definition:
(defconst *concrete-syntax-rules-parsed-and-abstracted* (abstract-rulelist *concrete-syntax-rules-parsed*))
Function:
(defun untranslate-preprocess-*concrete-syntax-rules-parsed-and-abstracted* (acl2::term acl2::wrld) (if (equal acl2::term (list 'quote *concrete-syntax-rules-parsed-and-abstracted*)) '*concrete-syntax-rules-parsed-and-abstracted* (untranslate-preprocess-*core-rules-parsed-and-abstracted* acl2::term acl2::wrld)))
Theorem:
(defthm *concrete-syntax-rules-parsed-and-abstracted*-correct (equal *concrete-syntax-rules-parsed-and-abstracted* *concrete-syntax-rules*) :rule-classes nil)