		Search-engine friendly clone of the ACL2 documentation.

Grammar

all-grammar-rules

All the JSON grammar rules, including the referenced ABNF core rules.

These are obtained by plugging the core rules into the IMAP rules.

These rules are well-formed and closed.

These rules generate terminal strings consisting only of Unicode codes, i.e. natural numbers between 0 and x10FFFF. Proving this by execution would take a long time due to the specification-appropriate but execution-inefficient definition of abnf::rulelist-in-termset-p and to the relatively large size of the range of natural numbers. Thus, we prove the theorems (quickly) by disabling the executable counterpart of ACL2::integers-from-to and by using library theorems that relate ACL2::integers-from-to to in and set::list-in.

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

Definition: *all-grammar-rules*

(defconst *all-grammar-rules*
  (abnf::plug-rules *grammar-rules* abnf::*core-rules*))

Definitions and Theorems

Function: untranslate-preprocess-*all-grammar-rules*

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

Theorem: rulelist-wfp-of-*all-grammar-rules*

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

Theorem: rulelist-closedp-of-*all-grammar-rules*

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

Theorem: unicode-only-*all-grammar-rules*

(defthm unicode-only-*all-grammar-rules*
  (abnf::rulelist-in-termset-p *all-grammar-rules*
                               (acl2::integers-from-to 0 1114111)))

Subtopics

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