		Search-engine friendly clone of the ACL2 documentation.

Meta-circular-validation

concrete-syntax-rules-parsed-and-abstracted

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 concrete-syntax-rules.abnf, yields a list of rules. This shows that the abstractor abstracts the parsed definition of the concrete syntax of ABNF without errors.

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: *concrete-syntax-rules-parsed-and-abstracted*

(defconst *concrete-syntax-rules-parsed-and-abstracted*
  (abstract-rulelist *concrete-syntax-rules-parsed*))

Definitions and Theorems

Function: untranslate-preprocess-*concrete-syntax-rules-parsed-and-abstracted*

(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: *concrete-syntax-rules-parsed-and-abstracted*-correct

(defthm *concrete-syntax-rules-parsed-and-abstracted*-correct
  (equal *concrete-syntax-rules-parsed-and-abstracted*
         *concrete-syntax-rules*)
  :rule-classes nil)