		Search-engine friendly clone of the ACL2 documentation.

Grammar

grammar

The grammar of C, in ACL2.

We use our verified grammar parser and our abstractor to turn the grammar in the grammar.abnf file into an ACL2 representation.

We use ACL2::add-const-to-untranslate-preprocess to keep this constant unexpanded in output.

We show that the grammar is well-formed, closed, and ASCII.

Definitions and Theorems

Function: untranslate-preprocess-*grammar*

(defun untranslate-preprocess-*grammar* (acl2::term acl2::wrld)
  (if (equal acl2::term (list 'quote *grammar*))
      '*grammar*
    (abnf::untranslate-preprocess-*grammar* acl2::term acl2::wrld)))

Theorem: rulelist-wfp-of-*grammar*

(defthm rulelist-wfp-of-*grammar*
  (abnf::rulelist-wfp *grammar*))

Theorem: rulelist-closedp-of-*grammar*

(defthm rulelist-closedp-of-*grammar*
  (abnf::rulelist-closedp *grammar*))

Theorem: ascii-only-*grammar*

(defthm ascii-only-*grammar*
  (abnf::rulelist-in-termset-p *grammar*
                               (acl2::integers-from-to 0 127)))

Subtopics

*grammar*-tree-operations: Tree operations specialized to *grammar*.