		Search-engine friendly clone of the ACL2 documentation.

Grammar

grammar

The grammar of PFCSes, in ACL2.

We use our verified ABNF grammar parser and our ABNF grammar 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*.