		Search-engine friendly clone of the ACL2 documentation.

Uri-example

all-uri-grammar-rules

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

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

The resulting rules are well-formed and closed. They generate terminal strings consisting only of ASCII codes; more precisely, the ASCII codes of all the visible characters (i.e. VCHAR in the ABNF core rules) except double quote, angle brackets, backslash, caret, curly braces, and vertical bar.

We keep this constant unexpanded in output.

Definition: *all-uri-grammar-rules*

(defconst *all-uri-grammar-rules*
  (plug-rules *uri-grammar-rules* *core-rules*))

Definitions and Theorems

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

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

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

(defthm rulelist-wfp-of-*all-uri-grammar-rules*
  (rulelist-wfp *all-uri-grammar-rules*))

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

(defthm rulelist-closedp-of-*all-uri-grammar-rules*
  (rulelist-closedp *all-uri-grammar-rules*))

Theorem: ascii-only-*all-uri-grammar-rules*

(defthm ascii-only-*all-uri-grammar-rules*
  (rulelist-in-termset-p *all-uri-grammar-rules*
                         (integers-from-to 0 127)))

Theorem: precise-ascii-codes-of-*all-uri-grammar-rules*

(defthm precise-ascii-codes-of-*all-uri-grammar-rules*
  (rulelist-in-termset-p *all-uri-grammar-rules*
                         (difference (integers-from-to 33 126)
                                     (list (char-code #\")
                                           (char-code #\<)
                                           (char-code #\>)
                                           (char-code #\\)
                                           (char-code #\^)
                                           (char-code #\{)
                                           (char-code #\|)
                                           (char-code #\})))))

Theorem: abnf-core-rules-in-*all-uri-grammar-rules*

(defthm abnf-core-rules-in-*all-uri-grammar-rules*
  (implies (member-equal core-rule *core-rules*)
           (iff (member-equal core-rule *all-uri-grammar-rules*)
                (member-equal core-rule
                              (list *rule_alpha*
                                    *rule_digit* *rule_hexdig*))))
  :rule-classes nil)

Subtopics

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