		Search-engine friendly clone of the ACL2 documentation.

Grammar-old

grammar-old

The parsed old ABNF grammar of Yul.

We parse the grammar file to obtain an ABNF grammar value.

We prove that the grammar is well-formed, is closed, and only generates terminals in the Unicode character set.

Definitions and Theorems

Function: untranslate-preprocess-*grammar-old*

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

Theorem: rulelist-wfp-of-*grammar-old*

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

Theorem: rulelist-closedp-of-*grammar-old*

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

Theorem: unicode-only-*grammar-old*

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